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

module CFRP where

open import NeilPrelude
open import List
open import RealTime
open import Real

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

Behaviour : Set  Set
Behaviour A = StartTime  SampleTime  A

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

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

constantB : {A : Set}  A  Behaviour A
constantB a = λ t0 t1  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 = result2 f beh

liftB2 : {A B D : Set}  (A  B  D)  Behaviour A  Behaviour B  Behaviour D
liftB2 f beh1 beh2 = λ t0 t1  f (beh1 t0 t1) (beh2 t0 t1)

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

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

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

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

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

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

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

open import BouncingBall

falling : Ball  Behaviour Ball
falling (h0 , v0) =  let  a = constantB (negate g)
                          v = iIntegral v0 a
                          h = iIntegral h0 v
                      in
                          liftB2 (_,_) h v

detectBounce : Behaviour Ball  Event Ball
detectBounce = when detectImpact

bouncingBall : (Ball  Behaviour Ball)  Ball  Behaviour Ball
bouncingBall f b =  let  beh = falling b
                    in
                         untilB beh (liftE f (detectBounce beh))

elasticBall : Ball  Behaviour Ball
elasticBall = bouncingBall (elasticBall  negateVel)

inelasticBall : Ball  Behaviour Ball
inelasticBall = bouncingBall  _  constantB (O , O))

resetBB : (Ball  Behaviour Ball)  Event Ball  Ball  Behaviour Ball
resetBB f ev b = untilB (bouncingBall f b) (liftE (resetBB f ev) ev)

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₀

resetBB' : (Ball  Behaviour Ball)  Event Ball  Ball  Behaviour Ball
resetBB' f ev b =  runningInEB ev  rev  resetBBaux rev b)
                   where
                          resetBBaux : Event Ball  Ball  Behaviour Ball
                          resetBBaux rev b' = untilB (bouncingBall f b') (liftE (resetBBaux rev) rev)

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