Project

General

Profile

Revision c02d255e src/printers.ml

View differences:

src/printers.ml
60 60
    | Expr_power (a, d) -> fprintf fmt "(%a^%a)" pp_expr a Dimension.pp_dimension d
61 61
    | Expr_tuple el -> fprintf fmt "(%a)" pp_tuple el
62 62
    | Expr_ite (c, t, e) -> fprintf fmt "(if %a then %a else %a)" pp_expr c pp_expr t pp_expr e
63
    | Expr_arrow (e1, e2) -> fprintf fmt "%a -> %a" pp_expr e1 pp_expr e2
63
    | Expr_arrow (e1, e2) -> fprintf fmt "(%a -> %a)" pp_expr e1 pp_expr e2
64 64
    | Expr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_expr e1 pp_expr e2
65 65
    | Expr_pre e -> fprintf fmt "pre %a" pp_expr e
66 66
    | Expr_when (e, id, l) -> fprintf fmt "%a when %s(%s)" pp_expr e l id
......
101 101
    | "!=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_expr e1 pp_expr e2
102 102
    | "=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a = %a)" pp_expr e1 pp_expr e2
103 103
    | "not", _ -> fprintf fmt "(not %a)" pp_expr e
104
    | _ -> fprintf fmt "%s (%a)" id pp_expr e)
104
    | _, Expr_tuple _ -> fprintf fmt "%s %a" id pp_expr e
105
    | _ -> fprintf fmt "%s (%a)" id pp_expr e
106
)
105 107
  | Some (x, l) -> fprintf fmt "%s (%a) every %s(%s)" id pp_expr e l x 
106 108
	
107 109
let pp_node_eq fmt eq = 
......
138 140
(*     | Ttuple tel -> fprintf_list ~sep:" * " pp_var_type fmt tel *)
139 141
(*   ) *)
140 142

  
143

  
144
let pp_econst fmt c = 
145
  match c with
146
    | EConst_int i -> pp_print_int fmt i
147
    | EConst_real r -> pp_print_string fmt r
148
    | EConst_float r -> pp_print_float fmt r
149
    | EConst_bool b -> pp_print_bool fmt b
150
    | EConst_string s -> pp_print_string fmt ("\"" ^ s ^ "\"")
151

  
152
let rec pp_eexpr fmt eexpr = 
153
  match eexpr.eexpr_desc with
154
    | EExpr_const c -> pp_econst fmt c
155
    | EExpr_ident id -> pp_print_string fmt id
156
    | EExpr_tuple el -> fprintf_list ~sep:"," pp_eexpr fmt el
157
    | EExpr_arrow (e1, e2) -> fprintf fmt "%a -> %a" pp_eexpr e1 pp_eexpr e2
158
    | EExpr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_eexpr e1 pp_eexpr e2
159
    (* | EExpr_concat (e1, e2) -> fprintf fmt "%a::%a" pp_eexpr e1 pp_eexpr e2 *)
160
    (* | EExpr_tail e -> fprintf fmt "tail %a" pp_eexpr e *)
161
    | EExpr_pre e -> fprintf fmt "pre %a" pp_eexpr e
162
    | EExpr_when (e, id) -> fprintf fmt "%a when %s" pp_eexpr e id
163
    | EExpr_merge (id, e1, e2) -> 
164
      fprintf fmt "merge (%s, %a, %a)" id pp_eexpr e1 pp_eexpr e2
165
    | EExpr_appl (id, e, r) -> pp_eapp fmt id e r
166
    | EExpr_forall (vars, e) -> fprintf fmt "forall %a; %a" pp_node_args vars pp_eexpr e 
167
    | EExpr_exists (vars, e) -> fprintf fmt "exists %a; %a" pp_node_args vars pp_eexpr e 
168

  
169

  
170
    (* | EExpr_whennot _ *)
171
    (* | EExpr_uclock _ *)
172
    (* | EExpr_dclock _ *)
173
    (* | EExpr_phclock _ -> assert false *)
174
and pp_eapp fmt id e r =
175
  match r with
176
  | None ->
177
    (match id, e.eexpr_desc with
178
    | "+", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_eexpr e1 pp_eexpr e2
179
    | "uminus", _ -> fprintf fmt "(- %a)" pp_eexpr e
180
    | "-", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_eexpr e1 pp_eexpr e2
181
    | "*", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_eexpr e1 pp_eexpr e2
182
    | "/", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_eexpr e1 pp_eexpr e2
183
    | "mod", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_eexpr e1 pp_eexpr e2
184
    | "&&", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a && %a)" pp_eexpr e1 pp_eexpr e2
185
    | "||", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a || %a)" pp_eexpr e1 pp_eexpr e2
186
    | "xor", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ^^ %a)" pp_eexpr e1 pp_eexpr e2
187
    | "impl", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ==> %a)" pp_eexpr e1 pp_eexpr e2
188
    | "<", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_eexpr e1 pp_eexpr e2
189
    | "<=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_eexpr e1 pp_eexpr e2
190
    | ">", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_eexpr e1 pp_eexpr e2
191
    | ">=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_eexpr e1 pp_eexpr e2
192
    | "!=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_eexpr e1 pp_eexpr e2
193
    | "=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a == %a)" pp_eexpr e1 pp_eexpr e2
194
    | "not", _ -> fprintf fmt "(! %a)" pp_eexpr e
195
    | "ite", EExpr_tuple([e1;e2;e3]) -> fprintf fmt "(if %a then %a else %a)" pp_eexpr e1 pp_eexpr e2 pp_eexpr e3
196
    | _ -> fprintf fmt "%s (%a)" id pp_eexpr e)
197
  | Some x -> fprintf fmt "%s (%a) every %s" id pp_eexpr e x 
198

  
199
  
200
let pp_ensures fmt e =
201
  match e with
202
    | EnsuresExpr e -> fprintf fmt "ensures %a;@ " pp_eexpr e
203
    | SpecObserverNode (name, args) -> fprintf fmt "observer %s (%a);@ " name (fprintf_list ~sep:", " pp_eexpr) args
204
 
205
let pp_spec fmt spec =
206
  fprintf fmt "@[<hov 2>(*@@ ";
207
  fprintf_list ~sep:"" (fun fmt r -> fprintf fmt "requires %a;@ " pp_eexpr r) fmt spec.requires;
208
  fprintf_list ~sep:"" pp_ensures fmt spec.ensures;
209
  fprintf_list ~sep:"@ " (fun fmt (name, assumes, requires) -> 
210
    fprintf fmt "behavior %s:@[@ %a@ %a@]" 
211
      name
212
      (fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "assumes %a;" pp_eexpr r)) assumes
213
      (fprintf_list ~sep:"@ " pp_ensures) requires
214
  ) fmt spec.behaviors;
215
  fprintf fmt "@]*)";
216
  ()
217

  
141 218
let pp_node fmt nd = 
142
fprintf fmt "@[<v>node %s (%a) returns (%a)@ %a%alet@ @[<h 2>   @ @[%a@]@ @]@ tel@]@ "
219
fprintf fmt "@[<v 0>%a%tnode %s (%a) returns (%a)@.%a%alet@.@[<h 2>   @ @[%a@]@ @]@.tel@]@."
220
  (fun fmt s -> match s with Some s -> pp_spec fmt s | _ -> ()) nd.node_spec
221
  (fun fmt -> match nd.node_spec with None -> () | Some _ -> Format.fprintf fmt "@.") 
143 222
  nd.node_id
144 223
  pp_node_args nd.node_inputs
145 224
  pp_node_args nd.node_outputs
......
212 291
      pp_node_args nd.node_outputs
213 292
  | ImportedNode _ | ImportedFun _ | Consts _ | Open _ -> ()
214 293

  
215
let pp_econst fmt c = 
216
  match c with
217
    | EConst_int i -> pp_print_int fmt i
218
    | EConst_real r -> pp_print_string fmt r
219
    | EConst_float r -> pp_print_float fmt r
220
    | EConst_bool b -> pp_print_bool fmt b
221
    | EConst_string s -> pp_print_string fmt ("\"" ^ s ^ "\"")
222 294

  
223
let rec pp_eexpr is_output fmt eexpr = 
224
  let pp_eexpr = pp_eexpr is_output in
225
  match eexpr.eexpr_desc with
226
    | EExpr_const c -> pp_econst fmt c
227
    | EExpr_ident id -> 
228
      if is_output id then pp_print_string fmt ("*" ^ id) else pp_print_string fmt id
229
    | EExpr_tuple el -> fprintf_list ~sep:"," pp_eexpr fmt el
230
    | EExpr_arrow (e1, e2) -> fprintf fmt "%a -> %a" pp_eexpr e1 pp_eexpr e2
231
    | EExpr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_eexpr e1 pp_eexpr e2
232
    | EExpr_concat (e1, e2) -> fprintf fmt "%a::%a" pp_eexpr e1 pp_eexpr e2
233
    | EExpr_tail e -> fprintf fmt "tail %a" pp_eexpr e
234
    | EExpr_pre e -> fprintf fmt "pre %a" pp_eexpr e
235
    | EExpr_when (e, id) -> fprintf fmt "%a when %s" pp_eexpr e id
236
    | EExpr_merge (id, e1, e2) -> 
237
      fprintf fmt "merge (%s, %a, %a)" id pp_eexpr e1 pp_eexpr e2
238
    | EExpr_appl (id, e, r) -> pp_eapp is_output fmt id e r
239
    | EExpr_forall (vars, e) -> fprintf fmt "forall %a; %a" pp_node_args vars pp_eexpr e 
240
    | EExpr_exists (vars, e) -> fprintf fmt "exists %a; %a" pp_node_args vars pp_eexpr e 
241

  
242

  
243
    | EExpr_whennot _
244
    | EExpr_uclock _
245
    | EExpr_dclock _
246
    | EExpr_phclock _ -> assert false
247
and pp_eapp is_output fmt id e r =
248
  let pp_eexpr = pp_eexpr is_output in
249
  match r with
250
  | None ->
251
    (match id, e.eexpr_desc with
252
    | "+", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_eexpr e1 pp_eexpr e2
253
    | "uminus", _ -> fprintf fmt "(- %a)" pp_eexpr e
254
    | "-", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_eexpr e1 pp_eexpr e2
255
    | "*", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_eexpr e1 pp_eexpr e2
256
    | "/", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_eexpr e1 pp_eexpr e2
257
    | "mod", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_eexpr e1 pp_eexpr e2
258
    | "&&", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a && %a)" pp_eexpr e1 pp_eexpr e2
259
    | "||", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a || %a)" pp_eexpr e1 pp_eexpr e2
260
    | "xor", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ^^ %a)" pp_eexpr e1 pp_eexpr e2
261
    | "impl", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ==> %a)" pp_eexpr e1 pp_eexpr e2
262
    | "<", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_eexpr e1 pp_eexpr e2
263
    | "<=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_eexpr e1 pp_eexpr e2
264
    | ">", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_eexpr e1 pp_eexpr e2
265
    | ">=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_eexpr e1 pp_eexpr e2
266
    | "!=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_eexpr e1 pp_eexpr e2
267
    | "=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a == %a)" pp_eexpr e1 pp_eexpr e2
268
    | "not", _ -> fprintf fmt "(! %a)" pp_eexpr e
269
    | "ite", EExpr_tuple([e1;e2;e3]) -> fprintf fmt "(if %a then %a else %a)" pp_eexpr e1 pp_eexpr e2 pp_eexpr e3
270
    | _ -> fprintf fmt "%s (%a)" id pp_eexpr e)
271
  | Some x -> fprintf fmt "%s (%a) every %s" id pp_eexpr e x 
272

  
273
  
274
let pp_ensures is_output fmt e =
275
  let pp_eexpr = pp_eexpr is_output in
276
  match e with
277
    | EnsuresExpr e -> fprintf fmt "ensures %a;@ " pp_eexpr e
278
    | SpecObserverNode (name, args) -> fprintf fmt "observer %s (%a);@ " name (fprintf_list ~sep:", " pp_eexpr) args
279
 
280
let pp_acsl_spec outputs fmt spec =
281
  let is_output = fun oid -> List.exists (fun v -> v.var_id = oid) outputs in
282
  let pp_eexpr = pp_eexpr is_output in
283
  fprintf fmt "@[<v 2>/*@@ ";
284
  fprintf_list ~sep:"" (fun fmt r -> fprintf fmt "requires %a;@ " pp_eexpr r) fmt spec.requires;
285
  fprintf_list ~sep:"" (pp_ensures is_output) fmt spec.ensures;
286
  fprintf fmt "@ ";
287
  (* fprintf fmt "assigns *self%t%a;@ "  *)
288
  (*   (fun fmt -> if List.length outputs > 0 then fprintf fmt ", ") *)
289
  (*   (fprintf_list ~sep:"," (fun fmt v -> fprintf fmt "*%s" v.var_id)) outputs; *)
290
  fprintf_list ~sep:"@ " (fun fmt (name, assumes, requires) -> 
291
    fprintf fmt "behavior %s:@[@ %a@ %a@]" 
292
      name
293
      (fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "assumes %a;" pp_eexpr r)) assumes
294
      (fprintf_list ~sep:"@ " (pp_ensures is_output)) requires
295
  ) fmt spec.behaviors;
296
  fprintf fmt "@]@ */@.";
297
  ()
298 295

  
299 296

  
300 297
let pp_lusi_header fmt filename prog =

Also available in: Unified diff