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