tallyingTest.ml 5.65 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

18
let norm_tests = [
19 20 21 22 23 24 25 26 27 28 29 30
  "(`$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")) 
31
                      (cap 
32 33
                        (mk_pos ("A","Int"))
                        (mk_neg ("Bool","B"))
34
                      );
35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54
  "(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"))
                        )

                      );
55 56
]

57 58
let m_compare = Tallying.CS.M.compare Types.compare

59
module MList = OUnitDiff.ListSimpleMake (struct 
60 61 62 63 64 65
  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)

66 67
let test_norm =
  "test tallying norm" >:::
68 69 70 71 72 73
    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
74
        MList.assert_equal (elem expected) (elem result)
75 76 77 78
      )
    ) norm_tests
;;

79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118
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");
]

let test_merge =
  let print_test l =
    String.concat ";" (List.map (fun (s,t) -> Printf.sprintf " %s \\ %s" s t) l)
  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
;;

119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137
let e_compare = Tallying.CS.E.compare Types.compare

let to_string pp t =
  Format.fprintf Format.str_formatter "%a@." pp t;
  Format.flush_str_formatter ()
;;

let compare_constr (v1,t1) (v2,t2) = 
  if (v1,t1) == (v2,t2) then 0
  else let c = Var.compare v1 v2 in if c <> 0 then c
  else Types.compare t1 t2

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)

138
module SubSet = OUnitDiff.SetMake (struct 
139 140 141 142 143 144 145 146 147 148 149 150 151 152 153
  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","Empty");("B","Empty")];
    [("A","Int | Bool");("B","Int | Bool")]
154 155 156 157 158 159
  ];
  [("(Int -> Int) | (Bool -> Bool)", "(`$A -> `$B)")], mk_e [
    [("A","Empty")];
    [("A","Empty");("B","Empty")];
  ];
  [("((Int,Int) , (Int | Bool))","(`$A,Int) | ((`$B,Int),Bool)")], mk_e [[("A", "(Int,Int)"); ("B","Int")]];
160 161 162 163 164 165
]

let test_tallying =
  let print_test l =
    String.concat ";" (List.map (fun (s,t) -> Printf.sprintf " %s \\ %s" s t) l)
  in
166
  "test tallying" >:::
167 168 169 170
    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
171 172
        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)
173 174 175 176
      )
    ) tallying_tests
;;

177 178 179
let all =
  "all tests" >::: [
    test_norm;
180
    test_merge;
181
    test_tallying;
182 183 184 185 186 187 188 189
  ]
 
let main () =
  OUnit.run_test_tt_main all
;;
 
main ()