[r2003-03-07 00:18:35 by cvscast] Empty log message

Original author: cvscast
Date: 2003-03-07 00:18:35+00:00

types/types.ml

@@ -283,33 +283,166 @@ let cap_product l =
     (any,any)
     l
 
-
-let cup_product l = 
-  List.fold_left 
-    (fun (d1,d2) (t1,t2) -> (cup_t d1 t1, cup_t d2 t2))
-    (empty,empty)
-    l
-
 let rec exists max f =
   (max > 0) && (f (max - 1) || exists (max - 1) f)
 
+let trivially_empty d = equal_descr d empty
 
-module Assumptions = Set.Make(struct type t = descr let compare = compare end)
+exception NotEmpty
 
-let memo = ref Assumptions.empty
-let cache_false = DescrHash.create 33000
+type slot = { mutable status : status; 
+	       mutable notify : notify;
+	       mutable active : bool }
+and status = Empty | NEmpty | Maybe
+and notify = Nothing | Do of slot * (slot -> unit) * notify
+
+let memo = DescrHash.create 33000
+
+let marks = ref [] 
+let slot_empty = { status = Empty; active = false; notify = Nothing }
+let slot_not_empty = { status = NEmpty; active = false; notify = Nothing }
+
+let rec notify = function
+  | Nothing -> ()
+  | Do (n,f,rem) -> 
+      if n.status = Maybe then (try f n with NotEmpty -> ());
+      notify rem
+
+let rec iter_s s f = function
+  | [] -> ()
+  | arg::rem -> f arg s; iter_s s f rem
+
+
+let set s =
+  s.status <- NEmpty;
+  notify s.notify;
+  raise NotEmpty
+
+let rec big_conj f l n =
+  match l with
+    | [] -> set n
+    | [arg] -> f arg n
+    | arg::rem ->
+	let s = { status = Maybe; active = false; notify = Do (n,(big_conj f rem), Nothing) } in
+	try 
+	  f arg s;
+	  if s.active then n.active <- true
+	with NotEmpty -> if n.status = NEmpty then raise NotEmpty
+
+let rec guard a f n =
+  let s = slot a in
+  match s.status with
+    | Empty -> ()
+    | Maybe -> n.active <- true; s.notify <- Do (n,f,s.notify)
+    | NEmpty -> f n
+
+and slot d =
+  if not ((Intervals.is_empty d.ints) && 
+	  (Atoms.is_empty d.atoms) &&
+	  (Chars.is_empty d.chars)) then slot_not_empty 
+  else try DescrHash.find memo d
+  with Not_found ->
+    let s = { status = Maybe; active = false; notify = Nothing } in
+    DescrHash.add memo d s;
+    (try
+       iter_s s check_times d.times;
+       iter_s s check_times d.xml;
+       iter_s s check_arrow d.arrow;
+       iter_s s check_record (get_record d.record);
+       if s.active then marks := s :: !marks else s.status <- Empty;
+     with
+	 NotEmpty -> ());
+    s
+
+and check_times (left,right) s =
+  let rec aux accu1 accu2 right s = match right with
+    | (t1,t2)::right ->
+	if trivially_empty (cap_t accu1 t1) || 
+	   trivially_empty (cap_t accu2 t2) then
+	     aux accu1 accu2 right s
+	else
+          let accu1' = diff_t accu1 t1 in guard accu1' (aux accu1' accu2 right) s;
+          let accu2' = diff_t accu2 t2 in guard accu2' (aux accu1 accu2' right) s
+    | [] -> set s
+  in
+  let (accu1,accu2) = cap_product left in
+  guard accu1 (guard accu2 (aux accu1 accu2 right)) s
 
-exception NotEmpty
+and check_arrow (left,right) s =
+  let single_right (s1,s2) s =
+    let rec aux accu1 accu2 left s = match left with
+      | (t1,t2)::left ->
+          let accu1' = diff_t accu1 t1 in guard accu1' (aux accu1' accu2 left) s;
+          let accu2' = cap_t  accu2 t2 in guard accu2' (aux accu1 accu2' left) s
+      | [] -> set s
+    in
+    let accu1 = descr s1 in
+    guard accu1 (aux accu1 (neg (descr s2)) left) s
+  in
+  big_conj single_right right s
 
-let trivially_empty d = equal_descr d empty
-  (* Remove generic equality ... *)
+and check_record (labels,(oleft,(left_opt,left)),rights) s =
+  let rec aux rights s = match rights with
+    | [] -> set s
+    | (oright,(right_opt,right))::rights ->
+	let next =
+	  (oleft && (not oright)) ||
+	  exists (Array.length left)
+	    (fun i ->
+	       (not (left_opt.(i) && right_opt.(i))) &&
+	       (trivially_empty (cap left.(i) right.(i))))
+	in
+	if next then aux rights s
+	else
+	  for i = 0 to Array.length left - 1 do
+	    let back = left.(i) in
+	    let oback = left_opt.(i) in
+	    let odi = oback && (not right_opt.(i)) in
+	    let di = diff back right.(i) in
+	    if odi then (
+	      left.(i) <- diff back right.(i);
+	      left_opt.(i) <- odi;
+	      aux rights s;
+	      left.(i) <- back;
+	      left_opt.(i) <- oback;
+	    ) else
+	      guard di (fun s ->
+			  left.(i) <- diff back right.(i);
+			  left_opt.(i) <- odi;
+			  aux rights s;
+			  left.(i) <- back;
+			  left_opt.(i) <- oback;
+		       ) s
+	  done
+  in
+  let rec start i s =
+    if (i < 0) then aux rights s
+    else
+      if left_opt.(i) then start (i - 1) s
+      else guard left.(i) (start (i - 1)) s
+  in
+  start (Array.length left - 1) s
+
+
+let is_empty d =
+  let s = slot d in
+  List.iter 
+    (fun s' -> if s'.status = Maybe then s'.status <- Empty; s'.notify <- Nothing) 
+    !marks;
+  marks := [];
+  s.status = Empty
+  
+
+module Assumptions = Set.Make(struct type t = descr let compare = compare end)
+let memo = ref Assumptions.empty
+let cache_false = DescrHash.create 33000
 
 let rec empty_rec d =
-  if DescrHash.mem cache_false d then false 
-  else if Assumptions.mem d !memo then true
-  else if not (Intervals.is_empty d.ints) then false
+  if not (Intervals.is_empty d.ints) then false
   else if not (Atoms.is_empty d.atoms) then false
   else if not (Chars.is_empty d.chars) then false
+  else if DescrHash.mem cache_false d then false 
+  else if Assumptions.mem d !memo then true
   else (
     let backup = !memo in
     memo := Assumptions.add d backup;
@@ -355,9 +488,9 @@ and empty_rec_arrow_aux (left,right) =
     let rec aux accu1 accu2 = function
       | (t1,t2)::left ->
           let accu1' = diff_t accu1 t1 in
-          if not (empty_rec accu1') then aux accu1 accu2 left;
+          if not (empty_rec accu1') then aux accu1' accu2 left;
           let accu2' = cap_t accu2 t2 in
-          if not (empty_rec accu2') then aux accu1 accu2 left
+          if not (empty_rec accu2') then aux accu1 accu2' left
       | [] -> raise NotEmpty
     in
     let accu1 = descr s1 in
@@ -402,8 +535,9 @@ and empty_rec_record_aux (labels,(oleft,(left_opt,left)),rights) =
 and empty_rec_record c =
   List.for_all empty_rec_record_aux (get_record c)
 
-let is_empty d =
+(*let is_empty d =
   empty_rec d
+*)
 
 let non_empty d = 
   not (is_empty d)