Project

General

Profile

« Previous | Next » 

Revision a7062da6

Added by LĂ©lio Brun over 3 years ago

another step towards refactoring

View differences:

src/backends/Horn/horn_backend_traces.ml
14 14

  
15 15
   This is a modified version that handle reset *)
16 16

  
17
open Utils
17 18
open Format
18 19
open Lustre_types
19 20
open Corelang
......
22 23
open Horn_backend_printers
23 24

  
24 25
let pp_traces =
25
  Utils.fprintf_list ~sep:", " (fun fmt (v, e) ->
26
      Format.fprintf fmt "%s -> %a" v Printers.pp_expr e)
26
  pp_comma_list (fun fmt (v, e) -> fprintf fmt "%s -> %a" v Printers.pp_expr e)
27 27

  
28 28
(* Compute memories associated to each machine *)
29 29
let compute_mems machines m =
......
51 51
        let filtered =
52 52
          List.filter (fun (kwds, _) -> kwds = [ "traceability" ]) all_annots
53 53
        in
54
        (* List.iter (Format.eprintf "Annots: %a@." Printers.pp_expr_annot)
54
        (* List.iter (eprintf "Annots: %a@." Printers.pp_expr_annot)
55 55
           (m.mannot); *)
56 56
        let content = List.map snd filtered in
57 57
        (* Elements are supposed to be a pair (tuple): variable, expression *)
......
68 68
              assert false)
69 69
          content
70 70
      in
71
      (* Format.eprintf "Build traces: %a@." pp_traces traces; *)
71
      (* eprintf "Build traces: %a@." pp_traces traces; *)
72 72
      m, traces)
73 73
    machines
74 74

  
......
90 90
          (* eprintf "Unable to found variable %a in traces (%a)@."
91 91
             Printers.pp_var v * pp_traces traces; *)
92 92
          p,
93
          mkexpr Location.dummy_loc (Expr_ident v.var_id) ))
93
          mkexpr Location.dummy (Expr_ident v.var_id) ))
94 94
    (compute_mems machines m)
95 95

  
96 96
let memories_next machines m =
......
117 117
                  false)
118 118
              m.mname.node_stmts
119 119
          with _ ->
120
            Format.eprintf
120
            eprintf
121 121
              "Unable to find definition of %s in stmts %a@.prefix=%a@.@?"
122 122
              var_id Printers.pp_node_stmts m.mname.node_stmts
123
              (Utils.fprintf_list ~sep:"," (fun fmt (id, n) ->
123
              (pp_comma_list (fun fmt (id, n) ->
124 124
                   fprintf fmt "(%s,%s)" id n.mname.node_id))
125 125
              (List.rev prefix);
126 126

  
......
140 140
        prefix, def
141 141
      | _ ->
142 142
        eprintf "Mem Failure: (prefix: %a, eexpr: %a)@.@?"
143
          (Utils.fprintf_list ~sep:"," (fun fmt (id, n) ->
143
          (pp_comma_list (fun fmt (id, n) ->
144 144
               fprintf fmt "(%s,%s)" id n.mname.node_id))
145 145
          (List.rev prefix) Printers.pp_expr ee;
146 146
        assert false)
147 147
    (memories_old machines m)
148 148

  
149 149
let pp_prefix_rev fmt prefix =
150
  Utils.fprintf_list ~sep:"."
150
  pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt ".")
151 151
    (fun fmt (id, n) -> fprintf fmt "(%s,%s)" id n.mname.node_id)
152 152
    fmt (List.rev prefix)
153 153

  
154 154
let traces_file fmt machines =
155
  let pp_l = pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt " | ") in
155 156
  fprintf fmt "<?xml version=\"1.0\"?>@.";
156 157
  fprintf fmt
157 158
    "<Traces xmlns:xsi=\"http://www.w3.org/2001/XMLSchema-instance\">@.";
158 159
  fprintf fmt "@[<v 5>@ %a@ @]@."
159
    (Utils.fprintf_list ~sep:"@ " (fun fmt m ->
160
    (pp_print_list (fun fmt m ->
160 161
         let pp_var = pp_horn_var m in
161 162
         let memories_old = memories_old machines m in
162 163
         let memories_next = memories_next machines m in
......
171 172
           rename_machine_list m.mname.node_id m.mstep.step_outputs
172 173
         in
173 174
         fprintf fmt "<input name=\"%a\" type=\"%a\">%a</input>@ "
174
           (Utils.fprintf_list ~sep:" | " (pp_horn_var m))
175
           input_vars
176
           (Utils.fprintf_list ~sep:" | " (fun fmt id ->
177
                pp_type fmt id.var_type))
178
           input_vars
179
           (Utils.fprintf_list ~sep:" | " (pp_horn_var m))
180
           m.mstep.step_inputs;
175
           (pp_l (pp_horn_var m)) input_vars
176
           (pp_l (fun fmt id -> pp_type fmt id.var_type)) input_vars
177
           (pp_l (pp_horn_var m)) m.mstep.step_inputs;
181 178

  
182 179
         fprintf fmt "<output name=\"%a\" type=\"%a\">%a</output>@ "
183
           (Utils.fprintf_list ~sep:" | " pp_var)
184
           output_vars
185
           (Utils.fprintf_list ~sep:" | " (fun fmt id ->
186
                pp_type fmt id.var_type))
187
           output_vars
188
           (Utils.fprintf_list ~sep:" | " pp_var)
189
           m.mstep.step_outputs;
180
           (pp_l pp_var) output_vars
181
           (pp_l (fun fmt id -> pp_type fmt id.var_type)) output_vars
182
           (pp_l pp_var) m.mstep.step_outputs;
190 183

  
191 184
         let local_vars =
192 185
           try full_memory_vars ~without_arrow:true machines m
193 186
           with Not_found ->
194
             Format.eprintf "machine %s@.@?" m.mname.node_id;
187
             eprintf "machine %s@.@?" m.mname.node_id;
195 188
             assert false
196 189
         in
197 190
         let init_local_vars = rename_next_list local_vars in
198 191
         let step_local_vars = rename_current_list local_vars in
199 192

  
200 193
         fprintf fmt "<localInit name=\"%a\" type=\"%a\">%t%a</localInit>@ "
201
           (Utils.fprintf_list ~sep:" | " pp_var)
202
           init_local_vars
203
           (Utils.fprintf_list ~sep:" | " (fun fmt id ->
204
                pp_type fmt id.var_type))
194
           (pp_l pp_var)
205 195
           init_local_vars
196
           (pp_l (fun fmt id -> pp_type fmt id.var_type)) init_local_vars
206 197
           (fun fmt ->
207 198
             match memories_next with [] -> () | _ -> fprintf fmt "")
208
           (Utils.fprintf_list ~sep:" | " (fun fmt (_, ee) ->
209
                fprintf fmt "%a" pp_xml_expr ee))
199
           (pp_l (fun fmt (_, ee) -> fprintf fmt "%a" pp_xml_expr ee))
210 200
           memories_next;
211 201

  
212 202
         fprintf fmt "<localStep name=\"%a\" type=\"%a\">%t%a</localStep>@ "
213
           (Utils.fprintf_list ~sep:" | " pp_var)
214
           step_local_vars
215
           (Utils.fprintf_list ~sep:" | " (fun fmt id ->
216
                pp_type fmt id.var_type))
217
           step_local_vars
203
           (pp_l pp_var) step_local_vars
204
           (pp_l (fun fmt id -> pp_type fmt id.var_type)) step_local_vars
218 205
           (fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt "")
219
           (Utils.fprintf_list ~sep:" | " (fun fmt (_, ee) ->
220
                fprintf fmt "(%a)" pp_xml_expr ee))
206
           (pp_l (fun fmt (_, ee) -> fprintf fmt "(%a)" pp_xml_expr ee))
221 207
           memories_old;
222 208

  
223 209
         let arrow_vars = arrow_vars machines m in
224 210
         let arrow_vars_curr = rename_current_list arrow_vars
225 211
         and arrow_vars_mid = rename_mid_list arrow_vars
226 212
         and arrow_vars_next = rename_next_list arrow_vars in
227
         Utils.fprintf_list ~sep:"@ "
228
           (fun fmt v -> fprintf fmt "<reset name=\"%a\"/>" pp_var v)
213
         pp_print_list (fun fmt v -> fprintf fmt "<reset name=\"%a\"/>" pp_var v)
229 214
           fmt
230 215
           (arrow_vars_curr @ arrow_vars_mid @ arrow_vars_next);
231 216
         fprintf fmt "@]@ </Node>"))

Also available in: Unified diff