max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: simplify MetavarContext

Browse source 
Remove `AbstractMetavarContext` and `TmpMetavarContext`.
Disable `TypeUtil` until we decide this is the right design.

Using very simple approach:
- No distinction betwen temporary and regular metavariables.
- Metavariables have a `depth` Nat field.
- 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.
- Metavariables from depth N+1 must be fully assigned before we return to level N.
- New design even allows us to invoke tactics from TC.

cc @dselsam
This commit is contained in:
Leonardo de Moura 2019-11-05 18:44:33 -08:00
parent 41e574d6cc
commit e844a5be74
4 changed files with 460 additions and 727 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

559
library/Init/Lean/AbstractMetavarContext.lean
View file

@ -1,559 +0,0 @@
/-
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Control.Reader
import Init.Control.Conditional
import Init.Data.Option
import Init.Data.List
import Init.Data.Nat
import Init.Lean.LocalContext
import Init.Lean.MonadCache
import Init.Lean.NameGenerator
/-
- We have two kinds of metavariables in Lean: regular and temporary.
- We use temporary metavariables during type class resolution,
matching the left-hand side of equations, etc.
- During type class resolution and simplifier,
we use temporary metavariables which are cheaper to create and
dispose. Moreover, given a particular task using temporary
metavariables (e.g., matching the left-hand side of an equation),
we assume all metavariables share the same local context.
- Each regular metavariable has a unique id, a user-facing name, a
local context, and a type. The term assigned to a metavariable must
only contain free variables in the local context.
- A regular metavariable may be marked a synthetic. Synthetic
metavariables cannot be assigned by the unifier. The tactic
framework and elaborator are some of the modules responsible for
assigning synthetic metavariables.
- When creating lambda/forall expressions, we need to convert/abstract
free variables and convert them to bound variables. Now, suppose we
a trying to create a lambda/forall expression by abstracting free
variables `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 not
synthetic, `?m` is synthetic. Assume the type of `?m` is `A`. Then,
in both cases we create an auxiliary metavariable `?n` with type
`forall xs => A`, and local context := local context of `?m` - `xs`.
In both cases, we produce the term `fun xs => t[?n xs]`
1- If `?m` is not synthetic, then we assign `?m := ?n xs`, and we produce the term
`fun xs => t[?n xs]`
2- If `?m` is synthetic, then we mark `?n` as a synthetic 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 assign `fun xs => s` to `?n`.
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.
- The type of variables `xs` may contain metavariables, and we must
recursively apply the process above. Again, we claim the process
terminates because the metavariables is ocurring in the types of
`xs`, they must have smaller local contexts.
- We can only assign `fun xs => s` to `?n` in case 2, the types
of `xs` must also not contain metavariables. To be precise, it is
sufficient they do not contain metavariables with local contexts
containing any of the `xs`s.
-/
namespace Lean
structure MetavarDecl :=
(userName : Name)
(lctx : LocalContext)
(type : Expr)
(synthetic : Bool)
namespace MetavarDecl
instance : Inhabited MetavarDecl :=
⟨⟨arbitrary _, arbitrary _, arbitrary _, false⟩⟩
end MetavarDecl
/--
A delayed assignment for a metavariable `?m`. It represents an assignment of the form
`?m := (fun fvars => val)`. The local context `lctx` provides the declarations for `fvars`.
Note that `fvars` may not be defined in the local context for `?m`. -/
structure DelayedMetavarAssignment :=
(lctx : LocalContext)
(fvars : Array Expr)
(val : Expr)
/--
Abstract interface for metavariable context objects. The
`MetavarContext` is the main implementation and is used in the
elaborator and tactic framework.
The `TemporaryMetavariableContext` is used to implement the
type class resolution procedures and matching for rewriting rules. -/
class AbstractMetavarContext (σ : Type) :=
(empty : σ)
(isReadOnlyLevelMVar (mctx : σ) (mvarId : Name) : Bool)
(getLevelAssignment (mctx : σ) (mvarId : Name) : Option Level)
(assignLevel (mctx : σ) (mvarId : Name) (val : Level) : σ)
(isReadOnlyExprMVar (mctx : σ) (mvarId : Name) : Bool)
(getExprAssignment (mctx : σ) (mvarId : Name) : Option Expr)
(assignExpr (mctx : σ) (mvarId : Name) (val : Expr) : σ)
(getDecl (mctx : σ) (mvarId : Name) : MetavarDecl)
(assignDelayed (mctx : σ) (mvarId : Name) (lctx : LocalContext) (fvars : Array Expr) (val : Expr) : σ)
(getDelayedAssignment (mctx : σ) (mvarId : Name) : Option DelayedMetavarAssignment)
(eraseDelayed (mctx : σ) (mvarId : Name) : σ)
/- Supports auxiliary metavariables -/
(auxMVarSupport : Bool)
/- Return `none` in case of failure, or if implementation does not support the creation of auxiliary metavariables. -/
(mkAuxMVar (mctx : σ) (mvarId : Name) (lctx : LocalContext) (type : Expr) (synthetic : Bool) : σ)
namespace AbstractMetavarContext
variables {σ : Type} [AbstractMetavarContext σ]
@[inline] def isLevelAssigned (mctx : σ) (mvarId : Name) : Bool :=
(getLevelAssignment mctx mvarId).isSome
@[inline] def isExprAssigned (mctx : σ) (mvarId : Name) : Bool :=
(getExprAssignment mctx mvarId).isSome
/-- Return true iff the given level contains a non-readonly metavariable. -/
def hasAssignableLevelMVar (mctx : σ) : Level → Bool
| Level.succ lvl => lvl.hasMVar && hasAssignableLevelMVar lvl
| Level.max lvl₁ lvl₂ => (lvl₁.hasMVar && hasAssignableLevelMVar lvl₁) || (lvl₂.hasMVar && hasAssignableLevelMVar lvl₂)
| Level.imax lvl₁ lvl₂ => (lvl₁.hasMVar && hasAssignableLevelMVar lvl₁) || (lvl₂.hasMVar && hasAssignableLevelMVar lvl₂)
| Level.mvar mvarId => !isReadOnlyLevelMVar mctx mvarId
| Level.zero => false
| Level.param _ => false
/-- Return true iff the given level contains an assigned metavariable. -/
def hasAssignedLevelMVar (mctx : σ) : Level → Bool
| Level.succ lvl => lvl.hasMVar && hasAssignedLevelMVar lvl
| Level.max lvl₁ lvl₂ => (lvl₁.hasMVar && hasAssignedLevelMVar lvl₁) || (lvl₂.hasMVar && hasAssignedLevelMVar lvl₂)
| Level.imax lvl₁ lvl₂ => (lvl₁.hasMVar && hasAssignedLevelMVar lvl₁) || (lvl₂.hasMVar && hasAssignedLevelMVar lvl₂)
| Level.mvar mvarId => isLevelAssigned mctx mvarId
| Level.zero => false
| Level.param _ => false
/-- Return `true` iff expression contains assigned (level/expr) metavariables -/
def hasAssignedMVar (mctx : σ) : Expr → Bool
| Expr.const _ lvls => lvls.any (hasAssignedLevelMVar mctx)
| Expr.sort lvl => hasAssignedLevelMVar mctx lvl
| Expr.app f a => (f.hasMVar && hasAssignedMVar f) || (a.hasMVar && hasAssignedMVar a)
| Expr.letE _ t v b => (t.hasMVar && hasAssignedMVar t) || (v.hasMVar && hasAssignedMVar v) || (b.hasMVar && hasAssignedMVar b)
| Expr.forallE _ _ d b => (d.hasMVar && hasAssignedMVar d) || (b.hasMVar && hasAssignedMVar b)
| Expr.lam _ _ d b => (d.hasMVar && hasAssignedMVar d) || (b.hasMVar && hasAssignedMVar b)
| Expr.fvar _ => false
| Expr.bvar _ => false
| Expr.lit _ => false
| Expr.mdata _ e => e.hasMVar && hasAssignedMVar e
| Expr.proj _ _ e => e.hasMVar && hasAssignedMVar e
| Expr.mvar mvarId => isExprAssigned mctx mvarId
partial def instantiateLevelMVars : Level → StateM σ Level
| lvl@(Level.succ lvl₁) => do lvl₁ ← instantiateLevelMVars lvl₁; pure (Level.updateSucc! lvl lvl₁)
| lvl@(Level.max lvl₁ lvl₂) => do lvl₁ ← instantiateLevelMVars lvl₁; lvl₂ ← instantiateLevelMVars lvl₂; pure (Level.updateMax! lvl lvl₁ lvl₂)
| lvl@(Level.imax lvl₁ lvl₂) => do lvl₁ ← instantiateLevelMVars lvl₁; lvl₂ ← instantiateLevelMVars lvl₂; pure (Level.updateIMax! lvl lvl₁ lvl₂)
| lvl@(Level.mvar mvarId) => do
mctx ← get;
match getLevelAssignment mctx mvarId with
| some newLvl =>
if !newLvl.hasMVar then pure newLvl
else do
newLvl' ← instantiateLevelMVars newLvl;
modify $ fun mctx => assignLevel mctx mvarId newLvl';
pure newLvl'
| none => pure lvl
| lvl => pure lvl
namespace InstantiateExprMVars
abbrev M (σ : Type) := StateM (WithHashMapCache Expr Expr σ)
@[inline] def instantiateLevelMVars (lvl : Level) : M σ Level :=
WithHashMapCache.fromState $ AbstractMetavarContext.instantiateLevelMVars lvl
@[inline] def visit (f : Expr → M σ Expr) (e : Expr) : M σ Expr :=
if !e.hasMVar then pure e else checkCache e f
@[inline] def getMCtx : M σ σ :=
do s ← get; pure s.state
@[inline] def modifyCtx (f : σ → σ) : M σ Unit :=
modify $ fun s => { state := f s.state, .. s }
/--
Auxiliary function for `instantiateDelayed`.
`instantiateDelayed main lctx fvars i body` is used to create `fun fvars[0, i) => body`.
It fails if one of variable declarations in `fvars` still contains unassigned metavariables.
Pre: all expressions in `fvars` are `Expr.fvar`, and `lctx` contains their declarations. -/
@[specialize] def instantiateDelayedAux (main : Expr → M σ Expr) (lctx : LocalContext) (fvars : Array Expr) : Nat → Expr → M σ (Option Expr)
| 0, b => pure b
| i+1, b => do
let fvar := fvars.get! i;
match lctx.findFVar fvar with
| none => panic! "unknown free variable"
| some (LocalDecl.cdecl _ _ n ty bi) => do
ty ← visit main ty;
if ty.hasMVar then pure none
else instantiateDelayedAux i (Expr.lam n bi (ty.abstractRange i fvars) b)
| some (LocalDecl.ldecl _ _ n ty val) => do
ty ← visit main ty;
if ty.hasMVar then pure none
else do
val ← visit main val;
if val.hasMVar then pure none
else
let ty := ty.abstractRange i fvars;
let val := val.abstractRange i fvars;
instantiateDelayedAux i (Expr.letE n ty val b)
/-- Try to instantiate a delayed assignment. Return `none` (i.e., fail) if assignment still contains variables. -/
@[inline] def instantiateDelayed (main : Expr → M σ Expr) (mvarId : Name) : DelayedMetavarAssignment → M σ (Option Expr)
| { lctx := lctx, fvars := fvars, val := val } => do
newVal ← visit main val;
let fail : M σ (Option Expr) := do {
/- Join point for updating delayed assignment and failing -/
modifyCtx $ fun mctx => assignDelayed mctx mvarId lctx fvars newVal;
pure none
};
if newVal.hasMVar then fail
else do
/- Create `fun fvars => newVal`.
It fails if there is a one of the variable declarations in `fvars` still contain metavariables. -/
newE ← instantiateDelayedAux main lctx fvars fvars.size (newVal.abstract fvars);
match newE with
| none => fail
| some newE => do
/- Succeeded. Thus, replace delayed assignment with a regular assignment. -/
modifyCtx $ fun mctx => assignExpr (eraseDelayed mctx mvarId) mvarId newE;
pure (some newE)
/-- instantiateExprMVars main function -/
partial def main : Expr → M σ Expr
| e@(Expr.proj _ _ s) => do s ← visit main s; pure (e.updateProj! s)
| e@(Expr.forallE _ _ d b) => do d ← visit main d; b ← visit main b; pure (e.updateForallE! d b)
| e@(Expr.lam _ _ d b) => do d ← visit main d; b ← visit main b; pure (e.updateLambdaE! d b)
| e@(Expr.letE _ t v b) => do t ← visit main t; v ← visit main v; b ← visit main b; pure (e.updateLet! t v b)
| e@(Expr.const _ lvls) => do lvls ← lvls.mapM instantiateLevelMVars; pure (e.updateConst! lvls)
| e@(Expr.sort lvl) => do lvl ← instantiateLevelMVars lvl; pure (e.updateSort! lvl)
| e@(Expr.mdata _ b) => do b ← visit main b; pure (e.updateMData! b)
| e@(Expr.app _ _) => e.withAppRev $ fun f revArgs => do
let wasMVar := f.isMVar;
f ← visit main f;
if wasMVar && f.isLambda then
-- Some of the arguments in revArgs are irrelevant after we beta reduce.
visit main (f.betaRev revArgs)
else do
revArgs ← revArgs.mapM (visit main);
pure (mkAppRev f revArgs)
| e@(Expr.mvar mvarId) => checkCache e $ fun e => do
mctx ← getMCtx;
match getExprAssignment mctx mvarId with
| some newE => do
newE' ← visit main newE;
modifyCtx $ fun mctx => assignExpr mctx mvarId newE';
pure newE'
| none =>
/- A delayed assignment can be transformed into a regular assignment
as soon as all metavariables occurring in the assigned value have
been assigned. -/
match getDelayedAssignment mctx mvarId with
| some d => do
newE ← instantiateDelayed main mvarId d;
pure $ newE.getD e
| none => pure e
| e => pure e
end InstantiateExprMVars
def instantiateMVars (e : Expr) : StateM σ Expr :=
if !e.hasMVar then pure e
else WithHashMapCache.toState $ InstantiateExprMVars.main e
namespace DependsOn
abbrev M := StateM ExprSet
@[inline] def visit (main : Expr → M Bool) (e : Expr) : M Bool :=
if !e.hasMVar && !e.hasFVar then
pure false
else do
s ← get;
if s.contains e then
pure false
else do
modify $ fun s => s.insert e;
main e
@[specialize] partial def dep (mctx : σ) (p : Name → Bool) : Expr → M Bool
| e@(Expr.proj _ _ s) => visit dep s
| e@(Expr.forallE _ _ d b) => visit dep d <||> visit dep b
| e@(Expr.lam _ _ d b) => visit dep d <||> visit dep b
| e@(Expr.letE _ t v b) => visit dep t <||> visit dep v <||> visit dep b
| e@(Expr.mdata _ b) => visit dep b
| e@(Expr.app f a) => visit dep a <||> if f.isApp then dep f else visit dep f
| e@(Expr.mvar mvarId) =>
match getExprAssignment mctx mvarId with
| some a => visit dep a
| none =>
let lctx := (getDecl mctx mvarId).lctx;
pure $ lctx.any $ fun decl => p decl.name
| e@(Expr.fvar fvarId) => pure $ p fvarId
| e => pure false
@[inline] partial def main (mctx : σ) (p : Name → Bool) (e : Expr) : M Bool :=
if !e.hasFVar && !e.hasMVar then pure false else dep mctx p e
end DependsOn
/--
Return `true` iff `e` depends on a free variable `x` s.t. `p x` is `true`.
For each metavariable `?m` occurring in `x`
1- If `?m := t`, then we visit `t` looking for `x`
2- If `?m` is unassigned, then we consider the worst case and check whether `x` is in the local context of `?m`.
This case is a "may dependency". That is, we may assign a term `t` to `?m` s.t. `t` contains `x`. -/
@[inline] def exprDependsOn (mctx : σ) (p : Name → Bool) (e : Expr) : Bool :=
(DependsOn.main mctx p e).run' {}
/--
Similar to `exprDependsOn`, but checks the expressions in the given local declaration
depends on a free variable `x` s.t. `p x` is `true`. -/
@[inline] def localDeclDependsOn (mctx : σ) (p : Name → Bool) : LocalDecl → Bool
| LocalDecl.cdecl _ _ _ type _ => exprDependsOn mctx p type
| LocalDecl.ldecl _ _ _ type value => (DependsOn.main mctx p type <||> DependsOn.main mctx p value).run' {}
inductive MkBindingException
| revertFailure (lctx : LocalContext) (toRevert : Array Expr) (decl : LocalDecl)
| readOnlyMVar (mvarId : Name)
| mkAuxMVarNotSupported
namespace MkBindingException
def toStr : MkBindingException → String
| revertFailure lctx toRevert decl =>
"failed to revert "
++ toString (toRevert.map (fun x => "'" ++ toString (lctx.findFVar x).get!.userName ++ "'"))
++ ", '" ++ toString decl.userName ++ "' depends on them, and it is an auxiliary declaration created by the elaborator"
++ " (possible solution: use tactic 'clear' to remove '" ++ toString decl.userName ++ "' from local context)"
| readOnlyMVar _ => "failed to create binding due to read only metavariable"
| mkAuxMVarNotSupported => "auxiliary metavariables are not supported"
instance : HasToString MkBindingException := ⟨toStr⟩
end MkBindingException
namespace MkBinding
/--
`MkBinding` and `elimMVarDepsAux` are mutually recursive, but `cache` is only used at `elimMVarDepsAux`.
We use a single state object for convenience.
We have a `NameGenerator` because we need to generate fresh auxiliary metavariables.
-/
structure MkBindingState (σ : Type) :=
(mctx : σ)
(ngen : NameGenerator)
(cache : HashMap Expr Expr := {}) --
abbrev M (σ : Type) := EStateM MkBindingException (MkBindingState σ)
instance (σ) : MonadHashMapCacheAdapter Expr Expr (M σ) :=
{ getCache := do s ← get; pure s.cache,
modifyCache := fun f => modify $ fun s => { cache := f s.cache, .. s } }
/-- Similar to `Expr.abstractRange`, but handles metavariables correctly.
It uses `elimMVarDeps` to ensure `e` and the type of the free variables `xs` do not
contain a metavariable `?m` s.t. local context of `?m` contains a free variable in `xs`.
`elimMVarDeps` is defined later in this file. -/
@[inline] def abstractRange (elimMVarDeps : Array Expr → Expr → M σ Expr) (lctx : LocalContext) (xs : Array Expr) (i : Nat) (e : Expr) : M σ Expr :=
do e ← elimMVarDeps xs e;
pure (e.abstractRange i xs)
/-- Similar to `LocalContext.mkBinding`, but handles metavariables correctly. -/
@[specialize] def mkBinding (isLambda : Bool) (elimMVarDeps : Array Expr → Expr → M σ Expr)
(lctx : LocalContext) (xs : Array Expr) (e : Expr) : M σ Expr :=
do e ← abstractRange elimMVarDeps lctx xs xs.size e;
xs.size.foldRevM
(fun i e =>
let x := xs.get! i;
match lctx.findFVar x with
| some (LocalDecl.cdecl _ _ n type bi) => do
type ← abstractRange elimMVarDeps lctx xs i type;
if isLambda then
pure $ Expr.lam n bi type e
else
pure $ Expr.forallE n bi type e
| some (LocalDecl.ldecl _ _ n type value) => do
type ← abstractRange elimMVarDeps lctx xs i type;
value ← abstractRange elimMVarDeps lctx xs i value;
pure $ Expr.letE n type value e
| none => panic! "unknown free variable")
e
@[inline] def mkLambda (elimMVarDeps : Array Expr → Expr → M σ Expr) (lctx : LocalContext) (xs : Array Expr) (b : Expr) : M σ Expr :=
mkBinding true elimMVarDeps lctx xs b
@[inline] def mkForall (elimMVarDeps : Array Expr → Expr → M σ Expr) (lctx : LocalContext) (xs : Array Expr) (b : Expr) : M σ Expr :=
mkBinding false elimMVarDeps lctx xs b
/-- Return the local declaration of the free variable `x` in `xs` with the smallest index -/
def getLocalDeclWithSmallestIdx (lctx : LocalContext) (xs : Array Expr) : LocalDecl :=
let d : LocalDecl := (lctx.findFVar $ xs.get! 0).get!;
xs.foldlFrom
(fun d x =>
let decl := (lctx.findFVar x).get!;
if decl.index < d.index then decl else d)
d 1
/-- Given `toRevert` an array of free variables s.t. `lctx` contains their declarations,
return a new array of free variables that contains `toRevert` and all free variables
in `lctx` that may depend on `toRevert`.
Remark: the result is sorted by `LocalDecl` indices. -/
def collectDeps (mctx : σ) (lctx : LocalContext) (toRevert : Array Expr) : Except MkBindingException (Array Expr) :=
if toRevert.size == 0 then pure toRevert
else
let minDecl := getLocalDeclWithSmallestIdx lctx toRevert;
lctx.foldlFromM
(fun newToRevert decl =>
if toRevert.any (fun x => decl.name == x.fvarId!) then
pure (newToRevert.push decl.toExpr)
else if localDeclDependsOn mctx (fun fvarId => newToRevert.any $ fun x => x.fvarId! == fvarId) decl then
if decl.binderInfo.isAuxDecl then
throw (MkBindingException.revertFailure lctx toRevert decl)
else
pure (newToRevert.push decl.toExpr)
else
pure newToRevert)
(Array.mkEmpty toRevert.size)
minDecl
/-- Create a new `LocalContext` by removing the free variables in `toRevert` from `lctx`.
We use this function when we create auxiliary metavariables at `elimMVarDepsAux`. -/
def reduceLocalContext (lctx : LocalContext) (toRevert : Array Expr) : LocalContext :=
toRevert.foldr
(fun x lctx => lctx.erase x.fvarId!)
lctx
@[inline] def visit (f : Expr → M σ Expr) (e : Expr) : M σ Expr :=
if !e.hasMVar then pure e else checkCache e f
@[inline] def getMCtx : M σ σ :=
do s ← get; pure s.mctx
@[inline] def mkFreshId : M σ Name :=
modifyGet $ fun s => (s.ngen.curr, { ngen := s.ngen.next, .. s})
/-- Return free variables in `xs` that are in the local context `lctx` -/
def getInScope (lctx : LocalContext) (xs : Array Expr) : Array Expr :=
xs.foldl
(fun scope x =>
if lctx.contains x.fvarId! then
scope.push x
else
scope)
#[]
/-- Execute `x` with an empty cache, and then restore the original cache. -/
@[inline] def withFreshCache {α} (x : M σ α) : M σ α :=
do cache ← modifyGet $ fun s => (s.cache, { cache := {}, .. s });
a ← x;
modify $ fun s => { cache := cache, .. s };
pure a
@[inline] def mkForallAux (elimMVarDepsAux : Array Expr → Expr → M σ Expr) (lctx : LocalContext) (xs : Array Expr) (b : Expr) : M σ Expr :=
mkForall
(fun xs e =>
if !e.hasMVar then
pure e
else
-- The cached results at `elimMVarDepsAux` depend on `xs`. So, we must reset the cache.
withFreshCache $ elimMVarDepsAux xs e)
lctx xs b
/-- Create an application `mvar ys` where `ys` are the free variables `xs` which are not let-declarations.
All free variables in `xs` are in the context `lctx`. -/
def mkMVarApp (lctx : LocalContext) (mvar : Expr) (xs : Array Expr) : Expr :=
xs.foldl (fun e x => if (lctx.findFVar x).get!.isLet then e else Expr.app e x) mvar
partial def elimMVarDepsAux : Array Expr → Expr → M σ Expr
| xs, e@(Expr.proj _ _ s) => do s ← visit (elimMVarDepsAux xs) s; pure (e.updateProj! s)
| xs, e@(Expr.forallE _ _ d b) => do d ← visit (elimMVarDepsAux xs) d; b ← visit (elimMVarDepsAux xs) b; pure (e.updateForallE! d b)
| xs, e@(Expr.lam _ _ d b) => do d ← visit (elimMVarDepsAux xs) d; b ← visit (elimMVarDepsAux xs) b; pure (e.updateLambdaE! d b)
| xs, e@(Expr.letE _ t v b) => do t ← visit (elimMVarDepsAux xs) t; v ← visit (elimMVarDepsAux xs) v; b ← visit (elimMVarDepsAux xs) b; pure (e.updateLet! t v b)
| xs, e@(Expr.mdata _ b) => do b ← visit (elimMVarDepsAux xs) b; pure (e.updateMData! b)
| xs, e@(Expr.app _ _) => e.withAppRev $ fun f revArgs => do
f ← visit (elimMVarDepsAux xs) f;
revArgs ← revArgs.mapM (visit (elimMVarDepsAux xs));
pure (mkAppRev f revArgs)
| xs, e@(Expr.mvar mvarId) => do
mctx ← getMCtx;
match getExprAssignment mctx mvarId with
| some a => visit (elimMVarDepsAux xs) a
| none =>
let mvarDecl := getDecl mctx mvarId;
let mvarLCtx := mvarDecl.lctx;
let toRevert := getInScope mvarLCtx xs;
if toRevert.size == 0 then
pure e
else if isReadOnlyExprMVar mctx mvarId then
throw $ MkBindingException.readOnlyMVar mvarId
else if !auxMVarSupport σ then
throw MkBindingException.mkAuxMVarNotSupported
else
match collectDeps mctx mvarLCtx toRevert with
| Except.error ex => throw ex
| Except.ok toRevert => do
let newMVarLCtx := reduceLocalContext mvarLCtx toRevert;
newMVarType ← mkForallAux (fun xs e => elimMVarDepsAux xs e) mvarLCtx toRevert mvarDecl.type;
mctx ← getMCtx;
newMVarId ← mkFreshId;
let mctx := mkAuxMVar mctx newMVarId newMVarLCtx newMVarType mvarDecl.synthetic;
modify $ fun s => { mctx := mctx, .. s };
let newMVar := Expr.mvar newMVarId;
let result := mkMVarApp mvarLCtx newMVar toRevert;
if mvarDecl.synthetic then
modify (fun s => { mctx := assignDelayed s.mctx newMVarId mvarLCtx toRevert e, .. s })
else
modify (fun s => { mctx := assignExpr s.mctx mvarId result, .. s });
pure result
| xs, e => pure e
partial def elimMVarDeps (xs : Array Expr) (e : Expr) : M σ Expr :=
if !e.hasMVar then
pure e
else
withFreshCache $ elimMVarDepsAux xs e
end MkBinding
def mkBinding (isLambda : Bool) (mctx : σ) (ngen : NameGenerator) (lctx : LocalContext) (xs : Array Expr) (e : Expr) : Except MkBindingException (σ × NameGenerator × Expr) :=
match (MkBinding.mkBinding isLambda MkBinding.elimMVarDeps lctx xs e).run { mctx := mctx, ngen := ngen } with
| EStateM.Result.ok e s => Except.ok (s.mctx, s.ngen, e)
| EStateM.Result.error err _ => Except.error err
@[inline] def mkLambda (mctx : σ) (ngen : NameGenerator) (lctx : LocalContext) (xs : Array Expr) (e : Expr) : Except MkBindingException (σ × NameGenerator × Expr) :=
mkBinding true mctx ngen lctx xs e
@[inline] def mkForall (mctx : σ) (ngen : NameGenerator) (lctx : LocalContext) (xs : Array Expr) (e : Expr) : Except MkBindingException (σ × NameGenerator × Expr) :=
mkBinding false mctx ngen lctx xs e
end AbstractMetavarContext
export AbstractMetavarContext (MkBindingException)
end Lean

493
library/Init/Lean/MetavarContext.lean
View file

@ -4,11 +4,36 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Lean.AbstractMetavarContext
import Init.Control.Reader
import Init.Control.Conditional
import Init.Data.Option
import Init.Data.List
import Init.Data.Nat
import Init.Lean.LocalContext
import Init.Lean.MonadCache
import Init.Lean.NameGenerator
namespace Lean
structure MetavarDecl :=
(userName : Name := Name.anonymous)
(lctx : LocalContext)
(type : Expr)
(depth : Nat)
(synthetic : Bool)
namespace MetavarDecl
instance : Inhabited MetavarDecl := ⟨{ lctx := arbitrary _, type := arbitrary _, depth := 0, synthetic := false }⟩
end MetavarDecl
structure DelayedMetavarAssignment :=
(lctx : LocalContext)
(fvars : Array Expr)
(val : Expr)
structure MetavarContext :=
(depth : Nat := 0)
(lDepth : PersistentHashMap Name Nat := {})
(decls : PersistentHashMap Name MetavarDecl := {})
(lAssignment : PersistentHashMap Name Level := {})
(eAssignment : PersistentHashMap Name Expr := {})
@ -26,8 +51,14 @@ fun _ => {}
It is used to implement actions in the monads `Elab` and `Tactic`.
It should not be used directly since the argument `(mvarId : Name)` is assumed to be "unique". -/
@[export lean_metavar_ctx_mk_decl]
def mkDecl (m : MetavarContext) (mvarId : Name) (userName : Name) (lctx : LocalContext) (type : Expr) (synthetic : Bool := false) : MetavarContext :=
{ decls := m.decls.insert mvarId { userName := userName, lctx := lctx, type := type, synthetic := synthetic }, .. m }
def mkDecl (mctx : MetavarContext) (mvarId : Name) (userName : Name) (lctx : LocalContext) (type : Expr) (synthetic : Bool := false) : MetavarContext :=
{ decls := mctx.decls.insert mvarId {
userName := userName,
lctx := lctx,
type := type,
depth := mctx.depth,
synthetic := synthetic },
.. mctx }
@[export lean_metavar_ctx_find_decl]
def findDecl (m : MetavarContext) (mvarId : Name) : Option MetavarDecl :=
@ -78,44 +109,436 @@ m.dAssignment.contains mvarId
def eraseDelayed (m : MetavarContext) (mvarId : Name) : MetavarContext :=
{ dAssignment := m.dAssignment.erase mvarId, .. m }
/- Remark: the following instance assumes all metavariables can be updated. -/
instance metavarContextIsAbstractMetavarContext : AbstractMetavarContext MetavarContext :=
{ empty := {},
isReadOnlyLevelMVar := fun _ _ => false,
getLevelAssignment := MetavarContext.getLevelAssignment,
assignLevel := MetavarContext.assignLevel,
isReadOnlyExprMVar := fun _ _ => false,
getExprAssignment := MetavarContext.getExprAssignment,
assignExpr := MetavarContext.assignExpr,
getDecl := MetavarContext.getDecl,
assignDelayed := MetavarContext.assignDelayed,
getDelayedAssignment := MetavarContext.getDelayedAssignment,
eraseDelayed := MetavarContext.eraseDelayed,
auxMVarSupport := true,
mkAuxMVar := fun mctx mvarId lctx type synthetic => MetavarContext.mkDecl mctx mvarId Name.anonymous lctx type synthetic
}
def isLevelAssignable (mctx : MetavarContext) (mvarId : Name) : Bool :=
match mctx.lDepth.find mvarId with
| some d => d == mctx.depth
| _ => panic! "unknown universe metavariable"
/-- Return `true` iff `lvl` contains assigned level metavariables -/
@[inline] def hasAssignedLevelMVar (m : MetavarContext) (lvl : Level) : Bool :=
AbstractMetavarContext.hasAssignedLevelMVar m lvl
def isExprAssignable (mctx : MetavarContext) (mvarId : Name) : Bool :=
let decl := mctx.getDecl mvarId;
decl.depth == mctx.depth
/-- Return `true` iff `e` contains assigned (level/expr) metavariables -/
@[inline] def hasAssignedMVar (m : MetavarContext) (e : Expr) : Bool :=
AbstractMetavarContext.hasAssignedMVar m e
/-- Return true iff the given level contains an assigned metavariable. -/
def hasAssignedLevelMVar (mctx : MetavarContext) : Level → Bool
| Level.succ lvl => lvl.hasMVar && hasAssignedLevelMVar lvl
| Level.max lvl₁ lvl₂ => (lvl₁.hasMVar && hasAssignedLevelMVar lvl₁) || (lvl₂.hasMVar && hasAssignedLevelMVar lvl₂)
| Level.imax lvl₁ lvl₂ => (lvl₁.hasMVar && hasAssignedLevelMVar lvl₁) || (lvl₂.hasMVar && hasAssignedLevelMVar lvl₂)
| Level.mvar mvarId => mctx.isLevelAssigned mvarId
| Level.zero => false
| Level.param _ => false
@[inline] def instantiateLevelMVars (m : MetavarContext) (lvl : Level) : Level × MetavarContext :=
AbstractMetavarContext.instantiateLevelMVars lvl m
/-- Return `true` iff expression contains assigned (level/expr) metavariables -/
def hasAssignedMVar (mctx : MetavarContext) : Expr → Bool
| Expr.const _ lvls => lvls.any (hasAssignedLevelMVar mctx)
| Expr.sort lvl => hasAssignedLevelMVar mctx lvl
| Expr.app f a => (f.hasMVar && hasAssignedMVar f) || (a.hasMVar && hasAssignedMVar a)
| Expr.letE _ t v b => (t.hasMVar && hasAssignedMVar t) || (v.hasMVar && hasAssignedMVar v) || (b.hasMVar && hasAssignedMVar b)
| Expr.forallE _ _ d b => (d.hasMVar && hasAssignedMVar d) || (b.hasMVar && hasAssignedMVar b)
| Expr.lam _ _ d b => (d.hasMVar && hasAssignedMVar d) || (b.hasMVar && hasAssignedMVar b)
| Expr.fvar _ => false
| Expr.bvar _ => false
| Expr.lit _ => false
| Expr.mdata _ e => e.hasMVar && hasAssignedMVar e
| Expr.proj _ _ e => e.hasMVar && hasAssignedMVar e
| Expr.mvar mvarId => mctx.isExprAssigned mvarId
@[inline] def instantiateMVars (m : MetavarContext) (e : Expr) : Expr × MetavarContext :=
AbstractMetavarContext.instantiateMVars e m
/-- Return true iff the given level contains a metavariable that can be assigned. -/
def hasAssignableLevelMVar (mctx : MetavarContext) : Level → Bool
| Level.succ lvl => lvl.hasMVar && hasAssignableLevelMVar lvl
| Level.max lvl₁ lvl₂ => (lvl₁.hasMVar && hasAssignableLevelMVar lvl₁) || (lvl₂.hasMVar && hasAssignableLevelMVar lvl₂)
| Level.imax lvl₁ lvl₂ => (lvl₁.hasMVar && hasAssignableLevelMVar lvl₁) || (lvl₂.hasMVar && hasAssignableLevelMVar lvl₂)
| Level.mvar mvarId => mctx.isLevelAssignable mvarId
| Level.zero => false
| Level.param _ => false
@[inline] def mkLambda (m : MetavarContext) (ngen : NameGenerator) (lctx : LocalContext) (xs : Array Expr) (e : Expr)
: Except MkBindingException (MetavarContext × NameGenerator × Expr) :=
AbstractMetavarContext.mkLambda m ngen lctx xs e
private partial def instantiateLevelMVarsAux : Level → StateM MetavarContext Level
| lvl@(Level.succ lvl₁) => do lvl₁ ← instantiateLevelMVarsAux lvl₁; pure (Level.updateSucc! lvl lvl₁)
| lvl@(Level.max lvl₁ lvl₂) => do lvl₁ ← instantiateLevelMVarsAux lvl₁; lvl₂ ← instantiateLevelMVarsAux lvl₂; pure (Level.updateMax! lvl lvl₁ lvl₂)
| lvl@(Level.imax lvl₁ lvl₂) => do lvl₁ ← instantiateLevelMVarsAux lvl₁; lvl₂ ← instantiateLevelMVarsAux lvl₂; pure (Level.updateIMax! lvl lvl₁ lvl₂)
| lvl@(Level.mvar mvarId) => do
mctx ← get;
match getLevelAssignment mctx mvarId with
| some newLvl =>
if !newLvl.hasMVar then pure newLvl
else do
newLvl' ← instantiateLevelMVarsAux newLvl;
modify $ fun mctx => mctx.assignLevel mvarId newLvl';
pure newLvl'
| none => pure lvl
| lvl => pure lvl
@[inline] def mkForall (m : MetavarContext) (ngen : NameGenerator) (lctx : LocalContext) (xs : Array Expr) (e : Expr)
: Except MkBindingException (MetavarContext × NameGenerator × Expr) :=
AbstractMetavarContext.mkForall m ngen lctx xs e
namespace InstantiateExprMVars
private abbrev M := StateM (WithHashMapCache Expr Expr MetavarContext)
@[inline] private def instantiateLevelMVars (lvl : Level) : M Level :=
WithHashMapCache.fromState $ instantiateLevelMVarsAux lvl
@[inline] private def visit (f : Expr → M Expr) (e : Expr) : M Expr :=
if !e.hasMVar then pure e else checkCache e f
@[inline] private def getMCtx : M MetavarContext :=
do s ← get; pure s.state
@[inline] private def modifyCtx (f : MetavarContext → MetavarContext) : M Unit :=
modify $ fun s => { state := f s.state, .. s }
/--
Auxiliary function for `instantiateDelayed`.
`instantiateDelayed main lctx fvars i body` is used to create `fun fvars[0, i) => body`.
It fails if one of variable declarations in `fvars` still contains unassigned metavariables.
Pre: all expressions in `fvars` are `Expr.fvar`, and `lctx` contains their declarations. -/
@[specialize] private def instantiateDelayedAux (main : Expr → M Expr) (lctx : LocalContext) (fvars : Array Expr) : Nat → Expr → M (Option Expr)
| 0, b => pure b
| i+1, b => do
let fvar := fvars.get! i;
match lctx.findFVar fvar with
| none => panic! "unknown free variable"
| some (LocalDecl.cdecl _ _ n ty bi) => do
ty ← visit main ty;
if ty.hasMVar then pure none
else instantiateDelayedAux i (Expr.lam n bi (ty.abstractRange i fvars) b)
| some (LocalDecl.ldecl _ _ n ty val) => do
ty ← visit main ty;
if ty.hasMVar then pure none
else do
val ← visit main val;
if val.hasMVar then pure none
else
let ty := ty.abstractRange i fvars;
let val := val.abstractRange i fvars;
instantiateDelayedAux i (Expr.letE n ty val b)
/-- Try to instantiate a delayed assignment. Return `none` (i.e., fail) if assignment still contains variables. -/
@[inline] private def instantiateDelayed (main : Expr → M Expr) (mvarId : Name) : DelayedMetavarAssignment → M (Option Expr)
| { lctx := lctx, fvars := fvars, val := val } => do
newVal ← visit main val;
let fail : M (Option Expr) := do {
/- Join point for updating delayed assignment and failing -/
modifyCtx $ fun mctx => assignDelayed mctx mvarId lctx fvars newVal;
pure none
};
if newVal.hasMVar then fail
else do
/- Create `fun fvars => newVal`.
It fails if there is a one of the variable declarations in `fvars` still contain metavariables. -/
newE ← instantiateDelayedAux main lctx fvars fvars.size (newVal.abstract fvars);
match newE with
| none => fail
| some newE => do
/- Succeeded. Thus, replace delayed assignment with a regular assignment. -/
modifyCtx $ fun mctx => assignExpr (eraseDelayed mctx mvarId) mvarId newE;
pure (some newE)
/-- instantiateExprMVars main function -/
partial def main : Expr → M Expr
| e@(Expr.proj _ _ s) => do s ← visit main s; pure (e.updateProj! s)
| e@(Expr.forallE _ _ d b) => do d ← visit main d; b ← visit main b; pure (e.updateForallE! d b)
| e@(Expr.lam _ _ d b) => do d ← visit main d; b ← visit main b; pure (e.updateLambdaE! d b)
| e@(Expr.letE _ t v b) => do t ← visit main t; v ← visit main v; b ← visit main b; pure (e.updateLet! t v b)
| e@(Expr.const _ lvls) => do lvls ← lvls.mapM instantiateLevelMVars; pure (e.updateConst! lvls)
| e@(Expr.sort lvl) => do lvl ← instantiateLevelMVars lvl; pure (e.updateSort! lvl)
| e@(Expr.mdata _ b) => do b ← visit main b; pure (e.updateMData! b)
| e@(Expr.app _ _) => e.withAppRev $ fun f revArgs => do
let wasMVar := f.isMVar;
f ← visit main f;
if wasMVar && f.isLambda then
-- Some of the arguments in revArgs are irrelevant after we beta reduce.
visit main (f.betaRev revArgs)
else do
revArgs ← revArgs.mapM (visit main);
pure (mkAppRev f revArgs)
| e@(Expr.mvar mvarId) => checkCache e $ fun e => do
mctx ← getMCtx;
match mctx.getExprAssignment mvarId with
| some newE => do
newE' ← visit main newE;
modifyCtx $ fun mctx => mctx.assignExpr mvarId newE';
pure newE'
| none =>
/- A delayed assignment can be transformed into a regular assignment
as soon as all metavariables occurring in the assigned value have
been assigned. -/
match mctx.getDelayedAssignment mvarId with
| some d => do
newE ← instantiateDelayed main mvarId d;
pure $ newE.getD e
| none => pure e
| e => pure e
end InstantiateExprMVars
def instantiateMVars (mctx : MetavarContext) (e : Expr) : Expr × MetavarContext :=
if !e.hasMVar then (e, mctx)
else (WithHashMapCache.toState $ InstantiateExprMVars.main e).run mctx
namespace DependsOn
private abbrev M := StateM ExprSet
@[inline] private def visit (main : Expr → M Bool) (e : Expr) : M Bool :=
if !e.hasMVar && !e.hasFVar then
pure false
else do
s ← get;
if s.contains e then
pure false
else do
modify $ fun s => s.insert e;
main e
@[specialize] private partial def dep (mctx : MetavarContext) (p : Name → Bool) : Expr → M Bool
| e@(Expr.proj _ _ s) => visit dep s
| e@(Expr.forallE _ _ d b) => visit dep d <||> visit dep b
| e@(Expr.lam _ _ d b) => visit dep d <||> visit dep b
| e@(Expr.letE _ t v b) => visit dep t <||> visit dep v <||> visit dep b
| e@(Expr.mdata _ b) => visit dep b
| e@(Expr.app f a) => visit dep a <||> if f.isApp then dep f else visit dep f
| e@(Expr.mvar mvarId) =>
match mctx.getExprAssignment mvarId with
| some a => visit dep a
| none =>
let lctx := (mctx.getDecl mvarId).lctx;
pure $ lctx.any $ fun decl => p decl.name
| e@(Expr.fvar fvarId) => pure $ p fvarId
| e => pure false
@[inline] partial def main (mctx : MetavarContext) (p : Name → Bool) (e : Expr) : M Bool :=
if !e.hasFVar && !e.hasMVar then pure false else dep mctx p e
end DependsOn
/--
Return `true` iff `e` depends on a free variable `x` s.t. `p x` is `true`.
For each metavariable `?m` occurring in `x`
1- If `?m := t`, then we visit `t` looking for `x`
2- If `?m` is unassigned, then we consider the worst case and check whether `x` is in the local context of `?m`.
This case is a "may dependency". That is, we may assign a term `t` to `?m` s.t. `t` contains `x`. -/
@[inline] def exprDependsOn (mctx : MetavarContext) (p : Name → Bool) (e : Expr) : Bool :=
(DependsOn.main mctx p e).run' {}
/--
Similar to `exprDependsOn`, but checks the expressions in the given local declaration
depends on a free variable `x` s.t. `p x` is `true`. -/
@[inline] def localDeclDependsOn (mctx : MetavarContext) (p : Name → Bool) : LocalDecl → Bool
| LocalDecl.cdecl _ _ _ type _ => exprDependsOn mctx p type
| LocalDecl.ldecl _ _ _ type value => (DependsOn.main mctx p type <||> DependsOn.main mctx p value).run' {}
inductive MkBindingException
| revertFailure (lctx : LocalContext) (toRevert : Array Expr) (decl : LocalDecl)
| readOnlyMVar (mvarId : Name)
| mkAuxMVarNotSupported
namespace MkBindingException
def toStr : MkBindingException → String
| revertFailure lctx toRevert decl =>
"failed to revert "
++ toString (toRevert.map (fun x => "'" ++ toString (lctx.findFVar x).get!.userName ++ "'"))
++ ", '" ++ toString decl.userName ++ "' depends on them, and it is an auxiliary declaration created by the elaborator"
++ " (possible solution: use tactic 'clear' to remove '" ++ toString decl.userName ++ "' from local context)"
| readOnlyMVar mvarId => "failed to create binding due to read only metavariable " ++ toString mvarId
| mkAuxMVarNotSupported => "auxiliary metavariables are not supported"
instance : HasToString MkBindingException := ⟨toStr⟩
end MkBindingException
namespace MkBinding
/--
`MkBinding` and `elimMVarDepsAux` are mutually recursive, but `cache` is only used at `elimMVarDepsAux`.
We use a single state object for convenience.
We have a `NameGenerator` because we need to generate fresh auxiliary metavariables.
-/
structure MkBindingState :=
(mctx : MetavarContext)
(ngen : NameGenerator)
(cache : HashMap Expr Expr := {}) --
private abbrev M := EStateM MkBindingException MkBindingState
instance : MonadHashMapCacheAdapter Expr Expr M :=
{ getCache := do s ← get; pure s.cache,
modifyCache := fun f => modify $ fun s => { cache := f s.cache, .. s } }
/-- Similar to `Expr.abstractRange`, but handles metavariables correctly.
It uses `elimMVarDeps` to ensure `e` and the type of the free variables `xs` do not
contain a metavariable `?m` s.t. local context of `?m` contains a free variable in `xs`.
`elimMVarDeps` is defined later in this file. -/
@[inline] private def abstractRange (elimMVarDeps : Array Expr → Expr → M Expr) (lctx : LocalContext) (xs : Array Expr) (i : Nat) (e : Expr) : M Expr :=
do e ← elimMVarDeps xs e;
pure (e.abstractRange i xs)
/-- Similar to `LocalContext.mkBinding`, but handles metavariables correctly. -/
@[specialize] def mkBinding (isLambda : Bool) (elimMVarDeps : Array Expr → Expr → M Expr)
(lctx : LocalContext) (xs : Array Expr) (e : Expr) : M Expr :=
do e ← abstractRange elimMVarDeps lctx xs xs.size e;
xs.size.foldRevM
(fun i e =>
let x := xs.get! i;
match lctx.findFVar x with
| some (LocalDecl.cdecl _ _ n type bi) => do
type ← abstractRange elimMVarDeps lctx xs i type;
if isLambda then
pure $ Expr.lam n bi type e
else
pure $ Expr.forallE n bi type e
| some (LocalDecl.ldecl _ _ n type value) => do
type ← abstractRange elimMVarDeps lctx xs i type;
value ← abstractRange elimMVarDeps lctx xs i value;
pure $ Expr.letE n type value e
| none => panic! "unknown free variable")
e
@[inline] private def mkLambda (elimMVarDeps : Array Expr → Expr → M Expr) (lctx : LocalContext) (xs : Array Expr) (b : Expr) : M Expr :=
mkBinding true elimMVarDeps lctx xs b
@[inline] private def mkForall (elimMVarDeps : Array Expr → Expr → M Expr) (lctx : LocalContext) (xs : Array Expr) (b : Expr) : M Expr :=
mkBinding false elimMVarDeps lctx xs b
/-- Return the local declaration of the free variable `x` in `xs` with the smallest index -/
private def getLocalDeclWithSmallestIdx (lctx : LocalContext) (xs : Array Expr) : LocalDecl :=
let d : LocalDecl := (lctx.findFVar $ xs.get! 0).get!;
xs.foldlFrom
(fun d x =>
let decl := (lctx.findFVar x).get!;
if decl.index < d.index then decl else d)
d 1
/-- Given `toRevert` an array of free variables s.t. `lctx` contains their declarations,
return a new array of free variables that contains `toRevert` and all free variables
in `lctx` that may depend on `toRevert`.
Remark: the result is sorted by `LocalDecl` indices. -/
private def collectDeps (mctx : MetavarContext) (lctx : LocalContext) (toRevert : Array Expr) : Except MkBindingException (Array Expr) :=
if toRevert.size == 0 then pure toRevert
else
let minDecl := getLocalDeclWithSmallestIdx lctx toRevert;
lctx.foldlFromM
(fun newToRevert decl =>
if toRevert.any (fun x => decl.name == x.fvarId!) then
pure (newToRevert.push decl.toExpr)
else if localDeclDependsOn mctx (fun fvarId => newToRevert.any $ fun x => x.fvarId! == fvarId) decl then
if decl.binderInfo.isAuxDecl then
throw (MkBindingException.revertFailure lctx toRevert decl)
else
pure (newToRevert.push decl.toExpr)
else
pure newToRevert)
(Array.mkEmpty toRevert.size)
minDecl
/-- Create a new `LocalContext` by removing the free variables in `toRevert` from `lctx`.
We use this function when we create auxiliary metavariables at `elimMVarDepsAux`. -/
private def reduceLocalContext (lctx : LocalContext) (toRevert : Array Expr) : LocalContext :=
toRevert.foldr
(fun x lctx => lctx.erase x.fvarId!)
lctx
@[inline] private def visit (f : Expr → M Expr) (e : Expr) : M Expr :=
if !e.hasMVar then pure e else checkCache e f
@[inline] private def getMCtx : M MetavarContext :=
do s ← get; pure s.mctx
/-- Return free variables in `xs` that are in the local context `lctx` -/
private def getInScope (lctx : LocalContext) (xs : Array Expr) : Array Expr :=
xs.foldl
(fun scope x =>
if lctx.contains x.fvarId! then
scope.push x
else
scope)
#[]
/-- Execute `x` with an empty cache, and then restore the original cache. -/
@[inline] private def withFreshCache {α} (x : M α) : M α :=
do cache ← modifyGet $ fun s => (s.cache, { cache := {}, .. s });
a ← x;
modify $ fun s => { cache := cache, .. s };
pure a
@[inline] private def mkForallAux (elimMVarDepsAux : Array Expr → Expr → M Expr) (lctx : LocalContext) (xs : Array Expr) (b : Expr) : M Expr :=
mkForall
(fun xs e =>
if !e.hasMVar then
pure e
else
-- The cached results at `elimMVarDepsAux` depend on `xs`. So, we must reset the cache.
withFreshCache $ elimMVarDepsAux xs e)
lctx xs b
/-- Create an application `mvar ys` where `ys` are the free variables `xs` which are not let-declarations.
All free variables in `xs` are in the context `lctx`. -/
private def mkMVarApp (lctx : LocalContext) (mvar : Expr) (xs : Array Expr) : Expr :=
xs.foldl (fun e x => if (lctx.findFVar x).get!.isLet then e else Expr.app e x) mvar
private def mkAuxMVar (lctx : LocalContext) (type : Expr) (synthetic : Bool) : M Name :=
do s ← get;
let mvarId := s.ngen.curr;
modify $ fun s => { mctx := s.mctx.mkDecl mvarId Name.anonymous lctx type synthetic, ngen := s.ngen.next, .. s };
pure mvarId
private partial def elimMVarDepsAux : Array Expr → Expr → M Expr
| xs, e@(Expr.proj _ _ s) => do s ← visit (elimMVarDepsAux xs) s; pure (e.updateProj! s)
| xs, e@(Expr.forallE _ _ d b) => do d ← visit (elimMVarDepsAux xs) d; b ← visit (elimMVarDepsAux xs) b; pure (e.updateForallE! d b)
| xs, e@(Expr.lam _ _ d b) => do d ← visit (elimMVarDepsAux xs) d; b ← visit (elimMVarDepsAux xs) b; pure (e.updateLambdaE! d b)
| xs, e@(Expr.letE _ t v b) => do t ← visit (elimMVarDepsAux xs) t; v ← visit (elimMVarDepsAux xs) v; b ← visit (elimMVarDepsAux xs) b; pure (e.updateLet! t v b)
| xs, e@(Expr.mdata _ b) => do b ← visit (elimMVarDepsAux xs) b; pure (e.updateMData! b)
| xs, e@(Expr.app _ _) => e.withAppRev $ fun f revArgs => do
f ← visit (elimMVarDepsAux xs) f;
revArgs ← revArgs.mapM (visit (elimMVarDepsAux xs));
pure (mkAppRev f revArgs)
| xs, e@(Expr.mvar mvarId) => do
mctx ← getMCtx;
match mctx.getExprAssignment mvarId with
| some a => visit (elimMVarDepsAux xs) a
| none =>
let mvarDecl := mctx.getDecl mvarId;
let mvarLCtx := mvarDecl.lctx;
let toRevert := getInScope mvarLCtx xs;
if toRevert.size == 0 then
pure e
else if !mctx.isExprAssignable mvarId then
throw $ MkBindingException.readOnlyMVar mvarId
else
match collectDeps mctx mvarLCtx toRevert with
| Except.error ex => throw ex
| Except.ok toRevert => do
let newMVarLCtx := reduceLocalContext mvarLCtx toRevert;
newMVarType ← mkForallAux (fun xs e => elimMVarDepsAux xs e) mvarLCtx toRevert mvarDecl.type;
newMVarId ← mkAuxMVar newMVarLCtx newMVarType mvarDecl.synthetic;
let newMVar := Expr.mvar newMVarId;
let result := mkMVarApp mvarLCtx newMVar toRevert;
if mvarDecl.synthetic then
modify (fun s => { mctx := assignDelayed s.mctx newMVarId mvarLCtx toRevert e, .. s })
else
modify (fun s => { mctx := assignExpr s.mctx mvarId result, .. s });
pure result
| xs, e => pure e
partial def elimMVarDeps (xs : Array Expr) (e : Expr) : M Expr :=
if !e.hasMVar then
pure e
else
withFreshCache $ elimMVarDepsAux xs e
end MkBinding
def mkBinding (isLambda : Bool) (mctx : MetavarContext) (ngen : NameGenerator) (lctx : LocalContext) (xs : Array Expr) (e : Expr)
: Except MkBindingException (MetavarContext × NameGenerator × Expr) :=
match (MkBinding.mkBinding isLambda MkBinding.elimMVarDeps lctx xs e).run { mctx := mctx, ngen := ngen } with
| EStateM.Result.ok e s => Except.ok (s.mctx, s.ngen, e)
| EStateM.Result.error err _ => Except.error err
@[inline] def mkLambda (mctx : MetavarContext) (ngen : NameGenerator) (lctx : LocalContext) (xs : Array Expr) (e : Expr)
: Except MkBindingException (MetavarContext × NameGenerator × Expr) :=
mkBinding true mctx ngen lctx xs e
@[inline] def mkForall (mctx : MetavarContext) (ngen : NameGenerator) (lctx : LocalContext) (xs : Array Expr) (e : Expr)
: Except MkBindingException (MetavarContext × NameGenerator × Expr) :=
mkBinding false mctx ngen lctx xs e
end MetavarContext
end Lean

132
library/Init/Lean/TmpMetavarContext.lean
View file

@ -1,132 +0,0 @@
/-
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Lean.MetavarContext
namespace Lean
/--
Several procedures (e.g., type class resolution, simplifier) need
to create metavariables that are needed for a short period of time.
For example, when applying a simplification lemma such as
```
forall x, f x x = x
```
to a subterm `t`, we need need to check whether the term
`t` is an instance of the pattern `f ?x ?x`, where `?x` is a fresh metavariable.
That is, we need to find an assignment for `?x` such that `t`
and `f ?x ?x` become definitionally equal. If the assignment is found,
we replace the term `t` with the term assigned to `?x`. After that,
we don't need the metavariable `?x` anymore. We don't want to
use regular metavariables for this operation since we don't want
to waste time declaring them at `MetavarContext`,
then creating the term `f ?x ?x` with the newly created metavariable,
and then performing the matching operation, and finally deleting `?x`.
We avoid this overhead by using temporary metavariables.
`TmpMetavarContext` implements `AbstractMetavarContext` for temporary metavariables.
All temporary metavariables used to solve a particular problem (e.g., matching)
share the same local context (field `mvarLCtx`), the type of a metavariable is stored in the
field `mvarTypes`. The assignments are implemented using small arrays.
We assume the number of temporary metavariables is usually small (< 1000),
and their names store a small integer that is used to read the arrays.
`TmpMetavarContext` also keeps a reference to the main `MetavarContext` used in the elaborator and
tactic framework. -/
structure TmpMetavarContext :=
(mctx : MetavarContext := {})
(mvarLCtx : LocalContext := {})
(mvarTypes : Array Expr := #[])
(lAssignment : Array (Option Level) := #[])
(eAssignment : Array (Option Expr) := #[])
def mkTmpMVarId (idx : Nat) :=
Name.mkNumeral `_tmp idx
def Name.isTmpMVarId : Name → Bool
| Name.mkNumeral `_tmp _ => true
| _ => false
def Name.getTmpMVarIdx : Name → Nat
| Name.mkNumeral _ i => i
| _ => panic! "expected a temporary metavariable name"
def Level.isTmpMVar : Level → Bool
| Level.mvar mvarId => mvarId.isTmpMVarId
| _ => false
def Expr.isTmpMVar : Expr → Bool
| Expr.mvar mvarId => mvarId.isTmpMVarId
| _ => false
/--
Create a temporary metavariable context with the following characteristics:
- It contains `numLevelMVars` temporary `Level` metavariables
- It contains `mvarTypes.size` temporary `Expr` metavariables
- The temporary metavariable `i` has type `mvarTypes[i]`
- All temporary metavariables have local context `mvarLCtx`
`mctx` is the main metavariable context, and it is used to
retrieve regular metavariable information. -/
def mkTmpMetavarContext (mctx : MetavarContext) (mvarLCtx : LocalContext) (mvarTypes : Array Expr) (numLevelMVars : Nat) : TmpMetavarContext :=
{ mctx := mctx,
mvarLCtx := mvarLCtx,
mvarTypes := mvarTypes,
eAssignment := mkArray mvarTypes.size none,
lAssignment := mkArray numLevelMVars none }
namespace TmpMetavarContext
instance : Inhabited TmpMetavarContext := ⟨{}⟩
def getLevelAssignment (m : TmpMetavarContext) (mvarId : Name) : Option Level :=
if mvarId.isTmpMVarId then
m.lAssignment.get! mvarId.getTmpMVarIdx
else
m.mctx.getLevelAssignment mvarId
def assignLevel (m : TmpMetavarContext) (mvarId : Name) (val : Level) : TmpMetavarContext :=
if mvarId.isTmpMVarId then
{ lAssignment := m.lAssignment.set! mvarId.getTmpMVarIdx val, .. m }
else
{ mctx := m.mctx.assignLevel mvarId val, .. }
def getExprAssignment (m : TmpMetavarContext) (mvarId : Name) : Option Expr :=
if mvarId.isTmpMVarId then
m.eAssignment.get! mvarId.getTmpMVarIdx
else
m.mctx.getExprAssignment mvarId
def assignExpr (m : TmpMetavarContext) (mvarId : Name) (val : Expr) : TmpMetavarContext :=
if mvarId.isTmpMVarId then
{ eAssignment := m.eAssignment.set! mvarId.getTmpMVarIdx val, .. m }
else
{ mctx := m.mctx.assignExpr mvarId val, .. }
def getDecl (m : TmpMetavarContext) (mvarId : Name) : MetavarDecl :=
if mvarId.isTmpMVarId then
{ userName := Name.anonymous, lctx := m.mvarLCtx, type := m.mvarTypes.get! mvarId.getTmpMVarIdx, synthetic := false }
else
m.mctx.getDecl mvarId
instance isAbstractMetavarContext : AbstractMetavarContext TmpMetavarContext :=
{ empty := {},
isReadOnlyLevelMVar := fun _ mvarId => !mvarId.isTmpMVarId,
getLevelAssignment := TmpMetavarContext.getLevelAssignment,
assignLevel := TmpMetavarContext.assignLevel,
isReadOnlyExprMVar := fun _ mvarId => !mvarId.isTmpMVarId,
getExprAssignment := TmpMetavarContext.getExprAssignment,
assignExpr := TmpMetavarContext.assignExpr,
getDecl := TmpMetavarContext.getDecl,
-- TmpMetavarContext does not support delayed assignments or the creation of auxiliary metavariables.
auxMVarSupport := false,
mkAuxMVar := fun _ _ _ _ _ => panic! "TmpMetavarContex does not support the creation of auxiliary metavariables",
assignDelayed := fun _ _ _ _ _ => panic! "TmpMetavarContex does not support delayed assignments",
eraseDelayed := fun _ _ => panic! "TmpMetavarContex does not support delayed assignments",
getDelayedAssignment := fun _ _ => none }
end TmpMetavarContext
end Lean

3
library/Init/Lean/TypeUtil.lean
View file

@ -7,13 +7,14 @@ prelude
import Init.Control.Reader
import Init.Lean.NameGenerator
import Init.Lean.Environment
import Init.Lean.AbstractMetavarContext
import Init.Lean.Trace
import Init.Lean.InductiveUtil
import Init.Lean.QuotUtil
import Init.Lean.AuxRecursor
import Init.Lean.ProjFns
#exit
/-
This module provides three (mutually dependent) goodies:
1- Weak head normal form computation with support for metavariables and transparency modes.