UnifyClock (p.lustre-v6.6.107.1.doc.lustre-v6.UnifyClock)

Module UnifyClockSource

Sub module of EvalClock that defines clock-checking utilities.

We have Two kind of substitutions.

subst1 is used to deal with the clock name binding, to relate node parameters and node arguments (to check clock equality up to alpha conversion).

subst2 is used to deal with polymorphic clock variables. Indeed, constant clock is intrinsically polymorphic. Hence, when clocking a contant (e.g., "42"), we return the clock_info Ci_var i, where i is a fresh integer. Afterwards, when encoutering an expression such as "42+x", where we know the clock of x (clk_x), we produce the substitution (i,clk_x).

XXX Shouldn't I merge the 2 kind of substitutions ? That would mean I need to invent a fake var_info_eff, but it would make the whole more homogeous.

XXX Make subst abstract?

Sourcetype subst1 = (Lv6Id.t * Lv6Id.t) list

Sourcetype subst2

Sourcetype subst = subst1 * subst2

Sourceval empty_subst : subst

Sourceval subst_to_string : subst -> string

Sourceval apply_subst : subst -> Lic.clock -> Lic.clock

Sourceval apply_subst2 : subst -> Lic.clock -> Lic.clock

Sourceval add_subst2 : int -> Lic.clock -> subst2 -> subst2

Sourceval add_link2 : int -> int -> subst2 -> subst2

Sourceval apply_subst_val_exp : subst -> Lic.val_exp -> Lic.val_exp

Sourceval f : subst -> Lxm.t -> Lic.clock -> Lic.clock -> subst

f lxm s clk_arg clk_par Raises a Compile_error is the 2 Lic.clock clk_arg and clk_par are not compatible. The accumulated substitution s is augmented with eventual clock variable instanciation.

For instance, when clock checking the expression 'toto(a,b)', if toto has the clock profile "alpha x alpha -> alpha", and the args 'a' and 'b' are on clock 'clk', the expression 'toto(a,b)' should be on clk too. We can check that later using the association "alpha->clk" is added in the returned substitution.

XXX UnifyClock.f is not a good name actually. CheckClock.f would better reflect the reality

Sourceval list : Lxm.t list -> Lic.clock list -> subst -> subst

Sourceval new_clock_var : subst -> subst * Lic.clock

Source

val const_to_val_eff : 
  Lxm.t ->
  bool ->
  subst ->
  Lic.const ->
  subst * Lic.val_exp

Transform a const into a val_exp const_to_val_eff lxm flag s const

flag tells if abstract const should be expanded
s is used to provide a clock to val_exp (actually, this is why this function is in this module, but it's a weird reason).