Introduce a "scope" mechanism to judgments and use for binder instantiation

book/src/formality_core/judgment_fn.md

@@ -329,6 +329,87 @@ implicit upcast or the collection type.
 This syntax is available inside a judgment's `let` premise; it is not an ordinary
 Rust expression. The `for_all` body does not select a collection type.
 
+### Entering and leaving scopes
+
+A proof sometimes needs temporary context: for example, fresh variables used to
+check the body of a binder. Before the proof's result can be used outside that
+context, it may need to be checked or transformed. A result that still refers to
+a temporary variable might not be meaningful outside the binder.
+
+The `scope` condition groups the premises that use this temporary context and
+passes their results through an explicit exit operation:
+
+```rust,ignore
+(scope(enter_binder(env, binder) => (env, body)) with(result)
+    (check_body(env, body) => result))
+```
+
+Here `enter_binder` and `check_body` are hypothetical helpers for the language
+being modeled. The macro does not provide binder handling itself. The general
+syntax is:
+
+```text
+(scope(enter_expression => inside_pattern) with(exported_names)
+    (premise)
+    ...)
+```
+
+The entry expression returns a pair: **a scope object and the values available
+inside it**. For the example above, its return type might be:
+
+```rust,ignore
+fn enter_binder(env: &Env, binder: &Binder) -> (BinderScope, (Env, Term))
+```
+
+The pattern `(env, body)` matches only the second element, `(Env, Term)`. The
+macro keeps the `BinderScope` object in a hidden local. The inner `env` shadows
+the outer one for the nested premises; after the scope, `env` refers to the
+outer environment again.
+
+#### Exporting results with `with`
+
+Bindings introduced inside the scope are local to its nested premises. List
+what the rest of the rule needs in `with(...)`. In the example, each successful
+proof of `check_body` supplies a `result` to the exit operation. The rest of the
+rule receives the result returned by that operation, which may differ from the
+one computed inside.
+
+Use `with(a, b)` to export two values, or `with()` when the nested premises only
+need to establish that something holds. Even with no exported values, the exit
+operation runs for each successful inner proof. Scopes can also be nested.
+
+#### Defining what it means to leave
+
+The scope object implements this trait from `formality_core::judgment`:
+
+```rust,ignore
+pub trait Scope<Values> {
+    fn leave(&self, values: Values) -> ProvenSet<Values>;
+}
+```
+
+`Values` is the tuple of exported values: `with(result)` uses `(ResultType,)`,
+`with(a, b)` uses `(A, B)`, and `with()` uses `()`. Thus the example requires an
+implementation of `Scope<(ResultType,)>` for `BinderScope`. The pair `(env, body)`
+is the input to the nested premises, not the object implementing `Scope`.
+
+For every successful inner proof, the macro effectively calls:
+
+```rust,ignore
+Scope::leave(&scope_object, (result,))
+```
+
+`leave` runs for each successful inner proof.
+`leave` returns a `ProvenSet`, so it can reject that result, return one
+transformed result, or produce several alternatives. The remaining premises
+of the rule run for each successful result returned by `leave`. If no inner
+proof can leave the scope successfully, this rule produces no result.
+
+The entry expression can use `?` to report a failure, just like other premise
+expressions. The `inside_pattern` must be irrefutable. A match confirmation
+marker `!` cannot appear inside a scope; put it on a premise before the scope
+when needed.
+
 ### Handling cycles
 
 Judgment functions must be **inductive**, which means that cycles are considered failures. We have a tabling implementation, which means we detect cycles and try to handle them intelligently. Basically we track a stack and, if a cycle is detected, we return an empty set of results. But we remember that the cycle happened. Then, once we are done, we'll have computed some intermediate set of results `R[0]`, and we execute again. This time, when we get the cycle, we return `R[0]` instead of an empty set. This will compute some new set of results, `R[1]`. So then we try again. We keep doing this until the new set of results `R[i]` is equal to the previous set of results `R[i-1]`. At that point, we have reached a fixed point, so we stop. Of course, it could be that you get an infinitely growing set of results, and execution never terminates. This means your rules are broken. Don't do that.

crates/formality-core/src/judgment.rs

@@ -13,13 +13,17 @@ pub use proven_set::{
     FailureLocation, FailureReason, LeafFailure, ProofTree, Proven, ProvenSet, RuleFailureCause,
 };
 
+mod scope;
 #[cfg(test)]
 mod test_comprehension;
+pub use scope::Scope;
+
 mod test_explicit_fail;
 mod test_fallible;
 mod test_filtered;
 mod test_for_all;
 mod test_reachable;
+mod test_scope;
 
 pub type JudgmentStack<J, O> = RefCell<FixedPointStack<J, Map<O, ProofTree>>>;
 
@@ -53,6 +57,34 @@ pub type JudgmentStack<J, O> = RefCell<FixedPointStack<J, Map<O, ProofTree>>>;
 ///   additionally carries the named variables between iterations. Shadow them
 ///   inside the loop to update them; later conditions see their final values.
 ///   The loop retains one successful result per element, not all combinations.
+/// * `(scope(<expr> => <pat>) with(<vars>) <conditions>)` -- proves the nested conditions inside a [`Scope`][], see below.
+///
+/// ## Scopes
+///
+/// `<expr>` enters a scope: it evaluates to a pair of the [`Scope`][] and
+/// what is inside it, which `<pat>` binds for the nested conditions. Those
+/// bindings, and any the nested conditions make, end with the `scope`
+/// condition. Only `<vars>` come out: each proof of the nested conditions
+/// leaves the scope with its values for them ([`Scope::leave`][]), and the
+/// rest of the rule sees what that yields.
+///
+/// Like any other condition's expression, `<expr>` may fail; the rule then
+/// does not apply. `<pat>` must be irrefutable: it binds what is inside the
+/// scope, so there is no other case for it to match.
+///
+/// ```ignore
+/// (
+///     (scope(enter_forall(env, binder) => (env, body)) with(c)
+///         (prove(env, body) => c))
+///     --------------------
+///     (prove(env, Goal::ForAll(binder)) => c)
+/// )
+/// ```
+///
+/// So the rule cannot forget to leave the scope, nor use what was inside it
+/// afterwards. A match commit point `!` cannot be nested in a `scope`; it
+/// marks how far the rule got before the scope, so it belongs beside the
+/// conditions `@accum` can see.
 ///
 /// The conclusions can be the following
 ///
@@ -537,6 +569,18 @@ macro_rules! push_rules {
     // expression `v` is carried in from the conclusion and forms the final
     // output of this rule, once all the conditions are evaluated.
 
+    // A match commit point nested in a `scope` would do nothing: the `@accum`
+    // phase only sees the conditions of the rule itself, so it never switched
+    // the match default, and setting it again here has no effect. Reject it
+    // rather than let it look like it works. (This arm must precede the one
+    // below, which would otherwise match.)
+    (
+        @body (scope($scope_proofs:ident, ($($with_var:ident,)*))); $_inputs:tt; $child_proof_trees:ident;
+        ! $($m:tt)*
+    ) => {
+        compile_error!("a match commit point `!` cannot be nested in a `scope`")
+    };
+
     (
         @body $args:tt; ($failed_rules:expr, $match_var:ident, $input_info:tt, $rule_name:literal); $child_proof_trees:ident;
         ! $($m:tt)*
@@ -838,6 +882,63 @@ macro_rules! push_rules {
             $($m)*);
     };
 
+    // `(scope(<expr> => <pat>) with(<vars>) <conditions>)`: prove the nested
+    // conditions inside a scope. Each of their proofs leaves the scope with
+    // its values for `<vars>`, and the rest of the rule continues with the
+    // result.
+    (
+        @body $args:tt; $inputs:tt; $child_proof_trees:ident;
+        (scope($scope:expr => $inside:pat) with($($with_var:ident),*) $($inner_step:tt)*) $($m:tt)*
+    ) => {
+        match $crate::judgment::try_catch(|| Ok($scope)) {
+            Err(e) => {
+                $crate::push_rules!(@record_failure $inputs; $scope; e);
+            }
+
+            Ok((scope, inside)) => {
+                // Prove the nested conditions. They see what is inside the scope
+                // (and, being in a block, what they bind ends with it). Collect
+                // each proof's values for the `with` variables.
+                let mut scope_proofs = vec![];
+                {
+                    #[allow(unused_variables)]
+                    let $inside = &inside;
+                    #[allow(unused_mut)]
+                    let mut inner_proof_trees: Vec<$crate::judgment::ProofTree> = Vec::new();
+                    $crate::push_rules!(@body (scope(scope_proofs, ($($with_var,)*))); $inputs; inner_proof_trees; $($inner_step)*);
+                }
+
+                // Leave the scope with each, and continue with what comes out.
+                for (values, inner_proof_trees) in scope_proofs {
+                    if let Err(e) = $crate::judgment::EachProof::each_proof(
+                        $crate::judgment::Scope::leave(&scope, values),
+                        |(values, leave_proof_tree)| {
+                            #[allow(unused_variables)]
+                            let ($($with_var,)*) = &values;
+
+                            let len = $child_proof_trees.len();
+
+                            let mut scope_proof_trees = inner_proof_trees.clone();
+                            scope_proof_trees.push(leave_proof_tree);
+                            $child_proof_trees.push($crate::judgment::ProofTree::new(
+                                "scope",
+                                None,
+                                scope_proof_trees,
+                            ));
+
+                            $crate::push_rules!(@body $args; $inputs; $child_proof_trees; $($m)*);
+
+                            assert!($child_proof_trees.len() > len);
+                            $child_proof_trees.truncate(len);
+                        },
+                    ) {
+                        $crate::push_rules!(@record_failure $inputs; $scope; e);
+                    }
+                }
+            }
+        }
+    };
+
     // for_all with accumulator: forward to @body_for_all
     (
         @body $args:tt; $inputs:tt; $child_proof_trees:ident;
@@ -1104,6 +1205,13 @@ macro_rules! push_rules {
         }
     };
 
+    (
+        @body (scope($scope_proofs:ident, ($($with_var:ident,)*))); $_inputs:tt; $child_proof_trees:ident;
+    ) => {
+        // one proof of the conditions nested in a `scope`: capture the values to leave it with.
+        $scope_proofs.push((($($with_var.clone(),)*), $child_proof_trees.clone()));
+    };
+
     (
         @body (loop($next_carried_and_proof:ident, ($($with_var:ident,)*))); $_inputs:tt; $child_proof_trees:ident;
     ) => {

crates/formality-core/src/judgment/scope.rs

@@ -0,0 +1,17 @@
+use super::ProvenSet;
+
+/// A scope that conditions of an inference rule can be proven in, with the
+/// `(scope(<expr> => <pat>) with(<vars>) <conditions>)` condition of
+/// [`judgment_fn!`](crate::judgment_fn).
+///
+/// `<expr>` enters the scope: it evaluates to the scope and to what the
+/// nested conditions see inside it, as a pair. A scope typically extends an
+/// environment for them, e.g. with the variables of a binder.
+///
+/// `Values` is the type of what they prove: the tuple of the `with`
+/// variables.
+pub trait Scope<Values> {
+    /// `values`, proven inside the scope, as they hold outside of it. There
+    /// may be several ways for them to, or none.
+    fn leave(&self, values: Values) -> ProvenSet<Values>;
+}