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

module Spartan6.Hierarchy.ResourceFlattening where

open import Spartan6.Prelude
open import Spartan6.Hierarchy.Interface
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.Semantics.Machine as Machine

record ResourceBoundary
  (Input Output : Interface)
  (ResourceInput ResourceObservation : Type₀) : Type₀ where
  constructor resourceBoundary
  field
    decodeBoundaryInput : Environment Input -> ResourceInput
    encodeBoundaryObservation :
      ResourceObservation -> Environment Output

open ResourceBoundary public

record ResourceInitialization
  {Initial Input Observation Domain State : Type₀}
  (resource : StateResource Initial Input Observation Domain State)
  : Type₀ where
  constructor resourceInitialization
  field
    initialParameters : Initial
    semanticInitial : State
    initializationAccepted :
      decodeInitial resource initialParameters ≡ just semanticInitial

open ResourceInitialization public

resourceComponent :
  ∀ {Input Output ResourceInput ResourceObservation
    Initial Domain State}
  -> (identity : Provenance.ComponentIdentity)
  -> (origin : Provenance.SourceOrigin)
  -> (resource : StateResource
      Initial ResourceInput ResourceObservation Domain State)
  -> ResourceBoundary
      Input Output ResourceInput ResourceObservation
  -> ResourceInitialization resource
  -> Component.Component Input Output (EdgeSet Domain) State
resourceComponent identity origin resource boundary initialization =
  Component.leafWithIdentity identity origin
    (Machine.machine
      (semanticInitial initialization)
      (λ input state ->
        encodeBoundaryObservation boundary
          (observeResource resource
            (decodeBoundaryInput boundary input) state))
      (λ edges input state ->
        stepResource resource edges
          (decodeBoundaryInput boundary input) state))

resourceFlatMachine :
  ∀ {Input Output ResourceInput ResourceObservation
    Initial Domain State width}
  -> (identity : Provenance.ComponentIdentity)
  -> (origin : Provenance.SourceOrigin)
  -> (resource : StateResource
      Initial ResourceInput ResourceObservation Domain State)
  -> (boundary : ResourceBoundary
      Input Output ResourceInput ResourceObservation)
  -> (initialization : ResourceInitialization resource)
  -> CertifiedBitLowering resource width
  -> Flat.FlatMachine Input Output (EdgeSet Domain)
resourceFlatMachine identity origin resource boundary initialization lowering =
  Flat.flatMachine identity
    (Provenance.leafProvenance origin) _
    (Machine.machine
      (encodeState lowering (semanticInitial initialization))
      (λ input state ->
        encodeBoundaryObservation boundary
          (observeBits lowering
            (decodeBoundaryInput boundary input) state))
      (λ edges input state ->
        stepBits lowering edges
          (decodeBoundaryInput boundary input) state))

resourceFlattens :
  ∀ {Input Output ResourceInput ResourceObservation
    Initial Domain State width}
  (identity : Provenance.ComponentIdentity)
  (origin : Provenance.SourceOrigin)
  (resource : StateResource
    Initial ResourceInput ResourceObservation Domain State)
  (boundary : ResourceBoundary
    Input Output ResourceInput ResourceObservation)
  (initialization : ResourceInitialization resource)
  (lowering : CertifiedBitLowering resource width)
  -> Flat.CertifiedMachineFlattening
      (resourceComponent identity origin resource boundary initialization)
Flat.flatTarget
  (resourceFlattens identity origin resource boundary initialization lowering) =
  resourceFlatMachine identity origin resource boundary initialization lowering
Flat.StateRelation
  (resourceFlattens identity origin resource boundary initialization lowering)
  semantic-state flat-state =
  encodeState lowering semantic-state ≡ flat-state
Flat.initialRelated
  (resourceFlattens identity origin resource boundary initialization lowering) =
  refl
Flat.observationPreserved
  (resourceFlattens identity origin resource boundary initialization lowering)
  input semantic-state flat-state related =
  cong (encodeBoundaryObservation boundary)
    (sym
      (observe-preserved lowering
        (decodeBoundaryInput boundary input) semantic-state))
  ∙ cong
      (λ state ->
        encodeBoundaryObservation boundary
          (observeBits lowering
            (decodeBoundaryInput boundary input) state))
      related
Flat.transitionPreserved
  (resourceFlattens identity origin resource boundary initialization lowering)
  edges input semantic-state flat-state related =
  sym
    (step-lowering-preserved lowering edges
      (decodeBoundaryInput boundary input) semantic-state)
  ∙ cong
      (stepBits lowering edges (decodeBoundaryInput boundary input))
      related
Flat.provenanceRetained
  (resourceFlattens identity origin resource boundary initialization lowering) =
  refl