{-# OPTIONS --type-in-type --no-termination-check
   #-}

module NaryFRP where

open import NeilPrelude
open import Maybe
open import List
open import RealTime
open import Real hiding (_-_)
open import TimeDeltaList
open import SigVecs
open import Utilities
open import StrictTotalOrder

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

identity : {as : SVDesc} → SF as as
identity = λ as → as

sfFst : {as bs : SVDesc} → SF (as , bs) as
sfFst = fst

sfSnd : {as bs : SVDesc} → SF (as , bs) bs
sfSnd = snd

infixr  _>>>_
infixr  _&&&_

_>>>_ :  {as bs cs : SVDesc} → SF as bs  → SF bs cs  → SF as cs
sf1 >>> sf2 = sf2 ∘ sf1

_&&&_ :  {as bs cs : SVDesc} → SF as bs  → SF as cs  → SF as (bs , cs)
sf1 &&& sf2 = λ as → (sf1 as , sf2 as)

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

-- We know the sample time is at least the event time,
-- but inserting a proof into the defintion would unnecessarily complicate it
private  
         postulate ≤-trustme : {te : EventTime} → {t : SampleTime} → te ≤ℜ₀ t

         _-_ : (t : SampleTime) → (te : EventTime) → Time
         t - te = ℜ₀-minus t te ≤-trustme


switchC : {as : SVDesc} → {A B : Set} → SF as (C B , E A) → (A → SF as (C B)) → SF as (C B)
switchC {as} sf f sa t with sf sa
... | (sb , se) with fstOcc se t
...    | nothing        =  sb t
...    | just (te , e)  =  (f e) (advance {as} te sa) (t - te)


switch : {as bs : SVDesc} → {A : Set} → (SF as (bs , E A)) → (A → SF as bs) → SF as bs
switch {as} {bs} sf f sa with sf sa
... | sb , se = svAtTime {bs} (λ t → maybe sb
                                           (uncurry (λ te e → (splice {bs} sb ((f e) (advance {as} te sa)) te)))
                                           (fstOcc se t))

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

constantS : {as : SVDesc} → {A : Set} → A → SF as (S A)
constantS a = const (a , const [])

never : {as : SVDesc} → {A : Set} → SF as (E A)
never = const (nothing , const [])

now : {as : SVDesc} → SF as (E Unit)
now = const (just unit , const []) 

hold : {A : Set} → A → SF (E A) (S A)
hold a = first (fromMaybe a)

edge : SF (S Bool) (E Unit)
edge (b , cp) = (nothing , edgeAux b ∘ cp)
  where
        edgeAux : Bool → ChangeList Bool → ChangeList Unit
        edgeAux _      []                   = []
        edgeAux true   ((_ , b) ∷ δbs)      = edgeAux b δbs
        edgeAux false  ((_ , false) ∷ δbs)  = edgeAux false δbs
        edgeAux false  ((δ , true) ∷ δbs)   = (δ , unit) ∷ edgeAux true δbs

integralS : SF (S ℜ) (C ℜ)
integralS (x₀ , cp) t =   let 
                               δas   =  cp t
                               ds    =  map (_>0 ∘ fst) δas ++ t ₀-₀ lastChangeTime δas ∷ []
                               xs    =  x₀ ∷ map snd δas 
                          in
                               sumℜ (zipWith _*_ ds xs)

postulate integralC : SF (C ℜ) (C ℜ)

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

delayC : {A : Set} → Time⁺ → (Time → A) → SF (C A) (C A)
delayC d f s t with compareℜ₀ t (d >0)
delayC d f s ._ | refl   = s O
delayC d f s t  | less p = f t
delayC d f s t  | more p = s (ℜ₀⁺₀-minus t d (inl p))

delayS : {A : Set} → Time⁺ → A → SF (S A) (S A)
delayS d a₀ (a₁ , cp) = a₀ , delayCP d (just a₁) cp

delayE : {A : Set} → Time⁺ → SF (E A) (E A)
delayE d (ma , cp) = nothing , delayCP d ma cp

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

liftC : {A B : Set} → (A → B) → SF (C A) (C B)
liftC = mapC

liftS : {A B : Set} → (A → B) → SF (S A) (S B)
liftS = mapS

liftE : {A B : Set} → (A → B) → SF (E A) (E B)
liftE = mapE

liftC2 : {A B Z : Set} → (A → B → Z) → SF (C A , C B) (C Z)
liftC2 f = uncurry (mapC2 f)

liftS2 : {A B Z : Set} → (A → B → Z) → SF (S A , S B) (S Z)
liftS2 f = uncurry (mapS2 f)

merge : {A B Z : Set} → (A → Z) → (B → Z) → (A → B → Z) → SF (E A , E B) (E Z)
merge fa fb fab = uncurry (mergeE2 fa fb fab)

join : {A B Z : Set} → (A → B → Z) → SF (E A , E B) (E Z)
join f = uncurry (joinE2 f)

sampleWithC : {A B Z : Set} → (A → B → Z) → SF (C A , E B) (E Z)
sampleWithC f = uncurry (mapCE f)

sampleWithS : {A B Z : Set} → (A → B → Z) → SF (S A , E B) (E Z)
sampleWithS f = uncurry (mapSE f)

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

fromS : {A : Set} -> SF (S A) (C A)
fromS = valS

postulate when : {A : Set} → (A → Bool) → SF (C A) (E A)


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

-- Unfortunately, Agda fails to infer the implicit SVDescs for the signal function combinators.
-- They can be filled in manually, but this makes the code unreadable.
-- Thus I've commented out the readable version of the code below,
-- and then placed the unreadable version with implicit arguments included below that.

-- The problem seems to be that SF is a function, rather than a data constructor.
-- In the sampled implementation (where SF is data),  it can infer them.

{-
toFst : {as bs cs : SVDesc} → SF as cs  →  SF (as , bs) cs
toFst sf = sfFst >>> sf

toSnd : {as bs cs : SVDesc} → SF bs cs  →  SF (as , bs) cs
toSnd sf = sfSnd >>> sf

_***_ : {as bs cs ds : SVDesc} → SF as cs → SF bs ds → SF (as , bs) (cs , ds)
sf1 *** sf2 = toFst sf1 &&& toSnd sf2

sfFirst : {as bs cs : SVDesc} → SF as bs → SF (as , cs) (bs , cs)
sfFirst sf = sf *** identity

sfSecond : {as bs cs : SVDesc} → SF bs cs → SF (as , bs) (as , cs)
sfSecond sf = identity *** sf

sfFork : {as : SVDesc} → SF as (as , as)
sfFork = identity &&& identity

sfSwap : {as bs : SVDesc} → SF (as , bs) (bs , as)
sfSwap = sfSnd &&& sfFst

fanoutFirst : {as bs : SVDesc} → SF as bs → SF as (bs , as)
fanoutFirst sf = sf &&& identity

fanoutSecond : {as bs : SVDesc} → SF as bs → SF as (as , bs)
fanoutSecond sf = identity &&& sf

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

switchWhen : {as bs : SVDesc} → {A : Set} → SF as bs → SF bs (E A) → (A → SF as bs) → SF as bs
switchWhen sf sfe = switch (sf >>> fanoutSecond sfe)

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

localTime : {as : SVDesc} → SF as (C ℜ)
localTime = constantS ı >>> integralS

after : {as : SVDesc} → Time⁺ → SF as (E Unit)
after t = now >>> delayE t

constantC : {as : SVDesc} → {A : Set} → A → SF as (C A)
constantC a = constantS a >>> fromS

iIntegralS : ℜ → SF (S ℜ) (C ℜ)
iIntegralS x = integralS >>> liftC (_+_ x)

iIntegralC : ℜ → SF (C ℜ) (C ℜ)
iIntegralC x = integralC >>> liftC (_+_ x)

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

open import BouncingBall

falling : {as : SVDesc} → Ball → SF as (C Ball)
falling (h , v) = constantS (negate g) >>> iIntegralS v >>> fanoutFirst (iIntegralC h) >>> liftC2 (_,_)

detectBounce : SF (C Ball) (E Ball)
detectBounce = when detectImpact

bouncingBall : {as : SVDesc} → (Ball → SF as (C Ball)) → Ball → SF as (C Ball)
bouncingBall f b = switchWhen (falling b) detectBounce f

elasticBall : {as : SVDesc} → Ball → SF as (C Ball)
elasticBall = bouncingBall (elasticBall ∘ negateVel)

inelasticBall : {as : SVDesc} → Ball → SF as (C Ball)
inelasticBall = bouncingBall (\ _ → constantC (t≡0 , t≡0))

resetBB : (Ball → SF (E Ball) (C Ball)) → Ball → SF (E Ball) (C Ball)
resetBB f b = switch (fanoutFirst (bouncingBall f b)) (resetBB f)

-------------------------------------------------------------------
-}

toFst : {as bs cs : SVDesc} → SF as cs  →  SF (as , bs) cs
toFst {as} {bs} {cs} sf = _>>>_ {as , bs} {as} {cs} (sfFst {as} {bs}) sf

toSnd : {as bs cs : SVDesc} → SF bs cs  →  SF (as , bs) cs
toSnd {as} {bs} {cs} sf = _>>>_ {as , bs} {bs} {cs} (sfSnd {as} {bs}) sf

_***_ : {as bs cs ds : SVDesc} → SF as cs → SF bs ds → SF (as , bs) (cs , ds)
_***_ {as} {bs} {cs} {ds} sf1 sf2 = _&&&_ {as , bs} {cs} {ds} (toFst {as} {bs} {cs} sf1) (toSnd {as} {bs} {ds} sf2)

sfFirst : {as bs cs : SVDesc} → SF as bs → SF (as , cs) (bs , cs)
sfFirst {as} {bs} {cs} sf = _***_ {as} {cs} {bs} {cs} sf (identity {cs})

sfSecond : {as bs cs : SVDesc} → SF bs cs → SF (as , bs) (as , cs)
sfSecond {as} {bs} {cs} sf = _***_ {as} {bs} {as} {cs} (identity {as}) sf

sfFork : {as : SVDesc} → SF as (as , as)
sfFork {as} = _&&&_ {as} {as} {as} (identity {as}) (identity {as})

sfSwap : {as bs : SVDesc} → SF (as , bs) (bs , as)
sfSwap {as} {bs} = _&&&_ {as , bs} {bs} {as} (sfSnd {as} {bs}) (sfFst {as} {bs})

fanoutFirst : {as bs : SVDesc} → SF as bs → SF as (bs , as)
fanoutFirst {as} {bs} sf = _&&&_ {as} {bs} {as} sf (identity {as})

fanoutSecond : {as bs : SVDesc} → SF as bs → SF as (as , bs)
fanoutSecond {as} {bs} sf = _&&&_ {as} {as} {bs} (identity {as}) sf

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

switchWhen : {as bs : SVDesc} → {A : Set} → SF as bs → SF bs (E A) → (A → SF as bs) → SF as bs
switchWhen {as} {bs} {A} sf sfe = switch {as} {bs} (_>>>_ {as} {bs} {bs , E A} sf (fanoutSecond {bs} {E A} sfe))

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

localTime : {as : SVDesc} → SF as (C ℜ)
localTime {as} = _>>>_ {as} {S ℜ} {C ℜ} (constantS {as} ı) integralS

after : {as : SVDesc} → Time⁺ → SF as (E Unit)
after {as} t = _>>>_ {as} {E Unit} {E Unit} (now {as}) (delayE {Unit} t)

constantC : {as : SVDesc} → {A : Set} → A → SF as (C A)
constantC {as} {A} a = _>>>_ {as} {S A} {C A} (constantS {as} a) (fromS {A})

iIntegralS : ℜ → SF (S ℜ) (C ℜ)
iIntegralS x = _>>>_ {S ℜ} {C ℜ} {C ℜ} integralS (liftC (_+_ x))

iIntegralC : ℜ → SF (C ℜ) (C ℜ)
iIntegralC x = _>>>_ {C ℜ} {C ℜ} {C ℜ} integralC (liftC (_+_ x))

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

open import BouncingBall

falling : {as : SVDesc} → Ball → SF as (C Ball)
falling {as} (h , v) = _>>>_ {as} {S ℜ} {C Ball} (constantS {as} (negate g))
                      (_>>>_ {S ℜ} {C ℜ} {C Ball} (iIntegralS v) 
                      (_>>>_ {C ℜ} {C ℜ , C ℜ} {C Ball} (fanoutFirst {C ℜ} {C ℜ} (iIntegralC h)) (liftC2 (_,_))))

detectBounce : SF (C Ball) (E Ball)
detectBounce = when detectImpact

bouncingBall : {as : SVDesc} → (Ball → SF as (C Ball)) → Ball → SF as (C Ball)
bouncingBall {as} f b = switchWhen {as} {C Ball} (falling {as} b) detectBounce f

elasticBall : {as : SVDesc} → Ball → SF as (C Ball)
elasticBall {as} = bouncingBall {as} (elasticBall {as} ∘ negateVel)

inelasticBall : {as : SVDesc} → Ball → SF as (C Ball)
inelasticBall {as} = bouncingBall {as} (\ _ → constantC {as} (O , O))

resetBB : (Ball → SF (E Ball) (C Ball)) → Ball → SF (E Ball) (C Ball)
resetBB f b = switch {E Ball} {C Ball} (fanoutFirst {E Ball} {C Ball} (bouncingBall {E Ball} f b)) (resetBB f)

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