Skip to content

GitLab

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

Fix various bugs in the pretty-printer (union of atoms not parenthesized, |... 

Fix various bugs in the pretty-printer (union of atoms not parenthesized, | instead of & for some toplevel variables)
parent 8aacb975
Hide whitespace changes
Inline Side-by-side
Showing with 136 additions and 113 deletions
types/atoms.ml
View file @ b8e562b5
......@@ -62,6 +62,18 @@ let print s = match get s with
Format.fprintf ppf " \\@ (%a)" (print_symbolset ns) s)
l ]
let extract s =
let tr l =
List.map (fun (ns, ss) -> ns, match ss with
SymbolSet.Finite l -> `Finite l
| SymbolSet.Cofinite l -> `Cofinite l) l
in
match get s with
`Finite l -> `Finite (tr l)
| `Cofinite l -> `Cofinite (tr l)
type 'a map = 'a Imap.t * 'a Imap.t * 'a option
let map_map f (m1,m2,o) =
......
types/atoms.mli
View file @ b8e562b5
......@@ -41,3 +41,9 @@ type 'a map
val mk_map: (t * 'a) list -> 'a map
val get_map: V.t -> 'a map -> 'a
val map_map: ('a -> 'b) -> 'a map -> 'b map
val extract : t ->
[ `Finite of (Ns.Uri.t * [`Finite of V.t list |`Cofinite of V.t list]) list
| `Cofinite of (Ns.Uri.t * [`Finite of V.t list |`Cofinite of V.t list]) list
]
types/types.ml
View file @ b8e562b5
......@@ -1567,7 +1567,8 @@ module Iter =
~empty ~full:any_record ~cup ~cap ~diff ~atom:(var_or record_bdd) t.record);]
let simplify t =
let simplify =
let memo = DescrHash.create 17 in
let aux (type bdd) (type atom)
inj
(module BV : BoolVar.S with type t = bdd and type Atom.t = atom ) b
......@@ -1595,29 +1596,35 @@ module Iter =
in
loop b
in
{ t with
atoms = aux (fun i -> { empty with atoms = i })
(module BoolAtoms) t.atoms;
chars = aux (fun i -> { empty with chars = i })
(module BoolChars) t.chars;
ints = aux (fun i -> { empty with ints = i })
(module BoolIntervals) t.ints;
abstract = aux (fun i -> { empty with abstract = i })
(module BoolAbstracts) t.abstract;
times = aux (fun i -> { empty with times = i })
(module BoolPair) t.times;
xml = aux (fun i -> { empty with xml = i })
(module BoolPair) t.xml;
arrow = aux (fun i -> { empty with arrow = i })
(module BoolPair) t.arrow;
record = aux (fun i -> { empty with record = i })
(module BoolRec) t.record;
}
fun t ->
try DescrHash.find memo t with
Not_found ->
let res =
{ t with
atoms = aux (fun i -> { empty with atoms = i })
(module BoolAtoms) t.atoms;
chars = aux (fun i -> { empty with chars = i })
(module BoolChars) t.chars;
ints = aux (fun i -> { empty with ints = i })
(module BoolIntervals) t.ints;
abstract = aux (fun i -> { empty with abstract = i })
(module BoolAbstracts) t.abstract;
times = aux (fun i -> { empty with times = i })
(module BoolPair) t.times;
xml = aux (fun i -> { empty with xml = i })
(module BoolPair) t.xml;
arrow = aux (fun i -> { empty with arrow = i })
(module BoolPair) t.arrow;
record = aux (fun i -> { empty with record = i })
(module BoolRec) t.record;
}
in
DescrHash.add memo t res;
DescrHash.add memo res res;
res
let compute_bdd ~typ ~cup ~cap ~neg ~var ~atoms ~ints ~chars ~times ~xml ~arrow ~record ~abstract ~absent t =
let t = simplify t in
let any_node2 = any_node, any_node in
let any_atoms = atoms Atoms.full in
let any_ints = ints Intervals.full in
......@@ -1954,6 +1961,7 @@ module Print = struct
}
and d =
| Name of gname
| Display of string
| Regexp of nd Pretty.regexp
| Atomic of (Format.formatter -> unit)
| Pair of nd * nd
......@@ -2073,6 +2081,13 @@ module Print = struct
end
in
loop t
let bool_type =
{ empty with atoms = BoolAtoms.atom
(`Atm(Atoms.cup
(Atoms.atom (Atoms.V.mk_ascii "false"))
(Atoms.atom (Atoms.V.mk_ascii "true"))))
}
(** [prepare d] massages a type and convert it to the syntactic form.
Rough algorithm:
......@@ -2172,27 +2187,6 @@ module Print = struct
) h; h'
with Not_found -> h
in
(*
let tt, rm_keys =
(* Simplify types of the form 'a & T | T \'a *)
VarTable.fold (fun (v1, v2) tt1 ((acc_empty, acc_keys) as acc) ->
match Var.Set.length v1, Var.Set.length v2 with
0, 1 | 1, 0 ->
let k2 = (v2, v1) in
begin try
let tt2 = VarTable.find h k2 in
if equiv tt2 tt1 then
(cup acc_empty tt1, k2::acc_keys)
else acc
with Not_found -> acc
end
| _ -> acc
) h ((try VarTable.find h Key.empty with Not_found -> empty), [])
in
if non_empty tt then VarTable.replace h Key.empty tt;
List.iter (fun (v1, v2) -> VarTable.remove h (v1, v2);
VarTable.remove h (v2, v1)) rm_keys; *)
let found_any, all_descrs =
try
......@@ -2242,9 +2236,9 @@ module Print = struct
let factv,remv = merge_variables vars in
merge_columns ((factv, remv,t)::acc) nll
in
(* list of (factv & remv & t) *)
let all_descrs = merge_columns [] all_descrs in
let inter_d l =
match l with
[] -> Neg (alloc [])
......@@ -2255,15 +2249,15 @@ module Print = struct
let inter_nd l =
match l with
[] -> Neg (alloc [])
| [ { def = [ p ] } ] -> p
| [ { def = [ p ] ; _ } ] -> p
| _ -> Intersection l
in
let prepare_boolvar get print bdd acc =
(* there should not be any toplevel variable left *)
match get bdd with
[ ] -> acc
| [ ([`Atm bdd], []) ] -> (print bdd) @ acc
| _ -> assert false
let diff_nd n1 n2 =
match n1, n2 with
| { def = []; _ }, { def = []; _ } -> []
| _ , { def = []; _ } -> n1.def
| { def = []; _ }, _ -> [ Neg n2 ]
| _ -> [ Diff(n1, n2) ]
in
let print_vars l =
Var.Set.fold
......@@ -2282,22 +2276,26 @@ module Print = struct
in
let print_descr (pvars,nvars) lvars tt =
if is_empty tt then [] else
(* [rem] prints the variable-less part of the type.
[pos] is true iff [rem] is positive
*)
let print_topvars pos rem =
let rem = List.rev rem in
let printed_nvars = List.rev (print_vars nvars) in
let negative_part = printed_nvars @ (if pos then [] else rem) in
let printed_lvars = print_pnvars lvars in
let positive_part2 = printed_lvars @ (if pos then rem else []) in
let positive_part =
(List.rev_map (fun e -> alloc [e]) (print_vars pvars))
@ (if positive_part2 == []
then [] else [ alloc positive_part2 ])
let alloc_l = function [] -> []
| l -> [ alloc l ]
in
match positive_part, negative_part with
[], [] -> []
| [], l -> [ Neg (alloc l) ]
| l, [] -> [ inter_nd l ]
| l1, l2 -> [ Diff (alloc [inter_nd l1], alloc l2) ]
let lpos =
List.fold_left (fun acc e ->
(alloc [e]) :: acc )
(alloc_l (if pos then rem else [])) (print_vars pvars)
in
let lneg = List.rev_append (print_vars nvars)
(if pos then [] else rem)
in
let lmid = alloc_l (List.rev (print_pnvars lvars)) in
diff_nd
(alloc [ inter_nd (lpos @ lmid) ])
(alloc lneg)
in
(*if subtype any tt then print_topvars true [] else*)
let tt, positive =
......@@ -2328,50 +2326,54 @@ module Print = struct
in
(* base types *)
let u_acc = prepare_boolvar BoolChars.get (fun bdd ->
match Chars.is_char bdd with
| Some c -> [Char c]
| None ->
List.map (fun x -> (Atomic x)) (Chars.print bdd)
) tt.chars u_acc
in
let u_acc = prepare_boolvar BoolIntervals.get (fun bdd ->
let l = Intervals.print bdd in
List.map (fun x -> (Atomic x)) l
) tt.ints u_acc
let u_acc =
(List.map (fun x -> Atomic x) (Chars.print (BoolChars.leafconj tt.chars)))
@ u_acc
in
let bool =
{ empty with atoms = BoolAtoms.atom
(`Atm(Atoms.cup
(Atoms.atom (Atoms.V.mk_ascii "false"))
(Atoms.atom (Atoms.V.mk_ascii "true"))))
}
let u_acc =
(List.map (fun x -> (Atomic x)) (Intervals.print (BoolIntervals.leafconj tt.ints)))
@ u_acc
in
let u_acc, tt = if finite_atoms &&
subtype bool tt
then
Atomic (fun ppf -> Format.fprintf ppf "Bool") :: u_acc,
diff tt bool
let u_acc, tt = if finite_atoms && subtype bool_type tt then
(Display "Bool") :: u_acc,
diff tt bool_type
else
u_acc, tt
in
let u_acc = prepare_boolvar BoolAtoms.get (fun bdd ->
List.map (fun x -> (Atomic x)) (Atoms.print bdd)
) tt.atoms u_acc
let pr_atoms l =
List.fold_left (fun acc (ns, atm) ->
(match atm with
`Finite l ->
List.map (fun a ->
Atomic (fun ppf -> Atoms.V.print_quote ppf a)) l
| `Cofinite l ->
[ Diff (alloc [ Atomic (fun ppf ->
Format.fprintf ppf "`%a"
Ns.InternalPrinter.print_any_ns ns) ]
,
alloc (List.map (fun a ->
Atomic (fun ppf -> Atoms.V.print_quote ppf a)) l))
]) @ acc
) [] l
in
let u_acc =
match Atoms.extract (BoolAtoms.leafconj tt.atoms) with
`Finite l -> (pr_atoms l) @ u_acc
| `Cofinite [] -> (Display "Atom") :: u_acc
| `Cofinite l -> (Diff (alloc[Display "Atom"],
alloc (pr_atoms l))) :: 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
let u_acc =
List.fold_left (fun acc (t1,t2) ->
(Pair (prepare t1, prepare t2)) :: acc
)
u_acc (Product.partition any (BoolPair.leafconj tt.times))
in
(* xml pairs *)
let u_acc = prepare_boolvar BoolPair.get (fun x ->
List.flatten (
let u_acc =
(List.flatten (
List.map (fun (t1,t2) ->
try let n = DescrPairMap.find (t1,t2) !named_xml in [(Name n)]
with Not_found ->
......@@ -2384,14 +2386,14 @@ module Print = struct
List.rev_map (fun (ta,tb) ->
(Xml (tag, prepare ta, prepare tb))
) (Product.get t2);
) (Product.partition any_pair x)
)
) tt.xml u_acc
) (Product.partition any_pair (BoolPair.leafconj tt.xml))
)
) @ u_acc
in
(* arrows *)
let u_acc = prepare_boolvar BoolPair.get (fun x ->
List.map (fun (p,n) ->
let u_acc =
(List.map (fun (p,n) ->
let p = List.fold_left (fun acc (t,s) ->
if is_empty (descr t) then acc else
(prepare (descr t), prepare (descr s)) :: acc) [] p
......@@ -2400,23 +2402,25 @@ module Print = struct
(prepare (descr t), prepare (descr s))) n
in
(Arrows (p,n))
) (Pair.get x)) tt.arrow u_acc
) (Pair.get (BoolPair.leafconj tt.arrow))) @ u_acc
in
(* records *)
let u_acc = prepare_boolvar BoolRec.get (fun x ->
List.map (fun (r,some,none) ->
let u_acc =
(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
)
(Record.get { empty with record =
BoolRec.atom (`Atm (BoolRec.leafconj tt.record)) })
) @ u_acc
in
let u_acc = prepare_boolvar BoolAbstracts.get (fun bdd ->
let l = Abstracts.print bdd in
List.map (fun x -> (Atomic x)) l
) tt.abstract u_acc
let u_acc =
(List.map (fun x -> (Atomic x))
(Abstracts.print (BoolAbstracts.leafconj tt.abstract))
) @ u_acc
in
if tt.absent then assert false; (* is taken care of at the top *)
assert (not tt.absent); (* is taken care of at the top *)
print_topvars positive u_acc
in
let all_printed =
......@@ -2471,7 +2475,7 @@ module Print = struct
and assign_name_rec = function
| Neg t -> assign_name t
| Abs t -> assign_name t
| Name _ | Char _ | Atomic _ -> ()
| Name _ | Char _ | Atomic _ | Display _-> ()
| Regexp r -> assign_name_regexp r
| Pair (t1,t2) -> assign_name t1; assign_name t2
| Intersection l -> List.iter assign_name l
......@@ -2569,6 +2573,7 @@ module Print = struct
| Neg t -> Format.fprintf ppf "Any \\ @[%a@]" (do_print_slot lv_diff) t
| Abs t -> Format.fprintf ppf "?(@[%a@])" (do_print_slot lv_min) t
| Name n -> print_gname ppf n
| Display s -> Format.fprintf ppf "%s" s
| Char c -> Chars.V.print ppf c
| Regexp r -> Format.fprintf ppf "@[[ %a ]@]" (do_print_regexp lv_min) r
| Atomic a -> a ppf
......
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