1.2. Formal Specification🔗

We formalize the validity of input string by the predicate IsWfDecimal (well-formed syntax of the grammar) and the function computeValue (value function).

IsWfDecimal is a direct transcription of the grammar's character-level productions. The building block is IsDigits, which captures Digit⁺ — a non-empty string all of whose characters satisfy Char.isDigit. It lives at the root namespace in Cedar.Thm.Data.String, shared with the duration and datetime grammars:

public def IsDigits (s : String) : Prop :=
  0 < s.length ∧ ∀ c ∈ s.toList, c.isDigit = true

Sign ::= ['-'] is the optional leading minus, common to the signed numeric grammars:

public def IsWfSign (s : String) : Prop :=
  s = "-" ∨ s = ""

And Digit{1,n} refines IsDigits by bounding the run's width from above:

public def IsDigitsUpTo (n : Nat) (s : String) : Prop :=
  IsDigits s ∧ s.length ≤ n

These three predicates — IsDigits, IsWfSign, and IsDigitsUpTo — are the shared vocabulary. The names for the decimal grammar's Natural and Fraction productions stay in its own grammar module.

Natural ::= Digit⁺ is IsDigits under the production's name for readability:

public abbrev IsNatural (s : String) : Prop := IsDigits s

The fraction production is the bounded-digits predicate at the grammar's width, Fraction ::= Digit{1,4}:

public def IsWfFrac (s : String) : Prop :=
  IsDigitsUpTo DECIMAL_DIGITS s

Well-formedness of the whole string then reads straight off the grammar: the string is the rendering of a Sign, a Natural, the '.' separator, and a Fraction, concatenated in that order:

public def IsWfDecimal (s : String) : Prop :=
  ∃ sign natural fraction,
    s = sign ++ natural ++ "." ++ fraction ∧
    IsWfSign sign ∧
    IsNatural natural ∧
    IsWfFrac fraction

This definition talks only about digit characters; it does not mention the string-to-number parsers toInt?'/toNat?'. That keeps well-formedness faithful to the grammar and independent of the parsing implementation.

computeValue follows the grammar's nesting directly. It first peels the outer Sign, then uses String.splitToList to recover Natural and Fraction from the unsigned body:

public def computeValue (s : String) : Option Int :=
  let (sign, body) :=
    if s.front = '-' then ((-1 : Int), (s.drop 1).copy) else (1, s)
  match body.splitToList (· = '.') with
  | [natural, fraction] =>
    match toNat?' natural, toNat?' fraction with
    | some n, some f =>
      some (sign * (n * Int.pow 10 DECIMAL_DIGITS
        + f * Int.pow 10 (DECIMAL_DIGITS - fraction.length)))
    | _, _ => none
  | _ => none