Revision 217837e2
Added by Pierre-Loïc Garoche over 6 years ago
| 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
Unified compilation of lusi and lus files
Different parsers yet but shared process.
In case of lusi input the C backend is bypassed since the .h is generated from the lusic and no C code should be generated since it may overwrite existing manually written code
But