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

open import NeilPrelude
open import Core
open import Nat
open import Bool
open import Maybe

module Primitives where

private
mapE : {A B : Set} → (A → B) → SVRep [ E A ] → SVRep [ E B ]
mapE f = hvwrap ∘ fmap f ∘ hvunwrap

mapC : {A B : Set} → (A → B) → SVRep [ C A ] → SVRep [ C B ]
mapC f = hvwrap ∘ f ∘ hvunwrap

mapC2 : {A B D : Set} → (A → B → D) → SVRep (C A ∷ C B ∷ []) → SVRep [ C D ]
mapC2 f (a ∷ b ∷ ⟨⟩) = hvwrap (f a b)

mkStateless : {as bs : SVDesc} → (SVRep as → SVRep bs) → SF as bs cau
mkStateless f = prim (λ _ _ as → unit , f as) unit

mkSource : {as bs : SVDesc} → {State : Set} → (Δt → State → State × SVRep bs) → State → SF as bs dec
mkSource f = dprim (λ t → first const ∘ f t)

-- Exported Primitives --

-- ⟨T⟩ is a proof of a singleton HetroVector containing an element of type True
-- I haven't found a way to automatically infer it

pureE : {A B : Set} → (A → B) → SF [ E A ] [ E B ] cau
pureE = mkStateless ∘ mapE

pure : {A B : Set} → (A → B) → SF [ C A ] [ C B ] cau
pure  = mkStateless ∘ mapC

pure2 : {A B D : Set} → (A → B → D) → SF (C A ∷ C B ∷ []) [ C D ] cau
pure2 = mkStateless ∘ mapC2

mergeWith : {A : Set} → (A → A → A) → SF (E A ∷ E A ∷ []) [ E A ] cau
mergeWith f = mkStateless (hvwrap ∘ uncurry (maybeMergeWith f) ∘ hvunwrap2)

private sampleAux : {A B : Set} → SVRep (E B ∷ C A ∷ []) → SVRep [ E A ]
sampleAux (me ∷ a ∷ ⟨⟩) = hvwrap (fmap (const a) me)

sample : {A B : Set} → SF (E B ∷ C A ∷ []) [ E A ] cau
sample = mkStateless sampleAux

constant : {as : SVDesc} → {A : Set} → A → SF as [ C A ] dec
constant a = mkSource (λ _ _ → unit , hvwrap a) unit

never : {as : SVDesc} → {A : Set} → SF as [ E A ] dec
never = mkSource (λ _ _ → unit , hvwrap nothing) unit

-- edge never produces an event at Time0
-- iEdge will produce an event at Time0, if the initial input is true

private edgeAux : Bool → SVRep [ C Bool ] → Bool × SVRep [ E Unit ]
edgeAux s (b ∷ ⟨⟩) = b , hvwrap (if b ∧ not s then just unit else nothing)

edge : SF [ C Bool ] [ E Unit ] cau
edge = prim (const edgeAux) true

iEdge : SF [ C Bool ] [ E Unit ] cau
iEdge = prim (const edgeAux) false

holdWith : {A B : Set} → (A → B → B) → B → SF [ E A ] [ C B ] cau
holdWith {A} {B} f = prim (const holdAux)
where
holdAux : B → SVRep [ E A ] → B × SVRep [ C B ]
holdAux s (nothing ∷ ⟨⟩) = s , hvwrap s
holdAux s (just a  ∷ ⟨⟩) = let b = f a s in b , hvwrap b

iPre : {A : Set} → A → SF [ C A ] [ C A ] dec
iPre = dprim (λ _ s → id , s) ∘ hvwrap

identity : {as : SVDesc} → SF as as cau
identity = mkStateless id

sfFork : {as : SVDesc} → SF as (as ++ as) cau
sfFork = mkStateless (λ as → as +++ as)

sfSink : {as : SVDesc} → SF as [] dec
sfSink = mkSource (λ _ _ → unit , ⟨⟩) unit

sfNil : SF [] [] dec
sfNil = sfSink

time : {as : SVDesc} → SF as [ C Time ] dec
time = mkSource (λ t s → (second hvwrap ∘ fork) (t + s)) t0

integral : SF [ C ℕ ] [ C ℕ ] cau
integral = prim (λ t s → second hvwrap ∘ fork ∘ _+_ s ∘ _*_ t ∘ hvunwrap) 0

-- dintegral stores the running total and the old input

dintegral : SF [ C ℕ ] [ C ℕ ] dec
dintegral = dprim dintegralAux (0 , 0)
where
dintegralAux : Δt → ℕ × ℕ → (SVRep [ C ℕ ] → ℕ × ℕ) × SVRep [ C ℕ ]
dintegralAux dt (tot , oldx) = let newtot : ℕ
newtot = tot + dt * oldx
in (λ cx → newtot , hvunwrap cx) , hvwrap newtot

open import Queue
open import NatOrd using (_<=ℕ_)
import Ord
open Ord _<=ℕ_

delay : {A : Set} → Time → A → SF [ C A ] [ C A ] dec
delay {A} tdelay a = dprim delayAux (t0 , a , emptyQueue)
where
-- DelayState = CurrentTime × CurrentOutput × Queue (ReleaseTime × Value)
DelayState = Time × A × Queue (Time × A)

deQueueC : Time → Queue (Time × A) → Maybe (A × Queue (Time × A))
deQueueC tnow q with deQueueWhile (λ ta → tnow > fst ta) q
... | q' , tas with reverse tas
...    | []               = nothing
...    | ((_ , anew) ∷ _) = just (anew , q')

enQueueC : Time → A → Queue (Time × A) → Queue (Time × A)
enQueueC tnow a = enQueue (tdelay + tnow , a)

delayAux : Δt → DelayState → (SVRep [ C A ] → DelayState) × SVRep [ C A ]
delayAux dt (told , aold , q) with dt + told
... | tnow with (maybe (aold , q) id ∘ deQueueC tnow) q
... |   aout , q' = (λ ain → tnow , aout , enQueueC tnow ain q') ∘ hvunwrap , hvwrap aout

-- DelayState = CurrentTime × Queue (ReleaseTime × Value)

delayE : {A : Set} → Time → SF [ E A ] [ E A ] dec
delayE {A} tdelay = dprim delayEAux (t0 , emptyQueue)
where
-- DelayState = CurrentTime × Queue (ReleaseTime × Value)
DelayState = Time × Queue (Time × A)

enQueueE : Time → SVRep [ E A ] → Queue (Time × A) → Queue (Time × A)
enQueueE tnow = maybe id (enQueue ∘ _,_ (tdelay + tnow)) ∘ hvunwrap

deQueueE : Time → Queue (Time × A) → Queue (Time × A) × SVRep [ E A ]
deQueueE tnow q with deQueueIf (λ ta → tnow > fst ta) q
... | nothing           = q  , hvwrap nothing
... | just (q' , _ , a) = q' , hvwrap (just a)

delayEAux : Δt → DelayState → (SVRep [ E A ] → DelayState) × SVRep [ E A ]
delayEAux dt (told , q) =  first (λ q' ea → tnow , enQueueE tnow ea q') (deQueueE tnow q)
where
tnow    = dt + told
```