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

module Spartan6.Primitive.LUT where

open import Spartan6.Prelude

import Cubical.Data.FinData.Properties as FinProperties

-- A truth table is stored in vendor INIT order: I0 is the least-significant
-- address bit.  Consequently the vector [ I0 , I1 , ... ] addresses entry
-- I0 + 2 * I1 + ... .

tableSize : ℕ → ℕ
tableSize zero = 1
tableSize (suc n) = tableSize n · 2

TruthTable : ℕ → Type₀
TruthTable n = Vec Bit (tableSize n)

bitIndex : Bit → Fin 2
bitIndex false = fzero
bitIndex true = fsuc fzero

address : ∀ {n} → Vec Bit n → Fin (tableSize n)
address [] = fzero
address {n = suc n} (bit ∷ bits) =
  fst (FinProperties.FinProdChar.Equiv (tableSize n) 2)
      (address bits , bitIndex bit)

evalLUT : ∀ {n} → TruthTable n → Vec Bit n → Bit
evalLUT table inputs = lookup (address inputs) table

LUT6Table : Type₀
LUT6Table = TruthTable 6

allLow6 : Vec Bit 6
allLow6 = low ∷ low ∷ low ∷ low ∷ low ∷ low ∷ []

onlyI0High6 : Vec Bit 6
onlyI0High6 = high ∷ low ∷ low ∷ low ∷ low ∷ low ∷ []

LUT6-all-low-address : address allLow6 ≡ fzero
LUT6-all-low-address = refl

LUT6-I0-is-least-significant : address onlyI0High6 ≡ fsuc fzero
LUT6-I0-is-least-significant = refl

LUT6-all-low-selects-INIT0 : ∀ (table : LUT6Table)
  → evalLUT table allLow6 ≡ lookup fzero table
LUT6-all-low-selects-INIT0 table = refl

LUT6-I0-selects-INIT1 : ∀ (table : LUT6Table)
  → evalLUT table onlyI0High6 ≡ lookup (fsuc fzero) table
LUT6-I0-selects-INIT1 table = refl

notTable : TruthTable 1
notTable = high ∷ low ∷ []

andTable : TruthTable 2
andTable = low ∷ low ∷ low ∷ high ∷ []

xorTable : TruthTable 2
xorTable = low ∷ high ∷ high ∷ low ∷ []

notTable-low : evalLUT notTable (low ∷ []) ≡ high
notTable-low = refl

notTable-high : evalLUT notTable (high ∷ []) ≡ low
notTable-high = refl

andTable-low-high : evalLUT andTable (low ∷ high ∷ []) ≡ low
andTable-low-high = refl

andTable-high-high : evalLUT andTable (high ∷ high ∷ []) ≡ high
andTable-high-high = refl

xorTable-low-low : evalLUT xorTable (low ∷ low ∷ []) ≡ low
xorTable-low-low = refl

xorTable-high-low : evalLUT xorTable (high ∷ low ∷ []) ≡ high
xorTable-high-low = refl

xorTable-low-high : evalLUT xorTable (low ∷ high ∷ []) ≡ high
xorTable-low-high = refl

xorTable-high-high : evalLUT xorTable (high ∷ high ∷ []) ≡ low
xorTable-high-high = refl