CristalCaveGem » LustreC

    | Expr_appl(_,_,reset) -> (

      match reset with None -> false | Some _ -> true

    )

  )

  | None -> assert false (* should have been assigned to an original lustre equation *)

      ISet.union accu_def common_def_vars,

      VSet.union accu_read read_vars)

    (ISet.empty, ISet.empty, VSet.empty) il

and branch_instr_vars m i =

  match Corelang.get_instr_desc i with

  | MLocalAssign (var,expr) 

  | MStep (vars, f, args)  ->

     let is_stateful = List.mem_assoc f m.minstances in 

     let lhs = ISet.of_list (List.map (fun v -> v.var_id) vars) in

     )

  | MBranch (g,(_,hd_il)::tl)     -> (* We focus on variables defined in all branches *)

     let read_guard = get_expr_vars g in

     let all_def_vars_hd, def_vars_hd, read_vars_hd = branch_block_vars m hd_il in

     let all_def_vars, def_vars, read_vars =

       List.fold_left

	 (all_def_vars_hd, def_vars_hd, read_vars_hd)

	 tl

     in

     all_def_vars, def_vars, VSet.union read_guard read_vars

  | MBranch _ -> assert false (* branch instruction should admit at least one case *)

  | MReset ni           

     let write = ISet.singleton (reset_name ni) in

     write, write, VSet.empty

(* A kind of super join_guards: all MBranch are postponed and sorted by

   guards so they can be easier merged *)

    | MStep(outputs, f, inputs ) -> (* This is an imported node *)

       EMF_library_calls.pp_call fmt m f outputs inputs

      -> Format.eprintf "unhandled comment in EMF@.@?"; assert false

  (* not  available for EMF output *)

  in

  fprintf fmt "{@[";

  fprintf fmt "\"mode_id\": \"%s\",@ "

    m.mode_id;

    pp_emf_eexprs m.ensure;

    pp_emf_eexprs m.require;

  fprintf fmt "@]}"

let pp_emf_spec fmt spec =

  fprintf fmt "{ @[<hov 0>";

  fprintf fmt "\"assume\": [%a],@ "

    pp_emf_eexprs spec.assume;

  fprintf fmt "\"guarantees\": [%a],@ "

    pp_emf_eexprs spec.guarantees;

    pp_emf_spec_modes spec.modes;

  fprintf fmt "@] }"

let pp_emf_annots cpt fmt annots = fprintf_list ~sep:",@ " (pp_emf_annot cpt) fmt annots.annots

let pp_emf_annots_list cpt fmt annots_list = fprintf_list ~sep:",@ " (pp_emf_annots cpt) fmt annots_list

let pp_machine fmt m =

  let instrs = (*merge_branches*) m.mstep.step_instrs in

  try

    fprintf fmt "@[<v 2>\"%a\": {@ "

      print_protect (fun fmt -> pp_print_string fmt m.mname.node_id);

    fprintf fmt "\"imported\": \"false\",@ ";

    fprintf fmt "\"kind\": %t,@ "

      (fun fmt -> if not ( snd (get_stateless_status m) )

    fprintf fmt "\"instrs\": {@[<v 0> %a@]@ },@ "

      (pp_emf_instrs m) instrs;

    (match m.mspec with | None -> () 

    );

    fprintf fmt "\"annots\": {@[<v 0> %a@]@ }" (pp_emf_annots_list (ref 0)) m.mannot;

    fprintf fmt "@]@ }"

    eprintf "node skipped - no output generated@ @]@."

  )

  match m.mspec with

  | None | Some (NodeSpec _) -> pp_machine fmt m

let pp_emf_imported_node fmt top =

  let ind = Corelang.imported_node_of_top top in

  try

  match dec_t with

  | Tydec_any -> (* Dynamical built variable. No declared type. Shall

                    use the infered one. *)

  | Tydec_int -> fprintf fmt "{ \"kind\": \"int\" }" (* !Options.int_type *)

  | Tydec_real -> fprintf fmt "{ \"kind\": \"real\" }" (* !Options.real_type *)

  (* TODO we could add more concrete types here if they were available in

(* Print the variable declaration *)

let pp_emf_var_decl fmt v =

    pp_var_name v

    pp_var_type v

    Printers.pp_var_name v

let pp_emf_cst c inf fmt =

  let pp_typ fmt =

  in

  match c with

  | Const_tag t->

    fprintf fmt "{@[\"type\": \"variable\",@ \"value\": \"%a\",@ "

      pp_var_name v;

    (*    fprintf fmt "\"original_name\": \"%a\",@ " Printers.pp_var_name v; *)

    fprintf fmt "@]}"

  )

  | _ -> eprintf "Not of cst or var: %a@." (pp_val m) v ; assert false (* Invalid argument *)

  | Expr_ident id ->

     fprintf fmt "{@[\"type\": \"variable\",@ \"value\": \"%a\",@ "

       print_protect (fun fmt -> pp_print_string fmt id);

      (pp_concrete_type

	 Tydec_any (* don't know much about that time since it was not

		      declared. That may not work with clock constants *)

      (fun fmt ->

	fprintf fmt "Warning: unhandled expression %a in annotation.@ "

	  Printers.pp_expr e;

      );    

    fprintf fmt "\"unhandled construct, complain to Ploc\""

  )

let pp_emf_exprs = pp_emf_list pp_emf_expr

let pp_emf_const fmt v =

    pp_var_name v

    pp_var_type v

    Printers.pp_var_name v

  | Eq eq -> (

    fprintf fmt "@[ @[<v 2>\"%a\": {@ " (Utils.fprintf_list ~sep:"_" pp_print_string) eq.eq_lhs;

    fprintf fmt "\"lhs\": [%a],@ " (Utils.fprintf_list ~sep:", " (fun fmt vid -> fprintf fmt "\"%s\"" vid)) eq.eq_lhs;

    fprintf fmt "@]@]@ }"

  )

let pp_emf_top_const fmt const_top = 

  let const = Corelang.const_of_top const_top in

(* Local Variables: *)

(* compile-command: "make -C ../.." *)

(* Print the instruction and update the set of reset instances *)

let rec pp_machine_instr machines reset_instances (m: machine_t) fmt instr : ident list =

  match get_instr_desc instr with

  | MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *)

    pp_no_reset machines m fmt i;

    i::reset_instances