module Compiler.NaturalMagnitude

import Compiler.NaturalMagnitudeArithmetic
import Compiler.IntegerLiteral
import Std.Natural

-- Checked admission for compile-time arbitrary natural magnitudes.
-- Canonical payload: decimal digit values 0..9, least significant first;
-- empty zero, no most-significant zero, at most 4096 significant digits.
family NaturalMagnitudeFailure : Type 0
constructor NaturalMagnitudeLiteralMalformed
field unrestricted naturalMagnitudeLiteralFailure : (family IntegerLiteralFailure)
constructor NaturalMagnitudeTooLarge
constructor NaturalMagnitudeNonCanonical
constructor NaturalMagnitudeNeedsType

end-family

family NaturalMagnitudeResult : Type 0
constructor NaturalMagnitudeAccepted
field unrestricted naturalMagnitudeDigitsLE : Bytes
constructor NaturalMagnitudeRejected
field unrestricted naturalMagnitudeFailure : (family NaturalMagnitudeFailure)

end-family

def magnitudeDigitLimit =
  (Std.Natural/naturalMultiply (byte-to-nat (byte 64)) (byte-to-nat (byte 64)))

def magnitudeDigitsValid =
  (lambda unrestricted digits : Bytes .
    (bytes-eliminate
      (lambda unrestricted rest : Bytes . Nat)
      (succ zero)
      (lambda unrestricted head : Byte .
        (lambda unrestricted tail : Bytes .
          (lambda unrestricted continue : Nat .
            (Std.Natural/naturalAnd
              (nat-less-than (byte-to-nat head) (byte-to-nat (byte 10)))
              continue))))
      digits))

def magnitudeBudgetAccept =
  (lambda unrestricted digits : Bytes .
    (app
      (nat-eliminate
        (lambda unrestricted flag : Nat .
          (pi unrestricted force : Nat . (family NaturalMagnitudeResult)))
        (lambda unrestricted force : Nat .
          (constructor NaturalMagnitudeResult NaturalMagnitudeAccepted digits))
        (lambda unrestricted predecessor : Nat .
          (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalMagnitudeResult)) .
            (lambda unrestricted force : Nat .
              (constructor
                NaturalMagnitudeResult
                NaturalMagnitudeRejected
                (constructor NaturalMagnitudeFailure NaturalMagnitudeTooLarge)))))
        (nat-less-than magnitudeDigitLimit (bytes-length digits)))
      zero))

def magnitudeDecodeCanonical =
  (lambda unrestricted digits : Bytes .
    (app
      (nat-eliminate
        (lambda unrestricted flag : Nat .
          (pi unrestricted force : Nat . (family NaturalMagnitudeResult)))
        (lambda unrestricted force : Nat .
          (constructor
            NaturalMagnitudeResult
            NaturalMagnitudeRejected
            (constructor NaturalMagnitudeFailure NaturalMagnitudeNonCanonical)))
        (lambda unrestricted predecessor : Nat .
          (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalMagnitudeResult)) .
            (lambda unrestricted force : Nat . (magnitudeBudgetAccept digits))))
        (Std.Natural/naturalAnd
          (magnitudeDigitsValid digits)
          (bytes-equal digits (magnitudeNormalize digits))))
      zero))

def magnitudeAdmitNormalized =
  (lambda unrestricted digits : Bytes . (magnitudeDecodeCanonical (magnitudeNormalize digits)))

def magnitudeDecimalDigits =
  (lambda unrestricted digits : Bytes .
    (magnitudeAdmitNormalized
      (app
        (bytes-eliminate
          (lambda unrestricted rest : Bytes . (pi unrestricted accumulator : Bytes . Bytes))
          (lambda unrestricted accumulator : Bytes . accumulator)
          (lambda unrestricted head : Byte .
            (lambda unrestricted tail : Bytes .
              (lambda unrestricted continue : (pi unrestricted accumulator : Bytes . Bytes) .
                (lambda unrestricted accumulator : Bytes .
                  (continue
                    (bytes-cons
                      (nat-to-byte
                        (Std.Natural/naturalSaturatingSubtract
                          (byte-to-nat head)
                          (byte-to-nat (byte 48))))
                      accumulator))))))
          digits)
        b"")))

def magnitudeRadixScale =
  (lambda unrestricted radix : (family IntegerLiteralRadix) .
    (lambda unrestricted digits : Bytes .
      (eliminate
        IntegerLiteralRadix
        (lambda unrestricted current : (family IntegerLiteralRadix) . Bytes)
        radix
        (branch IntegerLiteralDecimal . (magnitudeMultiplyDigit digits (byte 10)))
        (branch IntegerLiteralBinary . (magnitudeDouble digits))
        (branch
          IntegerLiteralHexadecimal
          .
          (magnitudeRepeatSmall
            Bytes
            (byte-to-nat (byte 4))
            (lambda unrestricted value : Bytes . (magnitudeDouble value))
            digits)))))

def magnitudeRadixDigits =
  (lambda unrestricted radix : (family IntegerLiteralRadix) .
    (lambda unrestricted digits : Bytes .
      (app
        (bytes-eliminate
          (lambda unrestricted rest : Bytes .
            (pi unrestricted accumulator : Bytes . (family NaturalMagnitudeResult)))
          (lambda unrestricted accumulator : Bytes .
            (constructor NaturalMagnitudeResult NaturalMagnitudeAccepted accumulator))
          (lambda unrestricted head : Byte .
            (lambda unrestricted tail : Bytes .
              (lambda unrestricted continue : (pi unrestricted accumulator : Bytes . (family NaturalMagnitudeResult)) .
                (lambda unrestricted accumulator : Bytes .
                  (eliminate
                    IntegerLiteralDigitResult
                    (lambda unrestricted current : (family IntegerLiteralDigitResult) .
                      (family NaturalMagnitudeResult))
                    (Compiler.IntegerLiteral/integerLiteralDecodeDigit radix head)
                    (branch
                      IntegerLiteralDigitValue
                      digit
                      .
                      (eliminate
                        NaturalMagnitudeResult
                        (lambda unrestricted current : (family NaturalMagnitudeResult) .
                          (family NaturalMagnitudeResult))
                        (magnitudeBudgetAccept
                          (magnitudeAdd
                            (magnitudeFromNatural digit)
                            (magnitudeRadixScale radix accumulator)))
                        (branch NaturalMagnitudeAccepted next . (continue next))
                        (branch
                          NaturalMagnitudeRejected
                          failure
                          .
                          (constructor NaturalMagnitudeResult NaturalMagnitudeRejected failure))))
                    (branch
                      IntegerLiteralDigitFailed
                      failure
                      .
                      (constructor
                        NaturalMagnitudeResult
                        NaturalMagnitudeRejected
                        (constructor
                          NaturalMagnitudeFailure
                          NaturalMagnitudeLiteralMalformed
                          failure))))))))
          digits)
        b"")))

def magnitudeConvertValidatedDigits =
  (lambda unrestricted radix : (family IntegerLiteralRadix) .
    (lambda unrestricted digits : Bytes .
      (eliminate
        IntegerLiteralRadix
        (lambda unrestricted current : (family IntegerLiteralRadix) .
          (family NaturalMagnitudeResult))
        radix
        (branch IntegerLiteralDecimal . (magnitudeDecimalDigits digits))
        (branch IntegerLiteralBinary . (magnitudeRadixDigits radix digits))
        (branch IntegerLiteralHexadecimal . (magnitudeRadixDigits radix digits)))))

def magnitudeParseDigits =
  (lambda unrestricted radix : (family IntegerLiteralRadix) .
    (lambda unrestricted digits : Bytes .
      (app
        (nat-eliminate
          (lambda unrestricted flag : Nat .
            (pi unrestricted force : Nat . (family NaturalMagnitudeResult)))
          (lambda unrestricted force : Nat .
            (eliminate
              IntegerLiteralSyntaxResult
              (lambda unrestricted current : (family IntegerLiteralSyntaxResult) .
                (family NaturalMagnitudeResult))
              (Compiler.IntegerLiteral/integerLiteralValidateSeparators radix digits)
              (branch
                IntegerLiteralSyntaxAccepted
                .
                (magnitudeConvertValidatedDigits
                  radix
                  (Compiler.IntegerLiteral/integerLiteralStripSeparators digits)))
              (branch
                IntegerLiteralSyntaxFailed
                failure
                .
                (constructor
                  NaturalMagnitudeResult
                  NaturalMagnitudeRejected
                  (constructor NaturalMagnitudeFailure NaturalMagnitudeLiteralMalformed failure)))))
          (lambda unrestricted predecessor : Nat .
            (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalMagnitudeResult)) .
              (lambda unrestricted force : Nat .
                (constructor
                  NaturalMagnitudeResult
                  NaturalMagnitudeRejected
                  (constructor
                    NaturalMagnitudeFailure
                    NaturalMagnitudeLiteralMalformed
                    (constructor IntegerLiteralFailure IntegerLiteralMissingDigits))))))
          (bytes-equal digits b""))
        zero)))

def magnitudeParseUnsigned =
  (lambda unrestricted spelling : Bytes .
    (app
      (nat-eliminate
        (lambda unrestricted flag : Nat .
          (pi unrestricted force : Nat . (family NaturalMagnitudeResult)))
        (lambda unrestricted force : Nat .
          (app
            (nat-eliminate
              (lambda unrestricted flag : Nat .
                (pi unrestricted force : Nat . (family NaturalMagnitudeResult)))
              (lambda unrestricted force : Nat .
                (magnitudeParseDigits
                  (constructor IntegerLiteralRadix IntegerLiteralDecimal)
                  spelling))
              (lambda unrestricted predecessor : Nat .
                (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalMagnitudeResult)) .
                  (lambda unrestricted force : Nat .
                    (app
                      (nat-eliminate
                        (lambda unrestricted flag : Nat .
                          (pi unrestricted force : Nat . (family NaturalMagnitudeResult)))
                        (lambda unrestricted force : Nat .
                          (app
                            (nat-eliminate
                              (lambda unrestricted flag : Nat .
                                (pi unrestricted force : Nat . (family NaturalMagnitudeResult)))
                              (lambda unrestricted force : Nat .
                                (magnitudeParseDigits
                                  (constructor IntegerLiteralRadix IntegerLiteralDecimal)
                                  spelling))
                              (lambda unrestricted predecessor : Nat .
                                (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalMagnitudeResult)) .
                                  (lambda unrestricted force : Nat .
                                    (magnitudeParseDigits
                                      (constructor IntegerLiteralRadix IntegerLiteralBinary)
                                      (bytes-tail (bytes-tail spelling))))))
                              (Std.Natural/naturalOr
                                (byte-equal (bytes-head (bytes-tail spelling)) (byte 98))
                                (byte-equal (bytes-head (bytes-tail spelling)) (byte 66))))
                            zero))
                        (lambda unrestricted predecessor : Nat .
                          (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalMagnitudeResult)) .
                            (lambda unrestricted force : Nat .
                              (magnitudeParseDigits
                                (constructor IntegerLiteralRadix IntegerLiteralHexadecimal)
                                (bytes-tail (bytes-tail spelling))))))
                        (Std.Natural/naturalOr
                          (byte-equal (bytes-head (bytes-tail spelling)) (byte 120))
                          (byte-equal (bytes-head (bytes-tail spelling)) (byte 88))))
                      zero))))
              (byte-equal (bytes-head spelling) (byte 48)))
            zero))
        (lambda unrestricted predecessor : Nat .
          (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalMagnitudeResult)) .
            (lambda unrestricted force : Nat .
              (constructor
                NaturalMagnitudeResult
                NaturalMagnitudeRejected
                (constructor NaturalMagnitudeFailure NaturalMagnitudeNeedsType)))))
        (byte-equal (bytes-head spelling) (byte 45)))
      zero))

def magnitudeCanonicalValid =
  (lambda unrestricted digits : Bytes .
    (eliminate
      NaturalMagnitudeResult
      (lambda unrestricted result : (family NaturalMagnitudeResult) . Nat)
      (magnitudeDecodeCanonical digits)
      (branch NaturalMagnitudeAccepted valid . (succ zero))
      (branch NaturalMagnitudeRejected failure . zero)))

def magnitudeFailureCode =
  (lambda unrestricted error : (family NaturalMagnitudeFailure) .
    (eliminate
      NaturalMagnitudeFailure
      (lambda unrestricted current : (family NaturalMagnitudeFailure) . Bytes)
      error
      (branch
        NaturalMagnitudeLiteralMalformed
        failure
        .
        (eliminate
          IntegerLiteralFailure
          (lambda unrestricted current : (family IntegerLiteralFailure) . Bytes)
          failure
          (branch
            IntegerLiteralMissingDigits
            .
            b"ALPHA-LITERAL-MISSING-DIGITS")
          (branch
            IntegerLiteralBadDigit
            .
            b"ALPHA-LITERAL-BAD-DIGIT")
          (branch
            IntegerLiteralBadSeparator
            .
            b"ALPHA-LITERAL-BAD-SEPARATOR")
          (branch
            IntegerLiteralOutOfRange
            .
            b"ALPHA-LITERAL-OUT-OF-RANGE")))
      (branch
        NaturalMagnitudeTooLarge
        .
        b"ALPHA-PARSE-NAT-LITERAL-TOO-LARGE")
      (branch
        NaturalMagnitudeNonCanonical
        .
        b"ALPHA-NAT-MAGNITUDE-NONCANONICAL")
      (branch
        NaturalMagnitudeNeedsType
        .
        b"ALPHA-LITERAL-NEEDS-TYPE")))

-- Validate both operands before invoking a checked binary operation.
def magnitudeBinaryChecked =
  (lambda unrestricted operation : (pi unrestricted left : Bytes . (pi unrestricted right : Bytes . (family NaturalMagnitudeResult))) .
    (lambda unrestricted left : Bytes .
      (lambda unrestricted right : Bytes .
        (eliminate
          NaturalMagnitudeResult
          (lambda unrestricted current : (family NaturalMagnitudeResult) .
            (family NaturalMagnitudeResult))
          (magnitudeDecodeCanonical left)
          (branch
            NaturalMagnitudeAccepted
            a
            .
            (eliminate
              NaturalMagnitudeResult
              (lambda unrestricted current : (family NaturalMagnitudeResult) .
                (family NaturalMagnitudeResult))
              (magnitudeDecodeCanonical right)
              (branch NaturalMagnitudeAccepted b . (operation a b))
              (branch
                NaturalMagnitudeRejected
                error
                .
                (constructor NaturalMagnitudeResult NaturalMagnitudeRejected error))))
          (branch
            NaturalMagnitudeRejected
            error
            .
            (constructor NaturalMagnitudeResult NaturalMagnitudeRejected error))))))

-- Nonzero n- and m-digit products have at least n+m-1 digits. Refuse
-- guaranteed overflow before multiplication; the boundary still needs exact admission.
def magnitudeMultiplyAdmitted =
  (lambda unrestricted left : Bytes .
    (lambda unrestricted right : Bytes .
      (app
        (nat-eliminate
          (lambda unrestricted flag : Nat .
            (pi unrestricted force : Nat . (family NaturalMagnitudeResult)))
          (lambda unrestricted force : Nat .
            (magnitudeAdmitNormalized (magnitudeMultiply left right)))
          (lambda unrestricted predecessor : Nat .
            (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalMagnitudeResult)) .
              (lambda unrestricted force : Nat .
                (constructor
                  NaturalMagnitudeResult
                  NaturalMagnitudeRejected
                  (constructor NaturalMagnitudeFailure NaturalMagnitudeTooLarge)))))
          (nat-less-than
            (succ magnitudeDigitLimit)
            (Std.Natural/naturalAdd (bytes-length left) (bytes-length right))))
        zero)))

def magnitudeAddChecked =
  (magnitudeBinaryChecked
    (lambda unrestricted left : Bytes .
      (lambda unrestricted right : Bytes . (magnitudeAdmitNormalized (magnitudeAdd left right)))))

def magnitudeSubtractChecked =
  (magnitudeBinaryChecked
    (lambda unrestricted left : Bytes .
      (lambda unrestricted right : Bytes .
        (magnitudeAdmitNormalized (magnitudeSubtract left right)))))

def magnitudeDivideChecked =
  (magnitudeBinaryChecked
    (lambda unrestricted left : Bytes .
      (lambda unrestricted right : Bytes . (magnitudeAdmitNormalized (magnitudeDivide left right)))))

def magnitudeModuloChecked =
  (magnitudeBinaryChecked
    (lambda unrestricted left : Bytes .
      (lambda unrestricted right : Bytes . (magnitudeAdmitNormalized (magnitudeModulo left right)))))

def magnitudeMultiplyChecked =
  (magnitudeBinaryChecked
    (lambda unrestricted left : Bytes .
      (lambda unrestricted right : Bytes . (magnitudeMultiplyAdmitted left right))))

def magnitudeSuccessorChecked =
  (lambda unrestricted digits : Bytes .
    (eliminate
      NaturalMagnitudeResult
      (lambda unrestricted current : (family NaturalMagnitudeResult) .
        (family NaturalMagnitudeResult))
      (magnitudeDecodeCanonical digits)
      (branch
        NaturalMagnitudeAccepted
        value
        .
        (magnitudeAdmitNormalized (magnitudeSuccessor value)))
      (branch
        NaturalMagnitudeRejected
        error
        .
        (constructor NaturalMagnitudeResult NaturalMagnitudeRejected error))))

def magnitudePredecessorChecked =
  (lambda unrestricted digits : Bytes .
    (eliminate
      NaturalMagnitudeResult
      (lambda unrestricted current : (family NaturalMagnitudeResult) .
        (family NaturalMagnitudeResult))
      (magnitudeDecodeCanonical digits)
      (branch
        NaturalMagnitudeAccepted
        value
        .
        (magnitudeAdmitNormalized (magnitudePredecessor value)))
      (branch
        NaturalMagnitudeRejected
        error
        .
        (constructor NaturalMagnitudeResult NaturalMagnitudeRejected error))))