Commit ae31d5c7 authored by Kim Nguyễn's avatar Kim Nguyễn

Further simplification of the pretty-printing code.

parent 8097d14b
...@@ -2019,6 +2019,66 @@ module Print = struct ...@@ -2019,6 +2019,66 @@ module Print = struct
(Atoms.atom (Atoms.V.mk_ascii "true")))) (Atoms.atom (Atoms.V.mk_ascii "true"))))
) )
(** pretty-printers for each kind, without top-level variables *)
let print_seq finite_atoms decompile acc tt =
let tt_times = VarTimes.(inj (proj tt)) in
if subtype tt_times seqs_descr && proper_seq tt_times then
let seq = cap tt seqs_descr in
let seq_times = VarTimes.(update Descr.empty (proj seq)) in
if is_empty seq || (is_empty seq_times && not finite_atoms) then
acc, tt
else
let tt =
let d = diff tt seqs_descr in
if finite_atoms then d
else cup d (cap tt nil_type)
in
(Regexp (decompile seq)) :: acc, tt
else
[], tt
let print_chars acc tt =
(* use fold_right to preserve order... see if that + the List.rev
at the end cancel nicely *)
List.fold_right (fun x acc -> (Atomic x) :: acc)
(Chars.print (VarChars.(leafconj (proj tt))))
acc
let print_ints acc tt =
List.fold_right (fun x acc -> (Atomic x) :: acc)
(Intervals.print (VarIntervals.(leafconj (proj tt))))
acc
let print_atoms acc tt =
(* We need this complex bit because Atoms.print does not know about
the precedence of outer operators *)
let pr_atoms acc 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
) acc l
in
match Atoms.extract (VarAtoms.(leafconj (proj tt))) with
`Finite l -> pr_atoms acc l
| `Cofinite [] -> (Display "Atom") :: acc
| `Cofinite l -> (Diff (alloc[Display "Atom"],
alloc (pr_atoms [] l))) :: acc
(** [prepare d] massages a type and convert it to the syntactic form. (** [prepare d] massages a type and convert it to the syntactic form.
Rough algorithm: Rough algorithm:
- check whether [d] has been memoized (recursive types) - check whether [d] has been memoized (recursive types)
...@@ -2038,6 +2098,8 @@ module Print = struct ...@@ -2038,6 +2098,8 @@ module Print = struct
- if an atomic type is finite and contains the atoms `false and `true - if an atomic type is finite and contains the atoms `false and `true
then write it has Bool. then write it has Bool.
*) *)
let rec prepare d = let rec prepare d =
let d = lookup d in let d = lookup d in
try DescrHash.find memo d try DescrHash.find memo d
...@@ -2229,63 +2291,23 @@ module Print = struct ...@@ -2229,63 +2291,23 @@ module Print = struct
(* sequence type. We do not want to split types such as (* sequence type. We do not want to split types such as
Any into Any \ [ Any *] | Any, and likewise, write Any into Any \ [ Any *] | Any, and likewise, write
Atom \ [] | []. *) Atom \ [] | []. *)
let finite_atoms = Atoms.is_finite (VarAtoms.leafconj tt.atoms) in let finite_atoms = Atoms.is_finite VarAtoms.(leafconj (proj tt)) in
let u_acc, tt =
let tt_times = VarTimes.(inj (proj tt)) in
if subtype tt_times seqs_descr && proper_seq tt_times then
let seq = cap tt seqs_descr in
let seq_times = VarTimes.(update Descr.empty (proj seq)) in
if is_empty seq || (is_empty seq_times && not finite_atoms) then
[], tt
else
let tt =
let d = diff tt seqs_descr in
if finite_atoms then d
else cup d (cap tt nil_type)
in
[ (Regexp (decompile seq)) ], tt
else
[], tt
in
(* base types *) let u_acc, tt = print_seq finite_atoms decompile [] tt in
let u_acc =
(List.map (fun x -> Atomic x) (Chars.print (VarChars.leafconj tt.chars))) (* basic types *)
@ u_acc let u_acc = print_chars u_acc tt in
in let u_acc = print_ints u_acc tt in
let u_acc =
(List.map (fun x -> (Atomic x)) (Intervals.print (VarIntervals.leafconj tt.ints))) (* display the Bool type explicitely if present *)
@ u_acc
in
let u_acc, tt = if finite_atoms && subtype bool_type tt then let u_acc, tt = if finite_atoms && subtype bool_type tt then
(Display "Bool") :: u_acc, (Display "Bool") :: u_acc,
diff tt bool_type diff tt bool_type
else else
u_acc, tt u_acc, tt
in in
let pr_atoms l = let u_acc = print_atoms u_acc tt in
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 (VarAtoms.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 *) (* pairs *)
let u_acc = let u_acc =
List.fold_left (fun acc (t1,t2) -> List.fold_left (fun acc (t1,t2) ->
...@@ -2301,7 +2323,7 @@ module Print = struct ...@@ -2301,7 +2323,7 @@ module Print = struct
try let n = DescrPairMap.find (t1,t2) !named_xml in [(Name n)] try let n = DescrPairMap.find (t1,t2) !named_xml in [(Name n)]
with Not_found -> with Not_found ->
let tag = let tag =
match Atoms.print_tag (VarAtoms.leafconj t1.atoms) with match Atoms.print_tag (VarAtoms.(leafconj (proj t1))) with
Some a when is_empty (VarAtoms.(update t1 empty)) -> `Tag a Some a when is_empty (VarAtoms.(update t1 empty)) -> `Tag a
| _ -> `Type (prepare t1) | _ -> `Type (prepare t1)
in in
...@@ -2343,7 +2365,6 @@ module Print = struct ...@@ -2343,7 +2365,6 @@ module Print = struct
(Abstracts.print (VarAbstracts.leafconj tt.abstract)) (Abstracts.print (VarAbstracts.leafconj tt.abstract))
) @ u_acc ) @ u_acc
in in
assert (not tt.absent); (* is taken care of at the top *)
print_topvars positive u_acc print_topvars positive u_acc
in in
let all_printed = let all_printed =
...@@ -2359,7 +2380,7 @@ module Print = struct ...@@ -2359,7 +2380,7 @@ module Print = struct
let tr = Product.merge_same_first tr in let tr = Product.merge_same_first tr in
let tr = Product.clean_normal tr in let tr = Product.clean_normal tr in
let eps = Atoms.contains nil_atom (VarAtoms.leafconj t.atoms) in let eps = Atoms.contains nil_atom (VarAtoms.(leafconj (proj t))) in
let tr_cons = List.map (fun (li,ti) -> (cons li, cons ti)) tr in let tr_cons = List.map (fun (li,ti) -> (cons li, cons ti)) tr in
try try
...@@ -2391,7 +2412,7 @@ module Print = struct ...@@ -2391,7 +2412,7 @@ module Print = struct
let g = !gen in let g = !gen in
s.state <- `Marked; s.state <- `Marked;
List.iter assign_name_rec s.def; List.iter assign_name_rec s.def;
(* + 8 allows to disable sharing for small subtrees *) (* + 8 disables sharing for small subtrees *)
if (s.state == `Marked) && (!gen < g + 8) then s.state <- `None if (s.state == `Marked) && (!gen < g + 8) then s.state <- `None
| `Marked -> s.state <- `Named (name ()); to_print := s :: !to_print | `Marked -> s.state <- `Named (name ()); to_print := s :: !to_print
| _ -> () | _ -> ()
......
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