Commit 796f7ee6 authored by Pietro Abate's avatar Pietro Abate
Browse files

More bug fix

- fix one more problem with internalize
- fix variance/contravariance problem in substituterec
- cleanup
parent 031befa2
......@@ -86,7 +86,7 @@ let mk_union_res l1 l2 =
(* check invariants on the constraints sets *)
let test_constraint_ops = [
let test_constraint_ops () = [
"prod pos",mk_prod [P(V "A","Int");P(V "A","Bool")], mk_pp (P(V "A","Int & Bool"));
......@@ -136,12 +136,12 @@ let test_constraints =
let elem s = (MSet.of_list (Tallying.CS.S.elements s)) in
MSet.assert_equal (elem expected) (elem result)
)
) test_constraint_ops
) (test_constraint_ops ())
;;
(* ^ => & -- v => | *)
let norm_tests = [
let norm_tests () = [
"(`$A -> Bool)", "(`$B -> `$B)", mk_s [
[P(V "B","Empty")];
[N("`$B",V "A");N("Bool",V "B")]
......@@ -205,6 +205,11 @@ let norm_tests = [
"Int", "Bool", Tallying.CS.unsat;
"Int", "Empty", Tallying.CS.unsat;
"[] -> []","Int -> `$A",Tallying.CS.unsat;
"((`$A , Int) | (`$B , Bool))","(Int , (Int | Bool))", mk_s [
[P(V "A","Int");P(V "B","Int")]
];
]
let test_norm =
......@@ -217,10 +222,10 @@ let test_norm =
let elem s = MSet.of_list (Tallying.CS.S.elements s) in
MSet.assert_equal (elem expected) (elem result)
)
) norm_tests
) (norm_tests ())
;;
let merge_tests = [
let merge_tests () = [
"empty empty", mk_s [[P(V "A", "Empty");P(V "B", "Empty")]],
mk_s [
[P(V "A","Empty");P(V "B","Empty")]
......@@ -262,7 +267,7 @@ let test_merge =
let elem s = MSet.of_list (Tallying.CS.S.elements s) in
MSet.assert_equal (elem expected) (elem result)
)
) merge_tests
) (merge_tests ())
;;
let mk_e ll =
......@@ -271,6 +276,12 @@ let mk_e ll =
) ll
let tallying_tests = [
(*
[("((Int | Bool) -> Int)", "(`$A -> `$B)")], mk_e [
[(V "A","Empty")];
[(V "A","Int | Bool");(V "B","Int")]
];
[("((Int | Bool) -> Int)", "(`$A -> `$B)"); ("(`$A -> Bool)","(`$B -> `$B)")], mk_e [
[(V "A","Int | Bool");(V "B","Int | Bool")];
[(V "A","Empty");(V "B","Empty")]
......@@ -288,14 +299,16 @@ let tallying_tests = [
[("((Int,Int) , (Int | Bool))","(`$A,Int) | ((`$B,Int),Bool)")], mk_e [
[(V "A", "(Int,Int)"); (V "B","Int")]
];
*)
[("((`$A , Int) | (`$B , Bool))","(Int , (Int | Bool))")], mk_e [
[(V "A","Int");(V "B","Int")]
];
(*
[("[] -> []","Int -> `$A")], [];
[("Bool -> Bool","Int -> `$A")], [];
[("((`$A , Int) & (`$B , Bool))","(Int , (Int & Bool))")], [];
[("((`$A , Int) & (`$B , Bool))","(Int , (Int & Bool))")], [[]];
*)
]
let test_tallying =
......
......@@ -155,7 +155,7 @@ module TLV = struct
* b : true if the type contains only variables *)
type t = { s : Set.t ; f : Var.Set.t ; b : bool }
let empty = { s = Set.empty ; f = Var.Set.empty ; b = true }
let empty = { s = Set.empty ; f = Var.Set.empty ; b = false }
let any = { s = Set.empty ; f = Var.Set.empty ; b = false }
let singleton (v,p) = { s = Set.singleton (v,p); f = Var.Set.singleton v; b = true }
......@@ -189,7 +189,7 @@ module TLV = struct
(* 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 no_variables x = (x.b == false) && (Var.Set.cardinal x.f = 0)
let no_variables x = (x.b == false) && (Var.Set.cardinal x.f = 0) && (Set.cardinal x.s = 0)
end
......@@ -411,9 +411,15 @@ let non_constructed_or_absent =
{ non_constructed with absent = true }
(* Descr.t type constructors *)
let times x y = { empty with times = BoolPair.atom (`Atm (Pair.atom (x,y))); toplvars = TLV.pair (descr x).toplvars (descr y).toplvars }
let xml x y = { empty with xml = BoolPair.atom (`Atm (Pair.atom (x,y))); toplvars = TLV.pair (descr x).toplvars (descr y).toplvars }
let arrow x y = { empty with arrow = BoolPair.atom (`Atm (Pair.atom (x,y))); toplvars = TLV.pair (descr x).toplvars (descr y).toplvars }
let times x y = { empty with
times = BoolPair.atom (`Atm (Pair.atom (x,y)));
toplvars = TLV.pair (descr x).toplvars (descr y).toplvars }
let xml x y = { empty with
xml = BoolPair.atom (`Atm (Pair.atom (x,y)));
toplvars = TLV.pair (descr x).toplvars (descr y).toplvars }
let arrow x y = { empty with
arrow = BoolPair.atom (`Atm (Pair.atom (x,y)));
toplvars = TLV.pair (descr x).toplvars (descr y).toplvars }
(* XXX toplevel variables are not properly set for records *)
let record label t =
......@@ -2087,7 +2093,7 @@ struct
let aux polarity constr l =
cap (
List.map ( function
|`Var a -> (polarity(var (`Var a)))
|`Var v -> (polarity(var (`Var v)))
|`Atm bdd ->
match noderec with
|None -> (polarity(ty (constr bdd)))
......@@ -2122,7 +2128,7 @@ struct
with Not_found -> begin
DescrHash.add memo_decompose t None;
let s =
if TLV.no_variables t.toplvars then ty t else
(* if TLV.no_variables t.toplvars then ty t else *)
cup [
decompose_aux atom (BoolAtoms.get t.atoms);
decompose_aux interval (BoolIntervals.get t.ints);
......@@ -2160,26 +2166,26 @@ struct
with Not_found -> begin
Hashtbl.add memo v.def None;
let r = aux v subst in
Hashtbl.add memo v.def (Some r);
Hashtbl.replace memo v.def (Some r);
r
end
(* returns a recursive type where all occurrences of alpha n t
* are substituted with a recursive variable X and all fresh variables
* in covariant position are substituted with any and contravariant
* position with empty *)
* in covariant position are substituted with empty and contravariant
* position with any *)
let substituterec t alpha =
let subst x d =
if Var.equal d alpha then x else
if Var.is_fresh d then
if Var.is_fresh d then begin
match Var.variance d with
| `Covariant -> ty any
| `ContraVariant -> ty empty
| `Covariant -> ty empty
| `ContraVariant -> ty any
| _ -> var d
else var d
end else var d
in
if TLV.no_variables t.toplvars then t
else begin
(* if TLV.no_variables t.toplvars then t
else *) begin
let x = forward () in
define x (substitute_aux (decompose t) (subst x));
descr(solve x)
......@@ -2566,14 +2572,10 @@ 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 *)
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
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 single_atoms = single_aux atom
......@@ -2798,16 +2800,16 @@ module Tallying = struct
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
let aux ((`Var v) as alpha) (s,t) acc =
if CS.E.mem alpha acc then assert false else
if equal s empty && equal t any then
let b = var (Var.fresh ~variance:(Var.variance v) ()) in
CS.E.add v b acc
else if equal t empty then CS.E.add v empty acc
else if equal s any then CS.E.add v t acc
let b = var (Var.fresh ~pre:v.Var.id ~variance:(Var.variance alpha) ()) in
CS.E.add alpha b acc
else if equal t empty then CS.E.add alpha empty acc
else if equal s any then CS.E.add alpha t acc
else
let b = var (Var.fresh ~variance:(Var.variance v) ()) in
CS.E.add v (cap (cup s b) t) acc
let b = var (Var.fresh ~pre:v.Var.id ~variance:(Var.variance alpha) ()) in
CS.E.add alpha (cap (cup s b) t) acc
in
let aux m =
let cache = Hashtbl.create (CS.M.cardinal m) in
......@@ -2840,7 +2842,7 @@ module Tallying = struct
let rec aux sol e =
if CS.E.is_empty e then sol
else begin
let ((`Var v as alpha),t) = CS.E.min_binding e in
let (alpha,t) = CS.E.min_binding e in
let e1 = CS.E.remove alpha e in
(* remove from E \ { (alpha,t) } every occurrences of alpha
* by mu X . (t{X/alpha}) with X fresh . X is a recursion variale *)
......@@ -2857,13 +2859,10 @@ module Tallying = struct
let tallying l =
let n = List.fold_left (fun acc (s,t) -> CS.prod acc (norm(diff s t))) CS.sat l in
Printf.printf "norm %d!\n%!" (CS.S.cardinal n);
if CS.S.is_empty n then raise Step1Fail 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
Printf.printf "solve merge %d !\n%!" (CS.ES.cardinal m);
if CS.ES.is_empty m then raise Step2Fail else
let el = CS.ES.fold (fun e acc -> CS.ES.add (unify e) acc) m CS.ES.empty in
Printf.printf "unify !\n%!";
List.map (CS.E.bindings) (CS.ES.elements el)
end
......@@ -2872,7 +2871,7 @@ exception KeepGoing
let apply t1 t2 =
DescrHash.clear Tallying.memo_norm;
let q = Queue.create () in
let gamma = var (Var.fresh ~variance:`ContraVariant ()) in
let gamma = var (Var.fresh ~pre:"gamma" ~variance:`ContraVariant ()) in
let rec aux (i,acc1) (j,acc2) t1 t2 () =
let acc1 = Lazy.force acc1 and acc2 = Lazy.force acc2 in
try Tallying.tallying [(acc1,arrow (cons acc2) (cons gamma))]
......
......@@ -60,17 +60,17 @@ module Make (X : Custom.T) = struct
let dump ppf = function
|`Atm x -> X.dump ppf x
|`Var x -> print ppf (`Var x)
|`Var x -> dump ppf (`Var x)
end
let mk ?fresh ?variance id =
`Var (make_id ?fresh ?variance id)
let fresh : ?variance:[ `None| `Both | `ContraVariant | `Covariant ] -> unit -> [> var ] =
let fresh : ?pre: string -> ?variance:[ `None| `Both | `ContraVariant | `Covariant ] -> unit -> [> var ] =
let counter = ref 0 in
fun ?variance -> fun _ ->
let id = (Printf.sprintf "_fresh_%d" !counter) in
fun ?(pre="_fresh_") -> fun ?variance -> fun _ ->
let id = (Printf.sprintf "%s%d" pre !counter) in
let v = mk ~fresh:true ?variance id in
incr counter;
v
......
......@@ -129,7 +129,7 @@ let deferr s = raise (Patterns.Error s)
(* x and y have been internalized; if they were equivalent,
they would be equal *)
else match x.desc,y.desc with
| IType (tx,_), IType (ty,_) when (Types.equal tx ty) -> if (Types.no_var tx) then () else link x y
| IType (tx,_), IType (ty,_) when (Types.equal tx ty) -> if Types.no_var tx then link x y
| IOr (x1,x2,_), IOr (y1,y2,_)
| IAnd (x1,x2,_), IAnd (y1,y2,_)
| IDiff (x1,x2,_), IDiff (y1,y2,_)
......
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