Project

General

Profile

« Previous | Next » 

Revision 7ee5f69e

Added by LĂ©lio Brun 9 months ago

corrections on loggers + spec in AST

View differences:

src/printers.ml
10 10
(********************************************************************)
11 11

  
12 12
open Lustre_types
13
open Format
14 13
open Utils
14
open Format
15 15

  
16 16
let kind2_language_cst =
17 17
  [ "initial" ]
......
348 348
  | Eq eq -> pp_node_eq fmt eq
349 349
  | Aut aut -> pp_node_aut fmt aut
350 350

  
351
and pp_node_stmts fmt stmts = fprintf_list ~sep:"@ " pp_node_stmt fmt stmts
351
and pp_node_stmts fmt stmts =
352
  pp_print_list
353
    ~pp_open_box:pp_open_vbox0
354
    ~pp_sep:pp_print_cut
355
    pp_node_stmt fmt stmts
352 356

  
353 357
and pp_node_aut fmt aut =
354 358
  fprintf fmt "@[<v 0>automaton %s@,%a@]"
......
475 479
  fprintf fmt "%s" (if nd.node_dec_stateless then "function" else "node")
476 480
  
477 481
let pp_node fmt nd =
478
  fprintf fmt "@[<v 0>";
479 482
  (* Prototype *)
480 483
  fprintf fmt  "%a @[<hov 0>%s (@[%a)@]@ returns (@[%a)@]@]@ "
481 484
    pp_node_vs_function nd
......
484 487
    pp_node_args nd.node_outputs;
485 488
  (* Contracts *)
486 489
  fprintf fmt "%a"
487
    (fun fmt s -> match s with Some s -> pp_spec_as_comment fmt (nd.node_inputs, nd.node_outputs, s) | _ -> ()) nd.node_spec
490
    (fun fmt s -> match s with
491
       | Some s -> pp_spec_as_comment fmt (nd.node_inputs, nd.node_outputs, s)
492
       | _ -> ()) nd.node_spec
488 493
    (* (fun fmt -> match nd.node_spec with None -> () | Some _ -> fprintf fmt "@ ") *);
489 494
  (* Locals *)
490 495
  fprintf fmt "%a" (fun fmt locals ->
491
      match locals with [] -> () | _ ->
492
                                    fprintf fmt "@[<v 4>var %a@]@ " 
493
                                      (fprintf_list ~sep:"@ " 
494
	                                 (fun fmt v -> fprintf fmt "%a;" pp_node_var v))
495
                                      locals
496
      match locals with
497
      | [] -> ()
498
      | _ ->
499
        fprintf fmt "@[<v 4>var %a@]@ "
500
          (fprintf_list ~sep:"@ "
501
	           (fun fmt v -> fprintf fmt "%a;" pp_node_var v))
502
          locals
496 503
    ) nd.node_locals;
497 504
  (* Checks *)
498 505
  fprintf fmt "%a"
499 506
    (fun fmt checks ->
500
      match checks with [] -> () | _ ->
501
                                    fprintf fmt "@[<v 4>check@ %a@]@ " 
502
                                      (fprintf_list ~sep:"@ " 
503
	                                 (fun fmt d -> fprintf fmt "%a" Dimension.pp_dimension d))
504
                                      checks
507
       match checks with
508
       | [] -> ()
509
       | _ ->
510
         fprintf fmt "@[<v 4>check@ %a@]@ "
511
           (fprintf_list ~sep:"@ "
512
	            (fun fmt d -> fprintf fmt "%a" Dimension.pp_dimension d))
513
           checks
505 514
    ) nd.node_checks;
506 515
  (* Body *)
507
  fprintf fmt "let@[<h 2>   @ @[<v>";
516
  fprintf fmt "@[<v 2>let@ ";
508 517
  (* Annotations *)
509
  fprintf fmt "%a@ " (fprintf_list ~sep:"@ " pp_expr_annot) nd.node_annot;
518
  fprintf fmt "%a" (fprintf_list ~sep:"@ " pp_expr_annot) nd.node_annot;
510 519
  (* Statements *)
511
  fprintf fmt "%a@ " pp_node_stmts nd.node_stmts;
520
  fprintf fmt "%a" pp_node_stmts nd.node_stmts;
512 521
  (* Asserts *)    
513 522
  fprintf fmt "%a" pp_asserts nd.node_asserts;
514 523
  (* closing boxes body (2)  and node (1) *) 
515
  fprintf fmt "@]@]@ tel@]@ "
524
  fprintf fmt "@]@ tel"
516 525

  
517 526

  
518 527
(*fprintf fmt "@ /* Scheduling: %a */ @ " (fprintf_list ~sep:", " pp_print_string) (Scheduling.schedule_node nd)*)
......
520 529
let pp_node fmt nd =
521 530
  match nd.node_spec, nd.node_iscontract with
522 531
  | None, false
523
    | Some (NodeSpec _), false 
524
    -> pp_node fmt nd
525
  | Some (Contract _), false -> pp_node fmt nd (* may happen early in the compil process *)
526
  | Some (Contract _), true -> pp_contract fmt nd 
532
  | Some (NodeSpec _), false ->
533
    pp_node fmt nd
534
  | Some (Contract _), false ->
535
    pp_node fmt nd (* may happen early in the compil process *)
536
  | Some (Contract _), true ->
537
    pp_contract fmt nd
527 538
  | _ -> assert false
528 539
     
529 540
let pp_imported_node fmt ind = 
......
547 558
let pp_const_decl_list fmt clist = 
548 559
  fprintf_list ~sep:"@ " pp_const_decl fmt clist
549 560

  
550

  
551 561
  
552 562
let pp_decl fmt decl =
553 563
  match decl.top_decl_desc with
554
  | Node nd -> fprintf fmt "%a" pp_node nd
564
  | Node nd ->
565
    fprintf fmt "%a" pp_node nd
555 566
  | ImportedNode ind -> (* We do not print imported nodes *)
556 567
     fprintf fmt "(* imported %a; *)" pp_imported_node ind
557
  | Const c -> fprintf fmt "const %a" pp_const_decl c
558
  | Open (local, s) -> if local then fprintf fmt "#open \"%s\"" s else fprintf fmt "#open <%s>" s
559
  | Include s -> fprintf fmt "include \"%s\"" s
560
  | TypeDef tdef -> fprintf fmt "%a" pp_typedef tdef
568
  | Const c ->
569
    fprintf fmt "const %a" pp_const_decl c
570
  | Open (local, s) ->
571
    if local then fprintf fmt "#open \"%s\"" s else fprintf fmt "#open <%s>" s
572
  | Include s ->
573
    fprintf fmt "include \"%s\"" s
574
  | TypeDef tdef ->
575
    fprintf fmt "%a" pp_typedef tdef
561 576
  
562 577
let pp_prog pp_decl fmt prog =
563 578
  (* we first print types: the function SortProg.sort could do the job but ut
564 579
     introduces a cyclic dependance *)
565 580

  
566 581
  let open_decl, prog =
567
    List.partition (fun decl -> match decl.top_decl_desc with Open _ -> true | _ -> false) prog
582
    List.partition (fun decl -> match decl.top_decl_desc with
583
          Open _ -> true | _ -> false) prog
568 584
  in
569 585
  let type_decl, prog =
570
    List.partition (fun decl -> match decl.top_decl_desc with TypeDef _ -> true | _ -> false) prog
586
    List.partition (fun decl -> match decl.top_decl_desc with
587
          TypeDef _ -> true | _ -> false) prog
571 588
  in
572
  fprintf fmt "@[<v 0>%a@]" (fprintf_list ~sep:"@ " pp_decl) (open_decl@type_decl@prog)
589
  pp_print_list
590
    ~pp_open_box:pp_open_vbox0
591
    ~pp_sep:pp_print_cutcut
592
    pp_decl
593
    fmt
594
    (open_decl @ type_decl @ prog)
573 595

  
574 596
(* Gives a short overview of model content. Do not print all node content *)
575 597
let pp_short_decl fmt decl =

Also available in: Unified diff