CristalCaveGem » LustreC

(* We extract the annotation dealing with traceability *)

  List.map (fun m ->

    let traces : (ident * expr) list=

      let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in

    m, traces

  ) machines

let memories_old machines m =

  List.map (fun (p, v) ->

    let machine = match p with | [] -> m | (_,m')::_ -> m' in

    let traces = List.assoc machine (machines_traces machines) in

      (

	(* We take the expression associated to variable v in the trace

	   info *)

	   Printers.pp_expr (List.assoc v.var_id traces); *)

	p, List.assoc v.var_id traces

      )

      begin

	(* We keep the variable as is: we create an expression v *)

	(* eprintf "Unable to found variable %a in traces (%a)@."  pp_var v

	   (Utils.fprintf_list ~sep:", " pp_print_string) (List.map fst

	p, mkexpr Location.dummy_loc (Expr_ident v.var_id)

      end

  ) (compute_mems machines m)

let memories_next  machines m = (* We remove the topest pre in each expression *)

  List.map

    (fun (prefix, ee) ->

      	Printers.pp_expr ee;

      	assert false)

    (memories_old machines m)

let pp_prefix_rev fmt prefix =

    (List.rev prefix)

let traces_file fmt basename prog machines =

  fprintf fmt "<?xml version=\"1.0\"?>@.";

      let pp_var = pp_horn_var m in

      let memories_old = memories_old  machines m in

      let memories_next = memories_next  machines m in

      (* fprintf fmt "; Node %s@." m.mname.node_id; *)

      fprintf fmt "@[<v 2><Node name=\"%s\">@ " m.mname.node_id;

      let input_vars = (rename_machine_list m.mname.node_id m.mstep.step_inputs) in

      let output_vars = (rename_machine_list m.mname.node_id m.mstep.step_outputs) in

      fprintf fmt "<input name=\"%a\" type=\"%a\">%a</input>@ "

	(Utils.fprintf_list ~sep:" | " pp_var)  output_vars

	(Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_type fmt id.var_type)) output_vars

	(Utils.fprintf_list ~sep:" | " pp_var) (m.mstep.step_outputs);

      in

      let step_local_vars = (rename_current_list (full_memory_vars ~without_arrow:true machines m)) in

      fprintf fmt "@]@ </Node>";

     )) (List.rev machines);

  fprintf fmt "</Traces>@."

(* (Utils.fprintf_list ~sep:" | " (fun fmt (prefix, ee) -> fprintf fmt

   "%a%a" pp_prefix_rev prefix Printers.pp_expr ee)) memories_next; *)