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

module CFRP where

open import NeilPrelude
open import List
open import RealTime renaming (_₀>=₀_ to _>=_ ; _₀>₀_ to _>_)
open import Real hiding (_>=_)

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

Behaviour : Set  Set
Behaviour A = StartTime  SampleTime  A

Event : Set  Set
Event A = StartTime  SampleTime  List (Time × A)

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

constant : {A : Set}  A  Behaviour A
constant a = λ t₀ t₁  a  

-- liftE : {A B : Set} → (A → B) → Event A → Event B
-- liftE f ev = (result2 ∘ map ∘ second) f ev 

liftB : {A B : Set}  (A  B)  Behaviour A  Behaviour B
liftB f beh = λ t₀ t₁  f (beh t₀ t₁)

liftB2 : {A B C : Set}  (A  B  C)  Behaviour A  Behaviour B  Behaviour C
liftB2 f beh₁ beh₂ = λ t₀ t₁  f (beh₁ t₀ t₁) (beh₂ t₀ t₁)

notYet : {A : Set}  Event A  Event A
notYet ev = λ t₀ t₁  dropWhile (_>=_ t₀  fst) (ev t₀ t₁)

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

postulate when : {A : Set}  (A  Bool)  Behaviour A  Event A
postulate integral : Behaviour   Behaviour 

iIntegral :   Behaviour   Behaviour 
iIntegral x = liftB (_+_ x)  integral

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

untilB : {A E : Set}  Behaviour A  Event E  (E  Behaviour A)  Behaviour A
untilB beh ev f t₀ t₁ with ev t₀ t₁
... | []            = beh t₀ t₁
... | (te , e)  _  = (f e) te t₁

untilB' : {A E : Set}  Behaviour A  Event E  (E  Behaviour A)  Behaviour A
untilB' beh ev f t₀ t₁ with ev t₀ t₁
... | []            = beh t₀ t₁
... | (te , e)  _  = (f e) t₀ t₁

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

replaceBeh₀ : {A E : Set}  Event E  Behaviour A  (E  Behaviour A)  Behaviour A
replaceBeh₀ ev beh f = untilB beh ev  e  replaceBeh₀ ev (f e) f)

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

runningInBB : {A B : Set}  Behaviour A  (Behaviour A  Behaviour B)  Behaviour B
runningInBB beh f = λ t₀  f  _  beh t₀) t₀

runningInEB : {A B : Set}  Event A  (Event A  Behaviour B)  Behaviour B
runningInEB ev f = λ t₀  f  te  dropWhile ((_>_ te)  fst)  ev t₀) t₀

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

replaceBeh : {A E : Set}  Event E  Behaviour A  (E  Behaviour A)  Behaviour A
replaceBeh {A} {E} ev beh f = runningInEB ev  rev  replaceBehAux rev beh)
                              where
                                   replaceBehAux : Event E  Behaviour A  Behaviour A
                                   replaceBehAux rev beh' = untilB beh' rev  e  replaceBehAux (notYet rev) (f e))

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

open import BouncingBall

fallingBall : Ball  Behaviour Ball
fallingBall (h₀ , v₀) =  let  a = constant (negate g)
                              v = iIntegral v₀ a
                              h = iIntegral h₀ v
                         in liftB2 (_,_) h v

detectBounce : Behaviour Ball  Event Ball
detectBounce = when detectImpact

elasticBall : Ball  Behaviour Ball
elasticBall b =  let beh = fallingBall b
                 in untilB beh (detectBounce beh) (elasticBall  negateVel)

inelasticBall : Ball  Behaviour Ball
inelasticBall b =  let beh = fallingBall b
                   in untilB beh (detectBounce beh)  _  constant (O , O))

resetBall₀ : Event Ball  (Ball  Behaviour Ball)  Ball  Behaviour Ball
resetBall₀ ev f b = untilB (f b) ev (resetBall₀ ev f)

resetBall : Event Ball  (Ball  Behaviour Ball)  Ball  Behaviour Ball
resetBall ev f b = replaceBeh ev (f b) f

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