CristalCaveGem » LustreC

let pp_emf_spec_mode fmt m =

  fprintf fmt "{@[";

  fprintf fmt "\"mode_id\": \"%s\",@ "

    m.mode_id;

  fprintf fmt "\"require\": [%a],@ "

    pp_emf_eexprs m.ensure;

  fprintf fmt "\"require\": [%a],@ "

    pp_emf_eexprs m.require;

  fprintf fmt "@]}"

let pp_emf_spec_modes = pp_emf_list pp_emf_spec_mode

let pp_emf_spec_import fmt i =

  fprintf fmt "{@[";

  fprintf fmt "\"contract\": \"%s\",@ "

    i.import_nodeid;

  fprintf fmt "\"inputs\": [%a],@ "

    pp_emf_exprs i.inputs;

  fprintf fmt "\"outputs\": [%a],@ "

    pp_emf_exprs i.outputs;

  fprintf fmt "@]}"

let pp_emf_spec_imports = pp_emf_list pp_emf_spec_import

let pp_emf_spec fmt spec =

  fprintf fmt "{ @[<hov 0>";

  fprintf fmt "\"consts\": [%a],@ "

    pp_emf_consts spec.consts;

  fprintf fmt "\"locals\": [%a],@ "

    pp_emf_vars_decl spec.locals;

  fprintf fmt "\"stmts\": [%a],@ "

    pp_emf_stmts spec.stmts;

  fprintf fmt "\"assume\": [%a],@ "

    pp_emf_eexprs spec.assume;

  fprintf fmt "\"guarantees\": [%a],@ "

    pp_emf_eexprs spec.guarantees;

  fprintf fmt "\"modes\": [%a],@ "

    pp_emf_spec_modes spec.modes;

  fprintf fmt "\"imports\": [%a]@ "

    pp_emf_spec_imports spec.imports;  

  fprintf fmt "@] }"

      print_protect (fun fmt -> pp_print_string fmt m.mname.node_id);

    fprintf fmt "\"imported\": \"false\",@ ";

    (match m.mspec with None -> () | Some spec -> fprintf fmt "\"spec\": %a,@ " pp_emf_spec spec);

let pp_emf_imported_node fmt top =

  let ind = Corelang.imported_node_of_top top in

   try

    fprintf fmt "@[<v 2>\"%a\": {@ "

      print_protect (fun fmt -> pp_print_string fmt ind.nodei_id);

    fprintf fmt "\"imported\": \"true\",@ ";

    fprintf fmt "\"inputs\": [%a],@ "

      pp_emf_vars_decl ind.nodei_inputs;

    fprintf fmt "\"outputs\": [%a],@ "

      pp_emf_vars_decl ind.nodei_outputs;

    fprintf fmt "\"original_name\": \"%s\",@ " ind.nodei_id;

    (match ind.nodei_spec with None -> () | Some spec -> fprintf fmt "\"spec\": %a" pp_emf_spec spec);

    fprintf fmt "@]@ }"

  with Unhandled msg -> (

    eprintf "[Error] @[<v 0>EMF backend@ Issues while translating node %s@ "

      ind.nodei_id;

    eprintf "%s@ " msg;

    eprintf "node skipped - no output generated@ @]@."

  )

  (* record_types prog; *)

  (* Typedef *)

  fprintf fmt "\"typedef\": [@[<v 0>%a@]],@ "

    (pp_emf_list pp_emf_typedef) (Corelang.get_typedefs prog);

  fprintf fmt "\"consts\": [@[<v 0>%a@]],@ "

    (pp_emf_list pp_emf_top_const) (Corelang.get_consts prog);

  fprintf fmt "\"imported_nodes\": @[<v 0>{@ ";

  pp_emf_list pp_emf_imported_node fmt (Corelang.get_imported_nodes prog);

  fprintf fmt "}@],@ ";

  pp_emf_list pp_machine fmt (List.rev machines);

let rec pp_emf_dim fmt dim_expr =

  fprintf fmt "{";

  (let open Dimension in

   match dim_expr.dim_desc with

   | Dbool b -> fprintf fmt "\"kind\": \"bool\",@ \"value\": \"%b\"" b

   | Dint i -> fprintf fmt "\"kind\": \"int\",@ \"value\": \"%i\"" i

   | Dident s -> fprintf fmt "\"kind\": \"ident\",@ \"value\": \"%s\"" s

   | Dappl(f, args) -> fprintf fmt "\"kind\": \"fun\",@ \"id\": \"%s\",@ \"args\": [@[%a@]]"

                         f (Utils.fprintf_list ~sep:",@ " pp_emf_dim) args 

   | Dite(i,t,e) -> fprintf fmt "\"kind\": \"ite\",@ \"guard\": \"%a\",@ \"then\": %a,@ \"else\": %a"

                      pp_emf_dim i pp_emf_dim t pp_emf_dim e 

   | Dlink e -> pp_emf_dim fmt e

   | Dvar

   | Dunivar -> assert false (* unresolved *)

  );

  fprintf fmt "}"

(* First try to print the declared one *)

  | Tydec_any -> (* Dynamical built variable. No declared type. Shall

                    use the infered one. *)

     pp_infered_type fmt infered_t

  | Tydec_int -> fprintf fmt "{ \"kind\": \"int\" }" (* !Options.int_type *)

  | Tydec_real -> fprintf fmt "{ \"kind\": \"real\" }" (* !Options.real_type *)

  | Tydec_bool -> fprintf fmt "{ \"kind\": \"bool\" }"

    (* This is an alias type *)

    (* id for a enumerated type, eg. introduced by automata *)

    (* Print the type name associated to this enumerated type. This is

       basically an integer *)

    pp_tag_type id typ infered_t fmt

  )

  | Tydec_struct _ | Tydec_enum _ ->

     assert false (* should not happen. These type are only built when

                     declaring a type in the prefix of the lustre

                     file. They shall not be associated to variables

                   *)

  | Tydec_array (dim, e) -> (

    let inf_base = match infered_t.Typing.tdesc with

      | Typing.Tarray(_,t) -> t

      | _ ->   (* returing something useless, hoping that the concrete

                  datatype will return something usefull *)

         Typing.new_var ()

    in

    fprintf fmt "{ \"kind\": \"array\", \"base_type\": %t, \"dim\": %a }"

      (pp_concrete_type e inf_base)

      pp_emf_dim dim

(* | _ -> eprintf

 *          "unhandled construct in type printing for EMF backend: %a@."

 *          Printers.pp_var_type_dec_desc dec_t; raise (Failure "var") *)

and pp_tag_type id typ inf fmt =

  (* We ought to represent these types as values: enum will become int, we keep the name for structs *)

  let rec aux tydec_desc =

    match tydec_desc with  

    | Tydec_int 

      | Tydec_real 

      | Tydec_bool

      | Tydec_array _ -> pp_concrete_type tydec_desc inf fmt

    | Tydec_const id ->

       (* Alias of an alias: unrolling definitions *)

       let typ = (Corelang.typedef_of_top

                    (Hashtbl.find Corelang.type_table tydec_desc))

       in

       pp_tag_type id typ inf fmt

    | Tydec_clock ty -> aux ty

    | Tydec_enum const_list -> ( (* enum can be mapped to int *)

      let size = List.length const_list in

      fprintf fmt "{ \"name\": \"%s\", \"kind\": \"enum\", \"size\": \"%i\" }" id size

    )

    | Tydec_struct _ ->

       fprintf fmt "{ \"name\": \"%s\", \"kind\": \"struct\" }" id

    | Tydec_any -> (* shall not happen: a declared type cannot be

                      bound to type any *)

       assert false

  in

  aux typ.tydef_desc

and pp_infered_type fmt t =

  (* Shall only be used for variable types that were not properly declared. Ie generated at compile time. *)

  let open Types in

  if is_bool_type t  then fprintf fmt "bool" else

    if is_int_type t then fprintf fmt "int" else (* !Options.int_type *)

      if is_real_type t then fprintf fmt "real" else (* !Options.real_type *)

        match t.tdesc with

        | Tclock t ->

           pp_infered_type fmt t

        | Tstatic (_, t) ->

           fprintf fmt "%a" pp_infered_type t

        | Tconst id ->

           (* This is a type id for a enumerated type, eg. introduced by automata *)

           let typ =

             (Corelang.typedef_of_top

                (Hashtbl.find Corelang.type_table (Tydec_const id)))

           in

           pp_tag_type id typ t fmt

        | Tlink ty -> 

           pp_infered_type fmt ty 

        | _ -> eprintf "unhandled type: %a@." Types.print_node_ty t; assert false

(* Provide both the declared type and the infered one. *)

  with Failure msg -> eprintf "failed var: %a@.%s@." Printers.pp_var v msg; assert false

let pp_emf_list ?(eol:('a, formatter, unit) Pervasives.format="") pp fmt l =

  match l with

    [] -> ()

  | _ -> fprintf fmt "@[";

         Utils.fprintf_list ~sep:",@ " pp fmt l;

         fprintf fmt "@]%(%)" eol

(* Print the variable declaration *)

let pp_emf_vars_decl = pp_emf_list pp_emf_var_decl

let pp_cst_type c inf fmt (*infered_typ*) =

  match c with

  | Const_tag t ->

     let typ = (Corelang.typedef_of_top (Hashtbl.find Corelang.tag_table t)) in

     if typ.tydef_id = "bool" then

       fprintf fmt "bool"

     else

       pp_tag_type t typ inf fmt

  | Const_int _ -> fprintf fmt "int" (*!Options.int_type*)

  | Const_real _ -> fprintf fmt "real" (*!Options.real_type*)

  | Const_string _ -> fprintf fmt "string" 

  | _ -> eprintf "cst: %a@." Printers.pp_const c; assert false

let pp_emf_cst c inf fmt =

  let pp_typ fmt =

    fprintf fmt "\"datatype\": \"";

    pp_cst_type c inf fmt;

    fprintf fmt "\"@ "

  in

       pp_typ fmt;

       pp_typ fmt;

     fprintf fmt "{@[\"type\": \"constant\",@ \"value\": \"%s\",@ " s;

     pp_typ fmt;

     fprintf fmt "@]}"

    pp_typ fmt;

(* Print a value: either a constant or a variable value *)

  | Cst c -> pp_emf_cst c v.value_type fmt 

  | Expr_const c -> pp_emf_cst c e.expr_type fmt 

 (* Missing these 

  | Expr_ite   of expr * expr * expr

  | Expr_arrow of expr * expr

  | Expr_fby of expr * expr

  | Expr_array of expr list

  | Expr_access of expr * Dimension.dim_expr

  | Expr_power of expr * Dimension.dim_expr

  | Expr_pre of expr

  | Expr_when of expr * ident * label

  | Expr_merge of ident * (label * expr) list

  | Expr_appl of call_t

  *)

let pp_emf_exprs = pp_emf_list pp_emf_expr

let pp_emf_const fmt v =

  fprintf fmt "@[{\"name\": \"%a\", \"datatype\":\"%a\", \"original_name\": \"%a\", \"value\": \"%a\"}@]"

    pp_var_name v

    pp_var_type v

    Printers.pp_var_name v

    pp_emf_expr (match v.var_dec_value with None -> assert false | Some e -> e)

let pp_emf_consts = pp_emf_list pp_emf_const

let pp_emf_eexprs = pp_emf_list pp_emf_eexpr

(*

                      TODO Thanksgiving

                      trouver un moyen de transformer en machine code les instructions de chaque spec

                      peut etre associer a chaque imported node une minimachine

                      et rajouter un champ a spec dans machine code pour stoquer memoire et instr

 *)                

let pp_emf_stmt fmt stmt =

  match stmt with

  | Aut _ -> assert false

  | Eq eq -> (

    fprintf fmt "@[ @[<v 2>\"%a\": {@ " (Utils.fprintf_list ~sep:"_" pp_print_string) eq.eq_lhs;

    fprintf fmt "\"lhs\": [%a],@ " (Utils.fprintf_list ~sep:", " (fun fmt vid -> fprintf fmt "\"%s\"" vid)) eq.eq_lhs;

    fprintf fmt "\"rhs\": \"%a\",@ " pp_emf_expr eq.eq_rhs;

    fprintf fmt "@]@]@ }"

  )

let pp_emf_stmts = pp_emf_list pp_emf_stmt 

(* Printing the type declaration, not its use *)

let rec pp_emf_typ_dec fmt tydef_dec =

  fprintf fmt "{";

  (match tydef_dec with

   | Tydec_any -> fprintf fmt "\"kind\": \"any\""

   | Tydec_int -> fprintf fmt "\"kind\": \"int\""

   | Tydec_real -> fprintf fmt "\"kind\": \"real\""

   | Tydec_bool-> fprintf fmt "\"kind\": \"bool\""

   | Tydec_clock ck -> pp_emf_typ_dec fmt ck

   | Tydec_const c -> fprintf fmt "\"kind\": \"alias\",@ \"value\": \"%s\"" c

   | Tydec_enum el -> fprintf fmt "\"kind\": \"enum\",@ \"elements\": [%a]"

                        (Utils.fprintf_list ~sep:", " (fun fmt e -> fprintf fmt "\"%s\"" e)) el

   | Tydec_struct s -> fprintf fmt "\"kind\": \"struct\",@ \"fields\": [%a]"

                         (Utils.fprintf_list ~sep:", " (fun fmt (id,typ) ->

                              fprintf fmt "\"%s\": %a" id pp_emf_typ_dec typ)) s

   | Tydec_array (dim, typ) -> fprintf fmt "\"kind\": \"array\",@ \"dim\": @[%a@],@ \"base\": %a"

                               pp_emf_dim dim

                               pp_emf_typ_dec typ

  );

  fprintf fmt "}"

let pp_emf_typedef fmt typdef_top =

  let typedef = Corelang.typedef_of_top typdef_top in

  fprintf fmt "\"%s\": @[%a@]" typedef.tydef_id pp_emf_typ_dec typedef.tydef_desc 

let pp_emf_top_const fmt const_top = 

  let const = Corelang.const_of_top const_top in

  fprintf fmt "\"%s\": " const.const_id;

  pp_emf_cst const.const_value const.const_type fmt

val get_var: ident -> var_decl list -> var_decl

     (* mutable eexpr_normalized: (var_decl * eq list * var_decl list) option; *)

(* translate_<foo> : vars -> context -> <foo> -> machine code/expression *)

let translate_ident vars _ (* (m, si, j, d, s) *) id =

  try (* id is a var that shall be visible here , ie. in vars *)

    let var_id = get_var id vars in

      let vdecl = (Corelang.var_decl_of_const

                     (const_of_top (Hashtbl.find Corelang.consts_table id)))

      in

      (* DONE construire une liste des enum declarés et alors chercher

         dedans la liste qui contient id *)

      with Not_found -> (Format.eprintf

                           "internal error: Machine_code.translate_ident %s"

                           id;

let rec control_on_clock vars ((m, si, j, d, s) as args) ck inst =

   control_on_clock vars args ck1 (mkinstr

				     (MBranch (translate_ident vars args id,

let rec translate_expr vars ((m, si, j, d, s) as args) expr =

  (* all calls are using the same arguments (vars for the variable

     enviroment and args for computed memories). No fold constructs

     here. We can do partial evaluation of translate_expr *)

  let translate_expr = translate_expr vars args in 

    | Expr_ident x                     -> (translate_ident vars args x).value_desc

    | Expr_array el                    -> Array (List.map translate_expr el)

    | Expr_access (t, i)               -> Access (translate_expr t,

                                                  translate_expr 

                                                    (expr_of_dimension i))

    | Expr_power  (e, n)               -> Power  (translate_expr e,

                                                  translate_expr

                                                    (expr_of_dimension n))

      | Expr_arrow _ 

      | Expr_fby _

      | Expr_pre _                       -> (Printers.pp_expr

                                               Format.err_formatter expr;

                                             Format.pp_print_flush

                                               Format.err_formatter ();

                                             raise NormalizationError)

    | Expr_when    (e1, _, _)          -> (translate_expr e1).value_desc

       let nd = node_from_name id in

       Fun (node_name nd, List.map translate_expr (expr_list_of_expr e))

	 Fun ("ite", [translate_expr g; translate_expr t; translate_expr e])

let translate_guard vars args expr =

  | Expr_ident x  -> translate_ident vars args x

  | _ -> (Format.eprintf "internal error: translate_guard %a@."

            Printers.pp_expr expr;

          assert false)

let rec translate_act vars ((m, si, j, d, s) as args) (y, expr) =

  let translate_act = translate_act vars args in

  let translate_guard = translate_guard vars args in

  let translate_ident = translate_ident vars args in

  let translate_expr = translate_expr vars args in

  | Expr_ite   (c, t, e) -> let g = translate_guard c in

                              [translate_act (y, t)]

                              [translate_act (y, e)]

  | Expr_merge (x, hl)   -> mkinstr ?lustre_eq:(Some eq)

                              (MBranch (translate_ident x,

                                        List.map (fun (t,  h) ->

                                            t, [translate_act (y, h)])

                                          hl))

  | _                    -> mkinstr ?lustre_eq:(Some eq)

                              (MLocalAssign (y, translate_expr expr))

let reset_instance vars args i r c =

  | Some r      -> let g = translate_guard vars args r in

                   [control_on_clock

                      vars

                      args

                      c

                      (mk_conditional

                         g

                         [mkinstr (MReset i)]

                         [mkinstr (MNoReset i)])

                   ]

let translate_eq vars ((m, si, j, d, s) as args) eq =

  let translate_expr = translate_expr vars args in

  let translate_act = translate_act vars args in

  let control_on_clock = control_on_clock vars args in

  let reset_instance = reset_instance vars args in

  (* Format.eprintf "translate_eq %a with clock %a@." 

     Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock;  *)

     let var_x = get_var x vars in

     let o = new_instance Arrow.arrow_top_decl eq.eq_rhs.expr_tag in

     let c1 = translate_expr e1 in

     let c2 = translate_expr e2 in

      (control_on_clock eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some eq) (MStep ([var_x], o, [c1;c2])))) :: s)

  | [x], Expr_pre e1 when VSet.mem (get_var x vars) d     ->

     let var_x = get_var x vars in

      control_on_clock eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some eq) (MStateAssign (var_x, translate_expr e1))) :: s)

  | [x], Expr_fby (e1, e2) when VSet.mem (get_var x vars) d ->

     let var_x = get_var x vars in

      mkinstr ?lustre_eq:(Some eq) (MStateAssign (var_x, translate_expr e1)) :: si,

      control_on_clock eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some eq) (MStateAssign (var_x, translate_expr e2))) :: s)

     let var_p = List.map (fun v -> get_var v vars) p in

     let vl = List.map translate_expr el in

     let o = new_instance node_f eq.eq_rhs.expr_tag in

       else reset_instance o r call_ck) @

	(control_on_clock call_ck (mkinstr ?lustre_eq:(Some eq) (MStep (var_p, o, vl)))) :: s)

    let var_x = get_var x vars in

       (translate_act (var_x, eq.eq_rhs)) :: s

let process_asserts nd =

          (i+1, assert_var::vars, eq::eqlist, {expr with expr_desc = Expr_ident var_id}::assertlist)

let translate_decl nd sch =

  (*Log.report ~level:1 (fun fmt -> Printers.pp_node fmt nd);*)

  let schedule = sch.Scheduling_type.schedule in

  let sorted_eqs = Scheduling.sort_equations_from_schedule nd schedule in

  let constant_eqs = constant_equations nd in

  (* In case of non functional backend (eg. C), additional local variables have

     to be declared for each assert *)

  let new_locals, assert_instrs, nd_node_asserts = process_asserts nd in

  let locals_list = nd.node_locals @ new_locals in

  let vars = get_node_vars nd in

  let m0, init0, j0, locals0, s0 =

    translate_eqs vars init_args constant_eqs

  in

  let m, init, j, locals, s as context_with_asserts =

    translate_eqs

      vars

      (m0, init0, j0, locals0, [])

      (assert_instrs@sorted_eqs)

  in

      step_checks = List.map (fun d -> d.Dimension.dim_loc,

                                       translate_expr vars init_args

                                         (expr_of_dimension d))

                      nd.node_checks;

      step_asserts = List.map (translate_expr vars context_with_asserts) nd_node_asserts;

  fun callee tag ->

	then Printf.sprintf "%s_inst_%d"

               o

               (incr cpt; !cpt)

val new_instance: Lustre_types.top_decl -> Lustre_types.tag -> Lustre_types.ident

	    (mk_fresh_var (norm_ctx.parentid, (norm_ctx.vars@vars)) expr.expr_loc)

	let _ = if Machine_types.is_active then

                  Machine_types.type_def (norm_ctx.parentid, norm_ctx.vars) new_aliases expr

        in

    List.fold_right (fun eq (def, vars) -> 

        let eq_defs = Splitting.tuple_split_eq eq in

        if eq_defs = [eq] then

          eq::def, vars 

        else

          List.fold_left (normalize_eq norm_ctx) (def, vars) eq_defs

      ) defs ([], vars)  

  with ex -> (

    raise ex

(* Projecting an eexpr to an eexpr associated to a single

   variable. Returns the updated ee, the bounded variable and the

   associated statement *)

let normalize_pred_eexpr decls norm_ctx (def,vars) ee =

  assert (ee.eexpr_quantifiers = []); (* We do not normalize quantifiers yet. This is for very far future. *)

  (* don't do anything is eexpr is just a variable *)

  let skip =

    match ee.eexpr_qfexpr.expr_desc with

    | Expr_ident _ | Expr_const _ -> true

    | _ -> false

  if skip then

    ee, (def, vars)

  else (

    (* New output variable *)

    let output_id = "spec" ^ string_of_int ee.eexpr_tag in

    let output_var = 

      mkvar_decl 

        ee.eexpr_loc 

        (output_id, 

         mktyp ee.eexpr_loc Tydec_bool, (* It is a predicate, hence a bool *)

         mkclock ee.eexpr_loc Ckdec_any, 

         false (* not a constant *),

         None,

         None

        ) 

    in

    let output_expr = expr_of_vdecl output_var in

    (* Rebuilding an eexpr with a silly expression, just a variable *)

    let ee' = { ee with eexpr_qfexpr = output_expr } in

    (* Now processing a fresh equation output_id = eexpr_qfexpr. We

       inline possible calls within, normalize it and type/clock the

       result.  *)

    let eq = mkeq ee.eexpr_loc ([output_id], ee.eexpr_qfexpr) in

    (* Inlining any calls *)

    let nodes = get_nodes decls in

    let calls = ISet.elements (get_expr_calls nodes ee.eexpr_qfexpr) in

    let vars, eqs =

      if calls = [] && not (eq_has_arrows eq) then

        vars, [eq]    

      else

        assert false (* TODO *)

    in

    (* Normalizing expr and eqs *)

    let defs, vars = List.fold_left (normalize_eq_split norm_ctx) (def, vars) eqs in

(*    let todefine =

      List.fold_left

        (fun m x-> if List.exists (fun y-> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m)

        (ISet.add output_id ISet.empty) vars in

 *)      

    (* Typing / Clocking *)

    try

      ignore (Typing.type_var_decl_list vars !Global.type_env vars);

        (*

    let env = Typing.type_var_decl [] !Global.type_env xxxx output_var in (* typing the variable *)

    (* Format.eprintf "typing var %s: %a@." output_id Types.print_ty output_var.var_type; *)

    let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in

    (*Format.eprintf "Env: %a@.@?" (Env.pp_env Types.print_ty) env;*)

    let undefined_vars = List.fold_left (Typing.type_eq (env, quant_vars@vars) false) todefine defs in

  (* check that table is empty *)

    if (not (ISet.is_empty undefined_vars)) then

      raise (Types.Error (ee.eexpr_loc, Types.Undefined_var undefined_vars));

    (*Format.eprintf "normalized eqs %a@.@?" 

      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs;  *)

         *)

    ee', (defs, vars)

  with (Types.Error (loc,err)) as exc ->

    eprintf "Typing error for eexpr %a: %a%a%a@."

      Printers.pp_eexpr ee

      Types.pp_error err

      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs

      Location.pp_loc loc

    ;

    raise exc

  )

   (*

(* We use node local vars to make sure we are creating fresh variables *) 

let normalize_spec decls parentid (in_vars, out_vars, l_vars) s =  

  (* Original set of variables actually visible from here: iun/out and

     spec locals (no node locals) *)

  let orig_vars = in_vars @ out_vars @ s.locals in

  let norm_ctx = {

      parentid = parentid;

      vars = in_vars @ out_vars @ l_vars;

      is_output = (fun _ -> false) (* no need to introduce fresh variables for outputs *);

    }

  in

  (* Normalizing existing stmts *)

  let eqs, auts = List.fold_right (fun s (el,al)  -> match s with Eq e -> e::el, al | Aut a -> el, a::al) s.stmts ([], []) in

  if auts != [] then assert false; (* Automata should be expanded by now. *)

  let defsvars = 

    List.fold_left (normalize_eq norm_ctx) ([], orig_vars) eqs

  in

  (* Iterate through predicates and normalize them on the go, creating

     fresh variables for any guarantees/assumes/require/ensure *)

  let process_predicates l defvars =

    List.fold_right (fun ee (accu, defvars) ->

        let ee', defvars = normalize_pred_eexpr decls norm_ctx defvars ee in

        ee'::accu, defvars

      ) l ([], defvars)

  let assume', defsvars = process_predicates s.assume defsvars in

  let guarantees', defsvars = process_predicates s.guarantees defsvars in

  let modes', (defs, vars) =

    List.fold_right (

        fun m (accu_m, defsvars) ->

        let require', defsvars = process_predicates m.require defsvars in

        let ensure', defsvars = process_predicates m.ensure defsvars in

        { m with require = require'; ensure = ensure' }:: accu_m, defsvars

      ) s.modes ([], defsvars)

  in

  let new_locals = List.filter not_is_orig_var vars in (* removing inouts and initial locals ones *)

    assume = assume';

    guarantees = guarantees';

    modes = modes'

  }

(* let nee _ = () in

 *   (\*normalize_eexpr decls iovars in *\)

 *   List.iter nee s.assume;

 *   List.iter nee s.guarantees;

 *   List.iter (fun m -> 

 *       List.iter nee m.require;

 *     List.iter nee m.ensure

 *     ) s.modes; *)

  let orig_vars = node.node_inputs@node.node_outputs@node.node_locals in

      match node.node_spec with None -> None | Some s -> Some (normalize_spec decls node.node_id (node.node_inputs, node.node_outputs, node.node_locals) s) 

     let s = normalize_spec decls nd.nodei_id (nd.nodei_inputs, nd.nodei_outputs, []) s in

(* TODO general remark: except in the add_vdecl, it seems to me that

      (* Typing each predicate expr *)

      let type_pred_ee ee : unit=

        type_subtyping_arg (env, vd_env) (false (* not in main *)) (false (* not a const *)) ee.eexpr_qfexpr type_bool

      in

      List.iter type_pred_ee

        (

          spec.assume 

          @ spec.guarantees

          @ List.flatten (List.map (fun m -> m.ensure @ m.require) spec.modes) 

        );