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.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419/// String/byte helpers for the `http` mote — Layer 0, pure Monad.////// Ships the small byte-level primitives the URI parser and percent-encoding/// need: a `split_on`, byte predicates, hex (de)coding, and list-slicing/// helpers. The stdlib has no `String.split_on` native, so it lives here./// `Strings` is an empty namespace type (never constructed) so the helpers/// resolve cross-module the same way `Headers.*` does.type Strings {}// ── split_on ────────────────────────────────────────────────────────────def Strings.split_on (delim : String) (s : String) : List String := Strings.split_on_bytes (String.to_list delim) (String.to_list s)def Strings.split_on_bytes (delim : List U8) (input : List U8) : List String := match delim { List.empty => List.singleton (String.from_list input), List.cons _ _ => Strings.split_on_go delim input List.empty }#[terminating]def Strings.split_on_go (delim : List U8) (input : List U8) (acc : List U8) : List String := match input { List.empty => List.singleton (String.from_list (List.reverse acc)), List.cons _ _ => if Strings.list_starts_with delim input then List.cons (String.from_list (List.reverse acc)) (Strings.split_on_go delim (Strings.list_drop_prefix delim input) List.empty) else match input { List.cons x rest => Strings.split_on_go delim rest (List.cons x acc) } }// ── list slicing ───────────────────────────────────────────────────────def Strings.list_starts_with (prefix : List U8) (xs : List U8) : Bool := match prefix { List.empty => true, List.cons p ps => match xs { List.empty => false, List.cons x xs2 => if U8.beq p x then Strings.list_starts_with ps xs2 else false } }def Strings.list_drop_prefix (prefix : List U8) (xs : List U8) : List U8 := match prefix { List.empty => xs, List.cons _ ps => match xs { List.empty => List.empty, List.cons _ xs2 => Strings.list_drop_prefix ps xs2 } }#[terminating]def Strings.drop_bytes (n : I64) (xs : List U8) : List U8 := if I64.beq n 0 then xs else match xs { List.empty => List.empty, List.cons _ rest => Strings.drop_bytes (I64.sub n 1) rest }def Strings.split_at_byte (c : U8) (bytes : List U8) : Pair (List U8) (List U8) := Strings.split_at_byte_go c bytes List.emptydef Strings.split_at_byte_go (c : U8) (bytes : List U8) (acc : List U8) : Pair (List U8) (List U8) := match bytes { List.empty => Pair.pair (List.reverse acc) List.empty, List.cons x rest => if U8.beq x c then Pair.pair (List.reverse acc) rest else Strings.split_at_byte_go c rest (List.cons x acc) }def Strings.split_at_byte_opt (c : U8) (bytes : List U8) : Option (Pair (List U8) (List U8)) := Strings.split_at_byte_opt_go c bytes List.emptydef Strings.split_at_byte_opt_go (c : U8) (bytes : List U8) (acc : List U8) : Option (Pair (List U8) (List U8)) := match bytes { List.empty => Option.none, List.cons x rest => if U8.beq x c then Option.some (Pair.pair (List.reverse acc) rest) else Strings.split_at_byte_opt_go c rest (List.cons x acc) }def Strings.option_from (bs : List U8) : Option String := match bs { List.empty => Option.none, List.cons _ _ => Option.some (String.from_list bs) }// ── byte predicates ────────────────────────────────────────────────────def Strings.is_upper_alpha (b : U8) : Bool := if U8.lt b 65u8 then false else U8.lt b 91u8def Strings.is_lower_alpha (b : U8) : Bool := if U8.lt b 97u8 then false else U8.lt b 123u8def Strings.is_alpha (b : U8) : Bool := if Strings.is_upper_alpha b then true else Strings.is_lower_alpha bdef Strings.is_digit (b : U8) : Bool := if U8.lt b 48u8 then false else U8.lt b 58u8def Strings.is_alnum (b : U8) : Bool := if Strings.is_alpha b then true else Strings.is_digit b/// RFC 3986 unreserved: ALPHA / DIGIT / "-" / "." / "_" / "~"def Strings.is_unreserved (b : U8) : Bool := if Strings.is_alnum b then true else if U8.beq b 45u8 then true else if U8.beq b 46u8 then true else if U8.beq b 95u8 then true else U8.beq b 126u8def Strings.is_scheme_char (b : U8) : Bool := if Strings.is_alnum b then true else if U8.beq b 43u8 then true else if U8.beq b 45u8 then true else U8.beq b 46u8def Strings.is_valid_scheme (bytes : List U8) : Bool := match bytes { List.empty => false, List.cons first rest => if Strings.is_alpha first then Strings.is_valid_scheme_rest rest else false }def Strings.is_valid_scheme_rest (bytes : List U8) : Bool := match bytes { List.empty => true, List.cons b rest => if Strings.is_scheme_char b then Strings.is_valid_scheme_rest rest else false }// ── hex ─────────────────────────────────────────────────────────────────def Strings.hex_char_of_nibble (n : U8) : U8 := if U8.lt n 10u8 then U8.add n 48u8 else U8.add n 55u8def Strings.hex_value (c : U8) : Option U8 := if U8.lt c 48u8 then Option.none else if U8.lt c 58u8 then Option.some (U8.sub c 48u8) else if U8.lt c 65u8 then Option.none else if U8.lt c 71u8 then Option.some (U8.sub c 55u8) else if U8.lt c 97u8 then Option.none else if U8.lt c 103u8 then Option.some (U8.sub c 87u8) else Option.nonedef Strings.decode_hex_pair (h1 : U8) (h2 : U8) : Result String U8 := match Strings.hex_value h1 { Option.none => Result.err "invalid hex digit", Option.some v1 => match Strings.hex_value h2 { Option.none => Result.err "invalid hex digit", Option.some v2 => Result.ok (U8.add (U8.mul v1 16u8) v2) } }// ── base64 ──────────────────────────────────────────────────────────────// RFC 4648 §4 decoding, for `Middleware.auth_basic`: the HTTP Basic// credential is base64 (RFC 7617), so a predicate that claims to see the// decoded "user:pass" has to actually decode it. Strict rather than// permissive — the input must be a whole number of 4-character groups,// `=` may appear only as the last one or two characters, and the bits a// padded group leaves over must be zero (the canonical encoding). A// malformed credential is a rejection, not a best-effort guess./// Value of a base64 alphabet character (the standard alphabet of RFC/// 4648 §4), or `Option.none` for anything outside it — including `=`,/// which the group decoder treats as padding rather than as a value.def Strings.base64_value (c : U8) : Option U8 := if U8.beq c 43u8 then Option.some 62u8 // '+' else if U8.beq c 47u8 then Option.some 63u8 // '/' else if Strings.is_digit c then Option.some (U8.add (U8.sub c 48u8) 52u8) else if Strings.is_upper_alpha c then Option.some (U8.sub c 65u8) else if Strings.is_lower_alpha c then Option.some (U8.add (U8.sub c 97u8) 26u8) else Option.none/// `x mod m`, as `x - (x/m)*m`: this language's `U8` has no remainder/// operation (nor any shift or bitwise one), so the bit arithmetic of/// base64 is written as multiplication and division throughout.def Strings.u8_mod (x : U8) (m : U8) : U8 := U8.sub x (U8.mul (U8.div x m) m)/// First byte of a 4-character group: `v1`'s 6 bits, then the top 2 of/// `v2`.def Strings.base64_byte1 (v1 : U8) (v2 : U8) : U8 := U8.add (U8.mul v1 4u8) (U8.div v2 16u8)/// Second byte: `v2`'s low 4 bits, then the top 4 of `v3`.def Strings.base64_byte2 (v2 : U8) (v3 : U8) : U8 := U8.add (U8.mul (Strings.u8_mod v2 16u8) 16u8) (U8.div v3 4u8)/// Third byte: `v3`'s low 2 bits, then all 6 of `v4`.def Strings.base64_byte3 (v3 : U8) (v4 : U8) : U8 := U8.add (U8.mul (Strings.u8_mod v3 4u8) 64u8) v4/// Decode a whole base64 string to the bytes it encodes.def Strings.base64_decode (s : String) : Result String (List U8) := Strings.base64_decode_go (String.to_list s) List.empty/// Walk the input 4 characters at a time, collecting decoded bytes in/// `out` (REVERSED — the caller flips it once at the end). A run that is/// not a whole number of groups is a `Result.err`, not a short read.#[terminating]def Strings.base64_decode_go (xs : List U8) (out : List U8) : Result String (List U8) := match xs { List.empty => Result.ok (List.reverse out), List.cons c1 r1 => match r1 { List.empty => Strings.base64_length_err, List.cons c2 r2 => match r2 { List.empty => Strings.base64_length_err, List.cons c3 r3 => match r3 { List.empty => Strings.base64_length_err, List.cons c4 r4 => Strings.base64_group c1 c2 c3 c4 r4 out } } } }def Strings.base64_length_err : Result String (List U8) := Result.err "base64: length is not a multiple of 4"def Strings.base64_char_err : Result String (List U8) := Result.err "base64: invalid character"def Strings.base64_pad_err : Result String (List U8) := Result.err "base64: data after the padding"def Strings.base64_canonical_err : Result String (List U8) := Result.err "base64: non-canonical padding bits"/// Decode one 4-character group. A trailing `=` makes it the LAST group:/// `xx==` is one byte and `xxx=` is two, and anything after it is an/// error (RFC 4648 §4 allows padding only at the end).////// `#[terminating]`: this and `base64_decode_go` call each other, so/// neither is structurally recursive on its own — the descent is real/// (`rest` is strictly shorter every time), but it alternates between/// the two.#[terminating]def Strings.base64_group (c1 : U8) (c2 : U8) (c3 : U8) (c4 : U8) (rest : List U8) (out : List U8) : Result String (List U8) := if U8.beq c4 61u8 then match rest { List.cons _ _ => Strings.base64_pad_err, List.empty => Strings.base64_group_padded c1 c2 c3 out } else match Strings.base64_value c1 { Option.none => Strings.base64_char_err, Option.some v1 => match Strings.base64_value c2 { Option.none => Strings.base64_char_err, Option.some v2 => match Strings.base64_value c3 { Option.none => Strings.base64_char_err, Option.some v3 => match Strings.base64_value c4 { Option.none => Strings.base64_char_err, Option.some v4 => Strings.base64_decode_go rest (List.cons (Strings.base64_byte3 v3 v4) (List.cons (Strings.base64_byte2 v2 v3) (List.cons (Strings.base64_byte1 v1 v2) out))) } } } }/// A group ending in one or two `=` characters (its 4th is already known/// to be one). The unused low bits of the last real character must be/// zero — `AA==` is canonical, `AB==` is not — and `AAA=`/`AAB=` differ/// the same way.def Strings.base64_group_padded (c1 : U8) (c2 : U8) (c3 : U8) (out : List U8) : Result String (List U8) := match Strings.base64_value c1 { Option.none => Strings.base64_char_err, Option.some v1 => match Strings.base64_value c2 { Option.none => Strings.base64_char_err, Option.some v2 => if U8.beq c3 61u8 then if U8.beq (Strings.u8_mod v2 16u8) 0u8 then Result.ok (List.reverse (List.cons (Strings.base64_byte1 v1 v2) out)) else Strings.base64_canonical_err else match Strings.base64_value c3 { Option.none => Strings.base64_char_err, Option.some v3 => if U8.beq (Strings.u8_mod v3 4u8) 0u8 then Result.ok (List.reverse (List.cons (Strings.base64_byte2 v2 v3) (List.cons (Strings.base64_byte1 v1 v2) out))) else Strings.base64_canonical_err } } }/// Map an ASCII digit byte ('0'..'9') to a U16, or none for non-digits./// The stdlib has no U8→U16 conversion, so the 10 cases are explicit.def Strings.u16_of_digit (d : U8) : Option U16 := if U8.beq d 48u8 then Option.some 0u16 else if U8.beq d 49u8 then Option.some 1u16 else if U8.beq d 50u8 then Option.some 2u16 else if U8.beq d 51u8 then Option.some 3u16 else if U8.beq d 52u8 then Option.some 4u16 else if U8.beq d 53u8 then Option.some 5u16 else if U8.beq d 54u8 then Option.some 6u16 else if U8.beq d 55u8 then Option.some 7u16 else if U8.beq d 56u8 then Option.some 8u16 else if U8.beq d 57u8 then Option.some 9u16 else Option.none// ── bounded decimal parsing ─────────────────────────────────────────────//// `u16_of_digit` gives a digit's value; these turn a digit run into a number,// and they are the only place a byte list becomes a `U16` or an `I64`. Both// bound the value BEFORE multiplying, so no intermediate ever leaves the// target range. An unbounded `U16.mul acc 10u16` truncates silently instead --// `"70000"` accumulated to `4464`, which is how an out-of-range port became a// plausible wrong one rather than an error./// Would `acc * 10 + digit` exceed 65535?////// Checked before multiplying, so `acc` itself never leaves `U16` range:/// `acc <= 6552` always fits, and `acc == 6553` fits only while the next digit/// is at most 5. The largest intermediate is `6553 * 10 + 9 = 65539`, which is/// why this is safe even though the comparison happens in `U16`.def Strings.u16_overflows (acc : U16) (digit : U16) : Bool := if U16.gt acc 6553u16 then true else if U16.beq acc 6553u16 then U16.gt digit 5u16 else false/// Parse a run of decimal digits into a `U16`. Fails on an empty run, on a/// non-digit, and on any value above 65535. `label` names the field so each/// caller keeps its own wording ("port", "status").def Strings.parse_u16_bounded (label : String) (bytes : List U8) : Result String U16 := match bytes { List.empty => Result.err (String.concat label " is empty"), List.cons _ _ => Strings.parse_u16_bounded_go label bytes 0u16 }#[terminating]def Strings.parse_u16_bounded_go (label : String) (bytes : List U8) (acc : U16) : Result String U16 := match bytes { List.empty => Result.ok acc, List.cons d rest => match Strings.u16_of_digit d { Option.none => Result.err (String.concat "invalid " (String.concat label " digit")), Option.some v => if Strings.u16_overflows acc v then Result.err (String.concat label " out of range") else Strings.parse_u16_bounded_go label rest (U16.add (U16.mul acc 10u16) v) } }/// Map an ASCII digit byte ('0'..'9') to I64 (no U8→I64 conversion exists).def Strings.i64_of_digit (d : U8) : Option I64 := if U8.beq d 48u8 then Option.some 0i64 else if U8.beq d 49u8 then Option.some 1i64 else if U8.beq d 50u8 then Option.some 2i64 else if U8.beq d 51u8 then Option.some 3i64 else if U8.beq d 52u8 then Option.some 4i64 else if U8.beq d 53u8 then Option.some 5i64 else if U8.beq d 54u8 then Option.some 6i64 else if U8.beq d 55u8 then Option.some 7i64 else if U8.beq d 56u8 then Option.some 8i64 else if U8.beq d 57u8 then Option.some 9i64 else Option.none/// Would `acc * 10 + digit` exceed 9223372036854775807? The same pre-multiply/// discipline as `u16_overflows`, against `I64.max`.def Strings.i64_overflows (acc : I64) (digit : I64) : Bool := if I64.gt acc 922337203685477580i64 then true else if I64.beq acc 922337203685477580i64 then I64.gt digit 7i64 else false/// Parse a trimmed run of decimal digits into an `I64`. `Option.none` on an/// empty run, on a non-digit, and on a value that would leave `I64` range --/// so an absurd `Content-Length` is rejected rather than wrapping into a/// plausible small one.def Strings.parse_i64 (s : String) : Option I64 := let bytes := String.to_list (String.trim s) in if List.is_empty bytes then Option.none else Strings.parse_i64_go bytes 0i64#[terminating]def Strings.parse_i64_go (bytes : List U8) (acc : I64) : Option I64 := match bytes { List.empty => Option.some acc, List.cons d rest => match Strings.i64_of_digit d { Option.none => Option.none, Option.some v => if Strings.i64_overflows acc v then Option.none else Strings.parse_i64_go rest (I64.add (I64.mul acc 10i64) v) } }