feat: clearer info tree formatting
This commit is contained in:
Mario Carneiro
Sebastian Ullrich
parent
7a6f7cb0ac
commit
66040a9803
2 changed files with 72 additions and 72 deletions
|
|
@ -190,17 +190,17 @@ def Info.updateContext? : Option ContextInfo → Info → Option ContextInfo
|
|||
|
||||
partial def InfoTree.format (tree : InfoTree) (ctx? : Option ContextInfo := none) : IO Format := do
|
||||
match tree with
|
||||
| hole id => return toString id.name
|
||||
| hole id => return .nestD f!"• ?{toString id.name}"
|
||||
| context i t => format t i
|
||||
| node i cs => match ctx? with
|
||||
| none => return "<context-not-available>"
|
||||
| none => return "• <context-not-available>"
|
||||
| some ctx =>
|
||||
let fmt ← i.format ctx
|
||||
if cs.size == 0 then
|
||||
return fmt
|
||||
return .nestD f!"• {fmt}"
|
||||
else
|
||||
let ctx? := i.updateContext? ctx?
|
||||
return f!"{fmt}{Std.Format.nestD <| Std.Format.prefixJoin (Std.format "\n") (← cs.toList.mapM fun c => format c ctx?)}"
|
||||
return .nestD f!"• {fmt}{Std.Format.prefixJoin .line (← cs.toList.mapM fun c => format c ctx?)}"
|
||||
|
||||
section
|
||||
variable [Monad m] [MonadInfoTree m]
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
[Elab.info] command @ ⟨6, 0⟩-⟨6, 31⟩ @ Lean.Elab.Command.elabSetOption
|
||||
[.] (Command.set_option "set_option" `trace.Elab.info) @ ⟨6, 0⟩-⟨6, 26⟩
|
||||
[Elab.info] • command @ ⟨6, 0⟩-⟨6, 31⟩ @ Lean.Elab.Command.elabSetOption
|
||||
• [.] (Command.set_option "set_option" `trace.Elab.info) @ ⟨6, 0⟩-⟨6, 26⟩
|
||||
1018unknowMVarIssue.lean:9:18-9:19: error: don't know how to synthesize placeholder
|
||||
context:
|
||||
α✝ β : Type
|
||||
|
|
@ -7,69 +7,69 @@ x : Fam2 α✝ β
|
|||
α : Type
|
||||
a : α
|
||||
⊢ α
|
||||
[Elab.info] command @ ⟨7, 0⟩-⟨10, 19⟩ @ Lean.Elab.Command.elabDeclaration
|
||||
α : Type @ ⟨7, 13⟩-⟨7, 14⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `α : some Sort.{?_uniq} @ ⟨7, 13⟩-⟨7, 14⟩
|
||||
α : Type @ ⟨7, 13⟩-⟨7, 14⟩
|
||||
a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
|
||||
α : Type @ ⟨7, 13⟩-⟨7, 14⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `α : some Sort.{?_uniq} @ ⟨7, 13⟩-⟨7, 14⟩
|
||||
α : Type @ ⟨7, 13⟩-⟨7, 14⟩
|
||||
a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
|
||||
Fam2 α β : Type 1 @ ⟨7, 21⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabApp
|
||||
[.] `Fam2 : some Sort.{?_uniq} @ ⟨7, 21⟩-⟨7, 25⟩
|
||||
Fam2 : Type → Type → Type 1 @ ⟨7, 21⟩-⟨7, 25⟩
|
||||
α : Type @ ⟨7, 26⟩-⟨7, 27⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `α : some Type @ ⟨7, 26⟩-⟨7, 27⟩
|
||||
α : Type @ ⟨7, 26⟩-⟨7, 27⟩
|
||||
β : Type @ ⟨7, 28⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `β : some Type @ ⟨7, 28⟩-⟨7, 29⟩
|
||||
β : Type @ ⟨7, 28⟩-⟨7, 29⟩
|
||||
x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩
|
||||
β : Type @ ⟨7, 33⟩-⟨7, 34⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `β : some Sort.{?_uniq} @ ⟨7, 33⟩-⟨7, 34⟩
|
||||
β : Type @ ⟨7, 33⟩-⟨7, 34⟩
|
||||
_example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩†-⟨10, 19⟩†
|
||||
a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
|
||||
x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩
|
||||
_example.match_1 (fun α β x a => β) α β x a (fun α_1 a => ?m x α_1 a) fun n a =>
|
||||
n : <failed-to-infer-type> @ ⟨8, 2⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabMatch
|
||||
x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩
|
||||
[.] `Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
|
||||
[.] `Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
|
||||
@Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
|
||||
[.] `Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
|
||||
Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
|
||||
[.] `n : none @ ⟨10, 13⟩-⟨10, 14⟩
|
||||
[.] `Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
|
||||
[.] `Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
|
||||
@Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
|
||||
[.] `a : none @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||||
[.] `Fam2.any : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨9, 4⟩-⟨9, 12⟩
|
||||
[.] `a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||||
α (isBinder := true) : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||||
α : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||||
Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
|
||||
α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
|
||||
a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||||
FVarAlias _uniq.641 -> _uniq.299
|
||||
FVarAlias _uniq.640 -> _uniq.297
|
||||
?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
|
||||
[.] `Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
|
||||
Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
|
||||
[.] `n : none @ ⟨10, 13⟩-⟨10, 14⟩
|
||||
[.] `a : none @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||||
[.] `Fam2.nat : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨10, 4⟩-⟨10, 12⟩
|
||||
[.] `n : some Nat @ ⟨10, 13⟩-⟨10, 14⟩
|
||||
[.] `a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||||
Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||||
Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||||
Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩
|
||||
n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩
|
||||
a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||||
FVarAlias _uniq.672 -> _uniq.299
|
||||
FVarAlias _uniq.671 -> _uniq.297
|
||||
n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩
|
||||
n : Nat @ ⟨10, 18⟩-⟨10, 19⟩
|
||||
@_example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩-⟨7, 7⟩
|
||||
[Elab.info] • command @ ⟨7, 0⟩-⟨10, 19⟩ @ Lean.Elab.Command.elabDeclaration
|
||||
• α : Type @ ⟨7, 13⟩-⟨7, 14⟩ @ Lean.Elab.Term.elabIdent
|
||||
• [.] `α : some Sort.{?_uniq} @ ⟨7, 13⟩-⟨7, 14⟩
|
||||
• α : Type @ ⟨7, 13⟩-⟨7, 14⟩
|
||||
• a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
|
||||
• α : Type @ ⟨7, 13⟩-⟨7, 14⟩ @ Lean.Elab.Term.elabIdent
|
||||
• [.] `α : some Sort.{?_uniq} @ ⟨7, 13⟩-⟨7, 14⟩
|
||||
• α : Type @ ⟨7, 13⟩-⟨7, 14⟩
|
||||
• a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
|
||||
• Fam2 α β : Type 1 @ ⟨7, 21⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabApp
|
||||
• [.] `Fam2 : some Sort.{?_uniq} @ ⟨7, 21⟩-⟨7, 25⟩
|
||||
• Fam2 : Type → Type → Type 1 @ ⟨7, 21⟩-⟨7, 25⟩
|
||||
• α : Type @ ⟨7, 26⟩-⟨7, 27⟩ @ Lean.Elab.Term.elabIdent
|
||||
• [.] `α : some Type @ ⟨7, 26⟩-⟨7, 27⟩
|
||||
• α : Type @ ⟨7, 26⟩-⟨7, 27⟩
|
||||
• β : Type @ ⟨7, 28⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabIdent
|
||||
• [.] `β : some Type @ ⟨7, 28⟩-⟨7, 29⟩
|
||||
• β : Type @ ⟨7, 28⟩-⟨7, 29⟩
|
||||
• x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩
|
||||
• β : Type @ ⟨7, 33⟩-⟨7, 34⟩ @ Lean.Elab.Term.elabIdent
|
||||
• [.] `β : some Sort.{?_uniq} @ ⟨7, 33⟩-⟨7, 34⟩
|
||||
• β : Type @ ⟨7, 33⟩-⟨7, 34⟩
|
||||
• _example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩†-⟨10, 19⟩†
|
||||
• a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
|
||||
• x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩
|
||||
• _example.match_1 (fun α β x a => β) α β x a (fun α_1 a => ?m x α_1 a) fun n a =>
|
||||
n : <failed-to-infer-type> @ ⟨8, 2⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabMatch
|
||||
• x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩
|
||||
• [.] `Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
|
||||
• [.] `Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
|
||||
• @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
|
||||
• [.] `Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
|
||||
• Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
|
||||
• [.] `n : none @ ⟨10, 13⟩-⟨10, 14⟩
|
||||
• [.] `Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
|
||||
• [.] `Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
|
||||
• @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
|
||||
• [.] `a : none @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||||
• [.] `Fam2.any : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨9, 4⟩-⟨9, 12⟩
|
||||
• [.] `a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||||
• α (isBinder := true) : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||||
• α : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||||
• Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
|
||||
• α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
|
||||
• a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||||
• FVarAlias _uniq.641 -> _uniq.299
|
||||
• FVarAlias _uniq.640 -> _uniq.297
|
||||
• ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
|
||||
• [.] `Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
|
||||
• Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
|
||||
• [.] `n : none @ ⟨10, 13⟩-⟨10, 14⟩
|
||||
• [.] `a : none @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||||
• [.] `Fam2.nat : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨10, 4⟩-⟨10, 12⟩
|
||||
• [.] `n : some Nat @ ⟨10, 13⟩-⟨10, 14⟩
|
||||
• [.] `a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||||
• Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||||
• Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||||
• Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩
|
||||
• n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩
|
||||
• a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||||
• FVarAlias _uniq.672 -> _uniq.299
|
||||
• FVarAlias _uniq.671 -> _uniq.297
|
||||
• n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
|
||||
• [.] `n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩
|
||||
• n : Nat @ ⟨10, 18⟩-⟨10, 19⟩
|
||||
• @_example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩-⟨7, 7⟩
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue