Project

General

Profile

« Previous | Next » 

Revision c6c8786b

Added by Pierre-Loïc Garoche over 2 years ago

kind2 output for printer. global option available

View differences:

src/printers.ml
348 348
      stmts = nd.node_stmts @ c.stmts;
349 349
    }
350 350
  )
351
  
351

  
352
(* Printing top contract as comments in regular output and as contract
353
   in kind2 *)
352 354
let pp_contract fmt nd =    
353
  
354
  let c = node_as_contract nd in
355
  fprintf fmt "@[<v 2>(*@contract %s(%a) returns (%a);@ "
355
   let c = node_as_contract nd in
356
  fprintf fmt "@[<v 2>%scontract %s(%a) returns (%a);@ "
357
    (if !Options.kind2_print then "" else "(*@")
356 358
    nd.node_id
357 359
    pp_node_args nd.node_inputs
358 360
    pp_node_args nd.node_outputs;
359 361
  fprintf fmt "@[<v 2>let@ ";
360 362
  pp_spec fmt c;
361
  fprintf fmt "@]@ tel@ @]*)@ "        
363
  fprintf fmt "@]@ tel@ @]%s@ "
364
  (if !Options.kind2_print then "" else "*)")
362 365
    
363 366
let pp_spec_as_comment fmt (inl, outl, spec) =
364 367
  match spec with

Also available in: Unified diff