Skip to content

Commit 8c3937f

Browse files
HKalbasiHKalbasi
committed
support const evaluation
1 parent e0c94db commit 8c3937f

File tree

30 files changed

+293
-115
lines changed

30 files changed

+293
-115
lines changed

‎chalk-engine/src/slg.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -293,6 +293,8 @@ impl<I: Interner> MayInvalidate<'_, I> {
293293

294294
// Only variants left are placeholder = concrete, which always fails
295295
(ConstValue::Placeholder(_), _) | (ConstValue::Concrete(_), _) => true,
296+
297+
_ => todo!(),
296298
}
297299
}
298300

‎chalk-engine/src/slg/aggregate.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -551,6 +551,8 @@ impl<I: Interner> AntiUnifier<'_, '_, I> {
551551
(ConstValue::Placeholder(_), _) | (_, ConstValue::Placeholder(_)) => {
552552
self.new_const_variable(ty)
553553
}
554+
555+
_ => todo!(),
554556
}
555557
}
556558

‎chalk-engine/src/slg/resolvent.rs

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -687,17 +687,28 @@ impl<'i, I: Interner> Zipper<'i, I> for AnswerSubstitutor<'i, I> {
687687
Ok(())
688688
}
689689

690+
(ConstValue::Function(name1, args1), ConstValue::Function(name2, args2)) => {
691+
assert!(name1 == name2);
692+
Ok(())
693+
}
694+
695+
(ConstValue::Function(..), ConstValue::Concrete(_)) | (ConstValue::Concrete(_), ConstValue::Function(..)) => {
696+
Ok(())
697+
}
698+
690699
(ConstValue::InferenceVar(_), _) | (_, ConstValue::InferenceVar(_)) => panic!(
691700
"unexpected inference var in answer `{:?}` or pending goal `{:?}`",
692701
answer, pending,
693702
),
694703

695704
(ConstValue::BoundVar(_), _)
696705
| (ConstValue::Placeholder(_), _)
706+
| (ConstValue::Function(..), _)
697707
| (ConstValue::Concrete(_), _) => panic!(
698708
"structural mismatch between answer `{:?}` and pending goal `{:?}`",
699709
answer, pending,
700710
),
711+
701712
}
702713
}
703714

‎chalk-integration/src/db.rs

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
use crate::{
22
error::ChalkError,
3-
interner::ChalkIr,
3+
interner::{ChalkIr, ConstEval},
44
lowering::lower_goal,
55
program::Program,
66
query::{Lowering, LoweringDatabase},
@@ -26,13 +26,15 @@ use std::sync::Arc;
2626
#[derive(Default)]
2727
pub struct ChalkDatabase {
2828
storage: salsa::Storage<Self>,
29+
interner: ChalkIr,
2930
}
3031

3132
impl Database for ChalkDatabase {}
3233

3334
impl ChalkDatabase {
34-
pub fn with(program_text: &str, solver_choice: SolverChoice) -> Self {
35+
pub fn with(program_text: &str, const_eval: ConstEval, solver_choice: SolverChoice) -> Self {
3536
let mut db = ChalkDatabase::default();
37+
db.interner.const_eval_fn = const_eval;
3638
db.set_program_text(Arc::new(program_text.to_string()));
3739
db.set_solver_choice(solver_choice);
3840
db
@@ -174,7 +176,7 @@ impl RustIrDatabase<ChalkIr> for ChalkDatabase {
174176
}
175177

176178
fn interner(&self) -> &ChalkIr {
177-
&ChalkIr
179+
&self.interner
178180
}
179181

180182
fn is_object_safe(&self, trait_id: TraitId<ChalkIr>) -> bool {

‎chalk-integration/src/interner.rs

Lines changed: 17 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -50,10 +50,22 @@ impl Debug for ChalkFnAbi {
5050
}
5151
}
5252

53+
pub type ConstEval = fn(String, Vec<u32>) -> u32;
54+
5355
/// The default "interner" and the only interner used by chalk
5456
/// itself. In this interner, no interning actually occurs.
5557
#[derive(Debug, Copy, Clone, Hash, PartialOrd, Ord, PartialEq, Eq)]
56-
pub struct ChalkIr;
58+
pub struct ChalkIr {
59+
pub const_eval_fn: ConstEval,
60+
}
61+
62+
impl Default for ChalkIr {
63+
fn default() -> Self {
64+
ChalkIr {
65+
const_eval_fn: |_, _| panic!("const eval is not supported on this interner"),
66+
}
67+
}
68+
}
5769

5870
impl Interner for ChalkIr {
5971
type InternedType = Arc<TyData<ChalkIr>>;
@@ -265,6 +277,10 @@ impl Interner for ChalkIr {
265277
c1 == c2
266278
}
267279

280+
fn const_eval(&self, name: String, args: Vec<u32>) -> u32 {
281+
(self.const_eval_fn)(name, args)
282+
}
283+
268284
fn intern_generic_arg(&self, generic_arg: GenericArgData<ChalkIr>) -> GenericArgData<ChalkIr> {
269285
generic_arg
270286
}

‎chalk-integration/src/lowering.rs

Lines changed: 12 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -108,7 +108,7 @@ lower_param_map!(
108108
);
109109

110110
fn get_type_of_usize() -> chalk_ir::Ty<ChalkIr> {
111-
chalk_ir::TyKind::Scalar(chalk_ir::Scalar::Uint(chalk_ir::UintTy::Usize)).intern(&ChalkIr)
111+
chalk_ir::TyKind::Scalar(chalk_ir::Scalar::Uint(chalk_ir::UintTy::Usize)).intern(&ChalkIr::default())
112112
}
113113

114114
impl Lower for VariableKind {
@@ -818,6 +818,14 @@ impl LowerWithEnv for Const {
818818
fn lower(&self, env: &Env) -> LowerResult<Self::Lowered> {
819819
let interner = env.interner();
820820
match self {
821+
Const::Function(f) => Ok(chalk_ir::ConstData {
822+
ty: get_type_of_usize(),
823+
value: chalk_ir::ConstValue::Function(
824+
f.name.to_string(),
825+
f.args.iter().map(|x| x.lower(env)).collect::<Result<Vec<_>, _>>()?,
826+
),
827+
}
828+
.intern(interner)),
821829
Const::Id(name) => {
822830
let parameter = env.lookup_generic_arg(name)?;
823831
parameter
@@ -1013,7 +1021,7 @@ impl LowerWithEnv for (&TraitDefn, chalk_ir::TraitId<ChalkIr>) {
10131021
}
10141022

10151023
pub fn lower_goal(goal: &Goal, program: &LoweredProgram) -> LowerResult<chalk_ir::Goal<ChalkIr>> {
1016-
let interner = &ChalkIr;
1024+
let interner = &ChalkIr::default();
10171025
let associated_ty_lookups: BTreeMap<_, _> = program
10181026
.associated_ty_data
10191027
.iter()
@@ -1054,6 +1062,7 @@ pub fn lower_goal(goal: &Goal, program: &LoweredProgram) -> LowerResult<chalk_ir
10541062
foreign_ty_ids: &program.foreign_ty_ids,
10551063
parameter_map: BTreeMap::new(),
10561064
auto_traits: &auto_traits,
1065+
interner: program.interner,
10571066
};
10581067

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

11551164
impl Kinded for chalk_ir::GenericArg<ChalkIr> {
11561165
fn kind(&self) -> Kind {
1157-
let interner = &ChalkIr;
1166+
let interner = &ChalkIr::default();
11581167
match self.data(interner) {
11591168
chalk_ir::GenericArgData::Ty(_) => Kind::Ty,
11601169
chalk_ir::GenericArgData::Lifetime(_) => Kind::Lifetime,

‎chalk-integration/src/lowering/env.rs

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -54,6 +54,7 @@ pub struct Env<'k> {
5454
/// GenericArg identifiers are used as keys, therefore
5555
/// all identifiers in an environment must be unique (no shadowing).
5656
pub parameter_map: ParameterMap,
57+
pub interner: ChalkIr,
5758
}
5859

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

8990
impl Env<'_> {
9091
pub fn interner(&self) -> &ChalkIr {
91-
&ChalkIr
92+
&self.interner
9293
}
9394

9495
pub fn lookup_generic_arg(

‎chalk-integration/src/lowering/program_lowerer.rs

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,6 @@ use crate::{interner::ChalkIr, TypeKind, TypeSort};
2222
#[derive(Default)]
2323
pub(super) struct ProgramLowerer {
2424
next_item_index: u32,
25-
2625
associated_ty_lookups: AssociatedTyLookups,
2726
associated_ty_value_ids: AssociatedTyValueIds,
2827
adt_ids: AdtIds,
@@ -178,6 +177,7 @@ impl ProgramLowerer {
178177
parameter_map: BTreeMap::new(),
179178
auto_traits: &self.auto_traits,
180179
foreign_ty_ids: &self.foreign_ty_ids,
180+
interner: ChalkIr::default(),
181181
};
182182

183183
match *item {
@@ -247,11 +247,11 @@ impl ProgramLowerer {
247247
let upvar_tys: LowerResult<Vec<chalk_ir::Ty<ChalkIr>>> =
248248
defn.upvars.iter().map(|ty| ty.lower(&env)).collect();
249249
let substitution = chalk_ir::Substitution::from_iter(
250-
&ChalkIr,
251-
upvar_tys?.into_iter().map(|ty| ty.cast(&ChalkIr)),
250+
&ChalkIr::default(),
251+
upvar_tys?.into_iter().map(|ty| ty.cast(&ChalkIr::default())),
252252
);
253253
Ok(chalk_ir::TyKind::Tuple(defn.upvars.len(), substitution)
254-
.intern(&ChalkIr))
254+
.intern(&ChalkIr::default()))
255255
})?;
256256
closure_upvars.insert(closure_def_id, upvars);
257257
}
@@ -500,6 +500,7 @@ impl ProgramLowerer {
500500
custom_clauses,
501501
object_safe_traits: self.object_safe_traits,
502502
foreign_ty_ids: self.foreign_ty_ids,
503+
interner: ChalkIr::default(),
503504
})
504505
}
505506
}
@@ -516,7 +517,7 @@ macro_rules! lower_type_kind {
516517
sort: TypeSort::$sort,
517518
name: self.name.str.clone(),
518519
binders: chalk_ir::Binders::new(
519-
VariableKinds::from_iter(&ChalkIr, $params(self).anonymize()),
520+
VariableKinds::from_iter(&ChalkIr::default(), $params(self).anonymize()),
520521
crate::Unit,
521522
),
522523
})

‎chalk-integration/src/program.rs

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -105,6 +105,9 @@ pub struct Program {
105105

106106
/// For each foreign type `extern { type A; }`
107107
pub foreign_ty_ids: BTreeMap<Identifier, ForeignDefId<ChalkIr>>,
108+
109+
/// interner of this program
110+
pub interner: ChalkIr,
108111
}
109112

110113
impl Program {
@@ -528,7 +531,7 @@ impl RustIrDatabase<ChalkIr> for Program {
528531
}
529532

530533
fn interner(&self) -> &ChalkIr {
531-
&ChalkIr
534+
&self.interner
532535
}
533536

534537
fn is_object_safe(&self, trait_id: TraitId<ChalkIr>) -> bool {

‎chalk-integration/src/test_macros.rs

Lines changed: 17 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -9,58 +9,58 @@ macro_rules! ty {
99

1010
}),
1111
chalk_ir::Substitution::from_iter(
12-
&chalk_integration::interner::ChalkIr,
12+
&chalk_integration::interner::ChalkIr::default(),
1313
vec![$(arg!($arg)),*] as Vec<chalk_ir::GenericArg<_>>
1414
),
1515
)
16-
.intern(&chalk_integration::interner::ChalkIr)
16+
.intern(&chalk_integration::interner::ChalkIr::default())
1717
};
1818

1919
(function $n:tt $($arg:tt)*) => {
2020
chalk_ir::TyKind::Function(chalk_ir::FnPointer {
2121
num_binders: $n,
2222
substitution: chalk_ir::FnSubst(chalk_ir::Substitution::from_iter(
23-
&chalk_integration::interner::ChalkIr,
23+
&chalk_integration::interner::ChalkIr::default(),
2424
vec![$(arg!($arg)),*] as Vec<chalk_ir::GenericArg<_>>
2525
)),
2626
sig: chalk_ir::FnSig {
2727
safety: chalk_ir::Safety::Safe,
2828
abi: <chalk_integration::interner::ChalkIr as chalk_ir::interner::Interner>::FnAbi::Rust,
2929
variadic: false,
3030
}
31-
}).intern(&chalk_integration::interner::ChalkIr)
31+
}).intern(&chalk_integration::interner::ChalkIr::default())
3232
};
3333

3434
(placeholder $n:expr) => {
3535
chalk_ir::TyKind::Placeholder(PlaceholderIndex {
3636
ui: UniverseIndex { counter: $n },
3737
idx: 0,
38-
}).intern(&chalk_integration::interner::ChalkIr)
38+
}).intern(&chalk_integration::interner::ChalkIr::default())
3939
};
4040

4141
(projection (item $n:tt) $($arg:tt)*) => {
4242
chalk_ir::AliasTy::Projection(chalk_ir::ProjectionTy {
4343
associated_ty_id: AssocTypeId(chalk_integration::interner::RawId { index: $n }),
4444
substitution: chalk_ir::Substitution::from_iter(
45-
&chalk_integration::interner::ChalkIr,
45+
&chalk_integration::interner::ChalkIr::default(),
4646
vec![$(arg!($arg)),*] as Vec<chalk_ir::GenericArg<_>>
4747
),
48-
}).intern(&chalk_integration::interner::ChalkIr)
48+
}).intern(&chalk_integration::interner::ChalkIr::default())
4949
};
5050

5151
(infer $b:expr) => {
5252
chalk_ir::TyKind::InferenceVar(chalk_ir::InferenceVar::from($b), chalk_ir::TyVariableKind::General)
53-
.intern(&chalk_integration::interner::ChalkIr)
53+
.intern(&chalk_integration::interner::ChalkIr::default())
5454
};
5555

5656
(bound $d:tt $b:tt) => {
5757
chalk_ir::TyKind::BoundVar(chalk_ir::BoundVar::new(chalk_ir::DebruijnIndex::new($d), $b))
58-
.intern(&chalk_integration::interner::ChalkIr)
58+
.intern(&chalk_integration::interner::ChalkIr::default())
5959
};
6060

6161
(bound $b:expr) => {
6262
chalk_ir::TyKind::BoundVar(chalk_ir::BoundVar::new(chalk_ir::DebruijnIndex::INNERMOST, $b))
63-
.intern(&chalk_integration::interner::ChalkIr)
63+
.intern(&chalk_integration::interner::ChalkIr::default())
6464
};
6565

6666
(expr $b:expr) => {
@@ -76,14 +76,14 @@ macro_rules! ty {
7676
macro_rules! arg {
7777
((lifetime $b:tt)) => {
7878
chalk_ir::GenericArg::new(
79-
&chalk_integration::interner::ChalkIr,
79+
&chalk_integration::interner::ChalkIr::default(),
8080
chalk_ir::GenericArgData::Lifetime(lifetime!($b)),
8181
)
8282
};
8383

8484
($arg:tt) => {
8585
chalk_ir::GenericArg::new(
86-
&chalk_integration::interner::ChalkIr,
86+
&chalk_integration::interner::ChalkIr::default(),
8787
chalk_ir::GenericArgData::Ty(ty!($arg)),
8888
)
8989
};
@@ -93,22 +93,22 @@ macro_rules! arg {
9393
macro_rules! lifetime {
9494
(infer $b:expr) => {
9595
chalk_ir::LifetimeData::InferenceVar(chalk_ir::InferenceVar::from($b))
96-
.intern(&chalk_integration::interner::ChalkIr)
96+
.intern(&chalk_integration::interner::ChalkIr::default())
9797
};
9898

9999
(bound $d:tt $b:tt) => {
100100
chalk_ir::LifetimeData::BoundVar(chalk_ir::BoundVar::new(chalk_ir::DebruijnIndex::new($d), $b))
101-
.intern(&chalk_integration::interner::ChalkIr)
101+
.intern(&chalk_integration::interner::ChalkIr::default())
102102
};
103103

104104
(bound $b:expr) => {
105105
chalk_ir::LifetimeData::BoundVar(chalk_ir::BoundVar::new(chalk_ir::DebruijnIndex::INNERMOST, $b))
106-
.intern(&chalk_integration::interner::ChalkIr)
106+
.intern(&chalk_integration::interner::ChalkIr::default())
107107
};
108108

109109
(placeholder $b:expr) => {
110110
chalk_ir::LifetimeData::Placeholder(PlaceholderIndex { ui: UniverseIndex { counter: $b }, idx: 0})
111-
.intern(&chalk_integration::interner::ChalkIr)
111+
.intern(&chalk_integration::interner::ChalkIr::default())
112112
};
113113

114114
(expr $b:expr) => {
@@ -123,6 +123,6 @@ macro_rules! lifetime {
123123
#[macro_export]
124124
macro_rules! empty_substitution {
125125
() => {
126-
chalk_ir::Substitution::empty(&chalk_integration::interner::ChalkIr)
126+
chalk_ir::Substitution::empty(&chalk_integration::interner::ChalkIr::default())
127127
};
128128
}

‎chalk-ir/src/debug.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -359,6 +359,7 @@ impl<I: Interner> Debug for ConstData<I> {
359359
ConstValue::InferenceVar(var) => write!(fmt, "{:?}", var),
360360
ConstValue::Placeholder(index) => write!(fmt, "{:?}", index),
361361
ConstValue::Concrete(evaluated) => write!(fmt, "{:?}", evaluated),
362+
ConstValue::Function(name, _) => write!(fmt, "#{}(<some args>)", name),
362363
}
363364
}
364365
}

‎chalk-ir/src/fold.rs

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -591,6 +591,16 @@ where
591591
}),
592592
}
593593
.intern(folder.interner())),
594+
ConstValue::Function(name, args) => Ok(ConstData {
595+
ty: fold_ty()?,
596+
value: ConstValue::Function(
597+
name.clone(),
598+
args.into_iter()
599+
.map(|x| x.clone().super_fold_with(folder, outer_binder))
600+
.collect::<Result<Vec<_>, _>>()?,
601+
),
602+
}
603+
.intern(folder.interner())),
594604
}
595605
}
596606
}

0 commit comments

Comments
 (0)