One big happy family

chalk-engine/src/context.rs

@@ -1,14 +1,30 @@
 use crate::fallible::Fallible;
 use crate::hh::HhGoal;
-use crate::{ExClause, SimplifiedAnswer};
+use crate::{DelayedLiteral, ExClause, SimplifiedAnswer};
 use std::fmt::Debug;
 use std::hash::Hash;
 
 crate mod prelude;
 
-/// The "context" in which the SLG solver operates.
-// FIXME(leodasvacas): Clone and Debug bounds are just for easy derive,
-//                     they are not actually necessary.
+/// The "context" in which the SLG solver operates. It defines all the
+/// types that the SLG solver may need to refer to, as well as a few
+/// very simple interconversion methods.
+///
+/// At any given time, the SLG solver may have more than one context
+/// active. First, there is always the *global* context, but when we
+/// are in the midst of pursuing some particular strand, we will
+/// instantiate a second context just for that work, via the
+/// `instantiate_ucanonical_goal` and `instantiate_ex_clause` methods.
+///
+/// In the chalk implementation, these two contexts are mapped to the
+/// same type. But in the rustc implementation, this second context
+/// corresponds to a fresh arena, and data allocated in that second
+/// context will be freed once the work is done. (The "canonicalizing"
+/// steps offer a way to convert data from the inference context back
+/// into the global context.)
+///
+/// FIXME: Clone and Debug bounds are just for easy derive, they are
+/// not actually necessary. But dang are they convenient.
 pub trait Context: Clone + Debug {
     type CanonicalExClause: Debug;
 
@@ -17,12 +33,6 @@ pub trait Context: Clone + Debug {
     /// the universes from the original.
     type UniverseMap: Clone + Debug;
 
-    /// Part of an answer: represents a canonicalized substitution,
-    /// combined with region constraints. See [the rustc-guide] for more information.
-    ///
-    /// [the rustc-guide]: https://rust-lang-nursery.github.io/rustc-guide/traits-canonicalization.html#canonicalizing-the-query-result
-    type CanonicalConstrainedSubst: Clone + Debug + Eq + Hash;
-
     /// Extracted from a canonicalized substitution or canonicalized ex clause, this is the type of
     /// substitution that is fully normalized with respect to inference variables.
     type InferenceNormalizedSubst: Debug;
@@ -43,9 +53,13 @@ pub trait Context: Clone + Debug {
     /// completely opaque to the SLG solver; it is produced by
     /// `make_solution`.
     type Solution;
-}
 
-pub trait ExClauseContext<C: Context>: Sized + Debug {
+    /// Part of an answer: represents a canonicalized substitution,
+    /// combined with region constraints. See [the rustc-guide] for more information.
+    ///
+    /// [the rustc-guide]: https://rust-lang-nursery.github.io/rustc-guide/traits-canonicalization.html#canonicalizing-the-query-result
+    type CanonicalConstrainedSubst: Clone + Debug + Eq + Hash;
+
     /// Represents a substitution from the "canonical variables" found
     /// in a canonical goal to specific values.
     type Substitution: Debug;
@@ -56,12 +70,7 @@ pub trait ExClauseContext<C: Context>: Sized + Debug {
 
     /// Represents a goal along with an environment.
     type GoalInEnvironment: Debug + Clone + Eq + Hash;
-}
 
-/// The set of types belonging to an "inference context"; in rustc,
-/// these types are tied to the lifetime of the arena within which an
-/// inference context operates.
-pub trait InferenceContext<C: Context>: ExClauseContext<C> {
     /// Represents a set of hypotheses that are assumed to be true.
     type Environment: Debug + Clone;
 
@@ -91,10 +100,15 @@ pub trait InferenceContext<C: Context>: ExClauseContext<C> {
     /// goal we are trying to solve to produce an ex-clause.
     type ProgramClause: Debug;
 
+    /// A vector of program clauses.
+    type ProgramClauses: Debug;
+
     /// The successful result from unification: contains new subgoals
     /// and things that can be attached to an ex-clause.
     type UnificationResult;
 
+    /// Given an environment and a goal, glue them together to create
+    /// a `GoalInEnvironment`.
     fn goal_in_environment(
         environment: &Self::Environment,
         goal: Self::Goal,
@@ -105,26 +119,6 @@ pub trait InferenceContext<C: Context>: ExClauseContext<C> {
 
     /// Create a "cannot prove" goal (see `HhGoal::CannotProve`).
     fn cannot_prove() -> Self::Goal;
-
-    /// Convert the context's goal type into the `HhGoal` type that
-    /// the SLG solver understands. The expectation is that the
-    /// context's goal type has the same set of variants, but with
-    /// different names and a different setup. If you inspect
-    /// `HhGoal`, you will see that this is a "shallow" or "lazy"
-    /// conversion -- that is, we convert the outermost goal into an
-    /// `HhGoal`, but the goals contained within are left as context
-    /// goals.
-    fn into_hh_goal(goal: Self::Goal) -> HhGoal<C, Self>;
-
-    /// Add the residual subgoals as new subgoals of the ex-clause.
-    /// Also add region constraints.
-    fn into_ex_clause(result: Self::UnificationResult, ex_clause: &mut ExClause<C, Self>);
-
-    // Used by: simplify
-    fn add_clauses(
-        env: &Self::Environment,
-        clauses: impl IntoIterator<Item = Self::ProgramClause>,
-    ) -> Self::Environment;
 }
 
 pub trait ContextOps<C: Context>: Sized + Clone + Debug + AggregateOps<C> {
@@ -201,7 +195,7 @@ pub trait ContextOps<C: Context>: Sized + Clone + Debug + AggregateOps<C> {
 pub trait WithInstantiatedUCanonicalGoal<C: Context> {
     type Output;
 
-    fn with<I: InferenceContext<C>>(
+    fn with<I: Context>(
         self,
         infer: &mut dyn InferenceTable<C, I>,
         subst: I::Substitution,
@@ -219,10 +213,10 @@ pub trait WithInstantiatedUCanonicalGoal<C: Context> {
 pub trait WithInstantiatedExClause<C: Context> {
     type Output;
 
-    fn with<I: InferenceContext<C>>(
+    fn with<I: Context>(
         self,
         infer: &mut dyn InferenceTable<C, I>,
-        ex_clause: ExClause<C, I>,
+        ex_clause: ExClause<I>,
     ) -> Self::Output;
 }
 
@@ -237,13 +231,29 @@ pub trait AggregateOps<C: Context> {
 
 /// An "inference table" contains the state to support unification and
 /// other operations on terms.
-pub trait InferenceTable<C: Context, I: InferenceContext<C>>:
+pub trait InferenceTable<C: Context, I: Context>:
     ResolventOps<C, I> + TruncateOps<C, I> + UnificationOps<C, I>
 {
+    /// Convert the context's goal type into the `HhGoal` type that
+    /// the SLG solver understands. The expectation is that the
+    /// context's goal type has the same set of variants, but with
+    /// different names and a different setup. If you inspect
+    /// `HhGoal`, you will see that this is a "shallow" or "lazy"
+    /// conversion -- that is, we convert the outermost goal into an
+    /// `HhGoal`, but the goals contained within are left as context
+    /// goals.
+    fn into_hh_goal(&mut self, goal: I::Goal) -> HhGoal<I>;
+
+    // Used by: simplify
+    fn add_clauses(
+        &mut self,
+        env: &I::Environment,
+        clauses: I::ProgramClauses,
+    ) -> I::Environment;
 }
 
 /// Methods for unifying and manipulating terms and binders.
-pub trait UnificationOps<C: Context, I: InferenceContext<C>> {
+pub trait UnificationOps<C: Context, I: Context> {
     /// Returns the set of program clauses that might apply to
     /// `goal`. (This set can be over-approximated, naturally.)
     fn program_clauses(
@@ -259,13 +269,13 @@ pub trait UnificationOps<C: Context, I: InferenceContext<C>> {
     fn instantiate_binders_existentially(&mut self, arg: &I::BindersGoal) -> I::Goal;
 
     // Used by: logic (but for debugging only)
-    fn debug_ex_clause(&mut self, value: &'v ExClause<C, I>) -> Box<dyn Debug + 'v>;
+    fn debug_ex_clause(&mut self, value: &'v ExClause<I>) -> Box<dyn Debug + 'v>;
 
     // Used by: logic
     fn canonicalize_goal(&mut self, value: &I::GoalInEnvironment) -> C::CanonicalGoalInEnvironment;
 
     // Used by: logic
-    fn canonicalize_ex_clause(&mut self, value: &ExClause<C, I>) -> C::CanonicalExClause;
+    fn canonicalize_ex_clause(&mut self, value: &ExClause<I>) -> C::CanonicalExClause;
 
     // Used by: logic
     fn canonicalize_constrained_subst(
@@ -280,6 +290,16 @@ pub trait UnificationOps<C: Context, I: InferenceContext<C>> {
         value: &C::CanonicalGoalInEnvironment,
     ) -> (C::UCanonicalGoalInEnvironment, C::UniverseMap);
 
+    fn sink_answer_subset(
+        &self,
+        value: &C::CanonicalConstrainedSubst,
+    ) -> I::CanonicalConstrainedSubst;
+
+    fn lift_delayed_literal(
+        &self,
+        value: DelayedLiteral<I>,
+    ) -> DelayedLiteral<C>;
+
     // Used by: logic
     fn invert_goal(&mut self, value: &I::GoalInEnvironment) -> Option<I::GoalInEnvironment>;
 
@@ -290,6 +310,10 @@ pub trait UnificationOps<C: Context, I: InferenceContext<C>> {
         a: &I::Parameter,
         b: &I::Parameter,
     ) -> Fallible<I::UnificationResult>;
+
+    /// Add the residual subgoals as new subgoals of the ex-clause.
+    /// Also add region constraints.
+    fn into_ex_clause(&mut self, result: I::UnificationResult, ex_clause: &mut ExClause<I>);
 }
 
 /// "Truncation" (called "abstraction" in the papers referenced below)
@@ -304,7 +328,7 @@ pub trait UnificationOps<C: Context, I: InferenceContext<C>> {
 ///   - Riguzzi and Swift; ACM Transactions on Computational Logic 2013
 /// - Radial Restraint
 ///   - Grosof and Swift; 2013
-pub trait TruncateOps<C: Context, I: InferenceContext<C>> {
+pub trait TruncateOps<C: Context, I: Context> {
     /// If `subgoal` is too large, return a truncated variant (else
     /// return `None`).
     fn truncate_goal(&mut self, subgoal: &I::GoalInEnvironment) -> Option<I::GoalInEnvironment>;
@@ -314,7 +338,7 @@ pub trait TruncateOps<C: Context, I: InferenceContext<C>> {
     fn truncate_answer(&mut self, subst: &I::Substitution) -> Option<I::Substitution>;
 }
 
-pub trait ResolventOps<C: Context, I: InferenceContext<C>> {
+pub trait ResolventOps<C: Context, I: Context> {
     /// Combines the `goal` (instantiated within `infer`) with the
     /// given program clause to yield the start of a new strand (a
     /// canonical ex-clause).
@@ -330,11 +354,11 @@ pub trait ResolventOps<C: Context, I: InferenceContext<C>> {
 
     fn apply_answer_subst(
         &mut self,
-        ex_clause: ExClause<C, I>,
+        ex_clause: ExClause<I>,
         selected_goal: &I::GoalInEnvironment,
         answer_table_goal: &C::CanonicalGoalInEnvironment,
         canonical_answer_subst: &C::CanonicalConstrainedSubst,
-    ) -> Fallible<ExClause<C, I>>;
+    ) -> Fallible<ExClause<I>>;
 }
 
 pub trait AnswerStream<C: Context> {

chalk-engine/src/context/prelude.rs

@@ -6,4 +6,3 @@ crate use super::AggregateOps;
 crate use super::ResolventOps;
 crate use super::TruncateOps;
 crate use super::InferenceTable;
-crate use super::InferenceContext;

chalk-engine/src/derived.rs

@@ -65,8 +65,8 @@ impl<C: Context> Hash for DelayedLiteral<C> {
 
 ///////////////////////////////////////////////////////////////////////////
 
-impl<C: Context, I: ExClauseContext<C>> PartialEq for Literal<C, I> {
-    fn eq(&self, other: &Literal<C, I>) -> bool {
+impl<C: Context> PartialEq for Literal<C> {
+    fn eq(&self, other: &Literal<C>) -> bool {
         match (self, other) {
             (Literal::Positive(goal1), Literal::Positive(goal2))
             | (Literal::Negative(goal1), Literal::Negative(goal2)) => goal1 == goal2,
@@ -76,10 +76,10 @@ impl<C: Context, I: ExClauseContext<C>> PartialEq for Literal<C, I> {
     }
 }
 
-impl<C: Context, I: ExClauseContext<C>> Eq for Literal<C, I> {
+impl<C: Context> Eq for Literal<C> {
 }
 
-impl<C: Context, I: ExClauseContext<C>> Hash for Literal<C, I> {
+impl<C: Context> Hash for Literal<C> {
     fn hash<H: Hasher>(&self, state: &mut H) {
         mem::discriminant(self).hash(state);
         match self {

chalk-engine/src/hh.rs

@@ -1,17 +1,17 @@
-use crate::context::{Context, InferenceContext};
+use crate::context::Context;
 
 #[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
 /// A general goal; this is the full range of questions you can pose to Chalk.
-pub enum HhGoal<C: Context, I: InferenceContext<C>> {
+pub enum HhGoal<C: Context> {
     /// Introduces a binding at depth 0, shifting other bindings up
     /// (deBruijn index).
-    ForAll(I::BindersGoal),
-    Exists(I::BindersGoal),
-    Implies(Vec<I::ProgramClause>, I::Goal),
-    And(I::Goal, I::Goal),
-    Not(I::Goal),
-    Unify(I::Parameter, I::Parameter),
-    DomainGoal(I::DomainGoal),
+    ForAll(C::BindersGoal),
+    Exists(C::BindersGoal),
+    Implies(C::ProgramClauses, C::Goal),
+    And(C::Goal, C::Goal),
+    Not(C::Goal),
+    Unify(C::Parameter, C::Parameter),
+    DomainGoal(C::DomainGoal),
 
     /// Indicates something that cannot be proven to be true or false
     /// definitively. This can occur with overflow but also with

chalk-engine/src/lib.rs

@@ -66,7 +66,7 @@
 extern crate stacker;
 extern crate fxhash;
 
-use crate::context::{Context, ExClauseContext};
+use crate::context::Context;
 use fxhash::FxHashSet;
 use std::cmp::min;
 use std::usize;
@@ -111,20 +111,20 @@ struct DepthFirstNumber {
 
 /// The paper describes these as `A :- D | G`.
 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
-pub struct ExClause<C: Context, E: ExClauseContext<C>> {
+pub struct ExClause<C: Context> {
     /// The substitution which, applied to the goal of our table,
     /// would yield A.
-    pub subst: E::Substitution,
+    pub subst: C::Substitution,
 
     /// Delayed literals: things that we depend on negatively,
     /// but which have not yet been fully evaluated.
     pub delayed_literals: Vec<DelayedLiteral<C>>,
 
     /// Region constraints we have accumulated.
-    pub constraints: Vec<E::RegionConstraint>,
+    pub constraints: Vec<C::RegionConstraint>,
 
     /// Subgoals: literals that must be proven
-    pub subgoals: Vec<Literal<C, E>>,
+    pub subgoals: Vec<Literal<C>>,
 }
 
 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
@@ -194,9 +194,9 @@ pub enum DelayedLiteral<C: Context> {
 
 /// Either `A` or `~A`, where `A` is a `Env |- Goal`.
 #[derive(Clone, Debug)]
-pub enum Literal<C: Context, E: ExClauseContext<C>> { // FIXME: pub b/c fold
-    Positive(E::GoalInEnvironment),
-    Negative(E::GoalInEnvironment),
+pub enum Literal<C: Context> { // FIXME: pub b/c fold
+    Positive(C::GoalInEnvironment),
+    Negative(C::GoalInEnvironment),
 }
 
 /// The `Minimums` structure is used to track the dependencies between