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

open import NeilPrelude
open import Core
open import Nat
open import Bool
open import Maybe
open import MaybeMonad using (fmap)


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