Revision 59020713
Added by Pierre-Loïc Garoche almost 6 years ago
| src/backends/EMF/EMF_backend.ml | ||
|---|---|---|
| 375 | 375 |
pp_emf_eexpr ee |
| 376 | 376 |
in |
| 377 | 377 |
incr cpt |
| 378 |
|
|
| 379 |
let pp_emf_spec_mode fmt m = |
|
| 380 |
fprintf fmt "{@[";
|
|
| 381 |
fprintf fmt "\"mode_id\": \"%s\",@ " |
|
| 382 |
m.mode_id; |
|
| 383 |
fprintf fmt "\"require\": [%a],@ " |
|
| 384 |
pp_emf_eexprs m.ensure; |
|
| 385 |
fprintf fmt "\"require\": [%a],@ " |
|
| 386 |
pp_emf_eexprs m.require; |
|
| 387 |
fprintf fmt "@]}" |
|
| 388 |
|
|
| 389 |
let pp_emf_spec_modes = pp_emf_list pp_emf_spec_mode |
|
| 390 |
|
|
| 391 |
let pp_emf_spec_import fmt i = |
|
| 392 |
fprintf fmt "{@[";
|
|
| 393 |
fprintf fmt "\"contract\": \"%s\",@ " |
|
| 394 |
i.import_nodeid; |
|
| 395 |
fprintf fmt "\"inputs\": [%a],@ " |
|
| 396 |
pp_emf_exprs i.inputs; |
|
| 397 |
fprintf fmt "\"outputs\": [%a],@ " |
|
| 398 |
pp_emf_exprs i.outputs; |
|
| 399 |
fprintf fmt "@]}" |
|
| 400 |
|
|
| 401 |
let pp_emf_spec_imports = pp_emf_list pp_emf_spec_import |
|
| 402 |
|
|
| 403 |
let pp_emf_spec fmt spec = |
|
| 404 |
fprintf fmt "{ @[<hov 0>";
|
|
| 405 |
fprintf fmt "\"consts\": [%a],@ " |
|
| 406 |
pp_emf_consts spec.consts; |
|
| 407 |
fprintf fmt "\"locals\": [%a],@ " |
|
| 408 |
pp_emf_vars_decl spec.locals; |
|
| 409 |
fprintf fmt "\"stmts\": [%a],@ " |
|
| 410 |
pp_emf_stmts spec.stmts; |
|
| 411 |
fprintf fmt "\"assume\": [%a],@ " |
|
| 412 |
pp_emf_eexprs spec.assume; |
|
| 413 |
fprintf fmt "\"guarantees\": [%a],@ " |
|
| 414 |
pp_emf_eexprs spec.guarantees; |
|
| 415 |
fprintf fmt "\"modes\": [%a],@ " |
|
| 416 |
pp_emf_spec_modes spec.modes; |
|
| 417 |
fprintf fmt "\"imports\": [%a]@ " |
|
| 418 |
pp_emf_spec_imports spec.imports; |
|
| 419 |
fprintf fmt "@] }" |
|
| 378 | 420 |
|
| 379 | 421 |
let pp_emf_annots cpt fmt annots = fprintf_list ~sep:",@ " (pp_emf_annot cpt) fmt annots.annots |
| 380 | 422 |
let pp_emf_annots_list cpt fmt annots_list = fprintf_list ~sep:",@ " (pp_emf_annots cpt) fmt annots_list |
| 423 |
|
|
| 424 |
|
|
| 425 |
|
|
| 381 | 426 |
let pp_machine fmt m = |
| 382 | 427 |
let instrs = (*merge_branches*) m.mstep.step_instrs in |
| 383 | 428 |
try |
| 384 | 429 |
fprintf fmt "@[<v 2>\"%a\": {@ "
|
| 385 |
print_protect (fun fmt -> pp_print_string fmt m.mname.node_id); |
|
| 430 |
print_protect (fun fmt -> pp_print_string fmt m.mname.node_id); |
|
| 431 |
fprintf fmt "\"imported\": \"false\",@ "; |
|
| 386 | 432 |
fprintf fmt "\"kind\": %t,@ " |
| 387 | 433 |
(fun fmt -> if not ( snd (get_stateless_status m) ) |
| 388 | 434 |
then fprintf fmt "\"stateful\"" |
| ... | ... | |
| 399 | 445 |
fprintf fmt "\"original_name\": \"%s\",@ " m.mname.node_id; |
| 400 | 446 |
fprintf fmt "\"instrs\": {@[<v 0> %a@]@ },@ "
|
| 401 | 447 |
(pp_emf_instrs m) instrs; |
| 448 |
(match m.mspec with None -> () | Some spec -> fprintf fmt "\"spec\": %a,@ " pp_emf_spec spec); |
|
| 402 | 449 |
fprintf fmt "\"annots\": {@[<v 0> %a@]@ }" (pp_emf_annots_list (ref 0)) m.mannot;
|
| 403 | 450 |
fprintf fmt "@]@ }" |
| 404 | 451 |
with Unhandled msg -> ( |
| ... | ... | |
| 408 | 455 |
eprintf "node skipped - no output generated@ @]@." |
| 409 | 456 |
) |
| 410 | 457 |
|
| 458 |
let pp_emf_imported_node fmt top = |
|
| 459 |
let ind = Corelang.imported_node_of_top top in |
|
| 460 |
try |
|
| 461 |
fprintf fmt "@[<v 2>\"%a\": {@ "
|
|
| 462 |
print_protect (fun fmt -> pp_print_string fmt ind.nodei_id); |
|
| 463 |
fprintf fmt "\"imported\": \"true\",@ "; |
|
| 464 |
fprintf fmt "\"inputs\": [%a],@ " |
|
| 465 |
pp_emf_vars_decl ind.nodei_inputs; |
|
| 466 |
fprintf fmt "\"outputs\": [%a],@ " |
|
| 467 |
pp_emf_vars_decl ind.nodei_outputs; |
|
| 468 |
fprintf fmt "\"original_name\": \"%s\",@ " ind.nodei_id; |
|
| 469 |
(match ind.nodei_spec with None -> () | Some spec -> fprintf fmt "\"spec\": %a" pp_emf_spec spec); |
|
| 470 |
fprintf fmt "@]@ }" |
|
| 471 |
with Unhandled msg -> ( |
|
| 472 |
eprintf "[Error] @[<v 0>EMF backend@ Issues while translating node %s@ " |
|
| 473 |
ind.nodei_id; |
|
| 474 |
eprintf "%s@ " msg; |
|
| 475 |
eprintf "node skipped - no output generated@ @]@." |
|
| 476 |
) |
|
| 411 | 477 |
(****************************************************) |
| 412 | 478 |
(* Main function: iterates over node and print them *) |
| 413 | 479 |
(****************************************************) |
| ... | ... | |
| 425 | 491 |
fprintf fmt "@ @]},@ " |
| 426 | 492 |
|
| 427 | 493 |
let translate fmt basename prog machines = |
| 428 |
(* record_types prog; *)
|
|
| 494 |
(* record_types prog; *) |
|
| 429 | 495 |
fprintf fmt "@[<v 0>{@ ";
|
| 430 | 496 |
pp_meta fmt basename; |
| 497 |
(* Typedef *) |
|
| 498 |
fprintf fmt "\"typedef\": [@[<v 0>%a@]],@ " |
|
| 499 |
(pp_emf_list pp_emf_typedef) (Corelang.get_typedefs prog); |
|
| 500 |
fprintf fmt "\"consts\": [@[<v 0>%a@]],@ " |
|
| 501 |
(pp_emf_list pp_emf_top_const) (Corelang.get_consts prog); |
|
| 502 |
fprintf fmt "\"imported_nodes\": @[<v 0>{@ ";
|
|
| 503 |
pp_emf_list pp_emf_imported_node fmt (Corelang.get_imported_nodes prog); |
|
| 504 |
fprintf fmt "}@],@ "; |
|
| 431 | 505 |
fprintf fmt "\"nodes\": @[<v 0>{@ ";
|
| 432 | 506 |
(* Previous alternative: mapping normalized lustre to EMF: |
| 433 | 507 |
fprintf_list ~sep:",@ " pp_decl fmt prog; *) |
| 434 |
fprintf_list ~sep:",@ " pp_machine fmt (List.rev machines);
|
|
| 508 |
pp_emf_list pp_machine fmt (List.rev machines);
|
|
| 435 | 509 |
fprintf fmt "}@]@ }"; |
| 436 | 510 |
fprintf fmt "@]@ }" |
| 437 | 511 |
|
Also available in: Unified diff
Some progress on EMF bqckend. Refactoring machines code