open import NeilPrelude1
open import Primitives1
open import Core1

module Library1 where

-- If maximum optimisation is desired, many of these signal functions could be defined differently
-- for example, now should be defined using a switch so that it switches into never 

now : {as : SVDesc} → SF as [ E Unit ] dec
now = constant true >>> iEdge

_&&&_ : {as bs cs : SVDesc} → {d₁ d₂ : Dec} → SF as bs d₁ → SF as cs d₂ → SF as (bs ++ cs) (d₁ ∨ d₂)
sf1 &&& sf2 = sfFork >>> sf1 *** sf2

-- basic switches don't use the event value

bswitch : {d₁ d₂ : Dec} → {as bs : SVDesc} → {e : Set} → SF as (E e ∷ bs) d₁ → SF as bs d₂ → SF as bs (d₁ ∨ d₂)
bswitch sfs sfr = switch sfs (λ _ → sfr) 

bdswitch : {d₁ d₂ : Dec} → {as bs : SVDesc} → {e : Set} → SF as (E e ∷ bs) d₁ → SF as bs d₂ → SF as bs (d₁ ∨ d₂)
bdswitch sfs sfr = dswitch sfs (λ _ → sfr) 


notYet : {A : Set} → SF [ E A ] [ E A ] cau
notYet = bdswitch (now &&& never) identity

supressInitial : {A : Set} → {as : SVDesc} → SF as [ E A ] cau → SF as [ E A ] cau
supressInitial = bdswitch (now &&& never)

initially : {A : Set} → A → SF [ C A ] [ C A ] cau
initially a = bdswitch (now &&& constant a) identity

initialise : {A : Set} → {as : SVDesc} → A → SF as [ C A ] cau → SF as [ C A ] cau
initialise a = bdswitch (now &&& constant a)


hold : {A : Set} → A → SF [ E A ] [ C A ] cau
hold = holdWith const


mergeL : {A : Set} → SF (E A ∷ E A ∷ []) [ E A ] cau
mergeL = mergeWith const

mergeR : {A : Set} → SF (E A ∷ E A ∷ []) [ E A ] cau
mergeR = mergeWith (flip const)

tag : {A B : Set} → B → SF [ E A ] [ E B ] cau
tag b = pureE (const b)

tagHold : {A B : Set} → B → B → SF [ E A ] [ C B ] cau
tagHold t i = tag t >>> hold i

edgeWhen : {A : Set} → (A → Bool) → SF [ C A ] [ E Unit ] cau
edgeWhen f = pure f >>> edge

iEdgeWhen : {A : Set} → (A → Bool) → SF [ C A ] [ E Unit ] cau
iEdgeWhen f = pure f >>> iEdge

nowTag : {as : SVDesc} → {A : Set} → A → SF as [ E A ] dec
nowTag a = now >>> tag a

sampleHold : {A B : Set} → B → SF (E A ∷ C B ∷ []) [ C B ] cau
sampleHold b = sample >>> hold b

once : {e : Set} → SF [ E e ] [ E e ] cau
once = bdswitch sfFork never


-------------------------------------------------

-- We're still experimenting with the best way to do routing at the
-- reactive level.  For this implementation, you have to use primitive
-- routing combinators (which isn't very neat but does suffice for
-- the moment).  For example, signals can be swapped by:

sfSwap : {a b : SigDesc} → SF (a ∷ b ∷ []) (b ∷ a ∷ []) cau
sfSwap {a} = sfSink {[ a ]} *** identity &&& identity {[ a ]} *** sfSink