Commit 8a4bacb8 authored by Pietro Abate's avatar Pietro Abate
Browse files

Fix merge and norm functions. All tests ok

parent 5b739da7
......@@ -51,16 +51,16 @@ let mk_pp = function
|N(t,V alpha) -> Tallying.CS.singleton (Tallying.Neg (parse_typ t,Var.mk alpha))
let mk_prod l =
List.fold_left (fun acc2 c ->
Tallying.CS.prod (mk_pp c) acc2
List.fold_left (fun acc c ->
Tallying.CS.prod (mk_pp c) acc
) Tallying.CS.sat l
let mk_union l1 l2 =
Tallying.CS.union (mk_prod l1) (mk_prod l2)
let mk_s ll =
List.fold_left (fun acc1 l ->
Tallying.CS.union (mk_prod l) acc1
List.fold_left (fun acc l ->
Tallying.CS.union (mk_prod l) acc
) Tallying.CS.S.empty ll
let mk_union_res l1 l2 =
......@@ -130,7 +130,7 @@ let test_constraint_ops = [
]
let test_constraints =
"test tallying data structures" >:::
"constraints" >:::
List.map (fun (test,result,expected) ->
test >:: (fun _ ->
let elem s = (MSet.of_list (Tallying.CS.S.elements s)) in
......@@ -159,9 +159,11 @@ let norm_tests = [
"(Int -> Int) | (Bool -> Bool)", "(`$A -> `$B)", mk_s [
[P(V "A","Empty")];
(* All these are subsumed as less general then (A <= 0)
[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")]
*)
];
"(`$A -> `$B)", "(Int -> Int) | (Bool -> Bool)", mk_s [
......@@ -198,11 +200,15 @@ let norm_tests = [
];
*)
"Bool -> Bool","Int -> `$A", mk_s [];
"Bool -> Bool","Int -> `$A", Tallying.CS.unsat;
"Int", "Bool", Tallying.CS.unsat;
"Int -> Bool", "`$A", mk_s [[N("Int -> Bool",V "A")]];
"[] -> []","Int -> `$A",Tallying.CS.unsat;
"((`$A , Int) & (`$B , Bool))","(Int , (Int & Bool))",Tallying.CS.sat;
]
let test_norm =
"test tallying norm" >:::
"norm" >:::
List.map (fun (s,t,expected) ->
(Printf.sprintf " %s \\ %s" s t) >:: (fun _ ->
let s = parse_typ s in
......@@ -224,7 +230,7 @@ let merge_tests = [
"unsat 2", mk_s [[N("Bool",V "B"); N("`$B", V "A"); P(V "A", "Empty")]], Tallying.CS.unsat;
"quad", mk_s [[N("Bool | Int",V "B"); N("`$B",V "A"); P(V "A", "Int | Bool")]],
"quad", mk_s [[N("Bool",V "B");N("Int",V "B");N("`$B",V "A"); P(V "A", "Int | Bool")]],
mk_s [
[N("`$B", V "A");P(V "A","Int | Bool");N("Int | Bool", V "B"); P(V "B","Int | Bool")]
];
......@@ -243,11 +249,11 @@ let merge_tests = [
];;
let test_merge =
"test tallying merge" >:::
"merge" >:::
List.map (fun (test,s,expected) ->
test >:: (fun _ ->
let result =
try
try
Tallying.CS.S.fold (fun c acc ->
Tallying.CS.union (Tallying.merge c) acc
) s Tallying.CS.S.empty
......@@ -283,32 +289,34 @@ let tallying_tests = [
[(V "A", "(Int,Int)"); (V "B","Int")]
];
[("((`$A , Int) & (`$B , Bool))","(Int , (Int & Bool))")], [[]];
[("((`$A , Int) | (`$B , Bool))","(Int , (Int | Bool))")], mk_e [
[(V "A","Int");(V "B","Int")]
];
[("[] -> []","Int -> `$A")], [[]];
[("Bool -> Bool","Int -> `$A")], [[]];
[("[] -> []","Int -> `$A")], [];
[("Bool -> Bool","Int -> `$A")], [];
[("((`$A , Int) & (`$B , Bool))","(Int , (Int & Bool))")], [];
]
let test_tallying =
let print_test l =
String.concat ";" (List.map (fun (s,t) -> Printf.sprintf " %s \\ %s" s t) l)
in
"test tallying" >:::
"tallying" >:::
List.map (fun (l,expected) ->
(print_test l) >:: (fun _ ->
let l = List.map (fun (s,t) -> (parse_typ s,parse_typ t)) l in
let result = Tallying.tallying l in
let elem s = SubStSet.of_list (List.map (fun l -> ESet.of_list l) s) in
SubStSet.assert_equal (elem expected) (elem result)
try
let l = List.map (fun (s,t) -> (parse_typ s,parse_typ t)) l in
let result = Tallying.tallying l in
let elem s = SubStSet.of_list (List.map (fun l -> ESet.of_list l) s) in
SubStSet.assert_equal (elem expected) (elem result)
with Tallying.Step1Fail -> assert_equal expected []
)
) tallying_tests
;;
let all =
"all tests" >::: [
let suite =
"tests" >::: [
test_constraints;
test_norm;
test_merge;
......@@ -316,7 +324,7 @@ let all =
]
let main () =
OUnit.run_test_tt_main all
OUnit.run_test_tt_main suite
;;
main ()
......
......@@ -28,8 +28,6 @@ let test_variance =
) set_op_tests
;;
let set_op_tests = [
"Int & `$B", "`$B & Int";
"Int | `$B", "`$B | Int";
......
......@@ -521,7 +521,7 @@ let get_record r =
List.map line (Rec.get r)
(* substitute variables occurring in t accoding to the function subvar *)
let rec substfree_aux subvar t =
let rec substfree_aux subvar (t,mem) =
let module C ( X : BoolVar.S ) =
struct
let atom_aux ?noderec subvar_aux =
......@@ -546,8 +546,8 @@ let rec substfree_aux subvar t =
List.fold_left (fun acc (left,rigth) ->
let deep_subst f l =
List.fold_left (fun acc (t1,t2) ->
let d1 = cons (substfree_aux subvar (descr t1)) in
let d2 = cons (substfree_aux subvar (descr t2)) in
let d1 = cons (substfree_aux subvar ((descr t1),mem)) in
let d2 = cons (substfree_aux subvar ((descr t2),mem)) in
BoolPair.cap acc (f(BoolPair.atom(`Atm (Pair.atom (d1,d2)))))
) BoolPair.full l
in
......@@ -571,26 +571,32 @@ let rec substfree_aux subvar t =
|_ -> acc
) s Var.Set.empty
in
{
atoms = (let module M = C(BoolAtoms) in M.subst) subatoms t.atoms;
ints = (let module M = C(BoolIntervals) in M.subst) subints t.ints;
chars = (let module M = C(BoolChars) in M.subst) subchars t.chars;
times = (let module M = C(BoolPair) in M.subst) ~noderec:subpairs subtimes t.times;
xml = (let module M = C(BoolPair) in M.subst) ~noderec:subpairs subxml t.xml;
(* XXX record still not done . need to define ~f:subrecord *)
record= (let module M = C(BoolRec) in M.subst) subrecord t.record;
arrow = (let module M = C(BoolPair) in M.subst) ~noderec:subpairs subarrow t.arrow;
abstract = t.abstract;
absent= t.absent;
toplvars = { t.toplvars with s = tlv (t.toplvars.s) }
}
try DescrHash.find mem t
with Not_found ->
let tsub =
{
atoms = (let module M = C(BoolAtoms) in M.subst) subatoms t.atoms;
ints = (let module M = C(BoolIntervals) in M.subst) subints t.ints;
chars = (let module M = C(BoolChars) in M.subst) subchars t.chars;
times = (let module M = C(BoolPair) in M.subst) ~noderec:subpairs subtimes t.times;
xml = (let module M = C(BoolPair) in M.subst) ~noderec:subpairs subxml t.xml;
(* XXX record still not done . need to define ~f:subrecord *)
record= (let module M = C(BoolRec) in M.subst) subrecord t.record;
arrow = (let module M = C(BoolPair) in M.subst) ~noderec:subpairs subarrow t.arrow;
abstract = t.abstract;
absent= t.absent;
toplvars = { t.toplvars with s = tlv (t.toplvars.s) }
}
in
DescrHash.add mem t tsub;
tsub
(* substitute in t all occurrences of v by the type s *)
let subst t (v,s) =
let subvar (`Var v,s) (`Var z) =
if Var.equal (`Var v) (`Var z) then `Constr s else (`Var z)
in
substfree_aux (subvar (v,s)) t
substfree_aux (subvar (v,s)) (t,DescrHash.create 17)
(* substitute in t all variables with a free variables *)
(* using a Hashtbl here hides lots of in place modifications *)
......@@ -604,7 +610,7 @@ let substfree t =
v
end
in
substfree_aux (subvar (Hashtbl.create 17)) t
substfree_aux (subvar (Hashtbl.create 17)) (t,DescrHash.create 17)
(* substitute all variables with s *)
let substvariance t =
......@@ -615,7 +621,7 @@ let substvariance t =
|`ContraVariant -> `Constr empty
|_ -> `Var t
in
substfree_aux subvar t
substfree_aux subvar (t,DescrHash.create 17)
(* Subtyping algorithm *)
......@@ -2384,8 +2390,6 @@ let cond_partition univ qs =
module Tallying = struct
exception UnSatConstr
type constr =
|Pos of (Var.var * s) (** alpha <= t | alpha \in P *)
|Neg of (s * Var.var) (** t <= alpha | alpha \in N *)
......@@ -2527,16 +2531,15 @@ module Tallying = struct
) x S.empty
(* cartesian product of two sets of contraints sets where each
* resulting constraint set is than merged *)
* resulting constraint set is than merged . If one of the two
* sets is empty the product is empty *)
let prod x y =
match S.is_empty x,S.is_empty y with
|true,true -> S.empty
|false,true -> S.empty
|true,false -> S.empty
|false,false ->
S.fold (fun m1 acc ->
S.fold (fun m2 acc1 -> union (S.singleton (merge m1 m2)) acc1) y acc
S.fold (fun m2 acc1 -> S.add (merge m1 m2) acc1) y acc
) x S.empty
|_,_ -> S.empty
end
......@@ -2555,10 +2558,14 @@ module Tallying = struct
let id = (fun x -> x) in
let t = cap (aux id constr p) (aux neg constr n) in
(* XXX the abstract field could be messed up ... maybe *)
if b then (* t = bigdisj ... alpha \in P --> alpha <= neg t *)
{ (neg t) with abstract = Abstract.empty }
else (* t = bigdisj ... alpha \in N --> t <= alpha *)
{ t with abstract = Abstract.empty }
let res =
if b then (* t = bigdisj ... alpha \in P --> alpha <= neg t *)
{ (neg t) with abstract = Abstract.empty }
else (* t = bigdisj ... alpha \in N --> t <= alpha *)
{ t with abstract = Abstract.empty }
in
Format.printf "Generating contraint %a %a\n" Var.print (`Var v) Print.print res;
res
let single_atoms = single_aux atom
......@@ -2606,7 +2613,8 @@ module Tallying = struct
(* norm generates a constraint set for the costraint t <= 0 *)
let rec norm ( (t,m) : (s * DescrSet.t)) =
if DescrSet.mem t m || is_empty t then CS.sat else begin
if is_empty t then CS.sat else
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.prod acc (toplevel single norm_aux m (pos,neg))
......@@ -2628,15 +2636,16 @@ module Tallying = struct
* [t1] ^ [t2] ^ [t1 \ s1] ^ [t2 \ s2] ^
* [t1 \ s1 \ s1_1] ^ [t2 \ s2 \ s2_1 ] ^
* [t1 \ s1 \ s1_1 \ s1_2] ^ [t2 \ s2 \ s2_1 \ s2_2 ] ^ ...
* prod(p,n) = [t1] ^ [t2] ^ prod'(t1,t2,n)
* prod'(t1,t2,{s1,s2} v n) = [t1\s1] ^ prod'(t1\s1,t2,n) v
* [t2\s2] ^ prod'(t1,t2\s2,n)
*
* prod(p,n) = [t1] v [t2] v prod'(t1,t2,n)
* prod'(t1,t2,{s1,s2} v n) = ([t1\s1] v prod'(t1\s1,t2,n)) ^
* ([t2\s2] v prod'(t1,t2\s2,n))
* *)
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 t2 = function
|[] -> CS.S.empty
|[] -> CS.sat
|(s1,s2) :: rest ->
let z1 = diff t1 (descr s1) in
let z2 = diff t2 (descr s2) in
......@@ -2661,7 +2670,7 @@ module Tallying = struct
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
|[] -> CS.S.empty
|[] -> CS.sat
|(false,_) :: rest when oleft -> aux accus seen rest
|(b,field) :: rest ->
let right = seen @ rest in
......@@ -2669,18 +2678,24 @@ module Tallying = struct
let di = diff accus.(i) t in
let accus' = Array.copy accus in accus'.(i) <- di ;
(i+1,CS.prod acc (CS.prod (norm (di,mem)) (aux accus' [] right)))
) (0,CS.S.empty) field
) (0,CS.sat) field
)
in
let c = Array.fold_left (fun acc t -> CS.prod (norm (t,mem)) acc) CS.S.empty left in
let c = Array.fold_left (fun acc t -> CS.prod (norm (t,mem)) acc) CS.sat left in
CS.prod (aux left [] rights) c
in
List.fold_left (fun acc (_,p,n) -> CS.prod 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.sat (get_record t)
(* arrow(p,{t1 -> t2}) = [t1] ^ arrow'(t1,any \\ t2,p)
(* arrow(p,{t1 -> t2}) = [t1] v arrow'(t1,any \ t2,p)
* arrow'(t1,acc,{s1 -> s2} v p) =
([t1\s1] ^ arrow'(t1\s1,acc,p)) v
([acc ^ {s2} \ t2] ^ arrow'(t1,acc ^ {s2},p))
([t1\s1] v arrow'(t1\s1,acc,p)) ^
([acc ^ {s2}] v arrow'(t1,acc ^ {s2},p))
t1 -> t2 \ s1 -> s2 =
[t1] v (([t1\s1] v {[]}) ^ ([any\t2^s2] v {[]}))
Bool -> Bool \ Int -> A =
[Bool] v (([Bool\Int] v {[]}) ^ ([Any\Bool^A] v {[]})
P(Q v {a}) = {a} v P(Q) v {X v {a} | X \in P(Q) }
*)
......@@ -2688,14 +2703,14 @@ module Tallying = struct
let mem = DescrSet.add { empty with arrow = BoolPair.atom (`Atm t) } mem in
let rec norm_arrow pos neg =
match neg with
|[] -> CS.S.empty
|[] -> CS.unsat
|(t1,t2) :: n ->
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.union (CS.union con1 con2) con0
and aux t1 acc = function
|[] -> CS.S.empty
|[] -> CS.unsat
|(s1,s2) :: p ->
let t1s1 = diff t1 (descr s1) in
let acc1 = cap acc (descr s2) in
......@@ -2711,6 +2726,8 @@ module Tallying = struct
let norm t = norm (t,DescrSet.empty)
exception UnSatConstr
let rec merge (m,mem) =
let aux (b,v) s m =
try
......@@ -2718,14 +2735,14 @@ module Tallying = struct
let x = if b then diff t s else diff s t in
if DescrSet.mem x mem then None
else begin
let n = let r = norm x in if CS.S.is_empty r then raise UnSatConstr else r in
let n = let n = norm x in if CS.S.is_empty n then raise UnSatConstr else n in
let c1 = CS.prod (CS.S.singleton m) n 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
end
with Not_found -> None
in
let mm =
let mm =
CS.M.fold (fun (b,v) s acc ->
match aux (b,v) s m with
|None -> acc
......@@ -2734,7 +2751,6 @@ module Tallying = struct
in
if CS.S.is_empty mm then CS.S.singleton m else mm
(* returns a constraint set or UnSatConstr *)
let merge m = merge (m,DescrSet.empty)
let solve s =
......@@ -2786,7 +2802,7 @@ module Tallying = struct
(* remove from E \ { (alpha,t) } every occurrences of alpha
* by mu X . (t{X/alpha}) with X fresh . X is a recursion variale *)
(* XXX : substvariance remove all previously introduced fresh variables *)
let x = (* substvariance *) (Positive.substitute t alpha) in
let x = substvariance (Positive.substitute t alpha) in
let es = CS.E.fold (fun beta s acc -> CS.E.add beta (subst s (alpha,x)) acc) e1 CS.E.empty in
aux ((CS.E.add alpha x sol),(CS.E.add alpha x acc)) es
in
......
......@@ -358,6 +358,8 @@ module Tallying : sig
|Neg of (t * Var.var) (** t <= alpha | alpha \in N *)
exception UnSatConstr
exception Step1Fail
exception Step2Fail
module CS : sig
module M : sig
......
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