Previous Up Next

1.10  Higher-order Reactive Features

1.10.1  Composing Functions

The language is a functional language: functions are first-class objects which can be given to functions or returned by functions. For example, the it function feeds back a network (i.e, it iterates a function on a stream of values). It graphical representation is given in figure 1.6.


Figure 1.6: A rewinding operator

let node it f init x = y where
  rec y = f x (init fby y)

val it : (’a -> ’b -> ’b) -> ’b -> ’a => ’b
val it :: (’a -> ’b -> ’b) -> ’b -> ’a -> ’b

such that:

sum x = it (+) 0 x

Note that type signature of it states that its argument f is considered to be a combinatorial function. To make a (more general) rewinding operator for a stateful function, one has to write instead:

let node it f init x = y where
  rec y = run (f x) (init fby y)

val it : (’a -> ’b => ’b) -> ’b -> ’a => ’b
val it :: (’a -> ’b -> ’b) -> ’b -> ’a -> ’b

The run keyword used in an expression states that its argument is expected to be a stateful function. Thus, run (f x) indicates that f x must have some type t1t2 instead of t1t2.

Higher-order is a natural way to build new primitives from existing ones. For example, the so-called “activation condition” is a build-in operator in block-diagram design tools (à la Scade/Lustre or Simulink). An activation condition takes a function f, a clock clk, a default value and an input an computes f(input when clk). It then sets the result on the base clock.

let node cond_act f clk default input =
  let rec o =
    merge clk (run f (input when clk))
              ((default fby o) whenot clk) in
  o

node cond_act :  (’a => ’b) -> bool -> ’b -> ’a -> ’b
node cond_act :: (’a on _c0 -> ’a on _c0) -> (_c0:’a) -> ’a -> ’a -> ’a

Using the cond_act construction, one can rewrite the RisingEdgeRetrigger operator given in section 1.2.2 as the following:

let node count_down (res, n) = cpt where
  rec cpt = if res then n else (n -> pre (cpt - 1))

let node rising_edge_retrigger rer_input number_of_cycle = rer_output where
    rec rer_output = (0 < v) & clk
    and v = cond_act count_down clk 0 (count, number_of_cycle)
    and c = false fby rer_output
    and clock clk = c or count
    and count = false -> (rer_input & pre (not rer_input))

The symmetric operation of the activation condition is an iterator which simulates an internal for or while loop, generalizing what has been done in paragraph 1.2.3. This operator consists in iterating a function on an input.

let node iter clk init f input =
    (* read input when clk is true *)
    let rec i = merge clk input ((init fby i) whenot clk) in
    let rec o = f i po
    and po = merge clk (init when clk) ((init fby o) whenot clk) in
    (* emit output when clk is true *)
    o when clk

val iter :  clock -> ’a -> (’a -> ’a -> ’a) -> ’a => ’a
val iter :: (_c0:’a) -> ’a -> (’a -> ’a -> ’a) -> ’a on _c0 -> ’a on _c0

iter clk init f input reads an input every time clk is true and computes f. The computation takes place at every instant (on clock 'a) whereas input is read only when clk is true.

We can illustrate this operator on the computation of the power of a sequence. Let x be some stream with clock 'a on clk such that the number of instants between two successive true values of clk is k. Now, write a program which computes the sequence (yi)iIN such that y0 = 1 and yi+1 = xiki.

clktfftftffftt...
xx0  x1 x2   x3x4...
k12312123411...
y1  x03 x12   x24x3...

This program can be implemented in the following way:

let node power clk x = o where
    o = iter clk 1 (fun i acc -> i * acc) x

let node power10 x = power ten x

1.10.2  Combinators

Here are some typical combinators.

let node (||) f g x = (run f x, run g x)

let node (>) f g x = run g (run f x)

let clock half = h where rec h = true -> not (pre h)

let node alternate f g x = merge half (run f (x when half))
                                      (run g (x whenot half))

val || :  (’a => ’b) -> (’a => ’c) -> ’a => ’b * ’c
val || :: (’a -> ’b) -> (’a -> ’c) -> ’a -> ’b * ’c
val > :  (’a => ’b) -> (’b => ’c) -> ’a => ’c
val > :: (’a -> ’b) -> (’b -> ’c) -> ’a -> ’c
val half :  bool
val half :: ’a
val alternate :  (’a => ’b) -> (’a => ’b) -> ’a => ’b
val alternate ::
  (’a on half -> ’b on half) ->
  (’a on not half -> ’b on not half) -> ’a -> ’b

The infix operator (||) computes the product of two functions f and g and (>) composes two functions. alternate alternates the execution of a function with another one.

All the programs defined above still define reactive systems: programs are compiled into finite state machines answering in bounding time and space whatever be their input.

1.10.3  Streams of Functions and Functions of Streams

In the examples considered previously, function used as parameters do not evolve during the execution. Intuitively, the it function receives a stream function f and instantiates it once.

The language provides some means to deal with streams of functions. This is strictly more expressive that the previous case and is a way to model reconfigurable systems.

1.10.4  Instantiating Streams of Functions

The function application instantiates a function with some argument. We can define a more general operator, say reconfigure which expects a stream of function code, an argument and instantiates the current value of the code every time a new code is received.

let node reconfigure code input = o where
  rec automaton
        Await -> do unless code(c) then Run(c)
      | Run(c) -> do emit o = c input unless code(c) then Run(c)
      end

We can make the example a little more complicated by bounding the time for computing c input. For example:

let node server code input money = o where
  automaton
    Await -> 
      do unless code(c) & money(m) then Run(c,m)
  | Run(c,m) ->
      let rec cpt = m -> pre cpt - 1 in
      do emit o = c input 
      until (cpt = 0) then Await
  end

Previous Up Next