{-# OPTIONS --safe --cubical #-}

module Spartan6.Foundation.Hex where

open import Spartan6.Prelude

open import Agda.Builtin.Char using (Char; primCharEquality)
open import Agda.Builtin.String using (primStringToList)

-- A nibble is written in conventional display order:
--
--   b3 ∷ b2 ∷ b1 ∷ b0 ∷ []
--
-- Thus the head is the most-significant bit and the final element is the
-- least-significant bit.

Nibble : Type₀
Nibble = Vec Bit 

nibble0 nibble1 nibble2 nibble3 : Nibble
nibble0 = low ∷ low ∷ low  ∷ low  ∷ []
nibble1 = low ∷ low ∷ low  ∷ high ∷ []
nibble2 = low ∷ low ∷ high ∷ low  ∷ []
nibble3 = low ∷ low ∷ high ∷ high ∷ []

nibble4 nibble5 nibble6 nibble7 : Nibble
nibble4 = low ∷ high ∷ low  ∷ low  ∷ []
nibble5 = low ∷ high ∷ low  ∷ high ∷ []
nibble6 = low ∷ high ∷ high ∷ low  ∷ []
nibble7 = low ∷ high ∷ high ∷ high ∷ []

nibble8 nibble9 nibbleA nibbleB : Nibble
nibble8 = high ∷ low ∷ low  ∷ low  ∷ []
nibble9 = high ∷ low ∷ low  ∷ high ∷ []
nibbleA = high ∷ low ∷ high ∷ low  ∷ []
nibbleB = high ∷ low ∷ high ∷ high ∷ []

nibbleC nibbleD nibbleE nibbleF : Nibble
nibbleC = high ∷ high ∷ low  ∷ low  ∷ []
nibbleD = high ∷ high ∷ low  ∷ high ∷ []
nibbleE = high ∷ high ∷ high ∷ low  ∷ []
nibbleF = high ∷ high ∷ high ∷ high ∷ []

-- Only the safe builtin character equality primitive is used to classify
-- input characters.  No locale, external process, or partial numeric parser
-- is involved.

hexDigit : Char → Maybe Nibble
hexDigit char =
  if primCharEquality char '0' then just nibble0 else
  if primCharEquality char '1' then just nibble1 else
  if primCharEquality char '2' then just nibble2 else
  if primCharEquality char '3' then just nibble3 else
  if primCharEquality char '4' then just nibble4 else
  if primCharEquality char '5' then just nibble5 else
  if primCharEquality char '6' then just nibble6 else
  if primCharEquality char '7' then just nibble7 else
  if primCharEquality char '8' then just nibble8 else
  if primCharEquality char '9' then just nibble9 else
  if primCharEquality char 'a' then just nibbleA else
  if primCharEquality char 'A' then just nibbleA else
  if primCharEquality char 'b' then just nibbleB else
  if primCharEquality char 'B' then just nibbleB else
  if primCharEquality char 'c' then just nibbleC else
  if primCharEquality char 'C' then just nibbleC else
  if primCharEquality char 'd' then just nibbleD else
  if primCharEquality char 'D' then just nibbleD else
  if primCharEquality char 'e' then just nibbleE else
  if primCharEquality char 'E' then just nibbleE else
  if primCharEquality char 'f' then just nibbleF else
  if primCharEquality char 'F' then just nibbleF else
  nothing

nibbleToMSBList : Nibble → List Bit
nibbleToMSBList (b3 ∷ b2 ∷ b1 ∷ b0 ∷ []) =
  b3 ∷ᴸ b2 ∷ᴸ b1 ∷ᴸ b0 ∷ᴸ []ᴸ

-- Text digits are decoded left-to-right and each digit remains MSB-first.
-- For example, "1A" becomes 0001 followed by 1010.

decodeCharsMSB : List Char → Maybe (List Bit)
decodeCharsMSB []ᴸ = just []ᴸ
decodeCharsMSB (char ∷ᴸ chars) with hexDigit char
... | nothing = nothing
... | just nibble with decodeCharsMSB chars
...   | nothing = nothing
...   | just bits = just (nibbleToMSBList nibble ++ᴸ bits)

decodeHexMSB : String → Maybe (List Bit)
decodeHexMSB text = decodeCharsMSB (primStringToList text)

reverseOnto : ∀ {ℓ} {A : Type ℓ} → List A → List A → List A
reverseOnto []ᴸ accumulator = accumulator
reverseOnto (value ∷ᴸ values) accumulator =
  reverseOnto values (value ∷ᴸ accumulator)

reverseList : ∀ {ℓ} {A : Type ℓ} → List A → List A
reverseList values = reverseOnto values []ᴸ

-- Vendor INIT index order places the least-significant bit first: the head of
-- the result is INIT[0], followed by INIT[1], and so on.  Converting a normal
-- hexadecimal spelling therefore reverses the complete MSB-first bit list,
-- including both digit order and bit order inside each nibble.

toVendorINITOrder : List Bit → List Bit
toVendorINITOrder = reverseList

decodeHexINITOrder : String → Maybe (List Bit)
decodeHexINITOrder text with decodeHexMSB text
... | nothing = nothing
... | just bits = just (toVendorINITOrder bits)

-- Exact-size validation.  Unlike truncating conversions, this succeeds only
-- when the list contains precisely the requested number of elements.

listToVecExact : ∀ {ℓ} {A : Type ℓ} (size : ℕ)
  → List A → Maybe (Vec A size)
listToVecExact zero    []ᴸ             = just []
listToVecExact zero    (value ∷ᴸ rest) = nothing
listToVecExact (suc n) []ᴸ             = nothing
listToVecExact (suc n) (value ∷ᴸ rest) with listToVecExact n rest
... | nothing = nothing
... | just values = just (value ∷ values)

decodeHexMSBFixed : (bitCount : ℕ) → String → Maybe (Vec Bit bitCount)
decodeHexMSBFixed bitCount text with decodeHexMSB text
... | nothing = nothing
... | just bits = listToVecExact bitCount bits

decodeHexINITFixed : (bitCount : ℕ) → String → Maybe (Vec Bit bitCount)
decodeHexINITFixed bitCount text with decodeHexINITOrder text
... | nothing = nothing
... | just bits = listToVecExact bitCount bits

-- LUT1 has a documented two-bit INIT even though hexadecimal text is
-- nibble-sized.  Its canonical spelling is one digit in the range 0..3.  The
-- upper two nibble bits must be zero; the result is returned in INIT index
-- order [ INIT[0] , INIT[1] ].  Values 4..F are rejected rather than silently
-- truncated.

twoBitINITNibble : Nibble → Maybe (Vec Bit )
twoBitINITNibble (b3 ∷ b2 ∷ b1 ∷ b0 ∷ []) =
  if b3 or b2
  then nothing
  else just (b0 ∷ b1 ∷ [])

decodeTwoBitINITChars : List Char → Maybe (Vec Bit )
decodeTwoBitINITChars []ᴸ = nothing
decodeTwoBitINITChars (char ∷ᴸ []ᴸ) with hexDigit char
... | nothing = nothing
... | just nibble = twoBitINITNibble nibble
decodeTwoBitINITChars (first ∷ᴸ second ∷ᴸ rest) = nothing

decodeHexINIT2 : String → Maybe (Vec Bit )
decodeHexINIT2 text = decodeTwoBitINITChars (primStringToList text)

-- Checked digit examples.

digit-0 : hexDigit '0' ≡ just (low ∷ low ∷ low ∷ low ∷ [])
digit-0 = refl

digit-1 : hexDigit '1' ≡ just (low ∷ low ∷ low ∷ high ∷ [])
digit-1 = refl

digit-8 : hexDigit '8' ≡ just (high ∷ low ∷ low ∷ low ∷ [])
digit-8 = refl

digit-F : hexDigit 'F' ≡ just (high ∷ high ∷ high ∷ high ∷ [])
digit-F = refl

digit-f : hexDigit 'f' ≡ just (high ∷ high ∷ high ∷ high ∷ [])
digit-f = refl

invalid-digit : hexDigit 'G' ≡ nothing
invalid-digit = refl

-- "1A" in conventional text/MSB order is 0001_1010.

multi-digit-MSB :
  decodeHexMSB "1A"
  ≡ just
      (low ∷ᴸ low ∷ᴸ low ∷ᴸ high
       ∷ᴸ high ∷ᴸ low ∷ᴸ high ∷ᴸ low ∷ᴸ []ᴸ)
multi-digit-MSB = refl

-- In vendor index order the same value is INIT[0..7] = 0101_1000.

multi-digit-INIT-order :
  decodeHexINITOrder "1A"
  ≡ just
      (low ∷ᴸ high ∷ᴸ low ∷ᴸ high
       ∷ᴸ high ∷ᴸ low ∷ᴸ low ∷ᴸ low ∷ᴸ []ᴸ)
multi-digit-INIT-order = refl

fixed-eight-bits :
  decodeHexINITFixed  "1A"
  ≡ just (low ∷ high ∷ low ∷ high ∷ high ∷ low ∷ low ∷ low ∷ [])
fixed-eight-bits = refl

fixed-size-rejects-too-many-bits : decodeHexMSBFixed  "1A" ≡ nothing
fixed-size-rejects-too-many-bits = refl

two-bit-INIT-zero : decodeHexINIT2 "0" ≡ just (low ∷ low ∷ [])
two-bit-INIT-zero = refl

two-bit-INIT-one : decodeHexINIT2 "1" ≡ just (high ∷ low ∷ [])
two-bit-INIT-one = refl

two-bit-INIT-two : decodeHexINIT2 "2" ≡ just (low ∷ high ∷ [])
two-bit-INIT-two = refl

two-bit-INIT-three : decodeHexINIT2 "3" ≡ just (high ∷ high ∷ [])
two-bit-INIT-three = refl

two-bit-INIT-rejects-high-padding : decodeHexINIT2 "4" ≡ nothing
two-bit-INIT-rejects-high-padding = refl

two-bit-INIT-rejects-two-digits : decodeHexINIT2 "00" ≡ nothing
two-bit-INIT-rejects-two-digits = refl