package lustre-v6

  1. Overview
  2. Docs

Expand user nodes

Expand nodes: ------------

if n is a node defined as follows

node n(x,y) returns(a,b); var v1,v2; let v1 = x+y; v2 = x*y; a = v1*x; b = v2*y; tel

equations such as :

o1,o2 = n(i1, i2);

becomes

h1 = i1+i2; h2 = i1*i2; o1 = h1*i1; o2 = h2*i2;

where h1 and h2 are fresh local vars

In other terms, we need to

  • create a fresh local var for each local var of n
  • take all the equations of n, and substitute
  • the inputs parameters by intput args
  • the outputs parameters by lhs list
  • the local vars by the fresh local var names

nb : to simplify, for equations like

f.a = n(t1, 3);

we first create fresh vars for "f.a", "t1", and "3"

_v1 = t1; _v2 = 3; f.a = _v3; _v3 = n(_v1,_v2);

and then we apply the transformation

Expand assertions: -----------------

In order to deal with assertions on nodes, i.e., of the form

assert (n(i1,i2));

we first transform it into

assert_var = n(i1,i2); assert(assert_var);

where assert_var is a fresh bool local var, and we apply the transformation on the first equation.

val doit : Lic.node_key list -> LicPrg.t -> LicPrg.t

nb : it performs no fixpoint, so nested calls won't be expanded entirely unless L2lSplit.doit has been call before.

I could remove that restriction by adding a fixpoint somewhere, but is it worth bothering ?

the first arf is the list of node to not expand

OCaml

Innovation. Community. Security.