1.3. Parser🔗

Decimal.parse returns some d when the input string is valid, and none otherwise (shown here directly from its source in Cedar.Spec.Ext.Decimal):

public def parse (str : String) : Option Decimal :=
  match str.splitToList (· = '.') with
  | ["-", _] => .none -- guard against bare "-"; redundant on current stdlib (`String.toInt? "-" = none`) but robust to stdlib changes
  | [left, right] =>
    let rlen := right.length
    if 0 < rlen ∧ rlen ≤ DECIMAL_DIGITS
    then
      match toInt?' left, toNat?' right with
      | .some l, .some r =>
        let l' := l * (Int.pow 10 DECIMAL_DIGITS)
        let r' := r * (Int.pow 10 (DECIMAL_DIGITS - rlen))
        let i  := if !left.startsWith "-" then l' + r' else l' - r'
        decimal? i
      | _, _ => .none
    else .none
  | _ => .none

For example:

some 12300#eval Decimal.parse "1.23"        -- valid

some 12300

none#eval Decimal.parse "123"         -- malformed

none

none#eval Decimal.parse "922337203685477.5808" -- overflow

none