Project

General

Profile

« Previous | Next » 

Revision 397d5ae3

Added by Pierre-Loïc Garoche about 5 years ago

Copied Printers.pp_expr functions to Horn backend to escape < and > in XML traces output

View differences:

src/backends/Horn/horn_backend_printers.ml
592 592
         end
593 593

  
594 594
        end
595

  
596

  
597
(**************** XML printing functions *************)
598

  
599
	  let rec pp_xml_expr fmt expr =
600
  (match expr.expr_annot with 
601
  | None -> fprintf fmt "%t" 
602
  | Some ann -> fprintf fmt "@[(%a %t)@]" pp_xml_expr_annot ann)
603
    (fun fmt -> 
604
      match expr.expr_desc with
605
    | Expr_const c -> Printers.pp_const fmt c
606
    | Expr_ident id -> fprintf fmt "%s" id
607
    | Expr_array a -> fprintf fmt "[%a]" pp_xml_tuple a
608
    | Expr_access (a, d) -> fprintf fmt "%a[%a]" pp_xml_expr a Dimension.pp_dimension d
609
    | Expr_power (a, d) -> fprintf fmt "(%a^%a)" pp_xml_expr a Dimension.pp_dimension d
610
    | Expr_tuple el -> fprintf fmt "(%a)" pp_xml_tuple el
611
    | Expr_ite (c, t, e) -> fprintf fmt "@[<hov 1>(if %a then@ @[<hov 2>%a@]@ else@ @[<hov 2>%a@]@])" pp_xml_expr c pp_xml_expr t pp_xml_expr e
612
    | Expr_arrow (e1, e2) -> fprintf fmt "(%a -> %a)" pp_xml_expr e1 pp_xml_expr e2
613
    | Expr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_xml_expr e1 pp_xml_expr e2
614
    | Expr_pre e -> fprintf fmt "pre %a" pp_xml_expr e
615
    | Expr_when (e, id, l) -> fprintf fmt "%a when %s(%s)" pp_xml_expr e l id
616
    | Expr_merge (id, hl) -> 
617
      fprintf fmt "merge %s %a" id pp_xml_handlers hl
618
    | Expr_appl (id, e, r) -> pp_xml_app fmt id e r
619
    )
620
and pp_xml_tuple fmt el =
621
 Utils.fprintf_list ~sep:"," pp_xml_expr fmt el
622

  
623
and pp_xml_handler fmt (t, h) =
624
 fprintf fmt "(%s -> %a)" t pp_xml_expr h
625

  
626
and pp_xml_handlers fmt hl =
627
 Utils.fprintf_list ~sep:" " pp_xml_handler fmt hl
628

  
629
and pp_xml_app fmt id e r =
630
  match r with
631
  | None -> pp_xml_call fmt id e
632
  | Some c -> fprintf fmt "%t every (%a)" (fun fmt -> pp_xml_call fmt id e) pp_xml_expr c 
633

  
634
and pp_xml_call fmt id e =
635
  match id, e.expr_desc with
636
  | "+", Expr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_xml_expr e1 pp_xml_expr e2
637
  | "uminus", _ -> fprintf fmt "(- %a)" pp_xml_expr e
638
  | "-", Expr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_xml_expr e1 pp_xml_expr e2
639
  | "*", Expr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_xml_expr e1 pp_xml_expr e2
640
  | "/", Expr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_xml_expr e1 pp_xml_expr e2
641
  | "mod", Expr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_xml_expr e1 pp_xml_expr e2
642
  | "&&", Expr_tuple([e1;e2]) -> fprintf fmt "(%a and %a)" pp_xml_expr e1 pp_xml_expr e2
643
  | "||", Expr_tuple([e1;e2]) -> fprintf fmt "(%a or %a)" pp_xml_expr e1 pp_xml_expr e2
644
  | "xor", Expr_tuple([e1;e2]) -> fprintf fmt "(%a xor %a)" pp_xml_expr e1 pp_xml_expr e2
645
  | "impl", Expr_tuple([e1;e2]) -> fprintf fmt "(%a => %a)" pp_xml_expr e1 pp_xml_expr e2
646
  | "<", Expr_tuple([e1;e2]) -> fprintf fmt "(%a &lt; %a)" pp_xml_expr e1 pp_xml_expr e2
647
  | "<=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a &lt;= %a)" pp_xml_expr e1 pp_xml_expr e2
648
  | ">", Expr_tuple([e1;e2]) -> fprintf fmt "(%a &gt; %a)" pp_xml_expr e1 pp_xml_expr e2
649
  | ">=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a &gt;= %a)" pp_xml_expr e1 pp_xml_expr e2
650
  | "!=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_xml_expr e1 pp_xml_expr e2
651
  | "=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a = %a)" pp_xml_expr e1 pp_xml_expr e2
652
  | "not", _ -> fprintf fmt "(not %a)" pp_xml_expr e
653
  | _, Expr_tuple _ -> fprintf fmt "%s %a" id pp_xml_expr e
654
  | _ -> fprintf fmt "%s (%a)" id pp_xml_expr e
655

  
656
and pp_xml_eexpr fmt e =
657
  fprintf fmt "%a%t %a"
658
    (Utils.fprintf_list ~sep:"; " Printers.pp_quantifiers) e.eexpr_quantifiers
659
    (fun fmt -> match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
660
    pp_xml_expr e.eexpr_qfexpr
661

  
662
and  pp_xml_sf_value fmt e =
663
   fprintf fmt "%a"
664
     (* (Utils.fprintf_list ~sep:"; " pp_xml_quantifiers) e.eexpr_quantifiers *)
665
     (* (fun fmt -> match e.eexpr_quantifiers *)
666
     (*             with [] -> () *)
667
     (*                | _ -> fprintf fmt ";") *)
668
     pp_xml_expr e.eexpr_qfexpr
669

  
670
and pp_xml_s_function fmt expr_ann =
671
  let pp_xml_annot fmt (kwds, ee) =
672
    Format.fprintf fmt " %t : %a"
673
                   (fun fmt -> match kwds with
674
                               | [] -> assert false
675
                               | [x] -> Format.pp_print_string fmt x
676
                               | _ -> Format.fprintf fmt "%a" (Utils.fprintf_list ~sep:"/" Format.pp_print_string) kwds)
677
                   pp_xml_sf_value ee
678
  in
679
  Utils.fprintf_list ~sep:"@ " pp_xml_annot fmt expr_ann.annots
680

  
681
and pp_xml_expr_annot fmt expr_ann =
682
  let pp_xml_annot fmt (kwds, ee) =
683
    Format.fprintf fmt "(*! %t: %a; *)"
684
      (fun fmt -> match kwds with | [] -> assert false | [x] -> Format.pp_print_string fmt x | _ -> Format.fprintf fmt "/%a/" (Utils.fprintf_list ~sep:"/" Format.pp_print_string) kwds)
685
      pp_xml_eexpr ee
686
  in
687
  Utils.fprintf_list ~sep:"@ " pp_xml_annot fmt expr_ann.annots
688

  
689

  
595 690
(* Local Variables: *)
596 691
(* compile-command:"make -C ../../.." *)
597 692
(* End: *)

Also available in: Unified diff