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

module Library2 where

open import NeilPrelude
open import RealTime
open import Real
open import SigVecs
open import NaryFRP
open import Library1
open import RSwitch
open import Bool using (not)

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

-- For human-readable versions of this library code
-- (i.e. without the implicit arguments)
-- see the Agda embeddings 

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

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 (forkSecond {bs} {E A} sfe))

rswitchWhen : {as bs : SVDesc}  {A : Set}  SF as bs  SF bs (E A)  (A  SF as bs)  SF as bs
rswitchWhen {as} {bs} {A} sf sfe f = rswitch {as} {bs} (_>>>_ {as} {bs} {bs , E A} sf (forkSecond {bs} {E A} sfe))  e  _>>>_ {as} {bs} {bs , E A} (f e) (forkSecond {bs} {E A} sfe)) 

replace : {as bs : SVDesc}  {A : Set}  SF as bs  (A  SF as bs)  SF (as , E A) bs
replace {as} {bs} {A} sf f = rswitch {as , E A} {bs} (sfFirst {as} {bs} {E A} sf)  e  sfFirst {as} {bs} {E A} (f e))

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

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

dhold : {A : Set}  A  SF (E A) (C A)
dhold {A} a = _>>>_ {E A} {S A} {C A} (hold a) (dfromS 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))

sampleC : {A B : Set}  SF (C A , E B) (E A)
sampleC = sampleWithC const

sampleS : {A B : Set}  SF (S A , E B) (E A)
sampleS = sampleWithS const

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

repeatedly : {as : SVDesc}  Time⁺  SF as (E Unit)
repeatedly {as} t = rswitchWhen {as} {E Unit} (never {as}) (after {E Unit} t)  _  now {as})

tag : {A B : Set}  A  SF (E B) (E A)
tag a = liftE (const a)

nowTag : {as : SVDesc}  {A : Set}  A  SF as (E A)
nowTag {as} {A} a = _>>>_ {as} {E Unit} {E A} (now {as}) (tag a)

afterTag : {as : SVDesc}  {A : Set}  Time⁺  A  SF as (E A)
afterTag {as} {A} t a = _>>>_ {as} {E Unit} {E A} (after {as} t) (tag a)

once : {A : Set}  SF (E A) (E A)
once {A} = switch {E A} {E A} (sfFork {E A}) (nowTag {E A})

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

symLoop : {as bs cs ds : SVDesc}  SF (as , cs) (bs , ds)  SF ds cs  SF as bs
symLoop {as} {bs} {cs} {ds} sff sfb = _>>>_ {as} {bs , ds} {bs} (loop {as} {bs , ds} {cs} sff (_>>>_ {bs , ds} {ds} {cs} (sfSnd {bs} {ds}) sfb)) (sfFst {bs} {ds})

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

save : {as bs : SVDesc}  {A : Set}  SF as bs  SF (as , E A) (bs , E (SF as bs))
save {as} {bs} {A} sf = _>>>_ {as , E A} {bs , (C _ , E A)} {bs , E _} (_>>>_ {as , E A} {(bs , C _) , E A} {bs , (C _ , E A)} (sfFirst {as} {bs , C _} {E A} (freeze {as} {bs} sf)) (sfAssocR {bs} {C _} {E A})) (sfSecond {bs} {C _ , E A} {E _} sampleC)

saveReplace : {as bs : SVDesc}  {A : Set}  SF as bs  SF ((as , E A) , E (SF as bs)) (bs , E (SF as bs))
saveReplace {as} {bs} {A} sf = replace {as , E A} {bs , E _} (save {as} {bs} sf) (save {as} {bs})

saveResume : {as bs : SVDesc}  {A B : Set}  SF as bs  SF ((as , E A) , E B) bs
saveResume {as} {bs} {A} {B} sf = symLoop {(as , E A) , E B} {bs} {C _} {E _} (_>>>_ {((as , E A) , E B) , C _} {(as , E A) , E _} {bs , E _} (_>>>_ {((as , E A) , E B) , C _} {(as , E A) , E B , C _} {(as , E A) , E _} (sfAssocR {as , E A} {E B} {C _}) (sfSecond {as , E A} {E B , C _} {E _} (_>>>_ {E B , C _} {C _ , E B} {E _} (sfSwap {E B} {C _}) sampleC))) (saveReplace {as} {bs} sf)) (dhold sf)

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

open import BouncingBall

fallingBall : {as : SVDesc}  Ball  SF as (C Ball)
fallingBall {as} (h , v) = _>>>_ {as} {S _} {C _} (constantS {as} (negate g)) (_>>>_ {S _} {C _} {C _} (iIntegralS v) (_>>>_ {C _} {C _ , C _} {C _} (forkFirst {C _} {C _} (iIntegralC h)) (liftC2 (_,_))))

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

elasticBall : {as : SVDesc}  Ball  SF as (C Ball)
elasticBall {as} b = rswitchWhen {as} {C _} (fallingBall {as} b) detectBounce (fallingBall {as}  negateVel)

inelasticBall : {as : SVDesc}  Ball  SF as (C Ball)
inelasticBall {as} b = switchWhen {as} {C _} (fallingBall {as} b) detectBounce  _  constantC {as} (O , O))

resetBall : {as : SVDesc}  (Ball  SF as (C Ball))  Ball  SF (as , E Ball) (C Ball)
resetBall {as} f b = replace {as} {C _} (f b) f

oneInelasticReset : Ball  SF (E Ball) (C Ball)
oneInelasticReset b = _>>>_ {E _} {E _} {C _} once (_>>>_ {E _} {E _ , E _} {C _} (sfFork {E _}) (resetBall {E _} (inelasticBall {E _}) b))

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

-- Thomson's Lamp
lamp : {as : SVDesc}  Time⁺  Bool  SF as (S Bool)
lamp {as} t b = rswitch {as} {S _} (lampAux (t , b)) lampAux
    where
          lampAux : (Time⁺ × Bool)  SF as (S Bool , E (Time⁺ × Bool))
          lampAux (t' , b') = _&&&_ {as} {S _} {E _} (constantS {as} b') (afterTag {as} t' (halfℜ⁺ t' , not b'))

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

sampleTime : {A : Set}  SF (E A) (E )
sampleTime = _>>>_ {E _} {C _ , E _} {E _} (forkFirst {E _} {C _} (localTime {E _})) sampleC

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