structure Sparkle.Core.Sim.PureLean.Simulator (α : Type) : Type

Pure-Lean simulator state: a closure over the signal and a mutable cycle counter. t is the next cycle to read.

• t : IO.Ref Nat

  Cycle to evaluate on the next read.

• evalAt : Nat → α

  Closure that, given a cycle index, returns the signal value.

def Sparkle.Core.Sim.PureLean.of {dom : Domain.DomainConfig} {α : Type} (s : Signal.Signal dom α) : IO (Simulator α)

Construct a pure-Lean simulator from a Signal value. The returned simulator is positioned at cycle 0 — call Sim.reset before reading if you've already stepped through it.

Equations

• Sparkle.Core.Sim.PureLean.of s = do let t ← liftM (IO.mkRef 0) pure { t := t, evalAt := s.val }

instance Sparkle.Core.Sim.PureLean.instSimSimulatorUnit {α : Type} : Sim (Simulator α) Unit α

Equations

• One or more equations did not get rendered due to their size.