Lean4
/-- Converts an entry (i.e., `List Key`) to the discrimination tree into
`MessageData` that is more user-friendly.
This is a copy of `Lean.Meta.DiscrTree.keysAsPattern`
-/
partial def keysAsPattern (keys : Array Key) : CoreM MessageData := do
let (msg, keys) ← go (paren := false) |>.run keys.toList
if !keys.isEmpty then
throwError "illegal discrimination tree entry: {keys.map Key.format}"
return msg
where
/-- Get the next key. -/
next : StateRefT (List Key) CoreM Key := do
let key :: keys ← get |
throwError "illegal discrimination tree entry: {keys.map Key.format}"
set keys
return key
/-- Format the application `f args`. -/
mkApp (f : MessageData) (nargs : Nat) (paren : Bool) : StateRefT (List Key) CoreM MessageData :=
if nargs == 0 then return f
else do
let mut r := m!""
for _ in [:nargs]do
r := r ++ Format.line ++ (← go)
r := f ++ .nest 2 r
if paren then
return .paren r
else
return .group r
/-- Format the next expression. -/
go (paren := true) : StateRefT (List Key) CoreM MessageData := do
let key ← next
match key with
| .const declName nargs =>
mkApp (m!"{← mkConstWithLevelParams declName}") nargs paren
| .fvar fvarId nargs =>
mkApp (m! "{mkFVar fvarId}") nargs paren
| .proj _ i nargs =>
mkApp (m!"{(← go)}.{i + 1}") nargs paren
| .bvar i nargs =>
mkApp (m! "#{i}") nargs paren
| .lam =>
return parenthesize (m!"λ, {← go (paren := false)}") paren
| .forall =>
return parenthesize (m!"{(← go)} → {← go (paren := false)}") paren
| _ =>
return key.format
/-- Add parentheses if `paren == true`. -/
parenthesize (msg : MessageData) (paren : Bool) : MessageData := if paren then msg.paren else msg.group
