Finish removing types on Context

Author: jackh726

Cargo.lock

@@ -9,9 +9,8 @@ use crate::hh::HhGoal;
 use crate::{CompleteAnswer, ExClause};
 use chalk_base::results::{Fallible, Floundered};
 use chalk_ir::interner::Interner;
-use chalk_ir::{Canonical, ConstrainedSubst, Constraint, DomainGoal, Environment, GenericArg, Goal, InEnvironment, Substitution, UCanonical};
+use chalk_ir::{AnswerSubst, Binders, Canonical, ConstrainedSubst, Constraint, DomainGoal, Environment, GenericArg, Goal, InEnvironment, ProgramClause, ProgramClauses, Substitution, UCanonical, UniverseMap};
 use std::fmt::Debug;
-use std::hash::Hash;
 
 /// 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
@@ -33,57 +32,19 @@ use std::hash::Hash;
 /// FIXME: Clone and Debug bounds are just for easy derive, they are
 /// not actually necessary. But dang are they convenient.
 pub trait Context<I: Interner>: Clone + Debug {
-    /// A map between universes. These are produced when
-    /// u-canonicalizing something; they map canonical results back to
-    /// the universes from the original.
-    type UniverseMap: Clone + Debug;
-
-    /// 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;
-
-    /// A u-canonicalized `GoalInEnvironment` -- this is one where the
-    /// free universes are renumbered to consecutive integers starting
-    /// from U1 (but preserving their relative order).
-    type UCanonicalGoalInEnvironment: Debug + Clone + Eq + Hash;
-
     /// A final solution that is passed back to the user. This is
     /// completely opaque to the SLG solver; it is produced by
     /// `make_solution`.
     type Solution;
 
-    /// Part of an answer: the canonical version of a substitution,
-    /// region constraints, and delayed literals.
-    type CanonicalAnswerSubst: Clone + Debug + Eq + Hash;
-
     /// Represents an inference table.
     type InferenceTable: InferenceTable<I, Self> + Clone;
 
-    /// A "higher-order" goal, quantified over some types and/or
-    /// lifetimes. When you have a quantification, like `forall<T> { G
-    /// }` or `exists<T> { G }`, this represents the `<T> { G }` part.
-    ///
-    /// (In Lambda Prolog, this would be a "lambda predicate", like `T
-    /// \ Goal`).
-    type BindersGoal: Debug;
-
-    /// A rule like `DomainGoal :- Goal`.
-    ///
-    /// `resolvent_clause` combines a program-clause and a concrete
-    /// goal we are trying to solve to produce an ex-clause.
-    type ProgramClause: Debug;
-
-    /// A vector of program clauses.
-    type ProgramClauses: Debug;
-
     /// How to relate two kinds when unifying: for example in rustc, we
     /// may want to unify parameters either for the sub-typing relation or for
     /// the equality relation.
     type Variance;
 
-    /// The type used to store concrete representations of "core types" from chalk-ir.
-    type Interner;
-
     /// Given an environment and a goal, glue them together to create
     /// a `GoalInEnvironment`.
     fn goal_in_environment(
@@ -94,24 +55,24 @@ pub trait Context<I: Interner>: Clone + Debug {
     /// Extracts the inner normalized substitution from a canonical ex-clause.
     fn inference_normalized_subst_from_ex_clause(
         canon_ex_clause: &Canonical<ExClause<I>>,
-    ) -> &Self::InferenceNormalizedSubst;
+    ) -> &Substitution<I>;
 
     /// Extracts the inner normalized substitution from a canonical constraint subst.
     fn inference_normalized_subst_from_subst(
-        canon_ex_clause: &Self::CanonicalAnswerSubst,
-    ) -> &Self::InferenceNormalizedSubst;
+        canon_ex_clause: &Canonical<AnswerSubst<I>>,
+    ) -> &Substitution<I>;
 
     /// True if this solution has no region constraints.
-    fn empty_constraints(ccs: &Self::CanonicalAnswerSubst) -> bool;
+    fn empty_constraints(ccs: &Canonical<AnswerSubst<I>>) -> bool;
 
     fn canonical(u_canon: &UCanonical<InEnvironment<Goal<I>>>) -> &Canonical<InEnvironment<Goal<I>>>;
 
-    fn has_delayed_subgoals(canonical_subst: &Self::CanonicalAnswerSubst) -> bool;
+    fn has_delayed_subgoals(canonical_subst: &Canonical<AnswerSubst<I>>) -> bool;
 
     fn num_universes(_: &UCanonical<InEnvironment<Goal<I>>>) -> usize;
 
     fn canonical_constrained_subst_from_canonical_constrained_answer(
-        canonical_subst: &Self::CanonicalAnswerSubst,
+        canonical_subst: &Canonical<AnswerSubst<I>>,
     ) -> Canonical<ConstrainedSubst<I>>;
 
     fn goal_from_goal_in_environment(goal: &InEnvironment<Goal<I>>) -> &Goal<I>;
@@ -137,10 +98,10 @@ pub trait ContextOps<I: Interner, C: Context<I>>: Sized + Clone + Debug + Aggreg
         environment: &Environment<I>,
         goal: &DomainGoal<I>,
         infer: &mut C::InferenceTable,
-    ) -> Result<Vec<C::ProgramClause>, Floundered>;
+    ) -> Result<Vec<ProgramClause<I>>, Floundered>;
 
     // Used by: simplify
-    fn add_clauses(&self, env: &Environment<I>, clauses: C::ProgramClauses) -> Environment<I>;
+    fn add_clauses(&self, env: &Environment<I>, clauses: ProgramClauses<I>) -> Environment<I>;
 
     /// Create an inference table for processing a new goal and instantiate that goal
     /// in that context, returning "all the pieces".
@@ -169,7 +130,7 @@ pub trait ContextOps<I: Interner, C: Context<I>>: Sized + Clone + Debug + Aggreg
     fn instantiate_answer_subst(
         &self,
         num_universes: usize,
-        answer: &C::CanonicalAnswerSubst,
+        answer: &Canonical<AnswerSubst<I>>,
     ) -> (
         C::InferenceTable,
         Substitution<I>,
@@ -194,7 +155,7 @@ pub trait ContextOps<I: Interner, C: Context<I>>: Sized + Clone + Debug + Aggreg
     /// but for the universes of universally quantified names.
     fn map_goal_from_canonical(
         &self,
-        _: &C::UniverseMap,
+        _: &UniverseMap,
         value: &Canonical<InEnvironment<Goal<I>>>,
     ) -> Canonical<InEnvironment<Goal<I>>>;
 
@@ -204,19 +165,19 @@ pub trait ContextOps<I: Interner, C: Context<I>>: Sized + Clone + Debug + Aggreg
     /// names.
     fn map_subst_from_canonical(
         &self,
-        _: &C::UniverseMap,
-        value: &C::CanonicalAnswerSubst,
-    ) -> C::CanonicalAnswerSubst;
+        _: &UniverseMap,
+        value: &Canonical<AnswerSubst<I>>,
+    ) -> Canonical<AnswerSubst<I>>;
 
-    fn interner(&self) -> &C::Interner;
+    fn interner(&self) -> &I;
 
     /// Upcast this domain goal into a more general goal.
     fn into_goal(&self, domain_goal: DomainGoal<I>) -> Goal<I>;
 
     fn is_trivial_substitution(
         &self,
         u_canon: &UCanonical<InEnvironment<Goal<I>>>,
-        canonical_subst: &C::CanonicalAnswerSubst,
+        canonical_subst: &Canonical<AnswerSubst<I>>,
     ) -> bool;
 
     /// Convert the context's goal type into the `HhGoal` type that
@@ -249,59 +210,59 @@ pub trait UnificationOps<I: Interner, C: Context<I>> {
     // Used by: simplify
     fn instantiate_binders_universally(
         &mut self,
-        interner: &C::Interner,
-        arg: &C::BindersGoal,
+        interner: &I,
+        arg: &Binders<Goal<I>>,
     ) -> Goal<I>;
 
     // Used by: simplify
     fn instantiate_binders_existentially(
         &mut self,
-        interner: &C::Interner,
-        arg: &C::BindersGoal,
+        interner: &I,
+        arg: &Binders<Goal<I>>,
     ) -> Goal<I>;
 
     // Used by: logic (but for debugging only)
     fn debug_ex_clause<'v>(
         &mut self,
-        interner: &C::Interner,
+        interner: &I,
         value: &'v ExClause<I>,
     ) -> Box<dyn Debug + 'v>;
 
     // Used by: logic
     fn fully_canonicalize_goal(
         &mut self,
-        interner: &C::Interner,
+        interner: &I,
         value: &InEnvironment<Goal<I>>,
-    ) -> (UCanonical<InEnvironment<Goal<I>>>, C::UniverseMap);
+    ) -> (UCanonical<InEnvironment<Goal<I>>>, UniverseMap);
 
     // Used by: logic
     fn canonicalize_ex_clause(
         &mut self,
-        interner: &C::Interner,
+        interner: &I,
         value: &ExClause<I>,
     ) -> Canonical<ExClause<I>>;
 
     // Used by: logic
     fn canonicalize_constrained_subst(
         &mut self,
-        interner: &C::Interner,
+        interner: &I,
         subst: Substitution<I>,
         constraints: Vec<InEnvironment<Constraint<I>>>,
     ) -> Canonical<ConstrainedSubst<I>>;
 
     // Used by: logic
     fn canonicalize_answer_subst(
         &mut self,
-        interner: &C::Interner,
+        interner: &I,
         subst: Substitution<I>,
         constraints: Vec<InEnvironment<Constraint<I>>>,
         delayed_subgoals: Vec<InEnvironment<Goal<I>>>,
-    ) -> C::CanonicalAnswerSubst;
+    ) -> Canonical<AnswerSubst<I>>;
 
     // Used by: logic
     fn invert_goal(
         &mut self,
-        interner: &C::Interner,
+        interner: &I,
         value: &InEnvironment<Goal<I>>,
     ) -> Option<InEnvironment<Goal<I>>>;
 
@@ -313,7 +274,7 @@ pub trait UnificationOps<I: Interner, C: Context<I>> {
     // Used by: simplify
     fn unify_generic_args_into_ex_clause(
         &mut self,
-        interner: &C::Interner,
+        interner: &I,
         environment: &Environment<I>,
         variance: C::Variance,
         a: &GenericArg<I>,
@@ -338,12 +299,12 @@ pub trait TruncateOps<I: Interner, C: Context<I>> {
     /// Check if `subgoal` is too large
     fn goal_needs_truncation(
         &mut self,
-        interner: &C::Interner,
+        interner: &I,
         subgoal: &InEnvironment<Goal<I>>,
     ) -> bool;
 
     /// Check if `subst` is too large
-    fn answer_needs_truncation(&mut self, interner: &C::Interner, subst: &Substitution<I>) -> bool;
+    fn answer_needs_truncation(&mut self, interner: &I, subst: &Substitution<I>) -> bool;
 }
 
 pub trait ResolventOps<I: Interner, C: Context<I>> {
@@ -354,20 +315,20 @@ pub trait ResolventOps<I: Interner, C: Context<I>> {
     /// The bindings in `infer` are unaffected by this operation.
     fn resolvent_clause(
         &mut self,
-        interner: &C::Interner,
+        interner: &I,
         environment: &Environment<I>,
         goal: &DomainGoal<I>,
         subst: &Substitution<I>,
-        clause: &C::ProgramClause,
+        clause: &ProgramClause<I>,
     ) -> Fallible<ExClause<I>>;
 
     fn apply_answer_subst(
         &mut self,
-        interner: &C::Interner,
+        interner: &I,
         ex_clause: &mut ExClause<I>,
         selected_goal: &InEnvironment<Goal<I>>,
         answer_table_goal: &Canonical<InEnvironment<Goal<I>>>,
-        canonical_answer_subst: &C::CanonicalAnswerSubst,
+        canonical_answer_subst: &Canonical<AnswerSubst<I>>,
     ) -> Fallible<()>;
 }
 
@@ -438,5 +399,5 @@ pub trait AnswerStream<I: Interner, C: Context<I>> {
 
     /// Invokes `test` with each possible future answer, returning true immediately
     /// if we find any answer for which `test` returns true.
-    fn any_future_answer(&self, test: impl Fn(&C::InferenceNormalizedSubst) -> bool) -> bool;
+    fn any_future_answer(&self, test: impl Fn(&Substitution<I>) -> bool) -> bool;
 }

chalk-engine/src/context.rs

@@ -6,11 +6,11 @@ use crate::{TableIndex, TimeStamp};
 use std::fmt::Display;
 
 use chalk_ir::interner::Interner;
-use chalk_ir::{Canonical, ConstrainedSubst, Goal, InEnvironment, UCanonical};
+use chalk_ir::{Canonical, ConstrainedSubst, Goal, InEnvironment, Substitution, UCanonical};
 
 pub struct Forest<I: Interner, C: Context<I>> {
     context: C,
-    pub(crate) tables: Tables<I, C>,
+    pub(crate) tables: Tables<I>,
 
     /// This is a clock which always increases. It is
     /// incremented every time a new subgoal is followed.
@@ -199,7 +199,7 @@ impl<'me, I: Interner, C: Context<I>, CO: ContextOps<I, C>> AnswerStream<I, C> f
         answer
     }
 
-    fn any_future_answer(&self, test: impl Fn(&C::InferenceNormalizedSubst) -> bool) -> bool {
+    fn any_future_answer(&self, test: impl Fn(&Substitution<I>) -> bool) -> bool {
         self.forest.any_future_answer(self.table, self.answer, test)
     }
 }

chalk-engine/src/forest.rs

@@ -1,16 +1,16 @@
 use crate::context::Context;
 
 use chalk_ir::interner::Interner;
-use chalk_ir::{DomainGoal, GenericArg, Goal};
+use chalk_ir::{Binders, DomainGoal, GenericArg, Goal, ProgramClauses};
 
 #[derive(Clone, PartialEq, Eq, Hash)]
 /// A general goal; this is the full range of questions you can pose to Chalk.
 pub enum HhGoal<I: Interner, C: Context<I>> {
     /// Introduces a binding at depth 0, shifting other bindings up
     /// (deBruijn index).
-    ForAll(C::BindersGoal),
-    Exists(C::BindersGoal),
-    Implies(C::ProgramClauses, Goal<I>),
+    ForAll(Binders<Goal<I>>),
+    Exists(Binders<Goal<I>>),
+    Implies(ProgramClauses<I>, Goal<I>),
     All(Vec<Goal<I>>),
     Not(Goal<I>),
     Unify(C::Variance, GenericArg<I>, GenericArg<I>),

chalk-engine/src/hh.rs

@@ -56,12 +56,11 @@
 #[macro_use]
 extern crate chalk_base;
 
-use crate::context::Context;
 use std::cmp::min;
 use std::usize;
 
 use chalk_ir::interner::Interner;
-use chalk_ir::{Canonical, Constraint, ConstrainedSubst, Goal, InEnvironment, Substitution};
+use chalk_ir::{AnswerSubst, Canonical, Constraint, ConstrainedSubst, Goal, InEnvironment, Substitution};
 
 mod boring_impls;
 pub mod context;
@@ -190,12 +189,12 @@ pub struct FlounderedSubgoal<I: Interner> {
 /// goal for a particular table (modulo delayed literals). It contains
 /// a substitution
 #[derive(Clone, Debug)]
-pub struct Answer<I: Interner, C: Context<I>> {
+pub struct Answer<I: Interner> {
     /// Contains values for the unbound inference variables for which
     /// the table is true, along with any delayed subgoals (Which must
     /// still be proven) and region constrained (which must still be
     /// proven, but not by chalk).
-    pub subst: C::CanonicalAnswerSubst,
+    pub subst: Canonical<AnswerSubst<I>>,
 
     /// If this flag is set, then the answer could be neither proven
     /// nor disproven. This could be the size of the answer exceeded