More work on type pretty printing

types/types.ml

@@ -1584,7 +1584,8 @@ struct
 	else 
         let slot = alloc [] in
         if not (worth_abbrev d) then slot.state <- `Expand;
-	  DescrHash.add memo d slot;
+
+	DescrHash.add memo d slot;
 
 	let (seq,not_seq) =
 	  if (subtype { empty with times = d.times } seqs_descr) then
@@ -1595,25 +1596,26 @@ struct
 
 	let add u = slot.def <- u :: slot.def in
 
-      let prepare_boolvar ?(t=false) get print tlv bdd =
+      let prepare_boolvar ?(displayvars=false) ?(displayatoms=true) get is_full print tlv bdd =
         List.iter (fun (p,n) ->
           let l1 = 
             List.fold_left (fun acc -> function
-              |(`Var v) as x -> 
-                  begin match (t, (TLV.mem (x,true) tlv)) with
-                  |(true,true)
-                  |(_,false) -> (Atomic (fun ppf -> Var.print ppf x))::acc
-                  |(false,true) -> acc end
-              |`Atm bdd -> (print bdd) @ acc
+              |(`Var v) as x ->
+                  begin match (displayvars, (TLV.mem (x,true) tlv)) with
+                  |(true,true) |(_,false) -> (Atomic (fun ppf -> Var.print ppf x))::acc
+                  |(_,_) -> acc 
+                  end
+              |`Atm bdd -> if displayatoms then (print bdd) @ acc else acc
             ) [] p
           in
           let l2 =
             List.fold_left (fun acc -> function
               |(`Var v) as x ->
-                  begin match (t, (TLV.mem (x,false) tlv)) with
-                  |(true,true)
-                  |(_,false) -> (Atomic (fun ppf -> Format.fprintf ppf "~ %a" Var.print x))::acc
-                  |(false,true) -> acc end
+                  begin match (displayvars, (TLV.mem (x,false) tlv)) with
+                  |(true,true) |(_,false) ->
+                      (Atomic (fun ppf -> Format.fprintf ppf "~ %a" Var.print x))::acc
+                  |(_,_) -> acc 
+                  end
               |`Atm bdd -> assert false
             ) [] n
           in
@@ -1625,30 +1627,33 @@ struct
 
 	if (non_empty seq) then add (Regexp (decompile seq));
 
+      let displayatoms = TLV.no_toplevel not_seq.toplvars in
+      let displayvars = true in
+
       (* base types *)
-      prepare_boolvar ~t:true BoolIntervals.get (fun x -> 
+      prepare_boolvar ~displayvars ~displayatoms BoolIntervals.get (Intervals.equal Intervals.full) (fun x -> 
         List.map (fun x -> (Atomic x)) (Intervals.print x)
         ) not_seq.toplvars not_seq.ints;
 
-      prepare_boolvar BoolChars.get (fun x ->
+      prepare_boolvar ~displayatoms BoolChars.get (Chars.equal Chars.full) (fun x ->
         match Chars.is_char x with 
         | Some c -> [(Char c)]
         | None -> List.map (fun x -> (Atomic x)) (Chars.print x)
         ) not_seq.toplvars not_seq.chars;
 
-      prepare_boolvar BoolAtoms.get (fun x ->
+      prepare_boolvar ~displayatoms BoolAtoms.get (Atoms.equal Atoms.full) (fun x ->
         List.map (fun x -> (Atomic x)) (Atoms.print x)
         ) not_seq.toplvars not_seq.atoms;
 
       (* pairs *)
-      prepare_boolvar BoolPair.get (fun x ->
+      prepare_boolvar ~displayatoms BoolPair.get (Pair.equal Pair.full) (fun x ->
         List.map (fun (t1,t2) ->
           (Pair (prepare t1, prepare t2))
       ) (Product.partition any x)) not_seq.toplvars not_seq.times;
 
 
       (* xml pairs *)
-      prepare_boolvar BoolPair.get (fun x ->
+      prepare_boolvar ~displayatoms BoolPair.get (Pair.equal Pair.full) (fun x ->
         List.flatten (
           List.map (fun (t1,t2) ->
             try let n = DescrPairMap.find (t1,t2) !named_xml in [(Name n)]
@@ -1666,7 +1671,7 @@ struct
         )) not_seq.toplvars not_seq.xml;
 
       (* arrows *)
-      prepare_boolvar BoolPair.get (fun x ->
+      prepare_boolvar ~displayatoms BoolPair.get (Pair.equal Pair.full) (fun x ->
         List.map (fun (p,n) ->
            let aux (t,s) = prepare (descr t), prepare (descr s) in
            let p = List.map aux p and n = List.map aux n in