Commit 0b580bbb authored by Pietro Abate's avatar Pietro Abate
Browse files

Merge branch 'master' into typing-test

parents ebe77f50 74752b11
...@@ -13,23 +13,8 @@ let to_string pp t = ...@@ -13,23 +13,8 @@ let to_string pp t =
Format.fprintf Format.str_formatter "%a@." pp t; Format.fprintf Format.str_formatter "%a@." pp t;
Format.flush_str_formatter () Format.flush_str_formatter ()
;; ;;
(*
let variance_test = [
"`$A -> `$B", [("A",`Covariant);("B",`ContraVariant)];
]
let test_variance =
"test variance annotations" >:::
List.map (fun (t1,expected) ->
(Printf.sprintf " %s" t1) >:: (fun _ ->
let t = parse_typ t1 in
assert_equal ~cmp:Types.equal ~printer:(to_string Types.Print.print) t1 t2
)
) set_op_tests
;;
*)
let tlv_tests = [ let tlv_tests = [ "is_var", [
"`$A", Types.is_var, true; "`$A", Types.is_var, true;
"Int", Types.is_var, false; "Int", Types.is_var, false;
"Empty", Types.is_var, false; "Empty", Types.is_var, false;
...@@ -38,38 +23,56 @@ let tlv_tests = [ ...@@ -38,38 +23,56 @@ let tlv_tests = [
"`$A & Any", Types.is_var, true; "`$A & Any", Types.is_var, true;
"`$A | Int", Types.is_var, false; "`$A | Int", Types.is_var, false;
"(`$A,Int)", Types.is_var, false; "(`$A,Int)", Types.is_var, false;
];
"no_var", [
"Int", Types.no_var, true; "Int", Types.no_var, true;
"Any", Types.no_var, true; "Any", Types.no_var, true;
"Empty", Types.no_var, true; "Empty", Types.no_var, true;
"`A", Types.no_var, true; "`A", Types.no_var, true;
"`$A", Types.no_var, false; "`$A", Types.no_var, false;
"`$A & `$B", Types.no_var, false;
"`$A & Int", Types.no_var, false; "`$A & Int", Types.no_var, false;
"`$A | Int", Types.no_var, false; "`$A | Int", Types.no_var, false;
"`$A | Char", Types.no_var, false;
"(`$A,Int)", Types.no_var, false; "(`$A,Int)", Types.no_var, false;
"(Char,Int)", Types.no_var, true; "(Char,Int)", Types.no_var, true;
];
"has_tlv", [
"Int", Types.has_tlv, false; "Int", Types.has_tlv, false;
"Any", Types.has_tlv, false; "Any", Types.has_tlv, false;
"Empty", Types.has_tlv, false; "Empty", Types.has_tlv, false;
"`A", Types.has_tlv, false; "`A", Types.has_tlv, false;
"`$A", Types.has_tlv, true; "`$A", Types.has_tlv, true;
"`$A & Int", Types.has_tlv, true;
"`$A | Int", Types.has_tlv, true;
"(`$A,Int)", Types.has_tlv, false; "(`$A,Int)", Types.has_tlv, false;
"`$B | (`$A,Int)", Types.has_tlv, false; "`$A & Int", Types.has_tlv, false;
"`$A | (Char,Int)", Types.has_tlv, false; "`$A | Int", Types.has_tlv, false;
"`$A | Char", Types.has_tlv, false;
"`$A | (Any,Any)", Types.has_tlv, false;
"`$A | (`$B,Int)", Types.has_tlv, true;
"`$A | (Char,Int)", Types.has_tlv, true;
];
] ]
let test_tlv_operations = let test_tlv_operations =
"test TLV operations" >::: "test TLV operations" >:::
List.map (fun (t,f,e) -> List.flatten (
(Printf.sprintf "test %s " t) >:: (fun _ -> List.map (fun (s,l) ->
let t = parse_typ t in List.map (fun (t,f,e) ->
assert_equal ~pp_diff:(fun fmt _ -> Types.Print.print fmt t) (f t) e (Printf.sprintf "test %s %s " s t) >:: (fun _ ->
) let t = (parse_typ t) in
) tlv_tests assert_equal ~pp_diff:(fun fmt _ ->
Format.fprintf fmt "%s = %b\ndump = %s\nrepr = %s\n"
s e
(to_string Types.dump t)
(to_string Types.Print.print t))
(f t) e
)
) l
) tlv_tests
)
;; ;;
let set_op_tests = [ let set_op_tests = [
...@@ -121,10 +124,12 @@ let test_substitution = ...@@ -121,10 +124,12 @@ let test_substitution =
let rec_subst_tests = [ let rec_subst_tests = [
"`$A", "A", "Empty"; "`$A", "A", "Empty";
"`$A", "B", "`$A"; "`$A", "B", "`$A";
"`$A -> `$B", "A", "X where X = X -> `$B";
"Bool -> `$B", "A", "Bool -> `$B"; "Bool -> `$B", "A", "Bool -> `$B";
"(`$A , `$B)", "A", "X where X = (X, `$B)"; "(`$A , `$B)", "A", "X where X = (X, `$B)";
(*
"`$A -> `$B", "A", "X where X = X -> `$B";
"(`$A , (`$B -> (Bool -> `$C)))", "C", "X where X = (`$A , (`$B -> (Bool -> X)))"; "(`$A , (`$B -> (Bool -> `$C)))", "C", "X where X = (`$A , (`$B -> (Bool -> X)))";
*)
];; ];;
let test_rec_subtitutions = let test_rec_subtitutions =
......
...@@ -163,37 +163,37 @@ module TLV = struct ...@@ -163,37 +163,37 @@ module TLV = struct
aux ppf (elements s) aux ppf (elements s)
end end
(* s : top level variables (* tlv : top level variables
* f : all free variables in the subtree * fv : all free variables in the subtree
* b : true if the type contains only variables *) * varonly : true if the type contains only variables *)
type t = { s : Set.t ; f : Var.Set.t ; b : bool } type t = { tlv : Set.t ; fv : Var.Set.t ; varonly : bool }
let empty = { s = Set.empty ; f = Var.Set.empty ; b = false } let empty = { tlv = Set.empty ; fv = Var.Set.empty ; varonly = false }
let any = { s = Set.empty ; f = Var.Set.empty ; b = false } let any = { tlv = Set.empty ; fv = Var.Set.empty ; varonly = false }
let singleton (v,p) = { s = Set.singleton (v,p); f = Var.Set.singleton v; b = true } let singleton (v,p) = { tlv = Set.singleton (v,p); fv = Var.Set.singleton v; varonly = true }
(* return the max of top level variables *) (* return the max of top level variables *)
let max x = Set.max_elt x.s let max x = Set.max_elt x.tlv
let pair x y = { let pair x y = {
b = false ; varonly = false ;
s = Set.empty ; tlv = Set.empty ;
f = Var.Set.union x.f y.f fv = Var.Set.union x.fv y.fv
} }
(* true if it contains only one variable *) (* true if it contains only one variable *)
let is_single x = x.b && (Var.Set.cardinal x.f = 1) && (Set.cardinal x.s = 1) let is_single x = x.varonly && (Var.Set.cardinal x.fv = 1) && (Set.cardinal x.tlv = 1)
let no_variables x = (x.b == false) && (Var.Set.cardinal x.f = 0) && (Set.cardinal x.s = 0) let no_variables x = (x.varonly == false) && (Var.Set.cardinal x.fv = 0) && (Set.cardinal x.tlv = 0)
let has_toplevel x = Set.cardinal x.s > 0 let has_toplevel x = Set.cardinal x.tlv > 0
let print ppf x = if x.b then Set.print ";" ppf x.s let print ppf x = if x.varonly then Set.print ";" ppf x.tlv
let dump ppf x = let dump ppf x =
Format.fprintf ppf "<b = %b ; f = {%a} ; s = {%a}>" Format.fprintf ppf "<varonly = %b ; fv = {%a} ; tlv = {%a}>"
x.b Var.Set.print x.f (Set.print ";") x.s x.varonly Var.Set.print x.fv (Set.print ";") x.tlv
let mem v x = Set.mem v x.s let mem v x = Set.mem v x.tlv
end end
...@@ -453,7 +453,7 @@ let is_var t = TLV.is_single t.toplvars ...@@ -453,7 +453,7 @@ let is_var t = TLV.is_single t.toplvars
let no_var t = TLV.no_variables t.toplvars let no_var t = TLV.no_variables t.toplvars
let has_tlv t = TLV.has_toplevel t.toplvars let has_tlv t = TLV.has_toplevel t.toplvars
let all_vars t = t.toplvars.TLV.f let all_vars t = t.toplvars.TLV.fv
(* XXX this function could be potentially costly. There should be (* XXX this function could be potentially costly. There should be
* better way to take trace of top level variables in a type *) * better way to take trace of top level variables in a type *)
...@@ -492,8 +492,12 @@ let update_tlv x y t = ...@@ -492,8 +492,12 @@ let update_tlv x y t =
(aux BoolRec.get t.record) (aux BoolRec.get t.record)
] ]
in in
let s = tlv t in { t with toplvars =
{ t with toplvars = { s = s ; f = Var.Set.union x.toplvars.f y.toplvars.f ; b = x.toplvars.b && x.toplvars.b } } {
tlv = tlv t ;
fv = Var.Set.union x.toplvars.fv y.toplvars.fv ;
varonly = x.toplvars.varonly && x.toplvars.varonly
} }
;; ;;
let char c = { empty with chars = BoolChars.atom (`Atm c) } let char c = { empty with chars = BoolChars.atom (`Atm c) }
...@@ -1972,9 +1976,9 @@ struct ...@@ -1972,9 +1976,9 @@ struct
Print.assign_name t; Print.assign_name t;
t;; t;;
let trace msg = let trace msg =
(* output_string stderr (msg ^ "\n"); (* output_string stderr (msg ^ "\n");
flush stderr *) flush stderr *)
();; ();;
let print_to_string f = let print_to_string f =
...@@ -2511,7 +2515,7 @@ struct ...@@ -2511,7 +2515,7 @@ struct
* position with any *) * position with any *)
let substituterec t alpha = let substituterec t alpha =
let subst x d = let subst x d =
if Var.equal d alpha then x if Var.equal d alpha then x
else var d else var d
in in
if no_var t then t if no_var t then t
...@@ -2557,9 +2561,9 @@ struct ...@@ -2557,9 +2561,9 @@ struct
| (b1, v1) :: ll -> (b1==b && v1==v) || (memq_pair key ll) | (b1, v1) :: ll -> (b1==b && v1==v) || (memq_pair key ll)
in in
let memo = ref [] in let memo = ref [] in
(* we memoize based on the pair (pos, v), since v can occur both (* we memoize based on the pair (pos, v), since v can occur both
* positively and negatively. and we want to manage the variables * positively and negatively. and we want to manage the variables
* differently in both cases *) * differently in both cases *)
let rec aux pos v = let rec aux pos v =
if not (memq_pair (pos,v) !memo) then if not (memq_pair (pos,v) !memo) then
let () = memo := (pos,v) :: !memo in let () = memo := (pos,v) :: !memo in
...@@ -3198,8 +3202,8 @@ let apply_raw s t = ...@@ -3198,8 +3202,8 @@ let apply_raw s t =
Queue.add (aux (0,lazy(s)) (1,lazy(Positive.substitutefree t)) s t) q; Queue.add (aux (0,lazy(s)) (1,lazy(Positive.substitutefree t)) s t) q;
let result = ref ([],(any,any)) in let result = ref ([],(any,any)) in
let counter = ref 0 in let counter = ref 0 in
(* I removed the condition to stop at the first solution since, (* I removed the condition to stop at the first solution since,
at least for map even it is only partial *) at least for map even it is only partial *)
while not(Queue.is_empty q) do while not(Queue.is_empty q) do
try try
incr counter; (* don't know about termination... *) incr counter; (* don't know about termination... *)
...@@ -3221,13 +3225,17 @@ let apply_full s t = ...@@ -3221,13 +3225,17 @@ let apply_full s t =
cap tacc (List.fold_left (fun tacc subst -> cap tacc (List.fold_left (fun tacc subst ->
Positive.substitute tacc subst) t constr_lst)) any subst_lst Positive.substitute tacc subst) t constr_lst)) any subst_lst
in in
let arr = Arrow.get ss in (*let arr = Arrow.get ss in
let res = Arrow.apply arr (tt) in let res = Arrow.apply arr (tt) in *)
let ss = Positive.clean_type ss in let ss = Positive.clean_type ss in
let tt = Positive.clean_type tt in let tt = Positive.clean_type tt in
let res = Positive.clean_type res in (*let res = Positive.clean_type res in *)
Format.printf "sl = %a\nfunction type = %a\nargument type = %a\nresult type = %a\n\n%!" let res2 = List.fold_left
Tallying.CS.pp_sl subst_lst Print.print ss Print.print tt Print.print res; res (fun acc l -> cap acc (snd (List.find (fun (`Var v, _) -> 0 == String.compare v.Var.id "Gamma") l))) any subst_lst
in
let res2 = Positive.clean_type res2 in
Format.printf "sl = %a\nfunction type = %a\nargument type = %a\nresult type = %a\n%!"
Tallying.CS.pp_sl subst_lst Print.print ss Print.print tt Print.print res2; res2
let apply s t = fst (apply_raw s t) let apply s t = fst (apply_raw s 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