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

open import NeilPrelude
open import Bool
open import Nat
open import CoreFull
open import Maybe


module PrimitivesFull where


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

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

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

        mkStatelessInit : {as bs : SVDesc0} → InitSV as → (SVRepR (svd0toR as) → SVRepR (svd0toR bs)) → SF as bs cau
        mkStatelessInit p f = sfprim (initialised p (prim (λ _ _ as → unit , f as)) unit)

        mkStatelessUninit : {as bs : SVDesc0} → NotInitSV bs → (SVRepR (svd0toR as) → SVRepR (svd0toR bs)) → SF as bs cau
        mkStatelessUninit p f = sfprim (uninitialised p (prim (λ _ _ as → unit , f as)) (const unit))

        mkDuni : {as bs : SVDesc0} → {State : Set} → NotInitSV bs → (Δt → State → (SVRepR (svd0toR as) → State) × SVRepR (svd0toR bs)) → (SVRep0 as → State) → SF as bs dec
        mkDuni p f = sfprim ∘ uninitialised p (dprim f)

        mkDini : {as bs : SVDesc0} → {State : Set} → InitSV as → (Δt → State → (SVRepR (svd0toR as) → State) × SVRepR (svd0toR bs)) → State → SF as bs dec
        mkDini p f = sfprim ∘ initialised p (dprim f) 

        mkUni : {as bs : SVDesc0} → {State : Set} → NotInitSV bs → (Δt → State → SVRepR (svd0toR as) → State × SVRepR (svd0toR bs)) → (SVRep0 as → State) → SF as bs cau
        mkUni p f = sfprim ∘ uninitialised p (prim f)

        mkIni : {as bs : SVDesc0} → {State : Set} → InitSV as → (Δt → State → SVRepR (svd0toR as) → State × SVRepR (svd0toR bs)) → State → SF as bs cau
        mkIni p f = sfprim ∘ initialised p (prim f)

        mkSource : {as bs : SVDesc0} → {State : Set} → (Δt → State → State × SVRepR (svd0toR bs)) → State → SF as bs dec
        mkSource f = sfprim ∘ source f 

        mkRouter : {as bs : SVDesc0} → (SVRep0 as → SVRep0 bs) → (SVRepR (svd0toR as) → SVRepR (svd0toR bs)) → SF as bs cau
        mkRouter f g = sfprim (router f g)


-- 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 = mkStatelessInit ⟨T⟩ ∘ mapE

pure : {i : Init} → {A B : Set} → (A → B) → SF [ C i A ] [ C i B ] cau
pure {false} = mkStatelessInit ⟨T⟩ ∘ mapC
pure {true}  = mkStatelessUninit ⟨T⟩ ∘ mapC

pure2 : {i₁ i₂ : Init} → {A B D : Set} → (A → B → D) → SF (C i₁ A ∷ C i₂ B ∷ []) [ C (i₁ ∨ i₂) D ] cau
pure2 {true}          = mkStatelessUninit ⟨T⟩ ∘ mapC2
pure2 {false} {true}  = mkStatelessUninit ⟨T⟩ ∘ mapC2
pure2 {false} {false} = mkStatelessInit ⟨TT⟩ ∘ mapC2

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

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

sample : {i : Init} → {A B : Set} → SF (E B ∷ C i A ∷ []) [ E A ] cau
sample {false} = mkStatelessInit ⟨TT⟩ sampleAux
sample {true}  = mkStatelessUninit ⟨T⟩ sampleAux


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

never : {as : SVDesc0} → {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 → SVRepR [ C Bool ] → Bool × SVRepR [ E Unit ]
        edgeAux s (b ∷ ⟨⟩) = b , hvwrap (if b ∧ not s then just unit else nothing)

edge : SF [ C ini Bool ] [ E Unit ] cau
edge = mkIni ⟨T⟩ (const edgeAux) true

iEdge : SF [ C ini Bool ] [ E Unit ] cau
iEdge = mkIni ⟨T⟩ (const edgeAux) false


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


pre : {A : Set} → SF [ C ini A ] [ C uni A ] dec
pre = mkDuni ⟨T⟩ (λ _ s → id , s) (sv0toR ⟨T⟩)

iPre : {A : Set} → A → SF [ C ini A ] [ C ini A ] dec
iPre = mkDini ⟨T⟩ (λ _ s → id , s) ∘ hvwrap

identity : {as : SVDesc0} → SF as as cau
identity = mkRouter id id


open import ListProps using (map++)

sfFork : {as : SVDesc0} → SF as (as ++ as) cau
sfFork {AS} = mkRouter (λ as → as +++ as) (λ as → substhv (sym (map++ AS)) (as +++ as))

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

sfNil : SF [] [] dec
sfNil = sfSink


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

integral : SF [ C ini ℕ ] [ C ini ℕ ] cau
integral = mkIni ⟨T⟩ (λ t s → second hvwrap ∘ fork ∘ _+_ s ∘ _*_ t ∘ hvunwrap) 

-- dintegral stores the running total and the old input

dintegral : SF [ C ini ℕ ] [ C ini ℕ ] dec
dintegral = mkDini ⟨T⟩ dintegralAux ( , )
            where
                  dintegralAux : Δt → ℕ × ℕ → (SVRepR [ C ℕ ] → ℕ × ℕ) × SVRepR [ 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 ini A ] [ C ini A ] dec
delay {A} tdelay a = mkDini ⟨T⟩ 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 → (SVRepR [ C A ] → DelayState) × SVRepR [ 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 = mkDini ⟨T⟩ delayEAux (t0 , emptyQueue)
  where
     -- DelayState = CurrentTime × Queue (ReleaseTime × Value)
        DelayState = Time × Queue (Time × A)

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

        deQueueE : Time → Queue (Time × A) → Queue (Time × A) × SVRepR [ 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 → (SVRepR [ E A ] → DelayState) × SVRepR [ E A ]
        delayEAux dt (told , q) =  first (λ q' ea → tnow , enQueueE tnow ea q') (deQueueE tnow q)
          where
                tnow    = dt + told