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

feat: simplify LCtx

Browse source
This commit is contained in:
Leonardo de Moura 2022-08-24 14:16:26 -07:00
parent 85866fc238
commit 4e8b4e96e9
1 changed files with 4 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/Lean/Compiler/LCNF/LCtx.lean
View file

@ -14,32 +14,27 @@ LCNF local context.
structure LCtx where
localDecls : Std.HashMap FVarId LocalDecl := {}
funDecls : Std.HashMap FVarId FunDecl := {}
fvarIds : Array FVarId := #[]
deriving Inhabited
def LCtx.addLocalDecl (lctx : LCtx) (fvarId : FVarId) (binderName : Name) (type : Expr) : LCtx :=
{ lctx with
localDecls := lctx.localDecls.insert fvarId (.cdecl 0 fvarId binderName type .default)
fvarIds := lctx.fvarIds.push fvarId }
localDecls := lctx.localDecls.insert fvarId (.cdecl 0 fvarId binderName type .default) }
def LCtx.addLetDecl (lctx : LCtx) (fvarId : FVarId) (binderName : Name) (type : Expr) (value : Expr) : LCtx :=
{ lctx with
localDecls := lctx.localDecls.insert fvarId (.ldecl 0 fvarId binderName type value true)
fvarIds := lctx.fvarIds.push fvarId }
localDecls := lctx.localDecls.insert fvarId (.ldecl 0 fvarId binderName type value true) }
def LCtx.addFunDecl (lctx : LCtx) (funDecl : FunDecl) : LCtx :=
{ lctx with
localDecls := lctx.localDecls.insert funDecl.fvarId (.cdecl 0 funDecl.fvarId funDecl.binderName funDecl.type .default)
funDecls := lctx.funDecls.insert funDecl.fvarId funDecl
fvarIds := lctx.fvarIds.push funDecl.fvarId }
funDecls := lctx.funDecls.insert funDecl.fvarId funDecl }
/--
Convert a LCNF local context into a regular Lean local context.
-/
def LCtx.toLocalContext (lctx : LCtx) : LocalContext := Id.run do
let mut result := {}
for fvarId in lctx.fvarIds do
let localDecl := lctx.localDecls.find? fvarId |>.get!
for (_, localDecl) in lctx.localDecls.toArray do
result := result.addDecl localDecl
return result