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

open import NeilPrelude
open import CoreFull
open import BoolOrd
open import BoolProps
open import ListProps

module EvaluatorFull where

-- Substitutions --

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

afterDSwitchCoerce : {d : Dec} → {bs bs' : SVDesc0} → {as : SVDescR} → initc bs <: bs' → SFR as (svd0toR bs') d → SFR as (svd0toR bs) d
afterDSwitchCoerce = substSFRo ∘ sym ∘ <:initc0toR

afterDSwitchWeaken : {d₁ d₂ : Dec} → {bs bs' : SVDesc0} → {as : SVDescR} → initc bs <: bs' → SFR as (svd0toR bs') d₂ → SFR as (svd0toR bs) (d₁ ∨ d₂)
afterDSwitchWeaken {d} wbs = afterSwitchWeaken {d} ∘ afterDSwitchCoerce wbs

parsubst : {as cs bs ds : SVDesc0} → {d : Dec} → SFR (svd0toR as ++ svd0toR bs) (svd0toR cs ++ svd0toR ds) d → SFR (svd0toR (as ++ bs)) (svd0toR (cs ++ ds)) d
parsubst {as} {cs} = substSFRio (sym (map++ as)) (sym (map++ cs))


-- Evaluation of Stateful Primitives --

evalStateful : {d : Dec} → {State : Set} → {as bs : SVDescR} → Δt → State → SFStateful State as bs d → SVRepR as → State × SVRepR bs
evalStateful t s (prim f) as = f t s as
evalStateful t s (dprim f) as = first (applyTo as) (f t s)

evalStatefulφ : {State : Set} → {as bs : SVDescR} → Δt → State → SFStateful State as bs dec → (SVRepR as → State) × SVRepR bs
evalStatefulφ t s (dprim f) = f t s


-- Initial Evaluation at Time0 --

evalPrim0 : {as bs : SVDesc0} → {d : Dec} → SFPrim as bs d → SVRep0 as → SFR (svd0toR as) (svd0toR bs) d × SVRep0 bs
evalPrim0 (initialised p sf s) as = (sfprim sf ∥ svRto0) (evalStateful t0 s sf (sv0toR p as)) 
evalPrim0 (uninitialised p sf fs) as = sfprim sf (fs as) , mkEmptySV p 
evalPrim0 (router f g) as = sfprim (prim (λ _ _ as → unit , g as)) unit , f as 
evalPrim0 (source f s) _ = (sfprim (dprim (λ t s → first const (f t s))) ∥ svRto0) (f t0 s)  

evalPrim0φ : {as bs : SVDesc0} → SFPrim as bs dec → (SVRep0 as → SFR (svd0toR as) (svd0toR bs) dec) × SVRep0 bs
evalPrim0φ (initialised p sf s) = ((λ g → sfprim sf ∘ g ∘ sv0toR p) ∥ svRto0) (evalStatefulφ t0 s sf)
evalPrim0φ (uninitialised p sf fs) = sfprim sf ∘ fs , mkEmptySV p 
evalPrim0φ (source f s) = (flip (λ _ → sfprim (dprim (λ t' → first const ∘ f t'))) ∥ svRto0) (f t0 s)

mutual

-- eval is the ⇒ evaluation relation at Time0

  eval0 : {as bs : SVDesc0} → {d : Dec} → SF as bs d → SVRep0 as → SFR (svd0toR as) (svd0toR bs) d × SVRep0 bs

  eval0 (sfprim sf) as = evalPrim0 sf as 

  eval0 (sfl >>> sfr) as with second (eval0 sfr) (eval0 sfl as)
  ... | sfl' , sfr' , bs = seq sfl' sfr' , bs  

  eval0 (_***_ {_} {_} {AS} {_} {CS} sfl sfr) as = (first (parsubst {AS} {CS}) ∘ par ∥∥ uncurry _+++_ ∘ eval0 sfl ∥ eval0 sfr ∘ svsplit0) as 

  eval0 (loop {_} {AS} {BS} sfs sff) as with eval0φ sff refl
  ... | g , cs with eval0 sfs (as +++ cs)
  ...    | sfs' , bsds = (first (loop (substSFRio (map++ AS) (map++ BS) sfs') ∘ g) ∘ swap ∘ svsplit0) bsds

  eval0 (switch {d} {_} {_} {BS} sf f) as with eval0 sf as
  ... | sf' , nothing ∷ bs = switch {_} {_} {_} {BS} sf' f , bs
  ... | _   , just e  ∷ _  = ((afterSwitchWeaken {d} ∘ substSFRo (svd0toRinitc BS)) ∥ coerceSV <:initc) (eval0 (f e) as)

  eval0 (diswitch {d} wbs sf f) as with eval0 sf as
  ... | sf' , nothing ∷ bs = diswitch wbs sf' f , bs
  ... | _   , just e  ∷ bs = (afterDSwitchWeaken {d} wbs ∘ fst ∘ eval0 (f e)) as , bs

  eval0 (weaken was wbs wd sf) as = ( (substSFRio (sym (<:0toR was)) (<:0toR wbs) ∘ weaken wd ) ∥ coerceSV wbs) (eval0 sf (coerceSV was 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 ⇒φ₂

  eval0φ : {as bs : SVDesc0} → {d : Dec} → SF as bs d → d ≡ dec → (SVRep0 as → SFR (svd0toR as) (svd0toR bs) dec) × SVRep0 bs

  eval0φ (sfprim sf) refl = evalPrim0φ sf

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

  eval0φ (_***_ {_} {_} {AS} {_} {CS} sfl sfr) p = (across (λ fl fr → parsubst {AS} {CS} ∘ uncurry par ∘ fl ∥ fr ∘ svsplit0) _+++_ ∘ eval0φ sfl ∥ eval0φ sfr ∘ ∨split) p

  eval0φ (loop .{_} {AS} {BS} sfs sff) refl with second (svsplit0 {BS}) (eval0φ sfs refl)
  ... | g , bs , ds with eval0 sff ds
  ...    | sff' , cs = ((λ as → loop (substSFRio (map++ AS) (map++ BS) (g (as +++ cs))) sff')) , bs

  eval0φ (switch {d₁} {d₂} {_} {BS} sf f) p with ∨split {d₁} {d₂} p
  eval0φ (switch .{_} .{_} {_} {BS} sf f) _ | refl , refl with eval0φ sf refl
  ... | g , nothing ∷ bs = flip (switch {_} {_} {_} {BS}) f ∘ g , bs
  ... | _ , just e  ∷ _ = (_∘_ (substSFRo (svd0toRinitc BS)) ∥ coerceSV <:initc) (eval0φ (f e) refl)

  eval0φ (diswitch {d₁} {d₂} wbs sf f) p with ∨split {d₁} {d₂} p
  eval0φ (diswitch .{_} .{_} wbs sf f) _ | refl , refl with eval0φ sf refl
  ... | g , nothing ∷ bs = flip (diswitch wbs) f ∘ g , bs
  ... | _ , just e  ∷ bs = ( (λ g → afterDSwitchCoerce wbs ∘ g ) ∘ fst ∘ eval0φ (f e)) refl , bs


  eval0φ (weaken {false} was wbs _ sf) refl = ((λ g → substSFRio (sym (<:0toR was)) (<:0toR wbs) ∘ g ∘ coerceSV was) ∥ coerceSV wbs) (eval0φ sf refl)
  eval0φ (weaken {true} was wbs (inl ()) sf) refl
  eval0φ (weaken {true} was wbs (inr ()) sf) refl


-- Evaluation of Running Signal Functions (after Time0) --

mutual

-- eval is the ⇒ evaluation relation after Time0

  eval : {as bs : SVDescR} → {d : Dec} → Δt → SFR as bs d → SVRepR as → SFR as bs d × SVRepR bs

  eval t (sfprim sf s) as = first (sfprim sf) (evalStateful t s sf as) 

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

  eval t (par sfl sfr) as = (par ∥∥ uncurry _+++_ ∘ eval t sfl ∥ eval t sfr ∘ svsplitR) 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 ∘ svsplitR) bsds

  eval t (switch {d} {_} {_} {BS} sf f) as with eval t sf as
  ... | sf' , nothing ∷ bs = switch {_} {_} {_} {BS} sf' f , bs
  ... | _   , just e  ∷ _  = ( (afterSwitchWeaken {d} ∘ substSFRo (svd0toRinitc BS)) ∥ svinit0toR BS)
                                (eval0 (f e) (svRto0 as))

  eval t (diswitch {d} wbs sf f) as with eval t sf as
  ... | sf' , nothing ∷ bs = diswitch wbs sf' f , bs
  ... | _   , just e  ∷ bs = (afterDSwitchWeaken {d} wbs ∘ fst ∘ eval0 (f e) ∘ svRto0) 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 : SVDescR} → {d : Dec} → Δt → SFR as bs d → d ≡ dec → (SVRepR as → SFR as bs dec) × SVRepR bs

  evalφ t (sfprim sf s) refl = first (_∘_ (sfprim sf)) (evalStatefulφ t s sf)

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

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


  evalφ t (loop .{_} {_} {BS} sfs sff) refl with second (svsplitR {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₂} {_} {BS} sf f) p with ∨split {d₁} {d₂} p
  evalφ t (switch .{_} .{_} {_} {BS} sf f) _ | refl , refl with evalφ t sf refl
  ... | g , nothing ∷ bs = flip (switch {_} {_} {_} {BS}) f ∘ g , bs
  ... | _ , just e  ∷ _  = ((λ g → substSFRo (svd0toRinitc BS) ∘ g ∘ svRto0) ∥ svinit0toR BS ∘ flip eval0φ refl) (f e)

  evalφ t (diswitch {d₁} {d₂} wbs sf f) p with ∨split {d₁} {d₂} p
  evalφ t (diswitch .{_} .{_} wbs sf f) _ | refl , refl with evalφ t sf refl
  ... | g , nothing ∷ bs = flip (diswitch wbs) f ∘ g , bs
  ... | _ , just e  ∷ bs = ((λ g → afterDSwitchCoerce wbs ∘ g ∘ svRto0) ∘ fst ∘ flip eval0φ refl) (f e) , bs

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