The unit-string grammar (esm-spec §4.8.2)

Lean module Esm.Units.Grammar, formal/Esm/Units/Grammar.lean at 184aa13d35e5
Imports Esm.Units.Registry

A unit string is resolved in four steps, each a function here:

normalize — the mandatory Unicode rewrite, applied BEFORE parsing.
lex — tokens. A symbol is a maximal run of identifier characters ([A-Za-z0-9_]); a run of digits alone (optionally digits.digits) is a number; % is a one-character symbol; whitespace separates tokens and is otherwise dropped.
parse — the grammar, to a syntax tree UExpr:
```
unit     := term (('*' | '/')? term)*
term     := atom (('^' | '**') exponent)?
exponent := integer | decimal | '(' integer '/' integer ')'
atom     := '1' | symbol | '(' unit ')'
```
*, / and juxtaposition are one precedence level, folded left to right. A numeric atom whose value is not 1 is a scaling factor and an error.
UExpr.eval — look each symbol up in the flat table and compose.

Readings chosen where §4.8.2 admits more than one are listed in the phase-1 report (the lexing of a run such as s1, a lone % inside a run, numeric atoms spelled 1.0, whitespace-only strings, whitespace inside a term).

Errors

def scalingFactorText source

def scalingFactorText : String

The two phrases §4.8.2 requires in the scaling-factor diagnostic.

Unicode normalisation

def supDigit source

def supDigit (c : Char) : Option Char

The ASCII digit of a superscript digit.

def supRun source

def supRun (cs : List Char) : List Char × List Char

The leading run of superscript digits, transliterated, and the rest.

def normalizeAux source

def normalizeAux : Nat → List Char → List Char

The §4.8.2 rewrite table, applied left to right.

Tokens

def isIdent source

def isIdent (c : Char) : Bool

Characters that may occur in a symbol run.

Syntax trees and the parser

def pInt source

def pInt : List Tok → Option (ℚ × List Tok)

'-'? integer.

def pExp source

def pExp : List Tok → Except Err (ℚ × List Tok)

exponent := integer | decimal | '(' integer '/' integer ')' (signs allowed).

def startsTerm source

def startsTerm : List Tok → Bool

Does the token list begin a term (an atom)?

def pTail source

def pTail : Nat → UExpr → List Tok → Except Err (UExpr × List Tok)

The left fold acc (op term)*.

def parse source

def parse (ts : List Tok) : Except Err UExpr

Parse a whole token list.

Evaluation and resolution

def resolveChars source

def resolveChars (cs : List Char) : Except Err U

Resolve a unit string given as characters. The empty string is the dimensionless key "".

def resolve source

def resolve (s : String) : Except Err U

Resolve a unit string (§4.8.1 table + §4.8.2 grammar).

def Resolves source

def Resolves (s : String) : Prop

Does the string resolve?