Something went wrong. Try again.
The Monad language. Dependent types, functional programming compiled with LLVM. Hobby project. monad-lang.org
dependent-types language compiler programming-language functional-programming
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260/// Text -> numbers, in pure Monad: strict, whole-string, no trimming.////// `Option`, not `Result`, because these classify a TOKEN rather than parse/// a document -- a YAML plain scalar that is not a number stays a string,/// which is exactly the `none` branch.////// PORTABLE BY CONSTRUCTION: no native is used, and in particular this does/// NOT call `F64.bits_of_string` (its `f64_of_string` native is web-gated,/// `lang/src/codegen/natives.mo`'s `web_only_natives`), so it works on every/// target including wasm. The value is built from F64 literals, a digit/// table and repeated multiplication/division.////// WHY THE ODD SPELLING OF ADDITION: written when `infix (+)` still/// resolved to `I64.add` (`init/src/lib.mo`'s since-removed override)/// and `a + b` on two `F64` values did not check. `+` resolves now/// (through `[Add A] HAdd A A A` and `Add F64`), but the spelling is/// kept: the subtraction form is what the digit-table verification ran/// against. `*`, `-` and `/` dispatch the same way, through the/// `HMul`/`HSub`/`HDiv` bridges and the `Mul`/`Sub`/`Div` instances.////// PRECISION: correctly rounded while the mantissa has at most 19/// significant digits and the decimal exponent is within +/-22 (each power/// of ten is then exact and the single final scale is one IEEE operation)./// Beyond that the result carries a bounded relative error (~1e-15), which/// is what config data needs. Exact `strtod` parity is deliberately not/// claimed.use init::string {}use init::number {}
// ─── Byte helpers ───
/// The decimal value of an ASCII digit byte, or `none`.def Parse.digit_value (b : U8) : Option I64 := if U8.beq b 48u8 then Option.some 0i64 else if U8.beq b 49u8 then Option.some 1i64 else if U8.beq b 50u8 then Option.some 2i64 else if U8.beq b 51u8 then Option.some 3i64 else if U8.beq b 52u8 then Option.some 4i64 else if U8.beq b 53u8 then Option.some 5i64 else if U8.beq b 54u8 then Option.some 6i64 else if U8.beq b 55u8 then Option.some 7i64 else if U8.beq b 56u8 then Option.some 8i64 else if U8.beq b 57u8 then Option.some 9i64 else Option.none
/// One digit as an F64. There is no `Int -> F64` conversion in the/// language, so this table is the bridge the mantissa accumulator uses.def Parse.digit_float (n : I64) : F64 := if I64.beq n 0i64 then 0.0f64 else if I64.beq n 1i64 then 1.0f64 else if I64.beq n 2i64 then 2.0f64 else if I64.beq n 3i64 then 3.0f64 else if I64.beq n 4i64 then 4.0f64 else if I64.beq n 5i64 then 5.0f64 else if I64.beq n 6i64 then 6.0f64 else if I64.beq n 7i64 then 7.0f64 else if I64.beq n 8i64 then 8.0f64 else 9.0f64
/// `a + b` for F64, spelled through subtraction -- see the module doc.def Parse.f64_plus (a : F64) (b : F64) : F64 := a - (0.0f64 - b)
// ─── Integers ───
/// Would `acc * 10 + d` overflow I64? Checked before the multiply, because/// I64 arithmetic wraps silently.def Parse.i64_overflows (acc : I64) (d : I64) : Bool := I64.gt acc (I64.div (I64.sub 9223372036854775807i64 d) 10i64)
/// Magnitude accumulator. `seen` is what rejects an empty digit run (a bare/// `+`, `-` or empty string); a non-digit ends the run with `none`, because/// these parsers require the WHOLE string to be a number.#[partial]def Parse.i64_go (bs : List U8) (acc : I64) (seen : Bool) : Option I64 := match bs { List.empty => if seen then Option.some acc else Option.none, List.cons b rest => match Parse.digit_value b { Option.none => Option.none, Option.some d => let dv : I64 := d in if Parse.i64_overflows acc dv then Option.none else Parse.i64_go rest (I64.add (I64.mul acc 10i64) dv) true, }, }
/// Parse a strict decimal integer: optional `+`/`-`, one or more digits,/// nothing else. Overflow is `none`. `0x`/`0o`/`0b` are not accepted (they/// are not in the YAML 1.2 core schema, and a caller that wants them can/// add a case).#[partial]pub def Parse.i64 (s : String) : Option I64 := match String.to_list s { List.empty => Option.none, List.cons b rest => if U8.beq b 45u8 then Parse.i64_magnitude rest true else if U8.beq b 43u8 then Parse.i64_magnitude rest false else Parse.i64_magnitude (List.cons b rest) false, }
#[partial]def Parse.i64_magnitude (bs : List U8) (neg : Bool) : Option I64 := match Parse.i64_go bs 0i64 false { Option.none => Option.none, Option.some n => Option.some (if neg then I64.neg n else n), }
// ─── Floats ───
/// The scanner's whole state. `phase` is 0 for the integer part, 1 for the/// fraction and 2 for the exponent.struct Parse.Decimal { mant : F64, sig : I64, frac : I64, phase : I64, exp_neg : Bool, exp_signed : Bool, exp_digits : Bool, expv : I64,}
/// The parser state is a pure record of `Copy` scalars, so sharing a/// snapshot across a branch is a bit-copy, not an ownership move.pub instance Copy Parse.Decimal { def copy (d : Parse.Decimal) : Pair Parse.Decimal Parse.Decimal := Pair.pair d d}
def Parse.decimal_init : Parse.Decimal := let d : Parse.Decimal := { mant := 0.0f64, sig := 0i64, frac := 0i64, phase := 0i64, exp_neg := false, exp_signed := false, exp_digits := false, expv := 0i64, } in d
/// Accumulate one byte. Returns `none` for any byte the grammar forbids.def Parse.decimal_step (d : Parse.Decimal) (b : U8) : Option Parse.Decimal := match Parse.digit_value b { Option.some n => if I64.beq d.phase 2i64 then let raw : I64 := I64.add (I64.mul d.expv 10i64) n in let capped : I64 := if I64.gt raw 1000i64 then 1000i64 else raw in let d2 : Parse.Decimal := { d with expv := capped, exp_digits := true } in Option.some d2 else let mant2 : F64 := Parse.f64_plus (d.mant * 10.0f64) (Parse.digit_float n) in let d2 : Parse.Decimal := if I64.beq d.phase 1i64 then { d with mant := mant2, sig := I64.add d.sig 1i64, frac := I64.add d.frac 1i64 } else { d with mant := mant2, sig := I64.add d.sig 1i64 } in Option.some d2, Option.none => if U8.beq b 46u8 then if I64.beq d.phase 0i64 then let d2 : Parse.Decimal := { d with phase := 1i64 } in Option.some d2 else Option.none else if Bool.or (U8.beq b 101u8) (U8.beq b 69u8) then if Bool.and (I64.gt d.sig 0i64) (Bool.or (I64.beq d.phase 0i64) (I64.beq d.phase 1i64)) then let d2 : Parse.Decimal := { d with phase := 2i64 } in Option.some d2 else Option.none else if Bool.or (U8.beq b 43u8) (U8.beq b 45u8) then if Bool.and (I64.beq d.phase 2i64) (Bool.not (Bool.or d.exp_signed d.exp_digits)) then let d2 : Parse.Decimal := { d with exp_neg := U8.beq b 45u8, exp_signed := true } in Option.some d2 else Option.none else Option.none, }
#[partial]def Parse.decimal_fold (bs : List U8) (d : Parse.Decimal) : Option Parse.Decimal := match bs { List.empty => Option.some d, List.cons b rest => match Parse.decimal_step d b { Option.none => Option.none, Option.some d2 => Parse.decimal_fold rest d2, }, }
/// `10^n` for `0 <= n <= 22`, where every such power is EXACTLY/// representable as a double (5^22 < 2^53). Multiplying or dividing by one/// of these is a single correctly-rounded operation -- which is what keeps/// `3.14` from becoming `3.1400000000000001` through two roundings. (Dividing/// 314 by 10 and then by 10 is NOT the same as dividing once by 100.)#[partial]def Parse.pow10_go (n : I64) (acc : F64) : F64 := if I64.gt n 0i64 then Parse.pow10_go (I64.sub n 1i64) (acc * 10.0f64) else acc
def Parse.pow10_exact (n : I64) : F64 := Parse.pow10_go n 1.0f64
/// Multiply/divide `v` by ten `n` times. Within |n| <= 22 this is one exact/// power and one IEEE operation (correctly rounded); beyond it, exact 1e22/// chunks keep the error to a handful of roundings rather than `n` of them.#[partial]def Parse.scale10 (v : F64) (n : I64) : F64 := if I64.gt n 22i64 then Parse.scale10 (v * Parse.pow10_exact 22i64) (I64.sub n 22i64) else if I64.lt n (I64.neg 22i64) then Parse.scale10 (v / Parse.pow10_exact 22i64) (I64.add n 22i64) else if I64.gt n 0i64 then v * Parse.pow10_exact n else if I64.lt n 0i64 then v / Parse.pow10_exact (I64.neg n) else v
def Parse.decimal_finish (d : Parse.Decimal) (neg : Bool) : Option F64 := if I64.gt d.sig 0i64 then if Bool.and (I64.beq d.phase 2i64) (Bool.not d.exp_digits) then Option.none else let e : I64 := if d.exp_neg then I64.neg d.expv else d.expv in let n : I64 := I64.sub e d.frac in let v : F64 := Parse.scale10 d.mant n in Option.some (if neg then 0.0f64 - v else v) else Option.none
#[partial]def Parse.f64_scan (bs : List U8) (neg : Bool) : Option F64 := match Parse.decimal_fold bs Parse.decimal_init { Option.none => Option.none, Option.some d => Parse.decimal_finish d neg, }
/// Parse a strict decimal float: optional sign, an integer part, an/// optional `.` + fraction (either part may be empty, but not both), and an/// optional `[eE]` + optional sign + digits. The whole string must be/// consumed. Non-finite spellings (`.inf`, `.nan`) are NOT accepted here;/// they are a YAML scalar-resolution concern, not a number grammar one.#[partial]pub def Parse.f64 (s : String) : Option F64 := match String.to_list s { List.empty => Option.none, List.cons b rest => if U8.beq b 45u8 then Parse.f64_scan rest true else if U8.beq b 43u8 then Parse.f64_scan rest false else Parse.f64_scan (List.cons b rest) false, }