Revert "Make distinction between (A ^ Int) and A in TLV"

This reverts commit 045a8519.

types/types.ml

@@ -142,19 +142,18 @@ module TLV = struct
   module Set = struct
     include Set.Make(
       struct
-        (* Var * polarity * if the variable is present in all kinds *)
-        type t = (Var.var * bool * bool)
-        let compare (v1,p1,b1) (v2,p2,b2) =
+        type t = (Var.var * bool)
+        let compare (v1,p1) (v2,p2) =
           let c = Var.compare v1 v2 in
           if c == 0 then
-            if p1 == p2 && b1 = b2 then 0
+            if p1 == p2 then 0
             else if p1 then 1 else -1
           else c
       end)
     let pp_aux ppf pp_elem s = 
       let f ppf = function
-        |(v,true,_) -> Format.fprintf ppf "%a" pp_elem v
-        |(v,false,_) -> Format.fprintf ppf "~ %a" pp_elem v
+        |(v,true) -> Format.fprintf ppf "%a" pp_elem v
+        |(v,false) -> Format.fprintf ppf "~ %a" pp_elem v
       in
       Utils.pp_list ~sep:";" ~delim:("{","}") f ppf (elements s)
     let dump ppf s = pp_aux ppf Var.dump s
@@ -165,42 +164,37 @@ module TLV = struct
 
   (* tlv : top level variables
    * fv : all free variables in the subtree *)
-  type t =  { tlv : Set.t ; fv : Var.Set.t }
+  type t =  { tlv : Set.t ; fv : Var.Set.t; isvar : bool }
 
-  let empty = { tlv = Set.empty ; fv = Var.Set.empty}
-  let any = { tlv = Set.empty ; fv = Var.Set.empty}
+  let empty = { tlv = Set.empty ; fv = Var.Set.empty; isvar = false }
+  let any = { tlv = Set.empty ; fv = Var.Set.empty; isvar = false }
 
-  let singleton (v,p) = { tlv = Set.singleton (v,p,true); fv = Var.Set.singleton v}
+  let singleton (v,p) = { tlv = Set.singleton (v,p); fv = Var.Set.singleton v; isvar = true }
 
   (* return the max of top level variables *)
-  let max x = let (v,p,_) = Set.max_elt x.tlv in (v,p)
+  let max x = Set.max_elt x.tlv
 
   let pair x y = {
     tlv = Set.empty ;
-    fv = Var.Set.union x.fv y.fv
+    fv = Var.Set.union x.fv y.fv ;
+    isvar = false
   }
 
   let record x = {
     tlv = Set.empty ;
-    fv = x.fv
+    fv = x.fv ;
+    isvar = false
   }
 
   (* true if it contains only one variable *)
-  let is_single t = 
-    let (tlvsolo,tlvmix) = Set.partition (fun (_,_,b) -> b) x.tlv in
-    (Set.cardinal tlvsolo = 1) && 
-    (Var.Set.cardinal t.fv = 1) && 
-    (Set.cardinal tlvmix = 0)
+  let is_single t = t.isvar && (Var.Set.cardinal t.fv = 1) && (Set.cardinal t.tlv = 1)
 
   let no_variables t = (Var.Set.cardinal t.fv = 0) && (Set.cardinal t.tlv = 0)
 
   let has_toplevel t = Set.cardinal t.tlv > 0
 
   let pp ppf x = Set.pp ppf x.tlv
-  let dump ppf x = 
-    let (tlvsolo,tlvmix) = Set.partition (fun (_,_,b) -> b) x.tlv in
-    Format.fprintf ppf "<fv = %a ; tlv(mix) = %a ; tlv(solo) = %a>"
-    Var.Set.dump x.fv Set.dump tlvsolo Set.dump tlvmix
+  let dump ppf x = Format.fprintf ppf "<fv = %a ; tlv = %a>" Var.Set.dump x.fv Set.dump x.tlv
   let printf = pp Format.std_formatter
 
   let mem v x = Set.mem v x.tlv
@@ -487,13 +481,13 @@ let update_tlv x y t =
         List.fold_left (fun acc (p,n) ->
           let acc1 =
             List.fold_left (fun acc -> function
-              |(`Var v) as x -> Set.union acc (Set.singleton (x,true,true))
+              |(`Var v) as x -> Set.union acc (Set.singleton (x,true))
               |_ -> acc
             ) Set.empty p
           in
           let acc2 =
             List.fold_left (fun acc -> function
-              |(`Var v) as x -> Set.union acc (Set.singleton (x,false,true))
+              |(`Var v) as x -> Set.union acc (Set.singleton (x,false))
               |_ -> assert false
             ) acc1 n
           in acc2::acc
@@ -504,32 +498,22 @@ let update_tlv x y t =
       |[h] -> h
       |h::l -> List.fold_left Set.union h l
     in
-    let vars = [
-      (aux BoolChars.get t.chars)
+    List.fold_left Set.union
+    (aux BoolChars.get t.chars)
+    [
       (aux BoolIntervals.get t.ints);
       (aux BoolAtoms.get t.atoms);
       (aux BoolPair.get t.arrow);
       (aux BoolPair.get t.xml);
-      (aux BoolRec.get t.record) ]
-    in
-    let (union,inter) =
-      let rec aux (union,inter) = function
-        |[] -> (union,inter)
-        |h :: t -> aux ((Set.union h union),(Set.inter h inter)) t
-      in
-      match vars with
-      |[] -> (Set.empty.Set.empty)
-      |h::t -> aux (h,h) t
-    in
-    let tlvmix = Set.fold (fun (v,p,_) -> (v,p,false)) (Set.diff union inter) in
-    let tlvsolo = inter in
-    Set.union tlvsolo tlvmix
+      (aux BoolRec.get t.record)
+    ]
   in
   let fv t =
     if Descr.is_empty t || equal t Descr.any then Var.Set.empty
     else Var.Set.union x.toplvars.fv y.toplvars.fv
   in
-  { t with toplvars = { tlv = tlv t ; fv = fv t} }
+  let toplvars = { tlv = tlv t ; fv = fv t ; isvar = t.toplvars.isvar } in
+  { t with toplvars = toplvars }
 ;;
 
 let char c = { empty with chars = BoolChars.atom (`Atm c) }
@@ -559,7 +543,8 @@ let cup x y =
       absent= x.absent || y.absent;
       toplvars = TLV.empty
     } in
-    update_tlv x y t
+    let isvar = (is_var x && equal x t) || (is_var y && equal y t) in
+    update_tlv x y { t with toplvars = { t.toplvars with TLV.isvar = isvar }}
 
 let cap x y =
   if x == y then x else
@@ -575,7 +560,8 @@ let cap x y =
       absent= x.absent && y.absent;
       toplvars = TLV.empty
     } in
-    update_tlv x y t
+    let isvar = (is_var x && equal x t) || (is_var y && equal y t) in
+    update_tlv x y { t with toplvars = { t.toplvars with TLV.isvar = isvar }}
 
 let diff x y =
   if x == y then empty else
@@ -591,7 +577,8 @@ let diff x y =
       absent= x.absent && not y.absent;
       toplvars = TLV.empty
     } in
-    update_tlv x y t
+    let isvar = (equal x any && is_var y) || (is_var x && equal y empty) in
+    update_tlv x y { t with toplvars = { t.toplvars with TLV.isvar = isvar }}
 
 (* TODO: optimize disjoint check for boolean combinations *)
 let trivially_disjoint a b =