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

module Spartan6.Netlist.PrimitiveHandler where

open import Spartan6.Prelude

import Spartan6.Netlist.Expression as Expression
import Spartan6.Primitive.Carry4 as Carry4
import Spartan6.Primitive.Clock as Clock
import Spartan6.Primitive.FDRE as FDRE
import Spartan6.Primitive.FDSE as FDSE
import Spartan6.Primitive.IO as IO
import Spartan6.Primitive.LUT as LUT
import Spartan6.Primitive.Mux as Mux

open import Cubical.Data.Vec using (_++_)
open import Cubical.Data.Vec.Properties using
  (FinVec→Vec; Vec→FinVec→Vec)

record CertifiedHandler (inputCount outputCount : ℕ) : Type₀ where
  constructor certifiedHandler
  field
    denotation : Vec Bit inputCount → Vec Bit outputCount
    loweredOutputs : Vec (Expression.Expr inputCount 0) outputCount
    outputsCorrect : ∀ input
      → Expression.evalAll input [] loweredOutputs ≡ denotation input

open CertifiedHandler public

record CertifiedStateHandler
  (inputCount outputCount stateCount : ℕ) : Type₀ where
  constructor certifiedStateHandler
  field
    initialState : Vec Bit stateCount
    stateDenotationOutput :
      Vec Bit inputCount → Vec Bit stateCount → Vec Bit outputCount
    stateDenotationNext :
      Vec Bit inputCount → Vec Bit stateCount → Vec Bit stateCount
    loweredStateOutputs :
      Vec (Expression.Expr inputCount stateCount) outputCount
    loweredNextState :
      Vec (Expression.Expr inputCount stateCount) stateCount
    stateOutputsCorrect : ∀ input state
      → Expression.evalAll input state loweredStateOutputs
        ≡ stateDenotationOutput input state
    nextStateCorrect : ∀ input state
      → Expression.evalAll input state loweredNextState
        ≡ stateDenotationNext input state

open CertifiedStateHandler public

inputExpressions : (count : ℕ) → Vec (Expression.Expr count 0) count
inputExpressions count = FinVec→Vec (λ index → Expression.input index)

eval-indexed-inputs :
  ∀ {source count}
    (input : Vec Bit source)
    (indices : Fin count → Fin source)
  → Expression.evalAll input []
      (FinVec→Vec (λ index → Expression.input (indices index)))
    ≡ FinVec→Vec (λ index → lookup (indices index) input)
eval-indexed-inputs {count = zero} input indices = refl
eval-indexed-inputs {count = suc count} input indices =
  cong (lookup (indices fzero) input ∷_)
    (eval-indexed-inputs input (λ index → indices (fsuc index)))

input-expressions-evaluate : ∀ count (input : Vec Bit count)
  → Expression.evalAll input [] (inputExpressions count) ≡ input
input-expressions-evaluate count input =
  eval-indexed-inputs input (λ index → index)
  ∙ Vec→FinVec→Vec input

identityHandler : CertifiedHandler 1 1
identityHandler = certifiedHandler
  (λ { (input ∷ []) → input ∷ [] })
  (Expression.input fzero ∷ [])
  (λ { (input ∷ []) → refl })

muxF7Handler : CertifiedHandler 3 1
muxF7Handler = certifiedHandler
  (λ { (input0 ∷ input1 ∷ select ∷ []) →
    Mux.muxF7 input0 input1 select ∷ [] })
  (Expression.select
    (Expression.input (fsuc (fsuc fzero)))
    (Expression.input fzero)
    (Expression.input (fsuc fzero)) ∷ [])
  (λ { (input0 ∷ input1 ∷ select ∷ []) → refl })

lutHandler : ∀ {arity} → LUT.TruthTable arity
  → CertifiedHandler arity 1
lutHandler {arity} table = certifiedHandler
  (λ input → LUT.evalLUT table input ∷ [])
  (Expression.lut table (inputExpressions arity) ∷ [])
  (λ input → cong (λ arguments → LUT.evalLUT table arguments ∷ [])
    (input-expressions-evaluate arity input))

bufgceHandler : CertifiedHandler 2 1
bufgceHandler = certifiedHandler
  (λ { (input ∷ enable ∷ []) → Clock.bufgce input enable ∷ [] })
  (Expression.select
    (Expression.input (fsuc fzero))
    (Expression.constant low)
    (Expression.input fzero) ∷ [])
  (λ { (input ∷ enable ∷ []) → refl })

obufdsDenotation : Vec Bit 1 → Vec Bit 2
obufdsDenotation (input ∷ []) with IO.obufds input
... | IO.differentialOutput positive negative = positive ∷ negative ∷ []

obufdsHandler : CertifiedHandler 1 2
obufdsHandler = certifiedHandler obufdsDenotation
  (Expression.input fzero
   ∷ Expression.invert (Expression.input fzero) ∷ [])
  (λ { (false ∷ []) → refl ; (true ∷ []) → refl })

flattenCarry : Carry4.Carry4Output → Vec Bit 8
flattenCarry output = Carry4.oPort output ++ Carry4.coPort output

carryDenotation : Vec Bit 9 → Vec Bit 8
carryDenotation
  (carry ∷ di0 ∷ di1 ∷ di2 ∷ di3
   ∷ s0 ∷ s1 ∷ s2 ∷ s3 ∷ []) =
  flattenCarry
    (Carry4.evalCarryChain carry
      (di0 ∷ di1 ∷ di2 ∷ di3 ∷ [])
      (s0 ∷ s1 ∷ s2 ∷ s3 ∷ []))

carry4Handler : CertifiedHandler 9 8
carry4Handler = certifiedHandler carryDenotation
  (o0 ∷ o1 ∷ o2 ∷ o3 ∷ c1 ∷ c2 ∷ c3 ∷ c4 ∷ [])
  (λ { (carry ∷ di0 ∷ di1 ∷ di2 ∷ di3
            ∷ s0-bit ∷ s1-bit ∷ s2-bit ∷ s3-bit ∷ []) → refl })
  where
  c0 = Expression.input fzero
  di0 = Expression.input (fsuc fzero)
  di1 = Expression.input (fsuc (fsuc fzero))
  di2 = Expression.input (fsuc (fsuc (fsuc fzero)))
  di3 = Expression.input (fsuc (fsuc (fsuc (fsuc fzero))))
  s0 = Expression.input (fsuc (fsuc (fsuc (fsuc (fsuc fzero)))))
  s1 = Expression.input (fsuc (fsuc (fsuc (fsuc (fsuc (fsuc fzero))))))
  s2 = Expression.input (fsuc (fsuc (fsuc (fsuc (fsuc (fsuc (fsuc fzero)))))))
  s3 = Expression.input (fsuc (fsuc (fsuc (fsuc (fsuc (fsuc (fsuc (fsuc fzero))))))))
  c1 = Expression.select s0 di0 c0
  c2 = Expression.select s1 di1 c1
  c3 = Expression.select s2 di2 c2
  c4 = Expression.select s3 di3 c3
  o0 = s0 Expression.xorE c0
  o1 = s1 Expression.xorE c1
  o2 = s2 Expression.xorE c2
  o3 = s3 Expression.xorE c3

fdreHandler : Bit → CertifiedStateHandler 3 1 1
fdreHandler initial = certifiedStateHandler
  (initial ∷ [])
  (λ { input (q ∷ []) → q ∷ [] })
  (λ { (data-in ∷ enable ∷ reset ∷ []) (q ∷ []) →
    FDRE.fdreStep data-in enable reset q ∷ [] })
  (Expression.register fzero ∷ [])
  (FDRE.fdreNext
    (Expression.input fzero)
    (Expression.input (fsuc fzero))
    (Expression.input (fsuc (fsuc fzero)))
    (Expression.register fzero) ∷ [])
  (λ { input (q ∷ []) → refl })
  (λ { (data-in ∷ enable ∷ reset ∷ []) (q ∷ []) → refl })

fdseHandler : Bit → CertifiedStateHandler 3 1 1
fdseHandler initial = certifiedStateHandler
  (initial ∷ [])
  (λ { input (q ∷ []) → q ∷ [] })
  (λ { (data-in ∷ enable ∷ set ∷ []) (q ∷ []) →
    FDSE.fdseStep data-in enable set q ∷ [] })
  (Expression.register fzero ∷ [])
  (FDSE.fdseNext
    (Expression.input fzero)
    (Expression.input (fsuc fzero))
    (Expression.input (fsuc (fsuc fzero)))
    (Expression.register fzero) ∷ [])
  (λ { input (q ∷ []) → refl })
  (λ { (data-in ∷ enable ∷ set ∷ []) (q ∷ []) → refl })

-- Extensibility probe: this test-only handler is locally certified and does
-- not require a case in any whole-design soundness proof.
inverterHandler : CertifiedHandler 1 1
inverterHandler = certifiedHandler
  (λ { (input ∷ []) → not input ∷ [] })
  (Expression.invert (Expression.input fzero) ∷ [])
  (λ { (false ∷ []) → refl ; (true ∷ []) → refl })