Skip to content

Commit

Permalink
doc: fix MetavarContext markdown (#3026)
Browse files Browse the repository at this point in the history 
I found the documentation page hard to parse, so I figured I should fix
this. It's mostly indentation (e.g. in lists), some line breaks and
making URLs clickable.
  • Loading branch information
@nomeata
nomeata authored Dec 6, 2023
1 parent d4f10bc commit 5d35e94
Showing 1 changed file with 135 additions and 122 deletions.
257 changes: 135 additions & 122 deletions src/Lean/MetavarContext.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,76 +15,79 @@ assignments. It is used in the elaborator, tactic framework, unifier
the requirements imposed by these modules.
- We may invoke TC while executing `isDefEq`. We need this feature to
be able to solve unification problems such as:
```
f ?a (ringAdd ?s) ?x ?y =?= f Int intAdd n m
```
where `(?a : Type) (?s : Ring ?a) (?x ?y : ?a)`
During `isDefEq` (i.e., unification), it will need to solve the constrain
```
ringAdd ?s =?= intAdd
```
We say `ringAdd ?s` is stuck because it cannot be reduced until we
synthesize the term `?s : Ring ?a` using TC. This can be done since we
have assigned `?a := Int` when solving `?a =?= Int`.
WellFoundedRelationbe able to solve unification problems such as:
```
f ?a (ringAdd ?s) ?x ?y =?= f Int intAdd n m
```
where `(?a : Type) (?s : Ring ?a) (?x ?y : ?a)`.
During `isDefEq` (i.e., unification), it will need to solve the constrain
```
ringAdd ?s =?= intAdd
```
We say `ringAdd ?s` is stuck because it cannot be reduced until we
synthesize the term `?s : Ring ?a` using TC. This can be done since we
have assigned `?a := Int` when solving `?a =?= Int`.
- TC uses `isDefEq`, and `isDefEq` may create TC problems as shown
above. Thus, we may have nested TC problems.
above. Thus, we may have nested TC problems.
- `isDefEq` extends the local context when going inside binders. Thus,
the local context for nested TC may be an extension of the local
context for outer TC.
the local context for nested TC may be an extension of the local
context for outer TC.
- TC should not assign metavariables created by the elaborator, simp,
tactic framework, and outer TC problems. Reason: TC commits to the
first solution it finds. Consider the TC problem `Coe Nat ?x`,
where `?x` is a metavariable created by the caller. There are many
solutions to this problem (e.g., `?x := Int`, `?x := Real`, ...),
and it doesn’t make sense to commit to the first one since TC does
not know the constraints the caller may impose on `?x` after the
TC problem is solved.
Remark: we claim it is not feasible to make the whole system backtrackable,
and allow the caller to backtrack back to TC and ask it for another solution
if the first one found did not work. We claim it would be too inefficient.
tactic framework, and outer TC problems. Reason: TC commits to the
first solution it finds. Consider the TC problem `Coe Nat ?x`,
where `?x` is a metavariable created by the caller. There are many
solutions to this problem (e.g., `?x := Int`, `?x := Real`, ...),
and it doesn’t make sense to commit to the first one since TC does
not know the constraints the caller may impose on `?x` after the
TC problem is solved.
Remark: we claim it is not feasible to make the whole system backtrackable,
and allow the caller to backtrack back to TC and ask it for another solution
if the first one found did not work. We claim it would be too inefficient.
- TC metavariables should not leak outside of TC. Reason: we want to
get rid of them after we synthesize the instance.
get rid of them after we synthesize the instance.
- `simp` invokes `isDefEq` for matching the left-hand-side of
equations to terms in our goal. Thus, it may invoke TC indirectly.
equations to terms in our goal. Thus, it may invoke TC indirectly.
- In Lean3, we didn’t have to create a fresh pattern for trying to
match the left-hand-side of equations when executing `simp`. We had a
mechanism called "tmp" metavariables. It avoided this overhead, but it
created many problems since `simp` may indirectly call TC which may
recursively call TC. Moreover, we may want to allow TC to invoke
tactics in the future. Thus, when `simp` invokes `isDefEq`, it may indirectly invoke
a tactic and `simp` itself. The Lean3 approach assumed that
metavariables were short-lived, this is not true in Lean4, and to some
extent was also not true in Lean3 since `simp`, in principle, could
trigger an arbitrary number of nested TC problems.
match the left-hand-side of equations when executing `simp`. We had a
mechanism called "tmp" metavariables. It avoided this overhead, but it
created many problems since `simp` may indirectly call TC which may
recursively call TC. Moreover, we may want to allow TC to invoke
tactics in the future. Thus, when `simp` invokes `isDefEq`, it may indirectly invoke
a tactic and `simp` itself. The Lean3 approach assumed that
metavariables were short-lived, this is not true in Lean4, and to some
extent was also not true in Lean3 since `simp`, in principle, could
trigger an arbitrary number of nested TC problems.
- Here are some possible call stack traces we could have in Lean3 (and Lean4).
```
Elaborator (-> TC -> isDefEq)+
Elaborator -> isDefEq (-> TC -> isDefEq)*
Elaborator -> simp -> isDefEq (-> TC -> isDefEq)*
```
In Lean4, TC may also invoke tactics in the future.
```
Elaborator (-> TC -> isDefEq)+
Elaborator -> isDefEq (-> TC -> isDefEq)*
Elaborator -> simp -> isDefEq (-> TC -> isDefEq)*
```
In Lean4, TC may also invoke tactics in the future.
- In Lean3 and Lean4, TC metavariables are not really short-lived. We
solve an arbitrary number of unification problems, and we may have
nested TC invocations.
solve an arbitrary number of unification problems, and we may have
nested TC invocations.
- TC metavariables do not share the same local context even in the
same invocation. In the C++ and Lean implementations we use a trick to
ensure they do:
https://github.com/leanprover/lean/blob/92826917a252a6092cffaf5fc5f1acb1f8cef379/src/library/type_context.cpp#L3583-L3594
same invocation. In the C++ and Lean implementations we use a trick to
ensure they do:
<https://github.com/leanprover/lean/blob/92826917a252a6092cffaf5fc5f1acb1f8cef379/src/library/type_context.cpp#L3583-L3594>
- Metavariables may be natural, synthetic or syntheticOpaque.
a) Natural metavariables may be assigned by unification (i.e., `isDefEq`).
b) Synthetic metavariables may still be assigned by unification,
1. Natural metavariables may be assigned by unification (i.e., `isDefEq`).
2. Synthetic metavariables may still be assigned by unification,
but whenever possible `isDefEq` will avoid the assignment. For example,
if we have the unification constraint `?m =?= ?n`, where `?m` is synthetic,
but `?n` is not, `isDefEq` solves it by using the assignment `?n := ?m`.
Expand All @@ -94,7 +97,7 @@ https://github.com/leanprover/lean/blob/92826917a252a6092cffaf5fc5f1acb1f8cef379
them, and check whether the synthesized result is compatible with the one
assigned by `isDefEq`.
c) SyntheticOpaque metavariables are never assigned by `isDefEq`.
3. SyntheticOpaque metavariables are never assigned by `isDefEq`.
That is, the constraint `?n =?= Nat.succ Nat.zero` always fail
if `?n` is a syntheticOpaque metavariable. This kind of metavariable
is created by tactics such as `intro`. Reason: in the tactic framework,
Expand All @@ -104,78 +107,80 @@ https://github.com/leanprover/lean/blob/92826917a252a6092cffaf5fc5f1acb1f8cef379
This distinction was not precise in Lean3 and produced
counterintuitive behavior. For example, the following hack was added
in Lean3 to work around one of these issues:
https://github.com/leanprover/lean/blob/92826917a252a6092cffaf5fc5f1acb1f8cef379/src/library/type_context.cpp#L2751
<https://github.com/leanprover/lean/blob/92826917a252a6092cffaf5fc5f1acb1f8cef379/src/library/type_context.cpp#L2751>
- When creating lambda/forall expressions, we need to convert/abstract
free variables and convert them to bound variables. Now, suppose we are
trying to create a lambda/forall expression by abstracting free
variable `xs` and a term `t[?m]` which contains a metavariable `?m`,
and the local context of `?m` contains `xs`. The term
```
fun xs => t[?m]
```
will be ill-formed if we later assign a term `s` to `?m`, and
`s` contains free variables in `xs`. We address this issue by changing
the free variable abstraction procedure. We consider two cases: `?m`
is natural or synthetic, or `?m` is syntheticOpaque. Assume the type of `?m` is
`A[xs]`. Then, in both cases we create an auxiliary metavariable `?n` with
type `forall xs => A[xs]`, and local context := local context of `?m` - `xs`.
In both cases, we produce the term `fun xs => t[?n xs]`
1- If `?m` is natural or synthetic, then we assign `?m := ?n xs`, and we produce
the term `fun xs => t[?n xs]`
2- If `?m` is syntheticOpaque, then we mark `?n` as a syntheticOpaque variable.
However, `?n` is managed by the metavariable context itself.
We say we have a "delayed assignment" `?n xs := ?m`.
That is, after a term `s` is assigned to `?m`, and `s`
does not contain metavariables, we replace any occurrence
`?n ts` with `s[xs := ts]`.
Gruesome details:
free variables and convert them to bound variables. Now, suppose we are
trying to create a lambda/forall expression by abstracting free
variable `xs` and a term `t[?m]` which contains a metavariable `?m`,
and the local context of `?m` contains `xs`. The term
```
fun xs => t[?m]
```
will be ill-formed if we later assign a term `s` to `?m`, and
`s` contains free variables in `xs`. We address this issue by changing
the free variable abstraction procedure. We consider two cases: `?m`
is natural or synthetic, or `?m` is syntheticOpaque. Assume the type of `?m` is
`A[xs]`. Then, in both cases we create an auxiliary metavariable `?n` with
type `forall xs => A[xs]`, and local context := local context of `?m` - `xs`.
In both cases, we produce the term `fun xs => t[?n xs]`
1. If `?m` is natural or synthetic, then we assign `?m := ?n xs`, and we produce
the term `fun xs => t[?n xs]`
2. If `?m` is syntheticOpaque, then we mark `?n` as a syntheticOpaque variable.
However, `?n` is managed by the metavariable context itself.
We say we have a "delayed assignment" `?n xs := ?m`.
That is, after a term `s` is assigned to `?m`, and `s`
does not contain metavariables, we replace any occurrence
`?n ts` with `s[xs := ts]`.
Gruesome details:
- When we create the type `forall xs => A` for `?n`, we may
encounter the same issue if `A` contains metavariables. So, the
process above is recursive. We claim it terminates because we keep
creating new metavariables with smaller local contexts.
encounter the same issue if `A` contains metavariables. So, the
process above is recursive. We claim it terminates because we keep
creating new metavariables with smaller local contexts.
- Suppose, we have `t[?m]` and we want to create a let-expression by
abstracting a let-decl free variable `x`, and the local context of
`?m` contains `x`. Similarly to the previous case
```
let x : T := v; t[?m]
```
will be ill-formed if we later assign a term `s` to `?m`, and
`s` contains free variable `x`. Again, assume the type of `?m` is `A[x]`.
1- If `?m` is natural or synthetic, then we create `?n : (let x : T := v; A[x])` with
and local context := local context of `?m` - `x`, we assign `?m := ?n`,
and produce the term `let x : T := v; t[?n]`. That is, we are just making
sure `?n` must never be assigned to a term containing `x`.
2- If `?m` is syntheticOpaque, we create a fresh syntheticOpaque `?n`
with type `?n : T -> (let x : T := v; A[x])` and local context := local context of `?m` - `x`,
create the delayed assignment `?n #[x] := ?m`, and produce the term `let x : T := v; t[?n x]`.
Now suppose we assign `s` to `?m`. We do not assign the term `fun (x : T) => s` to `?n`, since
`fun (x : T) => s` may not even be type correct. Instead, we just replace applications `?n r`
with `s[x/r]`. The term `r` may not necessarily be a bound variable. For example, a tactic
may have reduced `let x : T := v; t[?n x]` into `t[?n v]`.
We are essentially using the pair "delayed assignment + application" to implement a delayed
substitution.
abstracting a let-decl free variable `x`, and the local context of
`?m` contains `x`. Similarly to the previous case
```
let x : T := v; t[?m]
```
will be ill-formed if we later assign a term `s` to `?m`, and
`s` contains free variable `x`. Again, assume the type of `?m` is `A[x]`.
1. If `?m` is natural or synthetic, then we create `?n : (let x : T := v; A[x])` with
and local context := local context of `?m` - `x`, we assign `?m := ?n`,
and produce the term `let x : T := v; t[?n]`. That is, we are just making
sure `?n` must never be assigned to a term containing `x`.
2. If `?m` is syntheticOpaque, we create a fresh syntheticOpaque `?n`
with type `?n : T -> (let x : T := v; A[x])` and local context := local context of `?m` - `x`,
create the delayed assignment `?n #[x] := ?m`, and produce the term `let x : T := v; t[?n x]`.
Now suppose we assign `s` to `?m`. We do not assign the term `fun (x : T) => s` to `?n`, since
`fun (x : T) => s` may not even be type correct. Instead, we just replace applications `?n r`
with `s[x/r]`. The term `r` may not necessarily be a bound variable. For example, a tactic
may have reduced `let x : T := v; t[?n x]` into `t[?n v]`.
We are essentially using the pair "delayed assignment + application" to implement a delayed
substitution.
- We use TC for implementing coercions. Both Joe Hendrix and Reid Barton
reported a nasty limitation. In Lean3, TC will not be used if there are
metavariables in the TC problem. For example, the elaborator will not try
to synthesize `Coe Nat ?x`. This is good, but this constraint is too
strict for problems such as `Coe (Vector Bool ?n) (BV ?n)`. The coercion
exists independently of `?n`. Thus, during TC, we want `isDefEq` to throw
an exception instead of return `false` whenever it tries to assign
a metavariable owned by its caller. The idea is to sign to the caller that
it cannot solve the TC problem at this point, and more information is needed.
That is, the caller must make progress an assign its metavariables before
trying to invoke TC again.
In Lean4, we are using a simpler design for the `MetavarContext`.
reported a nasty limitation. In Lean3, TC will not be used if there are
metavariables in the TC problem. For example, the elaborator will not try
to synthesize `Coe Nat ?x`. This is good, but this constraint is too
strict for problems such as `Coe (Vector Bool ?n) (BV ?n)`. The coercion
exists independently of `?n`. Thus, during TC, we want `isDefEq` to throw
an exception instead of return `false` whenever it tries to assign
a metavariable owned by its caller. The idea is to sign to the caller that
it cannot solve the TC problem at this point, and more information is needed.
That is, the caller must make progress an assign its metavariables before
trying to invoke TC again.
In Lean4, we are using a simpler design for the `MetavarContext`.
- No distinction between temporary and regular metavariables.
Expand All @@ -184,6 +189,7 @@ In Lean4, we are using a simpler design for the `MetavarContext`.
- MetavarContext also has a `depth` field.
- We bump the `MetavarContext` depth when we create a nested problem.
Example: Elaborator (depth = 0) -> Simplifier matcher (depth = 1) -> TC (level = 2) -> TC (level = 3) -> ...
- When `MetavarContext` is at depth N, `isDefEq` does not assign variables from `depth < N`.
Expand All @@ -192,11 +198,12 @@ In Lean4, we are using a simpler design for the `MetavarContext`.
- New design even allows us to invoke tactics from TC.
* Main concern
We don't have tmp metavariables anymore in Lean4. Thus, before trying to match
the left-hand-side of an equation in `simp`. We first must bump the level of the `MetavarContext`,
create fresh metavariables, then create a new pattern by replacing the free variable on the left-hand-side with
these metavariables. We are hoping to minimize this overhead by
- Main concern
We don't have tmp metavariables anymore in Lean4. Thus, before trying to match
the left-hand-side of an equation in `simp`. We first must bump the level of the `MetavarContext`,
create fresh metavariables, then create a new pattern by replacing the free variable on the left-hand-side with
these metavariables. We are hoping to minimize this overhead by
- Using better indexing data structures in `simp`. They should reduce the number of time `simp` must invoke `isDefEq`.
Expand Down Expand Up @@ -480,7 +487,8 @@ def assignDelayedMVar [MonadMCtx m] (mvarId : MVarId) (fvars : Array Expr) (mvar
modifyMCtx fun m => { m with dAssignment := m.dAssignment.insert mvarId { fvars, mvarIdPending } }

/-!
Notes on artificial eta-expanded terms due to metavariables.
## Notes on artificial eta-expanded terms due to metavariables.
We try avoid synthetic terms such as `((fun x y => t) a b)` in the output produced by the elaborator.
This kind of term may be generated when instantiating metavariable assignments.
This module tries to avoid their generation because they often introduce unnecessary dependencies and
Expand All @@ -491,9 +499,11 @@ all free variables that may be used to "fill" the hole. Suppose, we create a met
containing `(x : Nat) (y : Nat) (b : Bool)`, then we can assign terms such as `x + y` to `?m` since `x` and `y`
are in the context used to create `?m`. Now, suppose we have the term `?m + 1` and we want to create the lambda expression
`fun x => ?m + 1`. This term is not correct since we may assign to `?m` a term containing `x`.
We address this issue by create a synthetic metavariable `?n : Nat → Nat` and adding the delayed assignment
`?n #[x] := ?m`, and the term `fun x => ?n x + 1`. When we later assign a term `t[x]` to `?m`, `fun x => t[x]` is assigned to
`?n`, and if we substitute it at `fun x => ?n x + 1`, we produce `fun x => ((fun x => t[x]) x) + 1`.
To avoid this term eta-expanded term, we apply beta-reduction when instantiating metavariable assignments in this module.
This operation is performed at `instantiateExprMVars`, `elimMVarDeps`, and `levelMVarToParam`.
-/
Expand Down Expand Up @@ -923,7 +933,8 @@ private def getLocalDeclWithSmallestIdx (lctx : LocalContext) (xs : Array Expr)
Remark: We used to throw an `Exception.revertFailure` exception when an auxiliary declaration
had to be reversed. Recall that auxiliary declarations are created when compiling (mutually)
recursive definitions. The `revertFailure` due to auxiliary declaration dependency was originally
introduced in Lean3 to address issue https://github.com/leanprover/lean/issues/1258.
introduced in Lean3 to address issue <https://github.com/leanprover/lean/issues/1258>.
In Lean4, this solution is not satisfactory because all definitions/theorems are potentially
recursive. So, even a simple (incomplete) definition such as
```
Expand All @@ -939,11 +950,13 @@ private def getLocalDeclWithSmallestIdx (lctx : LocalContext) (xs : Array Expr)
we create the metavariable `?n : {α : Type} → (a : α) → (f : α → List α) → List α`,
add the delayed assignment `?n #[α, a, f] := ?m`, and create the lambda
`fun {α : Type} (a : α) => ?n α a f`.
See `elimMVarDeps` for more information.
If we kept using the Lean3 approach, we would get the `Exception.revertFailure` exception because we are
reverting the auxiliary definition `f`.
Note that https://github.com/leanprover/lean/issues/1258 is not an issue in Lean4 because
Note that <https://github.com/leanprover/lean/issues/1258> is not an issue in Lean4 because
we have changed how we compile recursive definitions.
-/
def collectForwardDeps (lctx : LocalContext) (toRevert : Array Expr) : M (Array Expr) := do
Expand Down

0 comments on commit 5d35e94

Please sign in to comment.