Skip to content

GitLab

Commit 5bb3b23f authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Fix printing of sequence types intersected with variables.

parent a2efc762
Hide whitespace changes
Inline Side-by-side
Showing with 68 additions and 52 deletions
types/types.ml
View file @ 5bb3b23f
......@@ -1816,13 +1816,6 @@ struct
DescrHash.add memo d slot;
let (seq,not_seq) =
if (subtype { empty with times = d.times } seqs_descr) then
(cap d seqs_descr, diff d seqs_descr)
else
(empty, d)
in
(* 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)
......@@ -1848,14 +1841,14 @@ struct
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;
fill_line (module BoolIntervals) h (fun t -> t.ints) (fun t u -> {t with ints = u }) d;
fill_line (module BoolChars) h (fun t -> t.chars) (fun t u -> {t with chars = u }) d;
fill_line (module BoolAtoms) h (fun t -> t.atoms) (fun t u -> {t with atoms = u }) d;
fill_line (module BoolPair) h (fun t -> t.times) (fun t u -> {t with times = u }) d;
fill_line (module BoolPair) h (fun t -> t.xml) (fun t u -> {t with xml = u }) d;
fill_line (module BoolPair) h (fun t -> t.arrow) (fun t u -> {t with arrow = u }) d;
fill_line (module BoolRec) h (fun t -> t.record) (fun t u -> {t with record = u }) d;
fill_line (module BoolAbstracts) h (fun t -> t.abstract) (fun t u -> {t with abstract = u }) d;
let found_any, all_descrs =
try
let res =
......@@ -1929,47 +1922,70 @@ struct
| p, n -> (intersection (p @ (List.map (fun n -> Neg (alloc [ n] )) n))) :: acc
) acc (get bdd)
in
let printed_seq = if non_empty seq then (Regexp (decompile seq)) :: [] else [] in
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 =
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 =
if worth_complement tt then diff any tt, (fun x -> [Neg (alloc x)])
else tt , fun x -> x
let print_vars l =
Var.Set.fold
(fun acc v -> (Atomic (fun ppf -> Var.pp ppf v)) :: acc) [] l
in
let print_pnvars l =
List.fold_left (fun acc (p,n) ->
let pneg = print_vars n in
let ppos = print_vars p in
match List.rev ppos, List.rev pneg with
[],[] -> acc
| [p],[] -> p::acc
| [],l -> Neg(alloc[ (union l)]) :: acc
| l, [] -> (intersection l) :: acc
| l1,l2 -> (intersection [intersection l1;
Neg(alloc[ (union l2)])]) :: acc
) [] l
in
let print_descr (pvars,nvars) lvars tt =
if is_empty tt then [] else
let print_topvars rem =
let rem = match rem with
[] -> []
| _ -> [ union rem ]
in
let printed_lvars = print_pnvars lvars in
let printed_pvars = print_vars pvars in
let printed_nvars = print_vars nvars in
match printed_lvars, printed_pvars, printed_nvars with
[],[],[] -> rem
| [],l,[] -> [ intersection (l @ rem) ]
| l1,l2,[] -> [ intersection ((union l1) :: (l2 @ rem)) ]
| [],[],l2 -> [ intersection ([ Neg (alloc [union l2]) ] @ rem)]
| l1,l2, l3 -> [ intersection ([ union l1; intersection [ intersection l2; Neg(alloc l3)]] @ rem) ]
in
if subtype any tt then print_topvars [] else
let tt, fix =
if worth_complement tt then
diff any tt, (fun x -> [Neg (alloc x)])
else tt , fun x -> x
in
(* sequence type *)
let u_acc, tt =
if subtype { empty with times = tt.times } seqs_descr
&& not (BoolPair.is_empty tt.times)
then
let seq = cap tt seqs_descr in
[ (Regexp (decompile seq)) ], diff tt seqs_descr
else
[], tt
in
(* base types *)
let u_acc = prepare_boolvar BoolChars.get (fun bdd ->
match Chars.is_char bdd with
| Some c -> [Char c]
| None -> [Union(alloc (List.map (fun x -> (Atomic x)) (Chars.print bdd)))]
) tt.chars []
| None ->
[union (List.map (fun x -> (Atomic x)) (Chars.print bdd))]
) tt.chars u_acc
in
let u_acc = prepare_boolvar BoolIntervals.get (fun bdd ->
match Intervals.print bdd with
|[x] -> [Atomic x]
|l -> [Union(alloc (List.map (fun x -> (Atomic x)) l))]
|l -> [union (List.map (fun x -> (Atomic x)) l)]
) tt.ints u_acc
in
......@@ -1983,13 +1999,13 @@ struct
|[x] when (Atoms.equal bool bdd) ->
[Atomic (fun ppf -> Format.fprintf ppf "Bool")]
|[x] -> [Atomic x]
|l -> [Union(alloc (List.map (fun x -> (Atomic x)) l))]
|l -> [ union (List.map (fun x -> (Atomic x)) l) ]
) tt.atoms u_acc
in
(* pairs *)
let u_acc = prepare_boolvar BoolPair.get (fun x ->
List.map (fun (t1,t2) ->
List.rev_map (fun (t1,t2) ->
Pair (prepare t1, prepare t2)
) (Product.partition any x)
) tt.times u_acc
......@@ -2007,7 +2023,7 @@ struct
| _ -> `Type (prepare t1)
in
assert (equal { t2 with times = empty.times } empty);
List.map (fun (ta,tb) ->
List.rev_map (fun (ta,tb) ->
(Xml (tag, prepare ta, prepare tb))
) (Product.get t2);
) (Product.partition any_pair x)
......@@ -2019,7 +2035,7 @@ struct
let u_acc = prepare_boolvar BoolPair.get (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
let p = List.rev_map aux p and n = List.rev_map aux n in
(Arrows (p,n))
) (Pair.get x)) tt.arrow u_acc
in
......@@ -2044,7 +2060,7 @@ struct
else u_acc
in
let p_t = fix u_acc in
printed_topvars @ p_t
print_topvars p_t
in
let all_printed =
List.fold_left (fun acc (factvars,lvars,t) ->
......@@ -2052,7 +2068,7 @@ struct
[] -> acc
| [p] -> p :: acc
| l -> (intersection l) :: acc
) printed_seq all_descrs
) [] all_descrs
in
slot.def <- all_printed @ slot.def;
slot
......
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