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

feat: add toMono pass

Browse source 
It has to activate by default yet.
This commit is contained in:
Leonardo de Moura 2022-10-05 10:37:11 -07:00
parent 254e28bd99
commit b172ba8a34
2 changed files with 13 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Lean/Compiler/LCNF.lean
View file

@ -35,4 +35,5 @@ import Lean.Compiler.LCNF.Types
import Lean.Compiler.LCNF.Util
import Lean.Compiler.LCNF.ConfigOptions
import Lean.Compiler.LCNF.ForEachExpr
import Lean.Compiler.LCNF.MonoTypes
import Lean.Compiler.LCNF.MonoTypes
import Lean.Compiler.LCNF.ToMono

12
src/Lean/Compiler/LCNF/ToMono.lean
View file

@ -62,6 +62,16 @@ def Decl.toMono (decl : Decl) : CompilerM Decl := do
let type ← toMonoType decl.type
let params ← decl.params.mapM (·.toMono)
let value ← decl.value.toMono
return { decl with type, params, value, levelParams := [] }
let decl := { decl with type, params, value, levelParams := [] }
decl.saveMono
return decl
def toMono : Pass where
name := `toMono
run := fun decls => decls.mapM (·.toMono)
phase := .base
builtin_initialize
registerTraceClass `Compiler.toMono (inherited := true)
end Lean.Compiler.LCNF