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

- Introduce an abstract type for precedences used during pretty-printing.

- Change the precedence of the XML constructor to be stronger than the set-theoretic operations (compatibility with previous CDuce)
- Pretty-printing of regular expressions. When the input type contains a sequence type, print the sequence as a regular expression. Do not print empty sequences unless the rest of the atom components is finite:
     `a |`b | `nil
will be printed as
     [] | `a | `b
but
     Atom \ 'a
will be printed as
     Atom \'a
and not
     Atom \ ('a | `nil) | []
- Remove Arrow from positive arrow part (unless it is the only component)
- Fix a bug where records would be printed instead of attributes
parent 83ef66d7
......@@ -1841,7 +1841,7 @@ struct
fill_line (module BoolAbstracts) h (fun t -> t.abstract) (fun t u -> {t with abstract = u }) d;
let h =
try
let no_var = VarTable.find h Var.Set.(empty,empty) in
let no_var = VarTable.find h Key.empty in
let update_field (type s) (module BV : BoolVar.S with type t = s) get set d1 d2 =
let bdd = get d1 in
if BV.(is_empty (diff full bdd)) then set d2 bdd else d2
......@@ -1912,13 +1912,19 @@ struct
merge_columns ((factv, remv,t)::acc) nll
in
let all_descrs = merge_columns [] all_descrs in
let intersection l =
let inter_d l =
match l with
[] -> Neg (alloc [])
| [ p ] -> p
| [ p ; Neg { def = [] } ] -> p
| _ -> Intersection (List.map (fun x -> alloc [x]) l)
in
let inter_nd l =
match l with
[] -> Neg (alloc [])
| [ { 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
......@@ -1937,9 +1943,8 @@ struct
match List.rev ppos, List.rev pneg with
[],[] -> acc
| [],l -> Neg(alloc l) :: acc
| l, [] -> (intersection l) :: acc
| l1,l2 -> (intersection [intersection l1;
Neg(alloc l2)]) :: acc
| l, [] -> (inter_d l) :: acc
| l1,l2 -> (Diff (alloc [inter_d l1], alloc l2)) :: acc
) [] l
in
let print_descr (pvars,nvars) lvars tt =
......@@ -1958,8 +1963,8 @@ struct
match positive_part, negative_part with
[], [] -> []
| [], l -> [ Neg (alloc l) ]
| l, [] -> [ Intersection l ]
| l1, l2 -> [ Diff (alloc [Intersection l1], alloc l2) ]
| l, [] -> [ inter_nd l ]
| l1, l2 -> [ Diff (alloc [inter_nd l1], alloc l2) ]
in
if subtype any tt then print_topvars true [] else
let tt, positive =
......@@ -1967,13 +1972,33 @@ struct
diff any tt, false
else tt , true
in
(* sequence type *)
(* 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 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
if is_empty seq || (is_empty { empty with times = seq.times }
&& not finite_atoms)
then [], tt
else [ (Regexp (decompile seq)) ],
(let d = diff tt seqs_descr in
if finite_atoms then d else
cup d (cap tt nil_type))
else
[], tt
in
......@@ -2036,8 +2061,13 @@ struct
(* 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
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
in
let n = List.rev_map (fun (t,s) ->
(prepare (descr t), prepare (descr s))) n
in
(Arrows (p,n))
) (Pair.get x)) tt.arrow u_acc
in
......@@ -2140,120 +2170,131 @@ struct
Format.fprintf ppf "%s%a" cu Ns.QName.print n
(* operator precedences:
10 names, constants, ...
9 star plus ?
8 seq
7 \ left of \
6 \
5 &
4 | alt
3 <t1 >
2 arrow left of arrow
1 t1 -> t2
20 names, constants, ...
10 : <t1 >
9 : star plus ?
8 : seq
7 : \ left of \
6 : \
5 : &
4 : | alt
3 : should be xml but for compatibility xml is stronger than & | \
2 : arrow left of arrow
1 : arrow
0
We use a private type to force the use of a symbolic name
*)
let opar ppf ~level pri =
if level < pri then Format.fprintf ppf "@[("
module Level : sig
type t = private int
val make : int -> t
end
= struct
type t = int
let make x = x
end
let lv_min = Level.make 0
let lv_arrow = Level.make 1
let lv_larrow = Level.make 2
let _dummy_lv = Level.make 3
let lv_alt = Level.make 4
let lv_and = Level.make 5
let lv_diff = Level.make 6
let lv_ldiff = Level.make 7
let lv_seq = Level.make 8
let lv_post = Level.make 9
let lv_xml = Level.make 10
let lv_max = Level.make 20
let opar ppf ~level (pri : Level.t) =
if Pervasives.(level < pri) then Format.fprintf ppf "@[("
let cpar ppf ~level (pri : Level.t) =
if Pervasives.(level < pri) then Format.fprintf ppf ")@]"
let do_print_list empty pri op pri_op pr_e ppf l =
let rec loop l =
match l with
[] -> ()
| [ h ] -> (pr_e pri_op) ppf h
| h :: t -> Format.fprintf ppf "%a %s@ " (pr_e pri_op) h op; loop t
in
match l with
[] -> Format.fprintf ppf "%s" empty
| [ h ] -> (pr_e pri) ppf h
| _ ->
opar ppf ~level:pri_op pri;
loop l;
cpar ppf ~level:pri_op pri
let cpar ppf ~level pri =
if level < pri then Format.fprintf ppf ")@]"
let rec do_print_slot pri ppf s =
let rec do_print_slot (pri : Level.t) ppf s =
match s.state with
| `Named n -> U.print ppf n
| `GlobalName n -> print_gname ppf n
| _ -> do_print_slot_real pri ppf s.def
and do_print_slot_real pri ppf def =
let rec aux ppf = function
| [] -> assert false
| [ h ] -> (do_print 4) ppf h
| h :: t -> Format.fprintf ppf "%a |@ %a" (do_print 4) h aux t
in
match def with
[] -> Format.fprintf ppf "Empty"
| [ h ] -> do_print pri ppf h
| _ when pri >= 5 -> Format.fprintf ppf "@[(%a)@]" aux def
| _ -> aux ppf def
and do_print_slot_real pri ppf def =
do_print_list "Empty" pri "|" lv_alt do_print ppf def
and do_print pri ppf =
function
| Neg { def = [] } -> Format.fprintf ppf "Any"
| Neg t -> Format.fprintf ppf "Any \\ @[%a@]" (do_print_slot 6) t
| Abs t -> Format.fprintf ppf "?(@[%a@])" (do_print_slot 0) t
| 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
| Char c -> Chars.V.print ppf c
| Regexp r -> Format.fprintf ppf "@[[ %a ]@]" (do_print_regexp 0) r
| Regexp r -> Format.fprintf ppf "@[[ %a ]@]" (do_print_regexp lv_min) r
| Atomic a -> a ppf
| Diff (a, b) ->
opar ppf ~level:6 pri;
Format.fprintf ppf "@[%a@] \\ @[%a@]" (do_print_slot 7) a
(do_print_slot 6) b;
cpar ppf ~level:6 pri
opar ppf ~level:lv_diff pri;
Format.fprintf ppf "@[%a@] \\ @[%a@]" (do_print_slot lv_ldiff) a
(do_print_slot lv_diff) b;
cpar ppf ~level:lv_diff pri
| Intersection [] -> ()
| Intersection [ p ] -> do_print_slot pri ppf p
| Intersection a ->
opar ppf ~level:5 pri;
begin
match a with
[] -> assert false
| [ i ] -> do_print_slot pri ppf i
| h :: t ->
Format.fprintf ppf "%a" (do_print_slot 5) h;
List.iter (fun i -> Format.fprintf ppf " &@ %a" (do_print_slot 5) i) t
end;
cpar ppf ~level:5 pri
| Intersection a -> do_print_list "Any" pri "&" lv_and do_print_slot ppf a
| Pair (t1,t2) ->
Format.fprintf ppf "@[(%a,%a)@]"
(do_print_slot 0) t1
(do_print_slot 0) t2
(do_print_slot lv_min) t1
(do_print_slot lv_min) t2
| Xml (tag,attr,t) ->
opar ppf ~level:3 pri;
opar ppf ~level:lv_xml pri;
Format.fprintf ppf "<%a%a>%a"
do_print_tag tag
do_print_attr attr
(do_print_slot 3) t;
cpar ppf ~level:3 pri;
(do_print_slot lv_xml) t;
cpar ppf ~level:lv_xml pri;
| Record (r,some,none) ->
Format.fprintf ppf "@[{";
do_print_record ppf (r,some,none);
Format.fprintf ppf " }@]"
| Arrows (p,n) ->
if n != [] then opar ppf ~level:6 pri;
(match p with
| [] -> Format.fprintf ppf "Arrow"
| (t,s)::[] ->
let pri = if n == [] then pri else 7 in
Format.fprintf ppf "%a" (do_print_arrow pri) (t,s);
| (t,s)::l ->
Format.fprintf ppf "%a" (do_print_arrow 5) (t,s);
List.iter (fun (t,s) ->
Format.fprintf ppf " &@ %a" (do_print_arrow 5) (t,s)
) l
);
List.iter (fun (t,s) ->
let pri = if n == [] then pri else 6 in
Format.fprintf ppf " \\@ %a" (do_print_arrow pri) (t,s)
) n;
if n != [] then cpar ppf ~level:6 pri
| Arrows (p,[]) ->
do_print_list "Arrow" pri "&" lv_and do_print_arrow ppf p
| Arrows (p, n) ->
opar ppf ~level:lv_diff pri;
do_print_list "Arrow" lv_diff "&" lv_and do_print_arrow ppf p;
Format.fprintf ppf " \\@ ";
do_print_list "##ERROR" lv_diff "|" lv_alt do_print_arrow ppf n;
cpar ppf ~level:lv_diff pri
and do_print_arrow pri ppf (t,s) =
opar ppf ~level:1 pri;
opar ppf ~level:lv_arrow pri;
Format.fprintf ppf "%a -> %a"
(do_print_slot 2) t
(do_print_slot 1) s;
cpar ppf ~level:1 pri
(do_print_slot lv_larrow) t
(do_print_slot lv_arrow) s;
cpar ppf ~level:lv_arrow pri
and do_print_tag ppf = function
| `Tag s -> s ppf
| `Type t -> Format.fprintf ppf "(%a)" (do_print_slot 0) t
| `Type t -> Format.fprintf ppf "(%a)" (do_print_slot lv_min) t
and do_print_attr ppf = function
| { state = `Marked|`Expand|`None;
def = [ Record (r,some,none) ] } -> do_print_record ppf (r,some,none)
| t -> Format.fprintf ppf " (%a)" (do_print_slot 0) t
| t -> Format.fprintf ppf " (%a)" (do_print_slot lv_min) t
and do_print_record ppf (r,some,none) =
List.iter
(fun (l,(o,t)) ->
let opt = if o then "?" else "" in
Format.fprintf ppf "@ @[%a=%s@]%a"
Label.print_attr l opt (do_print_slot 0) t
Label.print_attr l opt (do_print_slot lv_min) t
) (LabelMap.get r);
if not none then Format.fprintf ppf "@ (+others)";
if some then Format.fprintf ppf " ..";
......@@ -2267,29 +2308,29 @@ struct
List.iter (Chars.V.print_in_string ppf) s;
Format.fprintf ppf "'"
| s, Some r ->
opar ppf ~level:8 pri;
opar ppf ~level:lv_seq pri;
Format.fprintf ppf "'";
List.iter (Chars.V.print_in_string ppf) s;
Format.fprintf ppf "' %a" (do_print_regexp 8) r;
cpar ppf ~level:8 pri)
Format.fprintf ppf "' %a" (do_print_regexp lv_seq) r;
cpar ppf ~level:lv_seq pri)
| Pretty.Seq (r1,r2) ->
opar ppf ~level:8 pri;
opar ppf ~level:lv_seq pri;
Format.fprintf ppf "%a@ %a"
(do_print_regexp 8) r1
(do_print_regexp 8) r2;
cpar ppf ~level:8 pri
(do_print_regexp lv_seq) r1
(do_print_regexp lv_seq) r2;
cpar ppf ~level:lv_seq pri
| Pretty.Alt (r,Pretty.Epsilon) | Pretty.Alt (Pretty.Epsilon,r) ->
Format.fprintf ppf "@[%a@]?" (do_print_regexp 9) r
Format.fprintf ppf "@[%a@]?" (do_print_regexp lv_post) r
| Pretty.Alt (r1,r2) ->
opar ppf ~level:4 pri;
opar ppf ~level:lv_alt pri;
Format.fprintf ppf "%a |@ %a"
(do_print_regexp 4) r1
(do_print_regexp 4) r2;
cpar ppf ~level:4 pri
(do_print_regexp lv_alt) r1
(do_print_regexp lv_alt) r2;
cpar ppf ~level:lv_alt pri
| Pretty.Star r ->
Format.fprintf ppf "@[%a@]*" (do_print_regexp 9) r
Format.fprintf ppf "@[%a@]*" (do_print_regexp lv_post) r
| Pretty.Plus r ->
Format.fprintf ppf "@[%a@]+" (do_print_regexp 9) r
Format.fprintf ppf "@[%a@]+" (do_print_regexp lv_post) r
| Pretty.Trans t ->
do_print_slot pri ppf t
and extract_string accu = function
......@@ -2308,17 +2349,17 @@ struct
let t = uniq t in
let t = prepare t in
assign_name t;
Format.fprintf ppf "@[@[%a@]" (do_print_slot 0) t;
Format.fprintf ppf "@[@[%a@]" (do_print_slot lv_min) t;
(match List.rev !to_print with
| [] -> ()
| s::t ->
Format.fprintf ppf
" where@ @[<v>%a = @[%a@]" U.print (get_name s)
(do_print_slot_real 0) s.def;
(do_print_slot_real lv_min) s.def;
List.iter
(fun s ->
Format.fprintf ppf " and@ %a = @[%a@]" U.print
(get_name s) (do_print_slot_real 0) s.def)
(get_name s) (do_print_slot_real lv_min) s.def)
t;
Format.fprintf 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