open import NeilPrelude1
open import Ord1

module Core1 where

-- We need lists of sets

data List1 (S : Set1) : Set1 where
  []      : List1 S
  _∷_     : S → List1 S → List1 S


_++_ : {S : Set1} → List1 S → List1 S → List1 S
[] ++ bs = bs
(a ∷ as) ++ bs = a ∷ (as ++ bs)

[_] : {S : Set1} → S → List1 S
[ s ] = s ∷ []


-- Decoupledness Descriptors -- 

-- Rather than create a datatype for Dec, we use booleans so we can use existing
-- boolean proofs

Dec : Set
Dec = Bool

dec : Dec
dec = false

cau : Dec
cau = true

-- Signal Descriptors --

data SigDesc : Set1 where
  E : Set → SigDesc
  C : Set → SigDesc

SVDesc : Set1
SVDesc = List1 SigDesc

SigRep : SigDesc → Set 
SigRep (C A) = A
SigRep (E A) = Maybe A


data SVRep : List1 SigDesc → Set1 where
  ⟨⟩  : SVRep []
  _∷_ : {a : SigDesc} → {as : SVDesc} → SigRep a → SVRep as → SVRep (a ∷ as)

_+++_ : {as bs : SVDesc} → SVRep as → SVRep bs → SVRep (as ++ bs)
⟨⟩ +++ bs = bs
(a ∷ as) +++ bs = a ∷ (as +++ bs) 

svsplit : {as bs : SVDesc} → SVRep (as ++ bs) → SVRep as 1×1 SVRep bs
svsplit {[]} asbs = ⟨⟩ & asbs
svsplit {_ ∷ AS} (a ∷ asbs) with svsplit {AS} asbs
... | as & bs = (a ∷ as) & bs

---------------------------------------------------------------------------------

Time : Set
Time = ℕ

Δt = Time

t0 = 


-- Signal Function Representation --

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


data SF : SVDesc → SVDesc → Dec → Set1 where
  prim    : {as bs : SVDesc} → {State : Set} → (Δt → State → SVRep as → State ×1 SVRep bs) → State    → SF as bs cau
  dprim   : {as bs : SVDesc} → {State : Set} → (Δt → State → (SVRep as → State) 1×1 SVRep bs) → State → SF as bs dec
  _>>>_   : {d₁ d₂ : Dec} → {as bs cs : SVDesc} → SF as bs d₁ → SF bs cs d₂                           → SF as cs (d₁ ∧ d₂)
  _***_   : {d₁ d₂ : Dec} → {as bs cs ds : SVDesc} → SF as cs d₁ → SF bs ds d₂                        → SF (as ++ bs) (cs ++ ds) (d₁ ∨ d₂)
  loop    : {d : Dec} → {as bs cs ds : SVDesc} → SF (as ++ cs) (bs ++ ds) d → SF ds cs dec            → SF as bs d
  switch  : {d₁ d₂ : Dec} → {as bs : SVDesc} → {e : Set} → SF as (E e ∷ bs) d₁ → (e → SF as bs d₂)    → SF as bs (d₁ ∨ d₂)
  dswitch : {d₁ d₂ : Dec} → {as bs : SVDesc} → {e : Set} → SF as (E e ∷ bs) d₁ → (e → SF as bs d₂)    → SF as bs (d₁ ∨ d₂)
  weaken  : {d d' : Dec} → {as bs : SVDesc} → d ≤ d' → SF as bs d                                     → SF as bs d'