Commit 89a5e61c authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Further improve the pretty printing with the following algorithm.

Given a type for which each kind is i DNF :

ints: \/ /\a /\v /\~b /\~w
chars: \/ /\a /\v /\~b /\~w
...

where a, b are atoms and v w toplevel variables, index the type by
pairs of variables, for each kind, which gives a matrix of 8 lines.
                    ...   (v, w) ...   (x,y) ...
ints:                      t1           t1
chars:                     ...         ...
atoms:
times:
xml:
arrow:
record:
abstract:                  t8           t8

let T = t1 | ... | t8,
we can write ((v & w) | (x & y)) & T
we now try to factor according to variables (intersection of v x and w y)
to have a type of the form: ('a | ... | 'd) & 'e ... & (Any \ 'f) & T
parent e2548aaa
......@@ -1823,14 +1823,6 @@ struct
(empty, d)
in
(*
We split the non_sequence type as follows to have a better display :
t = t_nv | (tlv^ tv)
t_nv : part of the types without any variables
tlv : intersection of toplevel variables that are common to all non empty kinds
tv : the rest of the type
*)
(* Given a bdd
\/_i (p_i & pvar_i, n_i& nvar_i)
we fill a table appropriately where the entries are the (pvar_i,nvar_i)
......@@ -1845,80 +1837,76 @@ struct
) (Var.Set.empty, init) l
in
let fill_line (type s)
(module BV : BoolVar.S with type t = s) (table : s VarTable.t) (bdd : s) =
(module BV : BoolVar.S with type t = s) table get set t =
List.iter (fun (p, n) ->
let v1, a1 = split_var_atom (fun a b -> BV.(cap (atom a) b)) BV.full p in
let v2, a2 = split_var_atom (fun a b -> BV.(cup (atom a) b)) BV.empty n in
let a = BV.diff a1 a2 in
let key = v1, v2 in
let new_a = try BV.cup a (VarTable.find table key) with Not_found -> a in
VarTable.replace table key new_a) (BV.get bdd);
table
in
let not_seq_matrix =
{ mints = (let h = VarTable.create 17 in fill_line (module BoolIntervals) h not_seq.ints);
mchars = (let h = VarTable.create 17 in fill_line (module BoolChars) h not_seq.chars);
matoms = (let h = VarTable.create 17 in fill_line (module BoolAtoms) h not_seq.atoms);
mtimes = (let h = VarTable.create 17 in fill_line (module BoolPair) h not_seq.times);
mxml = (let h = VarTable.create 17 in fill_line (module BoolPair) h not_seq.xml);
marrow = (let h = VarTable.create 17 in fill_line (module BoolPair) h not_seq.arrow);
mrecord = (let h = VarTable.create 17 in fill_line (module BoolRec) h not_seq.record);
mabstract = (let h = VarTable.create 17 in fill_line (module BoolAbstracts) h not_seq.abstract); }
in
let get_keys table acc = VarTable.fold (fun k _ acc ->
KeySet.add k acc) table acc
in
let all_keys =
let m = not_seq_matrix in
let acc = get_keys m.mints KeySet.empty in
let acc = get_keys m.mchars acc in
let acc = get_keys m.matoms acc in
let acc = get_keys m.mxml acc in
let acc = get_keys m.marrow acc in
let acc = get_keys m.mrecord acc in
get_keys m.mabstract acc
let old_t = try VarTable.find table key with Not_found -> {empty with absent = t.absent } in
let new_a = BV.cup a (get old_t) in
VarTable.replace table key (set old_t new_a)) (BV.get (get t))
in
let h = VarTable.create 17 in
fill_line (module BoolIntervals) h (fun t -> t.ints) (fun t u -> {t with ints = u }) not_seq;
fill_line (module BoolChars) h (fun t -> t.chars) (fun t u -> {t with chars = u }) not_seq;
fill_line (module BoolAtoms) h (fun t -> t.atoms) (fun t u -> {t with atoms = u }) not_seq;
fill_line (module BoolPair) h (fun t -> t.times) (fun t u -> {t with times = u }) not_seq;
fill_line (module BoolPair) h (fun t -> t.xml) (fun t u -> {t with xml = u }) not_seq;
fill_line (module BoolPair) h (fun t -> t.arrow) (fun t u -> {t with arrow = u }) not_seq;
fill_line (module BoolRec) h (fun t -> t.record) (fun t u -> {t with record = u }) not_seq;
fill_line (module BoolAbstracts) h (fun t -> t.abstract) (fun t u -> {t with abstract = u }) not_seq;
let found_any, all_descrs =
let m = not_seq_matrix in
let get k m e = try VarTable.find m k with Not_found -> e
in
let found_any = ref false in
let res =
KeySet.fold (fun ((v1, v2) as k) acc ->
(*Format.eprintf "Processing set: %a, %a@\n%!"
Var.Set.pp v1 Var.Set.pp v2; *)
if !found_any then acc
else if Var.Set.(not (is_empty (inter v1 v2)))
then ((*Format.eprintf "Found some variables in common: %a\n@!"
Var.Set.pp (Var.Set.inter v1 v2);*) acc)
else
let tt =
{ empty with
ints = get k m.mints BoolIntervals.empty;
chars = get k m.mchars BoolChars.empty;
atoms = get k m.matoms BoolAtoms.empty;
times = get k m.mtimes BoolPair.empty;
xml = get k m.mxml BoolPair.empty;
arrow = get k m.marrow BoolPair.empty;
record = get k m.mrecord BoolRec.empty;
abstract = get k m.mabstract BoolAbstracts.empty;
absent = not_seq.absent;
}
in
if is_empty tt then acc
try
let res =
VarTable.fold (fun ((v1, v2) as k) tt acc ->
if Var.Set.(not (is_empty (inter v1 v2))) || is_empty tt then acc
else if Var.Set.(is_empty v1 && is_empty v2) &&
subtype any tt then raise Not_found
else
if Var.Set.(is_empty v1 && is_empty v2) &&
subtype any tt then (found_any := true; acc) else
(k, tt) :: acc
) all_keys []
in
!found_any, res
(k, tt) :: acc
) h []
in
false, res
with Not_found -> true, [ Var.Set.(empty,empty), any ]
in
(*Format.eprintf "All descr has size: %i, all_keys has size: %i, found_any=%b@\n%!" (List.length all_descrs) KeySet.(cardinal all_keys) found_any; *)
if found_any then (slot.def <- [Neg (alloc [])];slot)
else
let merge_column_with (v1,t1) l =
List.fold_left (fun (accv, accl) ((v2,t2) as x) ->
if equal t1 t2 then (v2::accv, accl) else (accv,x::accl))
([ v1 ],[]) l
in
let merge_variables l =
match l with
[] -> (Var.Set.empty, Var.Set.empty), []
| i :: ll ->
let factp, factn =
List.fold_left (fun (accp, accn) (vp, vn) ->
Var.Set.(inter accp vp, inter accn vn))
i ll
in
let nl =
List.fold_left (fun acc (vp, vn) ->
let nvp = Var.Set.diff vp factp in
let nvn = Var.Set.diff vn factn in
if Var.Set.(is_empty nvp && is_empty nvn) then acc
else (nvp, nvn) :: acc
) [] l
in
(factp, factn), nl
in
let rec merge_columns acc l =
match l with
[] -> acc
| ((_, t) as e) :: ll ->
let vars, nll = merge_column_with e ll in
let factv,remv = merge_variables vars in
merge_columns ((factv, remv,t)::acc) nll
in
let all_descrs = merge_columns [] all_descrs in
let cons constr empty = function
[] -> empty
| [] -> empty
| [ t ] -> t
| l -> constr (alloc l)
in
......@@ -1927,7 +1915,8 @@ struct
let prepare_boolvar get print bdd acc =
let fold_line acc l = List.fold_left (fun acc t ->
match t with
| `Var _ as x -> (Atomic (fun ppf -> Var.pp ppf x)) :: acc
| `Var _ -> assert false
(* there should not be any toplevel variable left *)
| `Atm bdd -> (print bdd) @ acc) acc l
in
List.fold_left (fun acc (p,n) ->
......@@ -1941,15 +1930,28 @@ struct
) acc (get bdd)
in
let printed_seq = if non_empty seq then (Regexp (decompile seq)) :: [] else [] in
let print_descr tv_pos tv_neg tt =
let print_vars l =
List.fold_left (fun acc (p,n) ->
let pneg =
Var.Set.fold
(fun acc v -> (Neg (alloc [Atomic (fun ppf -> Var.pp ppf v)])) :: acc) [] n
in
match Var.Set.fold
(fun acc v -> (Atomic (fun ppf -> Var.pp ppf v)) :: acc) pneg p
with
[] -> acc
| [ p ] -> p :: acc
| l -> (intersection l) :: acc
) [] l
in
let print_descr factvars lvars tt =
if is_empty tt then [] else
let printed_lvars = print_vars lvars in
let printed_factvars = print_vars [ factvars ] in
let printed_topvars =
let pneg =
Var.Set.fold
(fun acc v -> (Neg (alloc [Atomic (fun ppf -> Var.pp ppf v)])) :: acc) [] tv_neg
in
Var.Set.fold
(fun acc v -> (Atomic (fun ppf -> Var.pp ppf v)) :: acc) pneg tv_pos
match printed_lvars, printed_factvars with
[], l -> l
| l1, l2 -> (union l1) :: l2
in
if subtype any tt then printed_topvars else
let tt, fix =
......@@ -2045,8 +2047,8 @@ struct
printed_topvars @ p_t
in
let all_printed =
List.fold_left (fun acc ((vp,vn),t) ->
match print_descr vp vn t with
List.fold_left (fun acc (factvars,lvars,t) ->
match print_descr factvars lvars t with
[] -> acc
| [p] -> p :: acc
| l -> (intersection l) :: acc
......
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