tallyingTest.ml 9.51 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 17 18 19 20 21 22 23
let to_string pp t =
  Format.fprintf Format.str_formatter "%a@." pp t;
  Format.flush_str_formatter ()
;;

(* the abstract field is ignored in the comparison *)
module ESet = OUnitDiff.SetMake (struct 
  type t = (Var.var * Types.t)
  let compare (v1,t1) (v2,t2) = 
    let a = Types.abstract Abstract.any in
    if (v1,t1) == (v2,t2) then 0
    else let c = Var.compare v1 v2 in if c <> 0 then c
    else Types.compare (diff t1 a) (diff t2 a)
24
  let pp_printer ppf (v,t) = Format.fprintf ppf "(%a = %s)" Var.print v (to_string Print.print t)
25 26
  let pp_print_sep = OUnitDiff.pp_comma_separator
end)
27

28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45
module SubStSet = OUnitDiff.SetMake (struct 
  type t = ESet.t
  let compare a b = ESet.compare a b
  let pp_printer ppf l = ESet.pp_printer ppf l
  let pp_print_sep = OUnitDiff.pp_comma_separator
end)

module MSet = OUnitDiff.SetMake (struct 
  type t = Tallying.CS.m
  let compare = 
    (* the abstract field is ignored in the comparison *)
    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
  let pp_printer = Tallying.CS.print_m
  let pp_print_sep = OUnitDiff.pp_comma_separator
end)

Pietro Abate's avatar
Pietro Abate committed
46 47 48
type pp = P of vv * string | N of string * vv
and vv = V of string

49
let mk_pp = function
50 51
  |P(V alpha,t) -> Tallying.CS.singleton (Tallying.Pos (Var.mk alpha,parse_typ t))
  |N(t,V alpha) -> Tallying.CS.singleton (Tallying.Neg (parse_typ t,Var.mk alpha))
52 53 54 55 56 57 58 59 60

let mk_prod l =
    List.fold_left (fun acc2 c ->
      Tallying.CS.prod (mk_pp c) acc2
    ) Tallying.CS.sat l

let mk_union l1 l2 =
  Tallying.CS.union (mk_prod l1) (mk_prod l2)

Pietro Abate's avatar
Pietro Abate committed
61 62
let mk_s ll =
  List.fold_left (fun acc1 l ->
63
    Tallying.CS.union (mk_prod l) acc1
Pietro Abate's avatar
Pietro Abate committed
64 65
  ) Tallying.CS.S.empty ll

66 67 68 69 70
let mk_union_res l1 l2 =
  let aux_merge k v1 v2 = match (k,v1,v2) with
    |(k,None,None) -> assert false
    |(k,Some v,None) -> Some v
    |(k,None,Some v) -> Some v
71
    |((_,v),Some x,Some y) when Types.equiv x y -> Some x
72 73 74 75 76
    |((true,v),Some x,Some y) -> assert false
    |((false,v),Some x,Some y) -> assert false
  in
  let aux l = 
    List.fold_left (fun acc -> function
77 78
      |P(V v,s) -> Tallying.CS.M.merge aux_merge acc (Tallying.CS.M.singleton (true,Var.mk v) (parse_typ s))
      |N(s,V v) -> Tallying.CS.M.merge aux_merge acc (Tallying.CS.M.singleton (false,Var.mk v) (parse_typ s))
79 80 81 82 83 84 85 86 87
    ) Tallying.CS.M.empty l
  in 
  match l1,l2 with
  |[],[] -> Tallying.CS.sat
  |l1,[] -> (Tallying.CS.S.singleton (aux l1))
  |[],l2 -> (Tallying.CS.S.singleton (aux l2))
  |l1,l2 -> Tallying.CS.S.union (Tallying.CS.S.singleton (aux l1)) (Tallying.CS.S.singleton (aux l2))


Pietro Abate's avatar
Pietro Abate committed
88
(* check invariants on the constraints sets *)
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 119 120 121 122 123 124 125 126 127 128 129 130
let test_constraint_ops = [

  "prod pos",mk_prod [P(V "A","Int");P(V "A","Bool")], mk_pp (P(V "A","Int & Bool"));

  "prod neg",mk_prod [N("Int",V "B");N("Bool",V "B")], mk_pp (N("Int | Bool",V "B"));

  "prod var",mk_prod [N("`$B",V "A");P(V "B","Bool | Int")],
      mk_union_res 
        [N("`$B",V "A");P(V "B","Bool | Int")] 
        [];

  "empty", mk_union [P(V "A","Empty")] [P(V "A","Empty")], mk_pp (P(V "A","Empty"));

  "empty <= int 1", mk_union [P(V "A","Int")] [P(V "A","Empty")], mk_pp (P(V "A","Int"));
  "empty <= int 2", mk_union [P(V "A","Empty")] [P(V "A","Int")], mk_pp (P(V "A","Int"));

  "int v bool <= int", mk_union [P(V "A","Int | Bool")] [P(V "A","Int")], mk_pp (P(V "A","Int | Bool"));

  "0 -> 1 <= a -> b", mk_union [P(V "A","Empty -> Any")] [P(V "A","Int -> Bool")], mk_pp (P(V "A","Empty -> Any"));

  "union 1",mk_union [P(V "A","Empty")] [P(V "A","Empty");N("Int",V "B")], mk_pp (P(V "A","Empty"));

  "union 2",mk_union [P(V "A","Empty")] [P(V "A","Int");P(V "A","Bool")],
      mk_union_res 
      [P(V "A","Int & Bool")]
      [P(V "A","Empty")];

  "union 2 comm",mk_union [P(V "A","Int");P(V "A","Bool")] [P(V "A","Empty")],
      mk_union_res
        [P(V "A","Int & Bool")]
        [(P(V "A","Empty"))];

  "union 3",mk_union [P(V "A","Empty")] [P(V "A","Empty");P(V "B","Empty")], mk_pp (P(V "A","Empty"));

  "union 4",mk_union [P(V "A","Empty")] [P(V "A","Empty");P(V "B","Int")], mk_pp (P(V "A","Empty"));

  "union 5",mk_union [P(V "A","Int | Bool");N("Int",V "B");P(V "B","Empty")] [P(V "A","Empty");P(V "B","Empty")],
      mk_union_res 
        [P(V "A","Int | Bool");N("Int",V "B");P(V "B","Empty")]
        [P(V "A","Empty");P(V "B","Empty")];

]
131

132 133 134 135 136 137 138 139 140 141 142
let test_constraints =
  "test tallying data structures" >:::
    List.map (fun (test,result,expected) ->
      test >:: (fun _ ->
        let elem s = (MSet.of_list (Tallying.CS.S.elements s)) in
        MSet.assert_equal (elem expected) (elem result)
      )
    ) test_constraint_ops
;;

(* ^ => & -- v => | *)
Pietro Abate's avatar
Pietro Abate committed
143 144 145 146 147 148

let norm_tests = [
  "(`$A -> Bool)", "(`$B -> `$B)", mk_s [
    [P(V "B","Empty")];
    [N("`$B",V "A");N("Bool",V "B")]
  ];
149

Pietro Abate's avatar
Pietro Abate committed
150 151 152 153
  "`$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")]];
154

Pietro Abate's avatar
Pietro Abate committed
155 156 157 158
  "(Int -> Bool)", "(`$A -> `$B)", mk_s [
    [P(V "A","Empty")];
    [P(V "A","Int");N("Bool",V "B")]
  ];
159

Pietro Abate's avatar
Pietro Abate committed
160 161 162 163 164 165
  "(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")]
  ];
166 167 168 169 170 171

  "(`$A -> `$B)", "(Int -> Int) | (Bool -> Bool)", mk_s [
    [P(V "B","Int");N("Int",V "A")];
    [P(V "B","Bool");N("Bool",V "A")];
  ];

Pietro Abate's avatar
Pietro Abate committed
172
  (*
173 174
  "([0--*] & `true)", "(`$A | Int) & ((Any \\ `$A) | Bool)",
  *)
175

Pietro Abate's avatar
Pietro Abate committed
176
  "(`$A , `$B)","(Int , Bool)", mk_s [
177 178
    [P(V "A","Empty")];
    [P(V "B","Empty")];
Pietro Abate's avatar
Pietro Abate committed
179 180
    [P(V "A","Int");P(V "B","Bool")]
  ];
181 182 183 184 185 186 187 188 189

  "(Int , Bool)","(`$A , `$B)", mk_s [ [N("Int", V "A");N("Bool", V "B")] ];
  "(Bool , Bool)","(`$A , `$B)", mk_s [ [N("Bool", V "A");N("Bool", V "B")] ];

  "(`$A | (`$B , `$C))","(Int , Int)", mk_s [
    [P(V "A","(Int , Int)"); P(V "B","Empty")];
    [P(V "A","(Int , Int)"); P(V "C","Empty")];
    [P(V "A","(Int , Int)"); P(V "B","Int"); P(V "C","Int")];

Pietro Abate's avatar
Pietro Abate committed
190
  ];
191 192

  "(`$A , Int) | (`$B , Bool))","(Int , (Int | Bool))", mk_s [
Pietro Abate's avatar
Pietro Abate committed
193 194
    [P(V "A","Int");P(V "B","Int")]
  ];
195
(*
Pietro Abate's avatar
Pietro Abate committed
196 197 198
  "(`$A1 -> `$B1) -> [ `$A1 ] -> [ `$B1 ]", "((Int -> Bool) | ((`$A \\ Int) -> (`$B \\ Int))) -> `$G", mk_s [
    [P(V "A","Empty")]
  ];
199
  *)
200 201 202 203
]

let test_norm =
  "test tallying norm" >:::
204 205 206 207 208
    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
209 210
        let elem s = MSet.of_list (Tallying.CS.S.elements s) in
        MSet.assert_equal (elem expected) (elem result)
211 212 213 214
      )
    ) norm_tests
;;

215
let merge_tests = [
216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241
  "empty  empty", mk_s [[P(V "A", "Empty");P(V "B", "Empty")]], 
    mk_s [
      [P(V "A","Empty");P(V "B","Empty")]
    ];

  "unsat 1", mk_s [[P(V "A", "Int | Bool");N("Int",V "B");P(V "B", "Empty")]], Tallying.CS.unsat;

  "unsat 2", mk_s [[N("Bool",V "B"); N("`$B", V "A"); P(V "A", "Empty")]], Tallying.CS.unsat;

  "quad", mk_s [[N("Bool | Int",V "B"); N("`$B",V "A"); P(V "A", "Int | Bool")]],
    mk_s [
      [N("`$B", V "A");P(V "A","Int | Bool");N("Int | Bool", V "B"); P(V "B","Int | Bool")]
    ];

  "add one", mk_s [[N("`$B", V "A");P(V "A","Int | Bool")]], 
    mk_s [[N("`$B", V "A");P(V "A","Int | Bool");P(V "B","Int | Bool")]];

  "A B", mk_s [[P(V "A", "`$B")]], mk_pp (P(V "A","`$B"));

  "", mk_s [[P(V "B", "Empty")]], mk_pp (P(V "B","Empty"));

  "", mk_s [[P(V "A", "Int");P(V "B", "Bool"); P(V "A", "Empty")]],
    mk_s [
      [P(V "A","Empty");P(V "B","Bool")]
    ]
];;
242 243 244

let test_merge =
  "test tallying merge" >:::
245 246 247 248 249 250 251 252
    List.map (fun (test,s,expected) ->
      test >:: (fun _ ->
        let result = 
          try 
            Tallying.CS.S.fold (fun c acc ->
              Tallying.CS.union (Tallying.merge c) acc
            ) s Tallying.CS.S.empty
          with Tallying.UnSatConstr -> Tallying.CS.unsat
253
        in
254 255
        let elem s = MSet.of_list (Tallying.CS.S.elements s) in
        MSet.assert_equal (elem expected) (elem result)
256 257 258 259
      )
    ) merge_tests
;;

260 261
let mk_e ll =
  List.map (fun l ->
262
    List.map (fun (V v,t) -> (Var.mk v),(parse_typ t)) l
263 264 265 266
  ) ll

let tallying_tests = [
  [("((Int | Bool) -> Int)", "(`$A -> `$B)"); ("(`$A -> Bool)","(`$B -> `$B)")], mk_e [
267 268
    [(V "A","Int | Bool");(V "B","Int | Bool")];
    [(V "A","Empty");(V "B","Empty")]
269
  ];
Pietro Abate's avatar
Pietro Abate committed
270 271

  [("(Int -> Bool)", "(`$A -> `$B)")], mk_e [
272 273
    [(V "A","Empty")];
    [(V "A","Int");(V "B","Bool")];
Pietro Abate's avatar
Pietro Abate committed
274 275
  ];

276
  [("(Int -> Int) | (Bool -> Bool)", "(`$A -> `$B)")], mk_e [
277
    [(V "A","Empty")];
278
  ];
Pietro Abate's avatar
Pietro Abate committed
279

280 281 282
  [("((Int,Int) , (Int | Bool))","(`$A,Int) | ((`$B,Int),Bool)")], mk_e [
    [(V "A", "(Int,Int)"); (V "B","Int")]
  ];
Pietro Abate's avatar
Pietro Abate committed
283

284
  [("((`$A , Int) & (`$B , Bool))","(Int , (Int & Bool))")], [[]];
Pietro Abate's avatar
Pietro Abate committed
285

286 287 288
  [("((`$A , Int) | (`$B , Bool))","(Int , (Int | Bool))")], mk_e [
    [(V "A","Int");(V "B","Int")]
  ];
289 290 291 292 293 294
]

let test_tallying =
  let print_test l =
    String.concat ";" (List.map (fun (s,t) -> Printf.sprintf " %s \\ %s" s t) l)
  in
295
  "test tallying" >:::
296 297 298 299
    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
300 301
        let elem s = SubStSet.of_list (List.map (fun l -> ESet.of_list l) s) in
        SubStSet.assert_equal (elem expected) (elem result)
302 303 304 305
      )
    ) tallying_tests
;;

306 307
let all =
  "all tests" >::: [
308
    test_constraints;
309
    test_norm;
310
    test_merge;
311
    test_tallying;
312 313 314 315 316 317 318 319
  ]
 
let main () =
  OUnit.run_test_tt_main all
;;
 
main ()