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

feat: remove unnecessary normalizeIds steps

Browse source
This commit is contained in:
Leonardo de Moura 2019-10-09 15:24:07 -07:00
parent feb9b66a30
commit dd69b3b46e
3 changed files with 1 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
library/Init/Lean/Compiler/IR/Borrow.lean
View file

@ -308,7 +308,6 @@ end Borrow
def inferBorrow (decls : Array Decl) : CompilerM (Array Decl) :=
do env ← getEnv;
let decls := decls.map Decl.normalizeIds;
let paramMap := Borrow.infer env decls;
pure (Borrow.applyParamMap decls paramMap)

2
library/Init/Lean/Compiler/IR/EmitC.lean
View file

@ -624,7 +624,7 @@ do env ← getEnv;
| _ => pure ()
def emitDecl (d : Decl) : M Unit :=
let d := d.normalizeIds;
let d := d.normalizeIds; -- ensure we don't have gaps in the variable indices
catch
(emitDeclAux d)
(fun err => throw (err ++ "\ncompiling:\n" ++ toString d))

1
library/Init/Lean/Compiler/IR/ExpandResetReuse.lean
View file

@ -275,7 +275,6 @@ partial def searchAndExpand : FnBody → Array FnBody → M FnBody
else searchAndExpand b.body (push bs b)
def main (d : Decl) : Decl :=
let d := d.normalizeIds;
match d with
| (Decl.fdecl f xs t b) =>
let m := mkProjMap d;