Commit 94b6c4a7 authored by Pietro Abate's avatar Pietro Abate
Browse files

Add Tallying soundness test

parent 7e813766
...@@ -310,6 +310,7 @@ let tallying_tests = [ ...@@ -310,6 +310,7 @@ let tallying_tests = [
[("(`$A -> `$B) -> [`$A] -> [`$B]","(Int -> Bool) & ((`$A \\ Int) -> (`$A \\ Int))")], [[]]; [("(`$A -> `$B) -> [`$A] -> [`$B]","(Int -> Bool) & ((`$A \\ Int) -> (`$A \\ Int))")], [[]];
] ]
(* to test tallying { sigma_i } -- > for all i => s sigma_i <= t sigma_i *)
let test_tallying = let test_tallying =
let print_test l = let print_test l =
String.concat ";" (List.map (fun (s,t) -> Printf.sprintf " %s \\ %s" s t) l) String.concat ";" (List.map (fun (s,t) -> Printf.sprintf " %s \\ %s" s t) l)
...@@ -320,8 +321,17 @@ let test_tallying = ...@@ -320,8 +321,17 @@ let test_tallying =
try try
let l = List.map (fun (s,t) -> (parse_typ s,parse_typ t)) l in let l = List.map (fun (s,t) -> (parse_typ s,parse_typ t)) l in
let result = Tallying.tallying l in let result = Tallying.tallying l in
List.iter (fun (s,t) ->
List.iter (fun sigma ->
let s_sigma = Tallying.apply_subst s sigma in
let t_sigma = Tallying.apply_subst t sigma in
assert_equal (Types.subtype s_sigma t_sigma) true
) result
) l
(*
let elem s = SubStSet.of_list (List.map (fun l -> ESet.of_list l) s) in let elem s = SubStSet.of_list (List.map (fun l -> ESet.of_list l) s) in
SubStSet.assert_equal (elem expected) (elem result) SubStSet.assert_equal (elem expected) (elem result)
*)
with Tallying.Step1Fail -> assert_equal expected [] with Tallying.Step1Fail -> assert_equal expected []
) )
) tallying_tests ) tallying_tests
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment