A parser for superscripts and subscripts #
This is intended for use in local notations. Basic usage is:
local syntax:arg term:max superscript(term) : term
local macro_rules | `($a:term $b:superscript) => `($a ^ $b)
where superscript(term)
indicates that it will parse a superscript, and the $b:superscript
antiquotation binds the term
argument of the superscript. Given a notation like this,
the expression 2⁶⁴
parses and expands to 2 ^ 64
.
The superscript body is considered to be the longest contiguous sequence of superscript tokens and
whitespace, so no additional bracketing is required (unless you want to separate two superscripts).
However, note that Unicode has a rather restricted character set for superscripts and subscripts
(see Mapping.superscript
and Mapping.subscript
in this file), so you should not use this
parser for complex expressions.
- toNormal : Lean.HashMap Char Char
Map from "special" (e.g. superscript) characters to "normal" characters.
- toSpecial : Lean.HashMap Char Char
Map from "normal" text to "special" (e.g. superscript) characters.
A bidirectional character mapping.
Instances For
Constructs a mapping (intended for compile time use). Panics on violated invariants.
Instances For
A mapping from superscripts to and from regular text.
Instances For
A mapping from subscripts to and from regular text.
Instances For
Collects runs of text satisfying p
followed by whitespace. Fails if the first character does
not satisfy p
. If many
is true, it will parse 1 or more many whitespace-separated runs,
otherwise it will parse only 1. If successful, it passes the result to k
as an array (a, b, c)
where a..b
is a token and b..c
is whitespace.
Instances For
Loop body of satisfyTokensFn
Given a predicate leftOfPartition
which is true for indexes < i
and false for ≥ i
,
returns i
, by binary search.
The core function for super/subscript parsing. It consists of three stages:
- Parse a run of superscripted characters, skipping whitespace and stopping when we hit a non-superscript character.
- Un-superscript the text and pass the body to the inner parser (usually
term
). - Take the resulting
Syntax
object and align all the positions to fit back into the original text (which as a side effect also rewrites all the substrings to be in subscript text).
If many
is false, then whitespace (and comments) are not allowed inside the superscript.
Instances For
Applies the alignment mapping to a position.
Instances For
Applies the alignment mapping to a Substring
.
Instances For
Applies the alignment mapping to a SourceInfo
.
Instances For
Applies the alignment mapping to a Syntax
.
The super/subscript parser.
m
: the character mappingantiquotName
: the name to use for antiquotation bindings$a:antiquotName
. Note that the actual syntax kind bound will be the body kind (parsed byp
), notkind
.errorMsg
: shown when the parser does not matchp
: the inner parser (usuallyterm
), to be called on the body of the superscriptmany
: if false, whitespace is not allowed inside the superscriptkind
: the term will be wrapped in a node with this kind
Instances For
Parenthesizer for the script parser.
Instances For
Formatter for the script parser.
Instances For
The parser superscript(term)
parses a superscript. Basic usage is:
local syntax:arg term:max superscript(term) : term
local macro_rules | `($a:term $b:superscript) => `($a ^ $b)
Given a notation like this, the expression 2⁶⁴
parses and expands to 2 ^ 64
.
Note that because of Unicode limitations, not many characters can actually be typed inside the superscript, so this should not be used for complex expressions. Legal superscript characters:
⁰¹²³⁴⁵⁶⁷⁸⁹ᵃᵇᶜᵈᵉᶠᵍʰⁱʲᵏˡᵐⁿᵒᵖ𐞥ʳˢᵗᵘᵛʷˣʸᶻᴬᴮᴰᴱᴳᴴᴵᴶᴷᴸᴹᴺᴼᴾꟴᴿᵀᵁⱽᵂᵝᵞᵟᵋᶿᶥᶹᵠᵡ⁺⁻⁼⁽⁾
Instances For
Formatter for the superscript parser.
Instances For
Formatter for the superscript parser.
Instances For
The parser subscript(term)
parses a subscript. Basic usage is:
local syntax:arg term:max subscript(term) : term
local macro_rules | `($a:term $i:subscript) => `($a $i)
Given a notation like this, the expression (a)ᵢ
parses and expands to a i
. (Either parentheses
or a whitespace as in a ᵢ
is required, because aᵢ
is considered as an identifier.)
Note that because of Unicode limitations, not many characters can actually be typed inside the subscript, so this should not be used for complex expressions. Legal subscript characters:
₀₁₂₃₄₅₆₇₈₉ₐₑₕᵢⱼₖₗₘₙₒₚᵣₛₜᵤᵥₓᴀʙᴄᴅᴇꜰɢʜɪᴊᴋʟᴍɴᴏᴘꞯʀꜱᴛᴜᴠᴡʏᴢᵦᵧᵨᵩᵪ₊₋₌₍₎
Instances For
Formatter for the subscript parser.
Instances For
Formatter for the subscript parser.