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,

    var_orig = false;

let undo_instance_var id =

 assert (is_instance_var id);

 String.sub id 1 (String.length id - 1)

    | Expr_appl (f, e, Some c) ->

      mashup_appl_dependencies f e (add_dep lhs_is_mem lhs c g)

    { var_decl with var_id = cp_var; var_orig = false },

    (fprintf_list ~sep:", " pp_print_string) trace

(** [clock_uncarry ck] drops the possible carrier(s) name(s) from clock [ck] *)

let rec clock_uncarry ck =

  | Con(ck', cr, l)    -> clock_on (clock_uncarry ck') cr l

  | Ctuple ckl         -> clock_of_clock_list (List.map clock_uncarry ckl)

(* Computes the root clock of a tuple or a node clock,

   which is not the same as the base clock.

   Root clock will be used as the call clock 

   of a given node instance *)

let compute_root_clock ck =

  let root = Clocks.root ck in

  let branch = ref None in

  let rec aux ck =

    match (repr ck).cdesc with

    | Ctuple cl ->

        List.iter aux cl

    | Carrow (ck1,ck2) ->

        aux ck1; aux ck2

    | _ ->

        begin

          match !branch with

          | None ->

              branch := Some (Clocks.branch ck)

          | Some br ->

              (* cannot fail *)

              branch := Some (Clocks.common_prefix br (Clocks.branch ck))

        end

  in

  begin

    aux ck;

    Clocks.clock_of_root_branch root (Utils.desome !branch)

  end

      | Some c      -> clock_standard_args env [c] in

      List.iter (fun (t, h) -> let ckh = clock_uncarry (clock_expr env h) in unify_tuple_clock (Some (new_ck (Con (cvar,crvar,t)) true)) ckh h.expr_loc) hl;

      let cres = clock_current ((snd (List.hd hl)).expr_clock) in

      expr.expr_clock <- cres;

      cres

let clock_current ck =

 clock_of_clock_list (List.map (fun ck -> match (repr ck).cdesc with Con(ck',_,_) -> ck' | _ -> assert false) (clock_list_of_clock ck))

let clock_of_root_branch r br =

 List.fold_left (fun ck (cr,l) -> new_ck (Con (ck, cr, l)) true) r br

(* Computes the (longest) common prefix of two branches *)

let rec common_prefix br1 br2 =

 match br1, br2 with

 | []          , _

 | _           , []           -> []

 | (cr1,l1)::q1, (cr2,l2)::q2 ->

   if eq_carrier cr1 cr2 && (l1 = l2)

   then (cr1, l1) :: common_prefix q1 q2

   else []

      (*ignore (Modules.load_header ISet.empty header);*)

    (*ignore (Modules.load_program ISet.empty prog);*)

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

    var_orig = orig;

    var_orig = true;

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

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

  | Expr_appl (_, arg, Some r) -> List.fold_left get_expr_vars vars [arg; r]

val mkvar_decl: Location.t -> ?orig:bool -> ident * type_dec * clock_dec * bool (* is const *) -> var_decl

val call_of_expr: expr -> (ident * expr list * expr option)

   var_orig = false;

     var_orig:bool;

and call_t = ident * expr * expr option 

     (* The third part denotes the boolean condition for resetting *)

    var_orig = false;

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

                   [control_on_clock node args c (conditional g [MReset i] [])]

    let env_cks = List.fold_right (fun arg cks -> arg.expr_clock :: cks) el [eq.eq_rhs.expr_clock] in

    let call_ck = Clock_calculus.compute_root_clock (Clock_predef.ck_tuple env_cks) in

    (*Clocks.new_var true in

    Format.eprintf "call %a: %a: %a@," Printers.pp_expr eq.eq_rhs Clocks.print_ck (Clock_predef.ck_tuple env_cks) Clocks.print_ck call_ck;*)

open Utils

    ignore (Modules.load_header ISet.empty header);

  (* Parsing source *)

  (* Removing automata *) 

  let prog = Automata.expand_decls prog in

  (* Importing source *)

  let _ = Modules.load_program ISet.empty prog in

(*Format.eprintf "Modules.add_type %B %s %a (owner=%s)@." itf name Printers.pp_typedef (typedef_of_top value) value.top_decl_owner;*)

    var_orig = false;

  let split_defs = Splitting.tuple_split_eq_list defs in

    annots = List.map (fun v ->

      let eq =

	try

	  List.find (fun eq -> eq.eq_lhs = [v.var_id]) split_defs 

	with Not_found -> (Format.eprintf "var not found %s@." v.var_id; assert false) in

      let expr = substitute_expr diff_vars split_defs eq.eq_rhs in

      let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in

      (["horn_backend";"trace"], pair)

    ) diff_vars;

   if so, update elim and return the remove flag,

let mkvar_decl x = mkvar_decl (get_loc ()) ~orig:true x

 STATE UIDENT COL unless_list locals LET stmt_list TEL until_list { Automata.mkhandler (get_loc ()) $2 $4 $9 $5 $7 }

| node_ident LPAR expr RPAR EVERY expr

    {mkexpr (Expr_appl ($1, $3, Some $6))}

| node_ident LPAR tuple_expr RPAR EVERY expr

    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some $6)) }

    { List.map (fun id -> mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, false)) $1 }

    { List.map (fun id -> mkvar_decl (id, mktyp $3, $4, false)) $1 }

    { List.map (fun id -> mkvar_decl (id, mktyp $4, mkclock Ckdec_any, true)) $2 }

  | Some c -> fprintf fmt "%t every (%a)" (fun fmt -> pp_call fmt id e) pp_expr c 

  Format.fprintf fmt "unless %a %a %s@ "

  Format.fprintf fmt "until %a %a %s@ "

  Format.fprintf fmt "state %s ->@ @[<v 2>  %a%alet@,@[<v 2>  %a@]@,tel%a@]"

    (Utils.fprintf_list ~sep:"@," pp_unless) handler.hand_unless

    (Utils.fprintf_list ~sep:"@," pp_until) handler.hand_until

  Format.fprintf fmt "@[<v 0>automaton %s@,%a@]"

(* Filters out normalization variables and renames instance variables to keep things readable,

   in a case of a dependency error *)

let filter_original n vl =

 List.fold_right (fun v res ->

   if ExprDep.is_instance_var v then Format.sprintf "node %s" (ExprDep.undo_instance_var v) :: res else

   let vdecl = get_node_var v n in

   if vdecl.var_orig then v :: res else res) vl []

  let node_vars = get_node_vars n in

    let disjoint = Disjunction.clock_disjoint_map node_vars in

  with (Causality.Cycle vl) as exc ->

    let vl = filter_original n vl in

    pp_error Format.err_formatter vl;

    | Some c -> 

      check_constant expr.expr_loc const false;	

      type_subtyping_arg env in_main const c Type_predef.type_bool);

./tests/automata/aut1.lus