module Std.Codec

import Std.Foundation
import Std.List
import Std.Natural

-- Codecs (Language Platform PRD §28.2 Hash/codec, LP-804).
--
-- Fixed-width and variable-length encodings with BOUNDED decoders: every
-- decoder here answers with what it read and what is left, and a decoder that
-- runs out of input answers that it did, rather than failing or reading past
-- the end. Encodings are little-endian and canonical: one value has exactly
-- one encoding, so equal values have equal bytes and a digest over them means
-- something.
-- What a decoder answers: the value and the remaining input, or the fact that
-- the input ended too soon.
family StdDecoded : Type 0
parameter erased stdDecodedValueType : Type 0
constructor StdDecodedValue
field unrestricted stdDecodedItem : stdDecodedValueType
field unrestricted stdDecodedRest : Bytes
constructor StdDecodedTruncated

end-family

-- 256, the base of a byte, written once.
def stdCodecByteBase =
  (succ (byte-to-nat (byte 255)))

-- 128, the base of a LEB128 group.
def stdCodecVarintBase =
  (byte-to-nat (byte 128))

-- The low byte of a natural.
def stdCodecLowByte =
  (lambda unrestricted value : Nat . (nat-to-byte (naturalModuloUnchecked value stdCodecByteBase)))

-- One byte, encoded.
def stdCodecEncodeByte =
  (lambda unrestricted value : Byte . (bytes-cons value b""))

-- One byte, decoded, with the rest of the input.
def stdCodecDecodeByte =
  (lambda unrestricted input : Bytes .
    (eliminate
      StdBool
      (lambda unrestricted current : (family StdBool) . (family StdDecoded Byte))
      (stdBoolFromNatural (bytes-length input))
      (branch
        StdTrue
        .
        (constructor StdDecoded StdDecodedValue Byte (bytes-head input) (bytes-tail input)))
      (branch StdFalse . (constructor StdDecoded StdDecodedTruncated Byte))))

-- LEB128, the variable-length encoding the interface cache uses: seven bits
-- per byte, low group first, the high bit meaning "more follows". Five groups
-- cover every value a 32-bit quantity can hold, and the encoding is canonical
-- because groups stop as soon as the remainder is zero.
def stdCodecEncodeVarint =
  (lambda unrestricted value : Nat .
    (let unrestricted group0 =
      (naturalModuloUnchecked value stdCodecVarintBase)
      in
      (let unrestricted rest0 =
        (naturalDivideUnchecked value stdCodecVarintBase)
        in
        (eliminate
          StdBool
          (lambda unrestricted current : (family StdBool) . Bytes)
          (stdBoolFromNatural rest0)
          -- more groups follow: set the continuation bit on this one
          (branch
            StdTrue
            .
            (bytes-cons
              (nat-to-byte (naturalAdd group0 stdCodecVarintBase))
              (let unrestricted group1 =
                (naturalModuloUnchecked rest0 stdCodecVarintBase)
                in
                (let unrestricted rest1 =
                  (naturalDivideUnchecked rest0 stdCodecVarintBase)
                  in
                  (eliminate
                    StdBool
                    (lambda unrestricted current : (family StdBool) . Bytes)
                    (stdBoolFromNatural rest1)
                    (branch
                      StdTrue
                      .
                      (bytes-cons
                        (nat-to-byte (naturalAdd group1 stdCodecVarintBase))
                        (let unrestricted group2 =
                          (naturalModuloUnchecked rest1 stdCodecVarintBase)
                          in
                          (let unrestricted rest2 =
                            (naturalDivideUnchecked rest1 stdCodecVarintBase)
                            in
                            (eliminate
                              StdBool
                              (lambda unrestricted current : (family StdBool) . Bytes)
                              (stdBoolFromNatural rest2)
                              (branch
                                StdTrue
                                .
                                (bytes-cons
                                  (nat-to-byte (naturalAdd group2 stdCodecVarintBase))
                                  (bytes-cons
                                    (nat-to-byte (naturalModuloUnchecked rest2 stdCodecVarintBase))
                                    b"")))
                              (branch StdFalse . (bytes-cons (nat-to-byte group2) b"")))))))
                    (branch StdFalse . (bytes-cons (nat-to-byte group1) b"")))))))
          (branch StdFalse . (bytes-cons (nat-to-byte group0) b""))))))

-- A natural as four little-endian bytes. Values wider than the field are
-- reduced modulo the width, which is stated here rather than discovered: a
-- caller who needs a checked conversion uses `Data.CheckedWord64`.
def stdCodecEncodeWord32 =
  (lambda unrestricted value : Nat .
    (let unrestricted byte0 =
      (naturalModuloUnchecked value stdCodecByteBase)
      in
      (let unrestricted rest1 =
        (naturalDivideUnchecked value stdCodecByteBase)
        in
        (let unrestricted byte1 =
          (naturalModuloUnchecked rest1 stdCodecByteBase)
          in
          (let unrestricted rest2 =
            (naturalDivideUnchecked rest1 stdCodecByteBase)
            in
            (let unrestricted byte2 =
              (naturalModuloUnchecked rest2 stdCodecByteBase)
              in
              (let unrestricted rest3 =
                (naturalDivideUnchecked rest2 stdCodecByteBase)
                in
                (bytes-cons
                  (nat-to-byte byte0)
                  (bytes-cons
                    (nat-to-byte byte1)
                    (bytes-cons
                      (nat-to-byte byte2)
                      (bytes-cons
                        (nat-to-byte (naturalModuloUnchecked rest3 stdCodecByteBase))
                        b"")))))))))))

-- Four little-endian bytes as a natural, with the remaining input. A shorter
-- input is reported as truncated, never padded.
def stdCodecDecodeWord32 =
  (lambda unrestricted input : Bytes .
    (eliminate
      StdBool
      (lambda unrestricted current : (family StdBool) . (family StdDecoded Nat))
      (stdBoolFromNatural (nat-less-than (bytes-length input) (byte-to-nat (byte 4))))
      (branch StdTrue . (constructor StdDecoded StdDecodedTruncated Nat))
      (branch
        StdFalse
        .
        (let unrestricted byte0 =
          (byte-to-nat (bytes-head input))
          in
          (let unrestricted after0 =
            (bytes-tail input)
            in
            (let unrestricted byte1 =
              (byte-to-nat (bytes-head after0))
              in
              (let unrestricted after1 =
                (bytes-tail after0)
                in
                (let unrestricted byte2 =
                  (byte-to-nat (bytes-head after1))
                  in
                  (let unrestricted after2 =
                    (bytes-tail after1)
                    in
                    (let unrestricted byte3 =
                      (byte-to-nat (bytes-head after2))
                      in
                      (constructor
                        StdDecoded
                        StdDecodedValue
                        Nat
                        (naturalAdd
                          byte0
                          (naturalMultiply
                            stdCodecByteBase
                            (naturalAdd
                              byte1
                              (naturalMultiply
                                stdCodecByteBase
                                (naturalAdd byte2 (naturalMultiply stdCodecByteBase byte3))))))
                        (bytes-tail after2))))))))))))

-- The checksum of a byte string: the same one the source snapshot uses, so a
-- library caller and the compiler agree on what a content digest is.
def stdCodecChecksum =
  (lambda unrestricted input : Bytes . (bytes-checksum input))

-- Did this decoder run out of input?
def stdDecodedIsTruncated =
  (lambda erased valueType : Type 0 .
    (lambda unrestricted decoded : (family StdDecoded valueType) .
      (eliminate
        StdDecoded
        (lambda unrestricted current : (family StdDecoded valueType) . (family StdBool))
        decoded
        (branch StdDecodedValue item rest . (constructor StdBool StdFalse))
        (branch StdDecodedTruncated . (constructor StdBool StdTrue)))))

-- The decoded value, or a default when the input ended too soon.
def stdDecodedValueOr =
  (lambda erased valueType : Type 0 .
    (lambda unrestricted fallback : valueType .
      (lambda unrestricted decoded : (family StdDecoded valueType) .
        (eliminate
          StdDecoded
          (lambda unrestricted current : (family StdDecoded valueType) . valueType)
          decoded
          (branch StdDecodedValue item rest . item)
          (branch StdDecodedTruncated . fallback)))))