module Compiler.IntegerLiteral

import Std.Byte
import Std.Word
import Std.Natural
import Data.Bytes
import Model.Parameter
import Model.Word64

-- The compiler owns literal syntax and its failures.  Std.Word owns arithmetic
-- and codecs; this module deliberately does not expose those diagnostics.
family IntegerLiteralRadix : Type 0
constructor IntegerLiteralDecimal
constructor IntegerLiteralBinary
constructor IntegerLiteralHexadecimal

end-family

family IntegerLiteralSign : Type 0
constructor IntegerLiteralPositive
constructor IntegerLiteralNegative

end-family

family IntegerLiteralKind : Type 0
constructor IntegerLiteralUnsigned
constructor IntegerLiteralSigned

end-family

family IntegerLiteralWidth : Type 0
constructor IntegerLiteralWidth8
constructor IntegerLiteralWidth16
constructor IntegerLiteralWidth32
constructor IntegerLiteralWidth64

end-family

family IntegerLiteralFailure : Type 0
constructor IntegerLiteralMissingDigits
constructor IntegerLiteralBadDigit
constructor IntegerLiteralBadSeparator
constructor IntegerLiteralOutOfRange

end-family

family IntegerLiteralResult : Type 0
constructor IntegerLiteralWord
field unrestricted integerLiteralWidth : (family IntegerLiteralWidth)
field unrestricted integerLiteralSign : (family IntegerLiteralSign)
field unrestricted integerLiteralBytesLE : Bytes
constructor IntegerLiteralFailed
field unrestricted integerLiteralFailure : (family IntegerLiteralFailure)

end-family

family IntegerLiteralDigitResult : Type 0
constructor IntegerLiteralDigitValue
field unrestricted integerLiteralDigit : Nat
constructor IntegerLiteralDigitFailed
field unrestricted integerLiteralDigitFailure : (family IntegerLiteralFailure)

end-family

family IntegerLiteralFoldResult : Type 0
constructor IntegerLiteralFoldValue
field unrestricted integerLiteralFoldAccumulator : (family ModelWord64)
constructor IntegerLiteralFoldFailed
field unrestricted integerLiteralFoldFailure : (family IntegerLiteralFailure)

end-family

family IntegerLiteralU64StepResult : Type 0
constructor IntegerLiteralU64StepSucceeded
field unrestricted integerLiteralU64StepValue : (family ModelWord64)
constructor IntegerLiteralU64StepFailed

end-family

family IntegerLiteralSyntaxResult : Type 0
constructor IntegerLiteralSyntaxAccepted
constructor IntegerLiteralSyntaxFailed
field unrestricted integerLiteralSyntaxFailure : (family IntegerLiteralFailure)

end-family

def integerLiteralZero =
  (constructor
    ModelWord64
    ModelWord64Value
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0))

def integerLiteralOne =
  (constructor
    ModelWord64
    ModelWord64Value
    (byte 1)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0))

def integerLiteralTwo =
  (constructor
    ModelWord64
    ModelWord64Value
    (byte 2)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0))

def integerLiteralTen =
  (constructor
    ModelWord64
    ModelWord64Value
    (byte 10)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0))

def integerLiteralSixteen =
  (constructor
    ModelWord64
    ModelWord64Value
    (byte 16)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0))

def integerLiteralMaxU8 =
  (constructor
    ModelWord64
    ModelWord64Value
    (byte 255)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0))

def integerLiteralMaxU16 =
  (constructor
    ModelWord64
    ModelWord64Value
    (byte 255)
    (byte 255)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0))

def integerLiteralMaxU32 =
  (constructor
    ModelWord64
    ModelWord64Value
    (byte 255)
    (byte 255)
    (byte 255)
    (byte 255)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0))

def integerLiteralMaxU64 =
  (constructor
    ModelWord64
    ModelWord64Value
    (byte 255)
    (byte 255)
    (byte 255)
    (byte 255)
    (byte 255)
    (byte 255)
    (byte 255)
    (byte 255))

def integerLiteralMaxI8 =
  (constructor
    ModelWord64
    ModelWord64Value
    (byte 127)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0))

def integerLiteralMaxI16 =
  (constructor
    ModelWord64
    ModelWord64Value
    (byte 255)
    (byte 127)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0))

def integerLiteralMaxI32 =
  (constructor
    ModelWord64
    ModelWord64Value
    (byte 255)
    (byte 255)
    (byte 255)
    (byte 127)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0))

def integerLiteralMaxI64 =
  (constructor
    ModelWord64
    ModelWord64Value
    (byte 255)
    (byte 255)
    (byte 255)
    (byte 255)
    (byte 255)
    (byte 255)
    (byte 255)
    (byte 127))

def integerLiteralMinMagnitudeI8 =
  (constructor
    ModelWord64
    ModelWord64Value
    (byte 128)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0))

def integerLiteralMinMagnitudeI16 =
  (constructor
    ModelWord64
    ModelWord64Value
    (byte 0)
    (byte 128)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0))

def integerLiteralMinMagnitudeI32 =
  (constructor
    ModelWord64
    ModelWord64Value
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 128)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0))

def integerLiteralMinMagnitudeI64 =
  (constructor
    ModelWord64
    ModelWord64Value
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 0)
    (byte 128))

def integerLiteralDigitWord =
  (lambda unrestricted digit : Byte .
    (constructor
      ModelWord64
      ModelWord64Value
      digit
      (byte 0)
      (byte 0)
      (byte 0)
      (byte 0)
      (byte 0)
      (byte 0)
      (byte 0)))

def integerLiteralFailureResult =
  (lambda unrestricted failure : (family IntegerLiteralFailure) .
    (constructor IntegerLiteralResult IntegerLiteralFailed failure))

def integerLiteralBadDigitResult =
  (constructor
    IntegerLiteralDigitResult
    IntegerLiteralDigitFailed
    (constructor IntegerLiteralFailure IntegerLiteralBadDigit))

def integerLiteralChoose =
  (lambda unrestricted condition : Nat .
    (lambda unrestricted whenTrue : (family IntegerLiteralDigitResult) .
      (lambda unrestricted whenFalse : (family IntegerLiteralDigitResult) .
        (nat-eliminate
          (lambda unrestricted current : Nat . (family IntegerLiteralDigitResult))
          whenFalse
          (lambda unrestricted predecessor : Nat .
            (lambda unrestricted induction : (family IntegerLiteralDigitResult) . whenTrue))
          condition))))

def integerLiteralDecodeDecimal =
  (lambda unrestricted value : Byte .
    (nat-eliminate
      (lambda unrestricted current : Nat . (family IntegerLiteralDigitResult))
      integerLiteralBadDigitResult
      (lambda unrestricted predecessor : Nat .
        (lambda unrestricted induction : (family IntegerLiteralDigitResult) .
          (nat-eliminate
            (lambda unrestricted current : Nat . (family IntegerLiteralDigitResult))
            integerLiteralBadDigitResult
            (lambda unrestricted predecessorAgain : Nat .
              (lambda unrestricted inductionAgain : (family IntegerLiteralDigitResult) .
                (constructor
                  IntegerLiteralDigitResult
                  IntegerLiteralDigitValue
                  (naturalSaturatingSubtract (byte-to-nat value) (byte-to-nat (byte 48))))))
            (byte-less-than value (byte 58)))))
      (byte-less-than (byte 47) value)))

def integerLiteralDecodeBinary =
  (lambda unrestricted value : Byte .
    (nat-eliminate
      (lambda unrestricted current : Nat . (family IntegerLiteralDigitResult))
      integerLiteralBadDigitResult
      (lambda unrestricted predecessor : Nat .
        (lambda unrestricted induction : (family IntegerLiteralDigitResult) .
          (nat-eliminate
            (lambda unrestricted current : Nat . (family IntegerLiteralDigitResult))
            integerLiteralBadDigitResult
            (lambda unrestricted predecessorAgain : Nat .
              (lambda unrestricted inductionAgain : (family IntegerLiteralDigitResult) .
                (constructor
                  IntegerLiteralDigitResult
                  IntegerLiteralDigitValue
                  (naturalSaturatingSubtract (byte-to-nat value) (byte-to-nat (byte 48))))))
            (byte-less-than value (byte 50)))))
      (byte-less-than (byte 47) value)))

def integerLiteralDecodeHexLetter =
  (lambda unrestricted value : Byte .
    (integerLiteralChoose
      (stdFlagAnd (byte-less-than (byte 64) value) (byte-less-than value (byte 71)))
      (constructor
        IntegerLiteralDigitResult
        IntegerLiteralDigitValue
        (naturalSaturatingSubtract (byte-to-nat value) (byte-to-nat (byte 55))))
      (integerLiteralChoose
        (stdFlagAnd (byte-less-than (byte 96) value) (byte-less-than value (byte 103)))
        (constructor
          IntegerLiteralDigitResult
          IntegerLiteralDigitValue
          (naturalSaturatingSubtract (byte-to-nat value) (byte-to-nat (byte 87))))
        integerLiteralBadDigitResult)))

def integerLiteralDecodeHex =
  (lambda unrestricted value : Byte .
    (eliminate
      IntegerLiteralDigitResult
      (lambda unrestricted current : (family IntegerLiteralDigitResult) .
        (family IntegerLiteralDigitResult))
      (integerLiteralDecodeDecimal value)
      (branch
        IntegerLiteralDigitValue
        digit
        .
        (constructor IntegerLiteralDigitResult IntegerLiteralDigitValue digit))
      (branch IntegerLiteralDigitFailed failure . (integerLiteralDecodeHexLetter value))))

def integerLiteralDecodeDigit =
  (lambda unrestricted radix : (family IntegerLiteralRadix) .
    (lambda unrestricted value : Byte .
      (eliminate
        IntegerLiteralRadix
        (lambda unrestricted current : (family IntegerLiteralRadix) .
          (family IntegerLiteralDigitResult))
        radix
        (branch IntegerLiteralDecimal . (integerLiteralDecodeDecimal value))
        (branch IntegerLiteralBinary . (integerLiteralDecodeBinary value))
        (branch IntegerLiteralHexadecimal . (integerLiteralDecodeHex value)))))

def integerLiteralRadixWord =
  (lambda unrestricted radix : (family IntegerLiteralRadix) .
    (eliminate
      IntegerLiteralRadix
      (lambda unrestricted current : (family IntegerLiteralRadix) . (family ModelWord64))
      radix
      (branch IntegerLiteralDecimal . integerLiteralTen)
      (branch IntegerLiteralBinary . integerLiteralTwo)
      (branch IntegerLiteralHexadecimal . integerLiteralSixteen)))

-- Source radices are fixed by the grammar. Checked addition chains avoid
-- a general 64-step multiply per digit, while Std.Word remains the arithmetic
-- owner. Every intermediate fits whenever the final nonnegative product fits;
-- an intermediate overflow therefore proves the literal cannot fit U64.
def integerLiteralCheckedAdd =
  (lambda unrestricted left : (family ModelWord64) .
    (lambda unrestricted right : (family ModelWord64) .
      (eliminate
        ModelWord64CheckedResult
        (lambda unrestricted current : (family ModelWord64CheckedResult) .
          (family IntegerLiteralU64StepResult))
        (stdU64AddChecked left right)
        (branch
          ModelWord64CheckedSucceeded
          value
          .
          (constructor IntegerLiteralU64StepResult IntegerLiteralU64StepSucceeded value))
        (branch
          ModelWord64CheckedFailed
          error
          .
          (constructor IntegerLiteralU64StepResult IntegerLiteralU64StepFailed)))))

def integerLiteralThen =
  (lambda unrestricted step : (family IntegerLiteralU64StepResult) .
    (lambda unrestricted continue : (pi unrestricted value : (family ModelWord64) . (family IntegerLiteralU64StepResult)) .
      (eliminate
        IntegerLiteralU64StepResult
        (lambda unrestricted current : (family IntegerLiteralU64StepResult) .
          (family IntegerLiteralU64StepResult))
        step
        (branch IntegerLiteralU64StepSucceeded value . (continue value))
        (branch
          IntegerLiteralU64StepFailed
          .
          (constructor IntegerLiteralU64StepResult IntegerLiteralU64StepFailed)))))

def integerLiteralScale =
  (lambda unrestricted radix : (family IntegerLiteralRadix) .
    (lambda unrestricted accumulator : (family ModelWord64) .
      (eliminate
        IntegerLiteralRadix
        (lambda unrestricted current : (family IntegerLiteralRadix) .
          (family IntegerLiteralU64StepResult))
        radix
        (branch
          IntegerLiteralDecimal
          .
          (integerLiteralThen
            (integerLiteralCheckedAdd accumulator accumulator)
            (lambda unrestricted twice : (family ModelWord64) .
              (integerLiteralThen
                (integerLiteralCheckedAdd twice twice)
                (lambda unrestricted four : (family ModelWord64) .
                  (integerLiteralThen
                    (integerLiteralCheckedAdd four four)
                    (lambda unrestricted eight : (family ModelWord64) .
                      (integerLiteralCheckedAdd eight twice))))))))
        (branch IntegerLiteralBinary . (integerLiteralCheckedAdd accumulator accumulator))
        (branch
          IntegerLiteralHexadecimal
          .
          (integerLiteralThen
            (integerLiteralCheckedAdd accumulator accumulator)
            (lambda unrestricted twice : (family ModelWord64) .
              (integerLiteralThen
                (integerLiteralCheckedAdd twice twice)
                (lambda unrestricted four : (family ModelWord64) .
                  (integerLiteralThen
                    (integerLiteralCheckedAdd four four)
                    (lambda unrestricted eight : (family ModelWord64) .
                      (integerLiteralCheckedAdd eight eight)))))))))))

def integerLiteralStep =
  (lambda unrestricted radix : (family IntegerLiteralRadix) .
    (lambda unrestricted accumulator : (family ModelWord64) .
      (lambda unrestricted digit : Byte .
        (integerLiteralThen
          (integerLiteralScale radix accumulator)
          (lambda unrestricted scaled : (family ModelWord64) .
            (integerLiteralCheckedAdd scaled (integerLiteralDigitWord digit)))))))

def integerLiteralStepBytes =
  (lambda unrestricted radix : (family IntegerLiteralRadix) .
    (lambda unrestricted accumulator : (family ModelWord64) .
      (lambda unrestricted digit : Byte .
        (eliminate
          IntegerLiteralU64StepResult
          (lambda unrestricted current : (family IntegerLiteralU64StepResult) . Bytes)
          (integerLiteralStep radix accumulator digit)
          (branch IntegerLiteralU64StepSucceeded value . (Std.Word/stdU64EncodeLE value))
          (branch IntegerLiteralU64StepFailed . b"")))))

-- Branches are suspended: the evaluator is strict in application arguments.
-- Calling the continuation in both value arguments would double the remaining
-- validation work at each byte, even when only one branch is selected.
def integerLiteralChooseSyntax =
  (lambda unrestricted condition : Nat .
    (lambda unrestricted whenTrue : (pi unrestricted ignored : Nat . (family IntegerLiteralSyntaxResult)) .
      (lambda unrestricted whenFalse : (pi unrestricted ignored : Nat . (family IntegerLiteralSyntaxResult)) .
        (app
          (nat-eliminate
            (lambda unrestricted current : Nat .
              (pi unrestricted ignored : Nat . (family IntegerLiteralSyntaxResult)))
            whenFalse
            (lambda unrestricted predecessor : Nat .
              (lambda unrestricted induction : (pi unrestricted ignored : Nat . (family IntegerLiteralSyntaxResult)) .
                whenTrue))
            condition)
          zero))))

-- A separator has a valid radix digit on both sides. The continuation
-- carries only that preceding-digit fact; arithmetic starts after validation.
def integerLiteralDigitValid =
  (lambda unrestricted radix : (family IntegerLiteralRadix) .
    (lambda unrestricted value : Byte .
      (eliminate
        IntegerLiteralDigitResult
        (lambda unrestricted current : (family IntegerLiteralDigitResult) . Nat)
        (integerLiteralDecodeDigit radix value)
        (branch IntegerLiteralDigitValue digit . (succ zero))
        (branch IntegerLiteralDigitFailed failure . zero))))

def integerLiteralSeparatorStep =
  (lambda unrestricted radix : (family IntegerLiteralRadix) .
    (lambda unrestricted head : Byte .
      (lambda unrestricted tail : Bytes .
        (lambda unrestricted continue : (pi unrestricted previousWasDigit : Nat . (family IntegerLiteralSyntaxResult)) .
          (lambda unrestricted previousWasDigit : Nat .
            (integerLiteralChooseSyntax
              (byte-equal head (byte 95))
              (lambda unrestricted ignored : Nat .
                (integerLiteralChooseSyntax
                  (stdFlagAnd previousWasDigit (integerLiteralDigitValid radix (bytes-head tail)))
                  (lambda unrestricted ignored : Nat . (continue zero))
                  (lambda unrestricted ignored : Nat .
                    (constructor
                      IntegerLiteralSyntaxResult
                      IntegerLiteralSyntaxFailed
                      (constructor IntegerLiteralFailure IntegerLiteralBadSeparator)))))
              (lambda unrestricted ignored : Nat .
                (eliminate
                  IntegerLiteralDigitResult
                  (lambda unrestricted current : (family IntegerLiteralDigitResult) .
                    (family IntegerLiteralSyntaxResult))
                  (integerLiteralDecodeDigit radix head)
                  (branch IntegerLiteralDigitValue digit . (continue (succ zero)))
                  (branch
                    IntegerLiteralDigitFailed
                    failure
                    .
                    (constructor IntegerLiteralSyntaxResult IntegerLiteralSyntaxFailed failure))))))))))

def integerLiteralValidateSeparators =
  (lambda unrestricted radix : (family IntegerLiteralRadix) .
    (lambda unrestricted digits : Bytes .
      (app
        (bytes-eliminate
          (lambda unrestricted remaining : Bytes .
            (pi unrestricted previousWasDigit : Nat . (family IntegerLiteralSyntaxResult)))
          (lambda unrestricted previousWasDigit : Nat .
            (integerLiteralChooseSyntax
              previousWasDigit
              (lambda unrestricted ignored : Nat .
                (constructor IntegerLiteralSyntaxResult IntegerLiteralSyntaxAccepted))
              (lambda unrestricted ignored : Nat .
                (constructor
                  IntegerLiteralSyntaxResult
                  IntegerLiteralSyntaxFailed
                  (constructor IntegerLiteralFailure IntegerLiteralBadSeparator)))))
          (integerLiteralSeparatorStep radix)
          digits)
        zero)))

def integerLiteralStripSeparators =
  (lambda unrestricted digits : Bytes .
    (bytes-eliminate
      (lambda unrestricted remaining : Bytes . Bytes)
      b""
      (lambda unrestricted head : Byte .
        (lambda unrestricted tail : Bytes .
          (lambda unrestricted slots : Bytes .
            (nat-eliminate
              (lambda unrestricted current : Nat . Bytes)
              (bytes-cons head slots)
              (lambda unrestricted predecessor : Nat .
                (lambda unrestricted induction : Bytes . slots))
              (byte-equal head (byte 95))))))
      digits))

def integerLiteralFoldDigits =
  (lambda unrestricted radix : (family IntegerLiteralRadix) .
    (lambda unrestricted digits : Bytes .
      (app
        (bytes-eliminate
          (lambda unrestricted remaining : Bytes .
            (pi unrestricted accumulator : (family ModelWord64) . (family IntegerLiteralFoldResult)))
          (lambda unrestricted accumulator : (family ModelWord64) .
            (constructor IntegerLiteralFoldResult IntegerLiteralFoldValue accumulator))
          (lambda unrestricted head : Byte .
            (lambda unrestricted tail : Bytes .
              (lambda unrestricted continue : (pi unrestricted accumulator : (family ModelWord64) . (family IntegerLiteralFoldResult)) .
                (lambda unrestricted accumulator : (family ModelWord64) .
                  (eliminate
                    IntegerLiteralDigitResult
                    (lambda unrestricted current : (family IntegerLiteralDigitResult) .
                      (family IntegerLiteralFoldResult))
                    (integerLiteralDecodeDigit radix head)
                    (branch
                      IntegerLiteralDigitValue
                      digit
                      .
                      (eliminate
                        IntegerLiteralU64StepResult
                        (lambda unrestricted current : (family IntegerLiteralU64StepResult) .
                          (family IntegerLiteralFoldResult))
                        (integerLiteralStep radix accumulator (nat-to-byte digit))
                        (branch IntegerLiteralU64StepSucceeded next . (continue next))
                        (branch
                          IntegerLiteralU64StepFailed
                          .
                          (constructor
                            IntegerLiteralFoldResult
                            IntegerLiteralFoldFailed
                            (constructor IntegerLiteralFailure IntegerLiteralOutOfRange)))))
                    (branch
                      IntegerLiteralDigitFailed
                      failure
                      .
                      (constructor IntegerLiteralFoldResult IntegerLiteralFoldFailed failure)))))))
          digits)
        integerLiteralZero)))

def integerLiteralLessOrEqual =
  (lambda unrestricted left : (family ModelWord64) .
    (lambda unrestricted right : (family ModelWord64) .
      -- Unsigned words form a total order. Negating the reverse comparison
      -- avoids the general XOR-based equality implementation at this boundary.
      (stdFlagNot (stdU64LessThan right left))))

def integerLiteralUnsignedBound =
  (lambda unrestricted width : (family IntegerLiteralWidth) .
    (eliminate
      IntegerLiteralWidth
      (lambda unrestricted current : (family IntegerLiteralWidth) . (family ModelWord64))
      width
      (branch IntegerLiteralWidth8 . integerLiteralMaxU8)
      (branch IntegerLiteralWidth16 . integerLiteralMaxU16)
      (branch IntegerLiteralWidth32 . integerLiteralMaxU32)
      (branch IntegerLiteralWidth64 . integerLiteralMaxU64)))

def integerLiteralSignedPositiveBound =
  (lambda unrestricted width : (family IntegerLiteralWidth) .
    (eliminate
      IntegerLiteralWidth
      (lambda unrestricted current : (family IntegerLiteralWidth) . (family ModelWord64))
      width
      (branch IntegerLiteralWidth8 . integerLiteralMaxI8)
      (branch IntegerLiteralWidth16 . integerLiteralMaxI16)
      (branch IntegerLiteralWidth32 . integerLiteralMaxI32)
      (branch IntegerLiteralWidth64 . integerLiteralMaxI64)))

def integerLiteralSignedNegativeBound =
  (lambda unrestricted width : (family IntegerLiteralWidth) .
    (eliminate
      IntegerLiteralWidth
      (lambda unrestricted current : (family IntegerLiteralWidth) . (family ModelWord64))
      width
      (branch IntegerLiteralWidth8 . integerLiteralMinMagnitudeI8)
      (branch IntegerLiteralWidth16 . integerLiteralMinMagnitudeI16)
      (branch IntegerLiteralWidth32 . integerLiteralMinMagnitudeI32)
      (branch IntegerLiteralWidth64 . integerLiteralMinMagnitudeI64)))

def integerLiteralEncodeWidth =
  (lambda unrestricted width : (family IntegerLiteralWidth) .
    (lambda unrestricted value : (family ModelWord64) .
      (eliminate
        ModelWord64
        (lambda unrestricted current : (family ModelWord64) . Bytes)
        value
        (branch
          ModelWord64Value
          b0
          b1
          b2
          b3
          b4
          b5
          b6
          b7
          .
          (eliminate
            IntegerLiteralWidth
            (lambda unrestricted current : (family IntegerLiteralWidth) . Bytes)
            width
            (branch IntegerLiteralWidth8 . (bytes b0))
            (branch IntegerLiteralWidth16 . (bytes b0 b1))
            (branch IntegerLiteralWidth32 . (bytes b0 b1 b2 b3))
            (branch IntegerLiteralWidth64 . (bytes b0 b1 b2 b3 b4 b5 b6 b7)))))))

def integerLiteralFinish =
  (lambda unrestricted kind : (family IntegerLiteralKind) .
    (lambda unrestricted sign : (family IntegerLiteralSign) .
      (lambda unrestricted width : (family IntegerLiteralWidth) .
        (lambda unrestricted folded : (family IntegerLiteralFoldResult) .
          (eliminate
            IntegerLiteralFoldResult
            (lambda unrestricted current : (family IntegerLiteralFoldResult) .
              (family IntegerLiteralResult))
            folded
            (branch
              IntegerLiteralFoldValue
              magnitude
              .
              (eliminate
                IntegerLiteralSign
                (lambda unrestricted current : (family IntegerLiteralSign) .
                  (family IntegerLiteralResult))
                sign
                (branch
                  IntegerLiteralPositive
                  .
                  (nat-eliminate
                    (lambda unrestricted current : Nat . (family IntegerLiteralResult))
                    (constructor
                      IntegerLiteralResult
                      IntegerLiteralFailed
                      (constructor IntegerLiteralFailure IntegerLiteralOutOfRange))
                    (lambda unrestricted predecessor : Nat .
                      (lambda unrestricted induction : (family IntegerLiteralResult) .
                        (constructor
                          IntegerLiteralResult
                          IntegerLiteralWord
                          width
                          sign
                          (integerLiteralEncodeWidth width magnitude))))
                    (integerLiteralLessOrEqual
                      magnitude
                      (eliminate
                        IntegerLiteralKind
                        (lambda unrestricted current : (family IntegerLiteralKind) .
                          (family ModelWord64))
                        kind
                        (branch IntegerLiteralUnsigned . (integerLiteralUnsignedBound width))
                        (branch IntegerLiteralSigned . (integerLiteralSignedPositiveBound width))))))
                (branch
                  IntegerLiteralNegative
                  .
                  (eliminate
                    IntegerLiteralKind
                    (lambda unrestricted current : (family IntegerLiteralKind) .
                      (family IntegerLiteralResult))
                    kind
                    (branch
                      IntegerLiteralUnsigned
                      .
                      (constructor
                        IntegerLiteralResult
                        IntegerLiteralFailed
                        (constructor IntegerLiteralFailure IntegerLiteralOutOfRange)))
                    (branch
                      IntegerLiteralSigned
                      .
                      (nat-eliminate
                        (lambda unrestricted current : Nat . (family IntegerLiteralResult))
                        (constructor
                          IntegerLiteralResult
                          IntegerLiteralFailed
                          (constructor IntegerLiteralFailure IntegerLiteralOutOfRange))
                        (lambda unrestricted predecessor : Nat .
                          (lambda unrestricted induction : (family IntegerLiteralResult) .
                            (constructor
                              IntegerLiteralResult
                              IntegerLiteralWord
                              width
                              sign
                              (integerLiteralEncodeWidth
                                width
                                (stdU64SubtractWrapping integerLiteralZero magnitude)))))
                        (integerLiteralLessOrEqual
                          magnitude
                          (integerLiteralSignedNegativeBound width))))))))
            (branch
              IntegerLiteralFoldFailed
              failure
              .
              (constructor IntegerLiteralResult IntegerLiteralFailed failure)))))))

-- Inspect only the first byte.  This keeps the empty/nonempty decision
-- bounded instead of materializing bytes-length as a second unary traversal
-- before the checked digit fold.
def integerLiteralHasDigits =
  (lambda unrestricted digits : Bytes .
    (bytes-eliminate
      (lambda unrestricted remaining : Bytes . Nat)
      zero
      (lambda unrestricted head : Byte .
        (lambda unrestricted tail : Bytes . (lambda unrestricted continue : Nat . (succ zero))))
      digits))

def integerLiteralParse =
  (lambda unrestricted radix : (family IntegerLiteralRadix) .
    (lambda unrestricted kind : (family IntegerLiteralKind) .
      (lambda unrestricted sign : (family IntegerLiteralSign) .
        (lambda unrestricted width : (family IntegerLiteralWidth) .
          (lambda unrestricted digits : Bytes .
            (nat-eliminate
              (lambda unrestricted current : Nat . (family IntegerLiteralResult))
              (integerLiteralFailureResult
                (constructor IntegerLiteralFailure IntegerLiteralMissingDigits))
              (lambda unrestricted predecessor : Nat .
                (lambda unrestricted induction : (family IntegerLiteralResult) .
                  (eliminate
                    IntegerLiteralSyntaxResult
                    (lambda unrestricted current : (family IntegerLiteralSyntaxResult) .
                      (family IntegerLiteralResult))
                    (integerLiteralValidateSeparators radix digits)
                    (branch
                      IntegerLiteralSyntaxAccepted
                      .
                      (integerLiteralFinish
                        kind
                        sign
                        width
                        (integerLiteralFoldDigits radix (integerLiteralStripSeparators digits))))
                    (branch
                      IntegerLiteralSyntaxFailed
                      failure
                      .
                      (integerLiteralFailureResult failure)))))
              (integerLiteralHasDigits digits)))))))

-- The public parser is intentionally continuation-shaped: bytes-eliminate
-- visits source bytes in order, so malformed syntax is observed before any
-- later arithmetic result can be accepted.  The radix-specific digit checker
-- is kept as a separate owner for the future lexer bridge.
def integerLiteralParseEmpty =
  (lambda unrestricted radix : (family IntegerLiteralRadix) .
    (lambda unrestricted sign : (family IntegerLiteralSign) .
      (lambda unrestricted width : (family IntegerLiteralWidth) .
        (integerLiteralFailureResult
          (constructor IntegerLiteralFailure IntegerLiteralMissingDigits)))))

def integerLiteralFailureTag =
  (lambda unrestricted failure : (family IntegerLiteralFailure) .
    (eliminate
      IntegerLiteralFailure
      (lambda unrestricted current : (family IntegerLiteralFailure) . Nat)
      failure
      (branch IntegerLiteralMissingDigits . (succ zero))
      (branch IntegerLiteralBadDigit . (succ (succ zero)))
      (branch IntegerLiteralBadSeparator . (succ (succ (succ zero))))
      (branch IntegerLiteralOutOfRange . (succ (succ (succ (succ zero)))))))

def integerLiteralResultBytes =
  (lambda unrestricted result : (family IntegerLiteralResult) .
    (eliminate
      IntegerLiteralResult
      (lambda unrestricted current : (family IntegerLiteralResult) . Bytes)
      result
      (branch IntegerLiteralWord width sign bytes . bytes)
      (branch IntegerLiteralFailed failure . b"")))

def integerLiteralResultFailureTag =
  (lambda unrestricted result : (family IntegerLiteralResult) .
    (eliminate
      IntegerLiteralResult
      (lambda unrestricted current : (family IntegerLiteralResult) . Nat)
      result
      (branch IntegerLiteralWord width sign bytes . zero)
      (branch IntegerLiteralFailed failure . (integerLiteralFailureTag failure))))