Laws of the unit-string grammar (esm-spec §4.8.2)
*,/and juxtaposition are one precedence level, folded LEFT to right (parse_fold), and^/**binds tighter than all three (parse_pow_binds).- A numeric atom other than 1 is a scaling factor wherever it stands
(
parse_scaling_factor_head,parse_scaling_factor_after). -is not an operator (parse_minus_rejected,resolve_minus_rejected).- Whitespace between terms is multiplication (
resolve_space_eq_star). - The table is flat: a single run of identifier characters resolves iff it is a
table key exactly as spelled — no SI-prefix mechanism, no implicit split
(
resolve_ident_run).
Token level
inductive Op
| star | slash | juxt
deriving DecidableEq, Repr
The three spellings of the one precedence level.
def foldOps (acc : UExpr) : List (Op × String) → UExpr
The left fold the spec prescribes.
def NoPowHead (ts : List Tok) : Prop
The token list does not start with ^ or **.
theorem pUnit_fold (a : String) (ops : List (Op × String)) (ts : List Tok) (hts : NoPowHead ts)
(n k : ℕ) (h : 3 * ops.length + k + 3 ≤ n) :
∃ m, k ≤ m ∧ pUnit n (.sym a :: opToks ops ++ ts) = pTail m (foldOps (.sym a) ops) ts
The parse of a, and of pUnit after it, through the left fold.
theorem parse_fold :
∀ (a : String) (ops : List (Op × String)),
parse (.sym a :: opToks ops) = .ok (foldOps (.sym a) ops)
*, / and juxtaposition are ONE precedence level, evaluated LEFT to RIGHT:
any chain of symbols joined by them parses as the left fold. (J/mol*K is
(J/mol)*K; L/mol/s is (L/mol)/s; kg/m*s is (kg/m)*s.)
theorem parse_minus_rejected :
∀ (a : String) (ops : List (Op × String)) (rest : List Tok),
∃ err, parse (.sym a :: opToks ops ++ .minus :: rest) = .error err
- is not an operator: a - after any chain of terms is rejected. (This is
why MOVES’s g/hp-hr does not resolve.)
theorem parse_scaling_factor_head :
∀ (lit : String) (v : ℚ) (i : Bool) (ts : List Tok), lit ≠ "1" →
parse (.num lit v i :: ts) = .error (.scalingFactor lit)
A numeric atom other than the literal 1 is a scaling factor (ruling
Q-104: 01 and 1.0 are too) — at the head of a unit string (1000/s,
0.5 m) …
theorem parse_scaling_factor_after :
∀ (a : String) (ops : List (Op × String)) (op : Tok) (lit : String) (v : ℚ) (i : Bool)
(rest : List Tok), (op = .star ∨ op = .slash) → lit ≠ "1" →
parse (.sym a :: opToks ops ++ op :: .num lit v i :: rest) = .error (.scalingFactor lit)
… and after any chain of terms and an operator ((m/s)^-1/3 reads as
((m/s)^-1)/3: the 3 is a scaling factor, not part of an exponent).
theorem parse_pow_binds :
∀ (a b lit : String) (q : ℚ) (i : Bool) (pw : Tok), (pw = .caret ∨ pw = .dstar) →
parse [.sym a, .slash, .sym b, pw, .num lit q i] = .ok (.div (.sym a) (.pow (.sym b) q)) ∧
parse [.sym a, .slash, .sym b, pw, .minus, .num lit q i] =
.ok (.div (.sym a) (.pow (.sym b) (-q)))
^ and ** bind tighter than / (and *, juxtaposition): a/b^q is
a / (b^q), for a signed or unsigned numeric exponent.
theorem pExp_rational :
∀ (p q : ℕ) (neg : Bool) (lp lq : String) (ts : List Tok), q ≠ 0 →
pExp (.lp :: (if neg then [Tok.minus] else []) ++
.num lp (p : ℚ) true :: .slash :: .num lq (q : ℚ) true :: .rp :: ts)
= .ok ((if neg then -(p : ℚ) else p) / q, ts)
Rational exponents: ^(p/q) and ^(-p/q) are the exponent ±p/q, exactly.
Character level
def IdentRun (a : List Char) : Prop
A run of identifier characters that starts with a letter: what the lexer reads as ONE symbol token.
def RunEnds (rest : List Char) : Prop
The rest after a symbol run: empty or starting with a non-identifier character.
theorem normalizeAux_ascii : ∀ (n : ℕ) (cs : List Char), (∀ x ∈ cs, x.toNat < 128) →
normalizeAux n cs = cs
On ASCII input the Unicode rewrite is the identity.
theorem resolve_ident_run :
∀ a : List Char, IdentRun a → ((∃ u, resolveChars a = .ok u) ↔ String.ofList a ∈ keys)
The table is FLAT, and there is NO SI-prefix mechanism: a run of identifier
characters resolves iff it is a §4.8.1 key exactly as spelled. So mm resolves
because it is a key, and kmolec, nppb, Tm, cm3 do not, because they are
not — nothing composes a prefix with a symbol, or splits a run.
theorem resolves_ident_run :
∀ s : String, IdentRun s.toList → (Resolves s ↔ s ∈ keys)
The same, for strings.
theorem resolve_space_eq_star :
∀ a b : List Char, IdentRun a → IdentRun b →
resolveChars (a ++ ' ' :: b) = resolveChars (a ++ '*' :: b)
WHITESPACE between terms means MULTIPLICATION: a b resolves exactly as
a*b, for any two symbol runs.
theorem resolve_minus_rejected :
∀ a b : List Char, IdentRun a → IdentRun b → ¬ ∃ u, resolveChars (a ++ '-' :: b) = .ok u
- is not an operator, at the string level: a-b never resolves.
The listed exclusions
theorem exclusions_do_not_resolve :
∀ s ∈ ["ton", "t", "d", "in", "yd", "foot", "feet", "mile", "miles", "mph", "tons",
"metric_ton", "short_tons", "gallon", "pound", "kmolec", "nppb", "Tm", "dam", "dg",
"PW", "fs", "cm3", "s2"], ¬ Resolves s
The exclusions §4.8.1 states (no ton, no t, no d; the imperial family is
symbol-only: no in, yd, foot, feet, mile, miles, fused mph; full
spellings only), plus prefixed spellings the flat table does not hold
(kmolec, nppb, Tm, dam, cm3). None of them resolves.
theorem hp_hr_rejected : ¬ Resolves "hp-hr"
hp-hr (MOVES’s spelling of g/hp-hr’s denominator) does not resolve.