Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support const evaluation #736

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions chalk-engine/src/slg.rs
Original file line number Diff line number Diff line change
Expand Up @@ -293,6 +293,8 @@ impl<I: Interner> MayInvalidate<I> {

// Only variants left are placeholder = concrete, which always fails
(ConstValue::Placeholder(_), _) | (ConstValue::Concrete(_), _) => true,

_ => todo!(),
}
}

Expand Down
2 changes: 2 additions & 0 deletions chalk-engine/src/slg/aggregate.rs
Original file line number Diff line number Diff line change
Expand Up @@ -551,6 +551,8 @@ impl<I: Interner> AntiUnifier<'_, I> {
(ConstValue::Placeholder(_), _) | (_, ConstValue::Placeholder(_)) => {
self.new_const_variable(ty)
}

_ => todo!(),
}
}

Expand Down
11 changes: 11 additions & 0 deletions chalk-engine/src/slg/resolvent.rs
Original file line number Diff line number Diff line change
Expand Up @@ -687,17 +687,28 @@ impl<'i, I: Interner> Zipper<I> for AnswerSubstitutor<'i, I> {
Ok(())
}

(ConstValue::Function(name1, args1), ConstValue::Function(name2, args2)) => {
assert!(name1 == name2);
Ok(())
}

(ConstValue::Function(..), ConstValue::Concrete(_)) | (ConstValue::Concrete(_), ConstValue::Function(..)) => {
Ok(())
}

(ConstValue::InferenceVar(_), _) | (_, ConstValue::InferenceVar(_)) => panic!(
"unexpected inference var in answer `{:?}` or pending goal `{:?}`",
answer, pending,
),

(ConstValue::BoundVar(_), _)
| (ConstValue::Placeholder(_), _)
| (ConstValue::Function(..), _)
| (ConstValue::Concrete(_), _) => panic!(
"structural mismatch between answer `{:?}` and pending goal `{:?}`",
answer, pending,
),

}
}

Expand Down
8 changes: 5 additions & 3 deletions chalk-integration/src/db.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
use crate::{
error::ChalkError,
interner::ChalkIr,
interner::{ChalkIr, ConstEval},
lowering::lower_goal,
program::Program,
query::{Lowering, LoweringDatabase},
Expand All @@ -26,13 +26,15 @@ use std::sync::Arc;
#[derive(Default)]
pub struct ChalkDatabase {
storage: salsa::Storage<Self>,
interner: ChalkIr,
}

impl Database for ChalkDatabase {}

impl ChalkDatabase {
pub fn with(program_text: &str, solver_choice: SolverChoice) -> Self {
pub fn with(program_text: &str, const_eval: ConstEval, solver_choice: SolverChoice) -> Self {
let mut db = ChalkDatabase::default();
db.interner.const_eval_fn = const_eval;
db.set_program_text(Arc::new(program_text.to_string()));
db.set_solver_choice(solver_choice);
db
Expand Down Expand Up @@ -174,7 +176,7 @@ impl RustIrDatabase<ChalkIr> for ChalkDatabase {
}

fn interner(&self) -> ChalkIr {
ChalkIr
self.interner
}

fn is_object_safe(&self, trait_id: TraitId<ChalkIr>) -> bool {
Expand Down
18 changes: 17 additions & 1 deletion chalk-integration/src/interner.rs
Original file line number Diff line number Diff line change
Expand Up @@ -50,10 +50,22 @@ impl Debug for ChalkFnAbi {
}
}

pub type ConstEval = fn(String, Vec<u32>) -> u32;

/// The default "interner" and the only interner used by chalk
/// itself. In this interner, no interning actually occurs.
#[derive(Debug, Copy, Clone, Hash, PartialOrd, Ord, PartialEq, Eq)]
pub struct ChalkIr;
pub struct ChalkIr {
pub const_eval_fn: ConstEval,
}

impl Default for ChalkIr {
fn default() -> Self {
ChalkIr {
const_eval_fn: |_, _| panic!("const eval is not supported on this interner"),
}
}
}

impl Interner for ChalkIr {
type InternedType = Arc<TyData<ChalkIr>>;
Expand Down Expand Up @@ -265,6 +277,10 @@ impl Interner for ChalkIr {
c1 == c2
}

fn const_eval(&self, name: String, args: Vec<u32>) -> u32 {
(self.const_eval_fn)(name, args)
}

fn intern_generic_arg(self, generic_arg: GenericArgData<ChalkIr>) -> GenericArgData<ChalkIr> {
generic_arg
}
Expand Down
15 changes: 12 additions & 3 deletions chalk-integration/src/lowering.rs
Original file line number Diff line number Diff line change
Expand Up @@ -108,7 +108,7 @@ lower_param_map!(
);

fn get_type_of_usize() -> chalk_ir::Ty<ChalkIr> {
chalk_ir::TyKind::Scalar(chalk_ir::Scalar::Uint(chalk_ir::UintTy::Usize)).intern(ChalkIr)
chalk_ir::TyKind::Scalar(chalk_ir::Scalar::Uint(chalk_ir::UintTy::Usize)).intern(ChalkIr::default())
}

impl Lower for VariableKind {
Expand Down Expand Up @@ -818,6 +818,14 @@ impl LowerWithEnv for Const {
fn lower(&self, env: &Env) -> LowerResult<Self::Lowered> {
let interner = env.interner();
match self {
Const::Function(f) => Ok(chalk_ir::ConstData {
ty: get_type_of_usize(),
value: chalk_ir::ConstValue::Function(
f.name.to_string(),
f.args.iter().map(|x| x.lower(env)).collect::<Result<Vec<_>, _>>()?,
),
}
.intern(interner)),
Const::Id(name) => {
let parameter = env.lookup_generic_arg(name)?;
parameter
Expand Down Expand Up @@ -1013,7 +1021,7 @@ impl LowerWithEnv for (&TraitDefn, chalk_ir::TraitId<ChalkIr>) {
}

pub fn lower_goal(goal: &Goal, program: &LoweredProgram) -> LowerResult<chalk_ir::Goal<ChalkIr>> {
let interner = ChalkIr;
let interner = ChalkIr::default();
let associated_ty_lookups: BTreeMap<_, _> = program
.associated_ty_data
.iter()
Expand Down Expand Up @@ -1054,6 +1062,7 @@ pub fn lower_goal(goal: &Goal, program: &LoweredProgram) -> LowerResult<chalk_ir
foreign_ty_ids: &program.foreign_ty_ids,
parameter_map: BTreeMap::new(),
auto_traits: &auto_traits,
interner: program.interner,
};

goal.lower(&env)
Expand Down Expand Up @@ -1154,7 +1163,7 @@ impl Kinded for chalk_ir::VariableKind<ChalkIr> {

impl Kinded for chalk_ir::GenericArg<ChalkIr> {
fn kind(&self) -> Kind {
let interner = ChalkIr;
let interner = ChalkIr::default();
match self.data(interner) {
chalk_ir::GenericArgData::Ty(_) => Kind::Ty,
chalk_ir::GenericArgData::Lifetime(_) => Kind::Lifetime,
Expand Down
3 changes: 2 additions & 1 deletion chalk-integration/src/lowering/env.rs
Original file line number Diff line number Diff line change
Expand Up @@ -54,6 +54,7 @@ pub struct Env<'k> {
/// GenericArg identifiers are used as keys, therefore
/// all identifiers in an environment must be unique (no shadowing).
pub parameter_map: ParameterMap,
pub interner: ChalkIr,
}

/// Information about an associated type **declaration** (i.e., an
Expand Down Expand Up @@ -88,7 +89,7 @@ pub enum TypeLookup<'k> {

impl Env<'_> {
pub fn interner(&self) -> ChalkIr {
ChalkIr
self.interner
}

pub fn lookup_generic_arg(
Expand Down
11 changes: 6 additions & 5 deletions chalk-integration/src/lowering/program_lowerer.rs
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,6 @@ use crate::{interner::ChalkIr, TypeKind, TypeSort};
#[derive(Default)]
pub(super) struct ProgramLowerer {
next_item_index: u32,

associated_ty_lookups: AssociatedTyLookups,
associated_ty_value_ids: AssociatedTyValueIds,
adt_ids: AdtIds,
Expand Down Expand Up @@ -178,6 +177,7 @@ impl ProgramLowerer {
parameter_map: BTreeMap::new(),
auto_traits: &self.auto_traits,
foreign_ty_ids: &self.foreign_ty_ids,
interner: ChalkIr::default(),
};

match *item {
Expand Down Expand Up @@ -248,11 +248,11 @@ impl ProgramLowerer {
let upvar_tys: LowerResult<Vec<chalk_ir::Ty<ChalkIr>>> =
defn.upvars.iter().map(|ty| ty.lower(&env)).collect();
let substitution = chalk_ir::Substitution::from_iter(
ChalkIr,
upvar_tys?.into_iter().map(|ty| ty.cast(ChalkIr)),
ChalkIr::default(),
upvar_tys?.into_iter().map(|ty| ty.cast(ChalkIr::default())),
);
Ok(chalk_ir::TyKind::Tuple(defn.upvars.len(), substitution)
.intern(ChalkIr))
.intern(ChalkIr::default()))
})?;
closure_upvars.insert(closure_def_id, upvars);
}
Expand Down Expand Up @@ -501,6 +501,7 @@ impl ProgramLowerer {
custom_clauses,
object_safe_traits: self.object_safe_traits,
foreign_ty_ids: self.foreign_ty_ids,
interner: ChalkIr::default(),
})
}
}
Expand All @@ -517,7 +518,7 @@ macro_rules! lower_type_kind {
sort: TypeSort::$sort,
name: self.name.str.clone(),
binders: chalk_ir::Binders::new(
VariableKinds::from_iter(ChalkIr, $params(self).anonymize()),
VariableKinds::from_iter(ChalkIr::default(), $params(self).anonymize()),
crate::Unit,
),
})
Expand Down
5 changes: 4 additions & 1 deletion chalk-integration/src/program.rs
Original file line number Diff line number Diff line change
Expand Up @@ -105,6 +105,9 @@ pub struct Program {

/// For each foreign type `extern { type A; }`
pub foreign_ty_ids: BTreeMap<Identifier, ForeignDefId<ChalkIr>>,

/// interner of this program
pub interner: ChalkIr,
}

impl Program {
Expand Down Expand Up @@ -528,7 +531,7 @@ impl RustIrDatabase<ChalkIr> for Program {
}

fn interner(&self) -> ChalkIr {
ChalkIr
self.interner
}

fn is_object_safe(&self, trait_id: TraitId<ChalkIr>) -> bool {
Expand Down
34 changes: 17 additions & 17 deletions chalk-integration/src/test_macros.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,58 +9,58 @@ macro_rules! ty {

}),
chalk_ir::Substitution::from_iter(
chalk_integration::interner::ChalkIr,
chalk_integration::interner::ChalkIr::default(),
vec![$(arg!($arg)),*] as Vec<chalk_ir::GenericArg<_>>
),
)
.intern(chalk_integration::interner::ChalkIr)
.intern(chalk_integration::interner::ChalkIr::default())
};

(function $n:tt $($arg:tt)*) => {
chalk_ir::TyKind::Function(chalk_ir::FnPointer {
num_binders: $n,
substitution: chalk_ir::FnSubst(chalk_ir::Substitution::from_iter(
chalk_integration::interner::ChalkIr,
chalk_integration::interner::ChalkIr::default(),
vec![$(arg!($arg)),*] as Vec<chalk_ir::GenericArg<_>>
)),
sig: chalk_ir::FnSig {
safety: chalk_ir::Safety::Safe,
abi: <chalk_integration::interner::ChalkIr as chalk_ir::interner::Interner>::FnAbi::Rust,
variadic: false,
}
}).intern(chalk_integration::interner::ChalkIr)
}).intern(chalk_integration::interner::ChalkIr::default())
};

(placeholder $n:expr) => {
chalk_ir::TyKind::Placeholder(PlaceholderIndex {
ui: UniverseIndex { counter: $n },
idx: 0,
}).intern(chalk_integration::interner::ChalkIr)
}).intern(chalk_integration::interner::ChalkIr::default())
};

(projection (item $n:tt) $($arg:tt)*) => {
chalk_ir::AliasTy::Projection(chalk_ir::ProjectionTy {
associated_ty_id: AssocTypeId(chalk_integration::interner::RawId { index: $n }),
substitution: chalk_ir::Substitution::from_iter(
chalk_integration::interner::ChalkIr,
chalk_integration::interner::ChalkIr::default(),
vec![$(arg!($arg)),*] as Vec<chalk_ir::GenericArg<_>>
),
}).intern(chalk_integration::interner::ChalkIr)
}).intern(chalk_integration::interner::ChalkIr::default())
};

(infer $b:expr) => {
chalk_ir::TyKind::InferenceVar(chalk_ir::InferenceVar::from($b), chalk_ir::TyVariableKind::General)
.intern(chalk_integration::interner::ChalkIr)
.intern(chalk_integration::interner::ChalkIr::default())
};

(bound $d:tt $b:tt) => {
chalk_ir::TyKind::BoundVar(chalk_ir::BoundVar::new(chalk_ir::DebruijnIndex::new($d), $b))
.intern(chalk_integration::interner::ChalkIr)
.intern(chalk_integration::interner::ChalkIr::default())
};

(bound $b:expr) => {
chalk_ir::TyKind::BoundVar(chalk_ir::BoundVar::new(chalk_ir::DebruijnIndex::INNERMOST, $b))
.intern(chalk_integration::interner::ChalkIr)
.intern(chalk_integration::interner::ChalkIr::default())
};

(expr $b:expr) => {
Expand All @@ -76,14 +76,14 @@ macro_rules! ty {
macro_rules! arg {
((lifetime $b:tt)) => {
chalk_ir::GenericArg::new(
chalk_integration::interner::ChalkIr,
chalk_integration::interner::ChalkIr::default(),
chalk_ir::GenericArgData::Lifetime(lifetime!($b)),
)
};

($arg:tt) => {
chalk_ir::GenericArg::new(
chalk_integration::interner::ChalkIr,
chalk_integration::interner::ChalkIr::default(),
chalk_ir::GenericArgData::Ty(ty!($arg)),
)
};
Expand All @@ -93,22 +93,22 @@ macro_rules! arg {
macro_rules! lifetime {
(infer $b:expr) => {
chalk_ir::LifetimeData::InferenceVar(chalk_ir::InferenceVar::from($b))
.intern(chalk_integration::interner::ChalkIr)
.intern(chalk_integration::interner::ChalkIr::default())
};

(bound $d:tt $b:tt) => {
chalk_ir::LifetimeData::BoundVar(chalk_ir::BoundVar::new(chalk_ir::DebruijnIndex::new($d), $b))
.intern(chalk_integration::interner::ChalkIr)
.intern(chalk_integration::interner::ChalkIr::default())
};

(bound $b:expr) => {
chalk_ir::LifetimeData::BoundVar(chalk_ir::BoundVar::new(chalk_ir::DebruijnIndex::INNERMOST, $b))
.intern(chalk_integration::interner::ChalkIr)
.intern(chalk_integration::interner::ChalkIr::default())
};

(placeholder $b:expr) => {
chalk_ir::LifetimeData::Placeholder(PlaceholderIndex { ui: UniverseIndex { counter: $b }, idx: 0})
.intern(chalk_integration::interner::ChalkIr)
.intern(chalk_integration::interner::ChalkIr::default())
};

(expr $b:expr) => {
Expand All @@ -123,6 +123,6 @@ macro_rules! lifetime {
#[macro_export]
macro_rules! empty_substitution {
() => {
chalk_ir::Substitution::empty(chalk_integration::interner::ChalkIr)
chalk_ir::Substitution::empty(chalk_integration::interner::ChalkIr::default())
};
}
1 change: 1 addition & 0 deletions chalk-ir/src/debug.rs
Original file line number Diff line number Diff line change
Expand Up @@ -359,6 +359,7 @@ impl<I: Interner> Debug for ConstData<I> {
ConstValue::InferenceVar(var) => write!(fmt, "{:?}", var),
ConstValue::Placeholder(index) => write!(fmt, "{:?}", index),
ConstValue::Concrete(evaluated) => write!(fmt, "{:?}", evaluated),
ConstValue::Function(name, _) => write!(fmt, "#{}(<some args>)", name),
}
}
}
Expand Down
10 changes: 10 additions & 0 deletions chalk-ir/src/fold.rs
Original file line number Diff line number Diff line change
Expand Up @@ -566,6 +566,16 @@ where
}),
}
.intern(folder.interner())),
ConstValue::Function(name, args) => Ok(ConstData {
ty: fold_ty()?,
value: ConstValue::Function(
name.clone(),
args.into_iter()
.map(|x| x.clone().super_fold_with(folder, outer_binder))
.collect::<Result<Vec<_>, _>>()?,
),
}
.intern(folder.interner())),
}
}
}
Expand Down
Loading