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

Diff of /types/types.ml

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

revision 219 by abate, Tue Jul 10 17:15:34 2007 UTC revision 220 by abate, Tue Jul 10 17:15:39 2007 UTC
# Line 211  Line 211 
211    
212  let print_descr = ref (fun _ _  -> assert false)  let print_descr = ref (fun _ _  -> assert false)
213    
 (*  
 let define n d = check d; define n d  
 *)  
   
 (*  
 let any_rec = cons { empty with record = Boolean.full }  
 let any_node = make ();;  
 define any_node   {  
   times = Boolean.full;  
   xml   = Boolean.atom  
             (cons { empty with atoms = Atoms.any },  
              cons (times any_rec any_node));  
   arrow = Boolean.full;  
   record= Boolean.full;  
   ints  = Intervals.any;  
   atoms = Atoms.any;  
   chars = Chars.any;  
 };;  
 internalize any_node;;  
 let any = descr any_node  
 *)  
   
214  let neg x = diff any x  let neg x = diff any x
215    
216  let any_node = cons any  let any_node = cons any
217    
 (*  
 let get_record r =  
   let add = SortedMap.add (fun (o1,t1) (o2,t2) -> (o1&&o2, cap t1 t2)) in  
   let line (p,n) =  
     let accu = List.fold_left  
                  (fun accu (l,o,t) -> add l (o,descr t) accu) [] p in  
     List.fold_left  
       (fun accu (l,o,t) -> add l (not o,neg (descr t)) accu) accu n in  
   List.map line r  
 *)  
   
218  module LabelSet = Set.Make(LabelPool)  module LabelSet = Set.Make(LabelPool)
219    
220  let get_record r =  let get_record r =
# Line 330  Line 297 
297  module Assumptions = Set.Make(struct type t = descr let compare = compare end)  module Assumptions = Set.Make(struct type t = descr let compare = compare end)
298    
299  let memo = ref Assumptions.empty  let memo = ref Assumptions.empty
300  let cache_false = ref Assumptions.empty  let cache_false = DescrHash.create 33000
301    
302  exception NotEmpty  exception NotEmpty
303    
304  let trivially_empty d = d = empty  let trivially_empty d = equal_descr d empty
305      (* Remove generic equality ... *)
306    
307  let rec empty_rec d =  let rec empty_rec d =
308    if Assumptions.mem d !cache_false then false    if DescrHash.mem cache_false d then false
309    else if Assumptions.mem d !memo then true    else if Assumptions.mem d !memo then true
310    else if not (Intervals.is_empty d.ints) then false    else if not (Intervals.is_empty d.ints) then false
311    else if not (Atoms.is_empty d.atoms) then false    else if not (Atoms.is_empty d.atoms) then false
# Line 353  Line 321 
321      then true      then true
322      else (      else (
323        memo := backup;        memo := backup;
324        cache_false := Assumptions.add d !cache_false;        DescrHash.add cache_false d ();
325        false        false
326      )      )
327    )    )
# Line 364  Line 332 
332  and empty_rec_times_aux (left,right) =  and empty_rec_times_aux (left,right) =
333    let rec aux accu1 accu2 = function    let rec aux accu1 accu2 = function
334      | (t1,t2)::right ->      | (t1,t2)::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*)  
 (* THIS IS NOT SOUND !!! *)  
335          if trivially_empty (cap_t accu1 t1) ||          if trivially_empty (cap_t accu1 t1) ||
336             trivially_empty (cap_t accu2 t2) then             trivially_empty (cap_t accu2 t2) then
337            aux accu1 accu2 right            aux accu1 accu2 right
# Line 381  Line 344 
344    in    in
345    let (accu1,accu2) = cap_product left in    let (accu1,accu2) = cap_product left in
346    (empty_rec accu1) || (empty_rec accu2) ||    (empty_rec accu1) || (empty_rec accu2) ||
 (* OPT? It does'nt seem so ...  The hope was to return false quickly  
    for large right hand-side *)  
   (  
     (* (if (List.length right > 2) then  
        let (cup1,cup2) = cup_product right in  
        (empty_rec (diff accu1 cup1)) && (empty_rec (diff accu2 cup2))  
      else true)  
     && *)  
347      (try aux accu1 accu2 right; true with NotEmpty -> false)      (try aux accu1 accu2 right; true with NotEmpty -> false)
348    )  
349    
350  and empty_rec_arrow c =  and empty_rec_arrow c =
351    List.for_all empty_rec_arrow_aux c    List.for_all empty_rec_arrow_aux c
# Line 420  Line 375 
375            exists (Array.length left)            exists (Array.length left)
376              (fun i ->              (fun i ->
377                 (not (left_opt.(i) && right_opt.(i))) &&                 (not (left_opt.(i) && right_opt.(i))) &&
378                 (empty_rec (cap left.(i) right.(i))))                 (trivially_empty (cap left.(i) right.(i))))
379          in          in
380          if next then aux rights          if next then aux rights
381          else          else
Legend:
Removed from v.219  
changed lines
  Added in v.220
CVS Admin">CVS Admin
 ViewVC Help
Powered by ViewVC 1.1.5