Intern Vec<ProgramClause<I>>

Author: tirr-c

chalk-engine/src/context.rs

@@ -154,9 +154,6 @@ pub trait Context: Clone + Debug {
 
     fn goal_from_goal_in_environment(goal: &Self::GoalInEnvironment) -> &Self::Goal;
 
-    // Used by: simplify
-    fn add_clauses(env: &Self::Environment, clauses: Self::ProgramClauses) -> Self::Environment;
-
     /// Selects the next appropriate subgoal index for evaluation.
     /// Used by: logic
     fn next_subgoal_index(ex_clause: &ExClause<Self>) -> usize;
@@ -180,6 +177,13 @@ pub trait ContextOps<C: Context>: Sized + Clone + Debug + AggregateOps<C> {
         infer: &mut C::InferenceTable,
     ) -> Result<Vec<C::ProgramClause>, Floundered>;
 
+    // Used by: simplify
+    fn add_clauses(
+        &self,
+        env: &C::Environment,
+        clauses: C::ProgramClauses,
+    ) -> C::Environment;
+
     /// Create an inference table for processing a new goal and instantiate that goal
     /// in that context, returning "all the pieces".
     ///

chalk-engine/src/simplify.rs

@@ -41,7 +41,7 @@ impl<C: Context> Forest<C> {
                     pending_goals.push((environment, context.into_hh_goal(subgoal)))
                 }
                 HhGoal::Implies(wc, subgoal) => {
-                    let new_environment = C::add_clauses(&environment, wc);
+                    let new_environment = context.add_clauses(&environment, wc);
                     pending_goals.push((new_environment, context.into_hh_goal(subgoal)));
                 }
                 HhGoal::All(subgoals) => {

chalk-integration/src/lowering.rs

@@ -1303,11 +1303,11 @@ impl<'k> LowerGoal<Env<'k>> for Goal {
                 // `T: Trait<Assoc = U>` to `FromEnv(T: Trait)` and `FromEnv(T: Trait<Assoc = U>)`
                 // in the assumptions of an `if` goal, e.g. `if (T: Trait) { ... }` lowers to
                 // `if (FromEnv(T: Trait)) { ... /* this part is untouched */ ... }`.
-                let where_clauses: LowerResult<Vec<_>> = hyp
+                let where_clauses = hyp
                     .into_iter()
                     .flat_map(|h| h.lower_clause(env).apply_result())
-                    .map(|result| result.map(|h| h.into_from_env_clause(interner)))
-                    .collect();
+                    .map(|result| result.map(|h| h.into_from_env_clause(interner)));
+                let where_clauses = chalk_ir::ProgramClauses::from_fallible(interner, where_clauses);
                 Ok(chalk_ir::GoalData::Implies(where_clauses?, g.lower(env)?).intern(interner))
             }
             Goal::And(g1, g2s) => {

chalk-integration/src/program.rs

@@ -5,8 +5,8 @@ use chalk_ir::interner::ChalkIr;
 use chalk_ir::tls;
 use chalk_ir::{
     debug::SeparatorTraitRef, AliasTy, ApplicationTy, AssocTypeId, Goal, Goals, ImplId, Lifetime,
-    Parameter, ProgramClause, ProgramClauseImplication, StructId, Substitution, TraitId, Ty,
-    TyData, TypeName,
+    Parameter, ProgramClause, ProgramClauseImplication, ProgramClauses, StructId, Substitution,
+    TraitId, Ty, TyData, TypeName,
 };
 use chalk_rust_ir::{
     AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId, ImplDatum, ImplType, StructDatum,
@@ -182,6 +182,15 @@ impl tls::DebugContext for Program {
         write!(fmt, "{:?}", clause.data(interner))
     }
 
+    fn debug_program_clauses(
+        &self,
+        clauses: &ProgramClauses<ChalkIr>,
+        fmt: &mut fmt::Formatter<'_>,
+    ) -> Result<(), fmt::Error> {
+        let interner = self.interner();
+        write!(fmt, "{:?}", clauses.as_slice(interner))
+    }
+
     fn debug_application_ty(
         &self,
         application_ty: &ApplicationTy<ChalkIr>,

chalk-ir/src/debug.rs

@@ -65,6 +65,12 @@ impl<I: Interner> Debug for ProgramClause<I> {
     }
 }
 
+impl<I: Interner> Debug for ProgramClauses<I> {
+    fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
+        I::debug_program_clauses(self, fmt).unwrap_or_else(|| write!(fmt, "{:?}", self.clauses))
+    }
+}
+
 impl<I: Interner> Debug for ApplicationTy<I> {
     fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
         I::debug_application_ty(self, fmt).unwrap_or_else(|| write!(fmt, "ApplicationTy(?)"))

chalk-ir/src/fold/boring_impls.rs

@@ -172,6 +172,26 @@ impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for Goals<I> {
     }
 }
 
+impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for ProgramClauses<I> {
+    type Result = ProgramClauses<TI>;
+    fn fold_with<'i>(
+        &self,
+        folder: &mut dyn Folder<'i, I, TI>,
+        outer_binder: DebruijnIndex,
+    ) -> Fallible<Self::Result>
+    where
+        I: 'i,
+        TI: 'i,
+    {
+        let interner = folder.interner();
+        let target_interner = folder.target_interner();
+        let folded = self
+            .iter(interner)
+            .map(|p| p.fold_with(folder, outer_binder));
+        Ok(ProgramClauses::from_fallible(target_interner, folded)?)
+    }
+}
+
 #[macro_export]
 macro_rules! copy_fold {
     ($t:ty) => {

chalk-ir/src/interner.rs

@@ -11,6 +11,7 @@ use crate::ParameterData;
 use crate::ProgramClause;
 use crate::ProgramClauseData;
 use crate::ProgramClauseImplication;
+use crate::ProgramClauses;
 use crate::SeparatorTraitRef;
 use crate::StructId;
 use crate::Substitution;
@@ -96,6 +97,14 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
     /// converted back to its underlying data via `substitution_data`.
     type InternedSubstitution: Debug + Clone + Eq + Hash;
 
+    /// "Interned" representation of a list of program clauses.  In normal user code,
+    /// `Self::InternedProgramClauses` is not referenced. Instead, we refer to
+    /// `ProgramClauses<Self>`, which wraps this type.
+    ///
+    /// An `InternedProgramClauses` is created by `intern_program_clauses` and can be
+    /// converted back to its underlying data via `program_clauses_data`.
+    type InternedProgramClauses: Debug + Clone + Eq + Hash;
+
     /// "Interned" representation of a "program clause".  In normal user code,
     /// `Self::InternedProgramClause` is not referenced. Instead, we refer to
     /// `ProgramClause<Self>`, which wraps this type.
@@ -259,6 +268,21 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
         None
     }
 
+    /// Prints the debug representation of a ProgramClauses. To get good
+    /// results, this requires inspecting TLS, and is difficult to
+    /// code without reference to a specific interner (and hence
+    /// fully known types).
+    ///
+    /// Returns `None` to fallback to the default debug output (e.g.,
+    /// if no info about current program is available from TLS).
+    #[allow(unused_variables)]
+    fn debug_program_clauses(
+        clauses: &ProgramClauses<Self>,
+        fmt: &mut fmt::Formatter<'_>,
+    ) -> Option<fmt::Result> {
+        None
+    }
+
     /// Prints the debug representation of an ApplicationTy. To get good
     /// results, this requires inspecting TLS, and is difficult to
     /// code without reference to a specific interner (and hence
@@ -374,6 +398,21 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
         &self,
         clause: &'a Self::InternedProgramClause,
     ) -> &'a ProgramClauseData<Self>;
+
+    /// Create an "interned" program clauses from `data`. This is not
+    /// normally invoked directly; instead, you invoke
+    /// `ProgramClauses::from` (which will ultimately call this
+    /// method).
+    fn intern_program_clauses(
+        &self,
+        data: impl IntoIterator<Item = ProgramClause<Self>>,
+    ) -> Self::InternedProgramClauses;
+
+    /// Lookup the `ProgramClauseData` that was interned to create a `ProgramClause`.
+    fn program_clauses_data<'a>(
+        &self,
+        clauses: &'a Self::InternedProgramClauses,
+    ) -> &'a [ProgramClause<Self>];
 }
 
 pub trait TargetInterner<I: Interner>: Interner {
@@ -429,6 +468,7 @@ mod default {
         type InternedGoals = Vec<Goal<ChalkIr>>;
         type InternedSubstitution = Vec<Parameter<ChalkIr>>;
         type InternedProgramClause = ProgramClauseData<ChalkIr>;
+        type InternedProgramClauses = Vec<ProgramClause<ChalkIr>>;
         type DefId = RawId;
         type Identifier = Identifier;
 
@@ -504,6 +544,13 @@ mod default {
             tls::with_current_program(|prog| Some(prog?.debug_program_clause(clause, fmt)))
         }
 
+        fn debug_program_clauses(
+            clause: &ProgramClauses<ChalkIr>,
+            fmt: &mut fmt::Formatter<'_>,
+        ) -> Option<fmt::Result> {
+            tls::with_current_program(|prog| Some(prog?.debug_program_clauses(clause, fmt)))
+        }
+
         fn debug_application_ty(
             application_ty: &ApplicationTy<ChalkIr>,
             fmt: &mut fmt::Formatter<'_>,
@@ -603,6 +650,20 @@ mod default {
         ) -> &'a ProgramClauseData<Self> {
             clause
         }
+
+        fn intern_program_clauses(
+            &self,
+            data: impl IntoIterator<Item = ProgramClause<Self>>,
+        ) -> Vec<ProgramClause<Self>> {
+            data.into_iter().collect()
+        }
+
+        fn program_clauses_data<'a>(
+            &self,
+            clauses: &'a Vec<ProgramClause<Self>>,
+        ) -> &'a [ProgramClause<Self>] {
+            clauses
+        }
     }
 
     impl HasInterner for ChalkIr {

chalk-ir/src/lib.rs

@@ -48,20 +48,20 @@ pub mod tls;
 /// The set of assumptions we've made so far, and the current number of
 /// universal (forall) quantifiers we're within.
 pub struct Environment<I: Interner> {
-    pub clauses: Vec<ProgramClause<I>>,
+    pub clauses: ProgramClauses<I>,
 }
 
 impl<I: Interner> Environment<I> {
-    pub fn new() -> Self {
-        Environment { clauses: vec![] }
+    pub fn new(interner: &I) -> Self {
+        Environment { clauses: ProgramClauses::new(interner) }
     }
 
-    pub fn add_clauses<II>(&self, clauses: II) -> Self
+    pub fn add_clauses<II>(&self, interner: &I, clauses: II) -> Self
     where
         II: IntoIterator<Item = ProgramClause<I>>,
     {
         let mut env = self.clone();
-        env.clauses = env.clauses.into_iter().chain(clauses).collect();
+        env.clauses = ProgramClauses::from(interner, env.clauses.iter(interner).cloned().chain(clauses));
         env
     }
 }
@@ -1265,6 +1265,56 @@ impl<I: Interner> ProgramClause<I> {
     }
 }
 
+#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord, HasInterner)]
+pub struct ProgramClauses<I: Interner> {
+    clauses: I::InternedProgramClauses,
+}
+
+impl<I: Interner> ProgramClauses<I> {
+    pub fn new(interner: &I) -> Self {
+        Self::from(interner, None::<ProgramClause<I>>)
+    }
+
+    pub fn interned(&self) -> &I::InternedProgramClauses {
+        &self.clauses
+    }
+
+    pub fn from(interner: &I, clauses: impl IntoIterator<Item = impl CastTo<ProgramClause<I>>>) -> Self {
+        use crate::cast::Caster;
+        ProgramClauses {
+            clauses: I::intern_program_clauses(interner, clauses.into_iter().casted(interner)),
+        }
+    }
+
+    pub fn from_fallible<E>(
+        interner: &I,
+        clauses: impl IntoIterator<Item = Result<impl CastTo<ProgramClause<I>>, E>>,
+    ) -> Result<Self, E> {
+        use crate::cast::Caster;
+        let clauses = clauses
+            .into_iter()
+            .casted(interner)
+            .collect::<Result<Vec<ProgramClause<I>>, _>>()?;
+        Ok(Self::from(interner, clauses))
+    }
+
+    pub fn iter(&self, interner: &I) -> std::slice::Iter<'_, ProgramClause<I>> {
+        self.as_slice(interner).iter()
+    }
+
+    pub fn is_empty(&self, interner: &I) -> bool {
+        self.as_slice(interner).is_empty()
+    }
+
+    pub fn len(&self, interner: &I) -> usize {
+        self.as_slice(interner).len()
+    }
+
+    pub fn as_slice(&self, interner: &I) -> &[ProgramClause<I>] {
+        interner.program_clauses_data(&self.clauses)
+    }
+}
+
 /// Wraps a "canonicalized item". Items are canonicalized as follows:
 ///
 /// All unresolved existential variables are "renumbered" according to their
@@ -1410,10 +1460,13 @@ impl<I: Interner> Goal<I> {
             QuantifierKind::ForAll,
             Binders::with_fresh_type_var(interner, |ty| {
                 GoalData::Implies(
-                    vec![
-                        DomainGoal::Compatible(()).cast(interner),
-                        DomainGoal::DownstreamType(ty).cast(interner),
-                    ],
+                    ProgramClauses::from(
+                        interner,
+                        vec![
+                            DomainGoal::Compatible(()),
+                            DomainGoal::DownstreamType(ty),
+                        ],
+                    ),
                     self.shifted_in(interner),
                 )
                 .intern(interner)
@@ -1422,7 +1475,7 @@ impl<I: Interner> Goal<I> {
         .intern(interner)
     }
 
-    pub fn implied_by(self, interner: &I, predicates: Vec<ProgramClause<I>>) -> Goal<I> {
+    pub fn implied_by(self, interner: &I, predicates: ProgramClauses<I>) -> Goal<I> {
         GoalData::Implies(predicates, self).intern(interner)
     }
 
@@ -1470,7 +1523,7 @@ pub enum GoalData<I: Interner> {
     /// Introduces a binding at depth 0, shifting other bindings up
     /// (deBruijn index).
     Quantified(QuantifierKind, Binders<Goal<I>>),
-    Implies(Vec<ProgramClause<I>>, Goal<I>),
+    Implies(ProgramClauses<I>, Goal<I>),
     All(Goals<I>),
     Not(Goal<I>),
 

chalk-ir/src/tls.rs

@@ -1,7 +1,8 @@
 use crate::interner::ChalkIr;
 use crate::{
     debug::SeparatorTraitRef, AliasTy, ApplicationTy, AssocTypeId, Goal, Goals, Lifetime,
-    Parameter, ProgramClause, ProgramClauseImplication, StructId, Substitution, TraitId, Ty,
+    Parameter, ProgramClause, ProgramClauseImplication, ProgramClauses, StructId, Substitution,
+    TraitId, Ty,
 };
 use std::cell::RefCell;
 use std::fmt;
@@ -74,6 +75,12 @@ pub trait DebugContext {
         fmt: &mut fmt::Formatter<'_>,
     ) -> Result<(), fmt::Error>;
 
+    fn debug_program_clauses(
+        &self,
+        clauses: &ProgramClauses<ChalkIr>,
+        fmt: &mut fmt::Formatter<'_>,
+    ) -> Result<(), fmt::Error>;
+
     fn debug_application_ty(
         &self,
         application_ty: &ApplicationTy<ChalkIr>,

chalk-ir/src/zip.rs

@@ -250,8 +250,9 @@ impl<I: Interner> Zip<I> for Environment<I> {
     where
         I: 'i,
     {
-        assert_eq!(a.clauses.len(), b.clauses.len()); // or different numbers of clauses
-        Zip::zip_with(zipper, &a.clauses, &b.clauses)?;
+        let interner = zipper.interner();
+        assert_eq!(a.clauses.len(interner), b.clauses.len(interner)); // or different numbers of clauses
+        Zip::zip_with(zipper, a.clauses.as_slice(interner), b.clauses.as_slice(interner))?;
         Ok(())
     }
 }
@@ -267,6 +268,17 @@ impl<I: Interner> Zip<I> for Goals<I> {
     }
 }
 
+impl<I: Interner> Zip<I> for ProgramClauses<I> {
+    fn zip_with<'i, Z: Zipper<'i, I>>(zipper: &mut Z, a: &Self, b: &Self) -> Fallible<()>
+    where
+        I: 'i,
+    {
+        let interner = zipper.interner();
+        Zip::zip_with(zipper, a.as_slice(interner), b.as_slice(interner))?;
+        Ok(())
+    }
+}
+
 /// Generates a Zip impl that requires the two enums be the same
 /// variant, then zips each field of the variant in turn. Only works
 /// if all variants have a single parenthesized value right now.