Commit 3add7855 authored by Pietro Abate's avatar Pietro Abate
Browse files

Fix more printing bug

- Better function to update the list of top level variable
  associated to a type
parent c097776b
......@@ -182,32 +182,18 @@ module TLV = struct
f = Var.Set.union x.f y.f
}
let union x y = {
b = x.b && y.b;
s = Set.union x.s y.s ;
f = Var.Set.union x.f y.f ;
}
let inter x y = {
b = x.b && y.b;
s = Set.inter x.s y.s ;
f = Var.Set.inter x.f y.f ;
}
let diff x y = {
b = x.b && y.b;
s = Set.inter x.s (Set.fold (fun (v,p) acc -> Set.add (v,not p) acc) y.s Set.empty);
f = Var.Set.union x.f y.f;
}
(* 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) && (Set.cardinal x.s = 0)
let no_toplevel x = (Set.cardinal x.s = 0)
let has_toplevel x = Set.cardinal x.s > 0
let print sep ppf x = if x.b then Set.print sep ppf x.s
let print ppf x = if x.b then Set.print ";" ppf x.s
let dump ppf x =
Format.fprintf ppf "<b = %b ; f = {%a} ; s = {%a}>"
x.b Var.Set.dump x.f (Set.print ";") x.s
let mem v x = Set.mem v x.s
end
......@@ -270,7 +256,7 @@ struct
List.iter (fun f -> f ppf; Format.fprintf ppf " |")
let dump ppf d =
Format.fprintf ppf "<types atoms(%a) ints(%a) chars(%a) times(%a) arrow(%a) record(%a) xml(%a) abstract(%a) absent(%b)>"
Format.fprintf ppf "<types atoms(%a) ints(%a) chars(%a) times(%a) arrow(%a) record(%a) xml(%a) abstract(%a) absent(%b)>\n%a"
BoolAtoms.dump d.atoms
BoolIntervals.dump d.ints
BoolChars.dump d.chars
......@@ -280,6 +266,7 @@ struct
BoolPair.dump d.xml
Abstract.dump d.abstract
d.absent
TLV.dump d.toplvars
let empty = {
times = BoolPair.empty;
......@@ -466,6 +453,45 @@ let var a = {
let is_var t = TLV.is_single t.toplvars
let no_var t = TLV.no_variables t.toplvars
(* XXX this function could be potentially costly. There should be
* better way to take trace of top level variables in a type *)
let update_tlv x y t =
let open TLV in
let tlv t =
let aux get bdd : Set.t =
let l =
List.fold_left (fun acc (p,n) ->
let acc1 =
List.fold_left (fun acc -> function
|(`Var v) as x -> Set.union acc (Set.singleton (x,true))
|_ -> acc
) Set.empty p
in
let acc2 =
List.fold_left (fun acc -> function
|(`Var v) as x -> Set.union acc (Set.singleton (x,false))
|_ -> assert false
) acc1 n
in acc2::acc
) [] (get bdd)
in
match l with
|[] -> Set.empty
|[h] -> h
|h::l -> List.fold_left Set.inter h l
in
List.fold_left Set.inter
(aux BoolChars.get t.chars)
[(aux BoolIntervals.get t.ints);
(aux BoolAtoms.get t.atoms);
(aux BoolPair.get t.arrow);
(aux BoolPair.get t.xml);
(aux BoolRec.get t.record)]
in
let s = tlv t in
{ t with toplvars = { s = s ; f = Var.Set.union x.toplvars.f y.toplvars.f ; b = x.toplvars.b && x.toplvars.b } }
;;
let char c = { empty with chars = BoolChars.atom (`Atm c) }
let interval i = { empty with ints = BoolIntervals.atom (`Atm i) }
let abstract a = { empty with abstract = a }
......@@ -473,7 +499,7 @@ let abstract a = { empty with abstract = a }
let get_abstract t = t.abstract
let cup x y =
if x == y then x else {
if x == y then x else update_tlv x y {
times = BoolPair.cup x.times y.times;
xml = BoolPair.cup x.xml y.xml;
arrow = BoolPair.cup x.arrow y.arrow;
......@@ -483,11 +509,11 @@ let cup x y =
chars = BoolChars.cup x.chars y.chars;
abstract = Abstract.cup x.abstract y.abstract;
absent= x.absent || y.absent;
toplvars = TLV.union x.toplvars y.toplvars
toplvars = TLV.empty
}
let cap x y =
if x == y then x else {
if x == y then x else update_tlv x y {
ints = BoolIntervals.cap x.ints y.ints;
times = BoolPair.cap x.times y.times;
xml = BoolPair.cap x.xml y.xml;
......@@ -497,11 +523,11 @@ let cap x y =
chars = BoolChars.cap x.chars y.chars;
abstract = Abstract.cap x.abstract y.abstract;
absent= x.absent && y.absent;
toplvars = TLV.union x.toplvars y.toplvars
toplvars = TLV.empty
}
let diff x y =
if x == y then empty else {
if x == y then empty else update_tlv x y {
times = BoolPair.diff x.times y.times;
xml = BoolPair.diff x.xml y.xml;
arrow = BoolPair.diff x.arrow y.arrow;
......@@ -511,7 +537,7 @@ let diff x y =
chars = BoolChars.diff x.chars y.chars;
abstract = Abstract.diff x.abstract y.abstract;
absent= x.absent && not y.absent;
toplvars = TLV.diff x.toplvars y.toplvars
toplvars = TLV.empty
}
(* TODO: optimize disjoint check for boolean combinations *)
......@@ -1596,26 +1622,24 @@ struct
let add u = slot.def <- u :: slot.def in
let prepare_boolvar ?(displayvars=false) ?(displayatoms=true) get is_full print tlv bdd =
(* variables are printed if displayvars OR if x is not a toplevel variable *)
let prepare_boolvar displayvars displayatoms get is_full print tlv bdd =
List.iter (fun (p,n) ->
let l1 =
List.fold_left (fun acc -> function
|(`Var v) as x ->
begin match (displayvars, (TLV.mem (x,true) tlv)) with
|(true,true) |(_,false) -> (Atomic (fun ppf -> Var.print ppf x))::acc
|(_,_) -> acc
end
if displayvars || not(TLV.mem (x,true) tlv) then
(Atomic (fun ppf -> Var.print ppf x))::acc
else acc
|`Atm bdd -> if displayatoms then (print bdd) @ acc else acc
) [] p
in
let l2 =
List.fold_left (fun acc -> function
|(`Var v) as x ->
begin match (displayvars, (TLV.mem (x,false) tlv)) with
|(true,true) |(_,false) ->
(Atomic (fun ppf -> Format.fprintf ppf "~ %a" Var.print x))::acc
|(_,_) -> acc
end
if displayvars || not(TLV.mem (x,true) tlv) then
(Atomic (fun ppf -> Format.fprintf ppf "~ %a" Var.print x))::acc
else acc
|`Atm bdd -> assert false
) [] n
in
......@@ -1627,33 +1651,37 @@ struct
if (non_empty seq) then add (Regexp (decompile seq));
let displayatoms = TLV.no_toplevel not_seq.toplvars in
let displayvars = true in
let displayatoms = true in
let displayvars = TLV.has_toplevel not_seq.toplvars in
let bool = Atoms.cup (Atoms.atom (Atoms.V.mk_ascii "false")) (Atoms.atom (Atoms.V.mk_ascii "true")) in
(* base types *)
prepare_boolvar ~displayvars ~displayatoms BoolIntervals.get (Intervals.equal Intervals.full) (fun x ->
List.map (fun x -> (Atomic x)) (Intervals.print x)
prepare_boolvar displayvars displayatoms BoolIntervals.get (Intervals.equal Intervals.full) (fun bdd ->
List.map (fun x -> (Atomic x)) (Intervals.print bdd)
) not_seq.toplvars not_seq.ints;
prepare_boolvar ~displayatoms BoolChars.get (Chars.equal Chars.full) (fun x ->
match Chars.is_char x with
let displayvars = false in
prepare_boolvar displayvars displayatoms BoolChars.get (Chars.equal Chars.full) (fun bdd ->
match Chars.is_char bdd with
| Some c -> [(Char c)]
| None -> List.map (fun x -> (Atomic x)) (Chars.print x)
| None -> List.map (fun x -> (Atomic x)) (Chars.print bdd)
) not_seq.toplvars not_seq.chars;
prepare_boolvar ~displayatoms BoolAtoms.get (Atoms.equal Atoms.full) (fun x ->
List.map (fun x -> (Atomic x)) (Atoms.print x)
prepare_boolvar displayvars displayatoms BoolAtoms.get (Atoms.equal Atoms.full) (fun bdd ->
if Atoms.equal bool bdd then [Atomic (fun ppf -> Format.fprintf ppf "Bool")]
else List.map (fun x -> (Atomic x)) (Atoms.print bdd)
) not_seq.toplvars not_seq.atoms;
(* pairs *)
prepare_boolvar ~displayatoms BoolPair.get (Pair.equal Pair.full) (fun x ->
prepare_boolvar displayvars displayatoms BoolPair.get (Pair.equal Pair.full) (fun x ->
List.map (fun (t1,t2) ->
(Pair (prepare t1, prepare t2))
) (Product.partition any x)) not_seq.toplvars not_seq.times;
(* xml pairs *)
prepare_boolvar ~displayatoms BoolPair.get (Pair.equal Pair.full) (fun x ->
prepare_boolvar displayvars displayatoms BoolPair.get (Pair.equal Pair.full) (fun x ->
List.flatten (
List.map (fun (t1,t2) ->
try let n = DescrPairMap.find (t1,t2) !named_xml in [(Name n)]
......@@ -1671,7 +1699,7 @@ struct
)) not_seq.toplvars not_seq.xml;
(* arrows *)
prepare_boolvar ~displayatoms BoolPair.get (Pair.equal Pair.full) (fun x ->
prepare_boolvar displayvars displayatoms BoolPair.get (Pair.equal Pair.full) (fun x ->
List.map (fun (p,n) ->
let aux (t,s) = prepare (descr t), prepare (descr s) in
let p = List.map aux p and n = List.map aux n in
......@@ -2198,7 +2226,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 no_var t then ty t else
cup [
decompose_aux atom (BoolAtoms.get t.atoms);
decompose_aux interval (BoolIntervals.get t.ints);
......@@ -2215,7 +2243,9 @@ struct
DescrHash.replace memo_decompose t (Some s);
s
end
in decompose t
in
DescrHash.clear memo_decompose;
decompose t
let solve v = internalize (make_node v)
......@@ -2255,15 +2285,15 @@ struct
| _ -> var d
end else var d
in
(* if TLV.no_variables t.toplvars then t
else *) begin
if no_var t then t
else begin
let x = forward () in
define x (substitute_aux (decompose t) (subst x));
descr(solve x)
end
let substitute t (alpha,s) =
if TLV.no_variables t.toplvars then t
if no_var t then t
else begin
let subst s d = if Var.equal d alpha then s else var d in
let x = forward () in
......@@ -2273,10 +2303,13 @@ struct
let substitutefree t =
let h = Hashtbl.create 17 in
let idx = ref 0 in
let subst h d =
try Hashtbl.find h d
with Not_found -> begin
let x = var (Var.fresh ~variance:(Var.variance d) ()) in
let id = Printf.sprintf "_%s_%d" (Var.id d) !idx in
let x = var (Var.mk ~fresh:false ~variance:(Var.variance d) id) in
incr idx;
Hashtbl.add h d x ;
x
end
......@@ -2597,7 +2630,7 @@ module Tallying = struct
|true,false -> y
|false,false ->
S.fold (fun m1 acc ->
if M.is_empty m1 then S.union y acc else
(* if M.is_empty m1 then S.union y acc else *)
S.fold (fun m2 acc1 ->
(* if M.is_empty m1 then S.add m2 acc1 else *)
if M.is_empty m2 then S.add m1 acc1 else
......@@ -2615,7 +2648,7 @@ module Tallying = struct
if S.is_empty x || S.is_empty y then S.empty
else
S.fold (fun m1 acc ->
if M.is_empty m1 then S.union y acc else
(* if M.is_empty m1 then S.union y acc else *)
S.fold (fun m2 acc1 -> S.add (merge m1 m2) acc1) y acc
) x S.empty
......@@ -2688,14 +2721,19 @@ module Tallying = struct
(* norm generates a constraint set for the costraint t <= 0 *)
let rec norm (t,mem) =
if DescrSet.mem t mem then CS.sat else begin (* if we already evaluated it, it is sat *)
(* if we already evaluated it, it is sat *)
if DescrSet.mem t mem then CS.sat else begin
(* if there is only one variable then is it A <= 0 or 1 <= A *)
(*
if is_var t then
let (v,p) = TLV.max t.toplvars in
let s = if p then (Pos (v,empty)) else (Neg (any,v)) in
CS.singleton s
else
(* XXX if there is only one variable then is it A <= 0 or 1 <= A *)
if is_empty t then CS.sat else (* if it empty then it is sat *)
(* if there are no vars, and it is not empty then unsat else sat *)
if no_var t then if is_empty t then CS.sat else CS.unsat
else
*)
let mem = DescrSet.add t mem in
let aux single norm_aux acc l = big_prod (toplevel single norm_aux mem) acc l in
......@@ -2862,20 +2900,32 @@ module Tallying = struct
let merge m = merge (m,DescrHash.create 17)
(* Add constraints of the form { alpha = ( s v fresh ) ^ t } *)
let solve s =
(* Add constraints of the form { alpha = ( s v fresh ) ^ t } *)
let aux ((`Var v) as alpha) (s,t) acc =
(* we cannot solve twice the same variable *)
if CS.E.mem alpha acc then assert false else
let pre = Printf.sprintf "_fr_%s_" (Var.id alpha) in
let b = var (Var.fresh ~pre ~variance:(Var.variance alpha) ()) in
(* 0 <= alpha <= 1 --> alpha = fresh *)
if equal s empty && equal t any then
let b = var (Var.fresh ~pre:v.Var.id ~variance:(Var.variance alpha) ()) in
CS.E.add alpha b acc
(* s <= alpha <= 0 --> alpha = empty *)
else if equal t empty then CS.E.add alpha empty acc
(* 1 <= alpha <= t --> alpha = t *)
else if equal s any then CS.E.add alpha t acc
(* s <= alpha <= 1 --> alpha = ( s v fresh ) *)
else if equal t any then
CS.E.add alpha (cup s b) acc
(* 0 <= alpha <= t --> alpha = ( t ^ fresh ) *)
else if equal s empty then
CS.E.add alpha (cap b t) acc
else
let b = var (Var.fresh ~pre:v.Var.id ~variance:(Var.variance alpha) ()) in
(* s <= alpha <= t --> alpha = ( s v fresh ) ^ t *)
CS.E.add alpha (cap (cup s b) t) acc
in
let aux m =
let aux1 m =
let cache = Hashtbl.create (CS.M.cardinal m) in
CS.M.fold (fun (b,alpha) s acc ->
if Hashtbl.mem cache alpha then acc else begin
......@@ -2892,7 +2942,7 @@ module Tallying = struct
else aux alpha (t,any) acc1
end else
(* alpha = ( s v fresh) ^ t *)
if b then aux alpha (t,s) acc else aux alpha (s,t) acc
if b then aux alpha (t,s) acc else aux alpha (s,t) acc;
with Not_found ->
(* upper bond or lower bound is missing, we replace it
* with a constratint of the form empty <= alpha <= s | s <= alpha <= any *)
......@@ -2900,55 +2950,66 @@ module Tallying = struct
end
) m CS.E.empty
in
CS.S.fold (fun m acc -> CS.ES.add (aux m) acc) s CS.ES.empty
CS.S.fold (fun m acc -> CS.ES.add (aux1 m) acc) s CS.ES.empty
let unify e =
let rec aux sol e =
(* Format.printf "e = %a\n" CS.print_e e; *)
if CS.E.is_empty e then sol
else begin
let (alpha,t) = CS.E.min_binding e in
(* Format.printf "Unify -> %a = %a\n" Var.print alpha Print.print t; *)
let e1 = CS.E.remove alpha e in
(* Format.printf "e1 = %a\n" CS.print_e e1; *)
(* remove from E \ { (alpha,t) } every occurrences of alpha
* by mu X . (t{X/alpha}) with X fresh . X is a recursion variale *)
(* substituterec remove also all previously introduced fresh variables *)
let x = Positive.substituterec t alpha in
(* Format.printf "X = %a %a %a\n" Var.print alpha Print.print x dump t; *)
let es = CS.E.fold (fun beta s acc -> CS.E.add beta (Positive.substitute s (alpha,x)) acc) e1 CS.E.empty in
(* Format.printf "es = %a\n" CS.print_e es; *)
aux ((CS.E.add alpha x sol)) es
end
in
aux CS.E.empty e
(* Format.printf "Begin e = %a\n" CS.print_e e; *)
let r = aux CS.E.empty e in
(* Format.printf "r = %a\n" CS.print_e r; *)
r
exception Step1Fail
exception Step2Fail
let tallying l =
let n = List.fold_left (fun acc (s,t) -> CS.prod acc (norm(diff s t))) CS.sat l in
Format.printf "Norm : %a\n" CS.print 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
Format.printf "Union/Merge : %a \n" CS.ES.print 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
Format.printf "Unify : %a\n" CS.ES.print el;
List.map (CS.E.bindings) (CS.ES.elements el)
end
exception KeepGoing
let apply t1 t2 =
let apply s t =
DescrHash.clear Tallying.memo_norm;
let q = Queue.create () in
let gamma = var (Var.mk ~variance:`ContraVariant "gamma") in
let gamma = var (Var.mk ~variance:`Covariant "Gamma") 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))]
try Tallying.tallying [(acc1,arrow (cons acc2) (cons gamma))]
with
|Tallying.Step1Fail -> raise Tallying.UnSatConstr
|Tallying.Step2Fail -> begin
Queue.add (aux (i+1,lazy(cap acc1 (Positive.substitutefree t1))) (j,lazy(acc2)) t1 t2) q;
Queue.add (aux (i,lazy(acc1)) (j+1,lazy(cap acc2 (Positive.substitutefree t2))) t1 t2) q;
Queue.add (aux (i+1,lazy(cap acc1 (Positive.substitutefree t1))) (j,lazy(acc2)) t1 t2) q;
raise KeepGoing
end
in
Queue.add (aux (0,lazy(t1)) (1,lazy(Positive.substitutefree t2)) t1 t2) q;
Queue.add (aux (1,lazy(Positive.substitutefree t1)) (0,lazy(t2)) t1 t2) q;
Queue.add (aux (1,lazy(Positive.substitutefree s)) (0,lazy(t)) s t) q;
Queue.add (aux (0,lazy(s)) (1,lazy(Positive.substitutefree t)) s t) q;
let result = ref [] in
while (List.length !result) = 0 && not(Queue.is_empty q) do
try result := (Queue.pop q) ()
......
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