Skip to content

Commit 45fb4e3

Browse files
hashedonehashedone
committed
Implementation and tests are corrected
1 parent 5f0c038 commit 45fb4e3

File tree

3 files changed

+58
-23
lines changed

3 files changed

+58
-23
lines changed

‎chalk-engine/src/logic.rs

Lines changed: 13 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ use crate::forest::Forest;
66
use crate::hh::HhGoal;
77
use crate::stack::{Stack, StackIndex};
88
use crate::strand::{CanonicalStrand, SelectedSubgoal, Strand};
9-
use crate::table::AnswerIndex;
9+
use crate::table::{AnswerIndex, Table};
1010
use crate::{
1111
Answer, CompleteAnswer, ExClause, FlounderedSubgoal, Literal, Minimums, TableIndex, TimeStamp,
1212
};
@@ -222,9 +222,9 @@ impl<C: Context> Forest<C> {
222222
goal
223223
);
224224
let coinductive_goal = context.is_coinductive(&goal);
225-
let table = self.tables.insert(goal, coinductive_goal);
226-
self.push_initial_strands(context, table);
227-
table
225+
let mut table = Table::new(goal.clone(), coinductive_goal);
226+
Self::push_initial_strands(context, self.tables.next_index(), &mut table);
227+
self.tables.insert(table)
228228
}
229229

230230
/// When a table is first created, this function is invoked to
@@ -238,23 +238,22 @@ impl<C: Context> Forest<C> {
238238
/// In terms of the NFTD paper, this corresponds to the *Program
239239
/// Clause Resolution* step being applied eagerly, as many times
240240
/// as possible.
241-
fn push_initial_strands(&mut self, context: &impl ContextOps<C>, table: TableIndex) {
241+
fn push_initial_strands(context: &impl ContextOps<C>, table_idx: TableIndex, table: &mut Table<C>) {
242242
// Instantiate the table goal with fresh inference variables.
243-
let table_goal = self.tables[table].table_goal.clone();
243+
let table_goal = table.table_goal.clone();
244244
let (infer, subst, environment, goal) = context.instantiate_ucanonical_goal(&table_goal);
245-
self.push_initial_strands_instantiated(context, table, infer, subst, environment, goal);
245+
Self::push_initial_strands_instantiated(context, table_idx, table, infer, subst, environment, goal);
246246
}
247247

248248
fn push_initial_strands_instantiated(
249-
&mut self,
250249
context: &impl ContextOps<C>,
251-
table: TableIndex,
250+
table_idx: TableIndex,
251+
table: &mut Table<C>,
252252
mut infer: C::InferenceTable,
253253
subst: C::Substitution,
254254
environment: C::Environment,
255255
goal: C::Goal,
256256
) {
257-
let table_ref = &mut self.tables[table];
258257
match context.into_hh_goal(goal) {
259258
HhGoal::DomainGoal(domain_goal) => {
260259
match context.program_clauses(&environment, &domain_goal, &mut infer) {
@@ -277,13 +276,13 @@ impl<C: Context> Forest<C> {
277276
last_pursued_time: TimeStamp::default(),
278277
};
279278
let canonical_strand = Self::canonicalize_strand(context, strand);
280-
table_ref.enqueue_strand(canonical_strand);
279+
table.enqueue_strand(canonical_strand);
281280
}
282281
}
283282
}
284283
Err(Floundered) => {
285-
debug!("Marking table {:?} as floundered!", table);
286-
table_ref.mark_floundered();
284+
debug!("Marking table {:?} as floundered!", table_idx);
285+
table.mark_floundered();
287286
}
288287
}
289288
}
@@ -311,7 +310,7 @@ impl<C: Context> Forest<C> {
311310
last_pursued_time: TimeStamp::default(),
312311
};
313312
let canonical_strand = Self::canonicalize_strand(context, strand);
314-
table_ref.enqueue_strand(canonical_strand);
313+
table.enqueue_strand(canonical_strand);
315314
}
316315
}
317316
}

‎chalk-engine/src/tables.rs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -31,11 +31,11 @@ impl<C: Context> Tables<C> {
3131

3232
pub(super) fn insert(
3333
&mut self,
34-
goal: C::UCanonicalGoalInEnvironment,
35-
coinductive_goal: bool,
34+
table: Table<C>,
3635
) -> TableIndex {
36+
let goal = table.table_goal.clone();
3737
let index = self.next_index();
38-
self.tables.push(Table::new(goal.clone(), coinductive_goal));
38+
self.tables.push(table);
3939
self.table_indices.insert(goal, index);
4040
index
4141
}

‎tests/integration/panic.rs

Lines changed: 42 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,17 +1,26 @@
1-
use chalk_ir::interner::ChalkIr;
1+
use chalk_ir::interner::{ChalkIr, RawId};
2+
use chalk_ir::ApplicationTy;
23
use chalk_ir::AssocTypeId;
4+
use chalk_ir::Binders;
35
use chalk_ir::ImplId;
46
use chalk_ir::OpaqueTyId;
57
use chalk_ir::Parameter;
8+
use chalk_ir::ParameterKinds;
69
use chalk_ir::ProgramClause;
710
use chalk_ir::StructId;
11+
use chalk_ir::Substitution;
812
use chalk_ir::TraitId;
13+
use chalk_ir::TraitRef;
14+
use chalk_ir::Ty;
915
use chalk_ir::TypeName;
1016
use chalk_rust_ir::AssociatedTyDatum;
1117
use chalk_rust_ir::AssociatedTyValue;
1218
use chalk_rust_ir::AssociatedTyValueId;
1319
use chalk_rust_ir::ImplDatum;
20+
use chalk_rust_ir::ImplDatumBound;
21+
use chalk_rust_ir::ImplType;
1422
use chalk_rust_ir::OpaqueTyDatum;
23+
use chalk_rust_ir::Polarity;
1524
use chalk_rust_ir::StructDatum;
1625
use chalk_rust_ir::TraitDatum;
1726
use chalk_rust_ir::WellKnownTrait;
@@ -40,7 +49,7 @@ impl RustIrDatabase<ChalkIr> for MockDatabase {
4049

4150
fn trait_datum(&self, id: TraitId<ChalkIr>) -> Arc<TraitDatum<ChalkIr>> {
4251
assert_eq!(id.0.index, 0);
43-
return Arc::new(chalk_rust_ir::TraitDatum {
52+
Arc::new(chalk_rust_ir::TraitDatum {
4453
id,
4554
binders: chalk_ir::Binders::new(
4655
chalk_ir::ParameterKinds::new(&ChalkIr),
@@ -58,11 +67,37 @@ impl RustIrDatabase<ChalkIr> for MockDatabase {
5867
},
5968
associated_ty_ids: vec![],
6069
well_known: None,
61-
});
70+
})
6271
}
6372

6473
fn impl_datum(&self, id: ImplId<ChalkIr>) -> Arc<ImplDatum<ChalkIr>> {
65-
unimplemented!()
74+
assert_eq!(id.0.index, 1);
75+
76+
let substitution = Ty::new(
77+
&ChalkIr,
78+
ApplicationTy {
79+
name: TypeName::Struct(StructId(RawId { index: 1 })),
80+
substitution: Substitution::empty(&ChalkIr),
81+
},
82+
);
83+
84+
let binders = Binders::new(
85+
ParameterKinds::new(&ChalkIr),
86+
ImplDatumBound {
87+
trait_ref: TraitRef {
88+
trait_id: TraitId(RawId { index: 0 }),
89+
substitution: Substitution::from1(&ChalkIr, substitution),
90+
},
91+
where_clauses: vec![],
92+
},
93+
);
94+
95+
Arc::new(ImplDatum {
96+
polarity: Polarity::Positive,
97+
binders,
98+
impl_type: ImplType::Local,
99+
associated_ty_value_ids: vec![],
100+
})
66101
}
67102

68103
fn associated_ty_value(
@@ -89,7 +124,8 @@ impl RustIrDatabase<ChalkIr> for MockDatabase {
89124
trait_id: TraitId<ChalkIr>,
90125
parameters: &[Parameter<ChalkIr>],
91126
) -> Vec<ImplId<ChalkIr>> {
92-
unimplemented!()
127+
assert_eq!(trait_id.0.index, 0);
128+
vec![ImplId(RawId { index: 1 })]
93129
}
94130

95131
fn local_impls_to_coherence_check(&self, trait_id: TraitId<ChalkIr>) -> Vec<ImplId<ChalkIr>> {
@@ -165,7 +201,7 @@ fn unwind_safety() {
165201
let result = panic::catch_unwind(panic::AssertUnwindSafe(|| {
166202
solver.solve(&db, &peeled_goal);
167203
}));
168-
assert!(result.is_err() == true);
204+
assert!(result.is_err());
169205

170206
// solve again but without panicking this time
171207
db.panic = false;

0 commit comments

Comments
 (0)