[r2003-03-06 13:51:30 by cvscast] Empty log message

Original author: cvscast
Date: 2003-03-06 13:51:30+00:00

tests/stress_opt_seq.cd

 type T = [ `A? `B? `C? `D? `E? `F? `G? `H? `I? `J?
-           `K? `L? `M? `N? `O? `P? `Q? `R? ];;
+           `K? `L? `M? `N? `O? `P? `Q? `R? `S? `T? ];;
 
 (*
 let fun f (Any -> T) T & x -> x | x -> f x;;
@@ -7,21 +7,25 @@ let fun f (Any -> T) T & x -> x | x -> f x;;
 debug compile Any T;;
 *)
 
-(*
 debug compile T
 P1 where
   P1 = (`A & (a := 1), P2) | (a := 2) & P2 and
   P2 = (`B & (b := 1), P3) | (b := 2) & P3 and
   P3 = (`C & (c := 1), P4) | (c := 2) & P4 and
   P4 = (`D & (d := 1), P5) | (d := 2) & P5 and
-  P5 = `nil;;
-*)
+  P5 = (`E & (e := 1), P6) | (e := 2) & P6 and
+  P6 = (`F & (f := 1), P7) | (f := 2) & P7 and
+  P7 = (`G & (g := 1), P8) | (g := 2) & P8 and
+  P8 = (`H & (h := 1), P9) | (h := 2) & P9 and
+
+  P9 = `nil;;
+
 
 (*
 match [ `A `B `C ] with (P1 where
-  P1 = (`A & (a := 1), P2) | (a := 2) & P2 and
-  P2 = (`B & (b := 1), P3) | (b := 2) & P3 and
-  P3 = (`C & (c := 1), P4) | (c := 2) & P4 and
-  P4 = (`D & (d := 1), P5) | (d := 2) & P5 and
+  P1 = (`A & (a := '1'), P2) | (a := '2') & P2 and
+  P2 = (`B & (b := '1'), P3) | (b := '2') & P3 and
+  P3 = (`C & (c := '1'), P4) | (c := '2') & P4 and
+  P4 = (`D & (d := '1'), P5) | (d := '2') & P5 and
   P5 = `nil) -> (a,b,c,d);;
 *)

types/types.ml

@@ -293,6 +293,8 @@ let cache_false = ref Assumptions.empty
 
 exception NotEmpty
 
+let trivially_empty d = d = empty
+
 let rec empty_rec d =
   if Assumptions.mem d !cache_false then false 
   else if Assumptions.mem d !memo then true
@@ -324,38 +326,19 @@ and empty_rec_times_aux (left,right) =
 (* This avoids explosion with huge rhs (+/- degenerated partitioning)
    May be slower when List.length right is small; could optimize
    this case... *)
-	if empty_rec (cap_t accu1 t1) || empty_rec (cap_t accu2 t2) then
+(*	if empty_rec (cap_t accu1 t1) || empty_rec (cap_t accu2 t2) then*)
+(* THIS IS NOT SOUND !!! *)
+	if trivially_empty (cap_t accu1 t1) || 
+	   trivially_empty (cap_t accu2 t2) then
 	  aux accu1 accu2 right
 	else
           let accu1' = diff_t accu1 t1 in
           if not (empty_rec accu1') then aux accu1' accu2 right;
           let accu2' = diff_t accu2 t2 in
-          if not (empty_rec accu2') then aux accu1 accu2' right
+	  if not (empty_rec accu2') then aux accu1 accu2' right
     | [] -> raise NotEmpty
   in
   let (accu1,accu2) = cap_product left in
-(*
-  let right' = List.filter 
-		 (fun (t1,t2) ->
-		    not 
-		    (empty_rec (cap_t accu1 t1) || empty_rec (cap_t accu2 t2)
-		    )
-		 ) right in
-  if List.length right > 15 then (
-    Format.fprintf Format.std_formatter "[%i=>%i]@." 
-				    (List.length right) (List.length right');
-    Format.fprintf Format.std_formatter "(%a,%a)@." 
-				    !print_descr accu1
-				    !print_descr accu2;
-    List.iter (fun (t1,t2) ->
-		 Format.fprintf Format.std_formatter "\ (%a,%a)@." 
-		   !print_descr (descr t1)
-		   !print_descr (descr t2);
-	      ) right
-  );
-  let right = right' in
-*)
-
   (empty_rec accu1) || (empty_rec accu2) ||
 (* OPT? It does'nt seem so ...  The hope was to return false quickly
    for large right hand-side *)
@@ -536,6 +519,7 @@ This version explodes when dealing with
      (t,s) \ (t1,s1) = (t&t',s\s') | (t\t',s),
    don't call normal_aux *)
 
+
   let get ?(kind=`Normal) d = 
     match kind with
       | `Normal -> get_aux d.times