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

feat: add renameMVar and improve forallMetaTelescopeReducingAux

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-19 15:48:42 -08:00
parent 0d25c5f55c
commit b577ff2073
1 changed files with 12 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/Init/Lean/Meta/Basic.lean
View file

@ -314,6 +314,9 @@ match mctx.findLevelDepth? mvarId with
| some depth => pure $ depth != mctx.depth
| _ => throwEx $ Exception.unknownLevelMVar mvarId
def renameMVar (mvarId : MVarId) (newUserName : Name) : MetaM Unit :=
modify $ fun s => { mctx := s.mctx.renameMVar mvarId newUserName, .. s }
@[inline] def isExprMVarAssigned (mvarId : MVarId) : MetaM Bool := do
mctx ← getMCtx;
pure $ mctx.isExprAssigned mvarId
@ -630,13 +633,15 @@ def lambdaTelescope {α} (e : Expr) (k : Array Expr → Expr → MetaM α) : Met
lctx ← getLCtx;
lambdaTelescopeAux k lctx #[] 0 e
-- `kind` specifies the metavariable kind for metavariables not corresponding to instance implicit `[ ... ]` arguments.
private partial def forallMetaTelescopeReducingAux
(reducing? : Bool) (maxMVars? : Option Nat)
(reducing? : Bool) (maxMVars? : Option Nat) (kind : MetavarKind)
: Array Expr → Array BinderInfo → Nat → Expr → MetaM (Array Expr × Array BinderInfo × Expr)
| mvars, bis, j, type@(Expr.forallE n d b c) => do
let process : Unit → MetaM (Array Expr × Array BinderInfo × Expr) := fun _ => do {
let d := d.instantiateRevRange j mvars.size mvars;
mvar ← mkFreshExprMVar d;
let d := d.instantiateRevRange j mvars.size mvars;
let k := if c.binderInfo.isInstImplicit then MetavarKind.synthetic else kind;
mvar ← mkFreshExprMVar d n k;
let mvars := mvars.push mvar;
let bis := bis.push c.binderInfo;
forallMetaTelescopeReducingAux mvars bis j b
@ -661,12 +666,12 @@ private partial def forallMetaTelescopeReducingAux
pure (mvars, bis, type)
/-- Similar to `forallTelescope`, but creates metavariables instead of free variables. -/
def forallMetaTelescope (e : Expr) : MetaM (Array Expr × Array BinderInfo × Expr) :=
forallMetaTelescopeReducingAux false none #[] #[] 0 e
def forallMetaTelescope (e : Expr) (kind := MetavarKind.natural) : MetaM (Array Expr × Array BinderInfo × Expr) :=
forallMetaTelescopeReducingAux false none kind #[] #[] 0 e
/-- Similar to `forallTelescopeReducing`, but creates metavariables instead of free variables. -/
def forallMetaTelescopeReducing (e : Expr) (maxMVars? : Option Nat := none) : MetaM (Array Expr × Array BinderInfo × Expr) :=
forallMetaTelescopeReducingAux true maxMVars? #[] #[] 0 e
def forallMetaTelescopeReducing (e : Expr) (maxMVars? : Option Nat := none) (kind := MetavarKind.natural) : MetaM (Array Expr × Array BinderInfo × Expr) :=
forallMetaTelescopeReducingAux true maxMVars? kind #[] #[] 0 e
/-- Similar to `forallMetaTelescopeReducingAux` but for lambda expressions. -/
private partial def lambdaMetaTelescopeAux (maxMVars? : Option Nat)