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

module Spartan6.Netlist.Checked where

open import Spartan6.Prelude
open import Spartan6.Primitive.LUT using (TruthTable)
open import Spartan6.Netlist.Expression
open import Spartan6.Semantics.Design

-- A Wire may refer only to external inputs, stored state, constants, or an
-- already constructed combinational node.  The local-node bound is what makes
-- combinational cycles and dangling references unrepresentable here.

data Wire (inputCount registerCount localCount : ℕ) : Type₀ where
  externalWire : Fin inputCount → Wire inputCount registerCount localCount
  storedWire   : Fin registerCount → Wire inputCount registerCount localCount
  localWire    : Fin localCount → Wire inputCount registerCount localCount
  literalWire  : Bit → Wire inputCount registerCount localCount

data Node (inputCount registerCount localCount : ℕ) : Type₀ where
  invertNode : Wire inputCount registerCount localCount
             → Node inputCount registerCount localCount
  andNode    : Wire inputCount registerCount localCount
             → Wire inputCount registerCount localCount
             → Node inputCount registerCount localCount
  orNode     : Wire inputCount registerCount localCount
             → Wire inputCount registerCount localCount
             → Node inputCount registerCount localCount
  xorNode    : Wire inputCount registerCount localCount
             → Wire inputCount registerCount localCount
             → Node inputCount registerCount localCount
  muxNode    : Wire inputCount registerCount localCount
             → Wire inputCount registerCount localCount
             → Wire inputCount registerCount localCount
             → Node inputCount registerCount localCount
  lutNode    : ∀ {arity}
             → TruthTable arity
             → Vec (Wire inputCount registerCount localCount) arity
             → Node inputCount registerCount localCount

infixl  _▻_

data Nodes (inputCount registerCount : ℕ) : ℕ → Type₀ where
  noNodes : Nodes inputCount registerCount 
  _▻_     : ∀ {localCount}
          → Nodes inputCount registerCount localCount
          → Node inputCount registerCount localCount
          → Nodes inputCount registerCount (suc localCount)

compileWire : ∀ {inputCount registerCount localCount}
            → Vec (Expr inputCount registerCount) localCount
            → Wire inputCount registerCount localCount
            → Expr inputCount registerCount
compileWire locals (externalWire index) = input index
compileWire locals (storedWire index) = register index
compileWire locals (localWire index) = lookup index locals
compileWire locals (literalWire bit) = constant bit

compileWires : ∀ {inputCount registerCount localCount arity}
             → Vec (Expr inputCount registerCount) localCount
             → Vec (Wire inputCount registerCount localCount) arity
             → Vec (Expr inputCount registerCount) arity
compileWires locals [] = []
compileWires locals (wire ∷ wires) =
  compileWire locals wire ∷ compileWires locals wires

compileNode : ∀ {inputCount registerCount localCount}
            → Vec (Expr inputCount registerCount) localCount
            → Node inputCount registerCount localCount
            → Expr inputCount registerCount
compileNode locals (invertNode wire) = invert (compileWire locals wire)
compileNode locals (andNode left right) =
  compileWire locals left andE compileWire locals right
compileNode locals (orNode left right) =
  compileWire locals left orE compileWire locals right
compileNode locals (xorNode left right) =
  compileWire locals left xorE compileWire locals right
compileNode locals (muxNode selector when-false when-true) =
  select (compileWire locals selector)
         (compileWire locals when-false)
         (compileWire locals when-true)
compileNode locals (lutNode table arguments) =
  lut table (compileWires locals arguments)

compileNodes : ∀ {inputCount registerCount localCount}
             → Nodes inputCount registerCount localCount
             → Vec (Expr inputCount registerCount) localCount
compileNodes noNodes = []
compileNodes (nodes ▻ node) =
  compileNode compiled node ∷ compiled
  where
  compiled = compileNodes nodes

record CheckedNetlist
  (inputCount outputCount registerCount localCount : ℕ) : Type₀ where
  constructor checkedNetlist
  field
    checkedInitial : Vec Bit registerCount
    checkedNodes   : Nodes inputCount registerCount localCount
    checkedOutputs : Vec (Wire inputCount registerCount localCount) outputCount
    checkedNext    : Vec (Wire inputCount registerCount localCount) registerCount

open CheckedNetlist public

compileNetlist : ∀ {inputCount outputCount registerCount localCount}
               → CheckedNetlist inputCount outputCount registerCount localCount
               → Design inputCount outputCount registerCount
compileNetlist netlist =
  mkDesign
    (checkedInitial netlist)
    (compileWires locals (checkedOutputs netlist))
    (compileWires locals (checkedNext netlist))
  where
  locals = compileNodes (checkedNodes netlist)

compile-preserves-initial :
  ∀ {inputCount outputCount registerCount localCount}
    (netlist : CheckedNetlist inputCount outputCount registerCount localCount)
  → initial (compileNetlist netlist) ≡ checkedInitial netlist
compile-preserves-initial netlist = refl