Add delta to Positive.clean_type and Tallying.norm

tests/libtest/tallyingTest.ml

@@ -39,8 +39,8 @@ and vv = V of string
 let mk_s ll =
   let aux l =
     List.fold_left (fun acc -> function
-      |P(V alpha,t) -> Tallying.CS.M.add ((*true,*)Var.mk alpha) (Types.empty,parse_typ t) acc
-      |N(t,V alpha) -> Tallying.CS.M.add ((*false,*)Var.mk alpha) (parse_typ t,Types.any) acc
+      |P(V alpha,t) -> Tallying.CS.M.add Var.Set.empty (Var.mk alpha) (Types.empty,parse_typ t) acc
+      |N(t,V alpha) -> Tallying.CS.M.add Var.Set.empty (Var.mk alpha) (parse_typ t,Types.any) acc
     ) Tallying.CS.M.empty l
   in
   List.fold_left (fun acc l ->
@@ -50,8 +50,8 @@ let mk_s ll =
 let mk_union_res l1 l2 =
   let aux l =
     List.fold_left (fun acc -> function
-      |P(V v,s) -> Tallying.CS.M.merge acc (Tallying.CS.M.singleton (Var.mk v) (Types.empty, parse_typ s))
-      |N(s,V v) -> Tallying.CS.M.merge acc (Tallying.CS.M.singleton (Var.mk v) (parse_typ s, Types.any))
+      |P(V v,s) -> Tallying.CS.M.inter Var.Set.empty acc (Tallying.CS.M.singleton (Var.mk v) (Types.empty, parse_typ s))
+      |N(s,V v) -> Tallying.CS.M.inter Var.Set.empty acc (Tallying.CS.M.singleton (Var.mk v) (parse_typ s, Types.any))
     ) Tallying.CS.M.empty l
   in
   match l1,l2 with
@@ -62,12 +62,12 @@ let mk_union_res l1 l2 =
 
 (* check invariants on the constraints sets *)
 let mk_pp = function
-  |P(V alpha,t) -> Tallying.CS.singleton (Tallying.Pos (Var.mk alpha,parse_typ t))
-  |N(t,V alpha) -> Tallying.CS.singleton (Tallying.Neg (parse_typ t,Var.mk alpha))
+  |P(V alpha,t) -> Tallying.CS.singleton Var.Set.empty (Tallying.Pos (Var.mk alpha,parse_typ t))
+  |N(t,V alpha) -> Tallying.CS.singleton Var.Set.empty (Tallying.Neg (parse_typ t,Var.mk alpha))
 
 let mk_prod l =
     List.fold_left (fun acc c ->
-      Tallying.CS.prod (mk_pp c) acc
+      Tallying.CS.prod Var.Set.empty (mk_pp c) acc
     ) Tallying.CS.sat l
 
 let mk_union l1 l2 =

types/boolVar.mli

+module type E = sig
+  type elem
+  include Custom.T
+
+  val empty : t
+  val full  : t
+  val cup   : t -> t -> t
+  val cap   : t -> t -> t
+  val diff  : t -> t -> t
+  val atom  : elem -> t
+
+end
+
+module type S = sig
+
+  type s
+  type elem = s Var.pairvar
+  include Custom.T
+
+  (** returns the union of all leaves in the BDD *)
+  val leafconj: t -> s
+
+  val get: t -> (elem list * elem list) list
+
+  val empty : t
+  val full  : t
+  (* same as full, but we keep it for the moment to avoid chaging the code everywhere *)
+  val any  : t
+  val cup   : t -> t -> t
+  val cap   : t -> t -> t
+  val diff  : t -> t -> t
+  val atom  : elem -> t
+
+  val trivially_disjoint: t -> t -> bool
+
+  (** vars a : return a bdd that is ( Any ^ Var a ) *)
+  val vars  : Var.var -> t
+
+  val iter: (elem-> unit) -> t -> unit
+
+  val compute: empty:'b -> full:'b -> cup:('b -> 'b -> 'b)
+    -> cap:('b -> 'b -> 'b) -> diff:('b -> 'b -> 'b) ->
+    atom:(elem -> 'b) -> t -> 'b
+
+  val is_empty : t -> bool
+
+  val pp_print : Format.formatter -> t -> unit
+
+  val print : ?f:(Format.formatter -> elem -> unit) -> t -> (Format.formatter -> unit) list
+
+end
+
+module type MAKE = functor (T : E) -> S with type s = T.t
+module Make : MAKE 

types/types.ml

@@ -295,7 +295,7 @@ struct
     ints  = BoolIntervals.full;
     atoms = BoolAtoms.full;
     chars = BoolChars.full;
-    abstract = BoolAbstracts.any;
+    abstract = BoolAbstracts.full;
     absent= false;
     toplvars = TLV.any
   }
@@ -466,7 +466,7 @@ let var a =  {
   ints  = BoolIntervals.vars a;
   atoms = BoolAtoms.vars a;
   chars = BoolChars.vars a;
-  abstract = BoolAbstracts.empty;
+  abstract = BoolAbstracts.vars a;
   absent= false;
   toplvars = TLV.singleton (a,true)
 }
@@ -1919,7 +1919,11 @@ struct
           (Record (r,some,none))
       ) (Record.get { empty with record = BoolRec.atom (`Atm x) })) not_seq.toplvars not_seq.record;
 
-	List.iter (fun x -> add (Atomic x)) (BoolAbstracts.print not_seq.abstract);
+      prepare_boolvar BoolAbstracts.get (Abstracts.equal Abstracts.full) (fun bdd ->
+        match Abstracts.print bdd with
+        |[x] -> [Atomic x]
+        |l -> [Union(alloc (List.map (fun x -> (Atomic x)) l))]
+      ) not_seq.toplvars not_seq.abstract;
 
 	if not_seq.absent then add (Atomic (fun ppf -> Format.fprintf ppf "#ABSENT"));
 	slot.def <- List.rev slot.def;
@@ -2729,6 +2733,8 @@ module Tallying = struct
     |Pos of (Var.var * s) (** alpha <= t | alpha \in P *)
     |Neg of (s * Var.var) (** t <= alpha | alpha \in N *)
 
+  exception UnSatConstr of string
+
   module CS = struct
 
     (* we require that types are semantically equivalent and not structurally
@@ -2749,18 +2755,7 @@ module Tallying = struct
       module VarMap =  Map.Make(Key)
       type t = (Descr.s * Descr.s) VarMap.t
       let singleton = VarMap.singleton
-      let empty = VarMap.empty
       let cardinal = VarMap.cardinal
-      let add v (inf, sup) map =
-        let new_i, new_s =
-          try
-            let old_i, old_s = VarMap.find v map in
-            cup old_i inf,
-            cap old_s sup
-          with
-            Not_found -> inf, sup
-        in
-        VarMap.add v (new_i, new_s) map
 
       (* a set of constraints m1 subsumes a set of constraints m2,
          that is the solutions for m1 contains all the solutions for
@@ -2768,7 +2763,6 @@ module Tallying = struct
          forall i1 <= v <= s1 in m1,
          there exists i2 <= v <= s2 in m2 such that i1 <= i2 <= v <= s2 <= s1
       *)
-
       let subsumes map1 map2 =
         VarMap.for_all (fun v (i1, s1) ->
           try let i2, s2 = VarMap.find v map2 in
@@ -2787,9 +2781,27 @@ module Tallying = struct
           if c == 0 then semantic_compare s1 s2
           else c) map1 map2
 
-      let inter map1 map2 = VarMap.fold add map1 map2
+      let add delta v (inf, sup) map =
+        let new_i, new_s =
+          try
+            let old_i, old_s = VarMap.find v map in
+            cup old_i inf,
+            cap old_s sup
+          with
+            Not_found -> inf, sup
+        in
+        if Var.Set.mem v delta then
+          if ((equal inf empty) && (equal sup any)) || 
+             (equal (var v) inf && equal (var v) sup) then
+               map
+          else
+            raise (UnSatConstr (Format.sprintf "%s is a monomorphic variable" (Utils.string_of_formatter Var.pp v)))
+        else
+          VarMap.add v (new_i, new_s) map
+
+      let inter delta map1 map2 = VarMap.fold (add delta) map1 map2
       let fold = VarMap.fold
-      let merge = inter
+      let empty = VarMap.empty
 
     end
 
@@ -2890,7 +2902,7 @@ module Tallying = struct
           loop s1 s2 []
 
       (* Square intersection *)
-      let inter s1 s2 =
+      let inter delta s1 s2 =
         match s1,s2 with
           [], _ | _, [] -> []
         | _ ->
@@ -2906,7 +2918,7 @@ module Tallying = struct
             fold (fun m2 acc2 ->
               let merged = if M.subsumes m1 m2 then m2
                 else if M.subsumes m2 m1 then m1
-                else M.inter m1 m2
+                else M.inter delta m1 m2
               in
               add merged acc2
             )
@@ -2929,9 +2941,19 @@ module Tallying = struct
 
     type sl = sigma list
 
-    let singleton = function
-      |Pos (v,s) -> S.singleton (M.singleton v (empty,s))
-      |Neg (s,v) -> S.singleton (M.singleton v (s,any))
+    let singleton delta = function
+      |Pos (v,s) ->
+          if Var.Set.mem v delta then
+            if equal s any || equal (var v) s then S.singleton M.empty
+            else raise (UnSatConstr (Format.sprintf "%s is a monomorphic variable" (Utils.string_of_formatter Var.pp v)))
+          else
+            S.singleton (M.singleton v (empty,s))
+      |Neg (s,v) ->
+          if Var.Set.mem v delta then
+            if equal s any || equal (var v) s then S.singleton M.empty
+            else raise (UnSatConstr (Format.sprintf "%s is a monomorphic variable" (Utils.string_of_formatter Var.pp v)))
+          else
+            S.singleton (M.singleton v (s,any))
 
     let pp_s = S.pp
     let pp_m = M.pp
@@ -2942,9 +2964,8 @@ module Tallying = struct
     let unsat = S.empty
 
     let union = S.union
-
-    let prod = S.inter
-    let merge = M.inter
+    let prod delta = S.inter delta
+    let merge delta = M.inter delta 
   end
 
   let normatoms (t,_,_) = if Atoms.is_empty t then CS.sat else CS.unsat
@@ -2986,31 +3007,31 @@ module Tallying = struct
   let toplevel delta single norm_rec mem p n = match (p,n) with
     |([],(`Var x)::neg) ->
         let t = single (false,x,[],neg) in
-        CS.singleton (Neg (t,`Var x))
+        CS.singleton delta (Neg (t,`Var x))
 
     |((`Var x)::pos,[]) ->
         let t = single (true,x,pos,[]) in
-        CS.singleton (Pos (`Var x,t))
+        CS.singleton delta (Pos (`Var x,t))
 
     |((`Var x)::pos, (`Var y)::neg) ->
         if Var.compare (`Var x) (`Var y) < 0 then
           let t = single (true,x,pos,n) in
-          CS.singleton (Pos (`Var x,t))
+          CS.singleton delta (Pos (`Var x,t))
         else
           let t = single (false,y,p,neg) in
-          CS.singleton (Neg (t,`Var y))
+          CS.singleton delta (Neg (t,`Var y))
 
     |([`Atm a], (`Var x)::neg) ->
         let t = single (false,x,p,neg) in
-        CS.singleton (Neg (t,`Var x))
+        CS.singleton delta (Neg (t,`Var x))
 
     |([`Atm t], []) -> norm_rec (t,delta,mem)
     |_,_ -> assert false
 
-  let big_prod f acc l =
+  let big_prod delta f acc l =
     List.fold_left (fun acc (pos,neg) ->
       (* if CS.S.is_empty acc then acc else *)
-        CS.prod acc (f pos neg)
+        CS.prod delta acc (f pos neg)
     ) acc l
 
   (* norm generates a constraint set for the costraint t <= 0 *)
@@ -3025,12 +3046,12 @@ module Tallying = struct
       else if is_var t then
         let (v,p) = TLV.max t.toplvars in
         let s = if p then (Pos (v,empty)) else (Neg (any,v)) in
-        CS.singleton s
+        CS.singleton delta s
       (* if there are no vars, and it is not empty then unsat *)
       else if no_var t then CS.unsat
       else begin
         let mem = DescrSet.add t mem in
-        let aux single norm_aux acc l = big_prod (toplevel delta single norm_aux mem) acc l in
+        let aux single norm_aux acc l = big_prod delta (toplevel delta single norm_aux mem) acc l in
 
         let acc = aux single_atoms normatoms CS.sat (BoolAtoms.get t.atoms) in
         let acc = aux single_chars normchars acc (BoolChars.get t.chars) in
@@ -3068,7 +3089,7 @@ module Tallying = struct
             let con20 = aux t1 z2 rest in
             let con11 = CS.union con1 con10 in
             let con22 = CS.union con2 con20 in
-            CS.prod con11 con22
+            CS.prod delta con11 con22
         end
       in
       (* cap_product return the intersection of all (fst pos,snd pos) *)
@@ -3078,7 +3099,7 @@ module Tallying = struct
       let con0 = aux t1 t2 neg in
       CS.union (CS.union con1 con2) con0
     in
-    big_prod norm_prod CS.sat (Pair.get t)
+    big_prod delta norm_prod CS.sat (Pair.get t)
 
   and normrec (t,delta,mem) =
     let norm_rec ((oleft,left),rights) =
@@ -3090,15 +3111,15 @@ module Tallying = struct
             snd (Array.fold_left (fun (i,acc) t ->
               let di = diff accus.(i) t in
               let accus' = Array.copy accus in accus'.(i) <- di ;
-              (i+1,CS.prod acc (CS.prod (norm (di,delta,mem)) (aux accus' [] right)))
+              (i+1,CS.prod delta acc (CS.prod delta (norm (di,delta,mem)) (aux accus' [] right)))
             ) (0,CS.sat) field
             )
       in
       let c = Array.fold_left (fun acc t -> CS.union (norm (t,delta,mem)) acc) CS.sat left in
-      CS.prod (aux left [] rights) c
+      CS.prod delta (aux left [] rights) c
     in
     List.fold_left (fun acc (_,p,n) ->
-      if CS.S.is_empty acc then acc else CS.prod acc (norm_rec (p,n))
+      if CS.S.is_empty acc then acc else CS.prod delta acc (norm_rec (p,n))
     ) CS.sat (get_record t)
 
   (* arrow(p,{t1 -> t2}) = [t1] v arrow'(t1,any \ t2,p)
@@ -3134,9 +3155,9 @@ module Tallying = struct
           let con20 = aux t1 acc1 p in
           let con11 = CS.union con1 con10 in
           let con22 = CS.union con2 con20 in
-          CS.prod con11 con22
+          CS.prod delta con11 con22
     in
-    big_prod norm_arrow CS.sat (Pair.get t)
+    big_prod delta norm_arrow CS.sat (Pair.get t)
 
   let memo_norm = DescrHash.create 17
   (* XXX here I hash over a set . this might lead to a 
@@ -3148,8 +3169,6 @@ module Tallying = struct
       DescrHash.add memo_norm t res; res
     end
 
-  exception UnSatConstr of string
-
   let rec merge (m,delta,mem) =
     let res =
       CS.M.fold (fun v (inf, sup) acc ->
@@ -3163,7 +3182,7 @@ module Tallying = struct
             let n =
               let n = norm delta x in if CS.S.is_empty n then raise (UnSatConstr "merge2") else n
             in
-            let c1 = CS.prod (CS.S.singleton m) n in
+            let c1 = CS.prod delta (CS.S.singleton m) n in
             let c2 = CS.S.fold (fun m1 acc -> CS.union acc (merge (m1,delta,mem))) c1 CS.S.empty in
             CS.union c2 acc
           end) m CS.S.empty
@@ -3239,7 +3258,7 @@ module Tallying = struct
         let d = diff s t in
         if is_empty d then CS.sat
         else if no_var d then CS.unsat
-        else CS.prod acc (norm delta d)
+        else CS.prod delta acc (norm delta d)
       ) CS.sat l
     in
     if Pervasives.(n = CS.unsat) then raise Step1Fail else
@@ -3335,24 +3354,16 @@ let set a i v =
   end
 let get a i = if i < 0 then any else (!a).(i)
 
-exception FoundSquareSub of Tallying.CS.sl * bool
+exception FoundSquareSub of Tallying.CS.sl
 
 let squaresubtype delta s t =
   DescrHash.clear Tallying.memo_norm;
-(*  assert (Var.Set.is_empty (Var.Set.diff (all_vars t) delta)); *)
   let ai = ref [| |] in
   let tallying i =
     try
       let s = get ai i in
       let sl = Tallying.tallying ~delta [ (s,t) ] in
-      let ss =
-        Positive.clean_type delta (
-          List.fold_left (fun acc si ->
-              cap acc (Tallying.(s $$ si))
-          ) any sl
-        )
-      in
-      raise (FoundSquareSub(sl,subtype ss t))
+      raise (FoundSquareSub sl)
     with
       Tallying.Step1Fail -> (assert (i == 0); raise (Tallying.UnSatConstr "apply_raw step1"))
     | Tallying.Step2Fail -> () (* continue *)
@@ -3364,17 +3375,14 @@ let squaresubtype delta s t =
         else (cap (Positive.substitutefree delta s) (get ai (i-1)))
       in
       set ai i ss;
-      (*
-      Format.printf "Starting expansion %i @\n@." i;
-      Format.printf "%a < %a\n@." Print.print ss Print.print t;
-      *)
       tallying i;
       loop (i+1)
-    with FoundSquareSub (sl,res) -> sl, res
+    with FoundSquareSub sl -> sl
   in
   loop 0
 
-let is_squaresubtype delta s t = snd(squaresubtype delta s t)
+let is_squaresubtype delta s t =
+  try ignore(squaresubtype delta s t);true with Tallying.UnSatConstr _ -> false
 
 exception FoundApply of t * int * int * Tallying.CS.sl
 

types/types.mli

@@ -164,11 +164,11 @@ module Positive : sig
   val times: v -> v -> v
   val xml: v -> v -> v
 
-  (* val decompose : t -> v *)
   val substitute : t -> (Var.var * t) -> t
   val substituterec : t -> Var.var -> t
   val solve: v -> Node.t
   val substitutefree : Var.Set.t -> t -> t
+  val clean_type : Var.Set.t -> t -> t
 end
 
 (** Normalization **)
@@ -203,7 +203,6 @@ module Product : sig
   val need_second: t -> bool
     (* Is there more than a single rectangle ? *)
 
-
   val clean_normal: t -> t
     (* Merge rectangles with same second component *)
 end
@@ -383,10 +382,10 @@ module Tallying : sig
       type t
       val compare  : t -> t -> int
       val empty : t
-      val add : key -> descr*descr -> t -> t
+      val add : Var.Set.t -> key -> descr*descr -> t -> t
       val singleton : key -> descr*descr -> t
       val pp : Format.formatter -> t -> unit
-      val merge : t -> t -> t
+      val inter : Var.Set.t -> t -> t -> t
     end
     module E : sig
       include Map.S with type key = Var.var
@@ -418,12 +417,12 @@ module Tallying : sig
     val pp_e  : Format.formatter -> sigma -> unit
     val pp_sl : Format.formatter -> sl -> unit
 
-    val merge : m -> m -> m
-    val singleton : constr -> s
+    (* val merge : m -> m -> m *)
+    val singleton : Var.Set.t -> constr -> s
     val sat : s
     val unsat : s
     val union : s -> s -> s
-    val prod : s -> s -> s
+    val prod : Var.Set.t -> s -> s -> s
   end
 
   val norm : Var.Set.t -> t -> CS.s
@@ -458,7 +457,7 @@ end
 (** Square Subtype relation. [squaresubtype delta s t] . 
     True if there exists a substitution such that s < t only 
     considering variables that are not in delta *)
-val squaresubtype : Var.Set.t -> t -> t -> (Tallying.CS.sl * bool)
+val squaresubtype : Var.Set.t -> t -> t -> Tallying.CS.sl
 val is_squaresubtype : Var.Set.t -> t -> t -> bool
 
 (** apply_raw s t returns the 4-tuple (subst,ss, tt, res) where

typing/typer.ml

@@ -912,7 +912,7 @@ and type_check' loc env ed constr precise = match ed with
           if not (Types.subtype t1 acc) then
             raise_loc loc (NonExhaustive (Types.diff t1 acc));
           let t = type_check_branches loc env t1 a.fun_body t2 false in
-          (fst(Types.squaresubtype env.delta t t2))::tacc (* H_j *)
+          (Types.squaresubtype env.delta t t2)::tacc (* H_j *)
         ) [] a.fun_iface
       in
       List.iter (fun sl ->