Skip to content

Commit 9f4c171

Browse files
gio256kmill
authored and
riccardobrasca
committed
feat: subscript and superscript delaborators (#23018)
We add the functions `delabSubscript` and `delabSuperscript` in the `Mathlib.Tactic` namespace. These delaborators are triggered only if the entirety of the provided expression can be subscripted (respectively, superscripted). The delaborators are not exhaustive, in that they will not successfully delaborate every expression that is valid in a subscript or superscript. We instead aim to make them overly conservative, so that any expression which is successfully delaborated must be subscriptable (or superscriptable). Co-authored-by: Kyle Miller <kmill31415@gmail.com>
1 parent cd1f842 commit 9f4c171

File tree

2 files changed

+191
-2
lines changed

2 files changed

+191
-2
lines changed

‎Mathlib/Util/Superscript.lean‎

Lines changed: 30 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ universe u
2929

3030
namespace Mathlib.Tactic
3131

32-
open Lean Parser PrettyPrinter Std
32+
open Lean Parser PrettyPrinter Delaborator Std
3333

3434
namespace Superscript
3535

@@ -181,7 +181,8 @@ partial def scriptFnNoAntiquot (m : Mapping) (errorMsg : String) (p : ParserFn)
181181
* `errorMsg`: shown when the parser does not match
182182
* `p`: the inner parser (usually `term`), to be called on the body of the superscript
183183
* `many`: if false, whitespace is not allowed inside the superscript
184-
* `kind`: the term will be wrapped in a node with this kind
184+
* `kind`: the term will be wrapped in a node with this kind;
185+
generally this is a name of the parser declaration itself.
185186
-/
186187
def scriptParser (m : Mapping) (antiquotName errorMsg : String) (p : Parser)
187188
(many := true) (kind : SyntaxNodeKind := by exact decl_name%) : Parser :=
@@ -299,4 +300,31 @@ def subscriptTerm := leading_parser (withAnonymousAntiquot := false) subscript t
299300

300301
initialize register_parser_alias subscript
301302

303+
/-- Returns true if every character in `stx : Syntax` can be superscripted
304+
(or subscripted). -/
305+
private partial def Superscript.isValid (m : Mapping) : Syntax → Bool
306+
| .node _ kind args => !(scripted kind) && args.all (isValid m)
307+
| .atom _ s => valid s
308+
| .ident _ _ s _ => valid s.toString
309+
| _ => false
310+
where
311+
valid (s : String) : Bool :=
312+
s.all ((m.toSpecial.insert ' ' ' ').contains ·)
313+
scripted : SyntaxNodeKind → Bool :=
314+
#[``subscript, ``superscript].contains
315+
316+
/-- Successfully delaborates only if the resulting expression can be superscripted.
317+
318+
See `Mapping.superscript` in this file for legal superscript characters. -/
319+
def delabSuperscript : Delab := do
320+
let stx ← delab
321+
if Superscript.isValid .superscript stx.raw then pure stx else failure
322+
323+
/-- Successfully delaborates only if the resulting expression can be subscripted.
324+
325+
See `Mapping.subscript` in this file for legal subscript characters. -/
326+
def delabSubscript : Delab := do
327+
let stx ← delab
328+
if Superscript.isValid .subscript stx.raw then pure stx else failure
329+
302330
end Mathlib.Tactic

‎MathlibTest/superscript.lean‎

Lines changed: 161 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -81,3 +81,164 @@ run_cmd Lean.Elab.Command.liftTermElabM do
8181
Lean.logInfo <| ← Lean.PrettyPrinter.ppTerm <| ← `(term| ($a)$α:subscript)
8282

8383
end
84+
85+
section delab
86+
87+
open Lean PrettyPrinter.Delaborator SubExpr
88+
open Mathlib.Tactic (delabSubscript delabSuperscript)
89+
90+
private def checkSubscript {α : Type} (_ : α) := ()
91+
local syntax:arg "testsub(" noWs subscript(term) noWs ")" : term
92+
local macro_rules | `(testsub($a:subscript)) => `(checkSubscript $a)
93+
94+
private def checkSuperscript {α : Type} (_ : α) := ()
95+
local syntax:arg "testsup(" noWs superscript(term) noWs ")" : term
96+
local macro_rules | `(testsup($a:superscript)) => `(checkSuperscript $a)
97+
98+
@[app_delab checkSubscript]
99+
private def delabCheckSubscript : Delab := withOverApp 2 do
100+
let sub ← withAppArg delabSubscript
101+
`(testsub($sub:subscript))
102+
103+
@[app_delab checkSuperscript]
104+
private def delabCheckSuperscript : Delab := withOverApp 2 do
105+
let sup ← withAppArg delabSuperscript
106+
`(testsup($sup:superscript))
107+
108+
universe u v
109+
110+
/-- `α` can not be subscripted or superscripted. -/
111+
private def α {γ : Type u} {δ : Type v} : γ → δ → δ := fun _ ↦ id
112+
/-- `β` can be both subscripted and superscripted. -/
113+
private def β {γ : Type u} {δ : Type v} : γ → δ → δ := fun _ ↦ id
114+
115+
/-- `d` can not be subscripted, so we create an alias for `id`. -/
116+
private abbrev ID {γ : Sort u} := @id γ
117+
118+
variable (n : Nat)
119+
120+
/-- info: checkSubscript testsub(₁) : Unit -/
121+
#guard_msgs in #check checkSubscript (checkSubscript 1)
122+
/-- info: checkSubscript testsup(¹) : Unit -/
123+
#guard_msgs in #check checkSubscript (checkSuperscript 1)
124+
/-- info: checkSuperscript testsup(¹) : Unit -/
125+
#guard_msgs in #check checkSuperscript (checkSuperscript 1)
126+
/-- info: checkSuperscript testsub(₁) : Unit -/
127+
#guard_msgs in #check checkSuperscript (checkSubscript 1)
128+
129+
section subscript
130+
131+
/-- info: testsub(₁₂₃₄₅₆₇₈₉₀ ₌₌ ₁₂₃₄₅₆₇₈₉₀) : Unit -/
132+
#guard_msgs in #check testsub(₁₂₃₄₅₆₇₈₉₀ ₌₌ ₁₂₃₄₅₆₇₈₉₀)
133+
/-- info: testsub(ᵦ ₙ ₍₁ ₊ ₂ ₋ ₃ ₌ ₀₎) : Unit -/
134+
#guard_msgs in #check testsub(ᵦ ₙ ₍₁ ₊ ₂ ₋ ₃ ₌ ₀₎)
135+
/-- info: testsub(ᵦ) : Unit -/
136+
#guard_msgs in #check testsub(ᵦ)
137+
/-- info: testsub(ᵦ ₍₎) : Unit -/
138+
#guard_msgs in #check testsub(ᵦ ₍₎)
139+
/-- info: testsub(ᵦ ᵦ ᵦ ᵦ) : Unit -/
140+
#guard_msgs in #check testsub(ᵦ ᵦ ᵦ ᵦ)
141+
/-- info: testsub(ɪᴅ ɪᴅ ₃₇) : Unit -/
142+
#guard_msgs in #check testsub(ɪᴅ ɪᴅ ₃₇)
143+
144+
end subscript
145+
146+
section superscript
147+
148+
/-- info: testsup(¹²³⁴⁵⁶⁷⁸⁹⁰ ⁼⁼ ¹²³⁴⁵⁶⁷⁸⁹⁰) : Unit -/
149+
#guard_msgs in #check testsup(¹²³⁴⁵⁶⁷⁸⁹⁰ ⁼⁼ ¹²³⁴⁵⁶⁷⁸⁹⁰)
150+
/-- info: testsup(ᵝ ⁿ ⁽¹ ⁺ ² ⁻ ³ ⁼ ⁰⁾) : Unit -/
151+
#guard_msgs in #check testsup(ᵝ ⁿ ⁽¹ ⁺ ² ⁻ ³ ⁼ ⁰⁾)
152+
/-- info: testsup(ᵝ) : Unit -/
153+
#guard_msgs in #check testsup(ᵝ)
154+
/-- info: testsup(ᵝ ⁽⁾) : Unit -/
155+
#guard_msgs in #check testsup(ᵝ ⁽⁾)
156+
/-- info: testsup(ᵝ ᵝ ᵝ ᵝ) : Unit -/
157+
#guard_msgs in #check testsup(ᵝ ᵝ ᵝ ᵝ)
158+
/-- info: testsup(ⁱᵈ ⁱᵈ ³⁷) : Unit -/
159+
#guard_msgs in #check testsup(ⁱᵈ ⁱᵈ ³⁷)
160+
161+
end superscript
162+
163+
private def card {γ : Sort u} := @id γ
164+
local prefix:arg "#" => card
165+
166+
private def factorial {γ : Sort u} := @id γ
167+
local notation:10000 n "!" => factorial n
168+
169+
abbrev Nat' := Nat
170+
def Nat'.γ : Nat' → Nat' := id
171+
172+
variable (n x_x : Nat')
173+
174+
section no_subscript
175+
176+
/-- info: checkSubscript x_x : Unit -/
177+
#guard_msgs in #check checkSubscript x_x
178+
/-- info: checkSubscript (α 0 0) : Unit -/
179+
#guard_msgs in #check checkSubscript (α 0 0)
180+
/-- info: checkSubscript (0 * 1) : Unit -/
181+
#guard_msgs in #check checkSubscript (0 * 1)
182+
/-- info: checkSubscript (0 ^ 1) : Unit -/
183+
#guard_msgs in #check checkSubscript (0 ^ 1)
184+
/-- info: checkSubscript [1] : Unit -/
185+
#guard_msgs in #check checkSubscript [1]
186+
/-- info: checkSubscript #n : Unit -/
187+
#guard_msgs in #check checkSubscript #n
188+
/-- info: checkSubscript 2! : Unit -/
189+
#guard_msgs in #check checkSubscript 2!
190+
191+
/- The delaborator should reject dot notation. -/
192+
open Nat' (γ) in
193+
/-- info: checkSubscript n.γ : Unit -/
194+
#guard_msgs in #check testsub(ᵧ ₙ)
195+
196+
/- The delaborator should reject metavariables. -/
197+
set_option pp.mvars false in
198+
/-- info: checkSubscript ?_ : Unit -/
199+
#guard_msgs in #check checkSubscript ?_
200+
201+
/- The delaborator should reject because `n` is shadowed and `✝` can not be
202+
subscripted. -/
203+
variable {x} (hx : x = testsub(ₙ)) (n : True) in
204+
/-- info: hx : x = checkSubscript n✝ -/
205+
#guard_msgs in #check hx
206+
207+
end no_subscript
208+
209+
section no_superscript
210+
211+
/-- info: checkSuperscript x_x : Unit -/
212+
#guard_msgs in #check checkSuperscript x_x
213+
/-- info: checkSuperscript (α 0 0) : Unit -/
214+
#guard_msgs in #check checkSuperscript (α 0 0)
215+
/-- info: checkSuperscript (0 * 1) : Unit -/
216+
#guard_msgs in #check checkSuperscript (0 * 1)
217+
/-- info: checkSuperscript (0 ^ 1) : Unit -/
218+
#guard_msgs in #check checkSuperscript (0 ^ 1)
219+
/-- info: checkSuperscript [1] : Unit -/
220+
#guard_msgs in #check checkSuperscript [1]
221+
/-- info: checkSuperscript #n : Unit -/
222+
#guard_msgs in #check checkSuperscript #n
223+
/-- info: checkSuperscript 2! : Unit -/
224+
#guard_msgs in #check checkSuperscript 2!
225+
226+
/- The delaborator should reject dot notation. -/
227+
open Nat' (γ) in
228+
/-- info: checkSuperscript n.γ : Unit -/
229+
#guard_msgs in #check testsup(ᵞ ⁿ)
230+
231+
/- The delaborator should reject metavariables. -/
232+
set_option pp.mvars false in
233+
/-- info: checkSuperscript ?_ : Unit -/
234+
#guard_msgs in #check checkSuperscript ?_
235+
236+
/- The delaborator should reject because `n` is shadowed and `✝` can not be
237+
superscripted. -/
238+
variable {x} (hx : x = testsup(ⁿ)) (n : True) in
239+
/-- info: hx : x = checkSuperscript n✝ -/
240+
#guard_msgs in #check hx
241+
242+
end no_superscript
243+
244+
end delab

0 commit comments

Comments
 (0)