CristalCaveGem » LustreC

let mkidentpair loc restart state =

let rename_output used name = mk_new_name used (Format.sprintf "%s_out" name)

let rec rename_stmts_outputs frename stmts =

  match stmts with

  | []           -> []

  | (Eq eq) :: q   -> let eq' = Eq { eq with eq_lhs = List.map frename eq.eq_lhs } in

		      eq' :: rename_stmts_outputs frename q

  | (Aut aut) :: q -> let handlers' = List.map (fun h -> { h with hand_stmts = rename_stmts_outputs frename h.hand_stmts}) aut.aut_handlers in

                      let aut' = Aut { aut with aut_handlers = handlers' } in

		      aut' :: rename_stmts_outputs frename q

let mk_frename used outputs =

  let table = ISet.fold (fun name table -> IMap.add name (rename_output used name) table) outputs IMap.empty in

  (fun name -> try IMap.find name table with Not_found -> name)

let node_of_handler nused used node aut_id handler =

  let (new_locals, inputs) = ISet.partition (fun v -> ISet.mem v outputs) (handler_read ISet.empty handler) in

  let frename = mk_frename used outputs in

  let var_inputs = List.map (fun v -> get_node_var v node) (ISet.elements inputs) in

  let new_var_locals = List.map (fun v -> get_node_var v node) (ISet.elements new_locals) in

  let var_outputs = List.map (fun v -> get_node_var v node) (ISet.elements outputs) in

  let new_var_outputs = List.map (fun vdecl -> { vdecl with var_id = frename vdecl.var_id }) var_outputs in

  let new_output_eqs = List.map2 (fun o o' -> Eq (mkeq handler.hand_loc ([o'.var_id], mkident handler.hand_loc o.var_id))) var_outputs new_var_outputs in

  var_outputs,

    node_inputs = var_inputs;

    node_outputs = new_var_outputs;

    node_locals = new_var_locals @ handler.hand_locals;

    node_stmts = new_output_eqs @ handler.hand_stmts;

  mkexpr loc (Expr_when (List.fold_right add_branch conds (mkidentpair loc restart state), state, tag))

  let args = List.map (fun v -> mkexpr loc (Expr_when (mkident loc v.var_id, state, tag))) node.node_inputs in

  let arg = mkexpr loc (Expr_tuple args) in

  let reset = Some (mkident loc restart) in

  mkexpr loc (Expr_appl (node.node_id, arg, reset))

  let outputs = fst (snd (List.hd hnodes)) in

  let assign_handlers = List.map (fun (hs, (_, n)) -> (hs, expr_of_handler loc actual_r actual_s n hs)) hnodes in

(*

let expand_automata nused used owner typedef node aut =

  let initial = (List.hd aut.aut_handlers).hand_state in

  let incoming_r = mk_new_name used (aut.aut_id ^ "__restart_in") in

  let incoming_s = mk_new_name used (aut.aut_id ^ "__state_in") in

  let actual_r = mk_new_name used (aut.aut_id ^ "__restart_act") in

  let actual_s = mk_new_name used (aut.aut_id ^ "__state_act") in

  let next_incoming_r = mk_new_name used (aut.aut_id ^ "__next_restart_in") in

  let next_incoming_s = mk_new_name used (aut.aut_id ^ "__next_state_in") in

  (* merge on incoming_s gives actual_s by the unless equations *)

  let actual_handlers = List.map (fun h -> (h.hand_state, expr_of_exit h.hand_loc incoming_r incoming_s h.hand_unless h.hand_state)) aut.aut_handlers in

  let actual_expr = mkexpr aut.aut_loc (Expr_merge (incoming_s, unless_handlers)) in

  let actual_eq = mkeq aut.aut_loc ([actual_r; actual_s], unless_expr) in

  (* next_incoming_s and initial conditions gives incoming_s *)

  let incoming_expr = mkfby aut.aut_loc (mkidentpair aut.aut_loc tag_false initial) (mkidentpair aut.aut_loc next_incoming_r next_incoming_s) in

  let incoming_eq = mkeq aut.aut_loc ([incoming_r; incoming_s], incoming_expr) in

  (* merge on actual_s gives handler assigned variables and next_incoming_s by the until equations *)

  let until_handlers = List.map (fun h -> (h.hand_state, expr_of_exit h.hand_loc actual_r actual_s h.hand_until h.hand_state)) aut.aut_handlers in

  let until_expr = mkexpr aut.aut_loc (Expr_merge (actual_s, until_handlers)) in

  let fby_until_expr = mkfby aut.aut_loc (mkidentpair aut.aut_loc tag_false initial) until_expr in

  let until_eq = mkeq aut.aut_loc ([incoming_r; incoming_s], fby_until_expr) in

  let hnodes = List.map (fun h -> (h.hand_state, node_of_handler nused used node aut.aut_id h)) aut.aut_handlers in

  let outputs = fst (snd (List.hd hnodes)) in

  let next_incoming_and_assigned_vars = next_incoming_r :: next_incoming_s :: List.map (fun v -> v.var_id) outputs in

  let next_incoming_and_assigned_handlers =

    List.map (fun h -> ) aut.aut_handlers in

  let next_incoming_and_assigned_expr = mkexpr loc (Expr_merge (actual_s, next_incoming_and_assigned_handlers) in

  let next_incoming_and_assigned_eq = mkeq aut.aut_loc (next_incoming_and_assigned_vars, next_incoming_and_assigned_expr) in

  (* declaration of new local variables, equations and handler nodes *)

  let tydec_bool = { ty_dec_desc = Tydec_bool; ty_dec_loc = aut.aut_loc } in

  let tydec_state id = { ty_dec_desc = Tydec_clock (Tydec_const id); ty_dec_loc = aut.aut_loc } in

  let ckdec_any = { ck_dec_desc = Ckdec_any; ck_dec_loc = aut.aut_loc } in

  let locals' = [mkvar_decl aut.aut_loc (incoming_r, tydec_bool, ckdec_any, false);

                 mkvar_decl aut.aut_loc (actual_r  , tydec_bool, ckdec_any, false);

                 mkvar_decl aut.aut_loc (next_incoming_r  , tydec_bool, ckdec_any, false);

                 mkvar_decl aut.aut_loc (incoming_s, tydec_state typedef.tydef_id, ckdec_any, false);

                 mkvar_decl aut.aut_loc (actual_s  , tydec_state typedef.tydef_id, ckdec_any, false);

                 mkvar_decl aut.aut_loc (next_incoming_s, tydec_state typedef.tydef_id, ckdec_any, false)] in

  let eqs' = [Eq actual_eq; Eq next_incoming_and_assigned_eq; Eq incoming_eq] in

  (List.map2 (fun h (hs, (_, n)) -> mktop_decl h.hand_loc owner false (Node n)) aut.aut_handlers hnodes,

  locals',

  eqs')

*)

  let fby_until_expr = mkfby aut.aut_loc (mkidentpair aut.aut_loc tag_false initial) until_expr in

  let hnodes = List.map (fun h -> (h.hand_state, node_of_handler nused used node aut.aut_id h)) aut.aut_handlers in

  let tydec_state id = { ty_dec_desc = Tydec_clock (Tydec_const id); ty_dec_loc = aut.aut_loc } in

                 mkvar_decl aut.aut_loc (incoming_s, tydec_state typedef.tydef_id, ckdec_any, false);

                 mkvar_decl aut.aut_loc (actual_s  , tydec_state typedef.tydef_id, ckdec_any, false)] in

  (List.map2 (fun h (hs, (_, n)) -> mktop_decl h.hand_loc owner false (Node n)) aut.aut_handlers hnodes,