[Merged by Bors] - feat: subscript and superscript delaborators

Mathlib/Util/Superscript.lean

@@ -29,7 +29,7 @@ universe u
 
 namespace Mathlib.Tactic
 
-open Lean Parser PrettyPrinter Std
+open Lean Parser PrettyPrinter Delaborator Std
 
 namespace Superscript
 
@@ -225,6 +225,30 @@ def scriptParser.formatter (name : String) (m : Mapping) (k : SyntaxNodeKind) (p
   | .ok newStack =>
     set { st with stack := stack ++ newStack }
 
+section Delab
+
+/-- Returns `true` if every character in `s` can be subscripted. -/
+private def isSubscriptable (s : String) : Bool :=
+  s.toList.all fun x ↦ x == ' ' || Mapping.subscript.toSpecial.contains x
+
+/-- Returns `true` if every character in `s` can be superscripted. -/
+private def isSuperscriptable (s : String) : Bool :=
+  s.toList.all fun x ↦ x == ' ' || Mapping.superscript.toSpecial.contains x
+
+private partial def superscriptable : Syntax → DelabM Unit
+  | .node _ _ args => args.forM superscriptable
+  | .atom _ val => guard <| isSuperscriptable val
+  | .ident _ _ val _ => guard <| isSuperscriptable val.toString
+  | _ => failure
+
+private partial def subscriptable : Syntax → DelabM Unit
+  | .node _ _ args => args.forM subscriptable
+  | .atom _ s => guard <| isSubscriptable s
+  | .ident _ _ s _ => guard <| isSubscriptable s.toString
+  | _ => failure
+
+end Delab
+
 end Superscript
 
 /--
@@ -263,6 +287,17 @@ def superscriptTerm := leading_parser (withAnonymousAntiquot := false) superscri
 
 initialize register_parser_alias superscript
 
+/-- Checks that the current expression can be superscripted before delaborating.
+
+This is a conservative approximation — it may not succeed even given a valid
+superscriptable expression as input.
+
+See `Mapping.superscript` in this file for legal superscript characters. -/
+def delabSuperscript : Delab := do
+  let de ← delab
+  let _ ← Superscript.superscriptable de.raw
+  pure de
+
 /--
 The parser `subscript(term)` parses a subscript. Basic usage is:
 ```
@@ -299,4 +334,15 @@ def subscriptTerm := leading_parser (withAnonymousAntiquot := false) subscript t
 
 initialize register_parser_alias subscript
 
+/-- Checks that the current expression can be subscripted before delaborating.
+
+This is a conservative approximation — it may not succeed even given a valid
+subscriptable expression as input.
+
+See `Mapping.subscript` in this file for legal subscript characters. -/
+def delabSubscript : Delab := do
+  let de ← delab
+  let _ ← Superscript.subscriptable de.raw
+  pure de
+
 end Mathlib.Tactic

MathlibTest/superscript.lean

@@ -81,3 +81,150 @@ run_cmd Lean.Elab.Command.liftTermElabM do
   Lean.logInfo <| ← Lean.PrettyPrinter.ppTerm <| ← `(term| ($a)$α:subscript)
 
 end
+
+section delab
+
+open Lean PrettyPrinter.Delaborator SubExpr
+open Mathlib.Tactic (delabSubscript delabSuperscript)
+
+private def check_subscript {α : Type} (_ : α) := ()
+local syntax:arg "test(" noWs subscript(term) noWs ")" : term
+local macro_rules | `(test($a:subscript)) => `(check_subscript $a)
+
+private def check_superscript {α : Type} (_ : α) := ()
+local syntax:arg "test(" noWs superscript(term) noWs ")" : term
+local macro_rules | `(test($a:superscript)) => `(check_superscript $a)
+
+@[app_delab check_subscript]
+private def delabCheckSubscript : Delab := withOverApp 2 do
+  let sub ← withAppArg delabSubscript
+  `(test($sub:subscript))
+
+@[app_delab check_superscript]
+private def delabCheckSuperscript : Delab := withOverApp 2 do
+  let sup ← withAppArg delabSuperscript
+  `(test($sup:superscript))
+
+universe u v w
+
+/-- `α` can not be subscripted or superscripted. -/
+private def α {γ : Type u} {δ : Type v} : γ → δ → δ := fun _ ↦ id
+/-- `β` can be both subscripted and superscripted. -/
+private def β {γ : Type u} {δ : Type v} : γ → δ → δ := fun _ ↦ id
+
+/-- `d` can not be subscripted, so we create an alias for `id`. -/
+private abbrev ID {γ : Sort u} := @id γ
+
+variable (n : String)
+
+section subscript
+
+/-- info: test(₁₂₃₄₅₆₇₈₉₀ ₌₌ ₁₂₃₄₅₆₇₈₉₀) : Unit -/
+#guard_msgs in #check test(₁₂₃₄₅₆₇₈₉₀ ₌₌ ₁₂₃₄₅₆₇₈₉₀)
+/-- info: test(ᵦ ₙ ₍₁ ₊ ₂ ₋ ₃ ₌ ₀₎) : Unit -/
+#guard_msgs in #check test(ᵦ ₙ ₍₁ ₊ ₂ ₋ ₃ ₌ ₀₎)
+/-- info: test(ᵦ) : Unit -/
+#guard_msgs in #check test(ᵦ)
+/-- info: test(ᵦ ₍₎) : Unit -/
+#guard_msgs in #check test(ᵦ ₍₎)
+/-- info: test(ᵦ ᵦ ᵦ ᵦ) : Unit -/
+#guard_msgs in #check test(ᵦ ᵦ ᵦ ᵦ)
+/-- info: test(ɪᴅ ɪᴅ ₃₇) : Unit -/
+#guard_msgs in #check test(ɪᴅ ɪᴅ ₃₇)
+
+end subscript
+
+section superscript
+
+/-- info: test(¹²³⁴⁵⁶⁷⁸⁹⁰ ⁼⁼ ¹²³⁴⁵⁶⁷⁸⁹⁰) : Unit -/
+#guard_msgs in #check test(¹²³⁴⁵⁶⁷⁸⁹⁰ ⁼⁼ ¹²³⁴⁵⁶⁷⁸⁹⁰)
+/-- info: test(ᵝ ⁿ ⁽¹ ⁺ ² ⁻ ³ ⁼ ⁰⁾) : Unit -/
+#guard_msgs in #check test(ᵝ ⁿ ⁽¹ ⁺ ² ⁻ ³ ⁼ ⁰⁾)
+/-- info: test(ᵝ) : Unit -/
+#guard_msgs in #check test(ᵝ)
+/-- info: test(ᵝ ⁽⁾) : Unit -/
+#guard_msgs in #check test(ᵝ ⁽⁾)
+/-- info: test(ᵝ ᵝ ᵝ ᵝ) : Unit -/
+#guard_msgs in #check test(ᵝ ᵝ ᵝ ᵝ)
+/-- info: test(ⁱᵈ ⁱᵈ ³⁷) : Unit -/
+#guard_msgs in #check test(ⁱᵈ ⁱᵈ ³⁷)
+
+end superscript
+
+variable (x_x : String)
+
+private def card {γ : Sort u} := @id γ
+local prefix:arg "#" => card
+
+private def factorial {γ : Sort u} := @id γ
+local notation:10000 n "!" => factorial n
+
+private class HSMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
+  hSMul : α → β → γ
+instance : HSMul Nat Nat Nat where
+  hSMul a b := a * b
+infixr:73 " • " => HSMul.hSMul
+
+section no_subscript
+
+/-- info: check_subscript x_x : Unit -/
+#guard_msgs in #check check_subscript x_x
+/-- info: check_subscript (α 0 0) : Unit -/
+#guard_msgs in #check check_subscript (α 0 0)
+/-- info: check_subscript (0 * 1) : Unit -/
+#guard_msgs in #check check_subscript (0 * 1)
+/-- info: check_subscript (0 ^ 1) : Unit -/
+#guard_msgs in #check check_subscript (0 ^ 1)
+/-- info: check_subscript [1] : Unit -/
+#guard_msgs in #check check_subscript [1]
+/-- info: check_subscript #n : Unit -/
+#guard_msgs in #check check_subscript #n
+/-- info: check_subscript 2! : Unit -/
+#guard_msgs in #check check_subscript 2!
+/-- info: check_subscript (1 • 2) : Unit -/
+#guard_msgs in #check check_subscript (1 • 2)
+
+set_option pp.mvars false in
+/-- info: check_subscript ?_ : Unit -/
+#guard_msgs in #check check_subscript ?_
+
+/- The delaborator should fail because `n` is shadowed and `✝` can not be
+subscripted. -/
+variable {x} (hx : x = test(ₙ)) (n : True) in
+/-- info: hx : x = check_subscript n✝ -/
+#guard_msgs in #check hx
+
+end no_subscript
+
+section no_superscript
+
+/-- info: check_superscript x_x : Unit -/
+#guard_msgs in #check check_superscript x_x
+/-- info: check_superscript (α 0 0) : Unit -/
+#guard_msgs in #check check_superscript (α 0 0)
+/-- info: check_superscript (0 * 1) : Unit -/
+#guard_msgs in #check check_superscript (0 * 1)
+/-- info: check_superscript (0 ^ 1) : Unit -/
+#guard_msgs in #check check_superscript (0 ^ 1)
+/-- info: check_superscript [1] : Unit -/
+#guard_msgs in #check check_superscript [1]
+/-- info: check_superscript #n : Unit -/
+#guard_msgs in #check check_superscript #n
+/-- info: check_superscript 2! : Unit -/
+#guard_msgs in #check check_superscript 2!
+/-- info: check_superscript (1 • 2) : Unit -/
+#guard_msgs in #check check_superscript (1 • 2)
+
+set_option pp.mvars false in
+/-- info: check_superscript ?_ : Unit -/
+#guard_msgs in #check check_superscript ?_
+
+/- The delaborator should fail because `n` is shadowed and `✝` can not be
+superscripted. -/
+variable {x} (hx : x = test(ⁿ)) (n : True) in
+/-- info: hx : x = check_superscript n✝ -/
+#guard_msgs in #check hx
+
+end no_superscript
+
+end delab