CristalCaveGem » LustreC

module VDeclModule =

struct (* Node module *)

module VMap = Map.Make(VDeclModule)

module VSet: sig

  val pp: Format.formatter -> t -> unit

  val get: ident -> t -> elt

end with type elt = var_decl =

  struct

    include Set.Make(VDeclModule)

    let pp fmt s =

      Format.fprintf fmt "{@[%a}@]" (Utils.fprintf_list ~sep:",@ " Printers.pp_var) (elements s)

    (* Strangley the find_first function of Set.Make is incorrect (at

       the current time of writting this comment. Had to switch to

       lists *)

    let get id s = List.find (fun v -> v.var_id = id) (elements s)

  end

let dummy_type_dec = {ty_dec_desc=Tydec_any; ty_dec_loc=Location.dummy_loc}

let dummy_clock_dec = {ck_dec_desc=Ckdec_any; ck_dec_loc=Location.dummy_loc}

let mktyp loc d =

  { ty_dec_desc = d; ty_dec_loc = loc }

let mkclock loc d =

  { ck_dec_desc = d; ck_dec_loc = loc }

let mkvar_decl loc ?(orig=false) (id, ty_dec, ck_dec, is_const, value, parentid) =

  { var_id = id;

    var_loc = loc }

    var_type =  typ;

    var_loc = Location.dummy_loc

  { expr_tag = Utils.new_tag ();

    expr_loc = loc }

let var_decl_of_const ?(parentid=None) c =

  { var_id = c.const_id;

    var_loc = c.const_loc }

    if used name

    then new_name (sprintf "_%s_%i" id cpt) (cpt+1)

    else name

  in new_name id 1

let mkeq loc (lhs, rhs) =

  { eq_lhs = lhs;

    eq_rhs = rhs;

    eq_loc = loc }

let mkassert loc expr =

  { assert_loc = loc;

    assert_expr = expr

  }

  { top_decl_desc = d; top_decl_loc = loc; top_decl_owner = own; top_decl_itf = itf }

let is_clock_dec_type cty =

  match cty with

  | Tydec_clock _ -> true

  | _             -> false

  match top_decl.top_decl_desc with

  | Const c -> c

  | _ -> assert false

  match top_decl.top_decl_desc with

  | Node nd -> nd

  | _ -> raise Not_found

  | ImportedNode ind -> ind

  | _ -> assert false

  match top_decl.top_decl_desc with

  | TypeDef tdef -> tdef

  | _ -> assert false

  | Open (local, dep) -> (local, dep)

  | _ -> assert false

  | TypeDef tdef ->

    (match tdef.tydef_desc with

       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

     | _               -> [])

  | _ -> assert false

    consts = []; locals = []; stmts = []; assume = []; guarantees = []; modes = []; imports = []; spec_loc = Location.dummy_loc;

(* For const declaration we do as for regular lustre node.

But for local flows we registered the variable and the lustre flow definition *)

  let v = mkvar_decl loc (id, typ, mkclock loc Ckdec_any, is_const, Some expr, None) in

  { empty_contract with consts = [v]; spec_loc = loc; }

    let v = mkvar_decl loc (id, typ, mkclock loc Ckdec_any, is_const, None, None) in

    let eq = mkeq loc ([id], expr) in 

    { empty_contract with locals = [v]; stmts = [Eq eq]; spec_loc = loc; }

let eexpr_add_name eexpr eexpr_name =

  { eexpr with eexpr_name }

  { empty_contract with guarantees = [eexpr_add_name eexpr name]; spec_loc = eexpr.eexpr_loc }

  { empty_contract with assume = [eexpr_add_name eexpr name]; spec_loc = eexpr.eexpr_loc }

  { empty_contract with modes = [{ mode_id = id; require = rl; ensure = el; mode_loc = loc; }]; spec_loc = loc }

  { empty_contract with imports = [{import_nodeid = id; inputs = ins; outputs = outs; import_loc = loc; }]; spec_loc = loc }

let merge_contracts ann1 ann2 = (* keeping the first item loc *)

  { consts = ann1.consts @ ann2.consts;

    spec_loc = ann1.spec_loc

  { eexpr_tag = Utils.new_tag ();

    eexpr_loc = loc }

let extend_eexpr q e = { e with eexpr_quantifiers = q@e.eexpr_quantifiers }

(*

let mkepredef_call loc funname args =

  mkeexpr loc (EExpr_appl (funname, mkeexpr loc (EExpr_tuple args), None))

let mkepredef_unary_call loc funname arg =

  mkeexpr loc (EExpr_appl (funname, arg, None))

*)

    | None, None -> assert false

    | Some _, None -> ann1

    | None, Some _ -> ann2

    | Some ann1, Some ann2 -> Some {

      annots = ann1.annots @ ann2.annots;

      annot_loc = ann1.annot_loc

    }

  List.iter (fun (key, _) -> 

    Annotations.add_expr_ann node_id e.expr_tag key

  ) annot.annots;

let mkinstr ?lustre_eq ?(instr_spec=[]) instr_desc = {

  instr_desc;

  (* lustre_expr = lustre_expr; *)

  instr_spec;

  lustre_eq;

}

  begin

    Format.fprintf fmt "{ /* node table */@.";

    Hashtbl.iter (fun id nd ->

      Format.fprintf fmt "%s |-> %a"

	id

	Printers.pp_short_decl nd

    ) node_table;

    Format.fprintf fmt "}@."

  end

  begin

    Format.fprintf fmt "{ /* consts table */@.";

    Hashtbl.iter (fun id const ->

      Format.fprintf fmt "%s |-> %a"

	id

	Printers.pp_const_decl (const_of_top const)

    ) consts_table;

    Format.fprintf fmt "}@."

  end

    match td.top_decl_desc with 

    | Node nd         -> nd.node_id

    | ImportedNode nd -> nd.nodei_id

    | _ -> assert false

  match td.top_decl_desc with 

  | Node nd         -> List.exists (fun v -> v.var_dec_const) nd.node_inputs

  | ImportedNode nd -> List.exists (fun v -> v.var_dec_const) nd.nodei_inputs

  | _ -> assert false

  match td.top_decl_desc with 

  | Node nd         -> nd.node_inputs

  | ImportedNode nd -> nd.nodei_inputs

  | _ -> assert false

let node_from_name id =

      Hashtbl.find node_table id

let update_node id top =

  Hashtbl.replace node_table id top

  match td.top_decl_desc with 

  | Node _         -> false

  | ImportedNode _ -> true

  | _ -> assert false

  match nd.node_spec with

  | Some (Contract _) -> true

  | _ -> false

  match nd.node_spec with

  | Some (Contract c) -> c

  | _ -> assert false

  match td.top_decl_desc with 

  | Node nd -> is_node_contract nd

  | _ -> false

let top_int_type = mktop (TypeDef {tydef_id = "int"; tydef_desc = Tydec_int})

let top_bool_type = mktop (TypeDef {tydef_id = "bool"; tydef_desc = Tydec_bool})

(* let top_float_type = mktop (TypeDef {tydef_id = "float"; tydef_desc = Tydec_float}) *)

let top_real_type = mktop (TypeDef {tydef_id = "real"; tydef_desc = Tydec_real})

  Utils.create_hashtable 20 [

    Tydec_int  , top_int_type;

    Tydec_bool , top_bool_type;

    (* Tydec_float, top_float_type; *)

    Tydec_real , top_real_type

  ]

  begin

    Format.fprintf fmt "{ /* type table */@.";

    Hashtbl.iter (fun tydec tdef ->

      Format.fprintf fmt "%a |-> %a"

	Printers.pp_var_type_dec_desc tydec

	Printers.pp_typedef (typedef_of_top tdef)

    ) type_table;

    Format.fprintf fmt "}@."

  end

  | Tydec_int | Tydec_bool | Tydec_real 

  (* | Tydec_float *) | Tydec_any | Tydec_const _ -> false

  | Tydec_clock typ' -> is_user_type typ'

  | _ -> true

  match ty1, ty2 with

  | Tydec_any           , _

  | _                   , Tydec_any             -> assert false

  | Tydec_const _       , Tydec_const _         -> get_repr_type ty1 = get_repr_type ty2

  | Tydec_const _       , _                     -> let ty1' = (typedef_of_top (Hashtbl.find type_table ty1)).tydef_desc

	       					   in (not (is_user_type ty1')) && coretype_equal ty1' ty2

  | _                   , Tydec_const _         -> coretype_equal ty2 ty1

  | Tydec_int           , Tydec_int

  | Tydec_real          , Tydec_real

  (* | Tydec_float         , Tydec_float *)

  | Tydec_bool          , Tydec_bool            -> true

  | Tydec_clock ty1     , Tydec_clock ty2       -> coretype_equal ty1 ty2

  | Tydec_array (d1,ty1), Tydec_array (d2, ty2) -> Dimension.is_eq_dimension d1 d2 && coretype_equal ty1 ty2

  | Tydec_enum tl1      , Tydec_enum tl2        -> List.sort compare tl1 = List.sort compare tl2

  | Tydec_struct fl1    , Tydec_struct fl2      ->

       List.length fl1 = List.length fl2

    && List.for_all2 (fun (f1, t1) (f2, t2) -> f1 = f2 && coretype_equal t1 t2)

      (List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl1)

      (List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl2)

  | _                                  -> false

  in ((*Format.eprintf "coretype_equal %a %a = %B@." Printers.pp_var_type_dec_desc ty1 Printers.pp_var_type_dec_desc ty2 res;*) res)

 match c with

 | Const_tag t -> t = tag_true || t = tag_false

 | _           -> false

  | Const_tag t when t = tag_true  -> Const_tag tag_false

  | _                              -> Const_tag tag_true

  | Const_tag t1, _            when t1 = tag_true -> c1

  | _           , Const_tag t2 when t2 = tag_true -> c2

  | _                                             -> Const_tag tag_false

  | Const_tag t1, _            when t1 = tag_false -> c1

  | _           , Const_tag t2 when t2 = tag_false -> c2

  | _                                              -> Const_tag tag_true

   match c1, c2 with

  | Const_tag t1, Const_tag t2 when t1 <> t2  -> Const_tag tag_true

  | _                                         -> Const_tag tag_false

  | Const_tag t1, _ when t1 = tag_false           -> Const_tag tag_true

  | _           , Const_tag t2 when t2 = tag_true -> Const_tag tag_true

  | _                                             -> Const_tag tag_false

  Utils.create_hashtable 20 [

   tag_true, top_bool_type;

   tag_false, top_bool_type

  ]

let field_table =

  Utils.create_hashtable 20 [

  ]

(*Format.eprintf "get_enum_type_tags %a@." Printers.pp_var_type_dec_desc cty;*)

 match cty with

 | Tydec_bool    -> [tag_true; tag_false]

 | Tydec_const _ -> (match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with

                     | Tydec_enum tl -> tl

                     | _             -> assert false)

 | _            -> assert false

 match cty with

 | Tydec_const _ -> (match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with

                     | Tydec_struct fl -> fl

                     | _               -> assert false)

 | _            -> assert false

let const_of_bool b =

 Const_tag (if b then tag_true else tag_false)

 match expr.expr_desc with

 | Expr_ident id -> id

 | _             -> assert false

  { expr_tag = Utils.new_tag ();

    expr_loc = v.var_loc }

  {expr_tag = Utils.new_tag ();

   expr_desc = Expr_ident id;

   expr_type = Types.new_var ();

   expr_clock = Clocks.new_var true;

   expr_delay = Delay.new_var ();

   expr_loc = loc;

   expr_annot = None}

 match expr.expr_desc with

  | Expr_tuple _ -> true

  | _            -> false

  match expr.expr_desc with

  | Expr_tuple elist -> elist

  | _                -> [expr]

 match elist with

 | [t]  -> { t with expr_loc = loc }

 | t::_ ->

    { t with expr_desc = Expr_tuple elist;

	     expr_type = Type_predef.type_tuple tlist;

	     expr_clock = Clock_predef.ck_tuple clist;

	     expr_tag = Utils.new_tag ();

	     expr_loc = loc }

 | _    -> assert false

 match expr.expr_desc with

 | Expr_appl (f, args, r) -> (f, expr_list_of_expr args, r)

 | _                      -> assert false

(* Conversion from dimension expr to standard expr, for the purpose of printing, typing, etc... *)

  match dim.dim_desc with

 | Dbool b        ->

     mkexpr dim.dim_loc (Expr_const (const_of_bool b))

 | Dint i         ->

     mkexpr dim.dim_loc (Expr_const (Const_int i))

 | Dident id      ->

     mkexpr dim.dim_loc (Expr_ident id)

 | Dite (c, t, e) ->

     mkexpr dim.dim_loc (Expr_ite (expr_of_dimension c, expr_of_dimension t, expr_of_dimension e))

 | Dappl (id, args) ->

     mkexpr dim.dim_loc (Expr_appl (id, expr_of_expr_list dim.dim_loc (List.map expr_of_dimension args), None))

 | Dlink dim'       -> expr_of_dimension dim'

 | Dvar

 | Dunivar          -> (Format.eprintf "internal error: Corelang.expr_of_dimension %a@." Dimension.pp_dimension dim;

			assert false)

  { expr

  with

    expr_type = Types.new_ty Types.type_int;

  }

 match const with

 | Const_int i                                    -> mkdim_int loc i

 | Const_tag t when t = tag_true || t = tag_false -> mkdim_bool loc (t = tag_true)

 | _                                              -> raise InvalidDimension

(* Conversion from standard expr to dimension expr, for the purpose of injecting static call arguments 

   into dimension expressions *)

  | Expr_const c  -> dimension_of_const expr.expr_loc c

  | Expr_ident id -> mkdim_ident expr.expr_loc id

      let k = Types.get_static_value (Env.lookup_value Basic_library.type_env f) in

      if k = None then raise InvalidDimension;

      mkdim_appl expr.expr_loc f (List.map dimension_of_expr (expr_list_of_expr args))

  | Expr_ite (i, t, e)        ->

      mkdim_ite expr.expr_loc (dimension_of_expr i) (dimension_of_expr t) (dimension_of_expr e)

  | _ -> raise InvalidDimension (* not a simple dimension expression *)

let sort_handlers hl =

 List.sort (fun (t, _) (t', _) -> compare t t') hl

  | Const_real r1, Const_real _

    -> Real.eq r1 r1 

  | Const_struct lcl1, Const_struct lcl2

    -> List.length lcl1 = List.length lcl2

    && List.for_all2 (fun (l1, c1) (l2, c2) -> l1 = l2 && is_eq_const c1 c2) lcl1 lcl2

  | _  -> c1 = c2

let rec is_eq_expr e1 e2 = match e1.expr_desc, e2.expr_desc with

  | Expr_const c1, Expr_const c2 -> is_eq_const c1 c2

  | Expr_ident i1, Expr_ident i2 -> i1 = i2

  | Expr_array el1, Expr_array el2 

  | Expr_tuple el1, Expr_tuple el2 -> 

    List.length el1 = List.length el2 && List.for_all2 is_eq_expr el1 el2 

  | Expr_arrow (e1, e2), Expr_arrow (e1', e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2'

  | Expr_fby (e1,e2), Expr_fby (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2'

  | Expr_ite (i1, t1, e1), Expr_ite (i2, t2, e2) -> is_eq_expr i1 i2 && is_eq_expr t1 t2 && is_eq_expr e1 e2

  (* | Expr_concat (e1,e2), Expr_concat (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2' *)

  | Expr_pre e, Expr_pre e' -> is_eq_expr e e'

  | Expr_when (e, i, l), Expr_when (e', i', l') -> l=l' && i=i' && is_eq_expr e e'

  | Expr_merge(i, hl), Expr_merge(i', hl') -> i=i' && List.for_all2 (fun (t, h) (t', h') -> t=t' && is_eq_expr h h') (sort_handlers hl) (sort_handlers hl')

  | Expr_appl (i, e, r), Expr_appl (i', e', r') -> i=i' && r=r' && is_eq_expr e e'

  | Expr_access (e1, i1), Expr_access (e2, i2) -> is_eq_expr e1 e2 && is_eq_expr (expr_of_dimension i1) (expr_of_dimension i2)

  | _ -> false

let get_node_vars nd =

  nd.node_inputs @ nd.node_locals @ nd.node_outputs

let get_var id var_list =

  List.find (fun v -> v.var_id = id) var_list

  try

    get_var id (get_node_vars node)

  with Not_found -> begin

    (* Format.eprintf "Unable to find variable %s in node %s@.@?" id node.node_id; *)

  end

	match stmt with

	| Eq eq -> eq :: res_eq, res_aut

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

      stmts

      ([], []) in

  (fun nd ->

      let (old, res) = Hashtbl.find table_eqs nd.node_id

      in if old == nd.node_stmts then res else raise Not_found

    with Not_found -> 

      begin

	Hashtbl.replace table_eqs nd.node_id (nd.node_stmts, res);

	res

      end)

  try

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

  with

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

let get_nodes prog = 

  List.fold_left (

    fun nodes decl ->

      | Node _ -> decl::nodes

      | Const _ | ImportedNode _ | Include _ | Open _ | TypeDef _ -> nodes

  ) [] prog

let get_imported_nodes prog = 

  List.fold_left (

    fun nodes decl ->

	| ImportedNode _ -> decl::nodes

	| Const _ | Node _ | Include _ | Open _ | TypeDef _-> nodes  

  ) [] prog

let get_consts prog = 

  List.fold_right (

    fun decl consts ->

	| Const _ -> decl::consts

	| Node _ | ImportedNode _ | Include _ | Open _ | TypeDef _ -> consts  

  ) prog []

let get_typedefs prog = 

  List.fold_right (

    fun decl types ->

	| TypeDef _ -> decl::types

	| Node _ | ImportedNode _ | Include _ | Open _ | Const _ -> types  

  ) prog []

  List.fold_right (

    fun decl deps ->

	| Open _ -> decl::deps

	| Node _ | ImportedNode _ | TypeDef _ | Include _ | Const _ -> deps  

  ) prog []

 {nodei_id = nd.node_id;

  nodei_type = nd.node_type;

  nodei_clock = nd.node_clock;

  nodei_inputs = nd.node_inputs;

  nodei_outputs = nd.node_outputs;

  nodei_stateless = nd.node_dec_stateless;

  nodei_spec = nd.node_spec;

  (* nodei_annot = nd.node_annot; *)

  nodei_prototype = None;

  nodei_in_lib = [];

 }

(*        Renaming / Copying                                                      *)

  mkvar_decl

    vdecl.var_loc

    ~orig:vdecl.var_orig

    (

      vdecl.var_id,

      vdecl.var_parent_nodeid

    )

let copy_const cdecl =

  { cdecl with const_type = Types.new_var () }

  { nd with

    node_type     = Types.new_var ();

    node_clock    = Clocks.new_var true;

    node_inputs   = List.map copy_var_decl nd.node_inputs;

    node_outputs  = List.map copy_var_decl nd.node_outputs;

    node_locals   = List.map copy_var_decl nd.node_locals;

    node_checks   = [];

  | Node nd -> { top with top_decl_desc = Node (copy_node nd)  }

  | Const c -> { top with top_decl_desc = Const (copy_const c) }

  | _       -> top

let copy_prog top_list =

  List.map copy_top top_list

 match cty with

 | Tydec_array (d, cty') -> Tydec_array (Dimension.expr_replace_expr rename d, rename_static rename cty')

 | Tydec_clock cty       -> Tydec_clock (rename_static rename cty)

 | Tydec_struct fl       -> Tydec_struct (List.map (fun (f, cty) -> f, rename_static rename cty) fl)

 | _                      -> cty

 match cck with

 | Ckdec_bool cl -> Ckdec_bool (List.map (fun (c, l) -> rename c, l) cl)

 | _             -> cck

 (*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

   match expr_desc with

   | Expr_const _ -> expr_desc

   | Expr_ident i -> Expr_ident (f_var i)

   | Expr_array el -> Expr_array (List.map re el)

   | Expr_access (e1, d) -> Expr_access (re e1, d)

   | Expr_power (e1, d) -> Expr_power (re e1, d)

   | Expr_tuple el -> Expr_tuple (List.map re el)

   | Expr_ite (c, t, e) -> Expr_ite (re c, re t, re e)

   | Expr_arrow (e1, e2)-> Expr_arrow (re e1, re e2) 

   | Expr_fby (e1, e2) -> Expr_fby (re e1, re e2)

   | Expr_pre e' -> Expr_pre (re e')

   | Expr_when (e', i, l)-> Expr_when (re e', f_var i, l)

   | Expr_merge (i, hl) -> 

     Expr_merge (f_var i, List.map (fun (t, h) -> (t, re h)) hl)

   | Expr_appl (i, e', i') -> 

     Expr_appl (f_node i, re e', Utils.option_map re i')

 let rename_var f_var v = {

     (copy_var_decl v) with

     var_id = f_var v.var_id;

     var_type = v.var_type;

     var_clock = v.var_clock;

 } 

 let rename_vars f_var = List.map (rename_var 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_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