Commit 16ea487d authored by Kim Nguyễn's avatar Kim Nguyễn

Start work on simplifying the pretty-printer.

parent e8ecd949
......@@ -110,6 +110,10 @@ let contains_sample s t =
| Some (ns, None),_ -> is_empty (diff (any_in_ns ns) t)
let trivially_disjoint = disjoint
let is_finite m =
match get m with
`Finite _ -> true
| _ -> false
let compute ~empty ~full ~cup ~cap ~diff ~atom b = assert false
let get _ = assert false
......
......@@ -36,7 +36,7 @@ val single : t -> V.t
type sample = (Ns.Uri.t * Ns.Label.t option) option
val sample : t -> sample
val contains_sample: sample -> t -> bool
val is_finite : t -> bool
type 'a map
val mk_map: (t * 'a) list -> 'a map
val get_map: V.t -> 'a map -> 'a
......
......@@ -2074,6 +2074,25 @@ module Print = struct
in
loop t
(** [prepare d] massages a type and convert it to the syntactic form.
Rough algorithm:
- check whether [d] has been memoized (recursive types)
- check whether [d] has a toplevel name
- check whether [d] may be absent (as part of a record field)
- check whether [d] needs to be expanded (i.e. isn't a trivially
empty or full pair or record
- for each kind (Atoms, Integers, Chars, Products, …) composing the type:
- Check whether the type is worth complementing (that is write
(Any \ Int) rather than (Arrow | Char | Atoms | ...)
- Separate and factorize toplevel variables (so that
'a&'b&Int | 'b&Int is written as 'b&Int.
- Print out the toplevel variables present in all kinds
- Print for each kind the top-level variables and the variable-less part.
- special case for products and atoms:
- products that are sequence types are written as regular expressions
- if an atomic type is finite and contains the atoms `false and `true
then write it has Bool.
*)
let rec prepare d =
let d = lookup d in
try DescrHash.find memo d
......@@ -2289,17 +2308,7 @@ module Print = struct
(* sequence type. We do not want to split types such as
Any into Any \ [ Any *] | Any, and likewise, write
Atom \ [] | []. *)
let finite_atoms =
try match BoolAtoms.get tt.atoms with
| [ ( [ `Atm bdd ], [] ) ] ->
let res =
match Atoms.sample bdd with
|None -> false
| _ -> true
in res
| _ -> false
with Not_found -> true
in
let finite_atoms = Atoms.is_finite (BoolAtoms.leafconj tt.atoms) in
let u_acc, tt =
let tt_times = { empty with times = tt.times } in
if subtype tt_times seqs_descr && proper_seq tt_times then
......@@ -2334,18 +2343,24 @@ module Print = struct
in
let bool =
Atoms.cup
(Atoms.atom (Atoms.V.mk_ascii "false"))
(Atoms.atom (Atoms.V.mk_ascii "true"))
{ empty with atoms = BoolAtoms.atom
(`Atm(Atoms.cup
(Atoms.atom (Atoms.V.mk_ascii "false"))
(Atoms.atom (Atoms.V.mk_ascii "true"))))
}
in
let u_acc, tt = if finite_atoms &&
subtype bool tt
then
Atomic (fun ppf -> Format.fprintf ppf "Bool") :: u_acc,
diff tt bool
else
u_acc, tt
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")]
| l -> List.map (fun x -> (Atomic x)) l
) tt.atoms u_acc
List.map (fun x -> (Atomic x)) (Atoms.print bdd)
) tt.atoms u_acc
in
(* pairs *)
let u_acc = prepare_boolvar BoolPair.get (fun x ->
List.rev_map (fun (t1,t2) ->
......
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