The following example illustrates the combination of synchrony and recursion. We program a buffer by composing several instances of a one place buffer 3.
A one-place buffer is defined in the following way. In doing it, it is important that the one-place buffer emits its internal values when it is full and receives a push in order to pass it to its son.
type 'a option = None | Some of 'a
let node count n = ok where
rec o = 0 -> (pre o + 1) mod n
and ok = false -> o = 0
(* the 1-buffer with bypass *)
let node buffer1 push pop = o where
rec last memo = None
and match last memo with
None ->
do present
push(v) & pop() -> do emit o = v done
| push(v) -> do memo = Some(v) done
end done
| Some(v) ->
do present
push(w) -> do emit o = v and memo = Some(w) done
| pop() -> do emit o = v and memo = None done
end done
end
The n-buffer is the composition of n one-place buffers.
(* the recursive buffer *)
let rec node buffer n push pop = o where
match n with
0 ->
do o = push done
| n ->
let pusho = buffer1 push pop in
do
o = buffer (n-1) pusho pop
done
end
(* the main buffer function only responds when it receives a pop *)
let node buffer n push pop = o where
rec pusho = buffer n push pop
and present
pop() & pusho(v) -> do emit o = v done
| _ -> do done
end
let node sbuffer (static n) push pop = buffer n push pop