Goals and folding goals

book/src/SUMMARY.md

@@ -10,6 +10,8 @@
     - [Rust types](./types/rust_types.md)
         - [Application types](./types/rust_types/application_ty.md)
     - [Rust lifetimes](./types/rust_lifetimes.md)
+    - [Operations](./types/operations.md)
+        - [Fold and the Folder trait](./types/operations/fold.md)
 - [Representing traits, impls, and other parts of Rust programs](./rust_ir.md)
 - [Lowering Rust IR to logic](./clauses.md)
     - [Unification and type equality](./clauses/type_equality.md)

book/src/types/operations.md

@@ -0,0 +1,4 @@
+# Operations
+
+This chapter describes various patterns and utilities for manipulating
+Rust types.

book/src/types/operations/fold.md

@@ -0,0 +1,95 @@
+# Fold and the Folder trait
+
+The [`Fold`] trait permits one to traverse a type or other term in the
+chalk-ir and make a copy of it, possibly making small substitutions or
+alterations along the way. Folding also allows copying a term from one
+type family to another.
+
+[`Fold`]: http://rust-lang.github.io/chalk/chalk_ir/fold/trait.Fold.html
+
+To use the [`Fold`] trait, one invokes the [`Fold::fold_with`] method, supplying some
+"folder" as well as the number of "in scope binders" for that term (typically `0`
+to start):
+
+```rust,ignore
+let output_ty = input_ty.fold_with(&mut folder, 0);
+```
+
+[`Fold::fold_with`]: http://rust-lang.github.io/chalk/chalk_ir/fold/trait.Fold.html#tymethod.fold_with
+
+The folder is some instance of the [`Folder`] trait. This trait
+defines a few key callbacks that allow you to substitute different
+values as the fold proceeds. For example, when a type is folded, the
+folder can substitute a new type in its place.
+
+[`Folder`]: http://rust-lang.github.io/chalk/chalk_ir/fold/trait.Folder.html
+
+## Uses for folders
+
+A common use for `Fold` is to permit a substitution -- that is,
+replacing generic type parameters with their values.
+
+## From Fold to Folder to SuperFold and back again
+
+The overall flow of folding is like this.
+
+1. [`Fold::fold_with`] is invoked on the outermost term. It recursively
+   walks the term.
+2. For those sorts of terms (types, lifetimes, goals, program clauses) that have
+   callbacks in the [`Folder`] trait, invoking [`Fold::fold_with`] will in turn
+   invoke the corresponding method on the [`Folder`] trait, such as `Folder::fold_ty`.
+3. The default implementation of `Folder::fold_ty`, in turn, invokes
+   `SuperFold::super_fold_with`.  This will recursively fold the
+   contents of the type. In some cases, the `super_fold_with`
+   implementation invokes more specialized methods on [`Folder`], such
+   as [`Folder::fold_free_var_ty`], which makes it easier to write
+   folders that just intercept *certain* types.
+
+Thus, as a user, you can customize folding by:
+
+* Defining your own `Folder` type
+* Implementing the appropriate methods to "intercept" types/lifetimes/etc at the right level of
+  detail
+* In those methods, if you find a case where you would prefer not to
+  substitute a new value, then invoke `SuperFold::super_fold_with` to
+  return to the default behavior.
+
+## The `binders` argument
+
+Each callback in the [`Folder`] trait takes a `binders` argument. This indicates
+the number of binders that we have traversed during folding, which is relevant for debruijn indices.
+So e.g. a bound variable with depth 1, if invoked with a `binders` value of 1, indicates something that was bound to something external to the fold.
+
+XXX explain with examples and in more detail
+
+## The `Fold::Result` associated type
+
+The `Fold` trait defines a [`Result`] associated type, indicating the
+type that will result from folding.
+
+[`Result`]: http://rust-lang.github.io/chalk/chalk_ir/fold/trait.Fold.html#associatedtype.Result
+
+## When to implement the Fold and SuperFold traits
+
+Any piece of IR that represents a kind of "term" (e.g., a type, part
+of a type, or a goal, etc) in the logic should implement `Fold`. We
+also implement `Fold` for common collection types like `Vec` as well
+as tuples, references, etc.
+
+The `SuperFold` trait should only be implemented for those types that
+have a callback defined on the `Folder` trait (e.g., types and
+lifetimes).
+
+## Derives
+
+Using the `chalk-derive` crate, you can auto-derive the `Fold` trait.
+There isn't presently a derive for `SuperFold` since it is very rare
+to require it. The derive for `Fold` is a bit cludgy and requires:
+
+* You must import `Fold` into scope.
+* The type you are deriving `Fold` on must have either:
+  * A type parameter that has a `TypeFamily` bound, like `TF: TypeFamily`
+  * A type parameter that has a `HasTypeFamily` bound, like `TF: HasTypeFamily`
+  * The `has_type_family(XXX)` attribute.
+
+

chalk-integration/src/lowering.rs

@@ -1134,16 +1134,12 @@ impl LowerClause for Clause {
         let implications = env.in_binders(self.all_parameters(), |env| {
             let consequences: Vec<chalk_ir::DomainGoal<ChalkIr>> = self.consequence.lower(env)?;
 
-            let conditions: Vec<chalk_ir::Goal<ChalkIr>> = self
-                .conditions
-                .iter()
-                .map(|g| g.lower(env))
-                .rev() // (*)
-                .collect::<LowerResult<_>>()?;
-
-            // (*) Subtle: in the SLG solver, we pop conditions from R to
-            // L. To preserve the expected order (L to R), we must
-            // therefore reverse.
+            let conditions = chalk_ir::Goals::from_fallible(
+                // Subtle: in the SLG solver, we pop conditions from R to
+                // L. To preserve the expected order (L to R), we must
+                // therefore reverse.
+                self.conditions.iter().map(|g| g.lower(env)).rev(),
+            )?;
 
             let implications = consequences
                 .into_iter()
@@ -1270,11 +1266,9 @@ impl<'k> LowerGoal<Env<'k>> for Goal {
                 Ok(chalk_ir::GoalData::Implies(where_clauses?, g.lower(env)?).intern())
             }
             Goal::And(g1, g2s) => {
-                let mut goals = vec![];
-                goals.push(g1.lower(env)?);
-                for g2 in g2s {
-                    goals.push(g2.lower(env)?);
-                }
+                let goals = chalk_ir::Goals::from_fallible(
+                    Some(g1).into_iter().chain(g2s).map(|g| g.lower(env)),
+                )?;
                 Ok(chalk_ir::GoalData::All(goals).intern())
             }
             Goal::Not(g) => Ok(chalk_ir::GoalData::Not(g.lower(env)?).intern()),

chalk-ir/src/cast.rs

@@ -183,7 +183,7 @@ where
     fn cast_to(self) -> ProgramClause<TF> {
         ProgramClause::Implies(ProgramClauseImplication {
             consequence: self.cast(),
-            conditions: vec![],
+            conditions: Goals::new(),
         })
     }
 }
@@ -199,7 +199,7 @@ where
         } else {
             ProgramClause::ForAll(self.map(|bound| ProgramClauseImplication {
                 consequence: bound.cast(),
-                conditions: vec![],
+                conditions: Goals::new(),
             }))
         }
     }

chalk-ir/src/debug.rs

@@ -279,17 +279,7 @@ impl<TF: TypeFamily> Debug for Goal<TF> {
                 write!(fmt, "> {{ {:?} }}", subgoal.value)
             }
             GoalData::Implies(ref wc, ref g) => write!(fmt, "if ({:?}) {{ {:?} }}", wc, g),
-            GoalData::All(ref goals) => {
-                write!(fmt, "all(")?;
-                for (goal, index) in goals.iter().zip(0..) {
-                    if index > 0 {
-                        write!(fmt, ", ")?;
-                    }
-                    write!(fmt, "{:?}", goal)?;
-                }
-                write!(fmt, ")")?;
-                Ok(())
-            }
+            GoalData::All(ref goals) => write!(fmt, "all{:?}", goals),
             GoalData::Not(ref g) => write!(fmt, "not {{ {:?} }}", g),
             GoalData::EqGoal(ref wc) => write!(fmt, "{:?}", wc),
             GoalData::DomainGoal(ref wc) => write!(fmt, "{:?}", wc),
@@ -298,6 +288,20 @@ impl<TF: TypeFamily> Debug for Goal<TF> {
     }
 }
 
+impl<TF: TypeFamily> Debug for Goals<TF> {
+    fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> {
+        write!(fmt, "(")?;
+        for (goal, index) in self.iter().zip(0..) {
+            if index > 0 {
+                write!(fmt, ", ")?;
+            }
+            write!(fmt, "{:?}", goal)?;
+        }
+        write!(fmt, ")")?;
+        Ok(())
+    }
+}
+
 impl<T: Debug> Debug for Binders<T> {
     fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> {
         let Binders {
@@ -334,16 +338,18 @@ impl<TF: TypeFamily> Debug for ProgramClauseImplication<TF> {
     fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> {
         write!(fmt, "{:?}", self.consequence)?;
 
-        let conds = self.conditions.len();
+        let conditions = self.conditions.as_slice();
+
+        let conds = conditions.len();
         if conds == 0 {
             return Ok(());
         }
 
         write!(fmt, " :- ")?;
-        for cond in &self.conditions[..conds - 1] {
+        for cond in &conditions[..conds - 1] {
             write!(fmt, "{:?}, ", cond)?;
         }
-        write!(fmt, "{:?}", self.conditions[conds - 1])
+        write!(fmt, "{:?}", conditions[conds - 1])
     }
 }
 

chalk-ir/src/family.rs

@@ -1,6 +1,7 @@
 use crate::tls;
 use crate::AliasTy;
 use crate::AssocTypeId;
+use crate::Goal;
 use crate::GoalData;
 use crate::LifetimeData;
 use crate::Parameter;
@@ -69,6 +70,14 @@ pub trait TypeFamily: Debug + Copy + Eq + Ord + Hash {
     /// converted back to its underlying data via `goal_data`.
     type InternedGoal: Debug + Clone + Eq + Ord + Hash;
 
+    /// "Interned" representation of a list of goals.  In normal user code,
+    /// `Self::InternedGoals` is not referenced. Instead, we refer to
+    /// `Goals<Self>`, which wraps this type.
+    ///
+    /// An `InternedGoals` is created by `intern_goals` and can be
+    /// converted back to its underlying data via `goals_data`.
+    type InternedGoals: Debug + Clone + Eq + Ord + Hash;
+
     /// "Interned" representation of a "substitution".  In normal user code,
     /// `Self::InternedSubstitution` is not referenced. Instead, we refer to
     /// `Substitution<Self>`, which wraps this type.
@@ -155,6 +164,15 @@ pub trait TypeFamily: Debug + Copy + Eq + Ord + Hash {
     /// Lookup the `GoalData` that was interned to create a `InternedGoal`.
     fn goal_data(goal: &Self::InternedGoal) -> &GoalData<Self>;
 
+    /// Create an "interned" goals from `data`. This is not
+    /// normally invoked directly; instead, you invoke
+    /// `GoalsData::intern` (which will ultimately call this
+    /// method).
+    fn intern_goals(data: impl IntoIterator<Item = Goal<Self>>) -> Self::InternedGoals;
+
+    /// Lookup the `GoalsData` that was interned to create a `InternedGoals`.
+    fn goals_data(goals: &Self::InternedGoals) -> &[Goal<Self>];
+
     /// Create an "interned" substitution from `data`. This is not
     /// normally invoked directly; instead, you invoke
     /// `SubstitutionData::intern` (which will ultimately call this
@@ -198,6 +216,7 @@ impl TypeFamily for ChalkIr {
     type InternedLifetime = LifetimeData<ChalkIr>;
     type InternedParameter = ParameterData<ChalkIr>;
     type InternedGoal = Arc<GoalData<ChalkIr>>;
+    type InternedGoals = Vec<Goal<ChalkIr>>;
     type InternedSubstitution = Vec<Parameter<ChalkIr>>;
     type DefId = RawId;
 
@@ -258,6 +277,14 @@ impl TypeFamily for ChalkIr {
         goal
     }
 
+    fn intern_goals(data: impl IntoIterator<Item = Goal<ChalkIr>>) -> Vec<Goal<ChalkIr>> {
+        data.into_iter().collect()
+    }
+
+    fn goals_data(goals: &Vec<Goal<ChalkIr>>) -> &[Goal<ChalkIr>] {
+        goals
+    }
+
     fn intern_substitution<E>(
         data: impl IntoIterator<Item = Result<Parameter<ChalkIr>, E>>,
     ) -> Result<Vec<Parameter<ChalkIr>>, E> {