Skip to content

GitLab

Commit 7a744984 authored by Pietro Abate's avatar Pietro Abate
Browse files

Minor changes and comments

parent b9334e65
Hide whitespace changes
Inline Side-by-side
tests/libtest/tallyingTest.ml
View file @ 7a744984
......@@ -15,6 +15,9 @@ 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))
(* ^ => |
* v => &
*)
let norm_tests = [
"(`$A -> Bool)", "(`$B -> `$B)",
cup (mk_pos ("B","Empty"))
......@@ -58,21 +61,16 @@ let norm_tests = [
"(`$A , `$B)","(Int , Bool)",
cap
(mk_pos ("A","Int"))
(mk_pos ("B","Bool"))
(*
cup
(mk_pos ("A","Empty"))
(cup
(cap
(mk_pos ("A","Int"))
(mk_pos ("B","Bool"))
)
(mk_pos ("B","Empty"))
);
*)
(mk_pos ("B","Bool"));
"(`$A & (`$B , `$C))","(Int , Int)",mk_pos ("A","(Int , Int) | (Any \\ (`$B , `$C))");
"(`$A , Int) & (`$B , Bool))","(Int , (Int & Bool))", cap (mk_pos ("A","Int")) (mk_pos ("B","Int"));
]
let m_compare = Tallying.CS.M.compare Types.compare
(* 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
module MList = OUnitDiff.ListSimpleMake (struct
type t = Tallying.CS.m
......@@ -135,17 +133,17 @@ let test_merge =
) merge_tests
;;
let e_compare = Tallying.CS.E.compare Types.compare
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 *)
let compare_constr (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 t1 t2
else Types.compare (diff t1 a) (diff t2 a)
module EList = OUnitDiff.ListSimpleMake (struct
type t = (Var.var * Types.t)
......@@ -168,13 +166,13 @@ let mk_e ll =
let tallying_tests = [
[("((Int | Bool) -> Int)", "(`$A -> `$B)"); ("(`$A -> Bool)","(`$B -> `$B)")], mk_e [
(* [("A","Empty");("B","Empty")]; *)
[("A","Int | Bool");("B","Int | Bool")]
];
[("(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")]];
[("(`$A , Int) & (`$B , Bool))","(Int , (Int & Bool))")], mk_e [[("A","Int");("B","Int")]];
]
let test_tallying =
......
types/types.ml
View file @ 7a744984
......@@ -2288,7 +2288,6 @@ module Tallying = struct
let c = compare Descr.compare m1 m2 in
if c = 0 then true
else
let m1,m2 = if c < 0 then m1,m2 else m2,m1 in
for_all (fun k1 t1 ->
exists (fun k2 t2 -> k1 == k2 && subtype t1 t2) m2
) m1
......@@ -2367,15 +2366,24 @@ module Tallying = struct
let sat = S.singleton M.empty
let unsat = S.empty
(* this is O(n^2) filter . Only more restritive constraints sets are kept *)
let cup x y =
let c = (S.cardinal x) - (S.cardinal y) in
let aux s1 s2 =
S.fold (fun m acc ->
if S.exists (M.subtype m) s2 then S.add m acc else acc
) s1 s2
in
if c <= 0 then aux x y else aux y x
match S.is_empty x,S.is_empty y with
|true,true -> S.empty
|false,true -> x
|true,false -> y
|false,false ->
let c = (S.cardinal x) - (S.cardinal y) in
let aux s1 s2 =
S.fold (fun m acc ->
if M.is_empty m then acc
else if S.exists (M.subtype m) s2 then S.add m acc
else acc
) s1 s2
in
(* Printf.printf "c = %d - #x = %d #y = %d\n" c (S.cardinal x) (S.cardinal y) ; *)
if c <= 0 then aux x y else aux y x
(* cartesian product of two sets of contraints sets where each
* resulting constraint set is than merged *)
......@@ -2407,8 +2415,7 @@ module Tallying = struct
let t = cap (aux id constr any p) (aux neg constr any n) in
(* XXX the abstract field could be messed up ... maybe *)
if b then (* t = bigdisj ... alpha \in P --> alpha <= neg t *)
let t1 = neg t in
{ t1 with abstract = Abstract.empty }
{ (neg t) with abstract = Abstract.empty }
else (* t = bigdisj ... alpha \in N --> t <= alpha *)
{ t with abstract = Abstract.empty }
......@@ -2483,10 +2490,10 @@ module Tallying = struct
* prod'(t1,t2,{s1,s2} v n) = [t1\s1] ^ prod'(t1\s1,t2,n) v
* [t2\s2] ^ prod'(t1,t2\s2,n)
* *)
and normpair ( (t,mem) : (BoolPair.s * DescrSet.t) ) =
and normpair (t,mem) =
let mem = DescrSet.add { empty with times = BoolPair.atom (`Atm t) } mem in
let norm_prod pos neg =
let rec aux (t1 : s) (t2 : s ) = function
let rec aux t1 t2 = function
|[] -> CS.S.empty
|(s1,s2) :: rest ->
let z1 = diff t1 (descr s1) in
......@@ -2508,7 +2515,7 @@ module Tallying = struct
in
List.fold_left (fun acc (p,n) -> CS.cap acc (norm_prod p n)) CS.sat (Pair.get t)
and normrec ( (t,mem) : (BoolRec.s * DescrSet.t) ) =
and normrec (t,mem) =
let mem = DescrSet.add { empty with record = BoolRec.atom (`Atm t) } mem in
let norm_rec ((oleft,left),rights) =
let rec aux accus seen = function
......@@ -2535,7 +2542,7 @@ module Tallying = struct
P(Q v {a}) = {a} v P(Q) v {X v {a} | X \in P(Q) }
*)
and normarrow ((t,mem) : (BoolPair.s * DescrSet.t) ) =
and normarrow (t,mem) =
let mem = DescrSet.add { empty with arrow = BoolPair.atom (`Atm t) } mem in
let rec norm_arrow pos neg =
match neg with
......@@ -2587,6 +2594,7 @@ module Tallying = struct
let merge m = merge (m,DescrSet.empty)
let solve s =
(* Add constraints of the form { alpha = ( s v fresh) ^ t } *)
let aux v (s,t) acc =
if CS.E.mem v acc then assert false else
if equal s empty && equal t any then
......@@ -2600,23 +2608,26 @@ module Tallying = struct
in
let aux m =
let cache = Hashtbl.create (CS.M.cardinal m) in
CS.M.fold (fun (b,v) s acc ->
if Hashtbl.mem cache v then acc else begin
Hashtbl.add cache v ();
CS.M.fold (fun (b,alpha) s acc ->
if Hashtbl.mem cache alpha then acc else begin
Hashtbl.add cache alpha ();
try
let t = CS.M.find (not b,v) m in
(* if t containts only a toplevel variable and nothing else *)
let t = CS.M.find (not b,alpha) m in
(* if t containts only a toplevel variable and nothing else
* means that the constraint is of the form (alpha,beta). *)
if t.toplvars.b && (Var.Set.cardinal t.toplvars.s) = 1 then begin
if b then
let z = Var.Set.max_elt t.toplvars.s in
aux z (empty,any) acc
else
let acc1 = if b then aux v (empty,t) acc else aux v (t,any) acc in
aux v (empty,any) acc1
let beta = Var.Set.max_elt t.toplvars.s in
let acc1 = aux beta (empty,any) acc in
(* alpha <= beta --> { empty <= alpha <= beta ; empty <= beta <= any } *)
if b then aux alpha (empty,t) acc1
else aux alpha (t,any) acc1
end else
if b then aux v (t,s) acc else aux v (s,t) acc
(* alpha = ( s v fresh) ^ t *)
if b then aux alpha (t,s) acc else aux alpha (s,t) acc
with Not_found ->
if b then aux v (any,s) acc else aux v (s,empty) acc
(* upper bond or lower bound is missing, we replace it
* with a constratint of the form empty <= alpha <= s | s <= alpha <= any *)
if b then aux alpha (empty,s) acc else aux alpha (s,any) acc
end
) m CS.E.empty
in
......
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