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

Fix regression where (wrong) Empty types appear everywhere. Also remove some suprious parentheses.

parent 5e0a09a3
......@@ -1702,16 +1702,6 @@ struct
end
module VarTable = Hashtbl.Make(Key)
module KeySet = Set.Make(Key)
type matrix = {
mchars : BoolChars.t VarTable.t;
mints : BoolIntervals.t VarTable.t;
matoms : BoolAtoms.t VarTable.t;
mtimes : BoolPair.t VarTable.t;
mxml : BoolPair.t VarTable.t;
marrow : BoolPair.t VarTable.t;
mrecord : BoolRec.t VarTable.t;
mabstract : BoolAbstracts.t VarTable.t;
}
let compare x y = x.id - y.id
......@@ -1965,139 +1955,139 @@ struct
) [] 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 ]
if is_empty tt then None else
let print_topvars pos rem =
let printed_nvars = print_vars nvars in
let negative_part = match printed_nvars @ (if not pos then rem else []) with
([] | [ _ ]) as l -> l
| l -> [ union l ]
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 -> [ intersection ((union l1) :: [ Neg (alloc [union l2]) ] @ rem) ]
| l1,l2, l3 -> [ intersection ([ union l1; intersection [ intersection l2; Neg(alloc l3)]] @ rem) ]
let positive_part2 = match printed_lvars @ (if pos then rem else []) with
([] | [ _ ]) as l -> l
| l -> [ union l ]
in
let positive_part = (print_vars pvars) @ positive_part2 in
match positive_part, negative_part with
[], [] -> None
| [], l -> Some ( Neg (alloc l) )
| l, [] -> Some ( intersection l )
| l1, l2 -> Some ( intersection [ intersection l1; Neg (alloc l2) ])
in
if subtype any tt then print_topvars [] else
let tt, fix =
if subtype any tt then print_topvars true [] else
let tt, positive =
if worth_complement tt then
diff any tt, (fun x -> [Neg (alloc x)])
else tt , fun x -> x
diff any tt, false
else tt , true
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
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 (List.map (fun x -> (Atomic x)) (Chars.print bdd))]
) tt.chars u_acc
in
let u_acc = prepare_boolvar BoolChars.get (fun bdd ->
match Chars.is_char bdd with
| Some c -> [Char c]
| 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 (List.map (fun x -> (Atomic x)) l)]
) tt.ints u_acc
in
let u_acc = prepare_boolvar BoolIntervals.get (fun bdd ->
match Intervals.print bdd with
|[x] -> [Atomic x]
|l -> [union (List.map (fun x -> (Atomic x)) l)]
) tt.ints u_acc
in
let bool =
Atoms.cup
(Atoms.atom (Atoms.V.mk_ascii "false"))
(Atoms.atom (Atoms.V.mk_ascii "true"))
in
let u_acc = prepare_boolvar BoolAtoms.get (fun bdd ->
match Atoms.print bdd with
|[x] when (Atoms.equal bool bdd) ->
[Atomic (fun ppf -> Format.fprintf ppf "Bool")]
|[x] -> [Atomic x]
|l -> [ union (List.map (fun x -> (Atomic x)) l) ]
) tt.atoms u_acc
in
let bool =
Atoms.cup
(Atoms.atom (Atoms.V.mk_ascii "false"))
(Atoms.atom (Atoms.V.mk_ascii "true"))
in
let u_acc = prepare_boolvar BoolAtoms.get (fun bdd ->
match Atoms.print bdd with
|[x] when (Atoms.equal bool bdd) ->
[Atomic (fun ppf -> Format.fprintf ppf "Bool")]
|[x] -> [Atomic x]
|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.rev_map (fun (t1,t2) ->
Pair (prepare t1, prepare t2)
) (Product.partition any x)
) tt.times u_acc
in
(* pairs *)
let u_acc = prepare_boolvar BoolPair.get (fun x ->
List.rev_map (fun (t1,t2) ->
Pair (prepare t1, prepare t2)
) (Product.partition any x)
) tt.times u_acc
in
(* xml pairs *)
let u_acc = prepare_boolvar BoolPair.get (fun x ->
List.flatten (
List.map (fun (t1,t2) ->
try let n = DescrPairMap.find (t1,t2) !named_xml in [(Name n)]
with Not_found ->
let tag =
match Atoms.print_tag (BoolAtoms.leafconj t1.atoms) with
| Some a when is_empty { t1 with atoms = BoolAtoms.empty } -> `Tag a
| _ -> `Type (prepare t1)
in
assert (equal { t2 with times = empty.times } empty);
List.rev_map (fun (ta,tb) ->
(Xml (tag, prepare ta, prepare tb))
) (Product.get t2);
) (Product.partition any_pair x)
)
) tt.xml u_acc
in
(* xml pairs *)
let u_acc = prepare_boolvar BoolPair.get (fun x ->
List.flatten (
List.map (fun (t1,t2) ->
try let n = DescrPairMap.find (t1,t2) !named_xml in [(Name n)]
with Not_found ->
let tag =
match Atoms.print_tag (BoolAtoms.leafconj t1.atoms) with
| Some a when is_empty { t1 with atoms = BoolAtoms.empty } -> `Tag a
| _ -> `Type (prepare t1)
in
assert (equal { t2 with times = empty.times } empty);
List.rev_map (fun (ta,tb) ->
(Xml (tag, prepare ta, prepare tb))
) (Product.get t2);
) (Product.partition any_pair x)
)
) tt.xml u_acc
in
(* arrows *)
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.rev_map aux p and n = List.rev_map aux n in
(Arrows (p,n))
) (Pair.get x)) tt.arrow u_acc
in
(* arrows *)
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.rev_map aux p and n = List.rev_map aux n in
(Arrows (p,n))
) (Pair.get x)) tt.arrow u_acc
in
(* records *)
let u_acc = prepare_boolvar BoolRec.get (fun x ->
List.map (fun (r,some,none) ->
let r = LabelMap.map (fun (o,t) -> (o, prepare t)) r in
(Record (r,some,none))
) (Record.get { empty with record = BoolRec.atom (`Atm x) })) tt.record u_acc
in
(* records *)
let u_acc = prepare_boolvar BoolRec.get (fun x ->
List.map (fun (r,some,none) ->
let r = LabelMap.map (fun (o,t) -> (o, prepare t)) r in
(Record (r,some,none))
) (Record.get { empty with record = BoolRec.atom (`Atm x) })) tt.record u_acc
in
let u_acc = prepare_boolvar BoolAbstracts.get (fun bdd ->
match Abstracts.print bdd with
|[x] -> [Atomic x]
|l -> [Union(alloc (List.map (fun x -> (Atomic x)) l))]
) tt.abstract u_acc
in
let u_acc = prepare_boolvar BoolAbstracts.get (fun bdd ->
match Abstracts.print bdd with
|[x] -> [Atomic x]
|l -> [Union(alloc (List.map (fun x -> (Atomic x)) l))]
) tt.abstract u_acc
in
let u_acc =
if tt.absent then (Atomic (fun ppf -> Format.fprintf ppf "#ABSENT")) :: u_acc
else u_acc
in
let p_t = fix u_acc in
print_topvars p_t
in
let all_printed =
List.fold_left (fun acc (factvars,lvars,t) ->
match print_descr factvars lvars t with
[] -> acc
| [p] -> p :: acc
| l -> (intersection l) :: acc
) [] all_descrs
in
slot.def <- all_printed @ slot.def;
slot
let u_acc =
if tt.absent then (Atomic (fun ppf -> Format.fprintf ppf "#ABSENT")) :: u_acc
else u_acc
in
print_topvars positive u_acc
in
let all_printed =
List.fold_left (fun acc (factvars,lvars,t) ->
match print_descr factvars lvars t, acc with
None, _ -> acc
| Some p, (Union { def = l }) :: racc -> (union (p :: l)) :: racc
| Some p, _ -> p::acc
) [] all_descrs
in
slot.def <- all_printed @ slot.def;
slot
and decompile d =
let aux t =
let tr = Product.get t in
......@@ -2127,6 +2117,62 @@ struct
in
Decompile.decompile aux d
(* clean a pretty-printed representation:
- merge intersection of intersections/unions of unions
*)
let cleanup_pretty nd =
let rec clean_nd parent nd =
{ nd with def = clean_slot parent nd.def }
and clean_slot parent l =
List.fold_right (fun d acc ->
(clean_d parent d) @ acc ) l []
and clean_d parent d =
match d with
| Name _ | Atomic _ | Char _ -> [ d ]
| Regexp reg -> [ Regexp (clean_regexp d reg) ]
| Pair (nd1, nd2) -> [ Pair(clean_nd d nd1, clean_nd d nd2) ]
| Xml (t, nd1, nd2) ->
let nt = match t with
`Tag _ as x -> x
| `Type nd0 -> `Type (clean_nd d nd0)
in
[ Xml (nt, clean_nd d nd1, clean_nd d nd2) ]
| Record (lm, b1, b2) ->
[ Record(Ident.LabelMap.map (fun (b, nd) -> b, clean_nd d nd) lm, b1, b2) ]
| Arrows (l1, l2) ->
[ Arrows (List.map (fun (nd1, nd2) -> (clean_nd d nd1, clean_nd d nd2)) l1,
List.map (fun (nd1, nd2) -> (clean_nd d nd1, clean_nd d nd2)) l2)]
| Intersection nd ->
let new_nd = clean_nd d nd in begin
match parent, new_nd.def with
Intersection _,_ | _, [ _ ] -> new_nd.def
| _ -> [ Intersection new_nd ]
end
| Union nd ->
let new_nd = clean_nd d nd in begin
match parent, new_nd.def with
Union _,_ | _, [ _ ] -> new_nd.def
| _ -> [ Union new_nd ] end
| Neg nd ->
let new_nd = clean_nd d nd in begin
match new_nd.def with
[ Neg nd' ] -> nd'.def
| _ -> [ Neg new_nd ] end
| Abs nd -> [ Abs (clean_nd d nd) ]
and clean_regexp parent reg =
match reg with
Pretty.Empty | Pretty.Epsilon -> reg
| Pretty.Seq (r1, r2) -> Pretty.Seq(clean_regexp parent r1,
clean_regexp parent r2)
| Pretty.Alt (r1, r2) -> Pretty.Alt(clean_regexp parent r1,
clean_regexp parent r2)
| Pretty.Star r -> Pretty.Star(clean_regexp parent r)
| Pretty.Plus r -> Pretty.Plus(clean_regexp parent r)
| Pretty.Trans nd -> Pretty.Trans(clean_nd parent nd)
in
clean_nd (Union (alloc [])) nd
let gen = ref 0
let rec assign_name s =
......@@ -2293,6 +2339,7 @@ struct
let pp_type ppf t =
let t = uniq t in
let t = prepare t in
let t = cleanup_pretty t in
assign_name t;
Format.fprintf ppf "@[@[%a@]" (do_print_slot 0) t;
(match List.rev !to_print with
......
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