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,94 @@
+# 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` and
+`SuperFold` traits. The derives are a bit cludgy and require:
+
+* You must import `Fold` (or `SuperFold`, respectively) 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-derive/src/lib.rs

@@ -147,6 +147,140 @@ pub fn derive_fold(item: TokenStream) -> TokenStream {
     panic!("derive(Fold) requires a parameter that implements HasTypeFamily or TypeFamily");
 }
 
+/// Derives Fold for structs and enums for which one of the following is true:
+/// - It has a `#[has_type_family(TheTypeFamily)]` attribute
+/// - There is a single parameter `T: HasTypeFamily` (does not have to be named `T`)
+/// - There is a single parameter `TF: TypeFamily` (does not have to be named `TF`)
+#[proc_macro_derive(SuperFold, attributes(has_type_family))]
+pub fn derive_super_fold(item: TokenStream) -> TokenStream {
+    let input = parse_macro_input!(item as DeriveInput);
+    let (impl_generics, ty_generics, where_clause_ref) = input.generics.split_for_impl();
+
+    let type_name = input.ident;
+    let body = derive_fold_body(&type_name, input.data);
+
+    if let Some(attr) = input
+        .attrs
+        .iter()
+        .find(|a| a.path.is_ident("has_type_family"))
+    {
+        // Hardcoded type-family:
+        //
+        // impl SuperFold<ChalkIr, ChalkIr> for Type {
+        // }
+        let arg = attr
+            .parse_args::<proc_macro2::TokenStream>()
+            .expect("Expected has_type_family argument");
+
+        return TokenStream::from(quote! {
+            impl #impl_generics SuperFold < #arg, #arg > for #type_name #ty_generics #where_clause_ref {
+                fn super_fold_with(
+                    &self,
+                    folder: &mut dyn Folder < #arg, #arg >,
+                    binders: usize,
+                ) -> ::chalk_engine::fallible::Fallible<Self::Result> {
+                    #body
+                }
+            }
+        });
+    }
+
+    match input.generics.params.len() {
+        1 => {}
+
+        0 => {
+            panic!("Fold derive requires a single type parameter or a `#[has_type_family]` attr");
+        }
+
+        _ => {
+            panic!("Fold derive only works with a single type parameter");
+        }
+    };
+
+    let generic_param0 = &input.generics.params[0];
+
+    if let Some(param) = has_type_family(&generic_param0) {
+        // HasTypeFamily bound:
+        //
+        // Example:
+        //
+        // impl<T, _TF, _TTF, _U> SuperFold<_TF, _TTF> for Binders<T>
+        // where
+        //     T: HasTypeFamily<TypeFamily = _TF>,
+        //     T: Fold<_TF, _TTF, Result = _U>,
+        //     U: HasTypeFamily<TypeFamily = _TTF>,
+        // {
+        // }
+
+        let mut impl_generics = input.generics.clone();
+        impl_generics.params.extend(vec![
+            GenericParam::Type(syn::parse(quote! { _TF: TypeFamily }.into()).unwrap()),
+            GenericParam::Type(syn::parse(quote! { _TTF: TargetTypeFamily<_TF> }.into()).unwrap()),
+            GenericParam::Type(
+                syn::parse(quote! { _U: HasTypeFamily<TypeFamily = _TTF> }.into()).unwrap(),
+            ),
+        ]);
+
+        let mut where_clause = where_clause_ref
+            .cloned()
+            .unwrap_or_else(|| syn::parse2(quote![where]).unwrap());
+        where_clause
+            .predicates
+            .push(syn::parse2(quote! { #param: HasTypeFamily<TypeFamily = _TF> }).unwrap());
+        where_clause
+            .predicates
+            .push(syn::parse2(quote! { #param: Fold<_TF, _TTF, Result = _U> }).unwrap());
+
+        return TokenStream::from(quote! {
+            impl #impl_generics SuperFold < _TF, _TTF > for #type_name < #param >
+                #where_clause
+            {
+                fn super_fold_with(
+                    &self,
+                    folder: &mut dyn Folder < _TF, _TTF >,
+                    binders: usize,
+                ) -> ::chalk_engine::fallible::Fallible<Self::Result> {
+                    #body
+                }
+            }
+        });
+    }
+
+    // TypeFamily bound:
+    //
+    // Example:
+    //
+    // impl<TF, _TTF> SuperFold<TF, _TTF> for Foo<TF>
+    // where
+    //     TF: TypeFamily,
+    //     _TTF: TargetTypeFamily<TF>,
+    // {
+    // }
+
+    if let Some(tf) = is_type_family(&generic_param0) {
+        let mut impl_generics = input.generics.clone();
+        impl_generics.params.extend(vec![GenericParam::Type(
+            syn::parse(quote! { _TTF: TargetTypeFamily<#tf> }.into()).unwrap(),
+        )]);
+
+        return TokenStream::from(quote! {
+            impl #impl_generics SuperFold < #tf, _TTF > for #type_name < #tf >
+                #where_clause_ref
+            {
+                fn super_fold_with(
+                    &self,
+                    folder: &mut dyn Folder < #tf, _TTF >,
+                    binders: usize,
+                ) -> ::chalk_engine::fallible::Fallible<Self::Result> {
+                    #body
+                }
+            }
+        });
+    }
+
+    panic!("derive(Fold) requires a parameter that implements HasTypeFamily or TypeFamily");
+}
+
 /// Generates the body of the Fold impl
 fn derive_fold_body(type_name: &Ident, data: Data) -> proc_macro2::TokenStream {
     match data {

chalk-integration/src/lowering.rs

@@ -1134,12 +1134,9 @@ 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<_>>()?;
+            let conditions = chalk_ir::Goals::from_fallible(
+                self.conditions.iter().map(|g| g.lower(env)).rev(), // (*)
+            )?;
 
             // (*) Subtle: in the SLG solver, we pop conditions from R to
             // L. To preserve the expected order (L to R), we must
@@ -1270,11 +1267,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])
     }
 }