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

Diff of /types/types.ml

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

revision 169 by abate, Tue Jul 10 17:12:13 2007 UTC revision 240 by abate, Tue Jul 10 17:18:24 2007 UTC
# Line 1  Line 1 
1  open Recursive  open Recursive
2  open Printf  open Printf
3    open Ident
4    
5    (* IDEAS for optimizations:
6    
7      * optimize lines of dnf for products and record;
8        instead of
9          (t1,s1) & ... & (tn,sn) \ ....
10        use:
11          (t1 & ... & tn, s1 & ... & sn) \ ....
12    
13        ---> more compact representation, more sharing, ...
14    
15      * re-consider using BDD-like representation instead of dnf
16    *)
17    
18    
19  let map_sort f l =  let map_sort f l =
# Line 12  Line 26 
26    let equal = (=)    let equal = (=)
27  end  end
28    
 module LabelPool = Pool.Make(HashedString)  
 module AtomPool  = Pool.Make(HashedString)  
   
 type label = LabelPool.t  
 type atom  = AtomPool.t  
29    
30  type const = Integer of Big_int.big_int | Atom of atom | Char of Chars.Unichar.t  type const =
31      | Integer of Intervals.v
32      | Atom of Atoms.v
33      | Char of Chars.v
34    
35  type pair_kind = [ `Normal | `XML ]  type pair_kind = [ `Normal | `XML ]
36    
37  module I = struct  type 'a node0 = { id : int; mutable descr : 'a }
38    type 'a t = {  
39      atoms : atom Atoms.t;  module NodePair = struct
40      type 'a t = 'a node0 * 'a node0
41      let compare (x1,y1) (x2,y2) =
42        if x1.id < x2.id then -1
43        else if x1.id > x2.id then 1
44        else y1.id - y2.id
45      let equal (x1,y1) (x2,y2) = (x1==x2) && (y1==y2)
46      let hash (x,y) = x.id + 17 * y.id
47    end
48    
49    module RecArg = struct
50      type 'a t = bool * 'a node0 label_map
51    
52      let rec compare_rec r1 r2 =
53        if r1 == r2 then 0
54        else match (r1,r2) with
55          | (l1,x1)::r1,(l2,x2)::r2 ->
56              if ((l1:int) < l2) then -1
57              else if (l1 > l2) then 1
58              else if x1.id < x2.id then -1
59              else if x1.id > x2.id then 1
60              else compare_rec r1 r2
61          | ([],_) -> -1
62          | _ -> 1
63    
64      let compare (o1,r1) (o2,r2) =
65        if o1 && not o2 then -1
66        else if o2 && not o1 then 1
67        else compare_rec (LabelMap.get r1) (LabelMap.get r2)
68    
69      let rec equal_rec r1 r2 =
70        (r1 == r2) ||
71        match (r1,r2) with
72          | (l1,x1)::r1,(l2,x2)::r2 ->
73              (x1.id == x2.id) && (l1 == l2) && (equal_rec r1 r2)
74          | _ -> false
75    
76      let equal (o1,r1) (o2,r2) =
77        (o1 == o2) && (equal_rec (LabelMap.get r1) (LabelMap.get r2))
78    
79      let rec hash_rec accu = function
80        | (l,x)::rem -> hash_rec (257 * accu + 17 * l + x.id) rem
81        | [] -> accu + 5
82    
83      let hash (o,r) = hash_rec (if o then 2 else 1) (LabelMap.get r)
84    end
85    
86    module BoolPair = Boolean.Make(NodePair)
87    module BoolRec = Boolean.Make(RecArg)
88    
89    type descr = {
90      atoms : Atoms.t;
91      ints  : Intervals.t;      ints  : Intervals.t;
92      chars : Chars.t;      chars : Chars.t;
93      times : ('a * 'a) Boolean.t;    times : descr BoolPair.t;
94      xml   : ('a * 'a) Boolean.t;    xml   : descr BoolPair.t;
95      arrow : ('a * 'a) Boolean.t;    arrow : descr BoolPair.t;
96      record: (bool * (label, (bool * 'a)) SortedMap.t) Boolean.t;    record: descr BoolRec.t;
97    }    absent: bool
98    } and node = descr node0
99    
100    
101    let empty = {    let empty = {
102      times = Boolean.empty;    times = BoolPair.empty;
103      xml   = Boolean.empty;    xml   = BoolPair.empty;
104      arrow = Boolean.empty;    arrow = BoolPair.empty;
105      record= Boolean.empty;    record= BoolRec.empty;
106      ints  = Intervals.empty;      ints  = Intervals.empty;
107      atoms = Atoms.empty;      atoms = Atoms.empty;
108      chars = Chars.empty;      chars = Chars.empty;
109      absent= false;
110    }    }
111    
112    let any =  {    let any =  {
113      times = Boolean.full;    times = BoolPair.full;
114      xml   = Boolean.full;    xml   = BoolPair.full;
115      arrow = Boolean.full;    arrow = BoolPair.full;
116      record= Boolean.full;    record= BoolRec.full;
117      ints  = Intervals.any;      ints  = Intervals.any;
118      atoms = Atoms.any;      atoms = Atoms.any;
119      chars = Chars.any;      chars = Chars.any;
120      absent= false;
121    }    }
122    
123    
124    let interval i = { empty with ints = i }    let interval i = { empty with ints = i }
125    let times x y = { empty with times = Boolean.atom (x,y) }  let times x y = { empty with times = BoolPair.atom (x,y) }
126    let xml x y = { empty with xml = Boolean.atom (x,y) }  let xml x y = { empty with xml = BoolPair.atom (x,y) }
127    let arrow x y = { empty with arrow = Boolean.atom (x,y) }  let arrow x y = { empty with arrow = BoolPair.atom (x,y) }
128    let record label opt t =  let record label t =
129      { empty with record = Boolean.atom (true,[label,(opt,t)]) }    { empty with record = BoolRec.atom (true,LabelMap.singleton label t) }
130    let record' x =  let record' (x : bool * node Ident.label_map) =
131      { empty with record = Boolean.atom x }    { empty with record = BoolRec.atom x }
132    let atom a = { empty with atoms = a }    let atom a = { empty with atoms = a }
133    let char c = { empty with chars = c }    let char c = { empty with chars = c }
134    let constant = function    let constant = function
# Line 69  Line 136 
136      | Atom a -> atom (Atoms.atom a)      | Atom a -> atom (Atoms.atom a)
137      | Char c -> char (Chars.atom c)      | Char c -> char (Chars.atom c)
138    
   
139    let cup x y =    let cup x y =
140      if x = y then x else {    if x == y then x else {
141        times = Boolean.cup x.times y.times;      times = BoolPair.cup x.times y.times;
142        xml   = Boolean.cup x.xml y.xml;      xml   = BoolPair.cup x.xml y.xml;
143        arrow = Boolean.cup x.arrow y.arrow;      arrow = BoolPair.cup x.arrow y.arrow;
144        record= Boolean.cup x.record y.record;      record= BoolRec.cup x.record y.record;
145        ints  = Intervals.cup x.ints  y.ints;        ints  = Intervals.cup x.ints  y.ints;
146        atoms = Atoms.cup x.atoms y.atoms;        atoms = Atoms.cup x.atoms y.atoms;
147        chars = Chars.cup x.chars y.chars;        chars = Chars.cup x.chars y.chars;
148        absent= x.absent || y.absent;
149      }      }
150    
151    let cap x y =    let cap x y =
152      if x = y then x else {    if x == y then x else {
153        times = Boolean.cap x.times y.times;      times = BoolPair.cap x.times y.times;
154        xml   = Boolean.cap x.xml y.xml;      xml   = BoolPair.cap x.xml y.xml;
155        record= Boolean.cap x.record y.record;      record= BoolRec.cap x.record y.record;
156        arrow = Boolean.cap x.arrow y.arrow;      arrow = BoolPair.cap x.arrow y.arrow;
157        ints  = Intervals.cap x.ints  y.ints;        ints  = Intervals.cap x.ints  y.ints;
158        atoms = Atoms.cap x.atoms y.atoms;        atoms = Atoms.cap x.atoms y.atoms;
159        chars = Chars.cap x.chars y.chars;        chars = Chars.cap x.chars y.chars;
160        absent= x.absent && y.absent;
161      }      }
162    
163    let diff x y =    let diff x y =
164      if x = y then empty else {    if x == y then empty else {
165        times = Boolean.diff x.times y.times;      times = BoolPair.diff x.times y.times;
166        xml   = Boolean.diff x.xml y.xml;      xml   = BoolPair.diff x.xml y.xml;
167        arrow = Boolean.diff x.arrow y.arrow;      arrow = BoolPair.diff x.arrow y.arrow;
168        record= Boolean.diff x.record y.record;      record= BoolRec.diff x.record y.record;
169        ints  = Intervals.diff x.ints  y.ints;        ints  = Intervals.diff x.ints  y.ints;
170        atoms = Atoms.diff x.atoms y.atoms;        atoms = Atoms.diff x.atoms y.atoms;
171        chars = Chars.diff x.chars y.chars;        chars = Chars.diff x.chars y.chars;
172        absent= x.absent && not y.absent;
173      }      }
174    
175    let count = ref 0
176    let make () = incr count; { id = !count; descr = empty }
177    let define n d = n.descr <- d
178    let cons d = incr count; { id = !count; descr = d }
179    let descr n = n.descr
180    let internalize n = n
181    let id n = n.id
182    
183    let rec compare_rec r1 r2 =
184      if r1 == r2 then 0
185      else match (r1,r2) with
186        | (l1,x1)::r1,(l2,x2)::r2 ->
187            if ((l1:int) < l2) then -1
188            else if (l1 > l2) then 1
189            else if x1.id < x2.id then -1
190            else if x1.id > x2.id then 1
191            else compare_rec r1 r2
192        | ([],_) -> -1
193        | _ -> 1
194    
195    let rec compare_rec_list l1 l2  =
196      if l1 == l2 then 0
197      else match (l1,l2) with
198        | (o1,r1)::l1, (o2,r2)::l2 ->
199            if o2 && not o1 then -1
200            else if o1 && not o2 then 1
201            else let c = compare_rec r1 r2 in if c <> 0 then c
202            else compare_rec_list l1 l2
203        | ([],_) -> -1
204        | _ -> 1
205    
206    let rec compare_rec_bool l1 l2  =
207      if l1 == l2 then 0
208      else match (l1,l2) with
209        | (p1,n1)::l1, (p2,n2)::l2 ->
210            let c = compare_rec_list p1 p2 in if c <> 0 then c
211            else let c = compare_rec_list n1 n2 in if c <> 0 then c
212            else compare_rec_bool l1 l2
213        | ([],_) -> -1
214        | _ -> 1
215    
216    let rec compare_times_list l1 l2  =
217      if l1 == l2 then 0
218      else match (l1,l2) with
219        | (x1,y1)::l1, (x2,y2)::l2 ->
220            if (x1.id < x2.id) then -1
221            else if (x1.id > x2.id) then 1
222            else if (y1.id < y2.id) then -1
223            else if (y1.id > y2.id) then 1
224            else compare_times_list l1 l2
225        | ([],_) -> -1
226        | _ -> 1
227    
228    let rec compare_times_bool l1 l2  =
229      if l1 == l2 then 0
230      else match (l1,l2) with
231        | (p1,n1)::l1, (p2,n2)::l2 ->
232            let c = compare_times_list p1 p2 in if c <> 0 then c
233            else let c = compare_times_list n1 n2 in if c <> 0 then c
234            else compare_times_bool l1 l2
235        | ([],_) -> -1
236        | _ -> 1
237    
238    let rec equal_rec e r1 r2 =  let rec equal_rec r1 r2 =
239      (r1 == r2) ||
240      match (r1,r2) with      match (r1,r2) with
241      | [],[] -> ()      | (l1,x1)::r1,(l2,x2)::r2 ->
242      | (l1,(o1,x1))::r1,(l2,(o2,x2))::r2 ->          (x1.id = x2.id) && (l1 == l2) && (equal_rec r1 r2)
243          if (l1 <> l2) || (o1 <> o2) then raise NotEqual;      | _ -> false
244          e x1 x2; equal_rec e r1 r2  
245      | _ -> raise NotEqual  let rec equal_rec_list l1 l2  =
246  (* check: faster to reverse the calls to e and to equal_rec ? *)    (l1 == l2) ||
247      match (l1,l2) with
248    let equal e a b =      | (o1,r1)::l1, (o2,r2)::l2 ->
249      if a.atoms <> b.atoms then raise NotEqual;          (o1 == o2) &&
250      if a.chars <> b.chars then raise NotEqual;          (equal_rec r1 r2) && (equal_rec_list l1 l2)
251      if a.ints <> b.ints then raise NotEqual;      | _ -> false
252      Boolean.equal (fun (x1,x2) (y1,y2) -> e x1 y1; e x2 y2) a.times b.times;  
253      Boolean.equal (fun (x1,x2) (y1,y2) -> e x1 y1; e x2 y2) a.xml b.xml;  let rec equal_rec_bool l1 l2 =
254      Boolean.equal (fun (x1,x2) (y1,y2) -> e x1 y1; e x2 y2) a.arrow b.arrow;    (l1 == l2) ||
255      Boolean.equal (fun (o1,r1) (o2,r2) ->    match (l1,l2) with
256                       if (o1 <> o2) then raise NotEqual;      | (p1,n1)::l1, (p2,n2)::l2 ->
257                       equal_rec e r1 r2)          (equal_rec_list p1 p2) &&
258        a.record b.record          (equal_rec_list n1 n2) &&
259            (equal_rec_bool l1 l2)
260    let map f a =      | _ -> false
261      { times = Boolean.map (fun (x1,x2) -> (f x1, f x2)) a.times;  
262        xml   = Boolean.map (fun (x1,x2) -> (f x1, f x2)) a.xml;  let rec equal_times_list l1 l2  =
263        arrow = Boolean.map (fun (x1,x2) -> (f x1, f x2)) a.arrow;    (l1 == l2) ||
264        record= Boolean.map (fun (o,r) ->    match (l1,l2) with
265                               (o, List.map (fun (l,(o,x)) -> (l,(o,f x))) r))      | (x1,y1)::l1, (x2,y2)::l2 ->
266                  a.record;          (x1.id = x2.id) &&
267        ints  = a.ints;          (y1.id = y2.id) &&
268        atoms = a.atoms;          (equal_times_list l1 l2)
269        chars = a.chars;      | _ -> false
270      }  
271    let rec equal_times_bool l1 l2 =
272      (l1 == l2) ||
273      match (l1,l2) with
274        | (p1,n1)::l1, (p2,n2)::l2 ->
275            (equal_times_list p1 p2) &&
276            (equal_times_list n1 n2) &&
277            (equal_times_bool l1 l2)
278        | _ -> false
279    
280    let equal_descr a b =
281      (Atoms.equal a.atoms b.atoms) &&
282      (Chars.equal a.chars b.chars) &&
283      (Intervals.equal a.ints  b.ints) &&
284      (BoolPair.equal a.times b.times) &&
285      (BoolPair.equal a.xml b.xml) &&
286      (BoolPair.equal a.arrow b.arrow) &&
287      (BoolRec.equal a.record b.record) &&
288      (a.absent == b.absent)
289    
290    let compare_descr a b =
291      let c = compare a.atoms b.atoms in if c <> 0 then c
292      else let c = compare a.chars b.chars in if c <> 0 then c
293      else let c = compare a.ints b.ints in if c <> 0 then c
294      else let c = BoolPair.compare a.times b.times in if c <> 0 then c
295      else let c = BoolPair.compare a.xml b.xml in if c <> 0 then c
296      else let c = BoolPair.compare a.arrow b.arrow in if c <> 0 then c
297      else let c = BoolRec.compare a.record b.record in if c <> 0 then c
298      else if a.absent && not b.absent then -1
299      else if b.absent && not a.absent then 1
300      else 0
301    
   let hash h a =  
     Hashtbl.hash (map h a)  
302  (*  (*
303      (Hashtbl.hash { (map h a) with ints = Intervals.empty })  let compare_descr a b =
304      + (Intervals.hash a.ints)    let c = compare_descr a b in
305      assert (c = compare a b);
306      c
307  *)  *)
308    
   let iter f a =  
     ignore (map f a)  
   
   let deep = 4  
 end  
309    
310    let rec hash_times_list accu = function
311      | (x,y)::l ->
312          hash_times_list (accu * 257 + x.id * 17 + y.id) l
313      | [] -> accu + 17
314    
315    let rec hash_times_bool accu = function
316      | (p,n)::l ->
317          hash_times_bool (hash_times_list (hash_times_list accu p) n) l
318      | [] -> accu + 3
319    
320    let rec hash_rec accu = function
321      | (l,x)::rem ->
322          hash_rec (257 * accu + 17 * (LabelPool.hash l) + x.id) rem
323      | [] -> accu + 5
324    
325    let rec hash_rec_list accu = function
326      | (o,r)::l ->
327          hash_rec_list (hash_rec (if o then accu*3 else accu) r) l
328      | [] -> accu + 17
329    
330    let rec hash_rec_bool accu = function
331      | (p,n)::l ->
332          hash_rec_bool (hash_rec_list (hash_rec_list accu p) n) l
333      | [] -> accu + 3
334    
335    
336    let hash_descr a =
337      let accu = Chars.hash 1 a.chars in
338      let accu = Intervals.hash accu a.ints in
339      let accu = Atoms.hash accu a.atoms in
340      let accu = 17 * accu + BoolPair.hash a.times in
341      let accu = 17 * accu + BoolPair.hash a.xml in
342      let accu = 17 * accu + BoolPair.hash a.arrow in
343      let accu = 17 * accu + BoolRec.hash a.record in
344      let accu = if a.absent then accu+5 else accu in
345      accu
346    
 module Algebra = Recursive_noshare.Make(I)  
 include I  
 include Algebra  
347  module DescrHash =  module DescrHash =
348    Hashtbl.Make(    Hashtbl.Make(
349      struct      struct
# Line 165  Line 355 
355    
356  let print_descr = ref (fun _ _  -> assert false)  let print_descr = ref (fun _ _  -> assert false)
357    
 (*  
 let define n d = check d; define n d  
 *)  
   
 let cons d =  
   let n = make () in  
   define n d;  
   internalize n  
   
 (*  
 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  
 *)  
   
358  let neg x = diff any x  let neg x = diff any x
359    
360  let any_node = cons any  let any_node = cons any
361    
362  (*  module LabelS = Set.Make(LabelPool)
 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  
 *)  
   
 module LabelSet = Set.Make(LabelPool)  
363    
364  let get_record r =  let get_record r =
365    let labs accu (_,r) =    let labs accu (_,r) =
366      List.fold_left (fun accu (l,_) -> LabelSet.add l accu) accu r in      List.fold_left
367    let extend (opts,descrs) labs (o,r) =        (fun accu (l,_) -> LabelS.add l accu) accu (LabelMap.get r) in
368      let extend descrs labs (o,r) =
369      let rec aux i labs r =      let rec aux i labs r =
370        match labs with        match labs with
371          | [] -> ()          | [] -> ()
372          | l1::labs ->          | l1::labs ->
373              match r with              match r with
374                | (l2,(o,x))::r when l1 = l2 ->                | (l2,x)::r when l1 == l2 ->
375                    descrs.(i) <- cap descrs.(i) (descr x);                    descrs.(i) <- cap descrs.(i) (descr x);
                   opts.(i) <- opts.(i) && o;  
376                    aux (i+1) labs r                    aux (i+1) labs r
377                | r ->                | r ->
378                    if not o then descrs.(i) <- empty;                    if not o then descrs.(i) <-
379                        cap descrs.(i) { empty with absent = true };
380                    aux (i+1) labs r                    aux (i+1) labs r
381      in      in
382      aux 0 labs r;      aux 0 labs (LabelMap.get r);
383      o      o
384    in    in
385    let line (p,n) =    let line (p,n) =
386      let labels =      let labels =
387        List.fold_left labs (List.fold_left labs LabelSet.empty p) n in        List.fold_left labs (List.fold_left labs LabelS.empty p) n in
388      let labels = LabelSet.elements labels in      let labels = LabelS.elements labels in
389      let nlab = List.length labels in      let nlab = List.length labels in
390      let mk () = Array.create nlab true, Array.create nlab any in      let mk () = Array.create nlab { any with absent = true } in
391    
392      let pos = mk () in      let pos = mk () in
393      let opos = List.fold_left      let opos = List.fold_left
# Line 250  Line 403 
403                       ) n in                       ) n in
404      (labels,p,n)      (labels,p,n)
405    in    in
406    List.map line r    List.map line (BoolRec.get r)
407    
408    
409  module DescrMap = Map.Make(struct type t = descr let compare = compare end)  module DescrMap = Map.Make(struct type t = descr let compare = compare end)
410    
411  let check d =  let check d =
412    Boolean.check d.times;    BoolPair.check d.times;
413    Boolean.check d.xml;    BoolPair.check d.xml;
414    Boolean.check d.arrow;    BoolPair.check d.arrow;
415    Boolean.check d.record;    BoolRec.check d.record;
416    ()    ()
417    
418    
# Line 275  Line 428 
428      (any,any)      (any,any)
429      l      l
430    
   
 let cup_product l =  
   List.fold_left  
     (fun (d1,d2) (t1,t2) -> (cup_t d1 t1, cup_t d2 t2))  
     (empty,empty)  
     l  
   
431  let rec exists max f =  let rec exists max f =
432    (max > 0) && (f (max - 1) || exists (max - 1) f)    (max > 0) && (f (max - 1) || exists (max - 1) f)
433    
434    let trivially_empty d = equal_descr d empty
435    
436  module Assumptions = Set.Make(struct type t = descr let compare = compare end)  exception NotEmpty
437    
438  let memo = ref Assumptions.empty  type slot = { mutable status : status;
439  let cache_false = ref Assumptions.empty                 mutable notify : notify;
440                   mutable active : bool }
441    and status = Empty | NEmpty | Maybe
442    and notify = Nothing | Do of slot * (slot -> unit) * notify
443    
444    let memo = DescrHash.create 33000
445    
446    let marks = ref []
447    let slot_empty = { status = Empty; active = false; notify = Nothing }
448    let slot_not_empty = { status = NEmpty; active = false; notify = Nothing }
449    
450    let rec notify = function
451      | Nothing -> ()
452      | Do (n,f,rem) ->
453          if n.status = Maybe then (try f n with NotEmpty -> ());
454          notify rem
455    
456    let rec iter_s s f = function
457      | [] -> ()
458      | arg::rem -> f arg s; iter_s s f rem
459    
460    
461    let set s =
462      s.status <- NEmpty;
463      notify s.notify;
464      raise NotEmpty
465    
466    let rec big_conj f l n =
467      match l with
468        | [] -> set n
469        | [arg] -> f arg n
470        | arg::rem ->
471            let s = { status = Maybe; active = false; notify = Do (n,(big_conj f rem), Nothing) } in
472            try
473              f arg s;
474              if s.active then n.active <- true
475            with NotEmpty -> if n.status = NEmpty then raise NotEmpty
476    
477    
478    let rec guard a f n =
479      match slot a with
480        | { status = Empty } -> ()
481        | { status = Maybe } as s -> n.active <- true; s.notify <- Do (n,f,s.notify)
482        | { status = NEmpty } -> f n
483    
484    and slot d =
485      if not ((Intervals.is_empty d.ints) &&
486              (Atoms.is_empty d.atoms) &&
487              (Chars.is_empty d.chars) &&
488              (not d.absent)) then slot_not_empty
489      else try DescrHash.find memo d
490      with Not_found ->
491        let s = { status = Maybe; active = false; notify = Nothing } in
492        DescrHash.add memo d s;
493        (try
494           iter_s s check_times (BoolPair.get d.times);
495           iter_s s check_times (BoolPair.get d.xml);
496           iter_s s check_arrow (BoolPair.get d.arrow);
497           iter_s s check_record (get_record d.record);
498           if s.active then marks := s :: !marks else s.status <- Empty;
499         with
500             NotEmpty -> ());
501        s
502    
503    and check_times (left,right) s =
504      let rec aux accu1 accu2 right s = match right with
505        | (t1,t2)::right ->
506            if trivially_empty (cap_t accu1 t1) ||
507               trivially_empty (cap_t accu2 t2) then
508                 aux accu1 accu2 right s
509            else
510              let accu1' = diff_t accu1 t1 in guard accu1' (aux accu1' accu2 right) s;
511              let accu2' = diff_t accu2 t2 in guard accu2' (aux accu1 accu2' right) s
512        | [] -> set s
513      in
514      let (accu1,accu2) = cap_product left in
515      guard accu1 (guard accu2 (aux accu1 accu2 right)) s
516    
517    and check_arrow (left,right) s =
518      let single_right (s1,s2) s =
519        let rec aux accu1 accu2 left s = match left with
520          | (t1,t2)::left ->
521              let accu1' = diff_t accu1 t1 in guard accu1' (aux accu1' accu2 left) s;
522              let accu2' = cap_t  accu2 t2 in guard accu2' (aux accu1 accu2' left) s
523          | [] -> set s
524        in
525        let accu1 = descr s1 in
526        guard accu1 (aux accu1 (neg (descr s2)) left) s
527      in
528      big_conj single_right right s
529    
530    and check_record (labels,(oleft,left),rights) s =
531      let rec aux rights s = match rights with
532        | [] -> set s
533        | (oright,right)::rights ->
534            let next =
535              (oleft && (not oright)) || (* ggg... why ???  check this line *)
536              exists (Array.length left)
537                (fun i ->
538                   trivially_empty (cap left.(i) right.(i)))
539            in
540            if next then aux rights s
541            else
542              for i = 0 to Array.length left - 1 do
543                let back = left.(i) in
544                let di = diff back right.(i) in
545                guard di (fun s ->
546                            left.(i) <- diff back right.(i);
547                            aux rights s;
548                            left.(i) <- back;
549                         ) s
550              done
551      in
552      let rec start i s =
553        if (i < 0) then aux rights s
554        else
555          guard left.(i) (start (i - 1)) s
556      in
557      start (Array.length left - 1) s
558    
559    
560    let is_empty d =
561      let s = slot d in
562      List.iter
563        (fun s' -> if s'.status = Maybe then s'.status <- Empty; s'.notify <- Nothing)
564        !marks;
565      marks := [];
566      s.status = Empty
567    
568  exception NotEmpty  
569    module Assumptions = Set.Make(struct type t = descr let compare = compare_descr end)
570    let memo = ref Assumptions.empty
571    let cache_false = DescrHash.create 33000
572    
573  let rec empty_rec d =  let rec empty_rec d =
574    if Assumptions.mem d !cache_false 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  
575    else if not (Atoms.is_empty d.atoms) then false    else if not (Atoms.is_empty d.atoms) then false
576    else if not (Chars.is_empty d.chars) then false    else if not (Chars.is_empty d.chars) then false
577      else if d.absent then false
578      else if DescrHash.mem cache_false d then false
579      else if Assumptions.mem d !memo then true
580    else (    else (
581      let backup = !memo in      let backup = !memo in
582      memo := Assumptions.add d backup;      memo := Assumptions.add d backup;
583      if      if
584        (empty_rec_times d.times) &&        (empty_rec_times (BoolPair.get d.times)) &&
585        (empty_rec_times d.xml) &&        (empty_rec_times (BoolPair.get d.xml)) &&
586        (empty_rec_arrow d.arrow) &&        (empty_rec_arrow (BoolPair.get d.arrow)) &&
587        (empty_rec_record d.record)        (empty_rec_record d.record)
588      then true      then true
589      else (      else (
590        memo := backup;        memo := backup;
591        cache_false := Assumptions.add d !cache_false;        DescrHash.add cache_false d ();
592        false        false
593      )      )
594    )    )
# Line 321  Line 599 
599  and empty_rec_times_aux (left,right) =  and empty_rec_times_aux (left,right) =
600    let rec aux accu1 accu2 = function    let rec aux accu1 accu2 = function
601      | (t1,t2)::right ->      | (t1,t2)::right ->
602  (* This avoids explosion with huge rhs (+/- degenerated partitioning)          if trivially_empty (cap_t accu1 t1) ||
603     May be slower when List.length right is small; could optimize             trivially_empty (cap_t accu2 t2) then
    this case... *)  
         if empty_rec (cap_t accu1 t1) || empty_rec (cap_t accu2 t2) then  
604            aux accu1 accu2 right            aux accu1 accu2 right
605          else          else
606            let accu1' = diff_t accu1 t1 in            let accu1' = diff_t accu1 t1 in
# Line 334  Line 610 
610      | [] -> raise NotEmpty      | [] -> raise NotEmpty
611    in    in
612    let (accu1,accu2) = cap_product left 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  
 *)  
   
613    (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)  
     && *)  
614      (try aux accu1 accu2 right; true with NotEmpty -> false)      (try aux accu1 accu2 right; true with NotEmpty -> false)
615    )  
616    
617  and empty_rec_arrow c =  and empty_rec_arrow c =
618    List.for_all empty_rec_arrow_aux c    List.for_all empty_rec_arrow_aux c
# Line 376  Line 622 
622      let rec aux accu1 accu2 = function      let rec aux accu1 accu2 = function
623        | (t1,t2)::left ->        | (t1,t2)::left ->
624            let accu1' = diff_t accu1 t1 in            let accu1' = diff_t accu1 t1 in
625            if not (empty_rec accu1') then aux accu1 accu2 left;            if not (empty_rec accu1') then aux accu1' accu2 left;
626            let accu2' = cap_t accu2 t2 in            let accu2' = cap_t accu2 t2 in
627            if not (empty_rec accu2') then aux accu1 accu2 left            if not (empty_rec accu2') then aux accu1 accu2' left
628        | [] -> raise NotEmpty        | [] -> raise NotEmpty
629      in      in
630      let accu1 = descr s1 in      let accu1 = descr s1 in
# Line 387  Line 633 
633    in    in
634    List.exists single_right right    List.exists single_right right
635    
636  and empty_rec_record_aux (labels,(oleft,(left_opt,left)),rights) =  and empty_rec_record_aux (labels,(oleft,left),rights) =
637    let rec aux = function    let rec aux = function
638      | [] -> raise NotEmpty      | [] -> raise NotEmpty
639      | (oright,(right_opt,right))::rights ->      | (oright,right)::rights ->
640          let next =          let next =
641            (oleft && (not oright)) ||            (oleft && (not oright)) ||
642            exists (Array.length left)            exists (Array.length left)
643              (fun i ->              (fun i ->
644                 (not (left_opt.(i) && right_opt.(i))) &&                 trivially_empty (cap left.(i) right.(i)))
                (empty_rec (cap left.(i) right.(i))))  
645          in          in
646          if next then aux rights          if next then aux rights
647          else          else
648            for i = 0 to Array.length left - 1 do            for i = 0 to Array.length left - 1 do
649              let back = left.(i) in              let back = left.(i) in
             let oback = left_opt.(i) in  
             let odi = oback && (not right_opt.(i)) in  
650              let di = diff back right.(i) in              let di = diff back right.(i) in
651              if odi || not (empty_rec di) then (              if not (empty_rec di) then (
652                left.(i) <- diff back right.(i);                left.(i) <- diff back right.(i);
               left_opt.(i) <- odi;  
653                aux rights;                aux rights;
654                left.(i) <- back;                left.(i) <- back;
               left_opt.(i) <- oback;  
655              )              )
656            done            done
657    in    in
658    exists (Array.length left)    exists (Array.length left)
659      (fun i -> not left_opt.(i) && (empty_rec left.(i)))      (fun i -> empty_rec left.(i))
660    ||    ||
661    (try aux rights; true with NotEmpty -> false)    (try aux rights; true with NotEmpty -> false)
662    
663    
664  and empty_rec_record c =  and empty_rec_record c =
 (*  
   let aux = List.exists (fun (_,(opt,t)) -> (not opt) && (empty_rec t)) in  
 *)  
665    List.for_all empty_rec_record_aux (get_record c)    List.for_all empty_rec_record_aux (get_record c)
666    
667    (*
668  let is_empty d =  let is_empty d =
669  (*  Printf.eprintf "+"; flush stderr; *)    empty_rec d
670    let old = !memo in    *)
   let r = empty_rec d in  
   if not r then memo := old;  
 (*  cache_false := Assumptions.empty;  *)  
 (*  Printf.eprintf "-\n"; flush stderr; *)  
   r  
671    
672  let non_empty d =  let non_empty d =
673    not (is_empty d)    not (is_empty d)
# Line 462  Line 696 
696          | [] -> res := (ref (t1,t2)) :: !res          | [] -> res := (ref (t1,t2)) :: !res
697          | ({contents = (d1,d2)} as r)::l ->          | ({contents = (d1,d2)} as r)::l ->
698              (*OPT*)              (*OPT*)
699              if d1 = t1 then r := (d1,cup d2 t2) else  (*          if equal_descr d1 t1 then r := (d1,cup d2 t2) else*)
700    
701                let i = cap t1 d1 in                let i = cap t1 d1 in
702                if is_empty i then loop t1 t2 l                if is_empty i then loop t1 t2 l
# Line 529  Line 763 
763              ) right in              ) right in
764          if non_empty !resid1 then accu := (!resid1, d2) :: !accu          if non_empty !resid1 then accu := (!resid1, d2) :: !accu
765      in      in
766      List.iter line d;      List.iter line (BoolPair.get d);
767      !accu      !accu
768  (* Maybe, can improve this function with:  (* Maybe, can improve this function with:
769       (t,s) \ (t1,s1) = (t&t',s\s') | (t\t',s),       (t,s) \ (t1,s1) = (t&t',s\s') | (t\t',s),
770     don't call normal_aux *)     don't call normal_aux *)
771    
772    
773    let get ?(kind=`Normal) d =    let get ?(kind=`Normal) d =
774      match kind with      match kind with
775        | `Normal -> get_aux d.times        | `Normal -> get_aux d.times
# Line 542  Line 777 
777    
778    let pi1 = List.fold_left (fun acc (t1,_) -> cup acc t1) empty    let pi1 = List.fold_left (fun acc (t1,_) -> cup acc t1) empty
779    let pi2 = List.fold_left (fun acc (_,t2) -> cup acc t2) empty    let pi2 = List.fold_left (fun acc (_,t2) -> cup acc t2) empty
780      let pi2_restricted restr =
781        List.fold_left (fun acc (t1,t2) ->
782                          if is_empty (cap t1 restr) then acc
783                          else cup acc t2) empty
784    
785    let restrict_1 rects pi1 =    let restrict_1 rects pi1 =
786      let aux accu (t1,t2) =      let aux acc (t1,t2) =
787        let t1 = cap t1 pi1 in if is_empty t1 then accu else (t1,t2)::accu in        let t1 = cap t1 pi1 in if is_empty t1 then acc else (t1,t2)::acc in
788      List.fold_left aux [] rects      List.fold_left aux [] rects
789    
790    type normal = t    type normal = t
791    
792    module Memo = Map.Make(struct    module Memo = Map.Make(struct type t = descr BoolPair.t let compare = BoolPair.compare end)
                            type t = (node * node) Boolean.t  
                            let compare = compare end)  
   
793    
794    
795    let memo = ref Memo.empty    let memo = ref Memo.empty
# Line 581  Line 817 
817      | [h] -> h ppf      | [h] -> h ppf
818      | h::t -> Format.fprintf ppf "@[%t |@ %a@]" h print_union t      | h::t -> Format.fprintf ppf "@[%t |@ %a@]" h print_union t
819    
   let print_atom ppf a =  
     Format.fprintf ppf "`%s" (AtomPool.value a)  
   
820    let print_tag ppf a =    let print_tag ppf a =
821      match Atoms.is_atom a with      match Atoms.is_atom a with
822        | Some a -> Format.fprintf ppf "%s" (AtomPool.value a)        | Some a -> Format.fprintf ppf "%s" (Atoms.value a)
823        | None ->        | None -> Format.fprintf ppf "(%a)" print_union (Atoms.print a)
           Format.fprintf ppf "(%a)"  
             print_union  
                (Atoms.print "Atom" print_atom a)  
824    
825    let print_const ppf = function    let print_const ppf = function
826      | Integer i -> Format.fprintf ppf "%s" (Big_int.string_of_big_int i)      | Integer i -> Intervals.print_v ppf i
827      | Atom a -> print_atom ppf a      | Atom a -> Atoms.print_v ppf a
828      | Char c -> Chars.Unichar.print ppf c      | Char c -> Chars.print_v ppf c
829    
830    let named = State.ref "Types.Printf.named" DescrMap.empty    let named = State.ref "Types.Printf.named" DescrMap.empty
831    let register_global name d =    let register_global name d =
# Line 610  Line 840 
840  (* TODO:  (* TODO:
841     check that these generated names does not conflict with declared types *)     check that these generated names does not conflict with declared types *)
842    
843    let bool_iter f b =    let trivial_rec b = b = BoolRec.empty || b = BoolRec.full
844      List.iter (fun (p,n) -> List.iter f p; List.iter f n) b    let trivial_pair b = b = BoolPair.empty || b = BoolPair.full
   
   let trivial b = b = Boolean.empty || b = Boolean.full  
845    
846    let worth_abbrev d =    let worth_abbrev d =
847      not (trivial d.times && trivial d.arrow && trivial d.record)      not (trivial_pair d.times && trivial_pair d.xml &&
848             trivial_pair d.arrow && trivial_rec d.record)
849    
850    let rec mark n = mark_descr (descr n)    let rec mark n = mark_descr (descr n)
851    and mark_descr d =    and mark_descr d =
# Line 629  Line 858 
858            wh := (na,d) :: !wh            wh := (na,d) :: !wh
859        with Not_found ->        with Not_found ->
860          DescrHash.add marks d (ref None);          DescrHash.add marks d (ref None);
861          bool_iter (fun (n1,n2) -> mark n1; mark n2) d.times;          BoolPair.iter (fun (n1,n2) -> mark n1; mark n2) d.times;
862          bool_iter          BoolPair.iter
863            (fun (n1,n2) -> mark n1; mark n2            (fun (n1,n2) -> mark n1; mark n2
864  (*  (*
865               List.iter               List.iter
# Line 649  Line 878 
878                 (Product.normal (descr n2))                 (Product.normal (descr n2))
879  *)  *)
880            ) d.xml;            ) d.xml;
881          bool_iter (fun (n1,n2) -> mark n1; mark n2) d.arrow;          BoolPair.iter (fun (n1,n2) -> mark n1; mark n2) d.arrow;
882          bool_iter (fun (o,l) -> List.iter (fun (l,(o,n)) -> mark n) l) d.record          BoolRec.iter
883              (fun (o,l) -> List.iter (fun (l,n) -> mark n) (LabelMap.get l))
884              d.record
885    
886    
887    let rec print ppf n = print_descr ppf (descr n)    let rec print ppf n = print_descr ppf (descr n)
# Line 667  Line 898 
898            Not_found -> assert false            Not_found -> assert false
899    and real_print_descr ppf d =    and real_print_descr ppf d =
900      if d = any then Format.fprintf ppf "Any" else      if d = any then Format.fprintf ppf "Any" else
901          (
902            if d.absent then Format.fprintf ppf "?";
903        print_union ppf        print_union ppf
904          (Intervals.print d.ints @          (Intervals.print d.ints @
905           Chars.print d.chars @           Chars.print d.chars @
906           Atoms.print "Atom" print_atom d.atoms @             Atoms.print d.atoms @
907           Boolean.print "Pair" print_times d.times @             BoolPair.print "Pair" print_times d.times @
908           Boolean.print "XML" print_xml d.xml @             BoolPair.print "XML" print_xml d.xml @
909           Boolean.print "Arrow" print_arrow d.arrow @             BoolPair.print "Arrow" print_arrow d.arrow @
910           Boolean.print "Record" print_record d.record             BoolRec.print "Record" print_record d.record
911              )
912          )          )
913    and print_times ppf (t1,t2) =    and print_times ppf (t1,t2) =
914      Format.fprintf ppf "@[(%a,%a)@]" print t1 print t2      Format.fprintf ppf "@[(%a,%a)@]" print t1 print t2
# Line 697  Line 931 
931      let o = if o then "" else "|" in      let o = if o then "" else "|" in
932      Format.fprintf ppf "@[{%s" o;      Format.fprintf ppf "@[{%s" o;
933      let first = ref true in      let first = ref true in
934      List.iter (fun (l,(o,t)) ->      List.iter (fun (l,t) ->
935                   let sep = if !first then (first := false; "") else ";" in                   let sep = if !first then (first := false; "") else ";" in
936                   Format.fprintf ppf "%s@ @[%s =%s@] %a" sep                   Format.fprintf ppf "%s@ @[%s =@] %a" sep
937                     (LabelPool.value l) (if o then "?" else "") print t                     (LabelPool.value l) print t
938                ) r;                ) (LabelMap.get r);
939      Format.fprintf ppf " %s}@]" o      Format.fprintf ppf " %s}@]" o
940  (*  (*
941    and print_attribs ppf r =    and print_attribs ppf r =
# Line 801  Line 1035 
1035    | x::r -> try f x with Not_found -> find f r    | x::r -> try f x with Not_found -> find f r
1036    
1037  type t =  type t =
1038    | Int of Big_int.big_int    | Int of Intervals.v
1039    | Atom of atom    | Atom of Atoms.v
1040    | Char of Chars.Unichar.t    | Char of Chars.v
1041    | Pair of (t * t)    | Pair of (t * t)
1042    | Xml of (t * t)    | Xml of (t * t)
1043    | Record of (label * t) list    | Record of (label * t) list
# Line 815  Line 1049 
1049    if (Assumptions.mem d memo) || (is_empty d) then raise Not_found    if (Assumptions.mem d memo) || (is_empty d) then raise Not_found
1050    else    else
1051      try Int (Intervals.sample d.ints) with Not_found ->      try Int (Intervals.sample d.ints) with Not_found ->
1052      try Atom (Atoms.sample (fun _ -> AtomPool.dummy_min) d.atoms) with      try Atom (Atoms.sample d.atoms) with
1053          Not_found ->          Not_found ->
1054  (* Here: could create a fresh atom ... *)  (* Here: could create a fresh atom ... *)
1055      try Char (Chars.sample d.chars) with Not_found ->      try Char (Chars.sample d.chars) with Not_found ->
1056      try sample_rec_arrow d.arrow with Not_found ->      try sample_rec_arrow (BoolPair.get d.arrow) with Not_found ->
1057    
1058      let memo = Assumptions.add d memo in      let memo = Assumptions.add d memo in
1059      try Pair (sample_rec_times memo d.times) with Not_found ->      try Pair (sample_rec_times memo (BoolPair.get d.times)) with Not_found ->
1060      try Xml (sample_rec_times memo d.xml) with Not_found ->      try Xml (sample_rec_times memo (BoolPair.get d.xml)) with Not_found ->
1061      try sample_rec_record memo d.record with Not_found ->      try sample_rec_record memo d.record with Not_found ->
1062      raise Not_found      raise Not_found
1063    
# Line 874  Line 1108 
1108  and sample_rec_record memo c =  and sample_rec_record memo c =
1109    Record (find (sample_rec_record_aux memo) (get_record c))    Record (find (sample_rec_record_aux memo) (get_record c))
1110    
1111  and sample_rec_record_aux memo (labels,(oleft,(left_opt,left)),rights) =  and sample_rec_record_aux memo (labels,(oleft,left),rights) =
1112    let rec aux = function    let rec aux = function
1113      | [] ->      | [] ->
1114          let l = ref labels and fields = ref [] in          let l = ref labels and fields = ref [] in
1115          for i = 0 to Array.length left - 1 do          for i = 0 to Array.length left - 1 do
           if not left_opt.(i) then  
1116              fields := (List.hd !l, sample_rec memo left.(i))::!fields;              fields := (List.hd !l, sample_rec memo left.(i))::!fields;
1117            l := List.tl !l            l := List.tl !l
1118          done;          done;
1119          raise (FoundSampleRecord (List.rev !fields))          raise (FoundSampleRecord (List.rev !fields))
1120      | (oright,(right_opt,right))::rights ->      | (oright,right)::rights ->
1121          let next = (oleft && (not oright)) in          let next = (oleft && (not oright)) in
1122          if next then aux rights          if next then aux rights
1123          else          else
1124            for i = 0 to Array.length left - 1 do            for i = 0 to Array.length left - 1 do
1125              let back = left.(i) in              let back = left.(i) in
             let oback = left_opt.(i) in  
             let odi = oback && (not right_opt.(i)) in  
1126              let di = diff back right.(i) in              let di = diff back right.(i) in
1127              if odi || not (is_empty di) then (              if not (is_empty di) then (
1128                left.(i) <- diff back right.(i);                left.(i) <- diff back right.(i);
               left_opt.(i) <- odi;  
1129                aux rights;                aux rights;
1130                left.(i) <- back;                left.(i) <- back;
               left_opt.(i) <- oback;  
1131              )              )
1132            done            done
1133    in    in
1134    if exists (Array.length left)    if exists (Array.length left)
1135      (fun i -> not left_opt.(i) && (is_empty left.(i))) then raise Not_found;      (fun i -> is_empty left.(i)) then raise Not_found;
1136    try aux rights; raise Not_found    try aux rights; raise Not_found
1137    with FoundSampleRecord r -> r    with FoundSampleRecord r -> r
1138    
# Line 920  Line 1149 
1149    
1150    
1151    let rec print ppf = function    let rec print ppf = function
1152      | Int i -> Format.fprintf ppf "%s" (Big_int.string_of_big_int i)      | Int i -> Intervals.print_v ppf i
1153      | Atom a ->      | Atom a -> Atoms.print_v ppf a
1154          if a = LabelPool.dummy_min then      | Char c -> Chars.print_v ppf c
           Format.fprintf ppf "(almost any atom)"  
         else  
           Format.fprintf ppf "`%s" (AtomPool.value a)  
     | Char c -> Chars.Unichar.print ppf c  
1155      | Pair (x1,x2) -> Format.fprintf ppf "(%a,%a)" print x1 print x2      | Pair (x1,x2) -> Format.fprintf ppf "(%a,%a)" print x1 print x2
1156      | Xml (x1,x2) -> Format.fprintf ppf "XML(%a,%a)" print x1 print x2      | Xml (x1,x2) -> Format.fprintf ppf "XML(%a,%a)" print x1 print x2
1157      | Record r ->      | Record r ->
# Line 956  Line 1181 
1181    
1182  module Record =  module Record =
1183  struct  struct
1184    type atom = bool * (label, (bool * node)) SortedMap.t    let has_record d = not (is_empty { empty with record = d.record })
1185    type t = atom Boolean.t    let or_absent d = { d with absent = true }
1186      let any_or_absent = or_absent any
1187    let get d = d.record    let has_absent d = d.absent
1188    
1189    module T = struct    module T = struct
1190      type t = descr      type t = descr
1191      let any = any      let any = any_or_absent
1192      let cap = cap      let cap = cap
1193      let cup = cup      let cup = cup
1194      let diff = diff      let diff = diff
1195      let empty = is_empty      let is_empty = is_empty
1196        let empty = empty
1197    end    end
1198    module R = struct    module R = struct
1199      (*Note: Boolean.cap,cup,diff would be ok,      type t = descr
1200        but we add here the simplification rules:      let any = { empty with record = any.record }
1201        { } & r --> r    ; { } | r -> { }      let cap = cap
1202        r \ { } --> Empty *)      let cup = cup
1203        let diff = diff
1204      type t = atom Boolean.t      let is_empty = is_empty
1205      let any = Boolean.full      let empty = empty
     let cap =  Boolean.cap  
     let cup = Boolean.cup  
     let diff = Boolean.diff  
     let empty x = is_empty { empty with record = x }  
1206    end    end
1207    module TR = Normal.Make(T)(R)    module TR = Normal.Make(T)(R)
1208    
1209    let atom = function    let any_record = { empty with record = BoolRec.full }
     | (true,[]) -> Boolean.full  
     | (o,l) -> Boolean.atom (o,l)  
   
   let somefield_possible t =  
     not (R.empty (R.diff t (Boolean.atom (false,[]))))  
   
   let nofield_possible t =  
     not (R.empty (R.cap t (Boolean.atom (false,[]))))  
   
   let restrict_label_absent t l =  
     Boolean.compute_bool  
       (fun (o,r) as x ->  
          try  
            let (lo,_) = List.assoc l r in  
            if lo then atom (o,SortedMap.diff r [l])  
            else Boolean.empty  
          with Not_found -> Boolean.atom x  
       )  
       t  
   
   let restrict_field t l d =  
     (* Is it correct ?  Do we need to keep track of "first component"  
        (value of l) as in label_present, then filter at the end ... ? *)  
     Boolean.compute_bool  
       (fun (o,r) as x ->  
          try  
            let (lo,lt) = List.assoc l r in  
            if (not lo) && (is_empty (cap d (descr lt))) then Boolean.empty  
            else atom (o, SortedMap.diff r [l])  
          with Not_found ->  
            if o then Boolean.atom x else Boolean.empty  
       )  
       t  
1210    
1211      let atom o l =
1212        if o && LabelMap.is_empty l then any_record else
1213        { empty with record = BoolRec.atom (o,l) }
1214    
1215      type zor = Pair of descr * descr | Any
1216    
1217    let label_present (t:t) l : (descr * t) list =    let aux_split d l=
1218      let x =      let f (o,r) =
       Boolean.compute_bool  
         (fun (o,r) as x ->  
1219             try             try
1220               let (_,lt) = List.assoc l r in          let (lt,rem) = LabelMap.assoc_remove l r in
1221               Boolean.atom (descr lt, atom (o, SortedMap.diff r [l]))          Pair (descr lt, atom o rem)
1222             with Not_found ->             with Not_found ->
1223               if o then Boolean.atom (any, Boolean.atom x) else Boolean.empty          if o then
1224          )            if LabelMap.is_empty r then Any else
1225          t              Pair (any_or_absent, { empty with record = BoolRec.atom (o,r) })
1226            else
1227              Pair ({empty with absent = true},
1228                    { empty with record = BoolRec.atom (o,r) })
1229      in      in
1230      TR.boolean x      List.fold_left
1231          (fun b (p,n) ->
1232    let restrict_label_present t l =           let rec aux_p accu = function
1233      Boolean.compute_bool             | x::p ->
1234        (fun (o,r) as x ->                 (match f x with
1235           try                    | Pair (t1,t2) -> aux_p ((t1,t2)::accu) p
1236             Boolean.atom (o, SortedMap.change_exists l (fun (_,lt) -> (false,lt)) r)                    | Any -> aux_p accu p)
1237           with Not_found ->             | [] -> aux_n accu [] n
1238             if o then Boolean.atom           and aux_n p accu = function
1239               (true, SortedMap.union_disj [l, (false,any_node)] r)             | x::n ->
1240             else Boolean.empty                 (match f x with
1241        )                    | Pair (t1,t2) -> aux_n p ((t1,t2)::accu) n
1242        t                    | Any -> b)
1243               | [] -> (p,accu) :: b in
1244             aux_p [] p)
1245          []
1246          (BoolRec.get d.record)
1247    
1248    let project_field t l =    let split (d : descr) l =
1249      let r = label_present t l in      TR.boolean (aux_split d l)
     List.fold_left (fun accu (d,_) -> cup accu d) empty r  
   
   let project t l =  
     let t = get t in  
     let r = label_present t l in  
     if r = [] then raise Not_found else  
       List.fold_left (fun accu (d,_) -> cup accu d) empty r  
   
   type normal =  
       [ `Success  
       | `Fail  
       | `NoField  
       | `SomeField  
       | `Label of label * (descr * normal) list * normal ]  
   
   let first_label t =  
     let min = ref None in  
     let lab l = match !min with  
       | Some l' when l >= l' -> ()  
       | _ -> min := Some l in  
     let aux = function  
       | _,[] -> ()  
       | _,(l,_)::_ -> lab l in  
     Boolean.iter aux t;  
     match !min with  
       | Some l -> `Label l  
       | None ->  
           let n =  
             Boolean.compute  
               ~empty:0  
               ~full:3  
               ~cup:(lor)  
               ~cap:(land)  
               ~diff:(fun a b -> a land lnot b)  
               ~atom:(function (true,[]) -> 3 | (false,[]) -> 1 | _ -> assert false)  
               t in  
           match n with  
             | 0 -> `Fail  
             | 1 -> `NoField  
             | 2 -> `SomeField  
             | _ -> `Success  
   
   
   let normal' t l =  
     let present = label_present t l  
     and absent = restrict_label_absent t l in  
     List.map (fun (d,t) -> d,t) present, absent  
   
   let rec normal_aux t =  
     match first_label t with  
       | `Label l ->  
           let present = label_present t l  
           and absent = restrict_label_absent t l in  
           `Label (l, List.map (fun (d,t) -> d, normal_aux t) present,  
                   normal_aux absent)  
       | `Fail -> `Fail  
       | `Success -> `Success  
       | `NoField -> `NoField  
       | `SomeField -> `SomeField  
1250    
1251    let normal t = normal_aux (get t)    let split_normal d l =
1252        TR.boolean_normal (aux_split d l)
1253    
1254    
1255      let project d l =
1256        let t = TR.pi1 (split d l) in
1257        if t.absent then raise Not_found;
1258        t
1259    
1260    let descr x = { empty with record = x }    let remove_field d l =
1261    let is_empty x = is_empty (descr x)      TR.pi2 (split d l)
 (*  
1262    
1263    type t = (label, (bool * descr)) SortedMap.t list    let first_label d =
1264        let min = ref LabelPool.dummy_max in
1265        let aux (_,r) =
1266          match LabelMap.get r with
1267              (l,_)::_ -> if (l:int) < !min then min := l | _ -> () in
1268        BoolRec.iter aux d.record;
1269        !min
1270    
1271      let empty_cases d =
1272        let x = BoolRec.compute
1273                  ~empty:0 ~full:3 ~cup:(lor) ~cap:(land)
1274                  ~diff:(fun a b -> a land lnot b)
1275                  ~atom:(function (o,r) ->
1276                           assert (LabelMap.get r = []);
1277                           if o then 3 else 1
1278                        )
1279                  d.record in
1280        (x land 2 <> 0, x land 1 <> 0)
1281    
   let get d =  
     let line r = List.for_all (fun (l,(o,d)) -> o || non_empty d) r in  
     List.filter line (get_record d.record)  
   
   let restrict_label_present t l =  
     let restr = function  
       | (true, d) -> if non_empty d then (false,d) else raise Exit  
       | x -> x in  
     let aux accu r =  
       try SortedMap.change l restr (false,any) r :: accu  
       with Exit -> accu in  
     List.fold_left aux [] t  
   
   let restrict_label_absent t l =  
     let restr = function (true, _) -> (true,empty) | _ -> raise Exit in  
     let aux accu r =  
       try SortedMap.change l restr (true,empty) r :: accu  
       with Exit -> accu in  
     List.fold_left aux [] t  
   
   let restrict_field t l d =  
     let restr (_,d1) =  
       let d1 = cap d d1 in  
       if is_empty d1 then raise Exit else (false,d1) in  
     let aux accu r =  
       try SortedMap.change l restr (false,d) r :: accu  
       with Exit -> accu in  
     List.fold_left aux [] t  
   
   let project_field t l =  
     let aux accu x =  
       match List.assoc l x with  
         | (false,t) -> cup accu t  
         | _ -> raise Not_found  
     in  
     List.fold_left aux empty t  
1282    
1283    let project d l =  (*TODO: optimize merge
1284      project_field (get_record d.record) l     - pre-compute the sequence of labels
1285       - remove empty or full { l = t }
1286    *)
1287    
1288    type normal =    let merge d1 d2 =
1289        [ `Success      let res = ref empty in
1290        | `Fail      let rec aux accu d1 d2 =
1291        | `Label of label * (descr * normal) list * normal ]        let l = min (first_label d1) (first_label d2) in
1292          if l = LabelPool.dummy_max then
1293    let rec merge_record n r =          let (some1,none1) = empty_cases d1
1294      match (n, r) with          and (some2,none2) = empty_cases d2 in
1295        | (`Success, _) | (_, []) -> `Success          let none = none1 && none2 and some = some1 || some2 in
1296        | (`Fail, r) ->          let accu = LabelMap.from_list (fun _ _ -> assert false) accu in
1297            let aux (l,(o,t)) n =          (* approx for the case (some && not none) ... *)
1298              `Label (l, [t,n], if o then n else `Fail) in          res := cup !res (record' (some, accu))
           List.fold_right aux r `Success  
       | (`Label (l1,present,absent), (l2,(o,t2))::r') ->  
           if (l1 < l2) then  
             let pr =  List.map (fun (t,x) -> (t, merge_record x r)) present in  
             let t = List.fold_left (fun a (t,_) -> diff a t) any present in  
             let pr =  
               if non_empty t then (t, merge_record `Fail r) :: pr  
               else pr in  
             `Label (l1,pr,merge_record absent r)  
           else if (l2 < l1) then  
             let n' = merge_record n r' in  
             `Label (l2, [t2, n'], if o then n' else n)  
1299            else            else
1300              let res = ref [] in          let l1 = split d1 l and l2 = split d2 l in
1301              let aux a (t,x) =          let loop (t1,d1) (t2,d2) =
1302                (let t = diff t t2 in            let t =
1303                 if non_empty t then res := (t,x) :: !res);              if t2.absent
1304                (let t = cap t t2 in              then cup t1 { t2 with absent = false }
1305                 if non_empty t then res := (t, merge_record x r') :: !res);              else t2
               diff a t  
1306              in              in
1307              let t2 = List.fold_left aux t2 present in            aux ((l,cons t)::accu) d1 d2
1308              let () =          in
1309                if non_empty t2 then          List.iter (fun x -> List.iter (loop x) l2) l1
               res := (t2, merge_record `Fail r') :: !res in  
             let abs = if o then merge_record absent r' else absent in  
             `Label (l1, !res, abs)  
   
   module Unify = Map.Make(struct type t = normal let compare = compare end)  
   
   let repository = ref Unify.empty  
   
   let rec canonize = function  
     | `Label (l,pr,ab) as x ->  
         (try Unify.find x !repository  
          with Not_found ->  
            let pr = List.map (fun (t,n) -> canonize n,t) pr in  
            let pr = SortedMap.from_list cup pr in  
            let pr = List.map (fun (n,t) -> (t,n)) pr in  
            let x = `Label (l, pr, canonize ab) in  
            try Unify.find x !repository  
            with Not_found -> repository := Unify.add x x !repository; x  
         )  
     | x -> x  
   
   let normal d =  
     let r = canonize (List.fold_left merge_record `Fail (get d)) in  
     repository := Unify.empty;  
     r  
   
   type normal' =  
       [ `Success  
       | `Label of label * (descr * descr) list * descr option ] option  
   
 (* NOTE: this function relies on the fact that generic order  
          makes smallest labels appear first *)  
   
   let first_label d =  
     let d = d.record in  
     let min = ref None in  
     let lab (l,o,t) = match !min with  
       | Some l' when l >= l' -> ()  
       | _ -> if o && (descr t = any) then () else min := Some l in  
     let line (p,n) =  
       (match p with f::_ -> lab f | _ -> ());  
       (match n with f::_ -> lab f | _ -> ()) in  
     List.iter line d;  
     match !min with  
       | None -> if d = [] then `Empty else `Any  
       | Some l -> `Label l  
   
   let normal' (d : descr) l =  
     let ab = ref empty in  
     let rec extract f = function  
       | (l',o,t) :: rem when l = l' ->  
           f o (descr t); extract f rem  
       | x :: rem -> x :: (extract f rem)  
       | [] -> [] in  
     let line (p,n) =  
       let ao = ref true and ad = ref any in  
       let p =  
         extract (fun o d -> ao := !ao && o; ad := cap !ad d) p  
       and n =  
         extract (fun o d -> ao := !ao && not o; ad := diff !ad d) n  
       in  
       (* Note: p and n are still sorted *)  
       let d = { empty with record = [(p,n)] } in  
       if !ao then ab := cup d !ab;  
       (!ad, d) in  
     let pr = List.map line d.record in  
     let pr = Product.normal_aux pr in  
     let ab = if is_empty !ab then None else Some !ab in  
     (pr, ab)  
1310    
1311  *)      in
1312        aux [] d1 d2;
1313        !res
1314    
1315    let any = { empty with record = any.record }    let any = { empty with record = any.record }
 (*  
   let is_empty d = d = []  
   let descr l =  
     let line l = map_sort (fun (l,(o,d)) -> (l,o,cons d)) l, [] in  
     { empty with record = map_sort line l }  
 *)  
1316  end  end
1317    
1318    
# Line 1286  Line 1326 
1326      let n = make () in      let n = make () in
1327      memo_normalize := DescrMap.add d n !memo_normalize;      memo_normalize := DescrMap.add d n !memo_normalize;
1328      let times =      let times =
1329        map_sort        List.fold_left
1330          (fun (d1,d2) -> [(rec_normalize d1, rec_normalize d2)],[])          (fun accu (d1,d2) -> BoolPair.cup accu (BoolPair.atom (rec_normalize d1, rec_normalize d2)))
1331          (Product.normal d)          BoolPair.empty (Product.normal d)
1332      in      in
1333      let xml =      let xml =
1334        map_sort        List.fold_left
1335          (fun (d1,d2) -> [(rec_normalize d1, rec_normalize d2)],[])          (fun accu (d1,d2) -> BoolPair.cup accu (BoolPair.atom (rec_normalize d1, rec_normalize d2)))
1336          (Product.normal ~kind:`XML d)          BoolPair.empty (Product.normal ~kind:`XML d)
1337      in      in
1338      let record = d.record      let record = d.record
1339  (*  (*
# Line 1324  Line 1364 
1364      (try aux accu1 (diff any (descr s2)) left; true with NotEmpty -> false)      (try aux accu1 (diff any (descr s2)) left; true with NotEmpty -> false)
1365    
1366    let check_strenghten t s =    let check_strenghten t s =
1367      let left = match t.arrow with [ (p,[]) ] -> p | _ -> assert false in      let left = match (BoolPair.get t.arrow) with [ (p,[]) ] -> p | _ -> assert false in
1368      let rec aux = function      let rec aux = function
1369        | [] -> raise Not_found        | [] -> raise Not_found
1370        | (p,n) :: rem ->        | (p,n) :: rem ->
1371            if (List.for_all (fun (a,b) -> check_simple left a b) p) &&            if (List.for_all (fun (a,b) -> check_simple left a b) p) &&
1372              (List.for_all (fun (a,b) -> not (check_simple left a b)) n) then              (List.for_all (fun (a,b) -> not (check_simple left a b)) n) then
1373                { empty with arrow = [ (SortedList.cup left p, n) ] }                { empty with arrow = Obj.magic [ (SortedList.cup left p, n) ] }  (* rework this ! *)
1374            else aux rem            else aux rem
1375      in      in
1376      aux s.arrow      aux (BoolPair.get s.arrow)
1377    
1378    let check_simple_iface left s1 s2 =    let check_simple_iface left s1 s2 =
1379      let rec aux accu1 accu2 = function      let rec aux accu1 accu2 = function
# Line 1356  Line 1396 
1396             (List.for_all (fun (a,b) -> not (check_simple_iface iface a b)) n))             (List.for_all (fun (a,b) -> not (check_simple_iface iface a b)) n))
1397            || (aux rem)            || (aux rem)
1398      in      in
1399      aux s.arrow      aux (BoolPair.get s.arrow)
1400    
1401    type t = descr * (descr * descr) list list    type t = descr * (descr * descr) list list
1402    
# Line 1374  Line 1414 
1414           )           )
1415        )        )
1416        (any, [])        (any, [])
1417        t.arrow        (BoolPair.get t.arrow)
1418    
1419    let domain (dom,_) = dom    let domain (dom,_) = dom
1420    
# Line 1434  Line 1474 
1474    let any = { empty with chars = Chars.any }    let any = { empty with chars = Chars.any }
1475  end  end
1476    
1477    let print_stat ppf =
1478    (*  Format.fprintf ppf "nb_rec = %i@." !nb_rec;
1479      Format.fprintf ppf "nb_norec = %i@." !nb_norec;
1480    *)
1481      ()
1482    
1483  (*  (*
1484  let rec print_normal_record ppf = function  let rec print_normal_record ppf = function
1485    | Success -> Format.fprintf ppf "Yes"    | Success -> Format.fprintf ppf "Yes"
Legend:
Removed from v.169  
changed lines
  Added in v.240
CVS Admin">CVS Admin
 ViewVC Help
Powered by ViewVC 1.1.5