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

open import NeilPrelude
open import Nat
open import Bool

module Core where

open import Descriptors public
open import HetroVector public
open import BoolOrd using (_≤_)


-- Signal Representation --

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

SVRep : SVDesc → Set
SVRep = HetVec SigRep


-- 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 = 

-- Signal Function Representation --

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


data SF : SVDesc → SVDesc → Dec → Set where
  prim    : {as bs : SVDesc} → {State : Set} → (Δt → State → SVRep as → State × SVRep bs) → State   → SF as bs cau
  dprim   : {as bs : SVDesc} → {State : Set} → (Δt → State → (SVRep as → State) × 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'



-- Utility Functions --

svsplit : {as bs : SVDesc} → SVRep (as ++ bs) → SVRep as × SVRep bs
svsplit = hvsplit

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