Better type printer (wip)

types/types.ml

@@ -456,6 +456,7 @@ let no_var t = TLV.no_variables t.toplvars
 let has_tlv t = TLV.has_toplevel t.toplvars
 
 let all_vars t = t.toplvars.TLV.fv
+let all_tlv t = t.toplvars.TLV.tlv
 
 (* XXX this function could be potentially costly. There should be
  * better way to take trace of top level variables in a type *)
@@ -1635,18 +1636,24 @@ struct
       let prepare_boolvar displayvars displayatoms get is_full print tlv bdd =
         List.iter (fun (p,n) ->
           let l1 =
+            let tlv_only = ref true in
             List.fold_left (fun acc -> function
               |(`Var v) as x ->
-                  if displayvars ||  not(TLV.mem (x,true) tlv) then
+                  if not(TLV.mem (x,true) tlv) then begin
+                    tlv_only := false;
                     (Atomic (fun ppf -> Var.print ppf x))::acc
-                  else acc
-              |`Atm bdd -> if displayatoms then (print bdd) @ acc else acc
+                  end else acc
+                  (* the bdd is printed if there one var that is not a tlv var or it
+                   * is not empty . It is not printed if it is full and there are only
+                   * tlv variables or it is empty *)
+              |`Atm bdd when (is_full bdd) && !tlv_only -> acc
+              |`Atm bdd -> print bdd
             ) [] p
           in
           let l2 =
             List.fold_left (fun acc -> function
               |(`Var v) as x ->
-                  if displayvars ||  not(TLV.mem (x,true) tlv) then
+                  if not(TLV.mem (x,true) tlv) then
                     (Atomic (fun ppf -> Format.fprintf ppf "~ %a" Var.print x))::acc
                   else acc
               |`Atm bdd -> assert false
@@ -1660,22 +1667,32 @@ struct
 
 	if (non_empty seq) then add (Regexp (decompile seq));
 
-      let displayatoms = true in
-      let displayvars = TLV.has_toplevel not_seq.toplvars in
-
-      (* base types *)
-      prepare_boolvar displayvars displayatoms BoolIntervals.get (Intervals.equal Intervals.full) (fun bdd ->
-        List.map (fun x -> (Atomic x)) (Intervals.print bdd)
-        ) not_seq.toplvars not_seq.ints;
+      if has_tlv not_seq then begin
+        let l =
+          TLV.Set.fold (fun ((`Var v) as x,p) acc ->
+            let s = 
+              if p then (Atomic (fun ppf -> Var.print ppf x))
+              else (Atomic (fun ppf -> Format.fprintf ppf "~ %a" Var.print x))
+            in s::acc
+          ) (all_tlv not_seq) []
+        in
+        add (Intersection (alloc l))
+      end;
 
+      let displayatoms = true in
       let displayvars = false in
 
+      (* base types *)
       prepare_boolvar displayvars displayatoms BoolChars.get (Chars.equal Chars.full) (fun bdd ->
         match Chars.is_char bdd with
         | Some c -> [(Char c)]
         | None -> List.map (fun x -> (Atomic x)) (Chars.print bdd)
         ) not_seq.toplvars not_seq.chars;
 
+      prepare_boolvar displayvars displayatoms BoolIntervals.get (Intervals.equal Intervals.full) (fun bdd ->
+        List.map (fun x -> (Atomic x)) (Intervals.print bdd)
+        ) not_seq.toplvars not_seq.ints;
+
       let bool =
         Atoms.cup
           (Atoms.atom (Atoms.V.mk_ascii "false"))
@@ -1692,7 +1709,6 @@ struct
           (Pair (prepare t1, prepare t2))
       ) (Product.partition any x)) not_seq.toplvars not_seq.times;
 
-
       (* xml pairs *)
       prepare_boolvar displayvars displayatoms BoolPair.get (Pair.equal Pair.full) (fun x ->
         List.flatten (