(* k-length delay. Complexity in O(k) *) let node delay_k(k)(v,u) = o where rec forall i in 0 .. (k - 1) do o = v fby (last o) initialize last o = u done (* k-length delay. Complexity in O(k) but with a *) (* functional update. Pasteur et al. [LCTES'12] define *) (* an optimisation to generate an in-place modification for *) (* this update. KCG 6.8 implements it... but not Zelus! *) let node delay_k_update(k)(v, u) = o where rec init w = Arrays.const k v and w = { last w with (i) = u } (* functional update *) and o = w.((i + 1) mod k) and i = 0 -> (pre i + 1) mod k (* reset a delay *) let node resettable_delay(k)(x0)(r, u) = o where rec reset o = delay_k(k)(x0)(u) every Edge_front_detectors.rising_bool(r) (* sliding window in O(k) *) let node window(k)(v, x) = t where rec forall i in 0 .. (k - 1), ti out t do acc = v fby (last acc) and ti = last acc initialize last acc = x done