From 9b136cad203cee65756904067059e835122cf225 Mon Sep 17 00:00:00 2001 From: Jack Huey Date: Tue, 1 Dec 2020 13:24:48 -0500 Subject: [PATCH 1/6] Remove RecursiveInferenceTable in favor of just InferneceTable --- chalk-recursive/src/fulfill.rs | 163 +++++++++++++++------------------ chalk-recursive/src/solve.rs | 126 ++----------------------- 2 files changed, 79 insertions(+), 210 deletions(-) diff --git a/chalk-recursive/src/fulfill.rs b/chalk-recursive/src/fulfill.rs index 5078979f616..a7d04d6349c 100644 --- a/chalk-recursive/src/fulfill.rs +++ b/chalk-recursive/src/fulfill.rs @@ -8,11 +8,13 @@ use chalk_ir::zip::Zip; use chalk_ir::{ Binders, Canonical, ConstrainedSubst, Constraint, Constraints, DomainGoal, Environment, EqGoal, Fallible, GenericArg, Goal, GoalData, InEnvironment, NoSolution, ProgramClauseImplication, - QuantifierKind, Substitution, SubtypeGoal, Ty, TyKind, TyVariableKind, UCanonical, + QuantifierKind, Substitution, SubtypeGoal, TyKind, TyVariableKind, UCanonical, UnificationDatabase, UniverseMap, Variance, }; use chalk_solve::debug_span; use chalk_solve::{Guidance, Solution}; +use chalk_solve::infer::{InferenceTable, ParameterEnaVariableExt}; +use chalk_solve::solve::truncate; use rustc_hash::FxHashSet; use std::fmt::Debug; use tracing::{debug, instrument}; @@ -60,68 +62,51 @@ enum NegativeSolution { Ambiguous, } -pub(super) trait RecursiveInferenceTable { - fn instantiate_binders_universally<'a, T>( - &mut self, - interner: &'a I, - arg: Binders, - ) -> T::Result - where - T: Fold + HasInterner; - - fn instantiate_binders_existentially<'a, T>( - &mut self, - interner: &'a I, - arg: Binders, - ) -> T::Result - where - T: Fold + HasInterner; - - fn canonicalize( - &mut self, - interner: &I, - value: T, - ) -> (Canonical, Vec>) - where - T: Fold, - T::Result: HasInterner; - - fn u_canonicalize( - &mut self, - interner: &I, - value0: &Canonical, - ) -> (UCanonical, UniverseMap) - where - T: Clone + HasInterner + Fold + Visit, - T::Result: HasInterner; - - fn unify( - &mut self, - interner: &I, - db: &dyn UnificationDatabase, - environment: &Environment, - variance: Variance, - a: &T, - b: &T, - ) -> Fallible>>> - where - T: ?Sized + Zip; - - fn instantiate_canonical(&mut self, interner: &I, bound: Canonical) -> T::Result - where - T: HasInterner + Fold + Debug; - - fn invert_then_canonicalize( - &mut self, - interner: &I, - value: T, - ) -> Option> - where - T: Fold + HasInterner; +fn canonicalize( + infer: &mut InferenceTable, + interner: &I, + value: T, +) -> (Canonical, Vec>) +where + T: Fold, + T::Result: HasInterner, +{ + let res = infer.canonicalize(interner, value); + let free_vars = res + .free_vars + .into_iter() + .map(|free_var| free_var.to_generic_arg(interner)) + .collect(); + (res.quantified, free_vars) +} - fn needs_truncation(&mut self, interner: &I, max_size: usize, value: impl Visit) -> bool; +fn u_canonicalize( + infer: &mut InferenceTable, + interner: &I, + value0: &Canonical, +) -> (UCanonical, UniverseMap) +where + T: Clone + HasInterner + Fold + Visit, + T::Result: HasInterner, +{ + let res = infer.u_canonicalize(interner, value0); + (res.quantified, res.universes) +} - fn normalize_ty_shallow(&mut self, interner: &I, leaf: &Ty) -> Option>; +fn unify( + infer: &mut InferenceTable, + interner: &I, + db: &dyn UnificationDatabase, + environment: &Environment, + variance: Variance, + a: &T, + b: &T, +) -> Fallible>>> +where + T: ?Sized + Zip, +{ + let res = infer.relate(interner, db, environment, variance, a, b)?; + Ok(res.goals) } /// A `Fulfill` is where we actually break down complex goals, instantiate @@ -134,15 +119,10 @@ pub(super) trait RecursiveInferenceTable { /// of type inference in general. But when solving trait constraints, *fresh* /// `Fulfill` instances will be created to solve canonicalized, free-standing /// goals, and transport what was learned back to the outer context. -pub(super) struct Fulfill< - 's, - I: Interner, - Solver: SolveDatabase, - Infer: RecursiveInferenceTable, -> { +pub(super) struct Fulfill<'s, I: Interner, Solver: SolveDatabase> { solver: &'s mut Solver, subst: Substitution, - infer: Infer, + infer: InferenceTable, /// The remaining goals to prove or refute obligations: Vec>, @@ -157,13 +137,11 @@ pub(super) struct Fulfill< cannot_prove: bool, } -impl<'s, I: Interner, Solver: SolveDatabase, Infer: RecursiveInferenceTable> - Fulfill<'s, I, Solver, Infer> -{ +impl<'s, I: Interner, Solver: SolveDatabase> Fulfill<'s, I, Solver> { #[instrument(level = "debug", skip(solver, infer))] pub(super) fn new_with_clause( solver: &'s mut Solver, - infer: Infer, + infer: InferenceTable, subst: Substitution, canonical_goal: InEnvironment>, clause: &Binders>, @@ -214,7 +192,7 @@ impl<'s, I: Interner, Solver: SolveDatabase, Infer: RecursiveInferenceTable, subst: Substitution, canonical_goal: InEnvironment>, ) -> Fallible { @@ -239,20 +217,24 @@ impl<'s, I: Interner, Solver: SolveDatabase, Infer: RecursiveInferenceTable { - if self - .infer - .needs_truncation(self.solver.interner(), self.solver.max_size(), goal) - { + if truncate::needs_truncation( + self.solver.interner(), + &mut self.infer, + self.solver.max_size(), + goal, + ) { // the goal is too big. Record that we should return Ambiguous self.cannot_prove = true; return; } } Obligation::Refute(goal) => { - if self - .infer - .needs_truncation(self.solver.interner(), self.solver.max_size(), goal) - { + if truncate::needs_truncation( + self.solver.interner(), + &mut self.infer, + self.solver.max_size(), + goal, + ) { // the goal is too big. Record that we should return Ambiguous self.cannot_prove = true; return; @@ -276,7 +258,8 @@ impl<'s, I: Interner, Solver: SolveDatabase, Infer: RecursiveInferenceTable + Debug, { - let goals = self.infer.unify( + let goals = unify( + &mut self.infer, self.solver.interner(), self.solver.db().unification_database(), environment, @@ -369,8 +352,8 @@ impl<'s, I: Interner, Solver: SolveDatabase, Infer: RecursiveInferenceTable Fallible> { let interner = self.solver.interner(); - let (quantified, free_vars) = self.infer.canonicalize(interner, wc); - let (quantified, universes) = self.infer.u_canonicalize(interner, &quantified); + let (quantified, free_vars) = canonicalize(&mut self.infer, interner, wc); + let (quantified, universes) = u_canonicalize(&mut self.infer, interner, &quantified); let result = self.solver.solve_goal(quantified, minimums); Ok(PositiveSolution { free_vars, @@ -393,9 +376,8 @@ impl<'s, I: Interner, Solver: SolveDatabase, Infer: RecursiveInferenceTable, Infer: RecursiveInferenceTable, Infer: RecursiveInferenceTable: Sized { @@ -187,17 +183,12 @@ trait SolveIterationHelpers: SolveDatabase { fn new_inference_table + HasInterner + Clone>( &self, ucanonical_goal: &UCanonical>, - ) -> ( - RecursiveInferenceTableImpl, - Substitution, - InEnvironment, - ) { + ) -> (InferenceTable, Substitution, InEnvironment) { let (infer, subst, canonical_goal) = InferenceTable::from_canonical( self.interner(), ucanonical_goal.universes, ucanonical_goal.canonical.clone(), ); - let infer = RecursiveInferenceTableImpl { infer }; (infer, subst, canonical_goal) } @@ -215,106 +206,3 @@ where I: Interner, { } - -struct RecursiveInferenceTableImpl { - infer: InferenceTable, -} - -impl RecursiveInferenceTable for RecursiveInferenceTableImpl { - fn instantiate_binders_universally<'a, T>( - &mut self, - interner: &'a I, - arg: Binders, - ) -> T::Result - where - T: Fold + HasInterner, - { - self.infer.instantiate_binders_universally(interner, arg) - } - - fn instantiate_binders_existentially<'a, T>( - &mut self, - interner: &'a I, - arg: Binders, - ) -> T::Result - where - T: Fold + HasInterner, - { - self.infer.instantiate_binders_existentially(interner, arg) - } - - fn canonicalize( - &mut self, - interner: &I, - value: T, - ) -> (Canonical, Vec>) - where - T: Fold, - T::Result: HasInterner, - { - let res = self.infer.canonicalize(interner, value); - let free_vars = res - .free_vars - .into_iter() - .map(|free_var| free_var.to_generic_arg(interner)) - .collect(); - (res.quantified, free_vars) - } - - fn u_canonicalize( - &mut self, - interner: &I, - value0: &Canonical, - ) -> (UCanonical, UniverseMap) - where - T: Clone + HasInterner + Fold + Visit, - T::Result: HasInterner, - { - let res = self.infer.u_canonicalize(interner, value0); - (res.quantified, res.universes) - } - - fn unify( - &mut self, - interner: &I, - db: &dyn UnificationDatabase, - environment: &Environment, - variance: Variance, - a: &T, - b: &T, - ) -> Fallible>>> - where - T: ?Sized + Zip, - { - let res = self - .infer - .relate(interner, db, environment, variance, a, b)?; - Ok(res.goals) - } - - fn instantiate_canonical(&mut self, interner: &I, bound: Canonical) -> T::Result - where - T: HasInterner + Fold + Debug, - { - self.infer.instantiate_canonical(interner, bound) - } - - fn invert_then_canonicalize( - &mut self, - interner: &I, - value: T, - ) -> Option> - where - T: Fold + HasInterner, - { - self.infer.invert_then_canonicalize(interner, value) - } - - fn needs_truncation(&mut self, interner: &I, max_size: usize, value: impl Visit) -> bool { - truncate::needs_truncation(interner, &mut self.infer, max_size, value) - } - - fn normalize_ty_shallow(&mut self, interner: &I, leaf: &Ty) -> Option> { - self.infer.normalize_ty_shallow(interner, leaf) - } -} From 8df3156f6f530998070ffb538dc849b6c1c52128 Mon Sep 17 00:00:00 2001 From: Jack Huey Date: Tue, 1 Dec 2020 14:26:19 -0500 Subject: [PATCH 2/6] Remove TruncatingInferenceTable in favor of InferenceTable --- chalk-engine/src/logic.rs | 109 ++++++++---- chalk-engine/src/simplify.rs | 82 +++++---- chalk-engine/src/slg.rs | 278 +----------------------------- chalk-engine/src/slg/resolvent.rs | 50 +++--- chalk-engine/src/strand.rs | 5 +- chalk-ir/src/lib.rs | 3 +- chalk-recursive/src/fulfill.rs | 5 +- chalk-solve/src/solve/truncate.rs | 12 ++ 8 files changed, 175 insertions(+), 369 deletions(-) diff --git a/chalk-engine/src/logic.rs b/chalk-engine/src/logic.rs index 30cb0f1990c..84ab4adda03 100644 --- a/chalk-engine/src/logic.rs +++ b/chalk-engine/src/logic.rs @@ -1,7 +1,6 @@ use crate::forest::Forest; -use crate::slg::{ - ResolventOps, SlgContext, SlgContextOps, TruncateOps, TruncatingInferenceTable, UnificationOps, -}; +use crate::normalize_deep::DeepNormalizer; +use crate::slg::{ResolventOps, SlgContext, SlgContextOps}; use crate::stack::{Stack, StackIndex}; use crate::strand::{CanonicalStrand, SelectedSubgoal, Strand}; use crate::table::{AnswerIndex, Table}; @@ -12,11 +11,14 @@ use crate::{ use chalk_ir::interner::Interner; use chalk_ir::{ - AnswerSubst, Canonical, ConstrainedSubst, FallibleOrFloundered, Floundered, Goal, GoalData, - InEnvironment, NoSolution, Substitution, UCanonical, UniverseMap, + AnswerSubst, Canonical, ConstrainedSubst, Constraints, FallibleOrFloundered, Floundered, Goal, + GoalData, InEnvironment, NoSolution, Substitution, UCanonical, UniverseMap, }; use chalk_solve::clauses::program_clauses_for_goal; use chalk_solve::coinductive_goal::IsCoinductive; +use chalk_solve::infer::ucanonicalize::UCanonicalized; +use chalk_solve::infer::InferenceTable; +use chalk_solve::solve::truncate; use tracing::{debug, debug_span, info, instrument}; type RootSearchResult = Result; @@ -157,13 +159,14 @@ impl Forest { fn canonicalize_strand_from( context: &SlgContextOps, - infer: &mut TruncatingInferenceTable, + infer: &mut InferenceTable, ex_clause: ExClause, selected_subgoal: Option, last_pursued_time: TimeStamp, ) -> CanonicalStrand { - let canonical_ex_clause = - infer.canonicalize_ex_clause(context.program().interner(), ex_clause); + let canonical_ex_clause = infer + .canonicalize(context.program().interner(), ex_clause) + .quantified; CanonicalStrand { canonical_ex_clause, selected_subgoal, @@ -188,7 +191,7 @@ impl Forest { fn get_or_create_table_for_subgoal( &mut self, context: &SlgContextOps, - infer: &mut TruncatingInferenceTable, + infer: &mut InferenceTable, subgoal: &Literal, ) -> Option<(TableIndex, UniverseMap)> { // Subgoal abstraction: @@ -276,7 +279,6 @@ impl Forest { canon_domain_goal.universes, canon_domain_goal.canonical, ); - let infer = TruncatingInferenceTable::new(context.max_size(), infer); match clauses { Ok(clauses) => { @@ -315,13 +317,12 @@ impl Forest { } _ => { - let (infer, subst, InEnvironment { environment, goal }) = + let (mut 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); // The goal for this table is not a domain goal, so we instead // simplify it into a series of *literals*, all of which must be // true. Thus, in EWFS terms, we are effectively creating a @@ -332,7 +333,11 @@ impl Forest { match Self::simplify_goal(context, &mut infer, subst, environment, goal) { FallibleOrFloundered::Ok(ex_clause) => { info!( - ex_clause = ?infer.debug_ex_clause(context.program().interner(), &ex_clause), + ex_clause = ?DeepNormalizer::normalize_deep( + &mut infer, + context.program().interner(), + ex_clause.clone(), + ), "pushing initial strand" ); let strand = Strand { @@ -361,13 +366,25 @@ impl Forest { /// `None`, which causes the subgoal to flounder. fn abstract_positive_literal( context: &SlgContextOps, - infer: &mut TruncatingInferenceTable, + infer: &mut InferenceTable, subgoal: InEnvironment>, ) -> Option<(UCanonical>>, UniverseMap)> { - if infer.goal_needs_truncation(context.program().interner(), &subgoal) { + if truncate::needs_truncation( + context.program().interner(), + infer, + context.max_size(), + &subgoal, + ) { None } else { - Some(infer.fully_canonicalize_goal(context.program().interner(), subgoal)) + let canonicalized_goal = infer + .canonicalize(context.program().interner(), subgoal) + .quantified; + let UCanonicalized { + quantified, + universes, + } = infer.u_canonicalize(context.program().interner(), &canonicalized_goal); + Some((quantified, universes)) } } @@ -380,7 +397,7 @@ impl Forest { /// said to "flounder"). fn abstract_negative_literal( context: &SlgContextOps, - infer: &mut TruncatingInferenceTable, + infer: &mut InferenceTable, subgoal: InEnvironment>, ) -> Option<(UCanonical>>, UniverseMap)> { // First, we have to check that the selected negative literal @@ -420,12 +437,24 @@ 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.program().interner(), subgoal)?; + let inverted_subgoal = infer.invert(context.program().interner(), subgoal)?; - if infer.goal_needs_truncation(context.program().interner(), &inverted_subgoal) { + if truncate::needs_truncation( + context.program().interner(), + infer, + context.max_size(), + &inverted_subgoal, + ) { None } else { - Some(infer.fully_canonicalize_goal(context.program().interner(), inverted_subgoal)) + let canonicalized_goal = infer + .canonicalize(context.program().interner(), inverted_subgoal) + .quantified; + let UCanonicalized { + quantified, + universes, + } = infer.u_canonicalize(context.program().interner(), &canonicalized_goal); + Some((quantified, universes)) } } } @@ -529,7 +558,6 @@ impl<'forest, I: Interner> SolveState<'forest, I> { num_universes, canonical_ex_clause, ); - let infer = TruncatingInferenceTable::new(context.max_size(), infer); Strand { infer, ex_clause, @@ -1092,7 +1120,6 @@ impl<'forest, I: Interner> SolveState<'forest, I> { num_universes, answer.subst.clone(), ); - let table = TruncatingInferenceTable::new(self.context.max_size(), infer); let delayed_subgoals = delayed_subgoals .into_iter() @@ -1100,7 +1127,7 @@ impl<'forest, I: Interner> SolveState<'forest, I> { .collect(); let strand = Strand { - infer: table, + infer, ex_clause: ExClause { subst, ambiguous: answer.ambiguous, @@ -1415,7 +1442,12 @@ impl<'forest, I: Interner> SolveState<'forest, I> { // 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.program().interner(), &subst) { + if truncate::needs_truncation( + self.context.program().interner(), + &mut infer, + self.context.max_size(), + &subst, + ) { self.forest.tables[table].mark_floundered(); return None; } @@ -1426,20 +1458,29 @@ impl<'forest, I: Interner> SolveState<'forest, I> { let filtered_delayed_subgoals = delayed_subgoals .into_iter() .filter(|delayed_subgoal| { - let (canonicalized, _) = infer.fully_canonicalize_goal( - self.context.program().interner(), - delayed_subgoal.clone(), - ); + let canonicalized_goal = infer + .canonicalize(self.context.program().interner(), delayed_subgoal.clone()) + .quantified; + let canonicalized = infer + .u_canonicalize(self.context.program().interner(), &canonicalized_goal) + .quantified; *table_goal != canonicalized }) .collect(); - let subst = infer.canonicalize_answer_subst( - self.context.program().interner(), - subst, - constraints, - filtered_delayed_subgoals, - ); + let subst = infer + .canonicalize( + self.context.program().interner(), + AnswerSubst { + subst, + constraints: Constraints::from_iter( + self.context.program().interner(), + constraints, + ), + delayed_subgoals: filtered_delayed_subgoals, + }, + ) + .quantified; debug!(?table, ?subst, ?floundered, "found answer"); let answer = Answer { subst, ambiguous }; diff --git a/chalk-engine/src/simplify.rs b/chalk-engine/src/simplify.rs index f9a1547e661..1c594af0149 100644 --- a/chalk-engine/src/simplify.rs +++ b/chalk-engine/src/simplify.rs @@ -1,13 +1,14 @@ use crate::forest::Forest; -use crate::slg::{SlgContextOps, TruncatingInferenceTable, UnificationOps}; +use crate::slg::SlgContextOps; use crate::{ExClause, Literal, TimeStamp}; -use chalk_ir::cast::Cast; +use chalk_ir::cast::{Cast, Caster}; use chalk_ir::interner::Interner; use chalk_ir::{ Environment, FallibleOrFloundered, Goal, GoalData, InEnvironment, QuantifierKind, Substitution, - Variance, + TyKind, TyVariableKind, Variance, }; +use chalk_solve::infer::InferenceTable; use tracing::debug; impl Forest { @@ -16,7 +17,7 @@ impl Forest { /// includes unifications that cannot be completed. pub(super) fn simplify_goal( context: &SlgContextOps, - infer: &mut TruncatingInferenceTable, + infer: &mut InferenceTable, subst: Substitution, initial_environment: Environment, initial_goal: Goal, @@ -70,36 +71,55 @@ impl Forest { subgoal.clone(), ))); } - GoalData::EqGoal(goal) => match infer.relate_generic_args_into_ex_clause( - context.program().interner(), - context.unification_database(), - &environment, - Variance::Invariant, - &goal.a, - &goal.b, - &mut ex_clause, - ) { - Ok(()) => {} - Err(_) => return FallibleOrFloundered::NoSolution, - }, + GoalData::EqGoal(goal) => { + let interner = context.program().interner(); + let db = context.unification_database(); + let a = &goal.a; + let b = &goal.b; + + let result = + match infer.relate(interner, db, &environment, Variance::Invariant, a, b) { + Ok(r) => r, + Err(_) => return FallibleOrFloundered::NoSolution, + }; + ex_clause.subgoals.extend( + result + .goals + .into_iter() + .casted(interner) + .map(Literal::Positive), + ); + } GoalData::SubtypeGoal(goal) => { - match infer.relate_tys_into_ex_clause( - context.program().interner(), - context.unification_database(), - &environment, - Variance::Covariant, - &goal.a, - &goal.b, - &mut ex_clause, + let interner = context.program().interner(); + let db = context.unification_database(); + let a_norm = infer.normalize_ty_shallow(interner, &goal.a); + let a = a_norm.as_ref().unwrap_or(&goal.a); + let b_norm = infer.normalize_ty_shallow(interner, &goal.b); + let b = b_norm.as_ref().unwrap_or(&goal.b); + + if matches!( + a.kind(interner), + TyKind::InferenceVar(_, TyVariableKind::General) + ) && matches!( + b.kind(interner), + TyKind::InferenceVar(_, TyVariableKind::General) ) { - FallibleOrFloundered::Ok(_) => {} - FallibleOrFloundered::Floundered => { - return FallibleOrFloundered::Floundered - } - FallibleOrFloundered::NoSolution => { - return FallibleOrFloundered::NoSolution - } + return FallibleOrFloundered::Floundered; } + + let result = + match infer.relate(interner, db, &environment, Variance::Covariant, a, b) { + Ok(r) => r, + Err(_) => return FallibleOrFloundered::Floundered, + }; + ex_clause.subgoals.extend( + result + .goals + .into_iter() + .casted(interner) + .map(Literal::Positive), + ); } GoalData::DomainGoal(domain_goal) => { ex_clause diff --git a/chalk-engine/src/slg.rs b/chalk-engine/src/slg.rs index 30a471b623b..028ef8492ea 100644 --- a/chalk-engine/src/slg.rs +++ b/chalk-engine/src/slg.rs @@ -1,14 +1,9 @@ -use crate::normalize_deep::DeepNormalizer; -use crate::{ExClause, Literal}; +use crate::ExClause; use chalk_derive::HasInterner; -use chalk_ir::cast::Caster; use chalk_ir::interner::Interner; use chalk_ir::*; -use chalk_solve::infer::ucanonicalize::UCanonicalized; -use chalk_solve::infer::unify::RelationResult; use chalk_solve::infer::InferenceTable; -use chalk_solve::solve::truncate; use chalk_solve::RustIrDatabase; use std::fmt::Debug; @@ -87,26 +82,6 @@ impl SlgContextOps<'_, I> { } } -/// "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 @@ -134,257 +109,6 @@ pub trait ResolventOps { ) -> 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 relate_generic_args_into_ex_clause( - &mut self, - interner: &I, - db: &dyn UnificationDatabase, - environment: &Environment, - variance: Variance, - a: &GenericArg, - b: &GenericArg, - ex_clause: &mut ExClause, - ) -> Fallible<()>; - - fn relate_tys_into_ex_clause( - &mut self, - interner: &I, - db: &dyn UnificationDatabase, - environment: &Environment, - variance: Variance, - a: &Ty, - b: &Ty, - ex_clause: &mut ExClause, - ) -> FallibleOrFloundered<()>; -} - -#[derive(Clone)] -pub struct TruncatingInferenceTable { - max_size: usize, - infer: InferenceTable, -} - -impl TruncatingInferenceTable { - pub(crate) fn new(max_size: usize, infer: InferenceTable) -> Self { - Self { max_size, infer } - } -} - -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) - } - - fn answer_needs_truncation(&mut self, interner: &I, subst: &Substitution) -> bool { - truncate::needs_truncation(interner, &mut self.infer, self.max_size, subst) - } -} - -impl UnificationOps for TruncatingInferenceTable { - fn instantiate_binders_universally(&mut self, interner: &I, arg: Binders>) -> Goal { - self.infer.instantiate_binders_universally(interner, arg) - } - - fn instantiate_binders_existentially( - &mut self, - interner: &I, - arg: Binders>, - ) -> Goal { - self.infer.instantiate_binders_existentially(interner, arg) - } - - fn debug_ex_clause<'v>(&mut self, interner: &I, value: &'v ExClause) -> Box { - Box::new(DeepNormalizer::normalize_deep( - &mut self.infer, - interner, - value.clone(), - )) - } - - fn fully_canonicalize_goal( - &mut self, - interner: &I, - value: InEnvironment>, - ) -> (UCanonical>>, UniverseMap) { - let canonicalized_goal = self.infer.canonicalize(interner, value).quantified; - let UCanonicalized { - quantified, - universes, - } = self.infer.u_canonicalize(interner, &canonicalized_goal); - (quantified, universes) - } - - fn canonicalize_ex_clause( - &mut self, - interner: &I, - value: ExClause, - ) -> Canonical> { - self.infer.canonicalize(interner, value).quantified - } - - fn canonicalize_constrained_subst( - &mut self, - interner: &I, - subst: Substitution, - constraints: Vec>>, - ) -> Canonical> { - self.infer - .canonicalize( - interner, - ConstrainedSubst { - subst, - constraints: Constraints::from_iter(interner, constraints), - }, - ) - .quantified - } - - fn canonicalize_answer_subst( - &mut self, - interner: &I, - subst: Substitution, - constraints: Vec>>, - delayed_subgoals: Vec>>, - ) -> Canonical> { - self.infer - .canonicalize( - interner, - AnswerSubst { - subst, - constraints: Constraints::from_iter(interner, constraints), - delayed_subgoals, - }, - ) - .quantified - } - - fn invert_goal( - &mut self, - interner: &I, - value: InEnvironment>, - ) -> Option>> { - self.infer.invert(interner, value) - } - - fn relate_generic_args_into_ex_clause( - &mut self, - interner: &I, - db: &dyn UnificationDatabase, - environment: &Environment, - variance: Variance, - a: &GenericArg, - b: &GenericArg, - ex_clause: &mut ExClause, - ) -> Fallible<()> { - let result = self - .infer - .relate(interner, db, environment, variance, a, b)?; - Ok(into_ex_clause(interner, result, ex_clause)) - } - - fn relate_tys_into_ex_clause( - &mut self, - interner: &I, - db: &dyn UnificationDatabase, - environment: &Environment, - variance: Variance, - a: &Ty, - b: &Ty, - ex_clause: &mut ExClause, - ) -> FallibleOrFloundered<()> { - let a_norm = self.infer.normalize_ty_shallow(interner, a); - let a = a_norm.as_ref().unwrap_or(a); - let b_norm = self.infer.normalize_ty_shallow(interner, b); - let b = b_norm.as_ref().unwrap_or(b); - - if matches!( - a.kind(interner), - TyKind::InferenceVar(_, TyVariableKind::General) - ) && matches!( - b.kind(interner), - TyKind::InferenceVar(_, TyVariableKind::General) - ) { - return FallibleOrFloundered::Floundered; - } - let result = match self.infer.relate(interner, db, environment, variance, a, b) { - Ok(r) => r, - Err(_) => return FallibleOrFloundered::Floundered, - }; - into_ex_clause(interner, result, ex_clause); - FallibleOrFloundered::Ok(()) - } -} - -/// Helper function -fn into_ex_clause( - interner: &I, - result: RelationResult, - ex_clause: &mut ExClause, -) { - ex_clause.subgoals.extend( - result - .goals - .into_iter() - .casted(interner) - .map(Literal::Positive), - ); -} - trait SubstitutionExt { fn may_invalidate(&self, interner: &I, subst: &Canonical>) -> bool; } diff --git a/chalk-engine/src/slg/resolvent.rs b/chalk-engine/src/slg/resolvent.rs index 55df2f76c45..906f8879a95 100644 --- a/chalk-engine/src/slg/resolvent.rs +++ b/chalk-engine/src/slg/resolvent.rs @@ -1,6 +1,7 @@ use crate::normalize_deep::DeepNormalizer; -use crate::slg::{self, ResolventOps, TruncatingInferenceTable}; +use crate::slg::ResolventOps; use crate::{ExClause, Literal, TimeStamp}; +use chalk_ir::cast::Caster; use chalk_ir::fold::shift::Shift; use chalk_ir::fold::Fold; use chalk_ir::interner::{HasInterner, Interner}; @@ -45,7 +46,7 @@ use tracing::{debug, instrument}; // // is the SLG resolvent of G with C. -impl ResolventOps for TruncatingInferenceTable { +impl ResolventOps for InferenceTable { /// Applies the SLG resolvent algorithm to incorporate a program /// clause into the main X-clause, producing a new X-clause that /// must be solved. @@ -81,13 +82,12 @@ impl ResolventOps for TruncatingInferenceTable { } = { let ProgramClauseData(implication) = clause.data(interner); - self.infer - .instantiate_binders_existentially(interner, implication.clone()) + self.instantiate_binders_existentially(interner, implication.clone()) }; debug!(?consequence, ?conditions, ?constraints); // Unify the selected literal Li with C'. - let unification_result = self.infer.relate( + let unification_result = self.relate( interner, db, environment, @@ -108,7 +108,13 @@ impl ResolventOps for TruncatingInferenceTable { }; // Add the subgoals/region-constraints that unification gave us. - slg::into_ex_clause(interner, unification_result, &mut ex_clause); + ex_clause.subgoals.extend( + unification_result + .goals + .into_iter() + .casted(interner) + .map(Literal::Positive), + ); ex_clause .constraints @@ -215,7 +221,7 @@ impl ResolventOps for TruncatingInferenceTable { answer_table_goal: &Canonical>>, canonical_answer_subst: Canonical>, ) -> Fallible<()> { - debug!(selected_goal = ?DeepNormalizer::normalize_deep(&mut self.infer, interner, selected_goal.clone())); + debug!(selected_goal = ?DeepNormalizer::normalize_deep(self, interner, selected_goal.clone())); // C' is now `answer`. No variables in common with G. let AnswerSubst { @@ -229,14 +235,12 @@ impl ResolventOps for TruncatingInferenceTable { constraints: answer_constraints, delayed_subgoals, - } = self - .infer - .instantiate_canonical(interner, canonical_answer_subst); + } = self.instantiate_canonical(interner, canonical_answer_subst); AnswerSubstitutor::substitute( interner, unification_database, - &mut self.infer, + self, &selected_goal.environment, &answer_subst, ex_clause, @@ -322,17 +326,21 @@ impl AnswerSubstitutor<'_, I> { .shifted_out_to(interner, self.outer_binder) .expect("truncate extracted a pending value that references internal binder"); - slg::into_ex_clause( + let result = self.table.relate( interner, - self.table.relate( - interner, - db, - &self.environment, - variance, - answer_param, - &GenericArg::new(interner, pending_shifted), - )?, - self.ex_clause, + db, + &self.environment, + variance, + answer_param, + &GenericArg::new(interner, pending_shifted), + )?; + + self.ex_clause.subgoals.extend( + result + .goals + .into_iter() + .casted(interner) + .map(Literal::Positive), ); Ok(true) diff --git a/chalk-engine/src/strand.rs b/chalk-engine/src/strand.rs index 06dbf3b7450..9c6d9227a70 100644 --- a/chalk-engine/src/strand.rs +++ b/chalk-engine/src/strand.rs @@ -1,4 +1,3 @@ -use crate::slg::TruncatingInferenceTable; use crate::table::AnswerIndex; use crate::{ExClause, TableIndex, TimeStamp}; use std::fmt::{Debug, Error, Formatter}; @@ -6,6 +5,8 @@ use std::fmt::{Debug, Error, Formatter}; use chalk_ir::interner::Interner; use chalk_ir::{Canonical, UniverseMap}; +use chalk_solve::infer::InferenceTable; + #[derive(Debug)] pub(crate) struct CanonicalStrand { pub(super) canonical_ex_clause: Canonical>, @@ -17,7 +18,7 @@ pub(crate) struct CanonicalStrand { } pub(crate) struct Strand { - pub(super) infer: TruncatingInferenceTable, + pub(super) infer: InferenceTable, pub(super) ex_clause: ExClause, diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs index c83f13e17bd..89f69bed9d6 100644 --- a/chalk-ir/src/lib.rs +++ b/chalk-ir/src/lib.rs @@ -39,8 +39,7 @@ pub enum FallibleOrFloundered { #[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] pub struct NoSolution; -/// Error type for the `UnificationOps::program_clauses` method -- -/// indicates that the complete set of program clauses for this goal +/// Indicates that the complete set of program clauses for this goal /// cannot be enumerated. pub struct Floundered; diff --git a/chalk-recursive/src/fulfill.rs b/chalk-recursive/src/fulfill.rs index a7d04d6349c..235185653f3 100644 --- a/chalk-recursive/src/fulfill.rs +++ b/chalk-recursive/src/fulfill.rs @@ -12,9 +12,9 @@ use chalk_ir::{ UnificationDatabase, UniverseMap, Variance, }; use chalk_solve::debug_span; -use chalk_solve::{Guidance, Solution}; use chalk_solve::infer::{InferenceTable, ParameterEnaVariableExt}; use chalk_solve::solve::truncate; +use chalk_solve::{Guidance, Solution}; use rustc_hash::FxHashSet; use std::fmt::Debug; use tracing::{debug, instrument}; @@ -547,7 +547,8 @@ impl<'s, I: Interner, Solver: SolveDatabase> Fulfill<'s, I, Solver> { // need to determine how to package up what we learned about type // inference as an ambiguous solution. - let canonical_subst = canonicalize(&mut self.infer, self.solver.interner(), self.subst.clone()); + let canonical_subst = + canonicalize(&mut self.infer, self.solver.interner(), self.subst.clone()); if canonical_subst .0 diff --git a/chalk-solve/src/solve/truncate.rs b/chalk-solve/src/solve/truncate.rs index 40a34a69ef3..368dbd40732 100644 --- a/chalk-solve/src/solve/truncate.rs +++ b/chalk-solve/src/solve/truncate.rs @@ -6,6 +6,18 @@ use chalk_ir::visit::{ControlFlow, SuperVisit, Visit, Visitor}; use chalk_ir::*; use std::cmp::max; +/// "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 fn needs_truncation( interner: &I, infer: &mut InferenceTable, From 5e5e3abd649de40078f147e8464f88f5fad9727e Mon Sep 17 00:00:00 2001 From: Jack Huey Date: Tue, 1 Dec 2020 15:12:49 -0500 Subject: [PATCH 3/6] Deduplicate a bit of Strand. (Currently slightly more verbose) --- chalk-engine/src/logic.rs | 289 ++++++++++++++++++------------------- chalk-engine/src/stack.rs | 8 +- chalk-engine/src/strand.rs | 52 ++++--- 3 files changed, 176 insertions(+), 173 deletions(-) diff --git a/chalk-engine/src/logic.rs b/chalk-engine/src/logic.rs index 84ab4adda03..45a23d137ac 100644 --- a/chalk-engine/src/logic.rs +++ b/chalk-engine/src/logic.rs @@ -2,7 +2,7 @@ use crate::forest::Forest; use crate::normalize_deep::DeepNormalizer; use crate::slg::{ResolventOps, SlgContext, SlgContextOps}; use crate::stack::{Stack, StackIndex}; -use crate::strand::{CanonicalStrand, SelectedSubgoal, Strand}; +use crate::strand::{CanonicalStrand, InferringStrand, InnerStrand, SelectedSubgoal}; use crate::table::{AnswerIndex, Table}; use crate::{ Answer, AnswerMode, CompleteAnswer, ExClause, FlounderedSubgoal, Literal, Minimums, TableIndex, @@ -134,44 +134,28 @@ impl Forest { // Check any unsolved strands, which may give further answers. self.tables[table] .strands() - .any(|strand| test(&strand.canonical_ex_clause.value.subst)) + .any(|strand| test(&strand.value.ex_clause.subst)) } pub(crate) fn answer(&self, table: TableIndex, answer: AnswerIndex) -> &Answer { self.tables[table].answer(answer).unwrap() } - fn canonicalize_strand(context: &SlgContextOps, strand: Strand) -> CanonicalStrand { - let Strand { - mut infer, - ex_clause, - selected_subgoal, - last_pursued_time, - } = strand; - Forest::canonicalize_strand_from( - context, - &mut infer, - ex_clause, - selected_subgoal, - last_pursued_time, - ) + fn canonicalize_strand( + context: &SlgContextOps, + mut strand: InferringStrand, + ) -> CanonicalStrand { + Forest::canonicalize_strand_from(context, &mut strand.infer, &strand.strand) } fn canonicalize_strand_from( context: &SlgContextOps, infer: &mut InferenceTable, - ex_clause: ExClause, - selected_subgoal: Option, - last_pursued_time: TimeStamp, + strand: &InnerStrand, ) -> CanonicalStrand { - let canonical_ex_clause = infer - .canonicalize(context.program().interner(), ex_clause) - .quantified; - CanonicalStrand { - canonical_ex_clause, - selected_subgoal, - last_pursued_time, - } + infer + .canonicalize(context.program().interner(), strand.clone()) + .quantified } /// Given a subgoal, converts the literal into u-canonical form @@ -294,11 +278,13 @@ impl Forest { &clause, ) { info!("pushing initial strand with ex-clause: {:#?}", &resolvent,); - let strand = Strand { + let strand = InferringStrand { infer, - ex_clause: resolvent, - selected_subgoal: None, - last_pursued_time: TimeStamp::default(), + strand: InnerStrand { + ex_clause: resolvent, + selected_subgoal: None, + last_pursued_time: TimeStamp::default(), + }, }; let canonical_strand = Self::canonicalize_strand(context, strand); table.enqueue_strand(canonical_strand); @@ -340,11 +326,13 @@ impl Forest { ), "pushing initial strand" ); - let strand = Strand { + let strand = InferringStrand { infer, - ex_clause, - selected_subgoal: None, - last_pursued_time: TimeStamp::default(), + strand: InnerStrand { + ex_clause, + selected_subgoal: None, + last_pursued_time: TimeStamp::default(), + }, }; let canonical_strand = Self::canonicalize_strand(context, strand); table.enqueue_strand(canonical_strand); @@ -532,45 +520,29 @@ impl<'forest, I: Interner> SolveState<'forest, I> { let next_strand = self.stack.top().active_strand.take().or_else(|| { forest.tables[table] .dequeue_next_strand_that(|strand| { - let (_, _, ex_clause) = chalk_solve::infer::InferenceTable::from_canonical( - context.program().interner(), - num_universes, - strand.canonical_ex_clause.clone(), - ); - let time_eligble = strand.last_pursued_time < clock; - let mode_eligble = match (table_answer_mode, ex_clause.ambiguous) { - (AnswerMode::Complete, false) => true, - (AnswerMode::Complete, true) => false, - (AnswerMode::Ambiguous, _) => true, - }; + let time_eligble = strand.value.last_pursued_time < clock; + let mode_eligble = + match (table_answer_mode, strand.value.ex_clause.ambiguous) { + (AnswerMode::Complete, false) => true, + (AnswerMode::Complete, true) => false, + (AnswerMode::Ambiguous, _) => true, + }; time_eligble && mode_eligble }) .map(|canonical_strand| { - let CanonicalStrand { - canonical_ex_clause, - selected_subgoal, - last_pursued_time, - } = canonical_strand; - - let (infer, _, ex_clause) = - chalk_solve::infer::InferenceTable::from_canonical( - context.program().interner(), - num_universes, - canonical_ex_clause, - ); - Strand { - infer, - ex_clause, - selected_subgoal, - last_pursued_time, - } + let (infer, _, strand) = chalk_solve::infer::InferenceTable::from_canonical( + context.program().interner(), + num_universes, + canonical_strand, + ); + InferringStrand { infer, strand } }) }); match next_strand { Some(mut strand) => { debug!("starting next strand = {:#?}", strand); - strand.last_pursued_time = clock; + strand.strand.last_pursued_time = clock; match self.select_subgoal(&mut strand) { SubGoalSelection::Selected => { // A subgoal has been selected. We now check this subgoal @@ -603,7 +575,10 @@ impl<'forest, I: Interner> SolveState<'forest, I> { /// 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 InferringStrand, + ) -> 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. @@ -611,7 +586,7 @@ impl<'forest, I: Interner> SolveState<'forest, I> { // If this answer is ambiguous and we don't want ambiguous answers // yet, then we act like this is a floundered subgoal. let ambiguous = { - let selected_subgoal = strand.selected_subgoal.as_ref().unwrap(); + let selected_subgoal = strand.strand.selected_subgoal.as_ref().unwrap(); let answer = self.forest.answer( selected_subgoal.subgoal_table, selected_subgoal.answer_index, @@ -635,8 +610,8 @@ impl<'forest, I: Interner> SolveState<'forest, I> { // The selected subgoal returned an ambiguous answer, but we don't want that. // So, we treat this subgoal as floundered. - let selected_subgoal = strand.selected_subgoal.take().unwrap(); - self.flounder_subgoal(&mut strand.ex_clause, selected_subgoal.subgoal_index); + let selected_subgoal = strand.strand.selected_subgoal.take().unwrap(); + self.flounder_subgoal(&mut strand.strand.ex_clause, selected_subgoal.subgoal_index); return Ok(()); } } @@ -647,8 +622,10 @@ impl<'forest, I: Interner> SolveState<'forest, I> { // Enqueue that alternative for later. // NOTE: this is separate from the match below because we `take` the selected_subgoal // below, but here we keep it for the new `Strand`. - let selected_subgoal = strand.selected_subgoal.as_ref().unwrap(); - if let Literal::Positive(_) = strand.ex_clause.subgoals[selected_subgoal.subgoal_index] { + let selected_subgoal = strand.strand.selected_subgoal.as_ref().unwrap(); + if let Literal::Positive(_) = + strand.strand.ex_clause.subgoals[selected_subgoal.subgoal_index] + { let answer = self.forest.answer( selected_subgoal.subgoal_table, selected_subgoal.answer_index, @@ -659,11 +636,13 @@ impl<'forest, I: Interner> SolveState<'forest, I> { { let mut next_subgoal = selected_subgoal.clone(); next_subgoal.answer_index.increment(); - let next_strand = Strand { + let next_strand = InferringStrand { infer: strand.infer.clone(), - ex_clause: strand.ex_clause.clone(), - selected_subgoal: Some(next_subgoal), - last_pursued_time: strand.last_pursued_time, + strand: InnerStrand { + ex_clause: strand.strand.ex_clause.clone(), + selected_subgoal: Some(next_subgoal), + last_pursued_time: strand.strand.last_pursued_time, + }, }; let table = self.stack.top().table; let canonical_next_strand = Forest::canonicalize_strand(self.context, next_strand); @@ -672,8 +651,9 @@ impl<'forest, I: Interner> SolveState<'forest, I> { } // Deselect and remove the selected subgoal, now that we have an answer for it. - let selected_subgoal = strand.selected_subgoal.take().unwrap(); + let selected_subgoal = strand.strand.selected_subgoal.take().unwrap(); let subgoal = strand + .strand .ex_clause .subgoals .remove(selected_subgoal.subgoal_index); @@ -697,18 +677,13 @@ impl<'forest, I: Interner> SolveState<'forest, I> { match strand.infer.apply_answer_subst( self.context.program().interner(), self.context.unification_database(), - &mut strand.ex_clause, + &mut strand.strand.ex_clause, &subgoal, &table_goal, answer_subst, ) { Ok(()) => { - let Strand { - infer: _, - ex_clause, - selected_subgoal: _, - last_pursued_time: _, - } = strand; + let ex_clause = &mut strand.strand.ex_clause; // If the answer had was ambiguous, we have to // ensure that `ex_clause` is also ambiguous. This is @@ -783,7 +758,7 @@ impl<'forest, I: Interner> SolveState<'forest, I> { // have an unconditional answer for the subgoal, // therefore we have failed to disprove it. debug!(?strand, "Marking Strand as ambiguous because answer to (negative) subgoal was ambiguous"); - strand.ex_clause.ambiguous = true; + strand.strand.ex_clause.ambiguous = true; // Strand is ambigious. return Ok(()); @@ -801,10 +776,10 @@ impl<'forest, I: Interner> SolveState<'forest, I> { /// 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 InferringStrand) -> 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] { + let selected_subgoal = strand.strand.selected_subgoal.take().unwrap(); + match strand.strand.ex_clause.subgoals[selected_subgoal.subgoal_index] { Literal::Positive(_) => { // If this strand depends on this positively, then we can // come back to it later. So, we mark that subgoal as @@ -814,7 +789,7 @@ impl<'forest, I: Interner> SolveState<'forest, I> { // floundered list, along with the time that it // floundered. We'll try to solve some other subgoals // and maybe come back to it. - self.flounder_subgoal(&mut strand.ex_clause, selected_subgoal.subgoal_index); + self.flounder_subgoal(&mut strand.strand.ex_clause, selected_subgoal.subgoal_index); false } @@ -845,7 +820,10 @@ impl<'forest, I: Interner> SolveState<'forest, I> { /// 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: InferringStrand, + ) -> 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 @@ -853,8 +831,9 @@ impl<'forest, I: Interner> SolveState<'forest, I> { // reach a trivial self-cycle. // This subgoal selection for the strand is finished, so take it - let selected_subgoal = strand.selected_subgoal.take().unwrap(); + let selected_subgoal = strand.strand.selected_subgoal.take().unwrap(); match strand + .strand .ex_clause .subgoals .remove(selected_subgoal.subgoal_index) @@ -867,7 +846,7 @@ impl<'forest, I: Interner> SolveState<'forest, I> { && self.forest.tables[selected_subgoal.subgoal_table].coinductive_goal ); - strand.ex_clause.delayed_subgoals.push(subgoal); + strand.strand.ex_clause.delayed_subgoals.push(subgoal); self.stack.top().active_strand = Some(strand); Ok(()) @@ -889,13 +868,13 @@ impl<'forest, I: Interner> SolveState<'forest, I> { /// * `minimums` is the collected minimum clock times fn on_positive_cycle( &mut self, - strand: Strand, + strand: InferringStrand, minimums: Minimums, ) -> Result<(), RootSearchFail> { // We can't take this because we might need it later to clear the cycle - let selected_subgoal = strand.selected_subgoal.as_ref().unwrap(); + let selected_subgoal = strand.strand.selected_subgoal.as_ref().unwrap(); - match strand.ex_clause.subgoals[selected_subgoal.subgoal_index] { + match strand.strand.ex_clause.subgoals[selected_subgoal.subgoal_index] { Literal::Positive(_) => { self.stack.top().cyclic_minimums.take_minimums(&minimums); } @@ -935,7 +914,10 @@ impl<'forest, I: Interner> SolveState<'forest, I> { /// /// * `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: InferringStrand, + ) -> Result<(), RootSearchFail> { // This may be a newly selected subgoal or an existing selected subgoal. let SelectedSubgoal { @@ -943,7 +925,7 @@ impl<'forest, I: Interner> SolveState<'forest, I> { subgoal_table, answer_index, universe_map: _, - } = *strand.selected_subgoal.as_ref().unwrap(); + } = *strand.strand.selected_subgoal.as_ref().unwrap(); debug!( ?subgoal_table, @@ -1017,8 +999,11 @@ impl<'forest, I: Interner> SolveState<'forest, I> { /// 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 { - let ambiguous = strand.ex_clause.ambiguous; + fn on_no_remaining_subgoals( + &mut self, + strand: InferringStrand, + ) -> NoRemainingSubgoalsResult { + let ambiguous = strand.strand.ex_clause.ambiguous; if let AnswerMode::Complete = self.forest.tables[self.stack.top().table].answer_mode { if ambiguous { // The strand can only return an ambiguous answer, but we don't @@ -1028,7 +1013,7 @@ impl<'forest, I: Interner> SolveState<'forest, I> { return NoRemainingSubgoalsResult::RootSearchFail(RootSearchFail::QuantumExceeded); } } - let floundered = !strand.ex_clause.floundered_subgoals.is_empty(); + let floundered = !strand.strand.ex_clause.floundered_subgoals.is_empty(); if floundered { debug!("all remaining subgoals floundered for the table"); } else { @@ -1126,21 +1111,23 @@ impl<'forest, I: Interner> SolveState<'forest, I> { .map(Literal::Positive) .collect(); - let strand = Strand { + let strand = InferringStrand { infer, - ex_clause: ExClause { - subst, - ambiguous: answer.ambiguous, - constraints: constraints - .as_slice(self.context.program().interner()) - .to_vec(), - subgoals: delayed_subgoals, - delayed_subgoals: Vec::new(), - answer_time: TimeStamp::default(), - floundered_subgoals: Vec::new(), + strand: InnerStrand { + ex_clause: ExClause { + subst, + ambiguous: answer.ambiguous, + constraints: constraints + .as_slice(self.context.program().interner()) + .to_vec(), + subgoals: delayed_subgoals, + delayed_subgoals: Vec::new(), + answer_time: TimeStamp::default(), + floundered_subgoals: Vec::new(), + }, + selected_subgoal: None, + last_pursued_time: TimeStamp::default(), }, - selected_subgoal: None, - last_pursued_time: TimeStamp::default(), }; Some(Forest::canonicalize_strand(self.context, strand)) @@ -1170,8 +1157,10 @@ impl<'forest, I: Interner> SolveState<'forest, I> { }; // This subgoal selection for the strand is finished, so take it - let caller_selected_subgoal = caller_strand.selected_subgoal.take().unwrap(); - return match caller_strand.ex_clause.subgoals[caller_selected_subgoal.subgoal_index] { + let caller_selected_subgoal = caller_strand.strand.selected_subgoal.take().unwrap(); + return match caller_strand.strand.ex_clause.subgoals + [caller_selected_subgoal.subgoal_index] + { // T' wanted an answer from T, but none is // forthcoming. Therefore, the active strand from T' // has failed and can be discarded. @@ -1190,6 +1179,7 @@ impl<'forest, I: Interner> SolveState<'forest, I> { // is what we want, so can remove this subgoal and // keep going. caller_strand + .strand .ex_clause .subgoals .remove(caller_selected_subgoal.subgoal_index); @@ -1244,8 +1234,8 @@ impl<'forest, I: Interner> SolveState<'forest, I> { }; // We can't take this because we might need it later to clear the cycle - let caller_selected_subgoal = caller_strand.selected_subgoal.as_ref().unwrap(); - match caller_strand.ex_clause.subgoals[caller_selected_subgoal.subgoal_index] { + let caller_selected_subgoal = caller_strand.strand.selected_subgoal.as_ref().unwrap(); + match caller_strand.strand.ex_clause.subgoals[caller_selected_subgoal.subgoal_index] { Literal::Positive(_) => { self.stack .top() @@ -1302,16 +1292,13 @@ impl<'forest, I: Interner> SolveState<'forest, I> { /// cycles too. fn clear_strands_after_cycle(&mut self, strands: impl IntoIterator>) { for strand in strands { - let CanonicalStrand { - canonical_ex_clause, - selected_subgoal, - last_pursued_time: _, - } = strand; + let selected_subgoal = strand.value.selected_subgoal; + let ex_clause = strand.value.ex_clause; let selected_subgoal = selected_subgoal.unwrap_or_else(|| { panic!( "clear_strands_after_cycle invoked on strand in table \ without a selected subgoal: {:?}", - canonical_ex_clause, + ex_clause, ) }); @@ -1321,38 +1308,38 @@ impl<'forest, I: Interner> SolveState<'forest, I> { } } - fn select_subgoal(&mut self, mut strand: &mut Strand) -> SubGoalSelection { + fn select_subgoal(&mut self, mut strand: &mut InferringStrand) -> SubGoalSelection { loop { - while strand.selected_subgoal.is_none() { - if strand.ex_clause.subgoals.is_empty() { - if strand.ex_clause.floundered_subgoals.is_empty() { + while strand.strand.selected_subgoal.is_none() { + if strand.strand.ex_clause.subgoals.is_empty() { + if strand.strand.ex_clause.floundered_subgoals.is_empty() { return SubGoalSelection::NotSelected; } - self.reconsider_floundered_subgoals(&mut strand.ex_clause); + self.reconsider_floundered_subgoals(&mut strand.strand.ex_clause); - if strand.ex_clause.subgoals.is_empty() { + if strand.strand.ex_clause.subgoals.is_empty() { // All the subgoals of this strand floundered. We may be able // to get helpful information from this strand still, but it // will *always* be ambiguous, so mark it as so. - assert!(!strand.ex_clause.floundered_subgoals.is_empty()); - strand.ex_clause.ambiguous = true; + assert!(!strand.strand.ex_clause.floundered_subgoals.is_empty()); + strand.strand.ex_clause.ambiguous = true; return SubGoalSelection::NotSelected; } continue; } - let subgoal_index = SlgContext::next_subgoal_index(&strand.ex_clause); + let subgoal_index = SlgContext::next_subgoal_index(&strand.strand.ex_clause); // Get or create table for this subgoal. match self.forest.get_or_create_table_for_subgoal( self.context, &mut strand.infer, - &strand.ex_clause.subgoals[subgoal_index], + &strand.strand.ex_clause.subgoals[subgoal_index], ) { Some((subgoal_table, universe_map)) => { - strand.selected_subgoal = Some(SelectedSubgoal { + strand.strand.selected_subgoal = Some(SelectedSubgoal { subgoal_index, subgoal_table, universe_map, @@ -1364,12 +1351,17 @@ impl<'forest, I: Interner> SolveState<'forest, I> { // If we failed to create a table for the subgoal, // that is because we have a floundered negative // literal. - self.flounder_subgoal(&mut strand.ex_clause, subgoal_index); + self.flounder_subgoal(&mut strand.strand.ex_clause, subgoal_index); } } } - let selected_subgoal_table = strand.selected_subgoal.as_ref().unwrap().subgoal_table; + let selected_subgoal_table = strand + .strand + .selected_subgoal + .as_ref() + .unwrap() + .subgoal_table; if self.forest.tables[selected_subgoal_table].is_floundered() { if self.propagate_floundered_subgoal(strand) { // This strand will never lead anywhere of interest. @@ -1395,23 +1387,18 @@ impl<'forest, I: Interner> SolveState<'forest, I> { /// 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: InferringStrand) -> Option { let table = self.stack.top().table; - let Strand { - mut infer, - ex_clause: - ExClause { - subst, - constraints, - ambiguous, - subgoals, - delayed_subgoals, - answer_time: _, - floundered_subgoals, - }, - selected_subgoal: _, - last_pursued_time: _, - } = strand; + let mut infer = strand.infer; + let ExClause { + subst, + constraints, + ambiguous, + subgoals, + delayed_subgoals, + answer_time: _, + floundered_subgoals, + } = strand.strand.ex_clause; // If there are subgoals left, they should be followed assert!(subgoals.is_empty()); // We can still try to get an ambiguous answer if there are floundered subgoals diff --git a/chalk-engine/src/stack.rs b/chalk-engine/src/stack.rs index 93023c5dc9b..d710da95744 100644 --- a/chalk-engine/src/stack.rs +++ b/chalk-engine/src/stack.rs @@ -1,5 +1,5 @@ use crate::index_struct; -use crate::strand::Strand; +use crate::strand::InferringStrand; use crate::tables::Tables; use crate::{Minimums, TableIndex, TimeStamp}; use std::fmt; @@ -81,7 +81,7 @@ 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 { @@ -136,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 { @@ -147,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 InferringStrand> { if self.pop_and_adjust_depth() { Some(self.top().active_strand.as_mut().unwrap()) } else { diff --git a/chalk-engine/src/strand.rs b/chalk-engine/src/strand.rs index 9c6d9227a70..abb58201538 100644 --- a/chalk-engine/src/strand.rs +++ b/chalk-engine/src/strand.rs @@ -1,15 +1,17 @@ use crate::table::AnswerIndex; use crate::{ExClause, TableIndex, TimeStamp}; -use std::fmt::{Debug, Error, Formatter}; +use std::fmt::{self, Debug}; +use chalk_derive::HasInterner; +use chalk_ir::fold::{Fold, Folder}; use chalk_ir::interner::Interner; -use chalk_ir::{Canonical, UniverseMap}; +use chalk_ir::{Canonical, DebruijnIndex, Fallible, UniverseMap}; use chalk_solve::infer::InferenceTable; -#[derive(Debug)] -pub(crate) struct CanonicalStrand { - pub(super) canonical_ex_clause: Canonical>, +#[derive(Clone, Debug, HasInterner)] +pub(crate) struct InnerStrand { + pub(super) ex_clause: ExClause, /// Index into `ex_clause.subgoals`. pub(crate) selected_subgoal: Option, @@ -17,15 +19,12 @@ pub(crate) struct CanonicalStrand { pub(crate) last_pursued_time: TimeStamp, } -pub(crate) struct Strand { - pub(super) infer: InferenceTable, - - pub(super) ex_clause: ExClause, - - /// Index into `ex_clause.subgoals`. - pub(crate) selected_subgoal: Option, +pub(crate) type CanonicalStrand = Canonical>; - pub(crate) last_pursued_time: TimeStamp, +#[derive(HasInterner)] +pub(crate) struct InferringStrand { + pub(crate) strand: InnerStrand, + pub(crate) infer: InferenceTable, } #[derive(Clone, Debug)] @@ -44,11 +43,28 @@ pub(crate) struct SelectedSubgoal { pub(crate) universe_map: UniverseMap, } -impl Debug for Strand { - fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> { - fmt.debug_struct("Strand") - .field("ex_clause", &self.ex_clause) - .field("selected_subgoal", &self.selected_subgoal) +impl Debug for InferringStrand { + fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result { + fmt.debug_struct("InferringStrand") + .field("strand", &self.strand) .finish() } } + +impl Fold for InnerStrand { + type Result = InnerStrand; + fn fold_with<'i>( + self, + folder: &mut dyn Folder<'i, I>, + outer_binder: DebruijnIndex, + ) -> Fallible + where + I: 'i, + { + Ok(InnerStrand { + ex_clause: self.ex_clause.fold_with(folder, outer_binder)?, + last_pursued_time: self.last_pursued_time, + selected_subgoal: self.selected_subgoal.clone(), + }) + } +} From ae3798487e7c67a0fb1e2fee41482825cdc6d0fc Mon Sep 17 00:00:00 2001 From: Jack Huey Date: Tue, 1 Dec 2020 17:48:38 -0500 Subject: [PATCH 4/6] Store strand as Canonical instead of Inferred --- chalk-engine/src/logic.rs | 237 ++++++++++++++----------- chalk-engine/src/stack.rs | 8 +- chalk-recursive/src/fulfill.rs | 4 +- chalk-solve/src/ext.rs | 4 +- chalk-solve/src/infer/ucanonicalize.rs | 6 +- 5 files changed, 139 insertions(+), 120 deletions(-) diff --git a/chalk-engine/src/logic.rs b/chalk-engine/src/logic.rs index 45a23d137ac..d3dee799c90 100644 --- a/chalk-engine/src/logic.rs +++ b/chalk-engine/src/logic.rs @@ -371,7 +371,7 @@ impl Forest { let UCanonicalized { quantified, universes, - } = infer.u_canonicalize(context.program().interner(), &canonicalized_goal); + } = InferenceTable::u_canonicalize(context.program().interner(), &canonicalized_goal); Some((quantified, universes)) } } @@ -441,7 +441,7 @@ impl Forest { let UCanonicalized { quantified, universes, - } = infer.u_canonicalize(context.program().interner(), &canonicalized_goal); + } = InferenceTable::u_canonicalize(context.program().interner(), &canonicalized_goal); Some((quantified, universes)) } } @@ -458,9 +458,7 @@ impl<'forest, I: Interner> Drop for SolveState<'forest, I> { if !self.stack.is_empty() { if let Some(active_strand) = self.stack.top().active_strand.take() { let table = self.stack.top().table; - let canonical_active_strand = - Forest::canonicalize_strand(self.context, active_strand); - self.forest.tables[table].enqueue_strand(canonical_active_strand); + self.forest.tables[table].enqueue_strand(active_strand); } self.unwind_stack(); } @@ -514,46 +512,34 @@ impl<'forest, I: Interner> SolveState<'forest, I> { // We also know that if the first strand has been pursued at this depth, // then all have. Otherwise, an answer to any strand would have provided an // answer for the table. - let num_universes = self.forest.tables[table].table_goal.universes; let forest = &mut self.forest; - let context = &self.context; let next_strand = self.stack.top().active_strand.take().or_else(|| { - forest.tables[table] - .dequeue_next_strand_that(|strand| { - let time_eligble = strand.value.last_pursued_time < clock; - let mode_eligble = - match (table_answer_mode, strand.value.ex_clause.ambiguous) { - (AnswerMode::Complete, false) => true, - (AnswerMode::Complete, true) => false, - (AnswerMode::Ambiguous, _) => true, - }; - time_eligble && mode_eligble - }) - .map(|canonical_strand| { - let (infer, _, strand) = chalk_solve::infer::InferenceTable::from_canonical( - context.program().interner(), - num_universes, - canonical_strand, - ); - InferringStrand { infer, strand } - }) + forest.tables[table].dequeue_next_strand_that(|strand| { + let time_eligble = strand.value.last_pursued_time < clock; + let mode_eligble = match (table_answer_mode, strand.value.ex_clause.ambiguous) { + (AnswerMode::Complete, false) => true, + (AnswerMode::Complete, true) => false, + (AnswerMode::Ambiguous, _) => true, + }; + time_eligble && mode_eligble + }) }); match next_strand { - Some(mut strand) => { - debug!("starting next strand = {:#?}", strand); + Some(mut canonical_strand) => { + debug!("starting next strand = {:#?}", canonical_strand); - strand.strand.last_pursued_time = clock; - match self.select_subgoal(&mut strand) { + canonical_strand.value.last_pursued_time = clock; + match self.select_subgoal(&mut canonical_strand) { SubGoalSelection::Selected => { // A subgoal has been selected. We now check this subgoal // table for an existing answer or if it's in a cycle. // If neither of those are the case, a strand is selected // and the next loop iteration happens. - self.on_subgoal_selected(strand)?; + self.on_subgoal_selected(canonical_strand)?; continue; } SubGoalSelection::NotSelected => { - match self.on_no_remaining_subgoals(strand) { + match self.on_no_remaining_subgoals(canonical_strand) { NoRemainingSubgoalsResult::RootAnswerAvailable => return Ok(()), NoRemainingSubgoalsResult::RootSearchFail(e) => return Err(e), NoRemainingSubgoalsResult::Success => continue, @@ -776,10 +762,10 @@ impl<'forest, I: Interner> SolveState<'forest, I> { /// be discarded. /// /// In other words, we return whether this strand flounders. - fn propagate_floundered_subgoal(&mut self, strand: &mut InferringStrand) -> bool { + fn propagate_floundered_subgoal(&mut self, strand: &mut CanonicalStrand) -> bool { // This subgoal selection for the strand is finished, so take it - let selected_subgoal = strand.strand.selected_subgoal.take().unwrap(); - match strand.strand.ex_clause.subgoals[selected_subgoal.subgoal_index] { + let selected_subgoal = strand.value.selected_subgoal.take().unwrap(); + match strand.value.ex_clause.subgoals[selected_subgoal.subgoal_index] { Literal::Positive(_) => { // If this strand depends on this positively, then we can // come back to it later. So, we mark that subgoal as @@ -789,7 +775,7 @@ impl<'forest, I: Interner> SolveState<'forest, I> { // floundered list, along with the time that it // floundered. We'll try to solve some other subgoals // and maybe come back to it. - self.flounder_subgoal(&mut strand.strand.ex_clause, selected_subgoal.subgoal_index); + self.flounder_subgoal(&mut strand.value.ex_clause, selected_subgoal.subgoal_index); false } @@ -822,7 +808,7 @@ impl<'forest, I: Interner> SolveState<'forest, I> { /// a coinductive cycle. fn on_coinductive_subgoal( &mut self, - mut strand: InferringStrand, + mut canonical_strand: CanonicalStrand, ) -> Result<(), RootSearchFail> { // This is a co-inductive cycle. That is, this table // appears somewhere higher on the stack, and has now @@ -831,9 +817,9 @@ impl<'forest, I: Interner> SolveState<'forest, I> { // reach a trivial self-cycle. // This subgoal selection for the strand is finished, so take it - let selected_subgoal = strand.strand.selected_subgoal.take().unwrap(); - match strand - .strand + let selected_subgoal = canonical_strand.value.selected_subgoal.take().unwrap(); + match canonical_strand + .value .ex_clause .subgoals .remove(selected_subgoal.subgoal_index) @@ -846,9 +832,13 @@ impl<'forest, I: Interner> SolveState<'forest, I> { && self.forest.tables[selected_subgoal.subgoal_table].coinductive_goal ); - strand.strand.ex_clause.delayed_subgoals.push(subgoal); + canonical_strand + .value + .ex_clause + .delayed_subgoals + .push(subgoal); - self.stack.top().active_strand = Some(strand); + self.stack.top().active_strand = Some(canonical_strand); Ok(()) } Literal::Negative(_) => { @@ -868,13 +858,13 @@ impl<'forest, I: Interner> SolveState<'forest, I> { /// * `minimums` is the collected minimum clock times fn on_positive_cycle( &mut self, - strand: InferringStrand, + canonical_strand: CanonicalStrand, minimums: Minimums, ) -> Result<(), RootSearchFail> { // We can't take this because we might need it later to clear the cycle - let selected_subgoal = strand.strand.selected_subgoal.as_ref().unwrap(); + let selected_subgoal = canonical_strand.value.selected_subgoal.as_ref().unwrap(); - match strand.strand.ex_clause.subgoals[selected_subgoal.subgoal_index] { + match canonical_strand.value.ex_clause.subgoals[selected_subgoal.subgoal_index] { Literal::Positive(_) => { self.stack.top().cyclic_minimums.take_minimums(&minimums); } @@ -900,7 +890,6 @@ impl<'forest, I: Interner> SolveState<'forest, I> { // We also can't mark these and return early from this // because the stack above us might change. let table = self.stack.top().table; - let canonical_strand = Forest::canonicalize_strand(self.context, strand); self.forest.tables[table].enqueue_strand(canonical_strand); // The strand isn't active, but the table is, so just continue @@ -916,7 +905,7 @@ impl<'forest, I: Interner> SolveState<'forest, I> { /// * `Err` if the subgoal failed in some way such that the strand can be abandoned. fn on_subgoal_selected( &mut self, - mut strand: InferringStrand, + mut canonical_strand: CanonicalStrand, ) -> Result<(), RootSearchFail> { // This may be a newly selected subgoal or an existing selected subgoal. @@ -925,7 +914,7 @@ impl<'forest, I: Interner> SolveState<'forest, I> { subgoal_table, answer_index, universe_map: _, - } = *strand.strand.selected_subgoal.as_ref().unwrap(); + } = *canonical_strand.value.selected_subgoal.as_ref().unwrap(); debug!( ?subgoal_table, @@ -943,6 +932,15 @@ impl<'forest, I: Interner> SolveState<'forest, I> { // There was a previous answer available for this table // We need to check if we can merge it into the current `Strand`. + let num_universes = self.forest.tables[self.stack.top().table] + .table_goal + .universes; + let (infer, _, strand) = chalk_solve::infer::InferenceTable::from_canonical( + self.context.program().interner(), + num_universes, + canonical_strand.clone(), + ); + let mut strand = InferringStrand { infer, strand }; match self.merge_answer_into_strand(&mut strand) { Err(e) => { debug!(?strand, "could not merge into current strand"); @@ -951,7 +949,12 @@ impl<'forest, I: Interner> SolveState<'forest, I> { } Ok(_) => { debug!(?strand, "merged answer into current strand"); - self.stack.top().active_strand = Some(strand); + canonical_strand = Forest::canonicalize_strand_from( + &self.context, + &mut strand.infer, + &strand.strand, + ); + self.stack.top().active_strand = Some(canonical_strand); return Ok(()); } } @@ -975,16 +978,16 @@ impl<'forest, I: Interner> SolveState<'forest, I> { if self.top_of_stack_is_coinductive_from(cyclic_depth) { debug!("table is coinductive"); - return self.on_coinductive_subgoal(strand); + return self.on_coinductive_subgoal(canonical_strand); } debug!("table encountered a positive cycle"); - return self.on_positive_cycle(strand, minimums); + return self.on_positive_cycle(canonical_strand, minimums); } // We don't know anything about the selected subgoal table. // Set this strand as active and push it onto the stack. - self.stack.top().active_strand = Some(strand); + self.stack.top().active_strand = Some(canonical_strand); let cyclic_minimums = Minimums::MAX; self.stack.push( @@ -1001,25 +1004,28 @@ impl<'forest, I: Interner> SolveState<'forest, I> { /// add the answer from the strand onto the table. fn on_no_remaining_subgoals( &mut self, - strand: InferringStrand, + canonical_strand: CanonicalStrand, ) -> NoRemainingSubgoalsResult { - let ambiguous = strand.strand.ex_clause.ambiguous; + let ambiguous = canonical_strand.value.ex_clause.ambiguous; if let AnswerMode::Complete = self.forest.tables[self.stack.top().table].answer_mode { if ambiguous { // The strand can only return an ambiguous answer, but we don't // want that right now, so requeue and we'll deal with it later. - let canonical_strand = Forest::canonicalize_strand(self.context, strand); self.forest.tables[self.stack.top().table].enqueue_strand(canonical_strand); return NoRemainingSubgoalsResult::RootSearchFail(RootSearchFail::QuantumExceeded); } } - let floundered = !strand.strand.ex_clause.floundered_subgoals.is_empty(); + let floundered = !canonical_strand + .value + .ex_clause + .floundered_subgoals + .is_empty(); if floundered { debug!("all remaining subgoals floundered for the table"); } else { debug!("no remaining subgoals for the table"); }; - match self.pursue_answer(strand) { + match self.pursue_answer(canonical_strand) { Some(answer_index) => { debug!("answer is available"); @@ -1157,8 +1163,8 @@ impl<'forest, I: Interner> SolveState<'forest, I> { }; // This subgoal selection for the strand is finished, so take it - let caller_selected_subgoal = caller_strand.strand.selected_subgoal.take().unwrap(); - return match caller_strand.strand.ex_clause.subgoals + let caller_selected_subgoal = caller_strand.value.selected_subgoal.take().unwrap(); + return match caller_strand.value.ex_clause.subgoals [caller_selected_subgoal.subgoal_index] { // T' wanted an answer from T, but none is @@ -1179,7 +1185,7 @@ impl<'forest, I: Interner> SolveState<'forest, I> { // is what we want, so can remove this subgoal and // keep going. caller_strand - .strand + .value .ex_clause .subgoals .remove(caller_selected_subgoal.subgoal_index); @@ -1234,8 +1240,8 @@ impl<'forest, I: Interner> SolveState<'forest, I> { }; // We can't take this because we might need it later to clear the cycle - let caller_selected_subgoal = caller_strand.strand.selected_subgoal.as_ref().unwrap(); - match caller_strand.strand.ex_clause.subgoals[caller_selected_subgoal.subgoal_index] { + let caller_selected_subgoal = caller_strand.value.selected_subgoal.as_ref().unwrap(); + match caller_strand.value.ex_clause.subgoals[caller_selected_subgoal.subgoal_index] { Literal::Positive(_) => { self.stack .top() @@ -1259,8 +1265,7 @@ impl<'forest, I: Interner> SolveState<'forest, I> { // We can't pursue this strand anymore, so push it back onto the table let active_strand = self.stack.top().active_strand.take().unwrap(); let table = self.stack.top().table; - let canonical_active_strand = Forest::canonicalize_strand(self.context, active_strand); - self.forest.tables[table].enqueue_strand(canonical_active_strand); + self.forest.tables[table].enqueue_strand(active_strand); // The strand isn't active, but the table is, so just continue return Ok(()); @@ -1274,9 +1279,7 @@ impl<'forest, I: Interner> SolveState<'forest, I> { match self.stack.pop_and_take_caller_strand() { Some(active_strand) => { let table = self.stack.top().table; - let canonical_active_strand = - Forest::canonicalize_strand(self.context, active_strand); - self.forest.tables[table].enqueue_strand(canonical_active_strand); + self.forest.tables[table].enqueue_strand(active_strand); } None => return, @@ -1308,38 +1311,59 @@ impl<'forest, I: Interner> SolveState<'forest, I> { } } - fn select_subgoal(&mut self, mut strand: &mut InferringStrand) -> SubGoalSelection { + fn select_subgoal( + &mut self, + mut canonical_strand: &mut CanonicalStrand, + ) -> SubGoalSelection { loop { - while strand.strand.selected_subgoal.is_none() { - if strand.strand.ex_clause.subgoals.is_empty() { - if strand.strand.ex_clause.floundered_subgoals.is_empty() { + while canonical_strand.value.selected_subgoal.is_none() { + if canonical_strand.value.ex_clause.subgoals.is_empty() { + if canonical_strand + .value + .ex_clause + .floundered_subgoals + .is_empty() + { return SubGoalSelection::NotSelected; } - self.reconsider_floundered_subgoals(&mut strand.strand.ex_clause); + self.reconsider_floundered_subgoals(&mut canonical_strand.value.ex_clause); - if strand.strand.ex_clause.subgoals.is_empty() { + if canonical_strand.value.ex_clause.subgoals.is_empty() { // All the subgoals of this strand floundered. We may be able // to get helpful information from this strand still, but it // will *always* be ambiguous, so mark it as so. - assert!(!strand.strand.ex_clause.floundered_subgoals.is_empty()); - strand.strand.ex_clause.ambiguous = true; + assert!(!canonical_strand + .value + .ex_clause + .floundered_subgoals + .is_empty()); + canonical_strand.value.ex_clause.ambiguous = true; return SubGoalSelection::NotSelected; } continue; } - let subgoal_index = SlgContext::next_subgoal_index(&strand.strand.ex_clause); + let subgoal_index = + SlgContext::next_subgoal_index(&canonical_strand.value.ex_clause); // Get or create table for this subgoal. + let num_universes = self.forest.tables[self.stack.top().table] + .table_goal + .universes; + let (mut infer, _, strand) = chalk_solve::infer::InferenceTable::from_canonical( + self.context.program().interner(), + num_universes, + canonical_strand.clone(), + ); match self.forest.get_or_create_table_for_subgoal( self.context, - &mut strand.infer, - &strand.strand.ex_clause.subgoals[subgoal_index], + &mut infer, + &strand.ex_clause.subgoals[subgoal_index], ) { Some((subgoal_table, universe_map)) => { - strand.strand.selected_subgoal = Some(SelectedSubgoal { + canonical_strand.value.selected_subgoal = Some(SelectedSubgoal { subgoal_index, subgoal_table, universe_map, @@ -1351,19 +1375,19 @@ impl<'forest, I: Interner> SolveState<'forest, I> { // If we failed to create a table for the subgoal, // that is because we have a floundered negative // literal. - self.flounder_subgoal(&mut strand.strand.ex_clause, subgoal_index); + self.flounder_subgoal(&mut canonical_strand.value.ex_clause, subgoal_index); } } } - let selected_subgoal_table = strand - .strand + let selected_subgoal_table = canonical_strand + .value .selected_subgoal .as_ref() .unwrap() .subgoal_table; if self.forest.tables[selected_subgoal_table].is_floundered() { - if self.propagate_floundered_subgoal(strand) { + if self.propagate_floundered_subgoal(canonical_strand) { // This strand will never lead anywhere of interest. return SubGoalSelection::NotSelected; } else { @@ -1387,9 +1411,12 @@ impl<'forest, I: Interner> SolveState<'forest, I> { /// 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: InferringStrand) -> Option { + fn pursue_answer(&mut self, canonical_strand: CanonicalStrand) -> Option { let table = self.stack.top().table; - let mut infer = strand.infer; + let Canonical { + binders, + value: strand, + } = canonical_strand; let ExClause { subst, constraints, @@ -1398,7 +1425,7 @@ impl<'forest, I: Interner> SolveState<'forest, I> { delayed_subgoals, answer_time: _, floundered_subgoals, - } = strand.strand.ex_clause; + } = strand.ex_clause; // If there are subgoals left, they should be followed assert!(subgoals.is_empty()); // We can still try to get an ambiguous answer if there are floundered subgoals @@ -1431,7 +1458,7 @@ impl<'forest, I: Interner> SolveState<'forest, I> { // even *need* the added complexity just for potentially more answers. if truncate::needs_truncation( self.context.program().interner(), - &mut infer, + &mut InferenceTable::new(), self.context.max_size(), &subst, ) { @@ -1441,33 +1468,29 @@ impl<'forest, I: Interner> SolveState<'forest, I> { let table_goal = &self.forest.tables[table].table_goal; - // FIXME: Avoid double canonicalization let filtered_delayed_subgoals = delayed_subgoals .into_iter() .filter(|delayed_subgoal| { - let canonicalized_goal = infer - .canonicalize(self.context.program().interner(), delayed_subgoal.clone()) - .quantified; - let canonicalized = infer - .u_canonicalize(self.context.program().interner(), &canonicalized_goal) - .quantified; + let canonicalized = InferenceTable::u_canonicalize( + self.context.program().interner(), + &chalk_ir::Canonical { + binders: binders.clone(), + value: delayed_subgoal.clone(), + }, + ) + .quantified; *table_goal != canonicalized }) .collect(); - let subst = infer - .canonicalize( - self.context.program().interner(), - AnswerSubst { - subst, - constraints: Constraints::from_iter( - self.context.program().interner(), - constraints, - ), - delayed_subgoals: filtered_delayed_subgoals, - }, - ) - .quantified; + let subst = Canonical { + binders: binders.clone(), + value: AnswerSubst { + subst, + constraints: Constraints::from_iter(self.context.program().interner(), constraints), + delayed_subgoals: filtered_delayed_subgoals, + }, + }; debug!(?table, ?subst, ?floundered, "found answer"); let answer = Answer { subst, ambiguous }; diff --git a/chalk-engine/src/stack.rs b/chalk-engine/src/stack.rs index d710da95744..66b53fa582f 100644 --- a/chalk-engine/src/stack.rs +++ b/chalk-engine/src/stack.rs @@ -1,5 +1,5 @@ use crate::index_struct; -use crate::strand::InferringStrand; +use crate::strand::CanonicalStrand; use crate::tables::Tables; use crate::{Minimums, TableIndex, TimeStamp}; use std::fmt; @@ -81,7 +81,7 @@ 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 { @@ -136,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 { @@ -147,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 InferringStrand> { + pub(super) fn pop_and_borrow_caller_strand(&mut self) -> Option<&mut CanonicalStrand> { if self.pop_and_adjust_depth() { Some(self.top().active_strand.as_mut().unwrap()) } else { diff --git a/chalk-recursive/src/fulfill.rs b/chalk-recursive/src/fulfill.rs index 235185653f3..a6296d7213a 100644 --- a/chalk-recursive/src/fulfill.rs +++ b/chalk-recursive/src/fulfill.rs @@ -81,7 +81,7 @@ where } fn u_canonicalize( - infer: &mut InferenceTable, + _infer: &mut InferenceTable, interner: &I, value0: &Canonical, ) -> (UCanonical, UniverseMap) @@ -89,7 +89,7 @@ where T: Clone + HasInterner + Fold + Visit, T::Result: HasInterner, { - let res = infer.u_canonicalize(interner, value0); + let res = InferenceTable::u_canonicalize(interner, value0); (res.quantified, res.universes) } diff --git a/chalk-solve/src/ext.rs b/chalk-solve/src/ext.rs index 8fb57c9a399..ee44845a429 100644 --- a/chalk-solve/src/ext.rs +++ b/chalk-solve/src/ext.rs @@ -92,7 +92,7 @@ impl GoalExt for Goal { } }; let canonical = infer.canonicalize(interner, peeled_goal).quantified; - infer.u_canonicalize(interner, &canonical).quantified + InferenceTable::u_canonicalize(interner, &canonical).quantified } /// Given a goal with no free variables (a "closed" goal), creates @@ -108,6 +108,6 @@ impl GoalExt for Goal { let mut infer = InferenceTable::new(); let env_goal = InEnvironment::new(&Environment::new(interner), self); let canonical_goal = infer.canonicalize(interner, env_goal).quantified; - infer.u_canonicalize(interner, &canonical_goal).quantified + InferenceTable::u_canonicalize(interner, &canonical_goal).quantified } } diff --git a/chalk-solve/src/infer/ucanonicalize.rs b/chalk-solve/src/infer/ucanonicalize.rs index 4bc7a989c35..2c4958e3f39 100644 --- a/chalk-solve/src/infer/ucanonicalize.rs +++ b/chalk-solve/src/infer/ucanonicalize.rs @@ -7,11 +7,7 @@ use chalk_ir::*; use super::InferenceTable; impl InferenceTable { - pub fn u_canonicalize( - &mut self, - interner: &I, - value0: &Canonical, - ) -> UCanonicalized + pub fn u_canonicalize(interner: &I, value0: &Canonical) -> UCanonicalized where T: Clone + HasInterner + Fold + Visit, T::Result: HasInterner, From f8ee5293561ddd3938942af44984df1d27f8078b Mon Sep 17 00:00:00 2001 From: Jack Huey Date: Tue, 1 Dec 2020 18:39:36 -0500 Subject: [PATCH 5/6] Remove InferringStrand and rename InnerStrand to Strand --- chalk-engine/src/logic.rs | 128 ++++++++++++++++--------------------- chalk-engine/src/strand.rs | 28 ++------ 2 files changed, 61 insertions(+), 95 deletions(-) diff --git a/chalk-engine/src/logic.rs b/chalk-engine/src/logic.rs index d3dee799c90..97b12e9df04 100644 --- a/chalk-engine/src/logic.rs +++ b/chalk-engine/src/logic.rs @@ -2,7 +2,7 @@ use crate::forest::Forest; use crate::normalize_deep::DeepNormalizer; use crate::slg::{ResolventOps, SlgContext, SlgContextOps}; use crate::stack::{Stack, StackIndex}; -use crate::strand::{CanonicalStrand, InferringStrand, InnerStrand, SelectedSubgoal}; +use crate::strand::{CanonicalStrand, SelectedSubgoal, Strand}; use crate::table::{AnswerIndex, Table}; use crate::{ Answer, AnswerMode, CompleteAnswer, ExClause, FlounderedSubgoal, Literal, Minimums, TableIndex, @@ -141,17 +141,10 @@ impl Forest { self.tables[table].answer(answer).unwrap() } - fn canonicalize_strand( - context: &SlgContextOps, - mut strand: InferringStrand, - ) -> CanonicalStrand { - Forest::canonicalize_strand_from(context, &mut strand.infer, &strand.strand) - } - fn canonicalize_strand_from( context: &SlgContextOps, infer: &mut InferenceTable, - strand: &InnerStrand, + strand: &Strand, ) -> CanonicalStrand { infer .canonicalize(context.program().interner(), strand.clone()) @@ -278,15 +271,13 @@ impl Forest { &clause, ) { info!("pushing initial strand with ex-clause: {:#?}", &resolvent,); - let strand = InferringStrand { - infer, - strand: InnerStrand { - ex_clause: resolvent, - selected_subgoal: None, - last_pursued_time: TimeStamp::default(), - }, + let strand = Strand { + ex_clause: resolvent, + selected_subgoal: None, + last_pursued_time: TimeStamp::default(), }; - let canonical_strand = Self::canonicalize_strand(context, strand); + let canonical_strand = + Self::canonicalize_strand_from(context, &mut infer, &strand); table.enqueue_strand(canonical_strand); } } @@ -326,15 +317,13 @@ impl Forest { ), "pushing initial strand" ); - let strand = InferringStrand { - infer, - strand: InnerStrand { - ex_clause, - selected_subgoal: None, - last_pursued_time: TimeStamp::default(), - }, + let strand = Strand { + ex_clause, + selected_subgoal: None, + last_pursued_time: TimeStamp::default(), }; - let canonical_strand = Self::canonicalize_strand(context, strand); + let canonical_strand = + Self::canonicalize_strand_from(context, &mut infer, &strand); table.enqueue_strand(canonical_strand); } FallibleOrFloundered::NoSolution => {} @@ -563,7 +552,8 @@ impl<'forest, I: Interner> SolveState<'forest, I> { /// On failure, `Err` is returned and the `Strand` should be discarded fn merge_answer_into_strand( &mut self, - strand: &mut InferringStrand, + infer: &mut InferenceTable, + strand: &mut Strand, ) -> RootSearchResult<()> { // At this point, we know we have an answer for // the selected subgoal of the strand. @@ -572,7 +562,7 @@ impl<'forest, I: Interner> SolveState<'forest, I> { // If this answer is ambiguous and we don't want ambiguous answers // yet, then we act like this is a floundered subgoal. let ambiguous = { - let selected_subgoal = strand.strand.selected_subgoal.as_ref().unwrap(); + let selected_subgoal = strand.selected_subgoal.as_ref().unwrap(); let answer = self.forest.answer( selected_subgoal.subgoal_table, selected_subgoal.answer_index, @@ -596,8 +586,8 @@ impl<'forest, I: Interner> SolveState<'forest, I> { // The selected subgoal returned an ambiguous answer, but we don't want that. // So, we treat this subgoal as floundered. - let selected_subgoal = strand.strand.selected_subgoal.take().unwrap(); - self.flounder_subgoal(&mut strand.strand.ex_clause, selected_subgoal.subgoal_index); + let selected_subgoal = strand.selected_subgoal.take().unwrap(); + self.flounder_subgoal(&mut strand.ex_clause, selected_subgoal.subgoal_index); return Ok(()); } } @@ -608,10 +598,8 @@ impl<'forest, I: Interner> SolveState<'forest, I> { // Enqueue that alternative for later. // NOTE: this is separate from the match below because we `take` the selected_subgoal // below, but here we keep it for the new `Strand`. - let selected_subgoal = strand.strand.selected_subgoal.as_ref().unwrap(); - if let Literal::Positive(_) = - strand.strand.ex_clause.subgoals[selected_subgoal.subgoal_index] - { + let selected_subgoal = strand.selected_subgoal.as_ref().unwrap(); + if let Literal::Positive(_) = strand.ex_clause.subgoals[selected_subgoal.subgoal_index] { let answer = self.forest.answer( selected_subgoal.subgoal_table, selected_subgoal.answer_index, @@ -622,24 +610,21 @@ impl<'forest, I: Interner> SolveState<'forest, I> { { let mut next_subgoal = selected_subgoal.clone(); next_subgoal.answer_index.increment(); - let next_strand = InferringStrand { - infer: strand.infer.clone(), - strand: InnerStrand { - ex_clause: strand.strand.ex_clause.clone(), - selected_subgoal: Some(next_subgoal), - last_pursued_time: strand.strand.last_pursued_time, - }, + let next_strand = Strand { + ex_clause: strand.ex_clause.clone(), + selected_subgoal: Some(next_subgoal), + last_pursued_time: strand.last_pursued_time, }; let table = self.stack.top().table; - let canonical_next_strand = Forest::canonicalize_strand(self.context, next_strand); + let canonical_next_strand = + Forest::canonicalize_strand_from(self.context, infer, &next_strand); self.forest.tables[table].enqueue_strand(canonical_next_strand); } } // Deselect and remove the selected subgoal, now that we have an answer for it. - let selected_subgoal = strand.strand.selected_subgoal.take().unwrap(); + let selected_subgoal = strand.selected_subgoal.take().unwrap(); let subgoal = strand - .strand .ex_clause .subgoals .remove(selected_subgoal.subgoal_index); @@ -660,16 +645,16 @@ impl<'forest, I: Interner> SolveState<'forest, I> { self.context.program().interner(), &self.forest.answer(subgoal_table, answer_index).subst, ); - match strand.infer.apply_answer_subst( + match infer.apply_answer_subst( self.context.program().interner(), self.context.unification_database(), - &mut strand.strand.ex_clause, + &mut strand.ex_clause, &subgoal, &table_goal, answer_subst, ) { Ok(()) => { - let ex_clause = &mut strand.strand.ex_clause; + let ex_clause = &mut strand.ex_clause; // If the answer had was ambiguous, we have to // ensure that `ex_clause` is also ambiguous. This is @@ -744,7 +729,7 @@ impl<'forest, I: Interner> SolveState<'forest, I> { // have an unconditional answer for the subgoal, // therefore we have failed to disprove it. debug!(?strand, "Marking Strand as ambiguous because answer to (negative) subgoal was ambiguous"); - strand.strand.ex_clause.ambiguous = true; + strand.ex_clause.ambiguous = true; // Strand is ambigious. return Ok(()); @@ -935,13 +920,12 @@ impl<'forest, I: Interner> SolveState<'forest, I> { let num_universes = self.forest.tables[self.stack.top().table] .table_goal .universes; - let (infer, _, strand) = chalk_solve::infer::InferenceTable::from_canonical( + let (mut infer, _, mut strand) = chalk_solve::infer::InferenceTable::from_canonical( self.context.program().interner(), num_universes, canonical_strand.clone(), ); - let mut strand = InferringStrand { infer, strand }; - match self.merge_answer_into_strand(&mut strand) { + match self.merge_answer_into_strand(&mut infer, &mut strand) { Err(e) => { debug!(?strand, "could not merge into current strand"); drop(strand); @@ -949,11 +933,8 @@ impl<'forest, I: Interner> SolveState<'forest, I> { } Ok(_) => { debug!(?strand, "merged answer into current strand"); - canonical_strand = Forest::canonicalize_strand_from( - &self.context, - &mut strand.infer, - &strand.strand, - ); + canonical_strand = + Forest::canonicalize_strand_from(&self.context, &mut infer, &strand); self.stack.top().active_strand = Some(canonical_strand); return Ok(()); } @@ -1099,7 +1080,7 @@ impl<'forest, I: Interner> SolveState<'forest, I> { let num_universes = self.forest.tables[table].table_goal.universes; let ( - infer, + mut infer, _, AnswerSubst { subst, @@ -1117,26 +1098,27 @@ impl<'forest, I: Interner> SolveState<'forest, I> { .map(Literal::Positive) .collect(); - let strand = InferringStrand { - infer, - strand: InnerStrand { - ex_clause: ExClause { - subst, - ambiguous: answer.ambiguous, - constraints: constraints - .as_slice(self.context.program().interner()) - .to_vec(), - subgoals: delayed_subgoals, - delayed_subgoals: Vec::new(), - answer_time: TimeStamp::default(), - floundered_subgoals: Vec::new(), - }, - selected_subgoal: None, - last_pursued_time: TimeStamp::default(), + let strand = Strand { + ex_clause: ExClause { + subst, + ambiguous: answer.ambiguous, + constraints: constraints + .as_slice(self.context.program().interner()) + .to_vec(), + subgoals: delayed_subgoals, + delayed_subgoals: Vec::new(), + answer_time: TimeStamp::default(), + floundered_subgoals: Vec::new(), }, + selected_subgoal: None, + last_pursued_time: TimeStamp::default(), }; - Some(Forest::canonicalize_strand(self.context, strand)) + Some(Forest::canonicalize_strand_from( + self.context, + &mut infer, + &strand, + )) } fn on_no_strands_left(&mut self) -> Result<(), RootSearchFail> { diff --git a/chalk-engine/src/strand.rs b/chalk-engine/src/strand.rs index abb58201538..d2b3d41100e 100644 --- a/chalk-engine/src/strand.rs +++ b/chalk-engine/src/strand.rs @@ -1,16 +1,14 @@ use crate::table::AnswerIndex; use crate::{ExClause, TableIndex, TimeStamp}; -use std::fmt::{self, Debug}; +use std::fmt::Debug; use chalk_derive::HasInterner; use chalk_ir::fold::{Fold, Folder}; use chalk_ir::interner::Interner; use chalk_ir::{Canonical, DebruijnIndex, Fallible, UniverseMap}; -use chalk_solve::infer::InferenceTable; - #[derive(Clone, Debug, HasInterner)] -pub(crate) struct InnerStrand { +pub(crate) struct Strand { pub(super) ex_clause: ExClause, /// Index into `ex_clause.subgoals`. @@ -19,13 +17,7 @@ pub(crate) struct InnerStrand { pub(crate) last_pursued_time: TimeStamp, } -pub(crate) type CanonicalStrand = Canonical>; - -#[derive(HasInterner)] -pub(crate) struct InferringStrand { - pub(crate) strand: InnerStrand, - pub(crate) infer: InferenceTable, -} +pub(crate) type CanonicalStrand = Canonical>; #[derive(Clone, Debug)] pub(crate) struct SelectedSubgoal { @@ -43,16 +35,8 @@ pub(crate) struct SelectedSubgoal { pub(crate) universe_map: UniverseMap, } -impl Debug for InferringStrand { - fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result { - fmt.debug_struct("InferringStrand") - .field("strand", &self.strand) - .finish() - } -} - -impl Fold for InnerStrand { - type Result = InnerStrand; +impl Fold for Strand { + type Result = Strand; fn fold_with<'i>( self, folder: &mut dyn Folder<'i, I>, @@ -61,7 +45,7 @@ impl Fold for InnerStrand { where I: 'i, { - Ok(InnerStrand { + Ok(Strand { ex_clause: self.ex_clause.fold_with(folder, outer_binder)?, last_pursued_time: self.last_pursued_time, selected_subgoal: self.selected_subgoal.clone(), From 17512fc9cffecd2b34c3219a2e8c2018864b2d3d Mon Sep 17 00:00:00 2001 From: Jack Huey Date: Tue, 1 Dec 2020 19:27:45 -0500 Subject: [PATCH 6/6] Make interned_slice_common macro and make Variances use it --- chalk-engine/src/normalize_deep.rs | 4 +- chalk-integration/src/program.rs | 4 +- chalk-ir/src/lib.rs | 166 ++++++++++++----------------- chalk-solve/src/infer/test.rs | 4 +- chalk-solve/src/infer/unify.rs | 2 +- 5 files changed, 78 insertions(+), 102 deletions(-) diff --git a/chalk-engine/src/normalize_deep.rs b/chalk-engine/src/normalize_deep.rs index 786b7e97620..4690ffceeab 100644 --- a/chalk-engine/src/normalize_deep.rs +++ b/chalk-engine/src/normalize_deep.rs @@ -120,11 +120,11 @@ mod test { struct TestDatabase; impl UnificationDatabase for TestDatabase { fn fn_def_variance(&self, _fn_def_id: FnDefId) -> Variances { - Variances::from(&ChalkIr, [Variance::Invariant; 20].iter().copied()) + Variances::from_iter(&ChalkIr, [Variance::Invariant; 20].iter().copied()) } fn adt_variance(&self, _adt_id: AdtId) -> Variances { - Variances::from(&ChalkIr, [Variance::Invariant; 20].iter().copied()) + Variances::from_iter(&ChalkIr, [Variance::Invariant; 20].iter().copied()) } } diff --git a/chalk-integration/src/program.rs b/chalk-integration/src/program.rs index 398c2a9308f..a77d5d1915e 100644 --- a/chalk-integration/src/program.rs +++ b/chalk-integration/src/program.rs @@ -368,14 +368,14 @@ impl tls::DebugContext for Program { impl UnificationDatabase for Program { fn fn_def_variance(&self, fn_def_id: FnDefId) -> Variances { - Variances::from( + Variances::from_iter( self.interner(), self.fn_def_variances[&fn_def_id].iter().copied(), ) } fn adt_variance(&self, adt_id: AdtId) -> Variances { - Variances::from(self.interner(), self.adt_variances[&adt_id].iter().copied()) + Variances::from_iter(self.interner(), self.adt_variances[&adt_id].iter().copied()) } } diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs index 89f69bed9d6..8fc2df88140 100644 --- a/chalk-ir/src/lib.rs +++ b/chalk-ir/src/lib.rs @@ -2420,70 +2420,6 @@ impl ProgramClause { } } -/// List of variable kinds with universe index. Wraps `InternedCanonicalVarKinds`. -#[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, HasInterner)] -pub struct Variances { - interned: I::InternedVariances, -} - -impl Variances { - /// Creates an empty list of canonical variable kinds. - pub fn empty(interner: &I) -> Self { - Self::from(interner, None::) - } - - /// Get the interned canonical variable kinds. - pub fn interned(&self) -> &I::InternedVariances { - &self.interned - } - - /// Creates a list of canonical variable kinds using an iterator. - pub fn from(interner: &I, variances: impl IntoIterator) -> Self { - Self::from_fallible( - interner, - variances - .into_iter() - .map(|p| -> Result { Ok(p) }), - ) - .unwrap() - } - - /// Tries to create a list of canonical variable kinds using an iterator. - pub fn from_fallible( - interner: &I, - variances: impl IntoIterator>, - ) -> Result { - Ok(Variances { - interned: I::intern_variances(interner, variances.into_iter())?, - }) - } - - /// Creates a list of canonical variable kinds from a single canonical variable kind. - pub fn from1(interner: &I, variance: Variance) -> Self { - Self::from(interner, Some(variance)) - } - - /// Get an iterator over the list of canonical variable kinds. - pub fn iter(&self, interner: &I) -> std::slice::Iter<'_, Variance> { - self.as_slice(interner).iter() - } - - /// Checks whether the list of canonical variable kinds is empty. - pub fn is_empty(&self, interner: &I) -> bool { - self.as_slice(interner).is_empty() - } - - /// Returns the number of canonical variable kinds. - pub fn len(&self, interner: &I) -> usize { - self.as_slice(interner).len() - } - - /// Returns a slice containing the canonical variable kinds. - pub fn as_slice(&self, interner: &I) -> &[Variance] { - interner.variances_data(&self.interned) - } -} - /// Wraps a "canonicalized item". Items are canonicalized as follows: /// /// All unresolved existential variables are "renumbered" according to their @@ -2947,7 +2883,7 @@ impl<'i, I: Interner> Folder<'i, I> for &SubstFolder<'i, I> { } } -macro_rules! interned_slice { +macro_rules! interned_slice_common { ($seq:ident, $data:ident => $elem:ty, $intern:ident => $interned:ident) => { /// List of interned elements. #[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, HasInterner)] @@ -2960,7 +2896,43 @@ macro_rules! interned_slice { pub fn interned(&self) -> &I::$interned { &self.interned } + + /// Returns a slice containing the elements. + pub fn as_slice(&self, interner: &I) -> &[$elem] { + Interner::$data(interner, &self.interned) + } + + /// Index into the sequence. + pub fn at(&self, interner: &I, index: usize) -> &$elem { + &self.as_slice(interner)[index] + } + + /// Create an empty sequence. + pub fn empty(interner: &I) -> Self { + Self::from_iter(interner, None::<$elem>) + } + + /// Check whether this is an empty sequence. + pub fn is_empty(&self, interner: &I) -> bool { + self.as_slice(interner).is_empty() + } + + /// Get an iterator over the elements of the sequence. + pub fn iter(&self, interner: &I) -> std::slice::Iter<'_, $elem> { + self.as_slice(interner).iter() + } + + /// Get the length of the sequence. + pub fn len(&self, interner: &I) -> usize { + self.as_slice(interner).len() + } } + }; +} + +macro_rules! interned_slice { + ($seq:ident, $data:ident => $elem:ty, $intern:ident => $interned:ident) => { + interned_slice_common!($seq, $data => $elem, $intern => $interned); impl $seq { /// Tries to create a sequence using an iterator of element-like things. @@ -2973,11 +2945,6 @@ macro_rules! interned_slice { }) } - /// Returns a slice containing the elements. - pub fn as_slice(&self, interner: &I) -> &[$elem] { - Interner::$data(interner, &self.interned) - } - /// Create a sequence from elements pub fn from_iter( interner: &I, @@ -2992,35 +2959,10 @@ macro_rules! interned_slice { .unwrap() } - /// Index into the sequence. - pub fn at(&self, interner: &I, index: usize) -> &$elem { - &self.as_slice(interner)[index] - } - /// Create a sequence from a single element. pub fn from1(interner: &I, element: impl CastTo<$elem>) -> Self { Self::from_iter(interner, Some(element)) } - - /// Create an empty sequence. - pub fn empty(interner: &I) -> Self { - Self::from_iter(interner, None::<$elem>) - } - - /// Check whether this is an empty sequence. - pub fn is_empty(&self, interner: &I) -> bool { - self.as_slice(interner).is_empty() - } - - /// Get an iterator over the elements of the sequence. - pub fn iter(&self, interner: &I) -> std::slice::Iter<'_, $elem> { - self.as_slice(interner).iter() - } - - /// Get the length of the sequence. - pub fn len(&self, interner: &I) -> usize { - self.as_slice(interner).len() - } } }; } @@ -3063,6 +3005,40 @@ interned_slice!( intern_substitution => InternedSubstitution ); +interned_slice_common!( + Variances, + variances_data => Variance, + intern_variance => InternedVariances +); + +impl Variances { + /// Tries to create a list of canonical variable kinds using an iterator. + pub fn from_fallible( + interner: &I, + variances: impl IntoIterator>, + ) -> Result { + Ok(Variances { + interned: I::intern_variances(interner, variances.into_iter())?, + }) + } + + /// Creates a list of canonical variable kinds using an iterator. + pub fn from_iter(interner: &I, variances: impl IntoIterator) -> Self { + Self::from_fallible( + interner, + variances + .into_iter() + .map(|p| -> Result { Ok(p) }), + ) + .unwrap() + } + + /// Creates a list of canonical variable kinds from a single canonical variable kind. + pub fn from1(interner: &I, variance: Variance) -> Self { + Self::from_iter(interner, Some(variance)) + } +} + /// Combines a substitution (`subst`) with a set of region constraints /// (`constraints`). This represents the result of a query; the /// substitution stores the values for the query's unknown variables, diff --git a/chalk-solve/src/infer/test.rs b/chalk-solve/src/infer/test.rs index c3a697248d4..ddf09037b94 100644 --- a/chalk-solve/src/infer/test.rs +++ b/chalk-solve/src/infer/test.rs @@ -11,11 +11,11 @@ use chalk_integration::{arg, lifetime, ty}; struct TestDatabase; impl UnificationDatabase for TestDatabase { fn fn_def_variance(&self, _fn_def_id: FnDefId) -> Variances { - Variances::from(&ChalkIr, [Variance::Invariant; 20].iter().copied()) + Variances::from_iter(&ChalkIr, [Variance::Invariant; 20].iter().copied()) } fn adt_variance(&self, _adt_id: AdtId) -> Variances { - Variances::from(&ChalkIr, [Variance::Invariant; 20].iter().copied()) + Variances::from_iter(&ChalkIr, [Variance::Invariant; 20].iter().copied()) } } diff --git a/chalk-solve/src/infer/unify.rs b/chalk-solve/src/infer/unify.rs index dda68f45575..22df33c07ff 100644 --- a/chalk-solve/src/infer/unify.rs +++ b/chalk-solve/src/infer/unify.rs @@ -223,7 +223,7 @@ impl<'t, I: Interner> Unifier<'t, I> { } self.zip_substs( variance, - Some(Variances::from( + Some(Variances::from_iter( &self.interner, std::iter::repeat(Variance::Covariant).take(*arity_a), )),