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

open import NeilPrelude
open import Primitives
open import Core
open import BoolProps

module Library 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 sf = switch sf ∘ const

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 sf = dswitch sf ∘ const


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

open import NatOrd using (_<=ℕ_)
import Ord
open Ord _<=ℕ_

after : {as : SVDesc} → Time → SF as [ E Unit ] dec
after t = time >>> edgeWhen (_<=_ t)

afterTag : {as : SVDesc} → {A : Set} → Time → A → SF as [ E A ] dec
afterTag t a = after t >>> tag a

afterEach : {as : SVDesc} → List Time → SF as [ E Unit ] dec
afterEach [] = never
afterEach (t ∷ ts) = bdswitch (after t >>> sfFork) (afterEach ts)

afterEachTag : {as : SVDesc} → {A : Set} → List (Time × A) → SF as [ E A ] dec
afterEachTag [] = never
afterEachTag ((t , a) ∷ tas) = bdswitch (afterTag t a >>> sfFork) (afterEachTag tas)


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

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


-- and first and second can be defined:

sfFirst : {as bs cs : SVDesc} → {d : Dec} → SF as bs d → SF (as ++ cs) (bs ++ cs) cau
sfFirst {_} {_} {_} {d} sf = substSFd (∨true d) (sf *** identity)

sfSecond : {as bs cs : SVDesc} → {d : Dec} → SF bs cs d → SF (as ++ bs) (as ++ cs) cau
sfSecond {as} sf = identity {as} *** sf