getEff.mli

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


(** This module defines functions that translate SyntaxTreeCore datatypes into
    Eff ones. 

    Basically, it 

    - calls [EvalConst.f] wherever it is necessary, i.e., for items
    that are required to be static, such as arrays sizes, or array
    indexes.  
    - recursively calls itself for translating sub-terms
    - checks the arguments and the parameters are compatible (i.e., that they unify)
*)

val typ  : Eff.id_solver -> SyntaxTreeCore.type_exp  -> Eff.type_
val clock: Eff.id_solver -> SyntaxTreeCore.var_info -> Eff.clock

(**
   A [node_exp] is a name plus a list of static arguments.

   The goal of [node] is to 
   - compute the effective type of static arguments
   - check they are compatible with the node signature 
   check the type of the static arguments (
*)
val node : Eff.id_solver -> SyntaxTreeCore.node_exp Lxm.srcflagged -> 
  Eff.node_exp

val eq : Eff.id_solver -> SyntaxTreeCore.eq_info Lxm.srcflagged -> 
  Eff.eq_info Lxm.srcflagged

val assertion : Eff.id_solver -> SyntaxTreeCore.val_exp Lxm.srcflagged -> 
  Eff.val_exp Lxm.srcflagged


(** Useful to type check node aliased by array iterators *)
val translate_predef_static_args: 
  Eff.id_solver -> SyntaxTreeCore.static_arg Lxm.srcflagged list -> 
  Lxm.t -> Eff.static_arg list