From 0cdc6c78f0d637f57f7816946fb9f6a99e3f72e5 Mon Sep 17 00:00:00 2001 From: Jack Huey Date: Wed, 16 Sep 2020 20:09:07 -0400 Subject: [PATCH] Remove Context trait from chalk-engine --- chalk-engine/src/context.rs | 255 +------------------------- chalk-engine/src/forest.rs | 23 +-- chalk-engine/src/logic.rs | 191 ++++++++++++-------- chalk-engine/src/simplify.rs | 30 ++-- chalk-engine/src/slg.rs | 290 ++++++++++++++---------------- chalk-engine/src/slg/aggregate.rs | 2 +- chalk-engine/src/slg/resolvent.rs | 5 +- chalk-engine/src/solve.rs | 13 +- chalk-engine/src/stack.rs | 39 ++-- chalk-engine/src/strand.rs | 8 +- 10 files changed, 313 insertions(+), 543 deletions(-) diff --git a/chalk-engine/src/context.rs b/chalk-engine/src/context.rs index 980e6617613..4964400807c 100644 --- a/chalk-engine/src/context.rs +++ b/chalk-engine/src/context.rs @@ -5,262 +5,11 @@ //! `DomainGoal` type, add arena lifetime parameters, and more. See //! [`Context`] trait for a list of types. -use crate::{CompleteAnswer, ExClause}; +use crate::CompleteAnswer; use chalk_ir::interner::Interner; -use chalk_ir::{ - AnswerSubst, Binders, Canonical, ConstrainedSubst, Constraint, DomainGoal, Environment, - Fallible, Floundered, GenericArg, Goal, InEnvironment, ProgramClause, ProgramClauses, - Substitution, UCanonical, UniverseMap, -}; +use chalk_ir::Substitution; use std::fmt::Debug; -/// The "context" in which the SLG solver operates. It defines all the -/// types that the SLG solver may need to refer to, as well as a few -/// very simple interconversion methods. -/// -/// At any given time, the SLG solver may have more than one context -/// active. First, there is always the *global* context, but when we -/// are in the midst of pursuing some particular strand, we will -/// instantiate a second context just for that work, via the -/// `instantiate_ucanonical_goal` and `instantiate_ex_clause` methods. -/// -/// In the chalk implementation, these two contexts are mapped to the -/// same type. But in the rustc implementation, this second context -/// corresponds to a fresh arena, and data allocated in that second -/// context will be freed once the work is done. (The "canonicalizing" -/// steps offer a way to convert data from the inference context back -/// into the global context.) -/// -/// FIXME: Clone and Debug bounds are just for easy derive, they are -/// not actually necessary. But dang are they convenient. -pub trait Context: Clone + Debug { - /// Represents an inference table. - type InferenceTable: InferenceTable + Clone; - - /// Selects the next appropriate subgoal index for evaluation. - /// Used by: logic - fn next_subgoal_index(ex_clause: &ExClause) -> usize; -} - -pub trait ContextOps>: Sized + Clone + Debug { - /// True if this is a coinductive goal -- e.g., proving an auto trait. - fn is_coinductive(&self, goal: &UCanonical>>) -> bool; - - /// Returns the set of program clauses that might apply to - /// `goal`. (This set can be over-approximated, naturally.) - /// - /// If this callback returns `None`, that indicates that the set - /// of program clauses cannot be enumerated because there are - /// unresolved type variables that would have to be resolved - /// first; the goal will be considered floundered. - fn program_clauses( - &self, - environment: &Environment, - goal: &DomainGoal, - infer: &mut C::InferenceTable, - ) -> Result>, Floundered>; - - // Used by: simplify - fn add_clauses(&self, env: &Environment, clauses: ProgramClauses) -> Environment; - - /// Create an inference table for processing a new goal and instantiate that goal - /// in that context, returning "all the pieces". - /// - /// More specifically: given a u-canonical goal `arg`, creates a - /// new inference table `T` and populates it with the universes - /// found in `arg`. Then, creates a substitution `S` that maps - /// each bound variable in `arg` to a fresh inference variable - /// from T. Returns: - /// - /// - the table `T` - /// - the substitution `S` - /// - the environment and goal found by substitution `S` into `arg` - fn instantiate_ucanonical_goal( - &self, - arg: &UCanonical>>, - ) -> (C::InferenceTable, Substitution, Environment, Goal); - - fn instantiate_ex_clause( - &self, - num_universes: usize, - canonical_ex_clause: &Canonical>, - ) -> (C::InferenceTable, ExClause); - - // Used by: logic - fn instantiate_answer_subst( - &self, - num_universes: usize, - answer: &Canonical>, - ) -> ( - C::InferenceTable, - Substitution, - Vec>>, - Vec>>, - ); - - /// Returns a identity substitution. - fn identity_constrained_subst( - &self, - goal: &UCanonical>>, - ) -> Canonical>; - - /// Convert a goal G *from* the canonical universes *into* our - /// local universes. This will yield a goal G' that is the same - /// but for the universes of universally quantified names. - fn map_goal_from_canonical( - &self, - _: &UniverseMap, - value: &Canonical>>, - ) -> Canonical>>; - - /// Convert a substitution *from* the canonical universes *into* - /// our local universes. This will yield a substitution S' that is - /// the same but for the universes of universally quantified - /// names. - fn map_subst_from_canonical( - &self, - _: &UniverseMap, - value: &Canonical>, - ) -> Canonical>; - - fn interner(&self) -> &I; - - /// Upcast this domain goal into a more general goal. - fn into_goal(&self, domain_goal: DomainGoal) -> Goal; - - fn is_trivial_constrained_substitution( - &self, - constrained_subst: &Canonical>, - ) -> bool; - - fn is_trivial_substitution( - &self, - u_canon: &UCanonical>>, - canonical_subst: &Canonical>, - ) -> bool; -} - -/// An "inference table" contains the state to support unification and -/// other operations on terms. -pub trait InferenceTable>: - ResolventOps + TruncateOps + UnificationOps -{ -} - -/// Methods for unifying and manipulating terms and binders. -pub trait UnificationOps> { - // Used by: simplify - fn instantiate_binders_universally(&mut self, interner: &I, arg: &Binders>) -> Goal; - - // Used by: simplify - fn instantiate_binders_existentially( - &mut self, - interner: &I, - arg: &Binders>, - ) -> Goal; - - // Used by: logic (but for debugging only) - fn debug_ex_clause<'v>(&mut self, interner: &I, value: &'v ExClause) -> Box; - - // Used by: logic - fn fully_canonicalize_goal( - &mut self, - interner: &I, - value: &InEnvironment>, - ) -> (UCanonical>>, UniverseMap); - - // Used by: logic - fn canonicalize_ex_clause( - &mut self, - interner: &I, - value: &ExClause, - ) -> Canonical>; - - // Used by: logic - fn canonicalize_constrained_subst( - &mut self, - interner: &I, - subst: Substitution, - constraints: Vec>>, - ) -> Canonical>; - - // Used by: logic - fn canonicalize_answer_subst( - &mut self, - interner: &I, - subst: Substitution, - constraints: Vec>>, - delayed_subgoals: Vec>>, - ) -> Canonical>; - - // Used by: logic - fn invert_goal( - &mut self, - interner: &I, - value: &InEnvironment>, - ) -> Option>>; - - /// First unify the parameters, then add the residual subgoals - /// as new subgoals of the ex-clause. - /// Also add region constraints. - /// - /// If the parameters fail to unify, then `Error` is returned - // Used by: simplify - fn unify_generic_args_into_ex_clause( - &mut self, - interner: &I, - environment: &Environment, - a: &GenericArg, - b: &GenericArg, - ex_clause: &mut ExClause, - ) -> Fallible<()>; -} - -/// "Truncation" (called "abstraction" in the papers referenced below) -/// refers to the act of modifying a goal or answer that has become -/// too large in order to guarantee termination. -/// -/// Currently we don't perform truncation (but it might me readded later). -/// -/// Citations: -/// -/// - Terminating Evaluation of Logic Programs with Finite Three-Valued Models -/// - Riguzzi and Swift; ACM Transactions on Computational Logic 2013 -/// - Radial Restraint -/// - Grosof and Swift; 2013 -pub trait TruncateOps> { - /// Check if `subgoal` is too large - fn goal_needs_truncation(&mut self, interner: &I, subgoal: &InEnvironment>) -> bool; - - /// Check if `subst` is too large - fn answer_needs_truncation(&mut self, interner: &I, subst: &Substitution) -> bool; -} - -pub trait ResolventOps> { - /// Combines the `goal` (instantiated within `infer`) with the - /// given program clause to yield the start of a new strand (a - /// canonical ex-clause). - /// - /// The bindings in `infer` are unaffected by this operation. - fn resolvent_clause( - &mut self, - interner: &I, - environment: &Environment, - goal: &DomainGoal, - subst: &Substitution, - clause: &ProgramClause, - ) -> Fallible>; - - fn apply_answer_subst( - &mut self, - interner: &I, - ex_clause: &mut ExClause, - selected_goal: &InEnvironment>, - answer_table_goal: &Canonical>>, - canonical_answer_subst: &Canonical>, - ) -> Fallible<()>; -} - pub enum AnswerResult { /// The next available answer. Answer(CompleteAnswer), diff --git a/chalk-engine/src/forest.rs b/chalk-engine/src/forest.rs index 2a6a3093932..410b9cd0a6b 100644 --- a/chalk-engine/src/forest.rs +++ b/chalk-engine/src/forest.rs @@ -1,5 +1,6 @@ -use crate::context::{AnswerResult, AnswerStream, Context, ContextOps}; +use crate::context::{AnswerResult, AnswerStream}; use crate::logic::RootSearchFail; +use crate::slg::SlgContextOps; use crate::table::AnswerIndex; use crate::tables::Tables; use crate::{TableIndex, TimeStamp}; @@ -8,7 +9,7 @@ use chalk_ir::interner::Interner; use chalk_ir::{Goal, InEnvironment, Substitution, UCanonical}; use tracing::debug; -pub(crate) struct Forest> { +pub(crate) struct Forest { pub(crate) tables: Tables, /// This is a clock which always increases. It is @@ -16,15 +17,13 @@ pub(crate) struct Forest> { /// This effectively gives us way to track what depth /// and loop a table or strand was last followed. pub(crate) clock: TimeStamp, - _context: std::marker::PhantomData, } -impl> Forest { +impl Forest { pub fn new() -> Self { Forest { tables: Tables::new(), clock: TimeStamp::default(), - _context: std::marker::PhantomData, } } @@ -40,7 +39,7 @@ impl> Forest { /// invocations. Invoking `next` fewer times is preferable =) pub fn iter_answers<'f>( &'f mut self, - context: &'f impl ContextOps, + context: &'f SlgContextOps<'f, I>, goal: &UCanonical>>, ) -> impl AnswerStream + 'f { let table = self.get_or_create_table_for_ucanonical_goal(context, goal.clone()); @@ -50,22 +49,18 @@ impl> Forest { context, table, answer, - _context: std::marker::PhantomData::, } } } -struct ForestSolver<'me, I: Interner, C: Context, CO: ContextOps> { - forest: &'me mut Forest, - context: &'me CO, +struct ForestSolver<'me, I: Interner> { + forest: &'me mut Forest, + context: &'me SlgContextOps<'me, I>, table: TableIndex, answer: AnswerIndex, - _context: std::marker::PhantomData, } -impl<'me, I: Interner, C: Context, CO: ContextOps> AnswerStream - for ForestSolver<'me, I, C, CO> -{ +impl<'me, I: Interner> AnswerStream for ForestSolver<'me, I> { /// # Panics /// /// Panics if a negative cycle was detected. diff --git a/chalk-engine/src/logic.rs b/chalk-engine/src/logic.rs index de17def4831..fbd5f82b76b 100644 --- a/chalk-engine/src/logic.rs +++ b/chalk-engine/src/logic.rs @@ -1,7 +1,7 @@ -use crate::context::{ - Context, ContextOps, InferenceTable, ResolventOps, TruncateOps, UnificationOps, -}; use crate::forest::Forest; +use crate::slg::{ + ResolventOps, SlgContext, SlgContextOps, TruncateOps, TruncatingInferenceTable, UnificationOps, +}; use crate::stack::{Stack, StackIndex}; use crate::strand::{CanonicalStrand, SelectedSubgoal, Strand}; use crate::table::{AnswerIndex, Table}; @@ -12,9 +12,11 @@ use crate::{ use chalk_ir::interner::Interner; use chalk_ir::{ - Canonical, ConstrainedSubst, Floundered, Goal, GoalData, InEnvironment, NoSolution, - Substitution, UCanonical, UniverseMap, + AnswerSubst, Canonical, CanonicalVarKinds, ConstrainedSubst, Floundered, Goal, GoalData, + InEnvironment, NoSolution, Substitution, UCanonical, UniverseMap, }; +use chalk_solve::clauses::program_clauses_for_goal; +use chalk_solve::coinductive_goal::IsCoinductive; use tracing::{debug, debug_span, info, instrument}; type RootSearchResult = Result; @@ -71,14 +73,14 @@ enum NoRemainingSubgoalsResult { Success, } -impl> Forest { +impl Forest { /// Returns an answer with a given index for the given table. This /// may require activating a strand and following it. It returns /// `Ok(answer)` if they answer is available and otherwise a /// `RootSearchFail` result. pub(super) fn root_answer( &mut self, - context: &impl ContextOps, + context: &SlgContextOps, table: TableIndex, answer_index: AnswerIndex, ) -> RootSearchResult> { @@ -132,10 +134,7 @@ impl> Forest { self.tables[table].answer(answer).unwrap() } - fn canonicalize_strand( - context: &impl ContextOps, - strand: Strand, - ) -> CanonicalStrand { + fn canonicalize_strand(context: &SlgContextOps, strand: Strand) -> CanonicalStrand { let Strand { mut infer, ex_clause, @@ -152,13 +151,14 @@ impl> Forest { } fn canonicalize_strand_from( - context: &impl ContextOps, - infer: &mut dyn InferenceTable, + context: &SlgContextOps, + infer: &mut TruncatingInferenceTable, ex_clause: &ExClause, selected_subgoal: Option, last_pursued_time: TimeStamp, ) -> CanonicalStrand { - let canonical_ex_clause = infer.canonicalize_ex_clause(context.interner(), &ex_clause); + let canonical_ex_clause = + infer.canonicalize_ex_clause(context.program().interner(), &ex_clause); CanonicalStrand { canonical_ex_clause, selected_subgoal, @@ -182,8 +182,8 @@ impl> Forest { #[instrument(level = "debug", skip(self, context, infer))] fn get_or_create_table_for_subgoal( &mut self, - context: &impl ContextOps, - infer: &mut dyn InferenceTable, + context: &SlgContextOps, + infer: &mut TruncatingInferenceTable, subgoal: &Literal, ) -> Option<(TableIndex, UniverseMap)> { // Subgoal abstraction: @@ -213,7 +213,7 @@ impl> Forest { #[instrument(level = "debug", skip(self, context))] pub(crate) fn get_or_create_table_for_ucanonical_goal( &mut self, - context: &impl ContextOps, + context: &SlgContextOps, goal: UCanonical>>, ) -> TableIndex { if let Some(table) = self.tables.index_of(&goal) { @@ -242,23 +242,38 @@ impl> Forest { /// Clause Resolution* step being applied eagerly, as many times /// as possible. fn build_table( - context: &impl ContextOps, + context: &SlgContextOps, table_idx: TableIndex, goal: UCanonical>>, ) -> Table { - let mut table = Table::new(goal.clone(), context.is_coinductive(&goal)); - let (mut infer, subst, environment, goal) = context.instantiate_ucanonical_goal(&goal); - let goal_data = goal.data(context.interner()); + let coinductive = goal.is_coinductive(context.program()); + let mut table = Table::new(goal.clone(), coinductive); + let (infer, subst, InEnvironment { environment, goal }) = + chalk_solve::infer::InferenceTable::from_canonical( + context.program().interner(), + goal.universes, + &goal.canonical, + ); + let mut infer = TruncatingInferenceTable::new(context.max_size(), infer); + let goal_data = goal.data(context.program().interner()); match goal_data { GoalData::DomainGoal(domain_goal) => { - match context.program_clauses(&environment, &domain_goal, &mut infer) { + let program = context.program(); + let clauses = program_clauses_for_goal( + program, + &environment, + &domain_goal, + &CanonicalVarKinds::empty(program.interner()), + ); + + match clauses { Ok(clauses) => { for clause in clauses { info!("program clause = {:#?}", clause); let mut infer = infer.clone(); if let Ok(resolvent) = infer.resolvent_clause( - context.interner(), + context.program().interner(), &environment, &domain_goal, &subst, @@ -300,7 +315,7 @@ impl> Forest { Self::simplify_goal(context, &mut infer, subst, environment, goal) { info!( - ex_clause = ?infer.debug_ex_clause(context.interner(), &ex_clause), + ex_clause = ?infer.debug_ex_clause(context.program().interner(), &ex_clause), "pushing initial strand" ); let strand = Strand { @@ -325,14 +340,14 @@ impl> Forest { /// of `subgoal`; but if the subgoal is getting too big, we return /// `None`, which causes the subgoal to flounder. fn abstract_positive_literal( - context: &impl ContextOps, - infer: &mut dyn InferenceTable, + context: &SlgContextOps, + infer: &mut TruncatingInferenceTable, subgoal: &InEnvironment>, ) -> Option<(UCanonical>>, UniverseMap)> { - if infer.goal_needs_truncation(context.interner(), subgoal) { + if infer.goal_needs_truncation(context.program().interner(), subgoal) { None } else { - Some(infer.fully_canonicalize_goal(context.interner(), subgoal)) + Some(infer.fully_canonicalize_goal(context.program().interner(), subgoal)) } } @@ -344,8 +359,8 @@ impl> Forest { /// variables appear in `subgoal` (in which case the execution is /// said to "flounder"). fn abstract_negative_literal( - context: &impl ContextOps, - infer: &mut dyn InferenceTable, + context: &SlgContextOps, + infer: &mut TruncatingInferenceTable, subgoal: &InEnvironment>, ) -> Option<(UCanonical>>, UniverseMap)> { // First, we have to check that the selected negative literal @@ -385,25 +400,23 @@ impl> Forest { // could instead generate an (imprecise) result). As you can // see a bit later, we also diverge in some other aspects that // affect completeness when it comes to subgoal abstraction. - let inverted_subgoal = infer.invert_goal(context.interner(), subgoal)?; + let inverted_subgoal = infer.invert_goal(context.program().interner(), subgoal)?; - if infer.goal_needs_truncation(context.interner(), &inverted_subgoal) { + if infer.goal_needs_truncation(context.program().interner(), &inverted_subgoal) { None } else { - Some(infer.fully_canonicalize_goal(context.interner(), &inverted_subgoal)) + Some(infer.fully_canonicalize_goal(context.program().interner(), &inverted_subgoal)) } } } -pub(crate) struct SolveState<'forest, I: Interner, C: Context, CO: ContextOps> { - forest: &'forest mut Forest, - context: &'forest CO, - stack: Stack, +pub(crate) struct SolveState<'forest, I: Interner> { + forest: &'forest mut Forest, + context: &'forest SlgContextOps<'forest, I>, + stack: Stack, } -impl<'forest, I: Interner, C: Context + 'forest, CO: ContextOps + 'forest> Drop - for SolveState<'forest, I, C, CO> -{ +impl<'forest, I: Interner> Drop for SolveState<'forest, I> { fn drop(&mut self) { if !self.stack.is_empty() { if let Some(active_strand) = self.stack.top().active_strand.take() { @@ -417,9 +430,7 @@ impl<'forest, I: Interner, C: Context + 'forest, CO: ContextOps + 'fore } } -impl<'forest, I: Interner, C: Context + 'forest, CO: ContextOps + 'forest> - SolveState<'forest, I, C, CO> -{ +impl<'forest, I: Interner> SolveState<'forest, I> { /// Ensures that answer with the given index is available from the /// given table. Returns `Ok` if there is an answer. /// @@ -472,8 +483,11 @@ impl<'forest, I: Interner, C: Context + 'forest, CO: ContextOps + 'fore let next_strand = self.stack.top().active_strand.take().or_else(|| { forest.tables[table] .dequeue_next_strand_that(|strand| { - let (_, ex_clause) = context - .instantiate_ex_clause(num_universes, &strand.canonical_ex_clause); + let (_, _, ex_clause) = chalk_solve::infer::InferenceTable::from_canonical( + context.program().interner(), + num_universes, + &strand.canonical_ex_clause, + ); let time_eligble = strand.last_pursued_time < clock; let mode_eligble = match (table_answer_mode, ex_clause.ambiguous) { (AnswerMode::Complete, false) => true, @@ -488,8 +502,14 @@ impl<'forest, I: Interner, C: Context + 'forest, CO: ContextOps + 'fore selected_subgoal, last_pursued_time, } = canonical_strand; - let (infer, ex_clause) = - context.instantiate_ex_clause(num_universes, &canonical_ex_clause); + + let (infer, _, ex_clause) = + chalk_solve::infer::InferenceTable::from_canonical( + context.program().interner(), + num_universes, + &canonical_ex_clause, + ); + let infer = TruncatingInferenceTable::new(context.max_size(), infer); Strand { infer, ex_clause, @@ -535,7 +555,7 @@ impl<'forest, I: Interner, C: Context + 'forest, CO: ContextOps + 'fore /// answer into the provided `Strand`. /// On success, `Ok` is returned and the `Strand` can be continued to process /// On failure, `Err` is returned and the `Strand` should be discarded - fn merge_answer_into_strand(&mut self, strand: &mut Strand) -> RootSearchResult<()> { + fn merge_answer_into_strand(&mut self, strand: &mut Strand) -> RootSearchResult<()> { // At this point, we know we have an answer for // the selected subgoal of the strand. // Now, we have to unify that answer onto the strand. @@ -585,10 +605,10 @@ impl<'forest, I: Interner, C: Context + 'forest, CO: ContextOps + 'fore selected_subgoal.subgoal_table, selected_subgoal.answer_index, ); - if !self.context.is_trivial_substitution( - &self.forest.tables[selected_subgoal.subgoal_table].table_goal, - &answer.subst, - ) { + if !self.forest.tables[selected_subgoal.subgoal_table] + .table_goal + .is_trivial_substitution(self.context.program().interner(), &answer.subst) + { let mut next_subgoal = selected_subgoal.clone(); next_subgoal.answer_index.increment(); let next_strand = Strand { @@ -617,20 +637,21 @@ impl<'forest, I: Interner, C: Context + 'forest, CO: ContextOps + 'fore answer_index, ref universe_map, } = selected_subgoal; - let table_goal = &self.context.map_goal_from_canonical( - &universe_map, + use chalk_solve::infer::ucanonicalize::UniverseMapExt; + let table_goal = universe_map.map_from_canonical( + self.context.program().interner(), &self.forest.tables[subgoal_table].table_goal.canonical, ); - let answer_subst = &self.context.map_subst_from_canonical( - &universe_map, + let answer_subst = universe_map.map_from_canonical( + self.context.program().interner(), &self.forest.answer(subgoal_table, answer_index).subst, ); match strand.infer.apply_answer_subst( - self.context.interner(), + self.context.program().interner(), &mut strand.ex_clause, &subgoal, - table_goal, - answer_subst, + &table_goal, + &answer_subst, ) { Ok(()) => { let Strand { @@ -731,7 +752,7 @@ impl<'forest, I: Interner, C: Context + 'forest, CO: ContextOps + 'fore /// be discarded. /// /// In other words, we return whether this strand flounders. - fn propagate_floundered_subgoal(&mut self, strand: &mut Strand) -> bool { + fn propagate_floundered_subgoal(&mut self, strand: &mut Strand) -> bool { // This subgoal selection for the strand is finished, so take it let selected_subgoal = strand.selected_subgoal.take().unwrap(); match strand.ex_clause.subgoals[selected_subgoal.subgoal_index] { @@ -775,7 +796,7 @@ impl<'forest, I: Interner, C: Context + 'forest, CO: ContextOps + 'fore /// This is called if the selected subgoal for a `Strand` is /// a coinductive cycle. - fn on_coinductive_subgoal(&mut self, mut strand: Strand) -> Result<(), RootSearchFail> { + fn on_coinductive_subgoal(&mut self, mut strand: Strand) -> Result<(), RootSearchFail> { // This is a co-inductive cycle. That is, this table // appears somewhere higher on the stack, and has now // recursively requested an answer for itself. This @@ -819,7 +840,7 @@ impl<'forest, I: Interner, C: Context + 'forest, CO: ContextOps + 'fore /// * `minimums` is the collected minimum clock times fn on_positive_cycle( &mut self, - strand: Strand, + strand: Strand, minimums: Minimums, ) -> Result<(), RootSearchFail> { // We can't take this because we might need it later to clear the cycle @@ -865,7 +886,7 @@ impl<'forest, I: Interner, C: Context + 'forest, CO: ContextOps + 'fore /// /// * `Ok` if we should keep searching. /// * `Err` if the subgoal failed in some way such that the strand can be abandoned. - fn on_subgoal_selected(&mut self, mut strand: Strand) -> Result<(), RootSearchFail> { + fn on_subgoal_selected(&mut self, mut strand: Strand) -> Result<(), RootSearchFail> { // This may be a newly selected subgoal or an existing selected subgoal. let SelectedSubgoal { @@ -947,7 +968,7 @@ impl<'forest, I: Interner, C: Context + 'forest, CO: ContextOps + 'fore /// it represents an answer. If the strand is ambiguous and we don't want /// it yet, we just enqueue it again to pick it up later. Otherwise, we /// add the answer from the strand onto the table. - fn on_no_remaining_subgoals(&mut self, strand: Strand) -> NoRemainingSubgoalsResult { + fn on_no_remaining_subgoals(&mut self, strand: Strand) -> NoRemainingSubgoalsResult { let ambiguous = strand.ex_clause.ambiguous; if let AnswerMode::Complete = self.forest.tables[self.stack.top().table].answer_mode { if ambiguous { @@ -1037,9 +1058,20 @@ impl<'forest, I: Interner, C: Context + 'forest, CO: ContextOps + 'fore } let num_universes = self.forest.tables[table].table_goal.universes; - let (table, subst, constraints, delayed_subgoals) = self - .context - .instantiate_answer_subst(num_universes, &answer.subst); + let ( + infer, + _, + AnswerSubst { + subst, + constraints, + delayed_subgoals, + }, + ) = chalk_solve::infer::InferenceTable::from_canonical( + self.context.program().interner(), + num_universes, + &answer.subst, + ); + let table = TruncatingInferenceTable::new(self.context.max_size(), infer); let delayed_subgoals = delayed_subgoals .into_iter() @@ -1051,7 +1083,9 @@ impl<'forest, I: Interner, C: Context + 'forest, CO: ContextOps + 'fore ex_clause: ExClause { subst, ambiguous: answer.ambiguous, - constraints, + constraints: constraints + .as_slice(self.context.program().interner()) + .to_vec(), subgoals: delayed_subgoals, delayed_subgoals: Vec::new(), answer_time: TimeStamp::default(), @@ -1239,7 +1273,7 @@ impl<'forest, I: Interner, C: Context + 'forest, CO: ContextOps + 'fore } } - fn select_subgoal(&mut self, mut strand: &mut Strand) -> SubGoalSelection { + fn select_subgoal(&mut self, mut strand: &mut Strand) -> SubGoalSelection { loop { while strand.selected_subgoal.is_none() { if strand.ex_clause.subgoals.is_empty() { @@ -1261,7 +1295,7 @@ impl<'forest, I: Interner, C: Context + 'forest, CO: ContextOps + 'fore continue; } - let subgoal_index = C::next_subgoal_index(&strand.ex_clause); + let subgoal_index = SlgContext::next_subgoal_index(&strand.ex_clause); // Get or create table for this subgoal. match self.forest.get_or_create_table_for_subgoal( @@ -1313,7 +1347,7 @@ impl<'forest, I: Interner, C: Context + 'forest, CO: ContextOps + 'fore /// strand led nowhere of interest. /// - the strand may represent a new answer, in which case it is /// added to the table and `Some(())` is returned. - fn pursue_answer(&mut self, strand: Strand) -> Option { + fn pursue_answer(&mut self, strand: Strand) -> Option { let table = self.stack.top().table; let Strand { mut infer, @@ -1360,7 +1394,7 @@ impl<'forest, I: Interner, C: Context + 'forest, CO: ContextOps + 'fore // Ultimately, the current decision to flounder the entire table mostly boils // down to "it works as we expect for the current tests". And, we likely don't // even *need* the added complexity just for potentially more answers. - if infer.answer_needs_truncation(self.context.interner(), &subst) { + if infer.answer_needs_truncation(self.context.program().interner(), &subst) { self.forest.tables[table].mark_floundered(); return None; } @@ -1371,14 +1405,14 @@ impl<'forest, I: Interner, C: Context + 'forest, CO: ContextOps + 'fore let filtered_delayed_subgoals = delayed_subgoals .into_iter() .filter(|delayed_subgoal| { - let (canonicalized, _) = - infer.fully_canonicalize_goal(self.context.interner(), delayed_subgoal); + let (canonicalized, _) = infer + .fully_canonicalize_goal(self.context.program().interner(), delayed_subgoal); *table_goal != canonicalized }) .collect(); let subst = infer.canonicalize_answer_subst( - self.context.interner(), + self.context.program().interner(), subst, constraints, filtered_delayed_subgoals, @@ -1446,13 +1480,14 @@ impl<'forest, I: Interner, C: Context + 'forest, CO: ContextOps + 'fore // is a *bit* suspect; e.g., those things in the environment // must be backed by an impl *eventually*). let is_trivial_answer = { - self.context - .is_trivial_substitution(&self.forest.tables[table].table_goal, &answer.subst) + self.forest.tables[table] + .table_goal + .is_trivial_substitution(self.context.program().interner(), &answer.subst) && answer .subst .value .constraints - .is_empty(self.context.interner()) + .is_empty(self.context.program().interner()) }; if let Some(answer_index) = self.forest.tables[table].push_answer(answer) { diff --git a/chalk-engine/src/simplify.rs b/chalk-engine/src/simplify.rs index a1087eea825..74ec46c58b3 100644 --- a/chalk-engine/src/simplify.rs +++ b/chalk-engine/src/simplify.rs @@ -1,20 +1,21 @@ -use crate::context::{Context, ContextOps, InferenceTable}; use crate::forest::Forest; +use crate::slg::{SlgContextOps, TruncatingInferenceTable, UnificationOps}; use crate::{ExClause, Literal, TimeStamp}; +use chalk_ir::cast::Cast; use chalk_ir::interner::Interner; use chalk_ir::{ Environment, Fallible, Goal, GoalData, InEnvironment, QuantifierKind, Substitution, }; use tracing::debug; -impl> Forest { +impl Forest { /// Simplifies a goal into a series of positive domain goals /// and negative goals. This operation may fail if the goal /// includes unifications that cannot be completed. pub(super) fn simplify_goal( - context: &impl ContextOps, - infer: &mut dyn InferenceTable, + context: &SlgContextOps, + infer: &mut TruncatingInferenceTable, subst: Substitution, initial_environment: Environment, initial_goal: Goal, @@ -33,23 +34,26 @@ impl> Forest { let mut pending_goals = vec![(initial_environment, initial_goal)]; while let Some((environment, goal)) = pending_goals.pop() { - match goal.data(context.interner()) { + match goal.data(context.program().interner()) { GoalData::Quantified(QuantifierKind::ForAll, subgoal) => { - let subgoal = - infer.instantiate_binders_universally(context.interner(), &subgoal); + let subgoal = infer + .instantiate_binders_universally(context.program().interner(), &subgoal); pending_goals.push((environment, subgoal.clone())); } GoalData::Quantified(QuantifierKind::Exists, subgoal) => { - let subgoal = - infer.instantiate_binders_existentially(context.interner(), &subgoal); + let subgoal = infer + .instantiate_binders_existentially(context.program().interner(), &subgoal); pending_goals.push((environment, subgoal.clone())); } GoalData::Implies(wc, subgoal) => { - let new_environment = context.add_clauses(&environment, wc.clone()); + let new_environment = environment.add_clauses( + context.program().interner(), + wc.iter(context.program().interner()).cloned(), + ); pending_goals.push((new_environment, subgoal.clone())); } GoalData::All(subgoals) => { - for subgoal in subgoals.iter(context.interner()) { + for subgoal in subgoals.iter(context.program().interner()) { pending_goals.push((environment.clone(), subgoal.clone())); } } @@ -62,7 +66,7 @@ impl> Forest { ))); } GoalData::EqGoal(goal) => infer.unify_generic_args_into_ex_clause( - context.interner(), + context.program().interner(), &environment, &goal.a, &goal.b, @@ -73,7 +77,7 @@ impl> Forest { .subgoals .push(Literal::Positive(InEnvironment::new( &environment, - context.into_goal(domain_goal.clone()), + domain_goal.clone().cast(context.program().interner()), ))); } GoalData::CannotProve => { diff --git a/chalk-engine/src/slg.rs b/chalk-engine/src/slg.rs index 640f12cc3ad..5ead945d24a 100644 --- a/chalk-engine/src/slg.rs +++ b/chalk-engine/src/slg.rs @@ -1,14 +1,10 @@ -use crate::context; use crate::normalize_deep::DeepNormalizer; use crate::{ExClause, Literal}; use chalk_derive::HasInterner; -use chalk_ir::cast::Cast; use chalk_ir::cast::Caster; use chalk_ir::interner::Interner; use chalk_ir::*; -use chalk_solve::clauses::program_clauses_for_goal; -use chalk_solve::coinductive_goal::IsCoinductive; use chalk_solve::infer::ucanonicalize::UCanonicalized; use chalk_solve::infer::unify::UnificationResult; use chalk_solve::infer::InferenceTable; @@ -26,6 +22,18 @@ pub(crate) struct SlgContext { phantom: PhantomData, } +impl SlgContext { + pub(crate) fn next_subgoal_index(ex_clause: &ExClause) -> usize { + // For now, we always pick the last subgoal in the + // list. + // + // FIXME(rust-lang-nursery/chalk#80) -- we should be more + // selective. For example, we don't want to pick a + // negative literal that will flounder, and we don't want + // to pick things like `?T: Sized` if we can help it. + ex_clause.subgoals.len() - 1 + } +} #[derive(Clone, Debug)] pub(crate) struct SlgContextOps<'me, I: Interner> { program: &'me dyn RustIrDatabase, @@ -45,131 +53,6 @@ impl SlgContextOps<'_, I> { expected_answers, } } -} - -#[derive(Clone)] -pub struct TruncatingInferenceTable { - max_size: usize, - infer: InferenceTable, -} - -impl context::Context for SlgContext { - type InferenceTable = TruncatingInferenceTable; - - // Used by: logic - fn next_subgoal_index(ex_clause: &ExClause) -> usize { - // For now, we always pick the last subgoal in the - // list. - // - // FIXME(rust-lang-nursery/chalk#80) -- we should be more - // selective. For example, we don't want to pick a - // negative literal that will flounder, and we don't want - // to pick things like `?T: Sized` if we can help it. - ex_clause.subgoals.len() - 1 - } -} - -impl<'me, I: Interner> context::ContextOps> for SlgContextOps<'me, I> { - fn is_coinductive(&self, goal: &UCanonical>>) -> bool { - goal.is_coinductive(self.program) - } - - fn map_goal_from_canonical( - &self, - map: &UniverseMap, - value: &Canonical>>, - ) -> Canonical>> { - use chalk_solve::infer::ucanonicalize::UniverseMapExt; - map.map_from_canonical(self.program.interner(), value) - } - - fn map_subst_from_canonical( - &self, - map: &UniverseMap, - value: &Canonical>, - ) -> Canonical> { - use chalk_solve::infer::ucanonicalize::UniverseMapExt; - map.map_from_canonical(self.program.interner(), value) - } - - fn program_clauses( - &self, - environment: &Environment, - goal: &DomainGoal, - _infer: &mut TruncatingInferenceTable, - ) -> Result>, Floundered> { - let clauses: Vec<_> = program_clauses_for_goal( - self.program, - environment, - goal, - &CanonicalVarKinds::empty(self.program.interner()), - )?; - - Ok(clauses) - } - - // Used by: simplify - fn add_clauses(&self, env: &Environment, clauses: ProgramClauses) -> Environment { - let interner = self.interner(); - env.add_clauses(interner, clauses.iter(interner).cloned()) - } - - fn instantiate_ucanonical_goal( - &self, - arg: &UCanonical>>, - ) -> ( - TruncatingInferenceTable, - Substitution, - Environment, - Goal, - ) { - let (infer, subst, InEnvironment { environment, goal }) = - InferenceTable::from_canonical(self.program.interner(), arg.universes, &arg.canonical); - let infer_table = TruncatingInferenceTable::new(self.max_size, infer); - (infer_table, subst, environment, goal) - } - - fn instantiate_ex_clause( - &self, - num_universes: usize, - canonical_ex_clause: &Canonical>, - ) -> (TruncatingInferenceTable, ExClause) { - let (infer, _subst, ex_cluse) = InferenceTable::from_canonical( - self.program.interner(), - num_universes, - canonical_ex_clause, - ); - let infer_table = TruncatingInferenceTable::new(self.max_size, infer); - (infer_table, ex_cluse) - } - - fn instantiate_answer_subst( - &self, - num_universes: usize, - answer: &Canonical>, - ) -> ( - TruncatingInferenceTable, - Substitution, - Vec>>, - Vec>>, - ) { - let ( - infer, - _subst, - AnswerSubst { - subst, - constraints, - delayed_subgoals, - }, - ) = InferenceTable::from_canonical(self.program.interner(), num_universes, answer); - let infer_table = TruncatingInferenceTable::new(self.max_size, infer); - ( - infer_table, - subst, - constraints.as_slice(self.interner()).to_vec(), - delayed_subgoals, - ) - } fn identity_constrained_subst( &self, @@ -191,39 +74,142 @@ impl<'me, I: Interner> context::ContextOps> for SlgContextOps<' .quantified } - fn interner(&self) -> &I { - self.program.interner() + pub(crate) fn program(&self) -> &dyn RustIrDatabase { + self.program } - fn into_goal(&self, domain_goal: DomainGoal) -> Goal { - domain_goal.cast(self.program.interner()) + pub(crate) fn max_size(&self) -> usize { + self.max_size } +} - fn is_trivial_constrained_substitution( - &self, - constrained_subst: &Canonical>, - ) -> bool { - let interner = self.interner(); - constrained_subst.value.subst.is_identity_subst(interner) - } +/// "Truncation" (called "abstraction" in the papers referenced below) +/// refers to the act of modifying a goal or answer that has become +/// too large in order to guarantee termination. +/// +/// Currently we don't perform truncation (but it might me readded later). +/// +/// Citations: +/// +/// - Terminating Evaluation of Logic Programs with Finite Three-Valued Models +/// - Riguzzi and Swift; ACM Transactions on Computational Logic 2013 +/// - Radial Restraint +/// - Grosof and Swift; 2013 +pub trait TruncateOps { + /// Check if `subgoal` is too large + fn goal_needs_truncation(&mut self, interner: &I, subgoal: &InEnvironment>) -> bool; + + /// Check if `subst` is too large + fn answer_needs_truncation(&mut self, interner: &I, subst: &Substitution) -> bool; +} - fn is_trivial_substitution( - &self, - u_canon: &UCanonical>>, - canonical_subst: &Canonical>, - ) -> bool { - let interner = self.interner(); - u_canon.is_trivial_substitution(interner, canonical_subst) - } +pub trait ResolventOps { + /// Combines the `goal` (instantiated within `infer`) with the + /// given program clause to yield the start of a new strand (a + /// canonical ex-clause). + /// + /// The bindings in `infer` are unaffected by this operation. + fn resolvent_clause( + &mut self, + interner: &I, + environment: &Environment, + goal: &DomainGoal, + subst: &Substitution, + clause: &ProgramClause, + ) -> Fallible>; + + fn apply_answer_subst( + &mut self, + interner: &I, + ex_clause: &mut ExClause, + selected_goal: &InEnvironment>, + answer_table_goal: &Canonical>>, + canonical_answer_subst: &Canonical>, + ) -> Fallible<()>; +} + +/// Methods for unifying and manipulating terms and binders. +pub trait UnificationOps { + // Used by: simplify + fn instantiate_binders_universally(&mut self, interner: &I, arg: &Binders>) -> Goal; + + // Used by: simplify + fn instantiate_binders_existentially( + &mut self, + interner: &I, + arg: &Binders>, + ) -> Goal; + + // Used by: logic (but for debugging only) + fn debug_ex_clause<'v>(&mut self, interner: &I, value: &'v ExClause) -> Box; + + // Used by: logic + fn fully_canonicalize_goal( + &mut self, + interner: &I, + value: &InEnvironment>, + ) -> (UCanonical>>, UniverseMap); + + // Used by: logic + fn canonicalize_ex_clause( + &mut self, + interner: &I, + value: &ExClause, + ) -> Canonical>; + + // Used by: logic + fn canonicalize_constrained_subst( + &mut self, + interner: &I, + subst: Substitution, + constraints: Vec>>, + ) -> Canonical>; + + // Used by: logic + fn canonicalize_answer_subst( + &mut self, + interner: &I, + subst: Substitution, + constraints: Vec>>, + delayed_subgoals: Vec>>, + ) -> Canonical>; + + // Used by: logic + fn invert_goal( + &mut self, + interner: &I, + value: &InEnvironment>, + ) -> Option>>; + + /// First unify the parameters, then add the residual subgoals + /// as new subgoals of the ex-clause. + /// Also add region constraints. + /// + /// If the parameters fail to unify, then `Error` is returned + // Used by: simplify + fn unify_generic_args_into_ex_clause( + &mut self, + interner: &I, + environment: &Environment, + a: &GenericArg, + b: &GenericArg, + ex_clause: &mut ExClause, + ) -> Fallible<()>; +} + +#[derive(Clone)] +pub struct TruncatingInferenceTable { + max_size: usize, + infer: InferenceTable, } impl TruncatingInferenceTable { - fn new(max_size: usize, infer: InferenceTable) -> Self { + pub(crate) fn new(max_size: usize, infer: InferenceTable) -> Self { Self { max_size, infer } } } -impl context::TruncateOps> for TruncatingInferenceTable { +impl TruncateOps for TruncatingInferenceTable { fn goal_needs_truncation(&mut self, interner: &I, subgoal: &InEnvironment>) -> bool { truncate::needs_truncation(interner, &mut self.infer, self.max_size, &subgoal) } @@ -233,9 +219,7 @@ impl context::TruncateOps> for TruncatingInference } } -impl context::InferenceTable> for TruncatingInferenceTable {} - -impl context::UnificationOps> for TruncatingInferenceTable { +impl UnificationOps for TruncatingInferenceTable { fn instantiate_binders_universally(&mut self, interner: &I, arg: &Binders>) -> Goal { self.infer.instantiate_binders_universally(interner, arg) } diff --git a/chalk-engine/src/slg/aggregate.rs b/chalk-engine/src/slg/aggregate.rs index d2387538cc0..09b4f6d079d 100644 --- a/chalk-engine/src/slg/aggregate.rs +++ b/chalk-engine/src/slg/aggregate.rs @@ -1,4 +1,4 @@ -use crate::context::{self, AnswerResult, ContextOps}; +use crate::context::{self, AnswerResult}; use crate::slg::SlgContextOps; use crate::slg::SubstitutionExt; use crate::CompleteAnswer; diff --git a/chalk-engine/src/slg/resolvent.rs b/chalk-engine/src/slg/resolvent.rs index 7cbdd697dd5..2313f519d93 100644 --- a/chalk-engine/src/slg/resolvent.rs +++ b/chalk-engine/src/slg/resolvent.rs @@ -1,6 +1,5 @@ -use crate::context; use crate::normalize_deep::DeepNormalizer; -use crate::slg::{self, SlgContext, TruncatingInferenceTable}; +use crate::slg::{self, ResolventOps, TruncatingInferenceTable}; use crate::{ExClause, Literal, TimeStamp}; use chalk_ir::fold::shift::Shift; use chalk_ir::fold::Fold; @@ -46,7 +45,7 @@ use tracing::{debug, instrument}; // // is the SLG resolvent of G with C. -impl context::ResolventOps> for TruncatingInferenceTable { +impl ResolventOps for TruncatingInferenceTable { /// Applies the SLG resolvent algorithm to incorporate a program /// clause into the main X-clause, producing a new X-clause that /// must be solved. diff --git a/chalk-engine/src/solve.rs b/chalk-engine/src/solve.rs index 6c3b0c321de..fc35adb6638 100644 --- a/chalk-engine/src/solve.rs +++ b/chalk-engine/src/solve.rs @@ -1,7 +1,7 @@ -use crate::context::{AnswerResult, AnswerStream, ContextOps}; +use crate::context::{AnswerResult, AnswerStream}; use crate::forest::Forest; use crate::slg::aggregate::AggregateOps; -use crate::slg::{SlgContext, SlgContextOps}; +use crate::slg::SlgContextOps; use chalk_ir::interner::Interner; use chalk_ir::{Canonical, ConstrainedSubst, Goal, InEnvironment, UCanonical}; use chalk_solve::{RustIrDatabase, Solution, Solver, SubstitutionResult}; @@ -9,7 +9,7 @@ use chalk_solve::{RustIrDatabase, Solution, Solver, SubstitutionResult}; use std::fmt; pub struct SLGSolver { - pub(crate) forest: Forest>, + pub(crate) forest: Forest, pub(crate) max_size: usize, pub(crate) expected_answers: Option, } @@ -63,7 +63,12 @@ impl Solver for SLGSolver { AnswerResult::Answer(answer) => { if !answer.ambiguous { SubstitutionResult::Definite(answer.subst) - } else if ops.is_trivial_constrained_substitution(&answer.subst) { + } else if answer + .subst + .value + .subst + .is_identity_subst(ops.program().interner()) + { SubstitutionResult::Floundered } else { SubstitutionResult::Ambiguous(answer.subst) diff --git a/chalk-engine/src/stack.rs b/chalk-engine/src/stack.rs index 4b2ea059d78..93023c5dc9b 100644 --- a/chalk-engine/src/stack.rs +++ b/chalk-engine/src/stack.rs @@ -1,4 +1,3 @@ -use crate::context::Context; use crate::index_struct; use crate::strand::Strand; use crate::tables::Tables; @@ -10,15 +9,15 @@ use chalk_ir::interner::Interner; /// See `Forest`. #[derive(Debug)] -pub(crate) struct Stack> { +pub(crate) struct Stack { /// Stack: as described above, stores the in-progress goals. - stack: Vec>, + stack: Vec>, } -impl> Stack { +impl Stack { // This isn't actually used, but it can be helpful when debugging stack issues #[allow(dead_code)] - pub(crate) fn debug_with<'a>(&'a self, tables: &'a Tables) -> StackDebug<'_, I, C> { + pub(crate) fn debug_with<'a>(&'a self, tables: &'a Tables) -> StackDebug<'_, I> { StackDebug { stack: self, tables, @@ -26,12 +25,12 @@ impl> Stack { } } -pub(crate) struct StackDebug<'a, I: Interner, C: Context> { - stack: &'a Stack, +pub(crate) struct StackDebug<'a, I: Interner> { + stack: &'a Stack, tables: &'a Tables, } -impl> fmt::Debug for StackDebug<'_, I, C> { +impl fmt::Debug for StackDebug<'_, I> { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { writeln!(f, "---- Stack ----")?; for entry in self.stack.stack.iter() { @@ -53,7 +52,7 @@ impl> fmt::Debug for StackDebug<'_, I, C> { } } -impl> Default for Stack { +impl Default for Stack { fn default() -> Self { Stack { stack: vec![] } } @@ -70,7 +69,7 @@ index_struct! { } #[derive(Debug)] -pub(crate) struct StackEntry> { +pub(crate) struct StackEntry { /// The goal G from the stack entry `A :- G` represented here. pub(super) table: TableIndex, @@ -82,10 +81,10 @@ pub(crate) struct StackEntry> { // FIXME: should store this as an index. // This would mean that if we unwind, // we don't need to worry about losing a strand - pub(super) active_strand: Option>, + pub(super) active_strand: Option>, } -impl> Stack { +impl Stack { pub(super) fn is_empty(&self) -> bool { self.stack.is_empty() } @@ -137,7 +136,7 @@ impl> Stack { /// Pops the top-most entry from the stack, which should have the depth `*depth`: /// * If the stack is now empty, returns None. /// * Otherwise, `take`s the active strand from the new top and returns it. - pub(super) fn pop_and_take_caller_strand(&mut self) -> Option> { + pub(super) fn pop_and_take_caller_strand(&mut self) -> Option> { if self.pop_and_adjust_depth() { Some(self.top().active_strand.take().unwrap()) } else { @@ -148,7 +147,7 @@ impl> Stack { /// Pops the top-most entry from the stack, which should have the depth `*depth`: /// * If the stack is now empty, returns None. /// * Otherwise, borrows the active strand (mutably) from the new top and returns it. - pub(super) fn pop_and_borrow_caller_strand(&mut self) -> Option<&mut Strand> { + pub(super) fn pop_and_borrow_caller_strand(&mut self) -> Option<&mut Strand> { if self.pop_and_adjust_depth() { Some(self.top().active_strand.as_mut().unwrap()) } else { @@ -156,21 +155,21 @@ impl> Stack { } } - pub(super) fn top(&mut self) -> &mut StackEntry { + pub(super) fn top(&mut self) -> &mut StackEntry { self.stack.last_mut().unwrap() } } -impl> Index for Stack { - type Output = StackEntry; +impl Index for Stack { + type Output = StackEntry; - fn index(&self, index: StackIndex) -> &StackEntry { + fn index(&self, index: StackIndex) -> &StackEntry { &self.stack[index.value] } } -impl> IndexMut for Stack { - fn index_mut(&mut self, index: StackIndex) -> &mut StackEntry { +impl IndexMut for Stack { + fn index_mut(&mut self, index: StackIndex) -> &mut StackEntry { &mut self.stack[index.value] } } diff --git a/chalk-engine/src/strand.rs b/chalk-engine/src/strand.rs index bc7f75ea7ba..06dbf3b7450 100644 --- a/chalk-engine/src/strand.rs +++ b/chalk-engine/src/strand.rs @@ -1,4 +1,4 @@ -use crate::context::Context; +use crate::slg::TruncatingInferenceTable; use crate::table::AnswerIndex; use crate::{ExClause, TableIndex, TimeStamp}; use std::fmt::{Debug, Error, Formatter}; @@ -16,8 +16,8 @@ pub(crate) struct CanonicalStrand { pub(crate) last_pursued_time: TimeStamp, } -pub(crate) struct Strand> { - pub(super) infer: C::InferenceTable, +pub(crate) struct Strand { + pub(super) infer: TruncatingInferenceTable, pub(super) ex_clause: ExClause, @@ -43,7 +43,7 @@ pub(crate) struct SelectedSubgoal { pub(crate) universe_map: UniverseMap, } -impl> Debug for Strand { +impl Debug for Strand { fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> { fmt.debug_struct("Strand") .field("ex_clause", &self.ex_clause)