Project

General

Profile

Revision 217837e2 src/printers.ml

View differences:

src/printers.ml
289 289
    (fun fmt -> match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
290 290
    pp_expr e.eexpr_qfexpr
291 291

  
292
    
293
let pp_spec_eq fmt eq = 
294
  fprintf fmt "var %a : %a = %a;" 
295
    pp_eq_lhs eq.eq_lhs
296
    Types.print_node_ty eq.eq_rhs.expr_type
297
    pp_expr eq.eq_rhs
298
  
299
let pp_spec_stmt fmt stmt =
300
  match stmt with
301
  | Eq eq -> pp_spec_eq fmt eq
302
  | Aut aut -> assert false (* Not supported yet *)
303
             
304
  
292 305
let pp_spec fmt spec =
293
  fprintf fmt "@[<hov 2>(*@@ ";
294 306
  (* const are prefixed with const in pp_var and with nothing for regular
295 307
     variables. We adapt the call to produce the appropriate output. *)
296
  fprintf_list ~sep:"@,@@ " (fun fmt v ->
297
    fprintf fmt "%s%a = %t;"
298
      (if v.var_dec_const then "" else "var")
308
    fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt v ->
309
    fprintf fmt "const %a = %t;"
299 310
      pp_var v
300
      (fun fmt -> match v.var_dec_value with None -> () | Some e -> pp_expr fmt e)
301
  ) fmt (spec.consts @ spec.locals);
302
  fprintf_list ~sep:"@,@@ " (fun fmt r -> fprintf fmt "assume %a;" pp_eexpr r) fmt spec.assume;
303
  fprintf_list ~sep:"@,@@ " (fun fmt r -> fprintf fmt "guarantees %a;" pp_eexpr r) fmt spec.guarantees;
304
  fprintf_list ~sep:"@,@@ " (fun fmt mode ->
311
      (fun fmt -> match v.var_dec_value with None -> assert false | Some e -> pp_expr fmt e)
312
    ) fmt spec.consts;
313
  
314
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt s -> pp_spec_stmt fmt s) fmt spec.stmts;
315
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt r -> fprintf fmt "assume %a;" pp_eexpr r) fmt spec.assume;
316
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt r -> fprintf fmt "guarantees %a;" pp_eexpr r) fmt spec.guarantees;
317
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt mode ->
305 318
    fprintf fmt "mode %s (@[@ %a@ %a@]);" 
306 319
      mode.mode_id
307
      (fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "require %a;" pp_eexpr r)) mode.require
308
      (fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "ensure %a;" pp_eexpr r)) mode.ensure
320
      (fprintf_list ~eol:"@," ~sep:"@ " (fun fmt r -> fprintf fmt "require %a;" pp_eexpr r)) mode.require
321
      (fprintf_list ~eol:"@," ~sep:"@ " (fun fmt r -> fprintf fmt "ensure %a;" pp_eexpr r)) mode.ensure
309 322
  ) fmt spec.modes;
310
  fprintf_list ~sep:"@,@@ " (fun fmt import ->
323
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt import ->
311 324
    fprintf fmt "import %s (%a) returns (%a);" 
312 325
      import.import_nodeid
313 326
      (fprintf_list ~sep:"@ " pp_expr) import.inputs
314 327
      (fprintf_list ~sep:"@ " pp_expr) import.outputs
315
  ) fmt spec.imports;
316
  fprintf fmt "@]*)";
317
  ()
328
  ) fmt spec.imports
318 329

  
330
let pp_spec_as_comment fmt spec =
331
  fprintf fmt "@[<hov 2>(*@@ ";
332
  pp_spec fmt spec;
333
  fprintf fmt "@]*)@ "
319 334
    
320 335
let pp_node fmt nd =
321 336
  fprintf fmt "@[<v 0>";
......
327 342
    pp_node_args nd.node_outputs;
328 343
  (* Contracts *)
329 344
  fprintf fmt "%a%t"
330
    (fun fmt s -> match s with Some s -> pp_spec fmt s | _ -> ()) nd.node_spec
345
    (fun fmt s -> match s with Some s -> pp_spec_as_comment fmt s | _ -> ()) nd.node_spec
331 346
    (fun fmt -> match nd.node_spec with None -> () | Some _ -> fprintf fmt "@ ");
332 347
  (* Locals *)
333 348
  fprintf fmt "%a" (fun fmt locals ->
......
361 376
(*fprintf fmt "@ /* Scheduling: %a */ @ " (fprintf_list ~sep:", " pp_print_string) (Scheduling.schedule_node nd)*)
362 377

  
363 378
let pp_imported_node fmt ind = 
364
  fprintf fmt "@[<v>%s %s (%a) returns (%a)@]"
379
  fprintf fmt "@[<v 0>";
380
  (* Prototype *)
381
  fprintf fmt  "%s @[<hov 0>%s (@[%a)@]@ returns (@[%a)@]@]@ "
365 382
    (if ind.nodei_stateless then "function" else "node")
366 383
    ind.nodei_id
367 384
    pp_node_args ind.nodei_inputs
368
    pp_node_args ind.nodei_outputs
385
    pp_node_args ind.nodei_outputs;
386
  (* Contracts *)
387
  fprintf fmt "%a%t"
388
    (fun fmt s -> match s with Some s -> pp_spec_as_comment fmt s | _ -> ()) ind.nodei_spec
389
    (fun fmt -> match ind.nodei_spec with None -> () | Some _ -> fprintf fmt "@ ");
390
  fprintf fmt "@]@ "
391
  
369 392

  
370 393
let pp_const_decl fmt cdecl =
371 394
  fprintf fmt "%s = %a;" cdecl.const_id pp_const cdecl.const_value

Also available in: Unified diff