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

feat: include def/fun/jp resulting type in the LCNF pretty printer

Browse source
This commit is contained in:
Leonardo de Moura 2022-10-09 08:23:56 -07:00
parent eeb98d9cf4
commit c14d07fe2e
1 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Lean/Compiler/LCNF/PrettyPrinter.lean
View file

@ -79,9 +79,12 @@ def ppLetDecl (letDecl : LetDecl) : M Format := do
else
return f!"let {letDecl.binderName} := {← ppValue letDecl.value}"
def getFunType (ps : Array Param) (type : Expr) : CoreM Expr :=
instantiateForall type (ps.map (mkFVar ·.fvarId))
mutual
partial def ppFunDecl (funDecl : FunDecl) : M Format := do
return f!"{funDecl.binderName}{← ppParams funDecl.params} :={indentD (← ppCode funDecl.value)}"
return f!"{funDecl.binderName}{← ppParams funDecl.params} : {← ppExpr (← getFunType funDecl.params funDecl.type)} :={indentD (← ppCode funDecl.value)}"
partial def ppAlt (alt : Alt) : M Format := do
match alt with
@ -110,11 +113,11 @@ def ppCode (code : Code) : CompilerM Format :=
def ppDecl (decl : Decl) : CompilerM Format :=
PP.run do
return f!"def {decl.name}{← PP.ppParams decl.params} :={indentD (← PP.ppCode decl.value)}"
return f!"def {decl.name}{← PP.ppParams decl.params} : {← PP.ppExpr (← PP.getFunType decl.params decl.type)} :={indentD (← PP.ppCode decl.value)}"
def ppFunDecl (decl : FunDecl) : CompilerM Format :=
PP.run do
return f!"fun {decl.binderName}{← PP.ppParams decl.params} :={indentD (← PP.ppCode decl.value)}"
return f!"fun {← PP.ppFunDecl decl}"
/--
Similar to `ppDecl`, but in `CoreM`, and it does not assume