{-# OPTIONS --type-in-type
    #-}

open import NeilPrelude
open import Nat
open import Bool

module CoreFull where

open import DescriptorsFull public
open import HetroVector public
open import BoolOrd

-- Signal Representation --

SigRep0 : SigDesc0 → Set
SigRep0 (E A)       = Maybe A
SigRep0 (C false A) = A
SigRep0 (C true  A) = Unit

SigRepR : SigDescR → Set
SigRepR (E A) = Maybe A
SigRepR (C A) = A

SVRep0 : SVDesc0 → Set
SVRep0 = HetVec SigRep0

SVRepR : SVDescR → Set
SVRepR = HetVec SigRepR


-- Time --

-- For the current prototype, we use natural numbers for Time
-- We would use floating point numbers or similar in a real implementation
-- In an ideal world it'd be nice to use reals

Time : Set
Time = ℕ

Δt : Set
Δt = Time

t0 : Time
t0 = 

-- SigRep Function Representation --

infixl  _***_
infixl  _>>>_


-- to exploit routing information, we should represent router better
-- Using Finite sets in De Braun Indices style would work (but have a complicated type siganture)
-- TO DO: Investigate Arow Calculus


data SFStateful (State : Set) (as bs : SVDescR) : Dec → Set where
  prim    : (Δt → State → SVRepR as → State × SVRepR bs)   → SFStateful State as bs cau
  dprim   : (Δt → State → (SVRepR as → State) × SVRepR bs) → SFStateful State as bs dec

data SFPrim (as bs : SVDesc0) : Dec → Set where
  initialised   : {d : Dec} → {State : Set} → InitSV as    → SFStateful State (svd0toR as) (svd0toR bs) d → State                → SFPrim as bs d
  uninitialised : {d : Dec} → {State : Set} → NotInitSV bs → SFStateful State (svd0toR as) (svd0toR bs) d → (SVRep0 as → State) → SFPrim as bs d
  router        : (SVRep0 as → SVRep0 bs) → (SVRepR (svd0toR as) → SVRepR (svd0toR bs))                                      → SFPrim as bs cau
  source        : {State : Set} → (Δt → State → State × SVRepR (svd0toR bs)) → State                                            → SFPrim as bs dec

data SF : SVDesc0 → SVDesc0 → Dec → Set where
  sfprim   : {as bs : SVDesc0} → {d : Dec} → SFPrim as bs d                                                                 → SF as bs d
  _>>>_    : {d₁ d₂ : Dec} → {as bs cs : SVDesc0} → SF as bs d₁ → SF bs cs d₂                                               → SF as cs (d₁ ∧ d₂)
  _***_    : {d₁ d₂ : Dec} → {as bs cs ds : SVDesc0} → SF as cs d₁ → SF bs ds d₂                                            → SF (as ++ bs) (cs ++ ds) (d₁ ∨ d₂)
  loop     : {d : Dec} → {as bs cs ds : SVDesc0} → SF (as ++ cs) (bs ++ ds) d → SF ds cs dec                                → SF as bs d
  switch   : {d₁ d₂ : Dec} → {as bs : SVDesc0} → {e : Set} → SF as (E e ∷ bs) d₁ → (e → SF as (initc bs) d₂)                → SF as bs (d₁ ∨ d₂)
  diswitch : {d₁ d₂ : Dec} → {as bs bs' : SVDesc0} → {e : Set} → initc bs <: bs' → SF as (E e ∷ bs) d₁ → (e → SF as bs' d₂) → SF as bs (d₁ ∨ d₂)
  weaken   : {d d' : Dec} → {as as' bs bs' : SVDesc0} → as' <: as → bs <: bs' → d ≤ d' → SF as bs d                         → SF as' bs' d'


data SFR : SVDescR → SVDescR → Dec → Set where
  sfprim   : {d : Dec} → {as bs : SVDescR} → {State : Set} → SFStateful State as bs d → State                                                  → SFR as bs d
  seq      : {d₁ d₂ : Dec} → {as bs cs : SVDescR} → SFR as bs d₁ → SFR bs cs d₂                                                                → SFR as cs (d₁ ∧ d₂)
  par      : {d₁ d₂ : Dec} → {as bs cs ds : SVDescR} → SFR as cs d₁ → SFR bs ds d₂                                                             → SFR (as ++ bs) (cs ++ ds) (d₁ ∨ d₂)
  loop     : {d : Dec} → {as bs cs ds : SVDescR} → SFR (as ++ cs) (bs ++ ds) d → SFR ds cs dec                                                 → SFR as bs d
  switch   : {d₁ d₂ : Dec} → {as bs : SVDesc0} → {e : Set} → SFR (svd0toR as) (E e ∷ svd0toR bs) d₁ → (e → SF as (initc bs) d₂)                → SFR (svd0toR as) (svd0toR bs) (d₁ ∨ d₂)
  diswitch : {d₁ d₂ : Dec} → {as bs bs' : SVDesc0} → {e : Set} → initc bs <: bs' → SFR (svd0toR as) (E e ∷ svd0toR bs) d₁ → (e → SF as bs' d₂) → SFR (svd0toR as) (svd0toR bs) (d₁ ∨ d₂)
  weaken   : {d d' : Dec} → {as bs : SVDescR} → d ≤ d' → SFR as bs d                                                                           → SFR as bs d'


-- Manipulating SigRep Vector Representations --

private mkEmptySig : {a : SigDesc0} → NotInitSD a → SigRep0 a
        mkEmptySig {C true _} _ = unit
        mkEmptySig {C false _} ()
        mkEmptySig {E _} _ = nothing

mkEmptySV : {as : SVDesc0} → NotInitSV as → SVRep0 as
mkEmptySV = hvmap mkEmptySig


s0toR : {a : SigDesc0} → InitSD a → SigRep0 a → SigRepR (sd0toR a)
s0toR {E _} _ ma      = ma
s0toR {C false _} _ a = a
s0toR {C true _} () _

sv0toR : {as : SVDesc0} → InitSV as → SVRep0 as → SVRepR (svd0toR as)
sv0toR = hvzipWith' s0toR


sinit0toR : (a : SigDesc0) → SigRep0 (initcAux a) → SigRepR (sd0toR a)
sinit0toR (E _) ma      = ma
sinit0toR (C false _) a = a
sinit0toR (C true _) a  = a


svinit0toR : (as : SVDesc0) → SVRep0 (initc as) → SVRepR (svd0toR as)
svinit0toR AS = hvmapB' AS sinit0toR


sRto0 : (a : SigDesc0) → SigRepR (sd0toR a) → SigRep0 a
sRto0 (E _) ma      = ma
sRto0 (C false _) a = a
sRto0 (C true _) _  = unit

svRto0 : {as : SVDesc0} → SVRepR (svd0toR as) → SVRep0 as
svRto0 = hvmapL' sRto0


coerceSig : {a a' : SigDesc0} → a <:' a' → SigRep0 a → SigRep0 a'
coerceSig (subC (inl f<t)) a = unit
coerceSig (subC (inr refl)) a = a
coerceSig subE ma = ma

coerceSV : {as as' : SVDesc0} → as <: as' → SVRep0 as → SVRep0 as'
coerceSV = hv2zipWithhv1 coerceSig

svsplitR : {as bs : SVDescR} → SVRepR (as ++ bs) → SVRepR as × SVRepR bs
svsplitR = hvsplit

svsplit0 : {as bs : SVDesc0} → SVRep0 (as ++ bs) → SVRep0 as × SVRep0 bs
svsplit0 = hvsplit


-- Substitutions --

substSFR : {as as' bs bs' : SVDescR} → {d d' : Dec} → as ≡ as' → bs ≡ bs' → d ≡ d' → SFR as bs d → SFR as' bs' d'
substSFR refl refl refl = id

substSFRio : {as as' bs bs' : SVDescR} → {d : Dec} → as ≡ as' → bs ≡ bs' → SFR as bs d → SFR as' bs' d
substSFRio refl refl = id

substSFRi : {as as' bs : SVDescR} → {d : Dec} → as ≡ as' → SFR as bs d → SFR as' bs d
substSFRi refl = id

substSFRo : {as bs bs' : SVDescR} → {d : Dec} → bs ≡ bs' → SFR as bs d → SFR as bs' d
substSFRo refl = id

substSFRd : {as bs : SVDescR} → {d d' : Dec} → d ≡ d' → SFR as bs d → SFR as bs d'
substSFRd refl = id


substSFd : {as bs : SVDesc0} → {d d' : Dec} → d ≡ d' → SF as bs d → SF as bs d'
substSFd refl = id