lazyCompiler.ml

(** Time-stamp: <modified the 01/06/2011 (at 13:40) by Erwan Jahier> *)


open Lxm
open Errors
open SyntaxTree
open SyntaxTreeCore
open Eff

(** DEBUG FLAG POUR CE MODULE : *)
let dbg = Verbose.get_flag "lazyc"

let finish_me msg = print_string ("\n\tXXX LazyCompiler:"^msg^" ->  finish me!\n")

(******************************************************************************)
(** Returns the ident on which the recursion was detected, plus an execution
    stack description. 
*)
exception Recursion_error of (Ident.long as 'id) * (string list as 'stack)

exception BadCheckRef_error

let recursion_error (lxm : Lxm.t) (stack : string list) =
  let rec string_of_stack = function
    | [] -> "nostack" 
    | s::[] -> s
    | s::l  -> s^"\n   > "^(string_of_stack l)
  in
    raise ( Compile_error 
              (lxm, "Recursion loop detected: \n***   " ^(string_of_stack stack)
   ))


(******************************************************************************)
(* Structure principale *)
type t = {
  src_tab : SyntaxTab.t;
  (* table des defs *)
  types  : (Eff.item_key, Eff.type_    Eff.check_flag) Hashtbl.t;
  consts : (Eff.item_key, Eff.const    Eff.check_flag) Hashtbl.t;
  nodes  : (Eff.node_key, Eff.node_exp Eff.check_flag) Hashtbl.t;
  (* table des prov *)
  prov_types  : (Eff.item_key, Eff.type_    Eff.check_flag) Hashtbl.t;
  prov_consts : (Eff.item_key, Eff.const    Eff.check_flag) Hashtbl.t;
  prov_nodes  : (Eff.node_key, Eff.node_exp Eff.check_flag) Hashtbl.t
}

(******************************************************************************)
(* exported *)

let (create : SyntaxTab.t -> t) =
  fun tbl -> 
    let nodes_tbl =   Hashtbl.create 0 in
    let prov_nodes_tbl =   Hashtbl.create 0 in
      List.iter
        (fun op -> 
           let op_str = Predef.op2string op in
           let op_eff = PredefEvalType.make_node_exp_eff None op (Lxm.dummy op_str) [] in
           let op_key = Predef.op_to_long op, [] in
             Hashtbl.add nodes_tbl op_key (Eff.Checked op_eff);
             Hashtbl.add prov_nodes_tbl op_key (Eff.Checked op_eff)
        )
        Predef.iterable_op;
      {
        src_tab = tbl;
        types = Hashtbl.create 0;
        consts =  Hashtbl.create 0;
        nodes  = nodes_tbl;
        prov_types = Hashtbl.create 0;
        prov_consts =  Hashtbl.create 0;
        prov_nodes  = prov_nodes_tbl;
      } 

(******************************************************************************)

(** Type checking + constant checking/evaluation

   This is performed (lazily) by 10 mutually recursive functions:

   checking types 
   --------------
   (1) [type_check env type_name lxm]: type check the type id [type_name]
   (2) [type_check_do]: untabulated version of [type_check] (do the real work).

   (3) [type_check_interface]: ditto, but for the interface part
   (4) [type_check_interface_do]: untabulated version (do the real work)

   (5) [solve_type_idref] solves constant reference (w.r.t. short/long ident)

   checking constants 
   ------------------
   (6) [const_check env const_name lxm]: eval/check the constant [const_name]
   (7) [const_check_do] : untabulated version (do the real work)

   (8) [const_check_interface]: ditto, but for the interface part
   (9) [const_check_interface_do]: untabulated version (do the real work)

   (10) [solve_const_idref] solves constant reference (w.r.t. short/long ident)

   checking nodes 
   --------------

   (11) [node_check env node_name lxm]: check the node [node_name]
    checking a node means checking its interface and checking it equations/asserts.
    checking an equation means checking that the type and clock of the
    left part is the same as the ones of the rigth part.


   (12) [node_check_do] : untabulated version (do the real work)

   (13) [node_check_interface]: ditto, but for the interface part
   (14) [node_check_interface_do]: untabulated version (do the real work)

   (15) [solve_node_idref] solves constant reference (w.r.t. short/long ident)

    XXX checking clocks 
    -------------------
    Ditto, but todo!


    nb: for x in {type, const, node, clock}, there are several functions 
    that returns [x_eff]:
    - [x_check]
        o tabulates its result
        o takes an x_key and returns an [x_eff]
        o lookups its (syntaxic) definition (x_info) via the symbolTab.t
        o calls [GetEff.of_X] to translate its sub-terms

    - [GetEff.of_X]
        o takes a [x_exp] (i.e., an expression) and returns an [x_eff]
        o compute the effective static args (for nodes)
        o calls [solve_x_idref] (via [id_solver]) to translate its sub-terms


    - [solve_x_idref]
        o takes an idref (plus a Eff.static_arg list for x=node!)
        o perform name resolution
        o calls [x_check] (loop!)


    nb2: the top-level call is [node_check], on a node that necessarily contains
    no static parameters.  
  

*)

(* Before starting, let's define a few utilitary functions. *)

(** Intermediary results are put into a table. This tabulation handling
    is common to type and constant checking, and is performed by the
    2 following functions.

    Since [x] is meant to stand for [type], [const], or [node], those 2
    functions will lead to the definition of 6 functions:
    [type_check], [const_check], [node_check],
    [type_check_interface], [const_check_interface], [node_check_interface].
*)
let x_check 
    tab find_x x_check_do lookup_x_eff pack_of_x_key name_of_x_key this x_key lxm =
  try lookup_x_eff tab x_key lxm 
  with Not_found ->
    Hashtbl.add tab x_key Eff.Checking;
    let (x_pack,xn) = (pack_of_x_key x_key, name_of_x_key x_key) in
    let x_pack_symbols = SyntaxTab.pack_body_env this.src_tab x_pack in
    let x_def = match find_x x_pack_symbols xn lxm with
      | SymbolTab.Local x_def -> x_def
      | SymbolTab.Imported (lid,_) -> 
          print_string ("*** " ^ (Ident.string_of_long lid) ^ "???\n" ^ 
                          (Lxm.details lxm));
          assert false (* should not occur *)
    in
    let res = x_check_do this x_key lxm x_pack_symbols false x_pack x_def in
      Hashtbl.replace tab x_key (Eff.Checked res);
      res

let x_check_interface 
    tab find_x x_check x_check_interface_do lookup_x_eff 
    pack_of_x_key name_of_x_key this x_key lxm =
  try lookup_x_eff tab x_key lxm
  with Not_found ->
    Hashtbl.add tab x_key Eff.Checking;
    let (xp,xn) = (pack_of_x_key x_key, name_of_x_key x_key) in
    let xp_prov_symbols_opt = SyntaxTab.pack_prov_env this.src_tab xp lxm in
    let res = (* [xp] migth have no provided symbol table *)
      match xp_prov_symbols_opt with
        | None -> 
            (* if [xp] have no provided symbol table, the whole package is exported. *)
            x_check this x_key lxm 
        | Some xp_prov_symbols ->
            let x_def = match find_x xp_prov_symbols xn lxm with
              | SymbolTab.Local x -> x
              | SymbolTab.Imported _ -> assert false (* should not occur *)
            in
              x_check_interface_do this x_key lxm xp_prov_symbols xp x_def
    in
      Hashtbl.replace tab x_key (Eff.Checked res);
      res

(* Returns the tabulated [type] or [const], if it has already been computed;
   otherwise, raise [Not_found] otherwise. *)
let lookup_x_eff x_label id_of_x_key x_tab x_key lxm  =
    match Hashtbl.find x_tab x_key with
      | Eff.Checked res -> res
      | Eff.Checking -> 
          raise (Recursion_error (id_of_x_key x_key, [x_label^(Lxm.details lxm)]))
      | Eff.Incorrect -> raise (BadCheckRef_error)

let (lookup_type_eff: (Eff.item_key, Eff.type_ Eff.check_flag) Hashtbl.t -> 
      Ident.long -> Lxm.t -> Eff.type_) = 
  lookup_x_eff "type ref "  (fun k -> k)

let (lookup_const_eff:(Eff.item_key, Eff.const Eff.check_flag) Hashtbl.t -> 
      Ident.long -> Lxm.t -> Eff.const) = 
  lookup_x_eff "const ref " (fun k -> k)

let (lookup_node_exp_eff:
       (Eff.node_key, Eff.node_exp Eff.check_flag) Hashtbl.t -> 
      Eff.node_key -> Lxm.t -> Eff.node_exp) = 
  fun tbl key lxm -> 
    try 
      let node_exp = lookup_x_eff "node ref "  (fun k -> fst k) tbl key lxm in
      Verbose.printf ~flag:dbg
         "#DBG: LazyCompiler.lookup_node_exp_eff: FOUND node key '%s'\n"
            (LicDump.string_of_node_key_iter key)
      ; 
      node_exp
    with 
        Not_found -> 
          if fst (fst key) = "Lustre" then (
            let msg = (LicDump.string_of_node_key_iter key) ^ ": unknown Lustre operator. "^
              "\n*** Available operators in the current scope are:\n" ^
              (Hashtbl.fold (fun nk _ acc -> acc ^ 
                               ("\t - "^ (LicDump.string_of_node_key_iter nk) ^ "\n")) tbl "")
            in
              raise (Compile_error(lxm, msg))
          )
          else (
            Verbose.exe ~flag:dbg (
               fun () -> 
                  Printf.fprintf stderr "#DBG: LazyCompiler.lookup_node_exp_eff: node key '%s' NOT FOUND\n"
                      (LicDump.string_of_node_key_iter key);
                  flush stderr
            );
            raise Not_found
         )
(*   lookup_x_eff "node ref "  (fun k -> fst k) *)



(** This function performs the identifier (idref) resolution,
    i.e., when an ident is not explicitely prefixed by a module
    name, we decide here to which module it belongs. 

    The [provide_flag] indicates whether that function was called
    from a  provide  part or not.
*)
let solve_x_idref
    x_check_interface x_check find_x x_label to_x_key this symbols
    provide_flag currpack idr sargs lxm =
  let s = Ident.name_of_idref idr in
    match Ident.pack_of_idref idr with
      | Some p -> 
          if p = currpack 
          then x_check this (to_x_key currpack s) lxm
          else x_check_interface this (to_x_key p s) lxm
      | None ->
          (* no pack name: it must be in the symbols table *)
          try
            match (find_x symbols s lxm) with
              | SymbolTab.Local x_info ->
                  if provide_flag
                  then x_check_interface this (to_x_key currpack s) lxm
                  else x_check this (to_x_key currpack s) lxm

              | SymbolTab.Imported(fid,params) ->
                  let (pi,si) = (Ident.pack_of_long fid, Ident.of_long fid) in
                    assert(params=[]); (* todo *)
                    x_check_interface this (to_x_key pi si) lxm

          with Not_found ->
            (raise (Compile_error(lxm,"unbounded " ^ x_label ^ " ident")))




(******************************************************************************)

let find_var_info lxm vars id =
  try Hashtbl.find vars.vartable id
  with Not_found -> 
    raise (Compile_error (lxm,"\n*** Unknown ident: " ^ (Ident.to_string id)))




(* And now we can start the big mutually recursive definition... *)

(** Tabulated version of [type_check_do]. *)
let rec (type_check : t -> Ident.long -> Lxm.t -> Eff.type_) =
  fun this -> 
    x_check this.types SymbolTab.find_type type_check_do lookup_type_eff 
      Ident.pack_of_long Ident.of_long this

(** Tabulated version of [const_check_do]. *)
and (const_check : t -> Ident.long -> Lxm.t -> Eff.const) =
  fun this -> 
    x_check this.consts SymbolTab.find_const const_check_do lookup_const_eff 
      Ident.pack_of_long Ident.of_long this

(** Tabulated version of [type_check_interface_do]. *)
and (type_check_interface: t -> Ident.long -> Lxm.t -> Eff.type_) =
  fun this -> 
    x_check_interface 
      this.prov_types SymbolTab.find_type type_check type_check_interface_do 
      lookup_type_eff Ident.pack_of_long Ident.of_long this

(** Tabulated version of [const_check_interface_do]. *)
and (const_check_interface: t -> Ident.long -> Lxm.t -> Eff.const) =
  fun this -> 
    x_check_interface 
      this.prov_consts SymbolTab.find_const const_check const_check_interface_do
      lookup_const_eff Ident.pack_of_long Ident.of_long this

(** solving type and constant references *)
and (solve_type_idref : t -> SymbolTab.t -> bool -> Ident.pack_name -> 
      Ident.idref -> Lxm.t -> Eff.type_) =
  fun this symbols provide_flag currpack idr lxm -> 
    solve_x_idref
      type_check_interface type_check SymbolTab.find_type "type"
      (fun p id -> Ident.make_long p id)
      this symbols provide_flag currpack idr [] lxm
      
and (solve_const_idref : t -> SymbolTab.t -> bool -> Ident.pack_name -> 
      Ident.idref -> Lxm.t -> Eff.const) =
  fun this symbols provide_flag currpack idr lxm ->
    solve_x_idref
      const_check_interface const_check SymbolTab.find_const "const"
      (fun p id -> Ident.make_long p id)
      this symbols provide_flag currpack idr [] lxm


(* now the real work! *)
and (type_check_interface_do: t -> Ident.long -> Lxm.t -> SymbolTab.t ->
      Ident.pack_name -> SyntaxTreeCore.type_info srcflagged -> 
      Eff.type_) =
  fun this type_name lxm prov_symbols pack_name type_def ->
    (* We type check the interface and the body. 
       For non-abstract types, we also check that both effective types are
       the same.  *)
    let body_type_eff = type_check this type_name lxm in
    let prov_type_eff =
      type_check_do this type_name lxm prov_symbols true pack_name type_def
    in
      if Eff.type_are_compatible prov_type_eff body_type_eff then
        prov_type_eff
      else
        raise(Compile_error (
                type_def.src,
                ("provided type \n\t" ^ 
                   (Eff.string_of_type prov_type_eff) ^
                   "\n is not compatible with its implementation \n\t" ^ 
                   (Eff.string_of_type body_type_eff))))


and (const_check_interface_do: t -> Ident.long -> Lxm.t -> SymbolTab.t -> 
      Ident.pack_name -> SyntaxTreeCore.const_info srcflagged -> 
      Eff.const) =
  fun this cn lxm prov_symbols p const_def -> 
    let prov_const_eff = const_check_do this cn lxm prov_symbols true p const_def in
    let body_const_eff = const_check this cn lxm in
      match prov_const_eff, body_const_eff with
        | Eff.Extern_const_eff (_), _ -> assert false
        | Eff.Abstract_const_eff (id, teff, v, is_exported),
            Eff.Abstract_const_eff (body_id, body_teff, body_v, body_is_exported)
            ->
            assert false
              (* indeed, how can a body constant be extern and have a value? *)

        | Eff.Abstract_const_eff (id, teff, v, is_exported),
              Eff.Extern_const_eff (body_id, body_teff) 
              -> 
            if (id <> cn) then assert false
            else if not (Eff.type_are_compatible teff body_teff) then 
              raise(Compile_error (
                      const_def.src,
                      ("provided constant type \n***\t" ^ 
                         (Eff.string_of_type teff)  ^ 
                         "   is not compatible with its implementation \n***\t" ^ 
                         (Eff.string_of_type body_teff) ^ "")))
            else if 
              is_exported 
            then
              raise(Compile_error (const_def.src, " constant values mismatch"))
            else
              Eff.Extern_const_eff (body_id, body_teff)

        | Eff.Abstract_const_eff (id, teff, v, is_exported), _ -> 
            let body_teff = Eff.type_of_const body_const_eff in
              if (id <> cn) then assert false
              else if not (Eff.type_are_compatible teff body_teff) then 
                raise(Compile_error (
                        const_def.src,
                        ("provided constant type \n***\t" ^ 
                           (Eff.string_of_type teff)  ^ 
                           "   is not compatible with its implementation \n***\t" ^ 
                           (Eff.string_of_type body_teff) ^ "")))
              else 
                if is_exported && body_const_eff <> v then
                  raise(Compile_error (const_def.src, " constant values mismatch"))
                else
                  Eff.Abstract_const_eff (id, teff, body_const_eff, is_exported)
                    
        | Eff.Enum_const_eff (_, _), _
        | Eff.Bool_const_eff _, _
        | Eff.Int_const_eff _, _
        | Eff.Real_const_eff _, _
        | Eff.Struct_const_eff (_,_), _
        | Eff.Array_const_eff (_,_), _
            ->
            if prov_const_eff = body_const_eff then
              body_const_eff
            else
              raise(Compile_error (
                      const_def.src, 
                      "\n*** provided constant does not match with its definition."))
        | Eff.Tuple_const_eff _, _ ->
                                print_internal_error "LazyCompiler.const_check_interface_do" "should not have been called for a tuple";
                                assert false


and (type_check_do: t -> Ident.long -> Lxm.t -> SymbolTab.t -> bool -> 
      Ident.pack_name -> SyntaxTreeCore.type_info srcflagged -> 
      Eff.type_) =
  fun this type_name lxm symbols provide_flag pack_name type_def -> 
    try (
      (* Solveur d'idref pour les appels  eval_type/eval_const *)
      let id_solver = {
        id2var   = (fun idref lxm -> raise (Unknown_var(lxm,idref)) (* should not occur *)); 
        id2const = solve_const_idref this symbols provide_flag pack_name;
        id2type  = solve_type_idref this symbols provide_flag pack_name;
        id2node  = solve_node_idref this symbols provide_flag pack_name;
        symbols  = symbols;
      }
      in
      let type_eff = 
        match type_def.it with
          | ArrayType _ -> finish_me " array handling "; assert false
          | ExternalType s -> (
              let lid = Ident.make_long pack_name s in
              let idref = Ident.idref_of_long lid in
                try 
                  Abstract_type_eff (lid, id_solver.id2type idref lxm)
                with e ->
                  External_type_eff (lid)
            )
          | AliasedType (s, texp) -> GetEff.of_type id_solver texp
          | EnumType (s, clst) -> (
              let n = Ident.make_long pack_name s in
              let add_pack_name x = Ident.make_long pack_name x.it in
                Enum_type_eff (n, List.map add_pack_name clst)
            )
          | StructType sti -> (
              let make_field (fname : Ident.t) =
                let field_def = Hashtbl.find sti.st_ftable fname in
                let teff = GetEff.of_type id_solver field_def.it.fd_type in
                  match field_def.it.fd_value with
                    | None -> (fname, (teff, None))
                    | Some vexp -> (
                        let veff = EvalConst.f id_solver vexp in
                          match veff with
                            | [v] -> (
                                let tv = Eff.type_of_const v in
                                  if (tv = teff) then (fname, (teff, Some v)) else 
                                    raise 
                                      (Compile_error(field_def.src, Printf.sprintf
                                                       " this field is declared as '%s' but evaluated as '%s'"
                                                       (Eff.string_of_type teff)
                                                       (Eff.string_of_type tv)))
                              )
                            | [] -> assert false (* should not occur *)
                            | _::_ -> 
                                raise (Compile_error(field_def.src,
                                                     "bad field value: tuple not allowed"))
                      )
              in
              let n = Ident.make_long pack_name sti.st_name in
              let eff_fields = List.map make_field sti.st_flist in
                Struct_type_eff (n, eff_fields)
            )
      in
      let is_struct_or_array = match type_eff with 
        | Array_type_eff(_)
        | Struct_type_eff(_) -> true
        | Any | Overload | Bool_type_eff | Int_type_eff | Real_type_eff
        | External_type_eff(_) | Abstract_type_eff(_) | Enum_type_eff(_) 
            -> false
      in        
        if 
          (not provide_flag) 
          && (not (!Global.expand_structs & is_struct_or_array)) 
(*           && not !Global.ec (* ec does not need type decl at all *) *)
         then
         (* ICI IMPRESSION DE TYPE DECL OBSOLETE *)
         (* output_string !Global.oc (LicDump.type_decl type_name type_eff); *)
         ();
        type_eff
    )
    with
        (* capte et complete/stoppe les recursions *)
        Recursion_error (root, stack) ->
          if (root = type_name) then recursion_error type_def.src stack else
            raise ( Recursion_error (root, ("type ref "^(Lxm.details lxm))::stack))
              
              
and (const_check_do : t -> Ident.long -> Lxm.t -> SymbolTab.t -> bool -> 
      Ident.pack_name -> SyntaxTreeCore.const_info srcflagged -> 
      Eff.const) =
  fun this cn lxm symbols provide_flag currpack const_def ->
    (* [cn] and [lxm] are used for recursion errors. 
       [symbols] is the current symbol table.
    *)
    try (
      (* Solveur d'idref pour les  les appels  eval_type/eval_const *)
      let id_solver = {
        id2var   = (fun idref lxm -> assert false (* should not occur *)); 
        id2const = solve_const_idref this symbols provide_flag currpack;
        id2type  = solve_type_idref  this symbols provide_flag currpack;
        id2node  = solve_node_idref  this symbols provide_flag currpack;
        symbols  = symbols;
      }
      in
      let const_eff =
        match const_def.it with
          | ExternalConst (id, texp, val_opt) ->
              let lid = Ident.make_long currpack id in
              let teff = GetEff.of_type id_solver texp in
                if provide_flag then 
                  match val_opt with
                    | None  -> 
                        (* we put a fake value here as we don't know yet the 
                           concrete value. this will be filled in 
                           const_check_interface_do. I could have put an option
                           type, but that would make quite a lot of noise in the
                           remaining...
                        *) 
                        Abstract_const_eff(lid, teff, Int_const_eff (-666), false)
                    | Some c -> 
                        let ceff = match EvalConst.f id_solver c with
                          | [ceff] -> ceff
                          | _  -> assert false
                        in
                          Abstract_const_eff(lid, teff, ceff, true)

                else
                  (match val_opt with
                     | None  -> Extern_const_eff(lid, teff)
                     | Some c -> assert false
                         (* indeed, how can a body constant be extern and have a value? *)
                  )
          | EnumConst (id, texp) ->
              Enum_const_eff ((Ident.make_long currpack id), GetEff.of_type id_solver texp)

          | DefinedConst (id, texp_opt, vexp ) -> (
              match (EvalConst.f id_solver vexp) with
                | [ceff] -> (
                    match texp_opt with
                      | None -> ceff
                      | Some texp -> (
                          let tdecl = GetEff.of_type id_solver texp in
                          let teff =  Eff.type_of_const ceff in
                            if (tdecl = teff ) then ceff else 
                              raise 
                                (Compile_error (const_def.src, Printf.sprintf
                                                  " this constant is declared as '%s' but evaluated as '%s'"
                                                  (Eff.string_of_type tdecl)
                                                  (Eff.string_of_type teff)
                                               )))
                  )
                | [] -> assert false (* should not occur *)
                | _::_ -> raise (Compile_error(const_def.src, 
                                               "bad constant value: tuple not allowed"))
            )
      in
      let is_struct_or_array = match const_eff with 
        | Struct_const_eff _ -> true 
        | Array_const_eff  _ -> true 
        | _  -> false 
      in
      let is_extern_const = 
        match const_eff with 
          | Enum_const_eff(_) ->
              !Global.expand_enums (* When expanding enums, we treat them as extern const *)
              && not provide_flag (* Avoid to define them twice *)
          | Extern_const_eff(_) 
            -> true 
          | _ -> false
      in
        if 
          (not provide_flag 
           && (not (!Global.expand_structs & is_struct_or_array)) 
           && (not !Global.ec) (* ec does not need constant decl, except extern ones *)
          ) || is_extern_const
        then
          (* ICI IMPRESSION DE CONST DECL OBSOLETE *)
          (* output_string !Global.oc (LicDump.const_decl cn const_eff); *)
         ();
        const_eff
    ) with Recursion_error (root, stack) -> (
      (* capte et complete/stoppe les recursions *)
      if (root = cn) then recursion_error const_def.src stack else 
        (* on complete la stack *)
        raise (Recursion_error (root, ("const ref "^(Lxm.details lxm))::stack))
    )


(******************************************************************************)



and (node_check_interface_do: t -> Eff.node_key -> Lxm.t ->
      SymbolTab.t -> Ident.pack_name -> SyntaxTreeCore.node_info srcflagged ->
      Eff.node_exp) =
  fun this nk lxm symbols pn node_def ->
    (* DEUX checks :
       - le "complet" donne 'body_node_exp_eff' qui sera stock comme le vrai rsultat 
       - le "provide" donne 'prov_node_exp_eff', non stock, sert  vrifier la
         cohrence avec l'ventuelle dclaration 'provide' 
    *)
    let body_node_exp_eff = node_check this nk lxm in
    let prov_node_exp_eff = node_check_do this nk lxm symbols true pn node_def in
      (** [type_eff_are_compatible t1 t2] checks that t1 is compatible with t2, i.e., 
          if t1 = t2 or t1 is abstract and and t2.
      *)
    let msg_prefix = 
      ("provided node for " ^ (Ident.string_of_long (fst nk)) ^ 
         " is not compatible with its implementation: ")
    in
    let str_of_var = Eff.string_of_var_info in
    let type_is_not_comp v1 v2 = not (Eff.var_are_compatible v1 v2) in

    (* Checking the type profile (w.r.t the body and the provided part) *)
    let ibtypes = List.map (fun v -> v.var_type_eff) body_node_exp_eff.inlist_eff
    and iptypes = List.map (fun v -> v.var_type_eff) prov_node_exp_eff.inlist_eff 
    and obtypes = List.map (fun v -> v.var_type_eff) body_node_exp_eff.outlist_eff
    and optypes = List.map (fun v -> v.var_type_eff) prov_node_exp_eff.outlist_eff 
    in
    let topt = UnifyType.profile_is_compatible nk
      node_def.src (iptypes,ibtypes) (optypes,obtypes)
    in
(* OBSOLETE
    let _ =
      (* the type profile seems ok, but it may need to unfreeze some
         polymorphic nodes *)
      match topt with
        | None -> ()
        | Some t -> GetEff.dump_polymorphic_nodes t
    in
*)
      if
        prov_node_exp_eff.node_key_eff <> body_node_exp_eff.node_key_eff
      then
        raise(Compile_error (node_def.src, msg_prefix ^ " ??? "))
      else if
        (* ougth to be checked above: well, it eats no bread to keep that check *)
        (List.exists2 type_is_not_comp 
           prov_node_exp_eff.inlist_eff body_node_exp_eff.inlist_eff) 
      then
        let msg = msg_prefix ^ "bad input profile. \n*** " ^ 
          (String.concat "*" (List.map str_of_var prov_node_exp_eff.inlist_eff)) ^
          " <> " ^
          (String.concat "*" (List.map str_of_var body_node_exp_eff.inlist_eff))
        in
          raise(Compile_error (node_def.src, msg))
      else if 
        (List.exists2 type_is_not_comp
           prov_node_exp_eff.outlist_eff body_node_exp_eff.outlist_eff) 
          (* ougth to be checked above: well, it eats no bread to keep that check *)
      then
        let msg = msg_prefix ^ "bad output profile. \n*** " ^ 
          (String.concat "*" (List.map str_of_var prov_node_exp_eff.outlist_eff)) ^
          " <> " ^
          (String.concat "*" (List.map str_of_var body_node_exp_eff.outlist_eff))
        in
          raise(Compile_error (node_def.src, msg))
      else if     
        prov_node_exp_eff.has_mem_eff <> body_node_exp_eff.has_mem_eff 
      then
        raise(Compile_error (node_def.src, msg_prefix ^ " node or function?"))
      else if 
        prov_node_exp_eff.is_safe_eff <> body_node_exp_eff.is_safe_eff
      then
        raise(Compile_error (node_def.src, msg_prefix ^ "safe or unsafe?"))
      else if 
        match prov_node_exp_eff.def_eff, body_node_exp_eff.def_eff with
          | (AbstractEff _,_) -> false
          | (_,_) -> prov_node_exp_eff.def_eff <> body_node_exp_eff.def_eff
      then
        raise(Compile_error (node_def.src, msg_prefix ^ "abstract or not?"))
      else
        match prov_node_exp_eff.def_eff, body_node_exp_eff.def_eff with
          | AbstractEff None, BodyEff  node_body -> 
              { prov_node_exp_eff with def_eff = AbstractEff (Some body_node_exp_eff) }
          | _,_ -> 
              prov_node_exp_eff

(* 
LE GROS DU BOULOT 
- suivant "provide_flag" : check d'interface (provide) ou le check de la dfinition
  (n.b. provide_flag influence la rsolution des idents dans l'env local de check)
*)
and node_check_do
   (this: t)
   (nk: Eff.node_key)
   (lxm: Lxm.t)
   (symbols: SymbolTab.t)
   (provide_flag: bool)
   (pack_name: Ident.pack_name)
   (node_def: SyntaxTreeCore.node_info srcflagged)
      : Eff.node_exp =
(* START node_check_do *)
(
    Verbose.printf ~flag:dbg
       "#DBG: LazyCompiler.node_check_do '%s' (%s)\n"
          (LicDump.string_of_node_key_iter nk)
          (Lxm.details lxm)
    ; 
    let lxm = node_def.src in
    (* Creates a local_env with just the global bindings,
       local bindinds will be added later (side effect)
    *)
    let local_env = make_local_env nk in
    let _ =
      Verbose.exe ~level:3
        ( fun () -> 
            Printf.printf "*** local_env while entering (node_check_do %s):\n" 
              (LicDump.string_of_node_key_rec nk);
            LicDump.dump_local_env local_env;
            flush stdout
        )
    in
    let node_id_solver = {
      (* a [node_id_solver] is a [id_solver] where we begin to look
         into the local environement before looking at the global
         one.  *)
      id2var = (* var can only be local to the node *)
        (fun id lxm ->
           try lookup_var local_env (Ident.of_idref id) lxm
           with Not_found ->
             raise (Unknown_var(lxm,id))
        );
      id2const =
        (fun id lxm ->
           try lookup_const local_env id lxm
           with Not_found ->
             solve_const_idref this symbols provide_flag pack_name id lxm
                        );
      id2type  =
        (fun id lxm ->
           try lookup_type local_env id lxm
           with Not_found ->
             Verbose.exe ~level:3 (
               fun () ->
                 Printf.printf "*** Dont find type %s in local_env\n" (Ident.string_of_idref id);
                 Printf.printf "*** local_env.lenv_types contain def for: ";
                 Hashtbl.iter 
                   (fun id t -> 
                      Printf.printf "%s, " (Ident.to_string id) )
                   local_env.lenv_types;
                 Printf.printf "\n";
                 flush stdout);
             solve_type_idref  this symbols provide_flag pack_name id lxm);
      id2node  =
        (fun id sargs lxm ->
           (try
              let (node_id,sargs), inlist, outlist = lookup_node local_env  id sargs lxm in
              let node_id = Ident.idref_of_long node_id in
                solve_node_idref this symbols provide_flag pack_name node_id sargs lxm
                  (*                node_check this (node_id,[]) lxm   *)

            with 
                Not_found -> 
                  solve_node_idref this symbols provide_flag pack_name id sargs lxm
              | _ -> assert false)
        );

      symbols  = symbols;
    }
    in
    let make_node_eff id node_def_eff = (
      (* building not aliased nodes *)
      Verbose.exe ~level:3 
        ( fun () -> 
            Printf.printf "*** local_env while entering (make_node_eff %s):\n" (Ident.to_string id);
            LicDump.dump_local_env local_env
        );
      (********************************************************)
      (* LOCAL CONSTANTS are evaluated and added to local_env *)
      (********************************************************)
      (* init intermediate table *)
      let sz = List.length node_def.it.loc_consts in
      let temp_const_eff_tab : (Ident.long, Eff.const Eff.check_flag) Hashtbl.t =
        Hashtbl.create sz
      in
      let temp_const_def_tab :
          (Ident.t,(Lxm.t * SyntaxTreeCore.type_exp option * SyntaxTreeCore.val_exp)) Hashtbl.t =
        Hashtbl.create sz
      in
      let init_local_const (lxm, cinfo) = (
        match cinfo with
          | DefinedConst (i,topt,ve) -> (
              Verbose.printf ~level:3 " * local const %s will be treated\n" i;
              Hashtbl.add temp_const_def_tab i (lxm,topt,ve)
            )
          | ExternalConst _ 
          | EnumConst _ -> (
              let msg = "*** abstract constant bot allowed within node "
              in
                raise (Compile_error(lxm, msg))
            )
      ) in
        List.iter init_local_const node_def.it.loc_consts ;
        (* differs from node_id_solver only on id2const *)
        let rec local_id_solver = {
          id2var   = node_id_solver.id2var;
          id2const = local_id2const;
          id2type  = node_id_solver.id2type;
          id2node  = node_id_solver.id2node;
          symbols  = node_id_solver.symbols;
        }
        and treat_local_const id = (
          Verbose.printf ~level:3 " * call treat_local_const %s\n" id;
          let id_key = ("", id) in
            try (
              let ce = lookup_const_eff temp_const_eff_tab id_key lxm in
                Verbose.printf ~level:3 " * const %s already treated = %s\n" 
                  id (LicDump.string_of_const_eff ce);
                ce
            ) with Not_found -> (
              let (lxmdef, toptdef, vedef) = Hashtbl.find temp_const_def_tab id in
                Verbose.printf ~level:3 " * const %s not yet treated ...\n" id ;
                (* yes, not yet checked *) 
                Hashtbl.add temp_const_eff_tab id_key Checking ;
                (* computes the value with EvalConst.f id_solver ve ... *)
                let ce = match (EvalConst.f local_id_solver vedef) with
                  | [ceff] -> (
                      match toptdef with
                        | None -> ceff
                        | Some texp -> (
                            let tdecl = GetEff.of_type local_id_solver texp in
                            let teff =  Eff.type_of_const ceff in
                              if (tdecl = teff ) then ceff else 
                                raise (Compile_error (
                                         lxmdef, Printf.sprintf
                                           " this constant is declared as '%s' but evaluated as '%s'"
                                           (Eff.string_of_type tdecl)
                                           (Eff.string_of_type teff)
                                       )))
                    )
                  | [] -> assert false (* should not occur *)
                  | _::_ -> raise (Compile_error(lxmdef, "bad constant value: tuple not allowed"))
                in
                  Verbose.printf ~level:3 " * const %s evaluated to %s\n"
                    id (LicDump.string_of_const_eff ce);
                  Hashtbl.replace temp_const_eff_tab id_key (Checked ce) ;
                  ce
            )
        )
        and local_id2const idrf lxm = (
          (* is id a local const ? *)
          try (
            (* certainly NOT if id has a pack *)
            let id = if (Ident.pack_of_idref idrf = None)
            then Ident.name_of_idref idrf
            else raise Not_found
            in
            let ce = treat_local_const id in
              ce
          ) with Not_found -> (
            (* not a local constant -> search in global env *)
            Verbose.printf ~level:3 " * %s not a local const, should be global ?" (Ident.string_of_idref idrf);
            let ce = node_id_solver.id2const idrf lxm in
              Verbose.printf ~level:3 " YES -> %s\n" (LicDump.string_of_const_eff ce);
              ce
          )
        ) in
          (* iters local_id2const n eeach declared constant *)
          Hashtbl.iter (fun id _ -> let _ = treat_local_const id in ()) temp_const_def_tab ;
          (* Finally, adds each local const to ICI *)
          let add_local_const idref ceck = (
            Verbose.printf ~level:3 " * add_local_const %s = %s\n"
              (snd idref)
              (match ceck with
                 | Checking -> "Checking"
                 | Checked ce -> (LicDump.string_of_const_eff ce)
                 | Incorrect -> "Incorrect"
              );
            match ceck with
              | Checked ce -> Hashtbl.add local_env.lenv_const (snd idref) ce
              | _ -> assert false
          ) in
            Hashtbl.iter add_local_const temp_const_eff_tab ;
            
            (********************************************************)
            (* LOCAL FLOWS are added to local_env                   *)
            (********************************************************)
            (* (i.e. ins,outs,locs) *)
            match node_def.it.vars with
        | None -> assert false (* a node with a body should have a profile *)
        | Some vars ->
            let is_polymorphic = ref false in
            let type_args id =
              let vi = find_var_info lxm vars id in
              let t_eff = GetEff.of_type node_id_solver vi.it.var_type in
              let _ = if Eff.is_polymorphic t_eff then is_polymorphic := true in
              let c_eff = GetEff.of_clock node_id_solver vi.it in
              let vi_eff = {
                var_name_eff   = vi.it.var_name;
                var_nature_eff = vi.it.var_nature;
                var_number_eff = vi.it.var_number;
                var_type_eff  = t_eff;
                var_clock_eff = c_eff;
              }
              in
                Hashtbl.add local_env.lenv_types id t_eff;
                Hashtbl.add local_env.lenv_vars id vi_eff;
                vi_eff
            in
            let (sort_vars : Ident.t list -> Ident.t list) =
              fun l -> 
                (* I cannot use List.sort as I only have a partial order on vars
                   -> hence I perform a topological sort *)
                let rec depends_on v1 v2 =
                  match (find_var_info lxm vars v1).it.var_clock with
                    | Base -> false
                    | NamedClock({it=(_,v1clk)}) -> v1clk = v2 || depends_on v1clk v2
                in
                let rec aux acc l = match l with
                  | [] -> acc
                  | v::tail -> (
                      match (find_var_info lxm vars v).it.var_clock with
                        | Base -> 
                            if List.mem v acc then 
                              aux acc tail 
                            else
                              aux (v::acc) tail
                        | NamedClock( { it=(_,v2) ; src=lxm }) ->
                            if List.mem v2 acc then
                              aux (v::acc) tail
                            else if
                              depends_on v2 v
                            then
                              raise (
                                Compile_error (
                                  lxm, 
                                  "\n*** Clock dependency loop: " ^ 
                                    (Ident.to_string v) ^ " depends on " ^
                                    (Ident.to_string v2) ^ ", which depends on " ^
                                    (Ident.to_string v))
                              )
                            else
                              let l1,l2 = List.partition (fun v -> v=v2) l in
                                if l1 = [] then
                                  (* v depends on a clock not in l *)
                                  aux (v::acc) tail 
                                else
                                  aux acc (v2::l2)
                    )
                in
                  List.rev(aux [] l)
            in
            let vars_in_sorted  = sort_vars vars.inlist
            and vars_out_sorted = sort_vars vars.outlist in
            let inlist  = List.map type_args vars_in_sorted
            and outlist = List.map type_args vars_out_sorted
            and loclist = 
              match vars.loclist with
                | None -> None
                | Some loclist -> 
                    let vars_loc_sorted = sort_vars loclist in
                      Some (List.map type_args vars_loc_sorted)
            in
            let unsort l_id l_vi =
              let tab = List.map (fun vi -> vi.var_name_eff, vi) l_vi in
                try List.map (fun id -> List.assoc id tab) l_id
                with Not_found -> assert false
            in
            let inlist2 = unsort vars.inlist inlist
            and outlist2 = unsort vars.outlist outlist in
              {
                node_key_eff = nk;
                inlist_eff   = inlist2;
                outlist_eff  = outlist2;
                loclist_eff  = loclist;
                def_eff = node_def_eff ();
                has_mem_eff  = node_def.it.has_mem;
                is_safe_eff  = node_def.it.is_safe;
                is_polym_eff = !is_polymorphic
              }
    ) in
      (* let's go *)