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

open import NeilPrelude
open import Core
open import Bool
open import BoolOrd
open import BoolProps

module Evaluator where

-- Utility Function --

afterSwitchWeaken : {d₁ d₂ : Dec} → {as bs : SVDesc} → SF as bs d₂ → SF as bs (d₁ ∨ d₂)
afterSwitchWeaken {d} = weaken (≤B-supR {d})

-- Evaluation Signal Functions --

mutual

-- eval is the ⇒ evaluation relation

eval : {as bs : SVDesc} → {d : Dec} → Δt → SF as bs d → SVRep as → SF as bs d × SVRep bs

eval t (prim f s) as = first (prim f) (f t s as)

eval t (dprim f s) as = first (dprim f ∘ applyTo as) (f t s)

eval t (sfl >>> sfr) as with second (eval t sfr) (eval t sfl as)
... | sfl' , sfr' , bs = sfl' >>> sfr' , bs

eval t (sfl *** sfr) as = (_***_ ∥∥ uncurry _+++_ ∘ eval t sfl ∥ eval t sfr ∘ svsplit) as

eval t (loop sfs sff) as with evalφ t sff refl
... | g , cs with eval t sfs (as +++ cs)
...    | sfs' , bsds = (first (loop sfs' ∘ g) ∘ swap ∘ svsplit) bsds

eval t (switch {d} sf f) as with eval t sf as
... | sf' , nothing ∷ bs = switch sf' f , bs
... | _   , just e  ∷ _ = first (afterSwitchWeaken {d}) (eval t0 (f e) as)

eval t (dswitch {d} sf f) as with eval t sf as
... | sf' , nothing ∷ bs = dswitch sf' f , bs
... | _   , just e  ∷ bs = (weaken (≤B-supR {d}) ∘ fst ∘ eval t0 (f e)) as , bs

eval t (weaken w sf) as = first (weaken w) (eval t sf as)

-- Rather than have a two phased evaluation function and an intermediate data structure,
-- we instead have evalφ return a function from input to updated signal function
-- thus evalφ does the work of both ⇒φ₁ and ⇒φ₂

evalφ : {as bs : SVDesc} → {d : Dec} → Δt → SF as bs d → d ≡ dec → (SVRep as → SF as bs dec) × SVRep bs

evalφ t (prim f s) ()

evalφ t (dprim f s) refl = first (λ g → dprim f ∘ g) (f t s)

evalφ t (_>>>_ {false} sfl sfr) _ with (evalφ t sfl refl)
... | g , bs = first (λ sfr' → flip _>>>_ sfr' ∘ g) (eval t sfr bs)
evalφ t (_>>>_ {true} sfl sfr) refl = first (λ g → uncurry _>>>_ ∘ second g ∘ eval t sfl) (evalφ t sfr refl)

evalφ t (sfl *** sfr) p = (across (λ fl fr → uncurry _***_ ∘ fl ∥ fr ∘ svsplit) _+++_ ∘ evalφ t sfl ∥ evalφ t sfr ∘ ∨split) p

evalφ t (loop .{_} {_} {BS} sfs sff) refl with second (svsplit {BS}) (evalφ t sfs refl)
... | g , bs , ds with eval t sff ds
...    | sff' , cs = (λ as → loop (g (as +++ cs)) sff') , bs

evalφ t (switch {d₁} {d₂} sf f) p with ∨split {d₁} {d₂} p
evalφ t (switch .{_} .{_} sf f) _ | refl , refl with evalφ t sf refl
... | g , nothing ∷ bs = flip switch f ∘ g , bs
... | _ , just e  ∷ _ = evalφ t0 (f e) refl

evalφ t (dswitch {d₁} {d₂} sf f) p with ∨split {d₁} {d₂} p
evalφ t (dswitch .{_} .{_} sf f) _ | refl , refl with evalφ t sf refl
... | g , nothing ∷ bs = flip dswitch f ∘ g , bs
... | _ , just e  ∷ bs = (λ as → (applyTo as ∘ fst ∘ evalφ t0 (f e)) refl) , bs

evalφ t (weaken (inr refl) sf) refl = evalφ t sf refl
evalφ t (weaken (inl f<t) _) ()

```