evalClock.mli

(** Time-stamp: <modified the 28/08/2008 (at 16:01) by Erwan Jahier> *)

open UnifyClock

(** [f ids ve] checks that [ve] is well-clocked (i.e., for node calls,
   it checks that the argument and the parameter clocks are compatible),
   and returns a clock profile that contains all the necessary information
   to be able to check.
*)
val f : Eff.id_solver -> subst -> Eff.val_exp -> Eff.clock list * subst


(** [check_res lxm cel cil] checks that the expected output clock
   profile of an expression "cil" is compatible with the result clocks
   "cel" of the expression.

   For instance, in order to clock check the equation 

      (x,y)=toto(a,b);

   it checks that the clock of "(x,y)" (cel) is compatible with the 
   output clock profile of node toto (cil).

   The type [Eff.clock_res] is exported to be able to call that
   function outside this module, which is necessary to clock
   equations (an equation is not an expression (i.e., not a
   Eff.val_exp).

*)

val check_res : Lxm.t -> subst -> Eff.left list -> Eff.clock list -> unit


(* Returns the clock of an expression. Note that this function uses
   an internal table, and therefore it should not be called before
   the clock checking has been done (by the function f above).*)
val get_val_exp_eff : Eff.val_exp -> Eff.clock list