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