Merge pull request #20 from leanprover/fix-anonymous-arrows

fix: Printing of argument names with macro scopes
main
Henrik Böving 2022-01-15 15:17:44 +01:00 committed by GitHub
commit 1edf4bbdab
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 15 additions and 10 deletions

View File

@ -102,17 +102,22 @@ structure Module where
deriving Inhabited deriving Inhabited
partial def typeToArgsType (e : Expr) : (Array (Name × Expr × BinderInfo) × Expr) := partial def typeToArgsType (e : Expr) : (Array (Name × Expr × BinderInfo) × Expr) :=
let helper := λ name type body data =>
-- Once we hit a name with a macro scope we stop traversing the expression
-- and print what is left after the : instead. The only exception
-- to this is instances since these almost never have a name
-- but should still be printed as arguments instead of after the :.
if name.hasMacroScopes ∧ ¬data.binderInfo.isInstImplicit then
(#[], e)
else
let name := name.eraseMacroScopes
let arg := (name, type, data.binderInfo)
let (args, final) := typeToArgsType (Expr.instantiate1 body (mkFVar ⟨name⟩))
(#[arg] ++ args, final)
match e.consumeMData with match e.consumeMData with
| Expr.lam name type body data => | Expr.lam name type body data => helper name type body data
let name := name.eraseMacroScopes | Expr.forallE name type body data => helper name type body data
let arg := (name, type, data.binderInfo)
let (args, final) := typeToArgsType (Expr.instantiate1 body (mkFVar ⟨name⟩))
(#[arg] ++ args, final)
| Expr.forallE name type body data =>
let name := name.eraseMacroScopes
let arg := (name, type, data.binderInfo)
let (args, final) := typeToArgsType (Expr.instantiate1 body (mkFVar ⟨name⟩))
(#[arg] ++ args, final)
| _ => (#[], e) | _ => (#[], e)
def prettyPrintTerm (expr : Expr) : MetaM CodeWithInfos := do def prettyPrintTerm (expr : Expr) : MetaM CodeWithInfos := do