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

open import NeilPrelude
open import Nat
open import Core
open import Evaluator
open import Vector

module Executer where

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

runSF : {as bs : SVDesc} → {d : Dec} → {n : ℕ} → Vec (SVRep as × Δt) n → SF as bs d → SF as bs d × Vec (SVRep bs) n
runSF [] sf = sf , []
runSF ((as , t) ∷ ass) sf with eval t sf as
... | sf' , bs = second (_∷_ bs) (runSF ass sf')


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

simpleRun : {bs : SVDesc} → {d : Dec} → (n : ℕ) → Δt → SF [] bs d → SF [] bs d × Vec (SVRep bs) n
simpleRun n t sf = runSF (vec (⟨⟩ , t)) sf