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

feat: add instantiateLCtxMVars and instantiateMVarDeclMVars

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-16 15:45:40 -08:00
parent b0298697c5
commit 0c9107fc72
2 changed files with 21 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Lean/LocalContext.lean
View file

@ -59,7 +59,7 @@ mkFVar decl.fvarId
end LocalDecl
structure LocalContext :=
(fvarIdToDecl : PersistentHashMap Name LocalDecl := {})
(fvarIdToDecl : PersistentHashMap FVarId LocalDecl := {})
(decls : PersistentArray (Option LocalDecl) := {})
namespace LocalContext

20
src/Init/Lean/MetavarContext.lean
View file

@ -546,6 +546,26 @@ def instantiateMVars (mctx : MetavarContext) (e : Expr) : Expr × MetavarContext
if !e.hasMVar then (e, mctx)
else (WithHashMapCache.toState $ InstantiateExprMVars.main e).run mctx
def instantiateLCtxMVars (mctx : MetavarContext) (lctx : LocalContext) : LocalContext × MetavarContext :=
lctx.foldl
(fun (result : LocalContext × MetavarContext) ldecl =>
let (lctx, mctx) := result;
match ldecl with
| LocalDecl.cdecl _ fvarId userName type bi =>
let (type, mctx) := mctx.instantiateMVars type;
(lctx.mkLocalDecl fvarId userName type bi, mctx)
| LocalDecl.ldecl _ fvarId userName type value =>
let (type, mctx) := mctx.instantiateMVars type;
let (value, mctx) := mctx.instantiateMVars value;
(lctx.mkLetDecl fvarId userName type value, mctx))
({}, mctx)
def instantiateMVarDeclMVars (mctx : MetavarContext) (mvarId : MVarId) : MetavarContext :=
let mvarDecl := mctx.getDecl mvarId;
let (lctx, mctx) := mctx.instantiateLCtxMVars mvarDecl.lctx;
let (type, mctx) := mctx.instantiateMVars mvarDecl.type;
{ decls := mctx.decls.insert mvarId { lctx := lctx, type := type, .. mvarDecl }, .. mctx }
namespace DependsOn
private abbrev M := StateM ExprSet