Commit df8cc601 authored by Pietro Abate's avatar Pietro Abate
Browse files

API change

Tallying.CS.cup -> union
Tallying.CS.cap -> prod

lessgeneral m1 m2 check if the constraint set m1 is less general of m2
parent 7a744984
......@@ -8,62 +8,65 @@ let parse_typ s =
Types.descr nodepat
;;
let cup = Tallying.CS.cup
let cap = Tallying.CS.cap
let union = Tallying.CS.union
let prod = Tallying.CS.prod
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 => &
*)
type pp = P of vv * string | N of string * vv
and vv = V of string
let mk_s ll =
List.fold_left (fun acc1 l ->
let x =
List.fold_left (fun acc2 -> function
|P(V a,b) -> Tallying.CS.prod (mk_pos (a,b)) acc2
|N(a,V b) -> Tallying.CS.prod (mk_neg (a,b)) acc2
) Tallying.CS.S.empty l
in Tallying.CS.union x acc1
) Tallying.CS.S.empty ll
(* check invariants on the constraints sets *)
let constraints_test = [];;
(* ^ => | -- v => & *)
let norm_tests = [
"(`$A -> Bool)", "(`$B -> `$B)",
cup (mk_pos ("B","Empty"))
(cap
(mk_neg ("`$B","A"))
(mk_neg ("Bool","B"))
);
"`$B", "`$A", mk_neg ("`$B","A");
"`$B", "Empty", mk_pos ("B","Empty");
"Int", "`$B", mk_neg ("Int","B");
"Int", "(`$A | `$B)", mk_neg ("Int \\ `$B","A");
"(Int -> Bool)", "(`$A -> `$B)",
cup (mk_pos ("A","Empty"))
(cap
(mk_pos ("A","Int"))
(mk_neg ("Bool","B"))
);
"(Int -> Int) | (Bool -> Bool)", "(`$A -> `$B)",
cup
(mk_pos ("A","Empty"))
(cup
(cup
(cap
(mk_pos ("A","Empty"))
(mk_neg ("Int","B"))
)
(cap
(mk_pos ("A","Empty"))
(mk_neg ("Bool","B"))
)
)
(cap
(mk_pos ("A","Empty"))
(mk_neg ("Int | Bool","B"))
)
);
(*
"(`$A -> Bool)", "(`$B -> `$B)", mk_s [
[P(V "B","Empty")];
[N("`$B",V "A");N("Bool",V "B")]
];
"`$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")]];
"(Int -> Bool)", "(`$A -> `$B)", mk_s [
[P(V "A","Empty")];
[P(V "A","Int");N("Bool",V "B")]
];
"(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")]
];
(*
"([0--*] & `true)", "(`$A | Int) & ((Any \\ `$A) | Bool)",
*)
"(`$A , `$B)","(Int , Bool)",
cap
(mk_pos ("A","Int"))
(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"));
"(`$A , `$B)","(Int , Bool)", mk_s [
[P(V "A","Int");P(V "B","Bool")]
];
"(`$A & (`$B , `$C))","(Int , Int)", mk_s [
[P(V "A","(Int , Int) | (Any \\ (`$B , `$C))")]
];
"(`$A , Int) & (`$B , Bool))","(Int , (Int & Bool))", mk_s [
[P(V "A","Int");P(V "B","Int")]
];
"(`$A1 -> `$B1) -> [ `$A1 ] -> [ `$B1 ]", "((Int -> Bool) | ((`$A \\ Int) -> (`$B \\ Int))) -> `$G", mk_s [
[P(V "A","Empty")]
];
]
(* the abstract field is ignored in the comparison *)
......@@ -93,22 +96,22 @@ let test_norm =
;;
let merge_tests = [
[("`$A", "Empty");("`$B", "Empty")], cap (mk_pos ("A", "Empty")) (mk_pos ("B", "Empty"));
[("`$A", "Empty");("`$B", "Empty")], prod (mk_pos ("A", "Empty")) (mk_pos ("B", "Empty"));
[("`$A", "Int | Bool");("Int","`$B");("`$B", "Empty")], Tallying.CS.unsat;
[("Bool","`$B"); ("`$B", "`$A"); ("`$A", "Empty")], Tallying.CS.unsat;
[("Bool","`$B"); ("Int","`$B"); ("`$B","`$A"); ("`$A", "Int | Bool")],
cap
Tallying.CS.prod
(mk_neg ("`$B","A")) (
cap
Tallying.CS.prod
(mk_pos ("A", "Int | Bool")) (
cap
Tallying.CS.prod
(mk_neg ("Int | Bool","B"))
(mk_pos ("B","Int | Bool"))
)
);
[("`$A", "`$B")], mk_pos ("A","`$B");
[("`$B", "Empty")], mk_pos ("B","Empty");
[("`$A", "Int");("`$B", "Bool"); ("`$A", "Empty")],cap (mk_pos ("A", "Empty")) (mk_pos ("B", "Bool"));
[("`$A", "Int");("`$B", "Bool"); ("`$A", "Empty")],Tallying.CS.prod (mk_pos ("A", "Empty")) (mk_pos ("B", "Bool"));
]
let test_merge =
......@@ -121,10 +124,10 @@ let test_merge =
let n = List.fold_left (fun acc (s,t) ->
let s = parse_typ s in
let t = parse_typ t in
Tallying.CS.cap acc (Tallying.norm(diff s t))) Tallying.CS.S.empty l
Tallying.CS.prod acc (Tallying.norm(diff s t))) Tallying.CS.S.empty l
in
let result = Tallying.CS.S.fold (fun c acc ->
try cup (Tallying.merge c) acc with Tallying.UnSatConstr -> acc
try Tallying.CS.union (Tallying.merge c) acc with Tallying.UnSatConstr -> acc
) n Tallying.CS.S.empty
in
let elem s = List.sort m_compare (Tallying.CS.S.elements s) in
......
......@@ -2280,24 +2280,13 @@ module Tallying = struct
else Pervasives.compare b1 b2
end)
(* m1 is a subset of m2 if for all elements (alpha,s) of
* m1 there is a correspoding element (alpha,t) in m2 such that
* s <= t . In this case m2 is a more restrictive constraint set
* then m1 *)
let subtype m1 m2 =
let c = compare Descr.compare m1 m2 in
if c = 0 then true
else
for_all (fun k1 t1 ->
exists (fun k2 t2 -> k1 == k2 && subtype t1 t2) m2
) m1
let print ppf m =
print_lst (fun ppf -> fun ((b,`Var v),s) ->
if b then
Format.fprintf ppf "(`$%s >= %a)" v Print.print s
Format.fprintf ppf "(`$%s <= %a)" v Print.print s
else
Format.fprintf ppf "(%a >= `$%s)" Print.print s v
Format.fprintf ppf "(%a <= `$%s)" Print.print s v
) ppf (bindings m);
end
......@@ -2367,27 +2356,43 @@ module Tallying = struct
let sat = S.singleton M.empty
let unsat = S.empty
(* m1 is less general than m2 if for all elements (alpha,s) of
* m1 there is a correspoding element (alpha,t) in m2 such that
* s <= t . In this case m2 is a more restrictive constraint set
* then m1 *)
let lessgeneral m1 m2 acc =
let test m1 m2 = (* m1 is less general them m2 *)
M.for_all (fun k1 t1 ->
M.exists (fun k2 t2 -> (Var.equal k1 k2) && (subtype t1 t2)) m2
) m1
in
if M.is_empty m1 then S.add m2 acc
else if M.is_empty m2 then S.add m1 acc else
if (M.compare compare m1 m2) = 0 then S.add m1 acc
(* m1 is less general them m2 *)
else if test m1 m2 then S.add m2 acc
(* m2 is less general them m1 *)
else if test m2 m1 then S.add m1 acc
else S.add m1 (S.add m2 acc)
(* this is O(n^2) filter . Only more restritive constraints sets are kept *)
let cup x y =
let union x y =
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
S.fold (fun m1 acc ->
S.fold (fun m2 acc1 ->
lessgeneral m1 m2 acc1
) y acc
) x y
(* cartesian product of two sets of contraints sets where each
* resulting constraint set is than merged *)
let cap x y =
let prod x y =
match S.is_empty x,S.is_empty y with
|true,true -> S.empty
|false,true -> x
......@@ -2467,7 +2472,7 @@ module Tallying = struct
if DescrSet.mem t m then CS.sat else begin
let aux_base single norm_aux acc l =
List.fold_left (fun acc (pos,neg) ->
CS.cap acc (toplevel single norm_aux m (pos,neg))
CS.prod acc (toplevel single norm_aux m (pos,neg))
) acc l
in
let accu = CS.sat in
......@@ -2502,18 +2507,18 @@ module Tallying = struct
let con2 = norm (z2, mem) in
let con10 = aux z1 t2 rest in
let con20 = aux t1 z2 rest in
let con11 = CS.cup con1 con10 in
let con22 = CS.cup con2 con20 in
CS.cap con11 con22
let con11 = CS.union con1 con10 in
let con22 = CS.union con2 con20 in
CS.prod con11 con22
in
(* cap_product return the intersection of all (fst pos,snd pos) *)
let (t1,t2) = cap_product any any pos in
let con1 = norm (t1, mem) in
let con2 = norm (t2, mem) in
let con0 = aux t1 t2 neg in
CS.cup (CS.cup con1 con2) con0
CS.union (CS.union con1 con2) con0
in
List.fold_left (fun acc (p,n) -> CS.cap acc (norm_prod p n)) CS.sat (Pair.get t)
List.fold_left (fun acc (p,n) -> CS.prod acc (norm_prod p n)) CS.sat (Pair.get t)
and normrec (t,mem) =
let mem = DescrSet.add { empty with record = BoolRec.atom (`Atm t) } mem in
......@@ -2526,14 +2531,14 @@ module Tallying = struct
snd (Array.fold_left (fun (i,acc) t ->
let di = diff accus.(i) t in
let accus' = Array.copy accus in accus'.(i) <- di ;
(i+1,CS.cap acc (CS.cap (norm (di,mem)) (aux accus' [] right)))
(i+1,CS.prod acc (CS.prod (norm (di,mem)) (aux accus' [] right)))
) (0,CS.S.empty) field
)
in
let c = Array.fold_left (fun acc t -> CS.cap (norm (t,mem)) acc) CS.S.empty left in
CS.cap (aux left [] rights) c
let c = Array.fold_left (fun acc t -> CS.prod (norm (t,mem)) acc) CS.S.empty left in
CS.prod (aux left [] rights) c
in
List.fold_left (fun acc (_,p,n) -> CS.cap acc (norm_rec (p,n))) CS.S.empty (get_record t)
List.fold_left (fun acc (_,p,n) -> CS.prod acc (norm_rec (p,n))) CS.S.empty (get_record t)
(* arrow(p,{t1 -> t2}) = [t1] ^ arrow'(t1,any \\ t2,p)
* arrow'(t1,acc,{s1 -> s2} v p) =
......@@ -2551,7 +2556,7 @@ module Tallying = struct
let con1 = norm (descr t1, mem) in
let con2 = aux (descr t1) (diff any (descr t2)) pos in
let con0 = norm_arrow pos n in
CS.cup (CS.cup con1 con2) con0
CS.union (CS.union con1 con2) con0
and aux t1 acc = function
|[] -> CS.S.empty
|(s1,s2) :: p ->
......@@ -2561,11 +2566,11 @@ module Tallying = struct
let con2 = norm (acc1, mem) in
let con10 = aux t1s1 acc p in
let con20 = aux t1 acc1 p in
let con11 = CS.cup con1 con10 in
let con22 = CS.cup con2 con20 in
CS.cap con11 con22
let con11 = CS.union con1 con10 in
let con22 = CS.union con2 con20 in
CS.prod con11 con22
in
List.fold_left (fun acc (p,n) -> CS.cap acc (norm_arrow p n)) CS.sat (Pair.get t)
List.fold_left (fun acc (p,n) -> CS.prod acc (norm_arrow p n)) CS.sat (Pair.get t)
let norm t = norm (t,DescrSet.empty)
......@@ -2576,8 +2581,8 @@ module Tallying = struct
let x = if b then diff t s else diff s t in
if DescrSet.mem x mem then None
else
let c1 = CS.cap (CS.S.singleton m) (norm x) in
let c2 = CS.S.fold (fun m1 acc -> CS.cup acc (merge (m1,DescrSet.add x mem))) c1 CS.S.empty in
let c1 = CS.prod (CS.S.singleton m) (norm x) in
let c2 = CS.S.fold (fun m1 acc -> CS.union acc (merge (m1,DescrSet.add x mem))) c1 CS.S.empty in
Some c2
with Not_found -> None
in
......@@ -2585,7 +2590,7 @@ module Tallying = struct
CS.M.fold (fun (b,v) s acc ->
match aux (b,v) s m with
|None -> acc
|Some c -> CS.cup c acc
|Some c -> CS.union c acc
) m CS.S.empty
in
if CS.S.is_empty mm then CS.S.singleton m else mm
......@@ -2647,7 +2652,7 @@ module Tallying = struct
aux (CS.E.empty,CS.E.empty) e
let tallying l =
let n = List.fold_left (fun acc (s,t) -> try CS.cap acc (norm(diff s t)) with UnSatConstr -> acc) CS.S.empty l in
let n = List.fold_left (fun acc (s,t) -> try CS.prod acc (norm(diff s t)) with UnSatConstr -> acc) CS.S.empty l in
if CS.S.is_empty n then raise UnSatConstr else
let m = CS.S.fold (fun c acc -> try CS.ES.union (solve (merge c)) acc with UnSatConstr -> acc) n CS.ES.empty in
if CS.ES.is_empty m then raise UnSatConstr else
......@@ -2655,3 +2660,17 @@ module Tallying = struct
List.map (CS.E.bindings) (CS.ES.elements el)
end
let appl t1 t2 =
let rec aux card s t =
let gamma = var (Var.fresh ()) in
(* create t1,t2 by increasing the cardinality ... ??? *)
let t1 = s and t2 = t in
let l = [(t1,arrow (cons t2) (cons gamma))] in
try Tallying.tallying l
with Tallying.UnSatConstr ->
if card >= 10 then assert false
else aux (card+1) t1 t2
in
aux 0 t1 t2
......@@ -388,8 +388,8 @@ module Tallying : sig
val singleton : constr -> s
val sat : s
val unsat : s
val cup : s -> s -> s
val cap : s -> s -> s
val union : s -> s -> s
val prod : s -> s -> s
end
val norm : t -> CS.s
......
......@@ -4,6 +4,7 @@ type var = [ `Var of t ]
type 'a pairvar = [ `Atm of 'a | var ]
let compare (x : var) (y : var) = Pervasives.compare x y
let equal x y = Pervasives.compare x y = 0
let hash (v : var) = Hashtbl.hash v
module Make (X : Custom.T) = struct
......
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