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

module Spartan6.Netlist.Renaming where

open import Spartan6.Prelude

import Cubical.Data.Empty as Empty
import Spartan6.Netlist.Checked as Checked
open import Spartan6.Netlist.Context

-- Renamings are covariant maps for each independent wire namespace.  Keeping
-- the three maps in one value prevents a local weakening from accidentally
-- changing input or state indices.

record Renaming (source target : Context) : Type₀ where
  constructor mkRenaming
  field
    renameInput : InputIndex source → InputIndex target
    renameState : StateIndex source → StateIndex target
    renameLocal : LocalIndex source → LocalIndex target

open Renaming public

identityRenaming : (Γ : Context) → Renaming Γ Γ
identityRenaming Γ = mkRenaming (λ index → index) (λ index → index)
  (λ index → index)

composeRenaming : ∀ {source middle target}
  → Renaming source middle
  → Renaming middle target
  → Renaming source target
composeRenaming first second =
  mkRenaming
    (λ index → renameInput second (renameInput first index))
    (λ index → renameState second (renameState first index))
    (λ index → renameLocal second (renameLocal first index))

renameWire : ∀ {source target}
  → Renaming source target → Wire source → Wire target
renameWire ρ (Checked.externalWire index) =
  Checked.externalWire (renameInput ρ index)
renameWire ρ (Checked.storedWire index) =
  Checked.storedWire (renameState ρ index)
renameWire ρ (Checked.localWire index) =
  Checked.localWire (renameLocal ρ index)
renameWire ρ (Checked.literalWire bit) = Checked.literalWire bit

renameWires : ∀ {source target count}
  → Renaming source target
  → Vec (Wire source) count
  → Vec (Wire target) count
renameWires ρ [] = []
renameWires ρ (wire ∷ wires) =
  renameWire ρ wire ∷ renameWires ρ wires

renameNode : ∀ {source target}
  → Renaming source target → Node source → Node target
renameNode ρ (Checked.invertNode wire) =
  Checked.invertNode (renameWire ρ wire)
renameNode ρ (Checked.andNode left right) =
  Checked.andNode (renameWire ρ left) (renameWire ρ right)
renameNode ρ (Checked.orNode left right) =
  Checked.orNode (renameWire ρ left) (renameWire ρ right)
renameNode ρ (Checked.xorNode left right) =
  Checked.xorNode (renameWire ρ left) (renameWire ρ right)
renameNode ρ (Checked.muxNode select when-low when-high) =
  Checked.muxNode
    (renameWire ρ select)
    (renameWire ρ when-low)
    (renameWire ρ when-high)
renameNode ρ (Checked.lutNode table arguments) =
  Checked.lutNode table (renameWires ρ arguments)

renameWire-identity : ∀ {Γ} (wire : Wire Γ)
  → renameWire (identityRenaming Γ) wire ≡ wire
renameWire-identity (Checked.externalWire index) = refl
renameWire-identity (Checked.storedWire index) = refl
renameWire-identity (Checked.localWire index) = refl
renameWire-identity (Checked.literalWire bit) = refl

renameWire-compose : ∀ {source middle target}
  (first : Renaming source middle)
  (second : Renaming middle target)
  (wire : Wire source)
  → renameWire (composeRenaming first second) wire
    ≡ renameWire second (renameWire first wire)
renameWire-compose first second (Checked.externalWire index) = refl
renameWire-compose first second (Checked.storedWire index) = refl
renameWire-compose first second (Checked.localWire index) = refl
renameWire-compose first second (Checked.literalWire bit) = refl

renameWires-identity : ∀ {Γ count}
  (wires : Vec (Wire Γ) count)
  → renameWires (identityRenaming Γ) wires ≡ wires
renameWires-identity [] = refl
renameWires-identity (wire ∷ wires) =
  cong₂ _∷_ (renameWire-identity wire) (renameWires-identity wires)

renameWires-compose : ∀ {source middle target count}
  (first : Renaming source middle)
  (second : Renaming middle target)
  (wires : Vec (Wire source) count)
  → renameWires (composeRenaming first second) wires
    ≡ renameWires second (renameWires first wires)
renameWires-compose first second [] = refl
renameWires-compose first second (wire ∷ wires) =
  cong₂ _∷_
    (renameWire-compose first second wire)
    (renameWires-compose first second wires)

renameNode-identity : ∀ {Γ} (node : Node Γ)
  → renameNode (identityRenaming Γ) node ≡ node
renameNode-identity (Checked.invertNode wire) =
  cong Checked.invertNode (renameWire-identity wire)
renameNode-identity (Checked.andNode left right) =
  cong₂ Checked.andNode
    (renameWire-identity left) (renameWire-identity right)
renameNode-identity (Checked.orNode left right) =
  cong₂ Checked.orNode
    (renameWire-identity left) (renameWire-identity right)
renameNode-identity (Checked.xorNode left right) =
  cong₂ Checked.xorNode
    (renameWire-identity left) (renameWire-identity right)
renameNode-identity (Checked.muxNode select when-low when-high) =
  cong₃ Checked.muxNode
    (renameWire-identity select)
    (renameWire-identity when-low)
    (renameWire-identity when-high)
renameNode-identity (Checked.lutNode table arguments) =
  cong (Checked.lutNode table) (renameWires-identity arguments)

renameNode-compose : ∀ {source middle target}
  (first : Renaming source middle)
  (second : Renaming middle target)
  (node : Node source)
  → renameNode (composeRenaming first second) node
    ≡ renameNode second (renameNode first node)
renameNode-compose first second (Checked.invertNode wire) =
  cong Checked.invertNode (renameWire-compose first second wire)
renameNode-compose first second (Checked.andNode left right) =
  cong₂ Checked.andNode
    (renameWire-compose first second left)
    (renameWire-compose first second right)
renameNode-compose first second (Checked.orNode left right) =
  cong₂ Checked.orNode
    (renameWire-compose first second left)
    (renameWire-compose first second right)
renameNode-compose first second (Checked.xorNode left right) =
  cong₂ Checked.xorNode
    (renameWire-compose first second left)
    (renameWire-compose first second right)
renameNode-compose first second
  (Checked.muxNode select when-low when-high) =
  cong₃ Checked.muxNode
    (renameWire-compose first second select)
    (renameWire-compose first second when-low)
    (renameWire-compose first second when-high)
renameNode-compose first second (Checked.lutNode table arguments) =
  cong (Checked.lutNode table)
    (renameWires-compose first second arguments)

-- Checked locals are newest-at-zero, so extending their context inserts a new
-- zero and shifts every earlier local index by one.  Inputs and state remain
-- untouched.

weakenNewestLocal : (Γ : Context)
  → Renaming Γ (extendLocal Γ)
weakenNewestLocal Γ =
  mkRenaming (λ index → index) (λ index → index) fsuc

-- The local component makes this renaming impossible independently of its
-- input and state components.

nonempty-to-empty-local-impossible : ∀ {inputs states}
  → Renaming
      (context inputs states )
      (context inputs states )
  → Empty.⊥
nonempty-to-empty-local-impossible ρ with renameLocal ρ fzero
... | ()