Project

General

Profile

Revision 9f77bff7 src/backends/Horn/horn_backend_traces.ml

View differences:

src/backends/Horn/horn_backend_traces.ml
39 39

  
40 40

  
41 41
(* We extract the annotation dealing with traceability *)
42
let machines_traces machines = 
42
let machines_traces machines =
43 43
  List.map (fun m ->
44 44
    let traces : (ident * expr) list=
45 45
      let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in
......
61 61
    m, traces
62 62

  
63 63
  ) machines
64
  
64

  
65 65
let memories_old machines m =
66 66
  List.map (fun (p, v) ->
67 67
    let machine = match p with | [] -> m | (_,m')::_ -> m' in
68 68
    let traces = List.assoc machine (machines_traces machines) in
69
    if List.mem_assoc v.var_id traces then 
69
    if List.mem_assoc v.var_id traces then
70 70
      (
71 71
	(* We take the expression associated to variable v in the trace
72 72
	   info *)
......
75 75
	   Printers.pp_expr (List.assoc v.var_id traces); *)
76 76
	p, List.assoc v.var_id traces
77 77
      )
78
    else 
78
    else
79 79
      begin
80 80

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

  
83 83
	(* eprintf "Unable to found variable %a in traces (%a)@."  pp_var v
84 84
	   (Utils.fprintf_list ~sep:", " pp_print_string) (List.map fst
85
	   traces); *)	    
85
	   traces); *)
86 86

  
87 87
	p, mkexpr Location.dummy_loc (Expr_ident v.var_id)
88 88
      end
89 89

  
90 90
  ) (compute_mems machines m)
91
      
91

  
92 92
let memories_next  machines m = (* We remove the topest pre in each expression *)
93 93
  List.map
94 94
    (fun (prefix, ee) ->
......
102 102
      	Printers.pp_expr ee;
103 103
      	assert false)
104 104
    (memories_old machines m)
105
      
105

  
106 106

  
107 107

  
108 108
let pp_prefix_rev fmt prefix =
109
  Utils.fprintf_list ~sep:"." 
110
    (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) 
111
    fmt 
109
  Utils.fprintf_list ~sep:"."
110
    (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id)
111
    fmt
112 112
    (List.rev prefix)
113
      
113

  
114 114

  
115 115
let traces_file fmt basename prog machines =
116 116
  fprintf fmt "<?xml version=\"1.0\"?>@.";
......
120 120
      let pp_var = pp_horn_var m in
121 121
      let memories_old = memories_old  machines m in
122 122
      let memories_next = memories_next  machines m in
123
      
123

  
124 124
      (* fprintf fmt "; Node %s@." m.mname.node_id; *)
125 125
      fprintf fmt "@[<v 2><Node name=\"%s\">@ " m.mname.node_id;
126
      
126

  
127 127
      let input_vars = (rename_machine_list m.mname.node_id m.mstep.step_inputs) in
128 128
      let output_vars = (rename_machine_list m.mname.node_id m.mstep.step_outputs) in
129 129
      fprintf fmt "<input name=\"%a\" type=\"%a\">%a</input>@ "
......
135 135
	(Utils.fprintf_list ~sep:" | " pp_var)  output_vars
136 136
	(Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_type fmt id.var_type)) output_vars
137 137
	(Utils.fprintf_list ~sep:" | " pp_var) (m.mstep.step_outputs);
138
      
139
      let init_local_vars = 
140
	
141
	  (rename_next_list (try full_memory_vars ~without_arrow:true machines m with Not_found -> Format.eprintf "mahine %s@.@?" m.mname.node_id; assert false)) 
142
	
138

  
139
      let init_local_vars =
140
	(rename_next_list
141
           (try full_memory_vars ~without_arrow:true machines m with Not_found -> Format.eprintf "mahine %s@.@?" m.mname.node_id; assert false))
142

  
143 143

  
144 144
      in
145 145
      let step_local_vars = (rename_current_list (full_memory_vars ~without_arrow:true machines m)) in
......
160 160
      fprintf fmt "@]@ </Node>";
161 161
     )) (List.rev machines);
162 162
  fprintf fmt "</Traces>@."
163
  
163

  
164 164

  
165 165
(* (Utils.fprintf_list ~sep:" | " (fun fmt (prefix, ee) -> fprintf fmt
166 166
   "%a%a" pp_prefix_rev prefix Printers.pp_expr ee)) memories_next; *)

Also available in: Unified diff