Project

General

Profile

« Previous | Next » 

Revision a7062da6

Added by LĂ©lio Brun over 3 years ago

another step towards refactoring

View differences:

src/backends/Horn/horn_backend_printers.ml
14 14

  
15 15
   This is a modified version that handle reset *)
16 16

  
17
open Utils
17 18
open Format
18 19
open Lustre_types
19 20
open Machine_code_types
......
218 219
  in
219 220

  
220 221
  fprintf fmt "(%a @[<v 0>%a)@]" pp_machine_reset_name (node_name n)
221
    (Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
222
    (pp_print_list (pp_horn_var m))
222 223
    (rename_machine_list (concat m.mname.node_id i)
223 224
       (rename_current_list (full_memory_vars machines target_machine))
224 225
    @ rename_machine_list (concat m.mname.node_id i)
......
261 262
      fprintf fmt "(= %a false)" (pp_horn_var m) mem_x;
262 263
      fprintf fmt ")@]"
263 264
    | _ ->
264
      fprintf fmt "(%a @[<v 0>%a%t%a%t%a)@]" pp_machine_step_name (node_name n)
265
        (Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m)))
266
        inputs
267
        (Utils.pp_final_char_if_non_empty "@ " inputs)
268
        (Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m)))
265
      fprintf fmt "(%a @[<v 0>%a%a%a)@]" pp_machine_step_name (node_name n)
266
        (pp_print_list ~pp_epilogue:pp_print_cut
267
           (pp_horn_val m self (pp_horn_var m))) inputs
268
        (pp_print_list ~pp_epilogue:pp_print_cut
269
           (pp_horn_val m self (pp_horn_var m)))
269 270
        (List.map (fun v -> mk_val (Var v) v.var_type) outputs)
270
        (Utils.pp_final_char_if_non_empty "@ " outputs)
271
        (Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
272
        (mid_mems @ next_mems)
271
        (pp_print_list (pp_horn_var m)) (mid_mems @ next_mems)
273 272
  with Not_found ->
274 273
    (* stateless node instance *)
275 274
    let n, _ = List.assoc i m.mcalls in
276
    fprintf fmt "(%a @[<v 0>%a%t%a)@]" pp_machine_stateless_name (node_name n)
277
      (Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m)))
278
      inputs
279
      (Utils.pp_final_char_if_non_empty "@ " inputs)
280
      (Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m)))
275
    fprintf fmt "(%a @[<v 0>%a%a)@]" pp_machine_stateless_name (node_name n)
276
      (pp_print_list ~pp_epilogue:pp_print_cut
277
         (pp_horn_val m self (pp_horn_var m))) inputs
278
      (pp_print_list (pp_horn_val m self (pp_horn_var m)))
281 279
      (List.map (fun v -> mk_val (Var v) v.var_type) outputs)
282 280

  
283 281
(* Print the instruction and update the set of reset instances *)
......
370 368
  fprintf fmt "@[<v 5>(and @ ";
371 369

  
372 370
  (* print "x_m = x_c" for each local memory *)
373
  (Utils.fprintf_list ~sep:"@ " (fun fmt v ->
371
  (pp_print_list (fun fmt v ->
374 372
       fprintf fmt "(= %a %a)" (pp_horn_var m) (rename_mid v) (pp_horn_var m)
375 373
         (rename_current v)))
376 374
    fmt locals;
......
378 376

  
379 377
  (* print "child_reset ( associated vars _ {c,m} )" for each subnode. Special
380 378
     treatment for _arrow: _first = true *)
381
  (Utils.fprintf_list ~sep:"@ " (fun fmt (id, (n, _)) ->
379
  (pp_print_list (fun fmt (id, (n, _)) ->
382 380
       let name = node_name n in
383 381
       if name = "_arrow" then
384 382
         fprintf fmt "(= %s._arrow._first_m true)" (concat m.mname.node_id id)
385 383
       else
386 384
         let machine_n = get_machine machines name in
387 385
         fprintf fmt "(%s_reset @[<hov 0>%a@])" name
388
           (Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
386
           (pp_print_list (pp_horn_var m))
389 387
           (rename_machine_list
390 388
              (concat m.mname.node_id id)
391 389
              (reset_vars machines machine_n))))
......
405 403
    fprintf fmt "; %s@." m.mname.node_id;
406 404

  
407 405
    (* Printing variables *)
408
    Utils.fprintf_list ~sep:"@." pp_decl_var fmt
406
    pp_print_list ~pp_open_box:pp_open_vbox0 pp_decl_var fmt
409 407
      (inout_vars m
410 408
      @ rename_current_list (full_memory_vars machines m)
411 409
      @ rename_mid_list (full_memory_vars machines m)
......
417 415
      (* Declaring single predicate *)
418 416
      fprintf fmt "(declare-rel %a (%a))@." pp_machine_stateless_name
419 417
        m.mname.node_id
420
        (Utils.fprintf_list ~sep:" " pp_type)
418
        (pp_print_list pp_type)
421 419
        (List.map (fun v -> v.var_type) (inout_vars m));
422 420

  
423 421
      match m.mstep.step_asserts with
......
430 428
             (* No reset info for stateless nodes *) m fmt m.mstep.step_instrs);
431 429
        fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@." pp_machine_stateless_name
432 430
          m.mname.node_id
433
          (Utils.fprintf_list ~sep:" " (pp_horn_var m))
431
          (pp_print_list (pp_horn_var m))
434 432
          (inout_vars m)
435 433
      | assertsl ->
436 434
        let pp_val =
......
443 441
        ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
444 442
        fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val)
445 443
          assertsl pp_machine_stateless_name m.mname.node_id
446
          (Utils.fprintf_list ~sep:" " (pp_horn_var m))
444
          (pp_print_list (pp_horn_var m))
447 445
          (step_vars machines m))
448 446
    else (
449 447
      (* Declaring predicate *)
450 448
      fprintf fmt "(declare-rel %a (%a))@." pp_machine_reset_name
451 449
        m.mname.node_id
452
        (Utils.fprintf_list ~sep:" " pp_type)
450
        (pp_print_list pp_type)
453 451
        (List.map (fun v -> v.var_type) (reset_vars machines m));
454 452

  
455 453
      fprintf fmt "(declare-rel %a (%a))@." pp_machine_step_name m.mname.node_id
456
        (Utils.fprintf_list ~sep:" " pp_type)
454
        (pp_print_list pp_type)
457 455
        (List.map (fun v -> v.var_type) (step_vars machines m));
458 456

  
459 457
      pp_print_newline fmt ();
......
462 460
      fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@."
463 461
        (pp_machine_reset machines)
464 462
        m pp_machine_reset_name m.mname.node_id
465
        (Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
463
        (pp_print_list (pp_horn_var m))
466 464
        (reset_vars machines m);
467 465

  
468 466
      match m.mstep.step_asserts with
......
473 471
        ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
474 472
        fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@." pp_machine_step_name
475 473
          m.mname.node_id
476
          (Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
474
          (pp_print_list (pp_horn_var m))
477 475
          (step_vars machines m)
478 476
      | assertsl ->
479 477
        let pp_val =
......
487 485
        ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
488 486
        fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val)
489 487
          assertsl pp_machine_step_name m.mname.node_id
490
          (Utils.fprintf_list ~sep:" " (pp_horn_var m))
488
          (pp_print_list (pp_horn_var m))
491 489
          (step_vars machines m)))
492 490

  
493 491
let mk_flags arity =
......
527 525
    (* Check if there is annotation for s-function *)
528 526
    if m.mannot != [] then
529 527
      Format.fprintf fmt "; @[%a@]@]@\n"
530
        (Utils.fprintf_list ~sep:"@ " Printers.pp_s_function)
528
        (pp_print_list Printers.pp_s_function)
531 529
        m.mannot;
532 530

  
533 531
    (* Printing variables *)
534
    Utils.fprintf_list ~sep:"@." pp_decl_var fmt
532
    pp_print_list ~pp_open_box:pp_open_vbox0 pp_decl_var fmt
535 533
      (step_vars machines m
536 534
      @ rename_machine_list m.mname.node_id m.mstep.step_locals);
537 535
    Format.pp_print_newline fmt ();
......
541 539
      (* Declaring single predicate *)
542 540
      Format.fprintf fmt "(declare-rel %a (%a))@." pp_machine_stateless_name
543 541
        m.mname.node_id
544
        (Utils.fprintf_list ~sep:" " pp_type)
542
        (pp_print_list pp_type)
545 543
        (List.map (fun v -> v.var_type) (reset_vars machines m));
546 544
      Format.pp_print_newline fmt ();
547 545
      (* Rule for single predicate *)
548 546
      let str_flags = sf_name ^ " " ^ mk_flags (int_of_string flags) in
549 547
      Format.fprintf fmt "@[<v 2>(rule (=> @ (%s %a) (%a %a)@]@.))@.@."
550 548
        str_flags
551
        (Utils.fprintf_list ~sep:" " (pp_horn_var m))
549
        (pp_print_list (pp_horn_var m))
552 550
        (reset_vars machines m) pp_machine_stateless_name m.mname.node_id
553
        (Utils.fprintf_list ~sep:" " (pp_horn_var m))
551
        (pp_print_list (pp_horn_var m))
554 552
        (reset_vars machines m))
555 553
    else (
556 554
      (* Declaring predicate *)
557 555
      Format.fprintf fmt "(declare-rel %a (%a))@." pp_machine_reset_name
558 556
        m.mname.node_id
559
        (Utils.fprintf_list ~sep:" " pp_type)
557
        (pp_print_list pp_type)
560 558
        (List.map (fun v -> v.var_type) (inout_vars m));
561 559

  
562 560
      Format.fprintf fmt "(declare-rel %a (%a))@." pp_machine_step_name
563 561
        m.mname.node_id
564
        (Utils.fprintf_list ~sep:" " pp_type)
562
        (pp_print_list pp_type)
565 563
        (List.map (fun v -> v.var_type) (step_vars machines m));
566 564

  
567 565
      Format.pp_print_newline fmt ();
......
573 571
        ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
574 572
        fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@." pp_machine_step_name
575 573
          m.mname.node_id
576
          (Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
574
          (pp_print_list (pp_horn_var m))
577 575
          (step_vars machines m)
578 576
      | assertsl ->
579 577
        let pp_val =
......
587 585
        ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
588 586
        fprintf fmt "@. %a)(%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
589 587
          pp_machine_step_name m.mname.node_id
590
          (Utils.fprintf_list ~sep:" " (pp_horn_var m))
588
          (pp_print_list (pp_horn_var m))
591 589
          (step_vars machines m)))
592 590

  
593 591
(**************** XML printing functions *************)
......
606 604
      | Expr_array a ->
607 605
        fprintf fmt "[%a]" pp_xml_tuple a
608 606
      | Expr_access (a, d) ->
609
        fprintf fmt "%a[%a]" pp_xml_expr a Dimension.pp_dimension d
607
        fprintf fmt "%a[%a]" pp_xml_expr a Dimension.pp d
610 608
      | Expr_power (a, d) ->
611
        fprintf fmt "(%a^%a)" pp_xml_expr a Dimension.pp_dimension d
609
        fprintf fmt "(%a^%a)" pp_xml_expr a Dimension.pp d
612 610
      | Expr_tuple el ->
613 611
        fprintf fmt "(%a)" pp_xml_tuple el
614 612
      | Expr_ite (c, t, e) ->
......
628 626
      | Expr_appl (id, e, r) ->
629 627
        pp_xml_app fmt id e r)
630 628

  
631
and pp_xml_tuple fmt el = Utils.fprintf_list ~sep:"," pp_xml_expr fmt el
629
and pp_xml_tuple fmt el = pp_comma_list pp_xml_expr fmt el
632 630

  
633 631
and pp_xml_handler fmt (t, h) = fprintf fmt "(%s -> %a)" t pp_xml_expr h
634 632

  
635
and pp_xml_handlers fmt hl = Utils.fprintf_list ~sep:" " pp_xml_handler fmt hl
633
and pp_xml_handlers fmt hl = pp_print_list pp_xml_handler fmt hl
636 634

  
637 635
and pp_xml_app fmt id e r =
638 636
  match r with
......
684 682

  
685 683
and pp_xml_eexpr fmt e =
686 684
  fprintf fmt "%a%t %a"
687
    (Utils.fprintf_list ~sep:"; " Printers.pp_quantifiers)
685
    (pp_print_list ~pp_sep:pp_print_semicolon Printers.pp_quantifiers)
688 686
    e.eexpr_quantifiers
689 687
    (fun fmt ->
690 688
      match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
......
709 707
          Format.pp_print_string fmt x
710 708
        | _ ->
711 709
          Format.fprintf fmt "%a"
712
            (Utils.fprintf_list ~sep:"/" Format.pp_print_string)
710
            (pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt "/")
711
               pp_print_string)
713 712
            kwds)
714 713
      pp_xml_sf_value ee
715 714
  in
716
  Utils.fprintf_list ~sep:"@ " pp_xml_annot fmt expr_ann.annots
715
  pp_print_list pp_xml_annot fmt expr_ann.annots
717 716

  
718 717
and pp_xml_expr_annot fmt expr_ann =
719 718
  let pp_xml_annot fmt (kwds, ee) =
......
726 725
          Format.pp_print_string fmt x
727 726
        | _ ->
728 727
          Format.fprintf fmt "/%a/"
729
            (Utils.fprintf_list ~sep:"/" Format.pp_print_string)
728
            (pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt "/")
729
               pp_print_string)
730 730
            kwds)
731 731
      pp_xml_eexpr ee
732 732
  in
733
  Utils.fprintf_list ~sep:"@ " pp_xml_annot fmt expr_ann.annots
733
  pp_print_list pp_xml_annot fmt expr_ann.annots
734 734

  
735 735
(* Local Variables: *)
736 736
(* compile-command:"make -C ../../.." *)

Also available in: Unified diff