feat: print nameless instances properly

main
Henrik 2023-09-09 23:56:21 +02:00
parent 3c80369cca
commit b0319462f1
3 changed files with 15 additions and 7 deletions

View File

@ -30,7 +30,10 @@ def argToHtml (arg : Arg) : HtmlM Html := do
| BinderInfo.implicit => ("{", "}", true) | BinderInfo.implicit => ("{", "}", true)
| BinderInfo.strictImplicit => ("⦃", "⦄", true) | BinderInfo.strictImplicit => ("⦃", "⦄", true)
| BinderInfo.instImplicit => ("[", "]", true) | BinderInfo.instImplicit => ("[", "]", true)
let mut nodes := #[Html.text s!"{l}{arg.name.toString} : "] let mut nodes :=
match arg.name with
| some name => #[Html.text s!"{l}{name.toString} : "]
| none => #[Html.text s!"{l}"]
nodes := nodes.append (← infoFormatToHtml arg.type) nodes := nodes.append (← infoFormatToHtml arg.type)
nodes := nodes.push r nodes := nodes.push r
let inner := <span class="fn">[nodes]</span> let inner := <span class="fn">[nodes]</span>

View File

@ -27,14 +27,16 @@ structure NameInfo where
doc : Option String doc : Option String
deriving Inhabited deriving Inhabited
/-- /--
An argument to a declaration, e.g. the `(x : Nat)` in `def foo (x : Nat) := x`. An argument to a declaration, e.g. the `(x : Nat)` in `def foo (x : Nat) := x`.
-/ -/
structure Arg where structure Arg where
/-- /--
The name of the argument. The name of the argument. For auto generated argument names like `[Monad α]`
this is none
-/ -/
name : Name name : Option Name
/-- /--
The pretty printed type of the argument. The pretty printed type of the argument.
-/ -/

View File

@ -15,17 +15,20 @@ def NameInfo.ofTypedName (n : Name) (t : Expr) : MetaM NameInfo := do
let env ← getEnv let env ← getEnv
return { name := n, type := ← prettyPrintTerm t, doc := ← findDocString? env n} return { name := n, type := ← prettyPrintTerm t, doc := ← findDocString? env n}
partial def typeToArgsType (e : Expr) : (Array (Name × Expr × BinderInfo) × Expr) := partial def typeToArgsType (e : Expr) : (Array ((Option Name) × Expr × BinderInfo) × Expr) :=
let helper := fun name type body data => let helper := fun name type body data =>
-- Once we hit a name with a macro scope we stop traversing the expression -- 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 -- and print what is left after the : instead. The only exception
-- to this is instances since these almost never have a name -- to this is instances since these almost never have a name
-- but should still be printed as arguments instead of after the :. -- but should still be printed as arguments instead of after the :.
if name.hasMacroScopes && !data.isInstImplicit then if data.isInstImplicit then
let arg := (none, type, data)
let (args, final) := typeToArgsType (Expr.instantiate1 body (mkFVar ⟨name⟩))
(#[arg] ++ args, final)
else if name.hasMacroScopes then
(#[], e) (#[], e)
else else
let name := name.eraseMacroScopes let arg := (some name, type, data)
let arg := (name, type, data)
let (args, final) := typeToArgsType (Expr.instantiate1 body (mkFVar ⟨name⟩)) let (args, final) := typeToArgsType (Expr.instantiate1 body (mkFVar ⟨name⟩))
(#[arg] ++ args, final) (#[arg] ++ args, final)
match e.consumeMData with match e.consumeMData with