fix: Printing of argument names with macro scopes

Previously we would print all names with macro scopes (after removing
the macro related stuff) which could cause confusion if for example
there was an actual parameter named `a` and one named `a` but
autogenerated by Lean itself. Now we only try to print names with
macro scopes iff they are names of type class parameters. Otherwise
the rest of the Expr is moved behind the :.
main
Henrik Böving 2022-01-15 15:12:55 +01:00
parent b93e1c9f54
commit 4a3e22490f
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