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

module Spartan6.Hierarchy.Interface where

open import Spartan6.Prelude

record StablePort : Type₀ where
  constructor stablePort
  field
    stablePortId : ℕ
    stablePortName : String
    stablePortWidth : ℕ

open StablePort public

infixr  _∥ᵢ_

data Interface : Type₀ where
  emptyInterface : Interface
  signalInterface : StablePort -> Interface
  _∥ᵢ_ : Interface -> Interface -> Interface

interfaceWidth : Interface -> ℕ
interfaceWidth emptyInterface = 
interfaceWidth (signalInterface port) = stablePortWidth port
interfaceWidth (left ∥ᵢ right) = interfaceWidth left + interfaceWidth right

-- The interpretation retains port grouping until the backend boundary.

Environment : Interface -> Type₀
Environment emptyInterface = Unit
Environment (signalInterface port) = Vec Bit (stablePortWidth port)
Environment (left ∥ᵢ right) = Environment left × Environment right

infixr  _∥ᵉ_

_∥ᵉ_ : ∀ {left right}
  -> Environment left -> Environment right
  -> Environment (left ∥ᵢ right)
_∥ᵉ_ = _,_

leftEnvironment : ∀ {left right}
  -> Environment (left ∥ᵢ right) -> Environment left
leftEnvironment = fst

rightEnvironment : ∀ {left right}
  -> Environment (left ∥ᵢ right) -> Environment right
rightEnvironment = snd

appendVec : ∀ {ℓ} {A : Type ℓ} {leftCount rightCount}
  -> Vec A leftCount -> Vec A rightCount
  -> Vec A (leftCount + rightCount)
appendVec [] right = right
appendVec (item ∷ left) right = item ∷ appendVec left right

splitVec : ∀ {ℓ} {A : Type ℓ} (leftCount rightCount : ℕ)
  -> Vec A (leftCount + rightCount)
  -> Vec A leftCount × Vec A rightCount
splitVec zero rightCount values = [] , values
splitVec (suc leftCount) rightCount (item ∷ values) =
  item ∷ fst pieces , snd pieces
  where
  pieces : Vec _ leftCount × Vec _ rightCount
  pieces = splitVec leftCount rightCount values

splitVec-append : ∀ {ℓ} {A : Type ℓ} {leftCount rightCount}
  (left : Vec A leftCount) (right : Vec A rightCount)
  -> splitVec leftCount rightCount (appendVec left right)
    ≡ (left , right)
splitVec-append [] right = refl
splitVec-append (item ∷ left) right =
  cong
    (λ pieces -> item ∷ fst pieces , snd pieces)
    (splitVec-append left right)

appendVec-split : ∀ {ℓ} {A : Type ℓ}
  (leftCount rightCount : ℕ)
  (values : Vec A (leftCount + rightCount))
  -> appendVec
      (fst (splitVec leftCount rightCount values))
      (snd (splitVec leftCount rightCount values))
    ≡ values
appendVec-split zero rightCount values = refl
appendVec-split (suc leftCount) rightCount (item ∷ values) =
  cong (item ∷_) (appendVec-split leftCount rightCount values)

flattenEnvironment : ∀ {interface}
  -> Environment interface -> Vec Bit (interfaceWidth interface)
flattenEnvironment {emptyInterface} environment = []
flattenEnvironment {signalInterface port} values = values
flattenEnvironment {left ∥ᵢ right} (left-values , right-values) =
  appendVec
    (flattenEnvironment {left} left-values)
    (flattenEnvironment {right} right-values)

unflattenEnvironment : ∀ {interface}
  -> Vec Bit (interfaceWidth interface) -> Environment interface
unflattenEnvironment {emptyInterface} values = tt
unflattenEnvironment {signalInterface port} values = values
unflattenEnvironment {left ∥ᵢ right} values =
  unflattenEnvironment {left} (fst pieces)
  , unflattenEnvironment {right} (snd pieces)
  where
  pieces : Vec Bit (interfaceWidth left) × Vec Bit (interfaceWidth right)
  pieces = splitVec (interfaceWidth left) (interfaceWidth right) values

flatten-unflatten : ∀ {interface}
  (values : Vec Bit (interfaceWidth interface))
  -> flattenEnvironment (unflattenEnvironment {interface} values) ≡ values
flatten-unflatten {emptyInterface} [] = refl
flatten-unflatten {signalInterface port} values = refl
flatten-unflatten {left ∥ᵢ right} values =
  cong₂ appendVec
    (flatten-unflatten {left}
      (fst (splitVec (interfaceWidth left) (interfaceWidth right) values)))
    (flatten-unflatten {right}
      (snd (splitVec (interfaceWidth left) (interfaceWidth right) values)))
  ∙ appendVec-split (interfaceWidth left) (interfaceWidth right) values

unflatten-append : ∀ {left right}
  (left-values : Vec Bit (interfaceWidth left))
  (right-values : Vec Bit (interfaceWidth right))
  -> unflattenEnvironment {left ∥ᵢ right}
      (appendVec left-values right-values)
    ≡ (unflattenEnvironment {left} left-values
      , unflattenEnvironment {right} right-values)
unflatten-append {left} {right} left-values right-values =
  cong
    (λ pieces ->
      (unflattenEnvironment {left} (fst pieces)
      , unflattenEnvironment {right} (snd pieces)))
    (splitVec-append left-values right-values)

unflatten-flatten : ∀ {interface}
  (environment : Environment interface)
  -> unflattenEnvironment (flattenEnvironment environment) ≡ environment
unflatten-flatten {emptyInterface} tt = refl
unflatten-flatten {signalInterface port} values = refl
unflatten-flatten {left ∥ᵢ right} (left-values , right-values) =
  unflatten-append
    (flattenEnvironment left-values)
    (flattenEnvironment right-values)
  ∙ cong₂ _,_
      (unflatten-flatten left-values)
      (unflatten-flatten right-values)

environment-from-flat : ∀ {interface}
  {left right : Environment interface}
  -> flattenEnvironment left ≡ flattenEnvironment right
  -> left ≡ right
environment-from-flat {left = left} {right = right} equality =
  sym (unflatten-flatten left)
  ∙ cong unflattenEnvironment equality
  ∙ unflatten-flatten right

-- Renamings are extensional typed wirings.  Their source and target
-- interfaces remain visible even when a client deliberately hides, reorders,
-- or duplicates a signal.

record Renaming (source target : Interface) : Type₀ where
  constructor mkRenaming
  field applyRenaming : Environment source -> Environment target

open Renaming public

identityRenaming : (interface : Interface) -> Renaming interface interface
identityRenaming interface = mkRenaming (λ environment -> environment)

composeRenaming : ∀ {source middle target}
  -> Renaming source middle -> Renaming middle target
  -> Renaming source target
composeRenaming first second =
  mkRenaming
    (λ environment -> applyRenaming second (applyRenaming first environment))

parallelRenaming : ∀ {left-source right-source left-target right-target}
  -> Renaming left-source left-target
  -> Renaming right-source right-target
  -> Renaming
      (left-source ∥ᵢ right-source)
      (left-target ∥ᵢ right-target)
parallelRenaming left-map right-map =
  mkRenaming
    (λ environment ->
      applyRenaming left-map (fst environment)
      , applyRenaming right-map (snd environment))

leftProjection : ∀ {left right}
  -> Renaming (left ∥ᵢ right) left
leftProjection = mkRenaming fst

rightProjection : ∀ {left right}
  -> Renaming (left ∥ᵢ right) right
rightProjection = mkRenaming snd

swapParallel : ∀ {left right}
  -> Renaming (left ∥ᵢ right) (right ∥ᵢ left)
swapParallel =
  mkRenaming (λ environment -> snd environment , fst environment)

renaming-identity : ∀ {interface} (environment : Environment interface)
  -> applyRenaming (identityRenaming interface) environment ≡ environment
renaming-identity environment = refl

renaming-compose : ∀ {source middle target}
  (first : Renaming source middle)
  (second : Renaming middle target)
  (environment : Environment source)
  -> applyRenaming (composeRenaming first second) environment
    ≡ applyRenaming second (applyRenaming first environment)
renaming-compose first second environment = refl