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