open import NeilPrelude1
open import Core1

module Primitives1 where

private

svwrap : {a : SigDesc}  SigRep a  SVRep [ a ]
svwrap a = a  ⟨⟩

svunwrap : {a : SigDesc}  SVRep [ a ]  SigRep a
svunwrap (a  ⟨⟩) = a

svunwrap2 : {a b : SigDesc}  SVRep ( a  b  [] )  SigRep a × SigRep b
svunwrap2 (a  b  ⟨⟩) = a & b

mapE : {A B : Set}  (A  B)  SVRep [ E A ]  SVRep [ E B ]
mapE f e = svwrap (maybeMap f (svunwrap e))

mapC : {A B : Set}  (A  B)  SVRep [ C A ]  SVRep [ C B ]
mapC f a = svwrap (f (svunwrap a))

mapC2 : {A B D : Set}  (A  B  D)  SVRep (C A  C B  [])  SVRep [ C D ]
mapC2 f (a  b  ⟨⟩) = svwrap (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 ×1 SVRep bs)  State  SF as bs dec
mkSource {as} {bs} {State} f = dprim aux
where aux : Time  State  (SVRep as  State) 1×1 SVRep bs
aux t s with f t s
... | s' & bs =  _  s') & bs

-- 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 f = mkStateless (mapE f)

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

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

mergeWith : {A : Set}  (A  A  A)  SF (E A  E A  []) [ E A ] cau
mergeWith f = mkStateless  g  svwrap (uncurry (maybeMergeWith f) (svunwrap2 g)))

private sampleAux : {A B : Set}  SVRep (E B  C A  [])  SVRep [ E A ]
sampleAux (me  a  ⟨⟩) = svwrap (maybeMap  _  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 & svwrap a) unit

never : {as : SVDesc}  {A : Set}  SF as [ E A ] dec
never = mkSource  _ _  unit & svwrap 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 ×1 SVRep [ E Unit ]
edgeAux s (b  ⟨⟩) = b & svwrap (if b  not s then just unit else nothing)

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

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

holdWith : {A B : Set}  (A  B  B)  B  SF [ E A ] [ C B ] cau
holdWith {A} {B} f = prim  _  holdAux)
where
holdAux : B  SVRep [ E A ]  B ×1 SVRep [ C B ]
holdAux s (nothing  ⟨⟩) = s & svwrap s
holdAux s (just a   ⟨⟩) = let b = f a s in b & svwrap b

iPre : {A : Set}  A  SF [ C A ] [ C A ] dec
iPre a = dprim  _ s  svunwrap & svwrap s) a

identity : {as : SVDesc}  SF as as cau
identity = mkStateless  a  a)

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  (t + s) & svwrap (t + s)) t0

integral : SF [ C  ] [ C  ] cau
integral = prim  t s a  (svunwrap a * t + s) & svwrap (svunwrap a * t + s)) 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  ]   × ) 1×1 SVRep [ C  ]
dintegralAux dt (tot & oldx) = let newtot :
newtot = tot + dt * oldx
in  cx  newtot & svunwrap cx) & svwrap newtot