Revision c6c8786b
Added by Pierre-Loïc Garoche almost 4 years ago
| 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
kind2 output for printer. global option available