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

open import NeilPrelude
open import PrimitivesFull
open import CoreFull
open import BoolOrd
open import BoolProps

module LibraryFull 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 : SVDesc0}  SF as [ E Unit ] dec
now = constant true >>> iEdge

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


dswitch : {d₁ d₂ : Dec}  {as bs : SVDesc0}  {e : Set}  SF as (E e  bs) d₁  (e  SF as bs d₂)  SF as bs (d₁  d₂)
dswitch sf f = diswitch <:initc sf f


-- basic switches don't use the event value

bswitch : {d₁ d₂ : Dec}  {as bs : SVDesc0}  {e : Set}  SF as (E e  bs) d₁  SF as (initc bs) d₂  SF as bs (d₁  d₂)
bswitch sf = switch sf  const

bdiswitch : {d₁ d₂ : Dec}  {as bs bs' : SVDesc0}  {e : Set}  initc bs <: bs'  SF as (E e  bs) d₁  SF as bs' d₂  SF as bs (d₁  d₂)
bdiswitch p sf = diswitch p sf  const

bdswitch : {d₁ d₂ : Dec}  {as bs : SVDesc0}  {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 : SVDesc0}  SF as [ E A ] cau  SF as [ E A ] cau
supressInitial = bdswitch (now &&& never)

initLem : {i : Init}  {A : Set}  [ C false A ] <: [ C i A ]
initLem = hv2wrap (subC ≤false)

initially : {i : Init}  {A : Set}  A  SF [ C i A ] [ C ini A ] cau
initially a = bdiswitch initLem (now &&& constant a) identity

initialise : {i : Init}  {A : Set}  {as : SVDesc0}  A  SF as [ C i A ] cau  SF as [ C ini A ] cau
initialise a = bdiswitch initLem (now &&& constant a)


hold : {A : Set}  A  SF [ E A ] [ C ini 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 ini B ] cau
tagHold t i = tag t >>> hold i

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

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

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

sampleHold : {i : Init}  {A B : Set}  B  SF (E A  C i B  []) [ C ini 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 : SVDesc0}  Time  SF as [ E Unit ] dec
after t = time >>> edgeWhen (_<=_ t)

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

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

afterEachTag : {as : SVDesc0}  {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 : SigDesc0}  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 : SVDesc0}  {d : Dec}  SF as bs d  SF (as ++ cs) (bs ++ cs) cau
sfFirst {_} {_} {_} {d} sf = substSFd (∨true d) (sf *** identity)

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