Skip to content

Commit

Permalink
support const evaluation
Browse files Browse the repository at this point in the history
  • Loading branch information
HKalbasi committed Dec 10, 2021
1 parent 9780653 commit 4ad26af
Show file tree
Hide file tree
Showing 30 changed files with 293 additions and 115 deletions.
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

0 comments on commit 4ad26af

Please sign in to comment.