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

module Spartan6.Netlist.Expression where

open import Spartan6.Prelude
open import Spartan6.Primitive.LUT using (TruthTable; evalLUT)

infixr  _andE_
infixr  _xorE_
infixr  _orE_

-- Expression trees are the first admitted combinational representation.
-- Their finite indices make dangling input and register references
-- unrepresentable.  Cyclic combinational raw netlists are rejected before
-- translation to this type.

data Expr (inputs registers : ℕ) : Type₀ where
  input    : Fin inputs → Expr inputs registers
  register : Fin registers → Expr inputs registers
  constant : Bit → Expr inputs registers
  invert   : Expr inputs registers → Expr inputs registers
  _andE_   : Expr inputs registers → Expr inputs registers → Expr inputs registers
  _orE_    : Expr inputs registers → Expr inputs registers → Expr inputs registers
  _xorE_   : Expr inputs registers → Expr inputs registers → Expr inputs registers
  select   : Expr inputs registers → Expr inputs registers → Expr inputs registers
           → Expr inputs registers
  lut      : ∀ {arity} → TruthTable arity → Vec (Expr inputs registers) arity
           → Expr inputs registers

mutual
  eval : ∀ {inputs registers}
       → Vec Bit inputs
       → Vec Bit registers
       → Expr inputs registers
       → Bit
  eval external state (input i) = lookup i external
  eval external state (register i) = lookup i state
  eval external state (constant bit) = bit
  eval external state (invert expression) = not (eval external state expression)
  eval external state (left andE right) =
    eval external state left and eval external state right
  eval external state (left orE right) =
    eval external state left or eval external state right
  eval external state (left xorE right) =
    eval external state left ⊕ eval external state right
  eval external state (select selector when-false when-true) =
    mux (eval external state selector)
        (eval external state when-false)
        (eval external state when-true)
  eval external state (lut table arguments) =
    evalLUT table (evalAll external state arguments)

  evalAll : ∀ {inputs registers arity}
          → Vec Bit inputs
          → Vec Bit registers
          → Vec (Expr inputs registers) arity
          → Vec Bit arity
  evalAll external state [] = []
  evalAll external state (expression ∷ expressions) =
    eval external state expression ∷ evalAll external state expressions

evalConstant : ∀ {inputs registers} external state bit
             → eval {inputs} {registers} external state (constant bit) ≡ bit
evalConstant external state bit = refl

evalSelect-low : ∀ {inputs registers} external state when-false when-true
               → eval {inputs} {registers} external state
                   (select (constant low) when-false when-true)
               ≡ eval external state when-false
evalSelect-low external state when-false when-true = refl

evalSelect-high : ∀ {inputs registers} external state when-false when-true
                → eval {inputs} {registers} external state
                    (select (constant high) when-false when-true)
                ≡ eval external state when-true
evalSelect-high external state when-false when-true = refl