From 4a3e22490fdd577aa02a1848d97c9fa1416fde5c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Sat, 15 Jan 2022 15:12:55 +0100
Subject: [PATCH] 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 :.
---
 DocGen4/Process.lean | 25 +++++++++++++++----------
 1 file changed, 15 insertions(+), 10 deletions(-)

diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean
index dc5d954..eb58f72 100644
--- a/DocGen4/Process.lean
+++ b/DocGen4/Process.lean
@@ -102,17 +102,22 @@ structure Module where
   deriving Inhabited
 
 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
-  | Expr.lam 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)
-  | 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)
+  | Expr.lam name type body data => helper name type body data
+  | Expr.forallE name type body data => helper name type body data
   | _ => (#[], e)
 
 def prettyPrintTerm (expr : Expr) : MetaM CodeWithInfos := do