CristalCaveGem » LustreC

    let eqs, auts = get_node_eqs nd in

    assert (auts = []); (* Not checking automata yet . *)

    List.fold_left (fun checks eq -> check_expr checks eq.eq_rhs) checks eqs in

    let calls_expr = Causality.NodeDep.get_calls (fun _ -> true) node in

    let eqs, auts = get_node_eqs node in

    assert (auts = []); (* TODO voir si on peut acceder directement aux eqs qui font les calls *)

  let get_node_eqs nd =

    let eqs, auts = get_node_eqs nd in

    if auts != [] then assert false (* No call on causality on a Lustre model

				       with automaton. They should be expanded by now. *);

    eqs

  let get_calls prednode nd =

    let accu f init objl = List.fold_left (fun accu o -> ESet.union accu (f o)) init objl in

    let get_eq_calls eq = get_expr_calls prednode eq.eq_rhs in

    let rec get_stmt_calls s =

      match s with Eq eq -> get_eq_calls eq | Aut aut -> get_aut_calls aut 

    and get_aut_calls aut =

      let get_handler_calls h =

	let get_cond_calls c = accu (fun (_,e,_,_) -> get_expr_calls prednode e) ESet.empty c in

	let until = get_cond_calls h.hand_until in

	let unless = get_cond_calls h.hand_unless in

	let calls = ESet.union until unless in 

	let calls = accu get_stmt_calls calls h.hand_stmts in

	let calls = accu (fun a -> get_expr_calls prednode a.assert_expr) calls h.hand_asserts in

	(* let calls = accu xx calls h.hand_annots in *) (* TODO: search for calls in eexpr *)

	calls

      in

      accu get_handler_calls ESet.empty aut.aut_handlers

    in

    let eqs, auts = get_node_eqs nd in

    let deps = accu get_eq_calls ESet.empty eqs in

    let deps = accu get_aut_calls deps auts in

	     (get_calls (fun _ -> true) nd) 

	   nd.node_gencalls <- get_calls prednode nd

    let eqs , auts = get_node_eqs node in

    assert (auts = []); (* TODO: check: For the moment we assume that auts are expanded by now *)

    let (mem_eqs, non_mem_eqs) = List.partition (fun eq -> List.exists (fun v -> ISet.mem v mems) eq.eq_lhs) eqs in

  let eqs, auts = get_node_eqs nd in (* TODO XXX: perform the clocking on auts.

					For the moment, it is ignored *)

  List.iter (clock_eq new_env) eqs;

  (*

    List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_inputs;

    List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_outputs;*)

  (*  if (is_main && is_polymorphic ck_node) then

      raise (Error (loc,(Cannot_be_polymorphic ck_node)));

  *)

(* Used in rename functions in Corelang. We have to propagate the renaming to

   ids of variables clocking the signals *)

(* Carrier are not renamed. They corresponds to enumerated type constants *)

(*

let rec rename_carrier f c =

  { c with carrier_desc = rename_carrier_desc fvar c.carrier_desc }

and rename_carrier_desc f 

let re = rename_carrier f

  match cd with

  | Carry_const id -> Carry_const (f id)

  | Carry_link ce -> Carry_link (re ce)

  | _ -> cd

*)

let rec rename_clock_expr fvar c =

  { c with cdesc = rename_clock_desc fvar c.cdesc }

and rename_clock_desc fvar cd =

  let re = rename_clock_expr fvar in

  match cd with

  | Carrow (c1, c2) -> Carrow (re c1, re c2)

  | Ctuple cl -> Ctuple (List.map re cl)

  | Con (c1, car, id) -> Con (re c1, car, fvar id)

  | Cvar 

  | Cunivar -> cd

  | Clink c -> Clink (re c)

  | Ccarrying (car, c) -> Ccarrying (car, re c)

    | Tydec_enum tags ->

       List.map

	 (fun tag ->

	   let cdecl = {

	     const_id = tag;

	     const_loc = top_decl.top_decl_loc;

	     const_value = Const_tag tag;

	     const_type = Type_predef.type_const tdef.tydef_id

	   } in

	   { top_decl with top_decl_desc = Const cdecl })

	 tags

      (fun stmt (res_eq, res_aut) ->

	| Eq eq -> eq :: res_eq, res_aut

	| Aut aut -> res_eq, aut::res_aut)

      ([], []) in

  let eqs, auts = get_node_eqs node in

  try

    List.find (fun eq -> List.mem id eq.eq_lhs) eqs

  with

    Not_found -> (* Shall be defined in automata auts *) raise Not_found

 (*Format.eprintf "Types.rename_static %a = %a@." print_ty ty print_ty res; res*)

 (* let rec expr_replace_var fvar expr = *)

 (*  { expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc } *)

 (* and expr_desc_replace_var fvar expr_desc = *)

 (*   match expr_desc with *)

 (*   | Expr_const _ -> expr_desc *)

 (*   | Expr_ident i -> Expr_ident (fvar i) *)

 (*   | Expr_array el -> Expr_array (List.map (expr_replace_var fvar) el) *)

 (*   | Expr_access (e1, d) -> Expr_access (expr_replace_var fvar e1, d) *)

 (*   | Expr_power (e1, d) -> Expr_power (expr_replace_var fvar e1, d) *)

 (*   | Expr_tuple el -> Expr_tuple (List.map (expr_replace_var fvar) el) *)

 (*   | Expr_ite (c, t, e) -> Expr_ite (expr_replace_var fvar c, expr_replace_var fvar t, expr_replace_var fvar e) *)

 (*   | Expr_arrow (e1, e2)-> Expr_arrow (expr_replace_var fvar e1, expr_replace_var fvar e2)  *)

 (*   | Expr_fby (e1, e2) -> Expr_fby (expr_replace_var fvar e1, expr_replace_var fvar e2) *)

 (*   | Expr_pre e' -> Expr_pre (expr_replace_var fvar e') *)

 (*   | Expr_when (e', i, l)-> Expr_when (expr_replace_var fvar e', fvar i, l) *)

 (*   | Expr_merge (i, hl) -> Expr_merge (fvar i, List.map (fun (t, h) -> (t, expr_replace_var fvar h)) hl) *)

 (*   | Expr_appl (i, e', i') -> Expr_appl (i, expr_replace_var fvar e', Utils.option_map (expr_replace_var fvar) i') *)

 let rec rename_expr  f_node f_var expr =

   { expr with expr_desc = rename_expr_desc f_node f_var expr.expr_desc }

 and rename_expr_desc f_node f_var expr_desc =

   let re = rename_expr  f_node f_var in

 let rename_dec_type f_node f_var t = assert false (*

						     Types.rename_dim_type (Dimension.rename f_node f_var) t*)

 let rename_dec_clock f_node f_var c = assert false (* 

					  Clocks.rename_clock_expr f_var c*)

 let rename_var f_node f_var v = {

   v with

     var_id = f_var v.var_id;

     var_dec_type = rename_dec_type f_node f_var v.var_type;

     var_dec_clock = rename_dec_clock f_node f_var v.var_clock

 } 

 let rename_vars f_node f_var = List.map (rename_var f_node f_var) 

 let rec rename_eq f_node f_var eq = { eq with

   eq_lhs = List.map f_var eq.eq_lhs; 

   eq_rhs = rename_expr f_node f_var eq.eq_rhs

 } 

 and rename_handler f_node f_var  h = {h with

   hand_state = f_var h.hand_state;

   hand_unless = List.map (

     fun (l,e,b,id) -> l, rename_expr f_node f_var e, b, f_var id

   ) h.hand_unless;

   hand_until = List.map (

     fun (l,e,b,id) -> l, rename_expr f_node f_var e, b, f_var id

   ) h.hand_until;

   hand_locals = rename_vars f_node f_var h.hand_locals;

   hand_stmts = rename_stmts f_node f_var h.hand_stmts;

   hand_annots = rename_annots f_node f_var h.hand_annots;

 } 

 and rename_aut f_node f_var  aut = { aut with

   aut_id = f_var aut.aut_id;

   aut_handlers = List.map (rename_handler f_node f_var) aut.aut_handlers;

 }

 and rename_stmts f_node f_var stmts = List.map (fun stmt -> match stmt with

   | Eq eq -> Eq (rename_eq f_node f_var eq)

   | Aut at -> Aut (rename_aut f_node f_var at))

   stmts

 and rename_annotl f_node f_var  annots = 

   List.map 

     (fun (key, value) -> key, rename_eexpr f_node f_var value) 

     annots

 and rename_annot f_node f_var annot =

   { annot with annots = rename_annotl f_node f_var annot.annots }

 and rename_annots f_node f_var annots =

   List.map (rename_annot f_node f_var) annots

and rename_eexpr f_node f_var ee =

   { ee with

     eexpr_tag = Utils.new_tag ();

     eexpr_qfexpr = rename_expr f_node f_var ee.eexpr_qfexpr;

     eexpr_quantifiers = List.map (fun (typ,vdecls) -> typ, rename_vars f_node f_var vdecls) ee.eexpr_quantifiers;

     eexpr_normalized = Utils.option_map 

       (fun (vdecl, eqs, vdecls) ->

	 rename_var f_node f_var vdecl,

	 List.map (rename_eq f_node f_var) eqs,

	 rename_vars f_node f_var vdecls

       ) ee.eexpr_normalized;

   }

 let rename_node f_node f_var nd =

   let rename_var = rename_var f_node f_var in

   let rename_expr = rename_expr f_node f_var in

   let rename_stmts = rename_stmts f_node f_var in

   let inputs = List.map rename_var nd.node_inputs in

   let outputs = List.map rename_var nd.node_outputs in

   let locals = List.map rename_var nd.node_locals in

   let gen_calls = List.map rename_expr nd.node_gencalls in

   let node_checks = List.map (Dimension.rename f_node f_var)  nd.node_checks in

   let node_asserts = List.map 

     (fun a -> 

       {a with assert_expr = 

	   let expr = a.assert_expr in

	   rename_expr expr})

     nd.node_asserts

   in

   let node_stmts = rename_stmts nd.node_stmts

   in

   let spec = 

     Utils.option_map 

       (fun s -> assert false; (*rename_node_annot f_node f_var s*) ) (* TODO: implement! *) 

       nd.node_spec 

   in

   let annot = rename_annots f_node f_var nd.node_annot in

   {

     node_id = f_node nd.node_id;

     node_type = nd.node_type;

     node_clock = nd.node_clock;

     node_inputs = inputs;

     node_outputs = outputs;

     node_locals = locals;

     node_gencalls = gen_calls;

     node_checks = node_checks;

     node_asserts = node_asserts;

     node_stmts = node_stmts;

     node_dec_stateless = nd.node_dec_stateless;

     node_stateless = nd.node_stateless;

     node_spec = spec;

     node_annot = annot;

   }

	 { top with top_decl_desc = Node (rename_node f_node f_var nd) }

(* Applies the renaming function [fvar] to every rhs

   only when the corresponding lhs satisfies predicate [pvar] *)

 let eq_replace_rhs_var pvar fvar eq =

   let pvar l = List.exists pvar l in

   let rec replace lhs rhs =

     { rhs with expr_desc =

     match lhs with

     | []  -> assert false

     | [_] -> if pvar lhs then rename_expr_desc (fun x -> x) fvar rhs.expr_desc else rhs.expr_desc

     | _   ->

       (match rhs.expr_desc with

       | Expr_tuple tl ->

	 Expr_tuple (List.map2 (fun v e -> replace [v] e) lhs tl)

       | Expr_appl (f, arg, None) when Basic_library.is_expr_internal_fun rhs ->

	 let args = expr_list_of_expr arg in

	 Expr_appl (f, expr_of_expr_list arg.expr_loc (List.map (replace lhs) args), None)

       | Expr_array _

       | Expr_access _

       | Expr_power _

       | Expr_const _

       | Expr_ident _

       | Expr_appl _   ->

	 if pvar lhs

	 then rename_expr_desc (fun x -> x) fvar rhs.expr_desc

	 else rhs.expr_desc

       | Expr_ite (c, t, e)   -> Expr_ite (replace lhs c, replace lhs t, replace lhs e)

       | Expr_arrow (e1, e2)  -> Expr_arrow (replace lhs e1, replace lhs e2) 

       | Expr_fby (e1, e2)    -> Expr_fby (replace lhs e1, replace lhs e2)

       | Expr_pre e'          -> Expr_pre (replace lhs e')

       | Expr_when (e', i, l) -> let i' = if pvar lhs then fvar i else i

				 in Expr_when (replace lhs e', i', l)

       | Expr_merge (i, hl)   -> let i' = if pvar lhs then fvar i else i

				 in Expr_merge (i', List.map (fun (t, h) -> (t, replace lhs h)) hl)

       )

     }

   in { eq with eq_rhs = replace eq.eq_lhs eq.eq_rhs }

and get_aut_handler_calls nodes h =

  List.fold_left (fun accu stmt -> match stmt with

  | Eq eq -> Utils.ISet.union (get_eq_calls nodes eq) accu

  | Aut aut' ->  Utils.ISet.union (get_aut_calls nodes aut') accu

  ) Utils.ISet.empty h.hand_stmts 

and get_aut_calls nodes aut =

  List.fold_left (fun accu h -> Utils.ISet.union (get_aut_handler_calls nodes h) accu)

    Utils.ISet.empty aut.aut_handlers

  let eqs, auts = get_node_eqs node in

  let aut_calls =

    List.fold_left

      (fun accu aut -> Utils.ISet.union (get_aut_calls nodes aut) accu)

      Utils.ISet.empty auts

  in

  List.fold_left

    (fun accu eq -> Utils.ISet.union (get_eq_calls nodes eq) accu)

    aut_calls eqs

and aut_has_arrows aut = List.exists (fun h -> List.exists (fun stmt -> match stmt with Eq eq -> eq_has_arrows eq | Aut aut' -> aut_has_arrows aut') h.hand_stmts ) aut.aut_handlers 

  let eqs, auts = get_node_eqs node in

  List.exists (fun eq -> eq_has_arrows eq) eqs || List.exists (fun aut -> aut_has_arrows aut) auts

val get_node_eqs: node_desc -> eq list * automata_desc list

(*val expr_replace_var: (ident -> ident) -> expr -> expr*)

(** val rename_expr f_node f_var expr *)

val rename_expr : (ident -> ident) -> (ident -> ident) -> expr -> expr

(** val rename_eq f_node f_var eq *)

val rename_eq : (ident -> ident) -> (ident -> ident) -> eq -> eq

(** val rename_aut f_node f_var aut *)

val rename_aut : (ident -> ident) -> (ident -> ident) -> automata_desc -> automata_desc

(** rename_prog f_node f_var prog *)

let rec rename fnode fvar e = 

 { e with dim_desc = expr_replace_var_desc fnode fvar e.dim_desc }

and expr_replace_var_desc fnode fvar e =

  let re = rename fnode fvar in

  | Dappl (id, el) -> Dappl (fnode id, List.map re el)

(* let rename_expr rename expr = expr_replace_var rename expr *)

(*

*)

  let eqs, auts = get_node_eqs node in

  let eqs' = List.map (rename_eq (fun x -> x) rename) eqs in

  let auts' = List.map (rename_aut (fun x -> x) rename) auts in

	 Utils.option_map (rename_expr (fun x -> x) rename) v.var_dec_value) in

  let eqs_r' = 

    let all_eqs = (List.map (fun eq -> Eq eq) eqs') @ (List.map (fun aut -> Aut aut) auts') in

      None -> all_eqs

    | Some cond -> (

      assert (auts' = []); (* TODO: we do not handle properly automaton in case of reset call *)

      List.map (fun eq -> Eq (add_eq_reset_cond cond eq)) eqs'

    )

  let assign_inputs = Eq (mkeq loc (List.map (fun v -> v.var_id) inputs',

                                expr_of_expr_list args.expr_loc (List.map snd dynamic_inputs))) in

	    rename_expr (fun x -> x) rename expr

     let args', locals', eqs', asserts', annots' = inline_expr args locals node nodes in 

     if List.exists (check_node_name id) nodes && (* the current node call is provided

						     as arguments nodes *)

       (not selection_on_annotation || is_inline_expr expr) (* and if selection on annotation is activated, 

							       it is explicitely inlined here *)

     then (

       (* Format.eprintf "Inlining call to %s in expression %a@." id Printers.pp_expr expr; *)

       (* The node should be inlined *)

       (* let _ =     Format.eprintf "Inlining call to %s@." id in *)

       let called = try List.find (check_node_name id) nodes 

	 with Not_found -> (assert false) in

       let called = node_of_top called in

       let called' = inline_node called nodes in

       let expr, locals', eqs'', asserts'', annots'' = 

	 inline_call called' expr.expr_loc expr.expr_tag args' reset locals' node in

       expr, locals', eqs'@eqs'', asserts'@asserts'', annots'@annots''

     )

     else 

       (* let _ =     Format.eprintf "Not inlining call to %s@." id in *)

       { expr with expr_desc = Expr_appl(id, args', reset)}, 

       locals', 

       eqs', 

       asserts',

       annots'

     let el', l', eqs', asserts', annots' = inline_tuple el in

     { expr with expr_desc = Expr_tuple el' }, l', eqs', asserts', annots'

     let g', t', e', l', eqs', asserts', annots' = inline_triple g t e in

     { expr with expr_desc = Expr_ite (g', t', e') }, l', eqs', asserts', annots'

     let e1', e2', l', eqs', asserts', annots' = inline_pair e1 e2 in

     { expr with expr_desc = Expr_arrow (e1', e2') } , l', eqs', asserts', annots'

     let e1', e2', l', eqs', asserts', annots' = inline_pair e1 e2 in

     { expr with expr_desc = Expr_fby (e1', e2') }, l', eqs', asserts', annots'

     let el', l', eqs', asserts', annots' = inline_tuple el in

     { expr with expr_desc = Expr_array el' }, l', eqs', asserts', annots'

     let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in 

     { expr with expr_desc = Expr_access (e', dim) }, l', eqs', asserts', annots'

     let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in 

     { expr with expr_desc = Expr_power (e', dim) }, l', eqs', asserts', annots'

     let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in 

     { expr with expr_desc = Expr_pre e' }, l', eqs', asserts', annots'

     let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in 

     { expr with expr_desc = Expr_when (e', id, label) }, l', eqs', asserts', annots'

     let el, l', eqs', asserts', annots' = inline_tuple (List.map snd branches) in

     let branches' = List.map2 (fun (label, _) v -> label, v) branches el in

     { expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts', annots'

    let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in

    let eqs, auts = get_node_eqs node in

    assert (auts = []); (* No inlining of automaton yet. One should visit each

			   handler eqs and perform similar computation *)

    let new_locals, stmts, asserts, annots = 

      List.fold_left (fun (locals, stmts, asserts, annots) eq ->

	let eq_rhs', locals', new_stmts', asserts', annots' = 

	  inline_expr eq.eq_rhs locals node nodes 

	in

	locals', Eq { eq with eq_rhs = eq_rhs' }::new_stmts'@stmts, asserts'@asserts, annots'@annots

      ) (node.node_locals, [], node.node_asserts, node.node_annot) eqs

    in

    let inlined = 

      { node with

	node_locals = new_locals;

	node_stmts = stmts;

	node_asserts = asserts;

	node_annot = annots;

      }

    in

    begin

      (*Format.eprintf "inline node:<< %a@.>>@." Printers.pp_node inlined;*)

      Hashtbl.add inline_table node.node_id inlined;

      inlined

    end

  let orig = rename_prog orig_rename (* f_node *) identity (* f_var *) identity (* f_const *) orig in

  let eqs, auts = get_node_eqs nd in

  assert (auts = []); (* Automata should be expanded by now *)

  let split_eqs = Splitting.tuple_split_eq_list eqs in

      let eqs, auts = get_node_eqs nd in

      assert (auts = []); (* Automata should be expanded by now *)

      		     Printers.pp_node_eqs eqs;

  let defs, vars =

    let eqs, auts = get_node_eqs node in

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

    List.fold_left (inject_eq node) ([], orig_vars) eqs in

let compute_records_node nd =

  let eqs, auts = get_node_eqs nd in

  assert (auts=[]); (* Automaton should be expanded by now *)

  merge_records (List.map compute_records_eq eqs)

    let eqs, auts = get_node_eqs node in

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

    List.fold_left (normalize_eq node) ([], orig_vars) eqs in

  (* we first print types: the function SortProg.sort could do the job but ut

     introduces a cyclic dependance *)

and compute_node nd = (* returns true iff the node is stateless.*)

  let eqs, aut = get_node_eqs nd in

  aut = [] && (* A node containinig an automaton will be stateful *)

      List.for_all (fun eq -> check_expr eq.eq_rhs) eqs

    Format.printf "TABLE: %a@." print_type_table ();

   (* TODO REMOVE *)

    let eqs, auts = get_node_eqs nd in

    (* TODO XXX: il faut typer les handlers de l'automate *)

    List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init eqs