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 ()