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

module Spartan6.Examples.ResourceHierarchy where

open import Spartan6.Prelude
open import Spartan6.Hierarchy.Interface
open import Spartan6.Semantics.StateAdapters
open import Spartan6.Semantics.StateResource

import Spartan6.Hierarchy.Component as Component
import Spartan6.Hierarchy.FlatMachine as Flat
import Spartan6.Hierarchy.Provenance as Provenance
import Spartan6.Hierarchy.ResourceFlattening as Resource
import Spartan6.Primitive.SRL16E as SRL16E

registerInputPort registerOutputPort
  shiftInputPort shiftOutputPort : StablePort
registerInputPort = stablePort  "data-enable-reset" 
registerOutputPort = stablePort  "q" 
shiftInputPort = stablePort  "a3-a2-a1-a0-data-enable" 
shiftOutputPort = stablePort  "q" 

registerInput registerOutput shiftInput shiftOutput : Interface
registerInput = signalInterface registerInputPort
registerOutput = signalInterface registerOutputPort
shiftInput = signalInterface shiftInputPort
shiftOutput = signalInterface shiftOutputPort

registerIdentity shiftIdentity : Provenance.ComponentIdentity
registerIdentity = Provenance.componentIdentity  "fdre-resource"
shiftIdentity = Provenance.componentIdentity  "srl16e-resource"

registerOrigin shiftOrigin : Provenance.SourceOrigin
registerOrigin =
  Provenance.sourceOrigin nothing nothing []ᴸ "constructed.fdre-resource"
shiftOrigin =
  Provenance.sourceOrigin nothing nothing []ᴸ "constructed.srl16e-resource"

registerBoundary : Resource.ResourceBoundary
  registerInput registerOutput FDREInput Bit
registerBoundary = Resource.resourceBoundary
  decode-input (λ observation -> observation ∷ [])
  where
  decode-input : Environment registerInput -> FDREInput
  decode-input (data-bit ∷ enable ∷ reset ∷ []) =
    fdreInput data-bit enable reset

registerInitialization :
  Resource.ResourceInitialization (fdreResource tt)
registerInitialization =
  Resource.resourceInitialization nothing low refl

registerHierarchy : Component.Component
  registerInput registerOutput (EdgeSet Unit) Bit
registerHierarchy =
  Resource.resourceComponent
    registerIdentity registerOrigin (fdreResource tt)
    registerBoundary registerInitialization

registerFlattening : Flat.CertifiedMachineFlattening registerHierarchy
registerFlattening =
  Resource.resourceFlattens
    registerIdentity registerOrigin (fdreResource tt)
    registerBoundary registerInitialization (fdreBitLowering tt)

register-flat-state-is-one-bit :
  Flat.flatStateCount (Flat.flatTarget registerFlattening) ≡ 
register-flat-state-is-one-bit = refl

register-owned-edge-loads :
  Flat.flatStep (Flat.flatTarget registerFlattening)
    allEdges (high ∷ high ∷ low ∷ []) (Flat.flatInitial
      (Flat.flatTarget registerFlattening))
  ≡ high ∷ []
register-owned-edge-loads = refl

register-flattening-preserves-load :
  Flat.StateRelation registerFlattening
    (Component.componentStep registerHierarchy allEdges
      (high ∷ high ∷ low ∷ [])
      (Component.componentInitial registerHierarchy))
    (Flat.flatStep (Flat.flatTarget registerFlattening)
      allEdges (high ∷ high ∷ low ∷ [])
      (Flat.flatInitial (Flat.flatTarget registerFlattening)))
register-flattening-preserves-load =
  Flat.transitionPreserved registerFlattening
    allEdges (high ∷ high ∷ low ∷ []) low (low ∷ []) refl

shiftBoundary : Resource.ResourceBoundary
  shiftInput shiftOutput SRL16EInput Bit
shiftBoundary = Resource.resourceBoundary
  decode-input (λ observation -> observation ∷ [])
  where
  decode-input : Environment shiftInput -> SRL16EInput
  decode-input (a3 ∷ a2 ∷ a1 ∷ a0 ∷ data-bit ∷ enable ∷ []) =
    srl16eInput (SRL16E.addressBits a3 a2 a1 a0) data-bit enable

shiftInitialization :
  Resource.ResourceInitialization (srl16eResource tt)
shiftInitialization =
  Resource.resourceInitialization
    nothing SRL16E.defaultInitialState refl

shiftHierarchy : Component.Component
  shiftInput shiftOutput (EdgeSet Unit) SRL16E.SRL16EState
shiftHierarchy =
  Resource.resourceComponent
    shiftIdentity shiftOrigin (srl16eResource tt)
    shiftBoundary shiftInitialization

shiftFlattening : Flat.CertifiedMachineFlattening shiftHierarchy
shiftFlattening =
  Resource.resourceFlattens
    shiftIdentity shiftOrigin (srl16eResource tt)
    shiftBoundary shiftInitialization (srl16eBitLowering tt)

shift-flat-state-is-sixteen-bits :
  Flat.flatStateCount (Flat.flatTarget shiftFlattening) ≡ 
shift-flat-state-is-sixteen-bits = refl

shift-owned-edge-loads-first-stage :
  Flat.flatStep (Flat.flatTarget shiftFlattening)
    allEdges
    (low ∷ low ∷ low ∷ low ∷ high ∷ high ∷ [])
    (Flat.flatInitial (Flat.flatTarget shiftFlattening))
  ≡ high
    ∷ low ∷ low ∷ low ∷ low
    ∷ low ∷ low ∷ low ∷ low
    ∷ low ∷ low ∷ low ∷ low
    ∷ low ∷ low ∷ low ∷ []
shift-owned-edge-loads-first-stage = refl

shift-flattening-preserves-load :
  Flat.StateRelation shiftFlattening
    (Component.componentStep shiftHierarchy allEdges
      (low ∷ low ∷ low ∷ low ∷ high ∷ high ∷ [])
      (Component.componentInitial shiftHierarchy))
    (Flat.flatStep (Flat.flatTarget shiftFlattening)
      allEdges
      (low ∷ low ∷ low ∷ low ∷ high ∷ high ∷ [])
      (Flat.flatInitial (Flat.flatTarget shiftFlattening)))
shift-flattening-preserves-load =
  Flat.transitionPreserved shiftFlattening
    allEdges
    (low ∷ low ∷ low ∷ low ∷ high ∷ high ∷ [])
    SRL16E.defaultInitialState SRL16E.defaultInitialState refl