tallyingTest.ml 6.31 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
;;

Pietro Abate's avatar
Pietro Abate committed
11 12
let union = Tallying.CS.union
let prod = Tallying.CS.prod
13 14 15 16
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 21 22 23 24 25 26 27 28 29 30 31 32
type pp = P of vv * string | N of string * vv
and vv = V of string

let mk_s ll =
  List.fold_left (fun acc1 l ->
    let x = 
      List.fold_left (fun acc2 -> function
        |P(V a,b) -> Tallying.CS.prod (mk_pos (a,b)) acc2
        |N(a,V b) -> Tallying.CS.prod (mk_neg (a,b)) acc2
      ) Tallying.CS.S.empty l
    in Tallying.CS.union x acc1
  ) Tallying.CS.S.empty ll

(* check invariants on the constraints sets *)
let constraints_test = [];;
33

Pietro Abate's avatar
Pietro Abate committed
34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55
(* ^ => | -- v => & *)

let norm_tests = [
  "(`$A -> Bool)", "(`$B -> `$B)", mk_s [
    [P(V "B","Empty")];
    [N("`$B",V "A");N("Bool",V "B")]
  ];
  "`$B", "`$A", mk_s [[N("`$B",V "A")]];
  "`$B", "Empty", mk_s [[P(V "B","Empty")]];
  "Int", "`$B", mk_s [[N("Int",V "B")]];
  "Int", "(`$A | `$B)", mk_s [[N("Int \\ `$B",V "A")]];
  "(Int -> Bool)", "(`$A -> `$B)", mk_s [
    [P(V "A","Empty")];
    [P(V "A","Int");N("Bool",V "B")]
  ];
  "(Int -> Int) | (Bool -> Bool)", "(`$A -> `$B)", mk_s [
    [P(V "A","Empty")];
    [P(V "A","Empty");N("Int",V "B")];
    [P(V "A","Empty");N("Bool",V "B")];
    [P(V "A","Empty");N("Int | Bool",V "B")]
  ];
  (*
56 57
  "([0--*] & `true)", "(`$A | Int) & ((Any \\ `$A) | Bool)",
  *)
Pietro Abate's avatar
Pietro Abate committed
58 59 60 61 62 63 64 65 66 67 68 69
  "(`$A , `$B)","(Int , Bool)", mk_s [
    [P(V "A","Int");P(V "B","Bool")]
  ];
  "(`$A & (`$B , `$C))","(Int , Int)", mk_s [
    [P(V "A","(Int , Int) | (Any \\ (`$B , `$C))")]
  ];
  "(`$A , Int) & (`$B , Bool))","(Int , (Int & Bool))", mk_s [
    [P(V "A","Int");P(V "B","Int")]
  ];
  "(`$A1 -> `$B1) -> [ `$A1 ] -> [ `$B1 ]", "((Int -> Bool) | ((`$A \\ Int) -> (`$B \\ Int))) -> `$G", mk_s [
    [P(V "A","Empty")]
  ];
70 71
]

Pietro Abate's avatar
Pietro Abate committed
72 73 74 75 76
(* 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
77

78
module MList = OUnitDiff.ListSimpleMake (struct 
79 80 81 82 83 84
  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)

85 86
let test_norm =
  "test tallying norm" >:::
87 88 89 90 91 92
    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
93
        MList.assert_equal (elem expected) (elem result)
94 95 96 97
      )
    ) norm_tests
;;

98
let merge_tests = [
Pietro Abate's avatar
Pietro Abate committed
99
  [("`$A", "Empty");("`$B", "Empty")], prod (mk_pos ("A", "Empty")) (mk_pos ("B", "Empty"));
100 101 102
  [("`$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")],
Pietro Abate's avatar
Pietro Abate committed
103
    Tallying.CS.prod
104
      (mk_neg ("`$B","A")) (
Pietro Abate's avatar
Pietro Abate committed
105
        Tallying.CS.prod 
106
          (mk_pos ("A", "Int | Bool")) (
Pietro Abate's avatar
Pietro Abate committed
107
            Tallying.CS.prod
108 109 110 111 112 113
            (mk_neg ("Int | Bool","B"))
            (mk_pos ("B","Int | Bool"))
          )
        );
  [("`$A", "`$B")], mk_pos ("A","`$B");
  [("`$B", "Empty")], mk_pos ("B","Empty");
Pietro Abate's avatar
Pietro Abate committed
114
  [("`$A", "Int");("`$B", "Bool"); ("`$A", "Empty")],Tallying.CS.prod (mk_pos ("A", "Empty")) (mk_pos ("B", "Bool"));
115 116 117 118
]

let test_merge =
  let print_test l =
119
    String.concat ";" (List.map (fun (s,t) -> Printf.sprintf " %s >= %s" s t) l)
120 121 122 123 124 125 126
  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
Pietro Abate's avatar
Pietro Abate committed
127
          Tallying.CS.prod acc (Tallying.norm(diff s t))) Tallying.CS.S.empty l 
128 129
        in
        let result = Tallying.CS.S.fold (fun c acc ->
Pietro Abate's avatar
Pietro Abate committed
130
          try Tallying.CS.union (Tallying.merge c) acc with Tallying.UnSatConstr -> acc
131 132 133 134 135 136 137 138
          ) 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
;;

139 140 141 142 143
let to_string pp t =
  Format.fprintf Format.str_formatter "%a@." pp t;
  Format.flush_str_formatter ()
;;

Pietro Abate's avatar
Pietro Abate committed
144
(* the abstract field is ignored in the comparison *)
145
let compare_constr (v1,t1) (v2,t2) = 
Pietro Abate's avatar
Pietro Abate committed
146
  let a = Types.abstract Abstract.any in
147 148
  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
149
  else Types.compare (diff t1 a) (diff t2 a)
150 151 152 153 154 155 156 157

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)

158
module SubSet = OUnitDiff.SetMake (struct 
159 160 161 162 163 164 165 166 167 168 169 170 171 172
  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")]
173 174 175 176 177
  ];
  [("(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
178
  [("(`$A , Int) & (`$B , Bool))","(Int , (Int & Bool))")], mk_e [[("A","Int");("B","Int")]];
179 180 181 182 183 184
]

let test_tallying =
  let print_test l =
    String.concat ";" (List.map (fun (s,t) -> Printf.sprintf " %s \\ %s" s t) l)
  in
185
  "test tallying" >:::
186 187 188 189
    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
190 191
        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)
192 193 194 195
      )
    ) tallying_tests
;;

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