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

module Spartan6.Netlist.Context where

open import Spartan6.Prelude

import Spartan6.Netlist.Checked as Checked

-- The three namespaces carried by a checked wire are deliberately distinct.
-- `stateCount` names the existing Checked register namespace semantically; the
-- compatibility representation itself is unchanged.

record Context : Type₀ where
  constructor context
  field
    inputCount : ℕ
    stateCount : ℕ
    localCount : ℕ

open Context public

InputIndex : Context → Type₀
InputIndex Γ = Fin (inputCount Γ)

StateIndex : Context → Type₀
StateIndex Γ = Fin (stateCount Γ)

LocalIndex : Context → Type₀
LocalIndex Γ = Fin (localCount Γ)

Wire : Context → Type₀
Wire Γ = Checked.Wire
  (inputCount Γ) (stateCount Γ) (localCount Γ)

Node : Context → Type₀
Node Γ = Checked.Node
  (inputCount Γ) (stateCount Γ) (localCount Γ)

record Environment (Γ : Context) : Type₀ where
  constructor environment
  field
    inputValues : Vec Bit (inputCount Γ)
    stateValues : Vec Bit (stateCount Γ)
    localValues : Vec Bit (localCount Γ)

open Environment public

emptyLocalContext : ℕ → ℕ → Context
emptyLocalContext inputs states = context inputs states 

extendLocal : Context → Context
extendLocal Γ =
  context (inputCount Γ) (stateCount Γ) (suc (localCount Γ))

sameBoundary : Context → Context → Type₀
sameBoundary source target =
  (inputCount source ≡ inputCount target)
  × (stateCount source ≡ stateCount target)