Commit 9a7819e6 authored by Pietro Abate's avatar Pietro Abate
Browse files

Add (broken) unit tests for apply_raw

parent cee524ae
......@@ -342,12 +342,145 @@ let test_tallying =
) tallying_tests
;;
let apply_raw_tests = [
"iter hd",
"(`$A -> []) -> [ `$A* ] -> []","[ `$A0* ] -> `$A0";
"iteri assoc",
"(Int -> `$A -> []) -> [ `$A* ] -> []","`$A1 -> [ (`$A1 , `$B1)* ] -> `$B1";
"map length",
"(`$A -> `$B) -> [ `$A* ] -> [ `$B* ]","[ `$A3* ] -> Int";
"map length & hd",
"(`$A -> `$B) -> [ `$A* ] -> [ `$B* ]","([ `$A3* ] -> Int) & ([ `$A4* ] -> `$A4)";
"mapi mem",
"(Int -> `$A -> `$B) -> [ `$A* ] -> [ `$B* ]","`$A45 -> [ `$A45* ] -> Bool";
"mapi mem & memq",
"(Int -> `$A -> `$B) -> [ `$A* ] -> [ `$B* ]","(`$A45 -> [ `$A45* ] -> Bool) & (`$A46 -> [ `$A46* ] -> Bool)";
"rev_map length",
"(`$A -> `$B) -> [ `$A* ] -> [ `$B* ]","[ `$A53* ] -> Int";
"rev_map length & hd",
"(`$A -> `$B) -> [ `$A* ] -> [ `$B* ]","([ `$A53* ] -> Int) & ([ `$A54* ] -> `$A54)";
"fold_left append",
"(`$A -> `$B -> `$A) -> `$A -> [ `$B* ] -> `$A","[ `$A95* ] -> [ `$A95* ] -> [ `$A95* ]";
"fold_right hd",
"(`$A -> `$B -> `$B) -> [ `$A* ] -> `$B -> `$B","[ `$A103* ] -> `$A103";
"iter2 hd",
"(`$A -> `$B -> []) -> [ `$A* ] -> [ `$B* ] -> []","[ `$A117* ] -> `$A117";
"map2 hd",
"(`$A -> `$B -> `$C) -> [ `$A* ] -> [ `$B* ] -> [ `$C* ]","[ `$A124* ] -> `$A124";
"rev_map2 hd",
"(`$A -> `$B -> `$C) -> [ `$A* ] -> [ `$B* ] -> [ `$C* ]","[ `$A160* ] -> `$A160";
"fold_left2 assoc",
"(`$A -> `$B -> `$C -> `$A) -> `$A -> [ `$B* ] -> [ `$C* ] -> `$A","`$A196 -> [ (`$A196 , `$B196)* ] -> `$B196";
"for_all hd",
"(`$A -> Bool) -> [ `$A* ] -> Bool","[ `$A198* ] -> `$A198";
"exists hd",
"(`$A -> Bool) -> [ `$A* ] -> Bool","[ `$A199* ] -> `$A199";
"for_all2 hd",
"(`$A -> `$B -> Bool) -> [ `$A* ] -> [ `$B* ] -> Bool","[ `$A200* ] -> `$A200";
"exists2 hd",
"(`$A -> `$B -> Bool) -> [ `$A* ] -> [ `$B* ] -> Bool","[ `$A211* ] -> `$A211";
"mem length",
"`$A -> [ `$A* ] -> Bool","[ `$A222* ] -> Int";
"memq length",
"`$A -> [ `$A* ] -> Bool","[ `$A264* ] -> Int";
"find hd",
"(`$A -> Bool) -> [ `$A* ] -> `$A","[ `$A306* ] -> `$A306";
"filter hd",
"(`$A -> Bool) -> [ `$A* ] -> [ `$A* ]","[ `$A307* ] -> `$A307";
"find_all hd",
"(`$A -> Bool) -> [ `$A* ] -> [ `$A* ]","[ `$A308* ] -> `$A308";
"partition hd",
"(`$A -> Bool) -> [ `$A* ] ->( [ `$A* ] , [ `$A* ])","[ `$A309* ] -> `$A309";
"assoc length",
"`$A -> [ (`$A , `$B)* ] -> `$B","[ `$A310* ] -> Int";
"assoc length & hd",
"`$A -> [ (`$A , `$B)* ] -> `$B","([ `$A310* ] -> Int) & ([ `$A311* ] -> `$A311)";
"mem_assoc length",
"`$A -> [ (`$A , `$B)* ] -> Bool","[ `$A394* ] -> Int";
"mem_assoc length & hd",
"`$A -> [ (`$A , `$B)* ] -> Bool","([ `$A394* ] -> Int) & ([ `$A395* ] -> `$A395)";
"mem_assq length",
"`$A -> [ (`$A , `$B)* ] -> Bool","[ `$A436* ] -> Int";
"mem_assq length & hd",
"`$A -> [ (`$A , `$B)* ] -> Bool","([ `$A436* ] -> Int) & ([ `$A437* ] -> `$A437)";
"remove_assoc length",
"`$A -> [ (`$A , `$B)* ] -> [ (`$A , `$B)* ]","[ `$A478* ] -> Int";
"remove_assoc length & hd",
"`$A -> [ (`$A , `$B)* ] -> [ (`$A , `$B)* ]","([ `$A478* ] -> Int) & ([ `$A479* ] -> `$A479)";
]
let test_apply =
let print_test msg s t = Printf.sprintf "%s : (%s) o (%s)\n" msg s t in
"apply" >:::
let sigmacup sl t =
List.fold_left (fun acc sigma ->
Types.cap acc Tallying.(t $$ sigma)
) Types.any sl
in
List.map (fun (msg,s,t) ->
(print_test msg s t) >:: (fun _ ->
try
let (s,t) = (parse_typ s,parse_typ t) in
let (sl,s,t,g) = Types.apply_raw s t in
let s_sigma = sigmacup sl s in
let t_sigma = sigmacup sl t in
let t_sigma_domain = (Types.Arrow.domain(Types.Arrow.get t_sigma)) in
assert_equal ~pp_diff:(fun fmt _ ->
Format.fprintf fmt "t @@ sl < 0 - 1 = %a\n" Types.Print.print t_sigma
) (Types.subtype t_sigma (parse_typ "Empty -> Any")) true;
assert_equal ~pp_diff:(fun fmt _ ->
Format.fprintf fmt "sl = %a\n" Types.Tallying.CS.pp_sl sl;
Format.fprintf fmt "(s @@ sl) = %a\n" Types.Print.print s_sigma;
Format.fprintf fmt "(t @@ sl) = %a\n" Types.Print.print t_sigma;
Format.fprintf fmt "g = %a\n" Types.Print.print g;
Format.fprintf fmt "domain(t @@ sl) = %a\n" Types.Print.print t_sigma_domain
) (Types.subtype s_sigma t_sigma) true
with Tallying.Step1Fail -> assert_equal [] []
)
) apply_raw_tests
;;
let suite =
"tests" >::: [
test_constraints;
test_norm;
test_merge;
test_tallying;
test_apply;
]
let main () =
......
......@@ -3247,6 +3247,9 @@ module Tallying = struct
in
(CS.ES.elements el)
(* apply sigma to t *)
let ($$) t si = CS.E.fold (fun v sub acc -> Positive.substitute acc (v,sub)) si t
type symsubst = I | S of CS.sigma | A of (symsubst * symsubst)
let rec dom = function
......@@ -3264,9 +3267,6 @@ module Tallying = struct
)
)
(* apply sigma to t *)
let ($$) t si = CS.E.fold (fun v sub acc -> Positive.substitute acc (v,sub)) si t
(* apply a symbolic substitution si to a type t *)
let (@@) t si =
let vst = ref Var.Set.empty in
......@@ -3375,7 +3375,7 @@ let apply_raw s t =
let apply_full s t =
let _,_,_,res = apply_raw s t in
Format.printf "result: %a@\n@." Print.print res;
(* Format.printf "result: %a@\n@." Print.print res; *)
res
let apply s t = let s,_,_,_ = apply_raw s t in s
......
......@@ -851,7 +851,6 @@ let flatten arg constr precise =
let rec type_check env e constr precise =
Printf.printf "aaaa\n%!";
let (ed,d) = type_check' e.exp_loc env e.exp_descr constr precise in
let d = if precise then d else constr in
e.exp_typ <- Types.cup e.exp_typ d;
......@@ -863,9 +862,8 @@ and type_check' loc env ed constr precise = match ed with
let t = Types.descr t in
ignore (type_check env e t false);
(ed,verify loc t constr)
(*
| Subst (e, sigma) -> (ed,type_check env e constr precise)
*)
| Subst (e, sigma) -> (* (ed,type_check env e constr precise) *) assert false
| Check (t0,e,t) ->
let te = type_check env e Types.any true in
......@@ -895,15 +893,12 @@ and type_check' loc env ed constr precise = match ed with
(fst(Types.squaresubtype env.delta t t2))::tacc (* H_j *)
) [] a.fun_iface
in
List.iter (function
(* If sigma empty (sat, we do not need any subst ...
| sigma when Types.Tallying.CS. sigma -> () *)
| sigma ->
List.iter (fun br ->
let e = br.br_body in
let loc = br.br_body.exp_loc in
br.br_body <- exp' loc (Subst(e,sigma));
) a.fun_body.br_branches
List.iter (fun sigma ->
List.iter (fun br ->
let e = br.br_body in
let loc = br.br_body.exp_loc in
br.br_body <- exp' loc (Subst(e,sigma));
) a.fun_body.br_branches
) (List.rev sl_list);
(ed,t)
......
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