unifyClock.mli

(** Time-stamp: <modified the 19/05/2009 (at 17:32) by Erwan Jahier> *)


(* XXX use Map.t 

   We have Two kind of substitutions. 

   - One is used to deal with the clock name binding, to relate node
   parameters and node arguments.

   - The other one 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 it abstract?
*)

type subst1 = (Ident.t * Ident.t) list
type subst2

type subst = subst1 * subst2
(* = (Ident.t * Ident.t) list  * (int * Eff.clock) list *)

val empty_subst : subst


val apply_subst:subst -> Eff.clock -> Eff.clock

(* only apply the part of the subst that deals with clock var *)
val apply_subst2:subst -> Eff.clock -> Eff.clock
val add_subst2 : int -> Eff.clock -> subst2 -> subst2
val add_link2 : int -> int -> subst2 -> subst2

val apply_subst_val_exp : subst -> Eff.val_exp -> Eff.val_exp

(** Raises a Compile_error is the 2 Eff.clock are not unifiable *)
val f : Lxm.t -> subst -> Eff.clock -> Eff.clock -> subst
val list : Lxm.t -> Eff.clock list -> subst -> Eff.clock * subst

val new_clock_var : subst -> subst * Eff.clock

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