{-# 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)

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