Previous Up

2.4  The Recursive Wired Buffer

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

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
          o = buffer (n-1) pusho pop

(* 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

let node sbuffer (static n) push pop = buffer n push pop

This corresponds to a hardware implementation and is certainly not a good way to implement it in software since pushing or poping a value is in O(n) for a n-place buffer. A more efficient version (which can also be programmed in Lucid Synchrone) stores values in a circular array.

Previous Up