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

-- dintegral stores the running total and the old input

dintegral : SF [ C ℕ ] [ C ℕ ] dec
dintegral = dprim dintegralAux ( & )
            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