tallyingTest.ml 6.43 KB
Newer Older
1
open OUnit
2
open Types
3 4 5 6 7 8 9 10

let parse_typ s =
  let st = Stream.of_string s in
  let astpat = Parser.pat st in 
  let nodepat = Typer.typ Builtin.env astpat in
  Types.descr nodepat
;;

11 12 13 14 15 16
let cup = Tallying.CS.cup
let cap = Tallying.CS.cap
let singleton = Tallying.CS.singleton

let mk_pos (alpha,t) = singleton (Tallying.Pos (`Var alpha,parse_typ t))
let mk_neg (t,alpha) = singleton (Tallying.Neg (parse_typ t,`Var alpha))
17

Pietro Abate's avatar
Pietro Abate committed
18 19 20
(* ^ => |
 * v => &
 *)
21
let norm_tests = [
22 23 24 25 26 27 28 29 30 31 32 33
  "(`$A -> Bool)", "(`$B -> `$B)", 
                    cup (mk_pos ("B","Empty"))
                      (cap 
                        (mk_neg ("`$B","A"))
                        (mk_neg ("Bool","B"))
                      );
  "`$B", "`$A", mk_neg ("`$B","A");
  "`$B", "Empty", mk_pos ("B","Empty");
  "Int", "`$B", mk_neg ("Int","B");
  "Int", "(`$A | `$B)", mk_neg ("Int \\ `$B","A");
  "(Int -> Bool)", "(`$A -> `$B)",
                    cup (mk_pos ("A","Empty")) 
34
                      (cap 
35 36
                        (mk_pos ("A","Int"))
                        (mk_neg ("Bool","B"))
37
                      );
38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57
  "(Int -> Int) | (Bool -> Bool)", "(`$A -> `$B)", 
                    cup 
                      (mk_pos ("A","Empty"))
                      (cup
                        (cup
                          (cap
                            (mk_pos ("A","Empty"))
                            (mk_neg ("Int","B"))
                          )
                          (cap
                            (mk_pos ("A","Empty"))
                            (mk_neg ("Bool","B"))
                          )
                        )
                        (cap 
                          (mk_pos ("A","Empty"))
                          (mk_neg ("Int | Bool","B"))
                        )

                      );
58 59 60 61 62 63
                      (*
  "([0--*] & `true)", "(`$A | Int) & ((Any \\ `$A) | Bool)",
  *)
  "(`$A , `$B)","(Int , Bool)",
                     cap
                        (mk_pos ("A","Int"))
Pietro Abate's avatar
Pietro Abate committed
64 65 66
                        (mk_pos ("B","Bool"));
  "(`$A & (`$B , `$C))","(Int , Int)",mk_pos ("A","(Int , Int) | (Any \\ (`$B , `$C))");
  "(`$A , Int) & (`$B , Bool))","(Int , (Int & Bool))", cap (mk_pos ("A","Int")) (mk_pos ("B","Int"));
67 68
]

Pietro Abate's avatar
Pietro Abate committed
69 70 71 72 73
(* the abstract field is ignored in the comparison *)
let m_compare = 
  let a = Types.abstract Abstract.any in
  let cmp t1 t2 = Types.compare (diff t1 a) (diff t2 a) in
  Tallying.CS.M.compare cmp
74

75
module MList = OUnitDiff.ListSimpleMake (struct 
76 77 78 79 80 81
  type t = Tallying.CS.m
  let compare = m_compare
  let pp_printer = Tallying.CS.print_m
  let pp_print_sep = OUnitDiff.pp_comma_separator
end)

82 83
let test_norm =
  "test tallying norm" >:::
84 85 86 87 88 89
    List.map (fun (s,t,expected) ->
      (Printf.sprintf " %s \\ %s" s t) >:: (fun _ ->
        let s = parse_typ s in
        let t = parse_typ t in
        let result = Tallying.norm (diff s t) in
        let elem s = List.sort m_compare (Tallying.CS.S.elements s) in
90
        MList.assert_equal (elem expected) (elem result)
91 92 93 94
      )
    ) norm_tests
;;

95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110
let merge_tests = [
  [("`$A", "Empty");("`$B", "Empty")], cap (mk_pos ("A", "Empty")) (mk_pos ("B", "Empty"));
  [("`$A", "Int | Bool");("Int","`$B");("`$B", "Empty")], Tallying.CS.unsat;
  [("Bool","`$B"); ("`$B", "`$A"); ("`$A", "Empty")], Tallying.CS.unsat;
  [("Bool","`$B"); ("Int","`$B"); ("`$B","`$A"); ("`$A", "Int | Bool")],
    cap 
      (mk_neg ("`$B","A")) (
        cap 
          (mk_pos ("A", "Int | Bool")) (
            cap
            (mk_neg ("Int | Bool","B"))
            (mk_pos ("B","Int | Bool"))
          )
        );
  [("`$A", "`$B")], mk_pos ("A","`$B");
  [("`$B", "Empty")], mk_pos ("B","Empty");
111
  [("`$A", "Int");("`$B", "Bool"); ("`$A", "Empty")],cap (mk_pos ("A", "Empty")) (mk_pos ("B", "Bool"));
112 113 114 115
]

let test_merge =
  let print_test l =
116
    String.concat ";" (List.map (fun (s,t) -> Printf.sprintf " %s >= %s" s t) l)
117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135
  in
  "test tallying merge" >:::
    List.map (fun (l,expected) ->
      (print_test l) >:: (fun _ ->
        let n = List.fold_left (fun acc (s,t) ->
          let s = parse_typ s in
          let t = parse_typ t in
          Tallying.CS.cap acc (Tallying.norm(diff s t))) Tallying.CS.S.empty l 
        in
        let result = Tallying.CS.S.fold (fun c acc ->
          try cup (Tallying.merge c) acc with Tallying.UnSatConstr -> acc
          ) n Tallying.CS.S.empty
        in
        let elem s = List.sort m_compare (Tallying.CS.S.elements s) in
        MList.assert_equal (elem expected) (elem result)
      )
    ) merge_tests
;;

136 137 138 139 140
let to_string pp t =
  Format.fprintf Format.str_formatter "%a@." pp t;
  Format.flush_str_formatter ()
;;

Pietro Abate's avatar
Pietro Abate committed
141
(* the abstract field is ignored in the comparison *)
142
let compare_constr (v1,t1) (v2,t2) = 
Pietro Abate's avatar
Pietro Abate committed
143
  let a = Types.abstract Abstract.any in
144 145
  if (v1,t1) == (v2,t2) then 0
  else let c = Var.compare v1 v2 in if c <> 0 then c
Pietro Abate's avatar
Pietro Abate committed
146
  else Types.compare (diff t1 a) (diff t2 a)
147 148 149 150 151 152 153 154

module EList = OUnitDiff.ListSimpleMake (struct 
  type t = (Var.var * Types.t)
  let compare = compare_constr
  let pp_printer ppf (`Var v,t) = Format.fprintf ppf "(%s = %s)" v (to_string Print.print t)
  let pp_print_sep = OUnitDiff.pp_comma_separator
end)

155
module SubSet = OUnitDiff.SetMake (struct 
156 157 158 159 160 161 162 163 164 165 166 167 168 169
  type t = EList.t
  let compare a b = EList.compare a b
  let pp_printer ppf l = EList.pp_printer ppf l
  let pp_print_sep = OUnitDiff.pp_comma_separator
end)

let mk_e ll =
  List.map (fun l ->
    List.map (fun (v,t) -> (`Var v),(parse_typ t)) l
  ) ll

let tallying_tests = [
  [("((Int | Bool) -> Int)", "(`$A -> `$B)"); ("(`$A -> Bool)","(`$B -> `$B)")], mk_e [
    [("A","Int | Bool");("B","Int | Bool")]
170 171 172 173 174
  ];
  [("(Int -> Int) | (Bool -> Bool)", "(`$A -> `$B)")], mk_e [
    [("A","Empty");("B","Empty")];
  ];
  [("((Int,Int) , (Int | Bool))","(`$A,Int) | ((`$B,Int),Bool)")], mk_e [[("A", "(Int,Int)"); ("B","Int")]];
Pietro Abate's avatar
Pietro Abate committed
175
  [("(`$A , Int) & (`$B , Bool))","(Int , (Int & Bool))")], mk_e [[("A","Int");("B","Int")]];
176 177 178 179 180 181
]

let test_tallying =
  let print_test l =
    String.concat ";" (List.map (fun (s,t) -> Printf.sprintf " %s \\ %s" s t) l)
  in
182
  "test tallying" >:::
183 184 185 186
    List.map (fun (l,expected) ->
      (print_test l) >:: (fun _ ->
        let l = List.map (fun (s,t) -> (parse_typ s,parse_typ t)) l in
        let result = Tallying.tallying l in
187 188
        let elem s = SubSet.of_list (List.map (fun l -> EList.of_list (List.sort compare_constr l)) s) in
        SubSet.assert_equal (elem expected) (elem result)
189 190 191 192
      )
    ) tallying_tests
;;

193 194 195
let all =
  "all tests" >::: [
    test_norm;
196
    test_merge;
197
    test_tallying;
198 199 200 201 202 203 204 205
  ]
 
let main () =
  OUnit.run_test_tt_main all
;;
 
main ()