From 66040a9803cb2ff46de3a19b22ebc8d5f1950bdb Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Wed, 28 Sep 2022 21:17:19 -0400 Subject: [PATCH] feat: clearer info tree formatting --- src/Lean/Elab/InfoTree/Main.lean | 8 +- .../1018unknowMVarIssue.lean.expected.out | 136 +++++++++--------- 2 files changed, 72 insertions(+), 72 deletions(-) diff --git a/src/Lean/Elab/InfoTree/Main.lean b/src/Lean/Elab/InfoTree/Main.lean index 0c626a034c..286ea0d11f 100644 --- a/src/Lean/Elab/InfoTree/Main.lean +++ b/src/Lean/Elab/InfoTree/Main.lean @@ -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 "" + | none => return "• " | 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] diff --git a/tests/lean/1018unknowMVarIssue.lean.expected.out b/tests/lean/1018unknowMVarIssue.lean.expected.out index a3315862db..7c3faea620 100644 --- a/tests/lean/1018unknowMVarIssue.lean.expected.out +++ b/tests/lean/1018unknowMVarIssue.lean.expected.out @@ -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 : @ ⟨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 : @ ⟨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⟩