open import NeilPrelude1
open import Core1
open import BoolOrd1
open import BoolProps1

module Evaluator1 where

-- Utility Function --

afterSwitchWeaken : {d₂ : Dec} → {as bs : SVDesc} → (d₁ : Dec) → SF as bs d₂ → SF as bs (d₁ ∨ d₂)
afterSwitchWeaken d = weaken (∨maxR 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 1×1 SVRep bs

  eval t (prim f s) as with f t s as
  ... | s' & bs = prim f s' & bs 

  eval t (dprim f s) as with f t s
  ... | g & bs = dprim f (g as) & bs

  eval t (sfl >>> sfr) as with eval t sfl as
  ... | sfl' & bs with eval t sfr bs
  ...    | sfr' & cs = sfl' >>> sfr' & cs

  eval t (_***_ {_} {_} {AS} sfl sfr) asbs with svsplit {AS} asbs
  ... | as & bs with eval t sfl as | eval t sfr bs
  ...    | sfl' & cs | sfr' & ds = sfl' *** sfr' & cs +++ ds  

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

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

  eval t (dswitch {d} sf f) as with eval t sf as
  ... | sf' & nothing  ∷ bs = dswitch sf' f & bs
  ... | _   & just e   ∷ bs with eval t0 (f e) as
  ...     | rsf & _ = afterSwitchWeaken d rsf & bs

  eval t (weaken w sf) as with eval t sf as
  ... | sf' & bs = weaken w sf' & bs


-- 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) 1×1 SVRep bs

  evalφ t (prim f s) ()

  evalφ t (dprim f s) refl with f t s
  ... | g & bs = (λ as → dprim f (g as)) & bs

  evalφ t (_>>>_ {false} sfl sfr) _ with (evalφ t sfl refl)
  ... | g & bs with eval t sfr bs
  ...    | sfr' & cs = (λ as → g as >>> sfr' ) & cs
  evalφ t (_>>>_ {true} .{_} {AS} {_} {CS} sfl sfr) refl with evalφ t sfr refl
  ... | g & cs = aux & cs
                 where aux : SVRep AS → SF AS CS dec
                       aux as with eval t sfl as
                       ... | sfl' & bs = sfl' >>> g bs

  evalφ t (_***_ {d} {_} {AS} {BS} {CS} {DS} sfl sfr) p with ∨split {d} p
  ... | pl & pr with evalφ t sfl pl | evalφ t sfr pr
  ...   | g & cs | h & ds = aux & cs +++ ds
                            where aux : SVRep (AS ++ BS) → SF (AS ++ BS) (CS ++ DS) dec
                                  aux asbs with svsplit {AS} asbs
                                  ... | as & bs = g as *** h bs

  evalφ t (loop .{_} {_} {BS} sfs sff) refl with evalφ t sfs refl
  ... | g & bsds with svsplit {BS} bsds
  ...   | 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 = (λ as → switch (g as) f) & 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 = (λ as → dswitch (g as) f) & bs
  ... | _ & just e   ∷ bs with evalφ t0 (f e) refl
  ...    | g & _ = g & bs

  evalφ t (weaken {false} _ sf) refl = evalφ t sf refl
  evalφ t (weaken {true} () _) refl