module Std.Byte

import Std.Natural

family ByteAddResult : Type 0
constructor ByteAddResultValue
field unrestricted byteAddLow : Byte
field unrestricted byteAddCarry : Nat

end-family

family ByteMultiplyResult : Type 0
constructor ByteMultiplyResultValue
field unrestricted byteMultiplyLow : Byte
field unrestricted byteMultiplyHigh : Byte

end-family

def byteNaturalTwo =
  (succ (succ zero))

def byteNaturalEight =
  (byte-to-nat (byte 8))

def byteNaturalTwoHundredFiftySix =
  (succ (byte-to-nat (byte 255)))

def byteAdd =
  (lambda unrestricted left : Byte .
    (lambda unrestricted right : Byte .
      (app
        (lambda unrestricted total : Nat .
          (constructor
            ByteAddResult
            ByteAddResultValue
            -- total is in 0..510. The primitive conversion keeps its low
            -- eight bits, and its high part is exactly the flag total > 255.
            -- Avoid general unary division/modulo in this bounded operation.
            (nat-to-byte total)
            (nat-less-than (byte-to-nat (byte 255)) total)))
        (naturalAdd (byte-to-nat left) (byte-to-nat right)))))

def byteMultiply =
  (lambda unrestricted left : Byte .
    (lambda unrestricted right : Byte .
      (app
        (lambda unrestricted product : Nat .
          (constructor
            ByteMultiplyResult
            ByteMultiplyResultValue
            (nat-to-byte (naturalModuloUnchecked product byteNaturalTwoHundredFiftySix))
            (nat-to-byte (naturalDivideUnchecked product byteNaturalTwoHundredFiftySix))))
        (naturalMultiply (byte-to-nat left) (byte-to-nat right)))))

-- The bit operations are the L21 byte primitives (one machine operation on
-- every lane). A shift amount is a Nat here, as it always was: an amount of
-- eight or more yields zero, decided by the primitive comparison so that
-- `nat-to-byte` never truncates an amount of 256 or more into a small one.
def byteAnd =
  (lambda unrestricted left : Byte . (lambda unrestricted right : Byte . (byte-and left right)))

def byteOr =
  (lambda unrestricted left : Byte . (lambda unrestricted right : Byte . (byte-or left right)))

def byteXor =
  (lambda unrestricted left : Byte . (lambda unrestricted right : Byte . (byte-xor left right)))

def byteShiftRight =
  (lambda unrestricted value : Byte .
    (lambda unrestricted amount : Nat .
      (nat-eliminate
        (lambda unrestricted current : Nat . Byte)
        (byte 0)
        (lambda unrestricted predecessor : Nat .
          (lambda unrestricted induction : Byte . (byte-shift-right value (nat-to-byte amount))))
        (nat-less-than amount byteNaturalEight))))

def byteShiftLeftTruncated =
  (lambda unrestricted value : Byte .
    (lambda unrestricted amount : Nat .
      (nat-eliminate
        (lambda unrestricted current : Nat . Byte)
        (byte 0)
        (lambda unrestricted predecessor : Nat .
          (lambda unrestricted induction : Byte . (byte-shift-left value (nat-to-byte amount))))
        (nat-less-than amount byteNaturalEight))))

def byteAddWithCarry =
  (lambda unrestricted left : Byte .
    (lambda unrestricted right : Byte .
      (lambda unrestricted carry : Nat .
        (eliminate
          ByteAddResult
          (lambda unrestricted current : (family ByteAddResult) . (family ByteAddResult))
          (byteAdd left right)
          (branch
            ByteAddResultValue
            firstLow
            firstCarry
            .
            (eliminate
              ByteAddResult
              (lambda unrestricted current : (family ByteAddResult) . (family ByteAddResult))
              (byteAdd firstLow (nat-to-byte carry))
              (branch
                ByteAddResultValue
                secondLow
                secondCarry
                .
                (constructor
                  ByteAddResult
                  ByteAddResultValue
                  secondLow
                  (naturalAdd firstCarry secondCarry)))))))))