Commit 40740c72 authored by Kim Nguyễn's avatar Kim Nguyễn

Improve the type pretty printer, as follows :

for each component (int, atoms, pairs...) we optimize the case where the component is like

  T1&'a | T2 | T3&'a

we split it into
- T2
- T1 &'a | T3 &'a
we retrieve { 'a } as the set of top level vars in the second type
we compute T2 &'a | T1 &'a | T3 &'a
then remove 'a from that type and return finally :

T2 | ('a & (T1 | T2 | T3))

We special case if (T1 | T2 | T3) is top, then we just display
T2 | 'a
parent ae786716
......@@ -4,7 +4,7 @@ let (=) : int -> int -> bool = (=)
(* this is the the of the Constructor container *)
module type E = sig
type elem
type elem
include Custom.T
val empty : t
......@@ -26,10 +26,10 @@ module type S = sig
val leafconj: t -> s
val get: t -> (elem list * elem list) list
val build : (elem list * elem list) list -> t
val empty : t
val full : t
(* same as full, but we keep it for the moment to avoid chaging
(* same as full, but we keep it for the moment to avoid chaging
* the code everywhere *)
val any : t
val cup : t -> t -> t
......@@ -44,7 +44,7 @@ module type S = sig
val iter: (elem -> unit) -> t -> unit
val compute: empty:'b -> full:'b -> cup:('b -> 'b -> 'b)
val compute: empty:'b -> full:'b -> cup:('b -> 'b -> 'b)
-> cap:('b -> 'b -> 'b) -> diff:('b -> 'b -> 'b) ->
atom:(elem -> 'b) -> t -> 'b
......@@ -55,7 +55,7 @@ module type S = sig
val print : ?f:(Format.formatter -> elem -> unit) -> t -> (Format.formatter -> unit) list
(*
val extractvars : t -> [> `Var of Var.t ] bdd * t
val extractvars : t -> [> `Var of Var.t ] bdd * t
*)
end
......@@ -64,7 +64,7 @@ module type MAKE = functor (T : E) -> S with type s = T.t
(* ternary BDD
* where the nodes are Atm of X.t | Var of String.t
* Variables are always before Values
* All the leaves are then base types
* All the leaves are then base types
*
* we add a third case when two leaves of the bdd are of the same
* kind, that's it Val of t1 , Val of t2
......@@ -74,7 +74,7 @@ module type MAKE = functor (T : E) -> S with type s = T.t
* Products can be merged for intersections
* Arrows can be never merged
*
* extract_var : copy the orginal tree and on one copy put to zero all
* extract_var : copy the orginal tree and on one copy put to zero all
* leaves that have an Atm on the other all leaves that have a Var
*
* *)
......@@ -110,13 +110,13 @@ module Make (T : E) : S with type s = T.t = struct
the minimum of the two when egality ... *)
let rec compare a b =
if (a == b) then 0
if (a == b) then 0
else match (a,b) with
| `Split (h1,x1, p1,i1,n1), `Split (h2,x2, p2,i2,n2) ->
if h1 < h2 then -1 else if h1 > h2 then 1
if h1 < h2 then -1 else if h1 > h2 then 1
else let c = X.compare x1 x2 in if c <> 0 then c
else let c = compare p1 p2 in if c <> 0 then c
else let c = compare i1 i2 in if c <> 0 then c
else let c = compare i1 i2 in if c <> 0 then c
else compare n1 n2
| `True,_ -> -1
| _, `True -> 1
......@@ -128,7 +128,7 @@ module Make (T : E) : S with type s = T.t = struct
| `False -> 0
| `Split(h,_,_,_,_) -> h
let compute_hash x p i n =
let compute_hash x p i n =
(X.hash x) + 17 * (hash p) + 257 * (hash i) + 16637 * (hash n)
let rec check = function
......@@ -146,11 +146,11 @@ module Make (T : E) : S with type s = T.t = struct
`Split (h, x,`True,`False,`False)
let vars v =
let compute_hash x p i n =
let compute_hash x p i n =
(Var.hash x) + 17 * (hash p) + 257 * (hash i) + 16637 * (hash n)
in
let a = atom (`Atm T.full) in
let h = compute_hash v a `False `False in
let a = atom (`Atm T.full) in
let h = compute_hash v a `False `False in
( `Split (h,v,a,`False,`False) :> t )
let rec iter f = function
......@@ -160,8 +160,8 @@ module Make (T : E) : S with type s = T.t = struct
let rec dump ppf = function
| `True -> Format.fprintf ppf "+"
| `False -> Format.fprintf ppf "-"
| `Split (_,x, p,i,n) ->
Format.fprintf ppf "%a(@[%a,%a,%a@])"
| `Split (_,x, p,i,n) ->
Format.fprintf ppf "%a(@[%a,%a,%a@])"
X.dump x (*X.hash x*) dump p dump i dump n
let rec print f ppf = function
......@@ -170,15 +170,15 @@ module Make (T : E) : S with type s = T.t = struct
| `Split (_, x, p,i, n) ->
let flag = ref false in
let b () = if !flag then Format.fprintf ppf " | " else flag := true in
(match p with
(match p with
| `True -> b(); Format.fprintf ppf "%a" f x
| `False -> ()
| _ -> b (); Format.fprintf ppf "%a & @[(%a)@]" f x (print f) p );
(match i with
(match i with
| `True -> assert false;
| `False -> ()
| _ -> b(); print f ppf i);
(match n with
(match n with
| `True -> b (); Format.fprintf ppf "@[~%a@]" f x
| `False -> ()
| _ -> b (); Format.fprintf ppf "@[~%a@] & @[(%a)@]" f x (print f) n)
......@@ -203,7 +203,7 @@ module Make (T : E) : S with type s = T.t = struct
accu
in aux [] [] [] x
let leafconj x =
let leafconj x =
let rec aux accu = function
| `True -> accu
| `False -> accu
......@@ -228,7 +228,7 @@ module Make (T : E) : S with type s = T.t = struct
cup (cup p i) n
in
aux b
(* Invariant: correct hash value *)
let split0 x pos ign neg =
......@@ -258,12 +258,12 @@ module Make (T : E) : S with type s = T.t = struct
let rec split x p i n =
if X.equal (`Atm T.empty) x then `False
(* 0?p:i:n -> 0 *)
else if i == `True then `True
else if i == `True then `True
(* x?p:1:n -> 1 *)
else if equal p n then p ++ i
else let p = simplify p [i] and n = simplify n [i] in
(* x?p:i:n when p = n -> bdd of (p ++ i) *)
if equal p n then p ++ i
if equal p n then p ++ i
else split0 x p i n
(* simplify t l -> bdd of ( t // l ) *)
......@@ -277,17 +277,17 @@ module Make (T : E) : S with type s = T.t = struct
if (has_true l) || (has_same a l) then `False
else s_aux2 a x p i n [] [] [] l
and s_aux2 a x p i n ap ai an = function
| [] ->
let p = simplify p ap
| [] ->
let p = simplify p ap
and n = simplify n an
and i = simplify i ai in
if equal p n then p ++ i else split0 x p i n
| b :: l -> s_aux3 a x p i n ap ai an l b
| b :: l -> s_aux3 a x p i n ap ai an l b
and s_aux3 a x p i n ap ai an l = function
| `False -> s_aux2 a x p i n ap ai an l
| `True -> assert false
| `Split (_,x2,p2,i2,n2) as b ->
if equal a b then `False
if equal a b then `False
else let c = X.compare x2 x in
if c < 0 then s_aux3 a x p i n ap ai an l i2
else if c > 0 then s_aux2 a x p i n (b :: ap) (b :: ai) (b :: an) l
......@@ -307,7 +307,7 @@ module Make (T : E) : S with type s = T.t = struct
| `Split (_,`Atm x1, `True,`False,`False), `Split (_,`Atm x2, `False,`False,`True)
| `Split (_,`Atm x1, `False,`False,`True), `Split (_,`Atm x2, `True,`False,`False) ->
assert false
| `Split (_,x1, p1,i1,n1), `Split (_,x2, p2,i2,n2) ->
let c = X.compare x1 x2 in
if c = 0 then split x1 (p1 ++ p2) (i1 ++ i2) (n1 ++ n2)
......@@ -337,10 +337,10 @@ module Make (T : E) : S with type s = T.t = struct
| `Split (_,x1, p1,i1,n1), `Split (_,x2, p2,i2,n2) ->
let c = X.compare x1 x2 in
if c = 0 then
split x1
split x1
(p1 ** (p2 ++ i2) ++ (p2 ** i1))
(i1 ** i2)
(n1 ** (n2 ++ i2) ++ (n2 ** i1))
(n1 ** (n2 ++ i2) ++ (n2 ** i1))
else if c < 0 then split x1 (p1 ** b) (i1 ** b) (n1 ** b)
else split x2 (p2 ** a) (i2 ** a) (n2 ** a)
......@@ -370,13 +370,13 @@ module Make (T : E) : S with type s = T.t = struct
| `Split (_,`Atm x, `True,`False,`False) -> split0 (`Atm(T.diff T.full x)) `True `False `False
| `Split (_,`Atm x, `False,`False,`True) -> split0 (`Atm(T.diff T.full x)) `True `False `False
| `Split (_,x, p,i,`False) -> split x `False (neg (i ++ p)) (neg i)
| `Split (_,x, `False,i,n) -> split x (neg i) (neg (i ++ n)) `False
| `Split (_,x, p,`False,n) -> split x (neg p) (neg (p ++ n)) (neg n)
| `Split (_,x, `False,i,n) -> split x (neg i) (neg (i ++ n)) `False
| `Split (_,x, p,`False,n) -> split x (neg p) (neg (p ++ n)) (neg n)
| `Split (_,x, p,i,n) -> split x (neg (i ++ p)) `False (neg (i ++ n))
let rec ( // ) a b =
let negatm = T.diff T.full in
if a == b then `False
if a == b then `False
else match (a,b) with
| `False,_ | _, `True -> `False
| a, `False -> a
......@@ -397,15 +397,15 @@ module Make (T : E) : S with type s = T.t = struct
| `Split (_,x1, p1,i1,n1), `Split (_,x2, p2,i2,n2) ->
let c = X.compare x1 x2 in
if c = 0 then
if (i2 == `False) && (n2 == `False)
if (i2 == `False) && (n2 == `False)
then split x1 (p1 // p2) (i1 // p2) (n1 ++ i1)
else
else
split x1 ((p1++i1) // (p2 ++ i2)) `False ((n1++i1) // (n2 ++ i2))
else if c < 0 then
split x1 (p1 // b) (i1 // b) (n1 // b)
split x1 (p1 // b) (i1 // b) (n1 // b)
else
split x2 (a // (i2 ++ p2)) `False (a // (i2 ++ n2))
let cup = ( ++ )
let cap = ( ** )
let diff = ( // )
......@@ -432,4 +432,11 @@ module Make (T : E) : S with type s = T.t = struct
(v,t)
*)
let build l =
let conj acc cons l =
List.fold_left (fun acc e -> cons acc (atom e)) acc l
in
List.fold_left (fun acc (p, n) ->
cup acc (diff (conj full cap p) (conj empty cup n)))
empty l
end
......@@ -21,7 +21,7 @@ module type S = sig
val leafconj: t -> s
val get: t -> (elem list * elem list) list
val build : (elem list * elem list) list -> t
val empty : t
val full : t
(* same as full, but we keep it for the moment to avoid chaging the code everywhere *)
......@@ -51,4 +51,4 @@ module type S = sig
end
module type MAKE = functor (T : E) -> S with type s = T.t
module Make : MAKE
module Make : MAKE
......@@ -1808,34 +1808,42 @@ struct
tlv : intersection of toplevel variables that are common to all non empty kinds
tv : the rest of the type
*)
let if_no_var (type s) (module BV : BoolVar.S with type t = s) bdd =
try
BV.iter (function `Var _ -> raise Not_found | _ -> ()) bdd;
bdd
with
_ -> BV.empty
let split_vars (type s) (module BV : BoolVar.S with type t = s) bdd =
List.fold_left (fun (acc_v, acc_nv) (p, n) ->
match p, n with
(([ `Atm _ ]|[]), ([ `Atm _]| [])) ->
acc_v, BV.cup acc_nv (BV.build [ (p,n)])
| _ -> BV.cup acc_v (BV.build [(p,n)]), acc_nv) (BV.empty,BV.empty) (BV.get bdd)
in
let if_eq empty t1 t2 = if t1 == t2 then empty else t2 in
let vchars, nvchars = split_vars (module BoolChars) not_seq.chars in
let vints, nvints = split_vars (module BoolIntervals) not_seq.ints in
let vatoms, nvatoms = split_vars (module BoolAtoms) not_seq.atoms in
let vtimes, nvtimes = split_vars (module BoolPair) not_seq.times in
let vxml, nvxml = split_vars (module BoolPair) not_seq.xml in
let varrow, nvarrow = split_vars (module BoolPair) not_seq.arrow in
let vrecord, nvrecord = split_vars (module BoolRec) not_seq.record in
let vabstract, nvabstract = split_vars (module BoolAbstracts) not_seq.abstract in
let not_var = { empty with
chars = if_no_var (module BoolChars) not_seq.chars;
ints = if_no_var (module BoolIntervals) not_seq.ints;
atoms = if_no_var (module BoolAtoms) not_seq.atoms;
times = if_no_var (module BoolPair) not_seq.times;
xml = if_no_var (module BoolPair) not_seq.xml;
arrow = if_no_var (module BoolPair) not_seq.arrow;
record = if_no_var (module BoolRec) not_seq.record;
abstract = if_no_var (module BoolAbstracts) not_seq.abstract
chars = nvchars;
ints = nvints;
atoms = nvatoms;
times = nvtimes;
xml = nvxml;
arrow = nvarrow;
record = nvrecord;
abstract = nvabstract;
}
in
let not_seq = { not_seq with
chars = if_eq BoolChars.empty not_var.chars not_seq.chars;
ints = if_eq BoolIntervals.empty not_var.ints not_seq.ints;
atoms = if_eq BoolAtoms.empty not_var.atoms not_seq.atoms;
times = if_eq BoolPair.empty not_var.times not_seq.times;
xml = if_eq BoolPair.empty not_var.xml not_seq.xml;
arrow = if_eq BoolPair.empty not_var.arrow not_seq.arrow;
record = if_eq BoolRec.empty not_var.record not_seq.record;
abstract = if_eq BoolAbstracts.empty not_var.abstract not_seq.abstract;
chars = vchars;
ints = vints;
atoms = vatoms;
times = vtimes;
xml = vxml;
arrow = varrow;
record = vrecord;
abstract = vabstract;
}
in
let all_vars_in_line l =
......@@ -1883,26 +1891,30 @@ struct
(cup (cap (inter_tlv (fun x -> x) tv_pos p)
(inter_tlv (fun x -> diff full x) tv_neg n)) acc)
) empty (get bdd)
in
let printed_topvar, not_seq =
if Var.Set.is_empty tv_pos && Var.Set.is_empty tv_neg then [], not_seq
else
(Var.Set.fold (fun acc v -> (Atomic (fun ppf -> Var.pp ppf v)) :: acc)
(Var.Set.fold (fun acc v -> (Neg (alloc [Atomic (fun ppf -> Var.pp ppf v)])) :: acc) [] tv_neg)
tv_pos),
{ not_seq with
chars = remove_tlv (module BoolChars) not_seq.chars;
ints = remove_tlv (module BoolIntervals) not_seq.ints;
atoms = remove_tlv (module BoolAtoms) not_seq.atoms;
times = remove_tlv (module BoolPair) not_seq.times;
xml = remove_tlv (module BoolPair) not_seq.xml;
arrow = remove_tlv (module BoolPair) not_seq.arrow;
record = remove_tlv (module BoolRec) not_seq.record;
abstract = remove_tlv (module BoolAbstracts) not_seq.abstract
}
in
in
let type_tlv =
diff (Var.Set.fold (fun acc v -> cap acc (var v)) any tv_pos)
(Var.Set.fold (fun acc v -> cup acc (var v)) empty tv_neg)
in
let printed_topvar, not_seq =
if Var.Set.is_empty tv_pos && Var.Set.is_empty tv_neg then [], not_seq
else
let not_seq = cup not_seq (cap not_var type_tlv) in
(Var.Set.fold (fun acc v -> (Atomic (fun ppf -> Var.pp ppf v)) :: acc)
(Var.Set.fold (fun acc v -> (Neg (alloc [Atomic (fun ppf -> Var.pp ppf v)])) :: acc) [] tv_neg)
tv_pos),
{ not_seq with
chars = remove_tlv (module BoolChars) not_seq.chars;
ints = remove_tlv (module BoolIntervals) not_seq.ints;
atoms = remove_tlv (module BoolAtoms) not_seq.atoms;
times = remove_tlv (module BoolPair) not_seq.times;
xml = remove_tlv (module BoolPair) not_seq.xml;
arrow = remove_tlv (module BoolPair) not_seq.arrow;
record = remove_tlv (module BoolRec) not_seq.record;
abstract = remove_tlv (module BoolAbstracts) not_seq.abstract
}
in
let cons constr empty = function
[] -> empty
......
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