/[svn]/types/types.ml
ViewVC logotype

Diff of /types/types.ml

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 220 by abate, Tue Jul 10 17:15:39 2007 UTC revision 221 by abate, Tue Jul 10 17:15:42 2007 UTC
# Line 283  Line 283 
283      (any,any)      (any,any)
284      l      l
285    
   
 let cup_product l =  
   List.fold_left  
     (fun (d1,d2) (t1,t2) -> (cup_t d1 t1, cup_t d2 t2))  
     (empty,empty)  
     l  
   
286  let rec exists max f =  let rec exists max f =
287    (max > 0) && (f (max - 1) || exists (max - 1) f)    (max > 0) && (f (max - 1) || exists (max - 1) f)
288    
289    let trivially_empty d = equal_descr d empty
290    
291  module Assumptions = Set.Make(struct type t = descr let compare = compare end)  exception NotEmpty
292    
293  let memo = ref Assumptions.empty  type slot = { mutable status : status;
294  let cache_false = DescrHash.create 33000                 mutable notify : notify;
295                   mutable active : bool }
296    and status = Empty | NEmpty | Maybe
297    and notify = Nothing | Do of slot * (slot -> unit) * notify
298    
299    let memo = DescrHash.create 33000
300    
301    let marks = ref []
302    let slot_empty = { status = Empty; active = false; notify = Nothing }
303    let slot_not_empty = { status = NEmpty; active = false; notify = Nothing }
304    
305    let rec notify = function
306      | Nothing -> ()
307      | Do (n,f,rem) ->
308          if n.status = Maybe then (try f n with NotEmpty -> ());
309          notify rem
310    
311    let rec iter_s s f = function
312      | [] -> ()
313      | arg::rem -> f arg s; iter_s s f rem
314    
315    
316    let set s =
317      s.status <- NEmpty;
318      notify s.notify;
319      raise NotEmpty
320    
321    let rec big_conj f l n =
322      match l with
323        | [] -> set n
324        | [arg] -> f arg n
325        | arg::rem ->
326            let s = { status = Maybe; active = false; notify = Do (n,(big_conj f rem), Nothing) } in
327            try
328              f arg s;
329              if s.active then n.active <- true
330            with NotEmpty -> if n.status = NEmpty then raise NotEmpty
331    
332    let rec guard a f n =
333      let s = slot a in
334      match s.status with
335        | Empty -> ()
336        | Maybe -> n.active <- true; s.notify <- Do (n,f,s.notify)
337        | NEmpty -> f n
338    
339    and slot d =
340      if not ((Intervals.is_empty d.ints) &&
341              (Atoms.is_empty d.atoms) &&
342              (Chars.is_empty d.chars)) then slot_not_empty
343      else try DescrHash.find memo d
344      with Not_found ->
345        let s = { status = Maybe; active = false; notify = Nothing } in
346        DescrHash.add memo d s;
347        (try
348           iter_s s check_times d.times;
349           iter_s s check_times d.xml;
350           iter_s s check_arrow d.arrow;
351           iter_s s check_record (get_record d.record);
352           if s.active then marks := s :: !marks else s.status <- Empty;
353         with
354             NotEmpty -> ());
355        s
356    
357  exception NotEmpty  and check_times (left,right) s =
358      let rec aux accu1 accu2 right s = match right with
359        | (t1,t2)::right ->
360            if trivially_empty (cap_t accu1 t1) ||
361               trivially_empty (cap_t accu2 t2) then
362                 aux accu1 accu2 right s
363            else
364              let accu1' = diff_t accu1 t1 in guard accu1' (aux accu1' accu2 right) s;
365              let accu2' = diff_t accu2 t2 in guard accu2' (aux accu1 accu2' right) s
366        | [] -> set s
367      in
368      let (accu1,accu2) = cap_product left in
369      guard accu1 (guard accu2 (aux accu1 accu2 right)) s
370    
371    and check_arrow (left,right) s =
372      let single_right (s1,s2) s =
373        let rec aux accu1 accu2 left s = match left with
374          | (t1,t2)::left ->
375              let accu1' = diff_t accu1 t1 in guard accu1' (aux accu1' accu2 left) s;
376              let accu2' = cap_t  accu2 t2 in guard accu2' (aux accu1 accu2' left) s
377          | [] -> set s
378        in
379        let accu1 = descr s1 in
380        guard accu1 (aux accu1 (neg (descr s2)) left) s
381      in
382      big_conj single_right right s
383    
384    and check_record (labels,(oleft,(left_opt,left)),rights) s =
385      let rec aux rights s = match rights with
386        | [] -> set s
387        | (oright,(right_opt,right))::rights ->
388            let next =
389              (oleft && (not oright)) ||
390              exists (Array.length left)
391                (fun i ->
392                   (not (left_opt.(i) && right_opt.(i))) &&
393                   (trivially_empty (cap left.(i) right.(i))))
394            in
395            if next then aux rights s
396            else
397              for i = 0 to Array.length left - 1 do
398                let back = left.(i) in
399                let oback = left_opt.(i) in
400                let odi = oback && (not right_opt.(i)) in
401                let di = diff back right.(i) in
402                if odi then (
403                  left.(i) <- diff back right.(i);
404                  left_opt.(i) <- odi;
405                  aux rights s;
406                  left.(i) <- back;
407                  left_opt.(i) <- oback;
408                ) else
409                  guard di (fun s ->
410                              left.(i) <- diff back right.(i);
411                              left_opt.(i) <- odi;
412                              aux rights s;
413                              left.(i) <- back;
414                              left_opt.(i) <- oback;
415                           ) s
416              done
417      in
418      let rec start i s =
419        if (i < 0) then aux rights s
420        else
421          if left_opt.(i) then start (i - 1) s
422          else guard left.(i) (start (i - 1)) s
423      in
424      start (Array.length left - 1) s
425    
426    
427    let is_empty d =
428      let s = slot d in
429      List.iter
430        (fun s' -> if s'.status = Maybe then s'.status <- Empty; s'.notify <- Nothing)
431        !marks;
432      marks := [];
433      s.status = Empty
434    
435  let trivially_empty d = equal_descr d empty  
436    (* Remove generic equality ... *)  module Assumptions = Set.Make(struct type t = descr let compare = compare end)
437    let memo = ref Assumptions.empty
438    let cache_false = DescrHash.create 33000
439    
440  let rec empty_rec d =  let rec empty_rec d =
441    if DescrHash.mem cache_false d then false    if not (Intervals.is_empty d.ints) then false
   else if Assumptions.mem d !memo then true  
   else if not (Intervals.is_empty d.ints) then false  
442    else if not (Atoms.is_empty d.atoms) then false    else if not (Atoms.is_empty d.atoms) then false
443    else if not (Chars.is_empty d.chars) then false    else if not (Chars.is_empty d.chars) then false
444      else if DescrHash.mem cache_false d then false
445      else if Assumptions.mem d !memo then true
446    else (    else (
447      let backup = !memo in      let backup = !memo in
448      memo := Assumptions.add d backup;      memo := Assumptions.add d backup;
# Line 355  Line 488 
488      let rec aux accu1 accu2 = function      let rec aux accu1 accu2 = function
489        | (t1,t2)::left ->        | (t1,t2)::left ->
490            let accu1' = diff_t accu1 t1 in            let accu1' = diff_t accu1 t1 in
491            if not (empty_rec accu1') then aux accu1 accu2 left;            if not (empty_rec accu1') then aux accu1' accu2 left;
492            let accu2' = cap_t accu2 t2 in            let accu2' = cap_t accu2 t2 in
493            if not (empty_rec accu2') then aux accu1 accu2 left            if not (empty_rec accu2') then aux accu1 accu2' left
494        | [] -> raise NotEmpty        | [] -> raise NotEmpty
495      in      in
496      let accu1 = descr s1 in      let accu1 = descr s1 in
# Line 402  Line 535 
535  and empty_rec_record c =  and empty_rec_record c =
536    List.for_all empty_rec_record_aux (get_record c)    List.for_all empty_rec_record_aux (get_record c)
537    
538  let is_empty d =  (*let is_empty d =
539    empty_rec d    empty_rec d
540    *)
541    
542  let non_empty d =  let non_empty d =
543    not (is_empty d)    not (is_empty d)
Legend:
Removed from v.220  
changed lines
  Added in v.221
CVS Admin">CVS Admin
 ViewVC Help
Powered by ViewVC 1.1.5