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

open import NeilPrelude
open import Nat
open import CoreFull
open import EvaluatorFull
open import Vector

module ExecuterFull where

-- Run a signal function over a finite amount of predetermined input

runSFR : {as bs : SVDescR} → {d : Dec} → {n : ℕ} → Vec (SVRepR as × Δt) n → SFR as bs d → SFR as bs d × Vec (SVRepR bs) n
runSFR [] sf = sf , []
runSFR ((as , t) ∷ ass) sf with eval t sf as
... | sf' , bs = second (_∷_ bs) (runSFR ass sf')

runSF : {as bs : SVDesc0} → {d : Dec} → {n : ℕ} → SVRep0 as → Vec (SVRepR (svd0toR as) × Δt) n → SF as bs d → SFR (svd0toR as) (svd0toR bs) d × SVRep0 bs × Vec (SVRepR (svd0toR bs)) n
runSF as0 ass sf with eval0 sf as0
... | sf' , bs with runSFR ass sf'
...    | sf'' , bss  = sf'' , bs , bss


-- Run a signal function that requires no input for n steps at a sampling rate t

simpleRunR : {bs : SVDescR} → {d : Dec} → (n : ℕ) → Δt → SFR [] bs d → SFR [] bs d × Vec (SVRepR bs) n
simpleRunR n t = runSFR (vec (⟨⟩ , t))

simpleRun : {bs : SVDesc0} → {d : Dec} → (n : ℕ) → Δt → SF [] bs d → SFR [] (svd0toR bs) d × SVRep0 bs × Vec (SVRepR (svd0toR bs)) n
simpleRun n t = runSF ⟨⟩ (vec (⟨⟩ , t))