Project

General

Profile

Revision 59020713 src/backends/EMF/EMF_backend.ml

View differences:

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