Project

General

Profile

Revision 0d54d8a8 src/printers.ml

View differences:

src/printers.ml
367 367
  | Const c -> fprintf fmt "const %a" pp_const_decl c
368 368
  | Open (local, s) -> if local then fprintf fmt "#open \"%s\"" s else fprintf fmt "#open <%s>" s
369 369
  | TypeDef tdef -> fprintf fmt "%a" pp_typedef tdef
370
  | Contract c -> pp_spec fmt c (* TODO: may be we need to produce it outside of comments.To be discussed *)
371 370
  
372 371
let pp_prog fmt prog =
373 372
  (* we first print types: the function SortProg.sort could do the job but ut
......
385 384
  | Const c -> fprintf fmt "const %a@ " pp_const_decl c
386 385
  | Open (local, s) -> if local then fprintf fmt "#open \"%s\"@ " s else fprintf fmt "#open <%s>@ " s
387 386
  | TypeDef tdef -> fprintf fmt "type %s;@ " tdef.tydef_id
388
  | Contract c -> fprintf fmt "(*@ contract *)@ "
389

  
387
  
390 388
let pp_lusi fmt decl = 
391 389
  match decl.top_decl_desc with
392 390
  | ImportedNode ind -> fprintf fmt "%a;@ " pp_imported_node ind
......
394 392
  | Open (local, s) -> if local then fprintf fmt "#open \"%s\"@ " s else fprintf fmt "#open <%s>@ " s
395 393
  | TypeDef tdef -> fprintf fmt "%a@ " pp_typedef tdef
396 394
  | Node _ -> assert false
397
  | Contract c -> pp_spec fmt c (* TODO idem pp_node: how to print contract in lusi, within/without comments brackets ? *)
398 395
                
399 396
let pp_lusi_header fmt basename prog =
400 397
  fprintf fmt "@[<v 0>";

Also available in: Unified diff