Skip to content

GitLab

Commit 3c1254ea authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Fix a bug where some variables appeared artificially as invariant, 

because they appeared both on negative and positive occurences in bdds
that are equivalent to the empty type.

For instance t = ('a | (Int\'a) | Int)

We use product normalization to clean up this.

Use the new debugging infrastructure to see what is going on during constraint solving.
parent 16d5e7eb
Hide whitespace changes
Inline Side-by-side
Showing with 80 additions and 20 deletions
types/types.ml
View file @ 3c1254ea
......@@ -1495,7 +1495,8 @@ end
module Iter =
struct
let any_node2 = any_node, any_node
let compute ~empty ~full ~cup ~cap ~diff ~var ~atom ~int ~char ~times ~xml ~arrow ~record ~abs ~opt t
let compute ?(normalize=false) ~empty ~full ~cup ~cap ~diff ~var ~atom ~int ~char ~times ~xml ~arrow ~record ~abs ~opt t
=
let var_or f =
function `Atm a -> f a
......@@ -1522,6 +1523,15 @@ module Iter =
| `Xml -> any_xml, xml
| `Arrow -> any_arrow, arrow
in
if normalize && Pervasives.(kind <> `Arrow) then
let rects =
match kind with
`Times -> Product.normal ~kind:`Normal { Descr.empty with times = BoolPair.atom (`Atm p) }
| `Xml -> Product.normal ~kind:`XML { Descr.empty with xml = BoolPair.atom (`Atm p) }
| _ -> assert false
in
List.fold_left (fun acc (d1, d2) -> cup acc (mk (cons d1, cons d2))) empty rects
else
Pair.compute ~empty ~full:any ~cup ~cap ~diff ~atom:mk p
in
List.fold_left (fun acc e -> cup acc e)
......@@ -1580,7 +1590,7 @@ module Variable =
Not_found ->
DescrHash.add memo t empty3;
let res =
Iter.compute
Iter.compute ~normalize:true
~empty:no3
~full:empty3
~cup:union3
......@@ -3009,7 +3019,10 @@ struct
let clean_type delta t =
if no_var t then t else
let _,pos, neg, all = Variable.collect_vars t in
let _tlv,pos, neg, all = Variable.collect_vars t in
DEBUG clean_type (Format.eprintf " - for type %a pos: %a, neg: %a, all: %a, tlv: %a@\n"
Print.pp_type t
Var.Set.pp pos Var.Set.pp neg Var.Set.pp all Var.Set.pp _tlv);
let vars = Var.Set.diff all delta in
if Var.Set.is_empty vars then t else
let idx = ref 0 in
......@@ -3037,6 +3050,12 @@ struct
in
app_subst t subst
let clean_type delta t =
let res = clean_type delta t in
DEBUG clean_type (Format.eprintf "@[ Calling clean_type(%a, %a) = %a@]@\n%!"
Var.Set.pp delta Print.pp_type t Print.pp_type res);
res
let hide_vars t =
if no_var t then t else
......@@ -3367,45 +3386,67 @@ module Tallying = struct
let memo_norm = NormMemoHash.create 17
let rec norm (t,delta,mem) =
DEBUG normrec ( Format.eprintf
" @[Entering norm rec(%a):@\n" Print.pp_type t);
let res =
try
(* If we find it in the global hashtable, we are finished *)
NormMemoHash.find memo_norm (t, delta)
let res = NormMemoHash.find memo_norm (t, delta) in
DEBUG normrec (Format.eprintf
"@[ - Result found in global table @]@\n");
res
with
Not_found ->
try
let finished, cst = NormMemoHash.find mem (t, delta) in
DEBUG normrec (Format.eprintf
"@[ - Result found in local table, finished = %b @]@\n" finished);
if finished then cst else CS.sat
with
Not_found ->
begin
let res =
(* base cases *)
if is_empty t then CS.sat (* empty type is sat *)
else if no_var t then CS.unsat (* if the type has no variable and is not empty, unsat *)
else if is_var t then (* a single top_level variable *)
begin
(* if there is only one variable then is it A <= 0 or 1 <= A *)
let (v,p) = extract_variable t in
if Var.Set.mem delta v then CS.unsat (* if it is monomorphic, unsat *)
else
(* otherwise, create a single constraint according to its polarity *)
let s = if p then (Pos (v,empty)) else (Neg (any,v)) in
CS.singleton s
if is_empty t then begin
DEBUG normrec (Format.eprintf "@[ - Empty type case @]@\n");
CS.sat
end else if no_var t then begin
DEBUG normrec (Format.eprintf "@[ - No var case @]@\n");
CS.unsat
end else if is_var t then begin
let (v,p) = extract_variable t in
if Var.Set.mem delta v then begin
DEBUG normrec (Format.eprintf "@[ - Monomorphic var case @]@\n");
CS.unsat (* if it is monomorphic, unsat *)
end else begin
DEBUG normrec (Format.eprintf "@[ - Polymorphic var case @]@\n");
(* otherwise, create a single constraint according to its polarity *)
let s = if p then (Pos (v,empty)) else (Neg (any,v)) in
CS.singleton s
end
else begin (* type is not empty and is not a variable *)
end else begin (* type is not empty and is not a variable *)
DEBUG normrec (Format.eprintf "@[ - Inductive case:@\n");
let mem = NormMemoHash.add mem (t,delta) (false, CS.sat); mem in
let aux single norm_aux acc l =
big_prod delta (toplevel delta single norm_aux mem) acc l
in
let acc = aux single_atoms normatoms CS.sat (BoolAtoms.get t.atoms) in
DEBUG normrec (Format.eprintf "@[ - After Atoms constraints: %a @]@\n" CS.pp_s acc);
let acc = aux single_chars normchars acc (BoolChars.get t.chars) in
DEBUG normrec (Format.eprintf "@[ - After Chars constraints: %a @]@\n" CS.pp_s acc);
let acc = aux single_ints normints acc (BoolIntervals.get t.ints) in
DEBUG normrec (Format.eprintf "@[ - After Ints constraints: %a @]@\n" CS.pp_s acc);
let acc = aux single_times normpair acc (BoolPair.get t.times) in
DEBUG normrec (Format.eprintf "@[ - After Times constraints: %a @]@\n" CS.pp_s acc);
let acc = aux single_xml normpair acc (BoolPair.get t.xml) in
DEBUG normrec (Format.eprintf "@[ - After Xml constraints: %a @]@\n" CS.pp_s acc);
let acc = aux single_arrow normarrow acc (BoolPair.get t.arrow) in
DEBUG normrec (Format.eprintf "@[ - After Arrow constraints: %a @]@\n" CS.pp_s acc);
let acc = aux single_abstract normabstract acc (BoolAbstracts.get t.abstract) in
DEBUG normrec (Format.eprintf "@[ - After Abstract constraints: %a @]@\n" CS.pp_s acc);
(* XXX normrec is not tested at all !!! *)
let acc = aux single_record normrec acc (BoolRec.get t.record) in
DEBUG normrec (Format.eprintf "@[ - After Record constraints: %a @]@\n" CS.pp_s acc);
let acc = (* Simplify the constraints on that type *)
CS.S.filter
(fun m -> CS.M.for_all (fun v (s, t) -> not (Var.Set.mem delta v) ||
......@@ -3413,11 +3454,20 @@ module Tallying = struct
) m)
acc
in
acc
DEBUG normrec (Format.eprintf "@[ - After Filtering constraints: %a @]@\n" CS.pp_s acc);
DEBUG normrec (Format.eprintf "@]@\n");
acc
end
in
NormMemoHash.replace mem (t, delta) (true,res); res
end
in
DEBUG normrec (Format.eprintf
"Leaving norm rec(%a) = %a@]@\n%!"
Print.pp_type t
CS.pp_s res
);
res
(* (t1,t2) = intersection of all (fst pos,snd pos) \in P
* (s1,s2) \in N
......@@ -3750,6 +3800,12 @@ exception FoundApply of t * int * int * Tallying.CS.sl
s @@ sigma_i < t @@ sigma_j for all i \in I, j \in J *)
let apply_raw delta s t =
DEBUG apply_raw (Format.eprintf " @[Entering apply_raw (delta:@[%a@], @[%a@], @[%a@])@\n%!"
Var.Set.pp delta
Print.pp_type s
Print.pp_type t
);
Tallying.NormMemoHash.clear Tallying.memo_norm;
let s = Substitution.kind delta Var.function_kind s in
let t = Substitution.kind delta Var.argument_kind t in
......@@ -3793,9 +3849,13 @@ let apply_raw delta s t =
tallying i i;
loop (i+1)
with FoundApply (res, i, j, sl) ->
(* we remove gamma from the substitution list as it is only used
here by the algorithm *)
(* let sl = (Tallying.filter (fun v -> not(Var.equal v vgamma)) sl) in *)
DEBUG apply_raw (Format.eprintf " Leaving apply_raw (delta:@[%a@], @[%a@], @[%a@]) = @[%a@], @[%a@] @]@\n%!"
Var.Set.pp delta
Print.pp_type s
Print.pp_type t
Print.pp_type res
Tallying.CS.pp_sl sl
);
(sl, get ai i, get aj j, res)
in
loop 0
......
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