Project

General

Profile

« Previous | Next » 

Revision 67ef9395

Added by Pierre-Loïc Garoche almost 3 years ago

minor bugs solved in printer: guarantee vs guarantees in cocospec. Imported node shall not be printed as regular code since it is not part of the grammar yet. Kept them as comment.

View differences:

src/printers.ml
316 316
  
317 317
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt s -> pp_spec_stmt fmt s) fmt spec.stmts;
318 318
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt r -> fprintf fmt "assume %a;" pp_eexpr r) fmt spec.assume;
319
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt r -> fprintf fmt "guarantees %a;" pp_eexpr r) fmt spec.guarantees;
319
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt r -> fprintf fmt "guarantee %a;" pp_eexpr r) fmt spec.guarantees;
320 320
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt mode ->
321 321
    fprintf fmt "mode %s (@[<v 0>%a@ %a@]);" 
322 322
      mode.mode_id
......
368 368
                      original information with the computed one in
369 369
                      nd. *)
370 370
     let pp_l = fprintf_list ~sep:"," pp_var_name in
371
     fprintf fmt "@[<hov 2>(*@@ contract import %s(%a) returns (%a)@]*)@ "
371
     fprintf fmt "@[<hov 2>(*@@ contract import %s(%a) returns (%a); @]*)@ "
372 372
       name
373 373
       pp_l inl
374 374
       pp_l outl
......
452 452
let pp_decl fmt decl =
453 453
  match decl.top_decl_desc with
454 454
  | Node nd -> fprintf fmt "%a" pp_node nd
455
  | ImportedNode ind ->
456
     fprintf fmt "imported %a;" pp_imported_node ind
455
  | ImportedNode ind -> (* We do not print imported nodes *)
456
     fprintf fmt "(* imported %a; *)" pp_imported_node ind
457 457
  | Const c -> fprintf fmt "const %a" pp_const_decl c
458 458
  | Open (local, s) -> if local then fprintf fmt "#open \"%s\"" s else fprintf fmt "#open <%s>" s
459 459
  | Include s -> fprintf fmt "include \"%s\"" s

Also available in: Unified diff