CristalCaveGem » LustreC

    | 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