{- Awsum standard prelude. Types and functions visible to every module
   without import. Architectural design: docs/prelude.md.

   The file is embedded in the compiler binary at build time. It has no
   `main` by design — the entry-point is a module concern, not a
   prelude one. -}

-- ---------------------- String

{- Concatenate two strings. Fails with `StringTooLong` if the result
   would exceed `maxStringLengthUtf16CodeUnits`. -}
(++) : String -> String -> Either StringTooLong String
(++) a b = BuiltIn.concatString a b

{- Split at the first occurrence of `separator`. Returns
   `Just (Tuple2 prefix suffix)` such that
   `prefix ++ separator ++ suffix == str`, or `Nothing` if `separator`
   does not appear in `str`. Matching is byte-level — for ASCII that
   is irrelevant, but a single-byte separator can land inside a
   multi-byte UTF-8 codepoint.

   Corner cases:
   - `splitOnFirst "" "abc"`     → `Just (Tuple2 "" "abc")` (empty separator matches at position 0)
   - `splitOnFirst ":" ":foo"`   → `Just (Tuple2 "" "foo")` (separator at start)
   - `splitOnFirst ":" "foo:"`   → `Just (Tuple2 "foo" "")` (separator at end)
   - `splitOnFirst "abc" "abc"`  → `Just (Tuple2 "" "")`
   - `splitOnFirst "abcde" "ab"` → `Nothing` (separator longer than string) -}
splitOnFirst : String -> String -> Maybe (Tuple2 String String)
splitOnFirst = BuiltIn.splitOnFirst

{- The string-length API is three explicit functions, not one `length`.
   Each name spells out the unit it counts; picking the wrong one
   silently produces wrong answers for any string with a surrogate
   pair. -}

{- Number of Unicode code points. A supplementary-plane character (e.g.
   `🔥`, U+1F525) counts as 1, not 2 UTF-16 code units, not 4 UTF-8
   bytes. Grapheme clusters (combining marks, ZWJ sequences) are wider
   still and not counted by any function in this family. -}
lengthCodePoints : String -> UInt32
lengthCodePoints = BuiltIn.lengthCodePoints

{- Number of UTF-16 code units. BMP characters count as 1; supplementary
   characters as 2 (surrogate pair). Equal to `String.length` on
   JVM/CLR/JS where strings are stored as UTF-16. -}
lengthUtf16CodeUnits : String -> UInt32
lengthUtf16CodeUnits = BuiltIn.lengthUtf16CodeUnits

{- Number of bytes when encoded as UTF-8 (RFC 3629). ASCII = 1,
   U+0080..U+07FF = 2, U+0800..U+FFFF = 3, U+10000..U+10FFFF = 4. -}
lengthUtf8Bytes : String -> UInt32
lengthUtf8Bytes = BuiltIn.lengthUtf8Bytes

{- Equality on `String`: `True` iff both strings have the same sequence
   of UTF-16 code units. Matches `String.equals` on the JVM,
   `String.Equals` on the CLR, and `===` in JS. -}
eqString : String -> String -> Bool
eqString = BuiltIn.eqString

{- Maximum string length in UTF-16 code units, identical on every
   backend. Operations producing a longer string return
   `Left StringTooLong`. Value `2^27 = 134_217_728`. Pinned by the
   WASM-32 budget (see docs/targets.md), not the smallest UTF-16
   runtime. -}
maxStringLengthUtf16CodeUnits : UInt32
maxStringLengthUtf16CodeUnits = 134_217_728

-- ---------------------- Unit

{- The unit type — exactly one value, also written `Unit`. Used wherever
   a function or effect has no meaningful result to return: most
   visibly in `IO Never Unit` for an action whose whole purpose is its
   side effect. -}
type Unit = Unit

{- Render the `Unit` value as the literal string `"Unit"`. -}
showUnit : Unit -> String
showUnit _ = "Unit"

-- ---------------------- Never

{- The empty type — no constructors, no values. Declared with
   `empty type` to mark it as the row identity: a value of any
   `empty type` (none exist at runtime) flows into any expected row
   position via row-subsumption. Most visible in `IO Never a`, meaning
   an IO action that cannot fail.

   Plain `type X` (no `empty`) declares a /distinct/ row label that
   may happen to be uninhabited — use that for phantom markers that
   must not collapse with `Never`. -}
empty type Never

-- ---------------------- Bool

{- Truth value: `True` or `False`. Awsum has no implicit boolean coercion
   — `if`-like conditionals are written as `case` on a `Bool`. -}
type Bool = True | False

{- Logical negation: turns `True` into `False` and `False` into `True`. -}
not : Bool -> Bool
not b = case b of
  True -> False
  False -> True

{- Logical conjunction: returns the second argument when the first is
   `True`, otherwise `False`. Both arguments are always evaluated —
   there is no short-circuit, because Awsum has no side effects whose
   suppression would be observable. -}
and : Bool -> Bool -> Bool
and a b = case a of
  True -> b
  False -> False

{- Logical disjunction: returns `True` when the first argument is `True`,
   otherwise the second argument. Both arguments are always evaluated. -}
or : Bool -> Bool -> Bool
or a b = case a of
  True -> True
  False -> b

{- Render a boolean as the literal string `"True"` or `"False"`. -}
showBool : Bool -> String
showBool b = case b of
  True -> "True"
  False -> "False"

-- ---------------------- Either

{- A `Left` carrying an error / failure, or a `Right` carrying a
   success. Honest-arithmetic and other total-but-effectful primitives
   report failure this way; no exceptions, no sentinels. -}
type Either a b = Left a | Right b

{- Chain two Either-returning operations. Error rows union: `e1` of the
   first and `e2` of the continuation become `(e1 | e2)` in the result.
   The `do` block desugars through this function. -}
bindEither : Either e1 a -> (a -> Either e2 b) -> Either (e1 | e2) b
bindEither x k = case x of
  Left e -> Left e
  Right a -> k a

{- Lift a value into `Either` on the `Right` side. -}
pureEither : a -> Either e a
pureEither x = Right x

{- Chain two Either-returning operations in continuation-first order:
   takes the continuation, then the value to feed it. Error rows union
   in the result `(e1 | e2)`. Pairs with `|>` for left-to-right reads
   (`x |> andThenEither k`). -}
andThenEither : (a -> Either e2 b) -> Either e1 a -> Either (e1 | e2) b
andThenEither k x = case x of
  Left e -> Left e
  Right a -> k a

{- Returns its first argument, ignores the second. Used by the
   `do`-notation desugarer to express continuations whose bound
   variable is unused. -}
const : a -> b -> a
const x _y = x

{- Apply `f` to the success value; leave the error untouched. -}
mapRight : Either e a -> (a -> b) -> Either e b
mapRight x f = case x of
  Left e -> Left e
  Right a -> Right (f a)

{- Apply `f` to the error value; leave the success untouched. Used to
   widen / narrow / rename a nominal error type without touching the
   success side. -}
mapLeft : Either e1 a -> (e1 -> e2) -> Either e2 a
mapLeft x f = case x of
  Left e -> Left (f e)
  Right a -> Right a

{- Convert a `Maybe a` to an `Either e a`, supplying the error to use
   on `Nothing`. `Just a` becomes `Right a`; `Nothing` becomes
   `Left e`. Lets `Maybe`-returning helpers (`headList`, `tailList`,
   `splitOnFirst`) chain inside a `do`-block on `Either`. -}
nothingAsLeft : e -> Maybe a -> Either e a
nothingAsLeft e m = case m of
  Nothing -> Left e
  Just a -> Right a

-- ---------------------- IO

{- A description of an effect that the runtime may execute. An
   `IO e a` value is **data** — constructing it does not perform any
   effect; the effect happens only when the runtime walks the IO tree
   returned from `main`. So
   `let _ = IO.Stdout.print "ignored" in IO.Stdout.print "real"`
   prints only `real`.

   The error row `e` works like `Either`'s: primitives that can fail
   declare it explicitly. `main` requires `IO Never Unit`; any
   `IO e _` with non-empty `e` must be reduced to `IO Never _` first
   (typically via `handleErrorIO`).

   Direct pattern-matching on the constructors works today but is **not
   part of the stable API**: new effects add new constructors, breaking
   existing case-matches (no catch-all by language design). Use
   `bindIO` / `mapIO` / `pureIO` and the platform built-ins for
   composition; direct matching is for first-party tooling that updates
   in lockstep with the compiler. -}
type IO e a
  = IOPure a
  | IOFail e
  | IOStdoutPrint String (IO e a)
  | IOGetArgs (Either (StringTooLong | UnpairedUtf16Surrogate) (List String) -> IO e a)
  | IOStdinReadAllString (Either (StringTooLong | InvalidUtf8) String -> IO e a)
  | IOStdinReadAllBytes (List UInt8 -> IO e a)

{- Lift a pure value into IO. -}
pureIO : a -> IO e a
pureIO x = IOPure x

{- Lift a failure value into IO. Useful for re-throwing inside a
   `handleErrorIO` handler that only closes part of an error row. -}
failIO : e -> IO e a
failIO e = IOFail e

{- Sequence two IO actions: run the first, feed its success value into
   a continuation producing the second. The error row of the result is
   the union `(e1 | e2)` of the two inputs' rows. If the first action
   fails, the continuation is not called and its failure is propagated
   unchanged. -}
bindIO : IO e1 a -> (a -> IO e2 b) -> IO (e1 | e2) b
bindIO io k = case io of
  IOPure a -> k a
  IOFail e -> IOFail e
  IOStdoutPrint s next -> IOStdoutPrint s (bindIO next k)
  IOGetArgs cont -> IOGetArgs (bindIOAfterArgs cont k)
  IOStdinReadAllString cont -> IOStdinReadAllString (bindIOAfterStdinString cont k)
  IOStdinReadAllBytes cont -> IOStdinReadAllBytes (bindIOAfterStdinBytes cont k)

{- Internal helper for `bindIO`'s `IOGetArgs` arm; top-level so the
   typechecker pins `cont`'s type via the signature. -}
bindIOAfterArgs : (Either (StringTooLong | UnpairedUtf16Surrogate) (List String) -> IO e1 a) -> (a -> IO e2 b) -> Either (StringTooLong | UnpairedUtf16Surrogate) (List String) -> IO (e1 | e2) b
bindIOAfterArgs cont k result = bindIO (cont result) k

{- Internal helper for `bindIO`'s `IOStdinReadAllString` arm; top-level
   so the typechecker pins `cont`'s type via the signature. -}
bindIOAfterStdinString : (Either (StringTooLong | InvalidUtf8) String -> IO e1 a) -> (a -> IO e2 b) -> Either (StringTooLong | InvalidUtf8) String -> IO (e1 | e2) b
bindIOAfterStdinString cont k result = bindIO (cont result) k

{- Internal helper for `bindIO`'s `IOStdinReadAllBytes` arm; top-level
   so the typechecker pins `cont`'s type via the signature. The raw-byte
   read cannot fail on content, so the continuation takes a bare
   `List UInt8` rather than an `Either`. -}
bindIOAfterStdinBytes : (List UInt8 -> IO e1 a) -> (a -> IO e2 b) -> List UInt8 -> IO (e1 | e2) b
bindIOAfterStdinBytes cont k bytes = bindIO (cont bytes) k

{- Sequence two IO actions in continuation-first order: takes the
   continuation, then the IO value to feed it. The error row of the
   result is the union `(e1 | e2)`. Pairs with `|>` for left-to-right
   chains (`io |> andThenIO k`). -}
andThenIO : (a -> IO e2 b) -> IO e1 a -> IO (e1 | e2) b
andThenIO k io = case io of
  IOPure a -> k a
  IOFail e -> IOFail e
  IOStdoutPrint s next -> IOStdoutPrint s (andThenIO k next)
  IOGetArgs cont -> IOGetArgs (\result -> andThenIO k (cont result))
  IOStdinReadAllString cont -> IOStdinReadAllString (\result -> andThenIO k (cont result))
  IOStdinReadAllBytes cont -> IOStdinReadAllBytes (\bytes -> andThenIO k (cont bytes))

{- Apply `f` to the success value of an IO action; leave the error row
   and the surrounding effect tree alone. The action structure is
   preserved end to end — only the final pure result is transformed. -}
mapIO : IO e a -> (a -> b) -> IO e b
mapIO io f = case io of
  IOPure a -> IOPure (f a)
  IOFail e -> IOFail e
  IOStdoutPrint s next -> IOStdoutPrint s (mapIO next f)
  IOGetArgs cont -> IOGetArgs (\result -> mapIO (cont result) f)
  IOStdinReadAllString cont -> IOStdinReadAllString (\result -> mapIO (cont result) f)
  IOStdinReadAllBytes cont -> IOStdinReadAllBytes (\bytes -> mapIO (cont bytes) f)

{- Apply `f` to the failure value of an IO action; leave the success
   and effect tree alone. Used to widen / narrow / rename the error row. -}
mapIOError : IO e1 a -> (e1 -> e2) -> IO e2 a
mapIOError io f = case io of
  IOPure a -> IOPure a
  IOFail e -> IOFail (f e)
  IOStdoutPrint s next -> IOStdoutPrint s (mapIOError next f)
  IOGetArgs cont -> IOGetArgs (\result -> mapIOError (cont result) f)
  IOStdinReadAllString cont -> IOStdinReadAllString (\result -> mapIOError (cont result) f)
  IOStdinReadAllBytes cont -> IOStdinReadAllBytes (\bytes -> mapIOError (cont bytes) f)

{- Route `IOFail` through a recovery handler. The handler may fully
   recover (return `IO Never a`), partially handle (return an IO with
   only re-thrown labels in its error row), or rename the failure type.
   Pairs with `|>` at the tail of a chain: `io |> handleErrorIO h`. -}
handleErrorIO : (e1 -> IO e2 a) -> IO e1 a -> IO e2 a
handleErrorIO h io = case io of
  IOPure a -> IOPure a
  IOFail e -> h e
  IOStdoutPrint s next -> IOStdoutPrint s (handleErrorIO h next)
  IOGetArgs cont -> IOGetArgs (\result -> handleErrorIO h (cont result))
  IOStdinReadAllString cont -> IOStdinReadAllString (\result -> handleErrorIO h (cont result))
  IOStdinReadAllBytes cont -> IOStdinReadAllBytes (\bytes -> handleErrorIO h (cont bytes))

{- Walk the IO tree returned from `main` and perform the effects in
   order. Called by per-target entry-point glue; user code never calls
   this directly. The `IOFail` arm is unreachable because `main` is
   `IO Never Unit` and `Never` is uninhabited. -}
runIO : IO Never Unit -> Unit
runIO io = case io of
  IOPure u -> u
  IOStdoutPrint s next -> case BuiltIn.internalStdoutPrint s of
    Unit -> runIO next
  IOGetArgs cont -> runIO (cont BuiltIn.internalGetArgs)
  IOStdinReadAllString cont -> runIO (cont BuiltIn.internalStdinReadAllString)
  IOStdinReadAllBytes cont -> runIO (cont BuiltIn.internalStdinReadAllBytes)

{- Lift an `Either` into IO: `Left` becomes a failed action, `Right` a
   pure success. The error row `e` carries over unchanged, so a fallible
   pure computation drops into an IO chain and composes with `bindIO` /
   `handleErrorIO` like any other action. -}
eitherToIO : Either e a -> IO e a
eitherToIO x = case x of
  Left e -> failIO e
  Right a -> pureIO a

-- ---------------------- Maybe

{- Optional value: `Just x` carries a payload, `Nothing` doesn't. For
   computations that legitimately produce "no result" without that
   being an error (e.g. a lookup). When the /reason/ for no value
   matters, reach for `Either` instead. -}
type Maybe a = Nothing | Just a

-- ---------------------- List

{- Singly-linked list: either empty (`Nil`) or a head `a` followed by a
   `List a` tail. The minimum needed to represent a sequence of values
   without committing to a literal syntax or a particular set of
   helpers — operate on it with ordinary recursion (the compiler lowers
   self- and mutually-recursive walks to stack-safe loops on every
   backend).

   No `[1, 2, 3]` syntax and no `(::)` infix constructor exist today:
   build values with explicit `Cons h t` and `Nil`. -}
type List a = Nil | Cons a (List a)

{- First element, or `Nothing` for the empty list. -}
headList : List a -> Maybe a
headList xs = case xs of
  Nil -> Nothing
  Cons h _t -> Just h

{- All elements except the first, or `Nothing` for the empty list. -}
tailList : List a -> Maybe (List a)
tailList xs = case xs of
  Nil -> Nothing
  Cons _h t -> Just t

-- ---------------------- Tuple2

{- A pair. Use for functions that produce two results without obvious
   names for them (e.g. `splitOnFirst` returning prefix and suffix).
   When the fields have meaningful names, prefer a domain-specific
   single-constructor sum (`type RangeI32 = RangeI32 Int32 Int32`). -}
type Tuple2 a b = Tuple2 a b

-- ---------------------- Tuple3

{- A triple. Use for functions producing three results that genuinely
   don't have meaningful names. For named fields, prefer a domain-
   specific single-constructor sum like
   `type ColumnSummary = ColumnSummary Int32 Int32 Int32`. -}
type Tuple3 a b c = Tuple3 a b c

-- ---------------------- UnderflowError

{- Reported when an integer result would leave the declared type's
   range on the low end (e.g. `predInt32 minInt32`). -}
type UnderflowError = UnderflowError

{- Render the `UnderflowError` value as the literal string
   `"UnderflowError"`. The type is nullary, so there is only ever one
   value to render. -}
showUnderflowError : UnderflowError -> String
showUnderflowError _ = "UnderflowError"

-- ---------------------- OverflowError

{- Reported when an integer result would exceed the declared type's
   range (e.g. `succInt32 maxInt32`). -}
type OverflowError = OverflowError

{- Render the `OverflowError` value as the literal string
   `"OverflowError"`. The type is nullary, so there is only ever one
   value to render. -}
showOverflowError : OverflowError -> String
showOverflowError _ = "OverflowError"

-- ---------------------- StringTooLong

{- Reported by string operations (`(++)`, future input parsing) when
   the resulting string would exceed
   `maxStringLengthUtf16CodeUnits`. -}
type StringTooLong = StringTooLong

{- Render the `StringTooLong` value as the literal string
   `"StringTooLong"`. The type is nullary, so there is only ever one
   value to render. -}
showStringTooLong : StringTooLong -> String
showStringTooLong _ = "StringTooLong"

-- ---------------------- UnpairedUtf16Surrogate

{- Reported by string-construction primitives reading host-decoded
   text (CLI arguments, future FFI) when a UTF-16 half-surrogate
   appears without its mate. Awsum strings are strict UTF-16; lone
   surrogates are not representable. This is a UTF-16-level failure:
   the host (e.g. Windows `CommandLineToArgvW`, the JVM's argv
   decoder) has already produced a code-unit sequence, and one of
   those code units is an unpaired surrogate. Stdin, read as raw
   bytes and decoded by Awsum itself, reports byte-level malformation
   as `InvalidUtf8` instead. Never appears as the result of a pure
   computation — only at the I/O boundary. -}
type UnpairedUtf16Surrogate = UnpairedUtf16Surrogate

{- Render the `UnpairedUtf16Surrogate` value as the literal string
   `"UnpairedUtf16Surrogate"`. The type is nullary, so there is only
   ever one value to render. -}
showUnpairedUtf16Surrogate : UnpairedUtf16Surrogate -> String
showUnpairedUtf16Surrogate _ = "UnpairedUtf16Surrogate"

-- ---------------------- InvalidUtf8

{- Reported by `IO.Stdin.readAllString` when the raw bytes read from
   stdin are not well-formed UTF-8 (RFC 3629): overlong encodings,
   truncated multi-byte sequences, stray continuation bytes, code
   points above U+10FFFF, or surrogate code points encoded in UTF-8
   (`ED A0 80`..). This is a byte-level failure, distinct from
   `UnpairedUtf16Surrogate`: stdin is decoded by Awsum from bytes, so
   it owns the full UTF-8 validity check, whereas host-decoded argv
   only exposes UTF-16-level surrogate errors. Never appears as the
   result of a pure computation — only at the I/O boundary. -}
type InvalidUtf8 = InvalidUtf8

{- Render the `InvalidUtf8` value as the literal string
   `"InvalidUtf8"`. The type is nullary, so there is only ever one
   value to render. -}
showInvalidUtf8 : InvalidUtf8 -> String
showInvalidUtf8 _ = "InvalidUtf8"

-- ---------------------- ParseError

{- Reported by parsing primitives (e.g. `parseInt32`) when the input
   does not match the expected grammar or yields a value outside the
   target type's range. The grammar and rejected inputs are documented
   on each parser. -}
type ParseError = ParseError

{- Render the `ParseError` value as the literal string `"ParseError"`.
   The type is nullary, so there is only ever one value to render. -}
showParseError : ParseError -> String
showParseError _ = "ParseError"

-- ---------------------- BrokenPipe

{- Will be reported by IO primitives that write to a pipe (e.g.
   `IO.Stdout.print`) when the consumer side closes before the write
   completes — SIGPIPE / EPIPE when output is piped into a consumer
   that exits early (`awsum-program | head`).

   Declared now as a placeholder: built-in print primitives still carry
   `IO Never Unit` and never produce this value at runtime. The type is
   in place so the eventual signature flip
   (`String -> IO BrokenPipe Unit`) won't require a rename. -}
type BrokenPipe = BrokenPipe

{- Render the `BrokenPipe` value as the literal string `"BrokenPipe"`.
   The type is nullary, so there is only ever one value to render. -}
showBrokenPipe : BrokenPipe -> String
showBrokenPipe _ = "BrokenPipe"

-- ---------------------- UInt8

{- Smallest representable `UInt8` value, `0`. -}
minUInt8 : UInt8
minUInt8 = 0

{- Largest representable `UInt8` value, `255`. -}
maxUInt8 : UInt8
maxUInt8 = 255

{- Equality on `UInt8`: returns `True` iff both arguments hold the same
   8-bit unsigned value. -}
eqUInt8 : UInt8 -> UInt8 -> Bool
eqUInt8 = BuiltIn.eqUInt8

{- Render a `UInt8` as its decimal string (`"0"` .. `"255"`), with no
   leading zeroes and no sign. -}
showUInt8 : UInt8 -> String
showUInt8 = BuiltIn.showUInt8

{- Render a `UInt8` as exactly two lowercase hex digits with no `0x`
   prefix (`0` -> `"00"`, `255` -> `"ff"`). -}
byteToHexStringNoPrefix : UInt8 -> String
byteToHexStringNoPrefix = BuiltIn.byteToHexStringNoPrefix

{- Render a list of bytes as their concatenated two-digit lowercase hex,
   no separators and no prefix (`[0, 255, 16]` -> `"00ff10"`). Fails with
   `StringTooLong` only if the combined hex would exceed the string cap. -}
bytesToHexStringNoPrefix : List UInt8 -> Either StringTooLong String
bytesToHexStringNoPrefix bytes = case bytes of
  Nil -> Right ""
  Cons b rest -> bindEither (bytesToHexStringNoPrefix rest) (\restHex -> byteToHexStringNoPrefix b ++ restHex)

{- Predecessor (`n - 1`). Returns `UnderflowError` when `n = 0`
   because the mathematical result is outside the `UInt8` range. -}
predUInt8 : UInt8 -> Either UnderflowError UInt8
predUInt8 = BuiltIn.predUInt8

{- Successor (`n + 1`). Returns `OverflowError` when `n = 255` because
   the mathematical result is outside the `UInt8` range. -}
succUInt8 : UInt8 -> Either OverflowError UInt8
succUInt8 = BuiltIn.succUInt8

{- Addition. Returns `OverflowError` when the mathematical sum exceeds
   `255`. No wrap-around, no saturation — the honest answer is either
   returned or rejected. -}
addUInt8 : UInt8 -> UInt8 -> Either OverflowError UInt8
addUInt8 = BuiltIn.addUInt8

{- Subtraction. Returns `UnderflowError` when the second operand
   exceeds the first (a negative result has no `UInt8` representation). -}
subUInt8 : UInt8 -> UInt8 -> Either UnderflowError UInt8
subUInt8 = BuiltIn.subUInt8

{- Multiplication. Returns `OverflowError` when the mathematical product
   exceeds `255`. No wrap-around, no saturation. -}
mulUInt8 : UInt8 -> UInt8 -> Either OverflowError UInt8
mulUInt8 = BuiltIn.mulUInt8

{- Parse a `UInt8` from a decimal string. Grammar: one or more decimal
   digits, nothing else — no sign, no whitespace, no leading `+`, no
   trailing characters. Range 0..255 inclusive.

   - `parseUInt8 "0"`   → `Right 0`
   - `parseUInt8 "255"` → `Right 255`
   - `parseUInt8 "256"` → `Left ParseError` (above max)
   - `parseUInt8 "-1"`  → `Left ParseError` (negative)
   - `parseUInt8 ""`    → `Left ParseError` (empty)
   - `parseUInt8 "12a"` → `Left ParseError` (trailing garbage)

   Digits are ASCII '0'..'9' (0x30..0x39); other Unicode digit forms
   are rejected. -}
parseUInt8 : String -> Either ParseError UInt8
parseUInt8 = BuiltIn.parseUInt8

-- ---------------------- UInt32

{- Smallest representable `UInt32` value, `0`. -}
minUInt32 : UInt32
minUInt32 = 0

{- Largest representable `UInt32` value, `4_294_967_295` (`2^32 - 1`). -}
maxUInt32 : UInt32
maxUInt32 = 4_294_967_295

{- Equality on `UInt32`: returns `True` iff both arguments hold the
   same 32-bit unsigned value. -}
eqUInt32 : UInt32 -> UInt32 -> Bool
eqUInt32 = BuiltIn.eqUInt32

{- Render a `UInt32` as its decimal string (`"0"` .. `"4294967295"`),
   with no leading zeroes and no sign. -}
showUInt32 : UInt32 -> String
showUInt32 = BuiltIn.showUInt32

{- Predecessor (`n - 1`). Returns `UnderflowError` when `n = 0`
   because the mathematical result is outside the `UInt32` range. -}
predUInt32 : UInt32 -> Either UnderflowError UInt32
predUInt32 = BuiltIn.predUInt32

{- Successor (`n + 1`). Returns `OverflowError` when `n = 4_294_967_295`
   because the mathematical result is outside the `UInt32` range. -}
succUInt32 : UInt32 -> Either OverflowError UInt32
succUInt32 = BuiltIn.succUInt32

{- Addition. Returns `OverflowError` when the mathematical sum exceeds
   `4_294_967_295`. No wrap-around, no saturation — the honest answer
   is either returned or rejected. -}
addUInt32 : UInt32 -> UInt32 -> Either OverflowError UInt32
addUInt32 = BuiltIn.addUInt32

{- Subtraction. Returns `UnderflowError` when the second operand
   exceeds the first (a negative result has no `UInt32` representation). -}
subUInt32 : UInt32 -> UInt32 -> Either UnderflowError UInt32
subUInt32 = BuiltIn.subUInt32

{- Multiplication. Returns `OverflowError` when the mathematical product
   exceeds `4_294_967_295`. No wrap-around, no saturation. -}
mulUInt32 : UInt32 -> UInt32 -> Either OverflowError UInt32
mulUInt32 = BuiltIn.mulUInt32

{- Parse a `UInt32` from a decimal string. Grammar: one or more decimal
   digits, nothing else — no sign, no whitespace, no leading `+`, no
   trailing characters. Range `0` .. `4_294_967_295` inclusive.

   - `parseUInt32 "0"`           → `Right 0`
   - `parseUInt32 "4294967295"`  → `Right 4294967295`
   - `parseUInt32 "4294967296"`  → `Left ParseError` (above max)
   - `parseUInt32 "-1"`          → `Left ParseError` (negative)
   - `parseUInt32 ""`            → `Left ParseError`
   - `parseUInt32 "12a"`         → `Left ParseError` (trailing garbage)

   Digits are ASCII `'0'`..`'9'` (0x30..0x39); other Unicode digit
   forms are rejected. -}
parseUInt32 : String -> Either ParseError UInt32
parseUInt32 = BuiltIn.parseUInt32

-- ---------------------- Int32

{- Smallest representable `Int32` value, `-2_147_483_648` (`-2^31`).
   Negating this value overflows — see `negInt32`. -}
minInt32 : Int32
minInt32 = -2_147_483_648

{- Largest representable `Int32` value, `2_147_483_647` (`2^31 - 1`). -}
maxInt32 : Int32
maxInt32 = 2_147_483_647

{- Equality on `Int32`: returns `True` iff both arguments hold the same
   32-bit signed value. -}
eqInt32 : Int32 -> Int32 -> Bool
eqInt32 = BuiltIn.eqInt32

{- Render an `Int32` as its decimal string. Negative values get a
   leading `-`; non-negative values have no sign. No leading zeroes. -}
showInt32 : Int32 -> String
showInt32 = BuiltIn.showInt32

{- Predecessor (`n - 1`). Returns `UnderflowError` when `n = minInt32`
   because the mathematical result is below the `Int32` range. -}
predInt32 : Int32 -> Either UnderflowError Int32
predInt32 = BuiltIn.predInt32

{- Successor (`n + 1`). Returns `OverflowError` when `n = maxInt32`
   because the mathematical result is above the `Int32` range. -}
succInt32 : Int32 -> Either OverflowError Int32
succInt32 = BuiltIn.succInt32

{- Addition. Returns `UnderflowError` when the mathematical sum is
   below `minInt32`, `OverflowError` when above `maxInt32`. No
   wrap-around, no saturation. -}
addInt32 : Int32 -> Int32 -> Either (UnderflowError | OverflowError) Int32
addInt32 = BuiltIn.addInt32

{- Subtraction. Returns `UnderflowError` when the mathematical result
   is below `minInt32`, `OverflowError` when above `maxInt32`. -}
subInt32 : Int32 -> Int32 -> Either (UnderflowError | OverflowError) Int32
subInt32 = BuiltIn.subInt32

{- Multiplication. Returns `UnderflowError` when the mathematical
   product is below `minInt32`, `OverflowError` when above `maxInt32`. -}
mulInt32 : Int32 -> Int32 -> Either (UnderflowError | OverflowError) Int32
mulInt32 = BuiltIn.mulInt32

{- Arithmetic negation (`0 - n`). Returns `OverflowError` only for
   `n = minInt32`, where the mathematical result `2_147_483_648` is
   above `maxInt32`. Every other input succeeds; `negInt32 0` is `0`. -}
negInt32 : Int32 -> Either OverflowError Int32
negInt32 = BuiltIn.negInt32

{- Parse an `Int32` from a decimal string. Grammar: optional leading
   `-`, then one or more decimal digits, nothing else — no `+`, no
   whitespace, no trailing characters. Range `minInt32..maxInt32`
   inclusive.

   - `parseInt32 "42"`          → `Right 42`
   - `parseInt32 "-42"`         → `Right -42`
   - `parseInt32 "2147483648"`  → `Left ParseError` (above maxInt32)
   - `parseInt32 "-2147483649"` → `Left ParseError` (below minInt32)
   - `parseInt32 "+42"`         → `Left ParseError` (`+` is not accepted, mirroring the literal grammar)
   - `parseInt32 ""`            → `Left ParseError`
   - `parseInt32 "-"`           → `Left ParseError` (sign without digits)
   - `parseInt32 "12abc"`       → `Left ParseError` (trailing garbage)

   Digits are ASCII '0'..'9' (0x30..0x39); other Unicode digit forms
   are rejected. -}
parseInt32 : String -> Either ParseError Int32
parseInt32 = BuiltIn.parseInt32