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

Diff of /types/types.ml

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

revision 131 by abate, Tue Jul 10 17:09:08 2007 UTC revision 245 by abate, Tue Jul 10 17:18:53 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    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;
     atoms : atom Atoms.t;  
     times : ('a * 'a) Boolean.t;  
     xml   : ('a * 'a) Boolean.t;  
     arrow : ('a * 'a) Boolean.t;  
     record: (label * bool * 'a) Boolean.t;  
92      chars : Chars.t;      chars : Chars.t;
93    }    times : descr BoolPair.t;
94      xml   : descr BoolPair.t;
95      arrow : descr BoolPair.t;
96      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 = { empty with record = Boolean.atom (label,opt,t) }  let record label t =
129      { empty with record = BoolRec.atom (true,LabelMap.singleton label t) }
130    let record' (x : bool * node Ident.label_map) =
131      { 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 66  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 r1 r2 =
239      (r1 == r2) ||
240      match (r1,r2) with
241        | (l1,x1)::r1,(l2,x2)::r2 ->
242            (x1.id = x2.id) && (l1 == l2) && (equal_rec r1 r2)
243        | _ -> false
244    
245    let rec equal_rec_list l1 l2  =
246      (l1 == l2) ||
247      match (l1,l2) with
248        | (o1,r1)::l1, (o2,r2)::l2 ->
249            (o1 == o2) &&
250            (equal_rec r1 r2) && (equal_rec_list l1 l2)
251        | _ -> false
252    
253    let rec equal_rec_bool l1 l2 =
254      (l1 == l2) ||
255      match (l1,l2) with
256        | (p1,n1)::l1, (p2,n2)::l2 ->
257            (equal_rec_list p1 p2) &&
258            (equal_rec_list n1 n2) &&
259            (equal_rec_bool l1 l2)
260        | _ -> false
261    
262    let rec equal_times_list l1 l2  =
263      (l1 == l2) ||
264      match (l1,l2) with
265        | (x1,y1)::l1, (x2,y2)::l2 ->
266            (x1.id = x2.id) &&
267            (y1.id = y2.id) &&
268            (equal_times_list l1 l2)
269        | _ -> 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 equal e a b =  
     if a.atoms <> b.atoms then raise NotEqual;  
     if a.chars <> b.chars then raise NotEqual;  
     if a.ints <> b.ints then raise NotEqual;  
     Boolean.equal (fun (x1,x2) (y1,y2) -> e x1 y1; e x2 y2) a.times b.times;  
     Boolean.equal (fun (x1,x2) (y1,y2) -> e x1 y1; e x2 y2) a.xml b.xml;  
     Boolean.equal (fun (x1,x2) (y1,y2) -> e x1 y1; e x2 y2) a.arrow b.arrow;  
     Boolean.equal (fun (l1,o1,x1) (l2,o2,x2) ->  
                      if (l1 <> l2) || (o1 <> o2) then raise NotEqual;  
                      e x1 x2) a.record b.record  
   
   let map f a =  
     { times = Boolean.map (fun (x1,x2) -> (f x1, f x2)) a.times;  
       xml   = Boolean.map (fun (x1,x2) -> (f x1, f x2)) a.xml;  
       arrow = Boolean.map (fun (x1,x2) -> (f x1, f x2)) a.arrow;  
       record= Boolean.map (fun (l,o,x) -> (l,o, f x)) a.record;  
       ints  = a.ints;  
       atoms = a.atoms;  
       chars = a.chars;  
     }  
   
   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 150  Line 355 
355    
356  let print_descr = ref (fun _ _  -> assert false)  let print_descr = ref (fun _ _  -> assert false)
357    
358  (*  let neg x = diff any x
 let define n d = check d; define n d  
 *)  
359    
360  let cons d =  let any_node = cons any
   let n = make () in  
   define n d;  
   internalize n  
361    
362  (*  module LabelS = Set.Make(LabelPool)
 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  
 *)  
   
 let neg x = diff any x  
363    
364  let get_record r =  let get_record r =
365    let add = SortedMap.add (fun (o1,t1) (o2,t2) -> (o1&&o2, cap t1 t2)) in    let labs accu (_,r) =
   let line (p,n) =  
     let accu = List.fold_left  
                  (fun accu (l,o,t) -> add l (o,descr t) accu) [] p in  
366      List.fold_left      List.fold_left
367        (fun accu (l,o,t) -> add l (not o,neg (descr t)) accu) accu n in        (fun accu (l,_) -> LabelS.add l accu) accu (LabelMap.get r) in
368    List.map line r    let extend descrs labs (o,r) =
369        let rec aux i labs r =
370          match labs with
371            | [] -> ()
372            | l1::labs ->
373                match r with
374                  | (l2,x)::r when l1 == l2 ->
375                      descrs.(i) <- cap descrs.(i) (descr x);
376                      aux (i+1) labs r
377                  | r ->
378                      if not o then descrs.(i) <-
379                        cap descrs.(i) { empty with absent = true };
380                      aux (i+1) labs r
381        in
382        aux 0 labs (LabelMap.get r);
383        o
384      in
385      let line (p,n) =
386        let labels =
387          List.fold_left labs (List.fold_left labs LabelS.empty p) n in
388        let labels = LabelS.elements labels in
389        let nlab = List.length labels in
390        let mk () = Array.create nlab { any with absent = true } in
391    
392        let pos = mk () in
393        let opos = List.fold_left
394                     (fun accu x ->
395                        (extend pos labels x) && accu)
396                     true p in
397        let p = (opos, pos) in
398    
399        let n = List.map (fun x ->
400                            let neg = mk () in
401                            let o = extend neg labels x in
402                            (o,neg)
403                         ) n in
404        (labels,p,n)
405      in
406      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 211  Line 428 
428      (any,any)      (any,any)
429      l      l
430    
431    let rec exists max f =
432      (max > 0) && (f (max - 1) || exists (max - 1) f)
433    
434  let cup_product l =  let trivially_empty d = equal_descr d empty
   List.fold_left  
     (fun (d1,d2) (t1,t2) -> (cup_t d1 t1, cup_t d2 t2))  
     (empty,empty)  
     l  
435    
436    exception NotEmpty
437    
438  module Assumptions = Set.Make(struct type t = descr let compare = compare end)  type slot = { mutable status : status;
439                   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 memo = ref Assumptions.empty  let rec iter_s s f = function
457  let cache_false = ref Assumptions.empty    | [] -> ()
458      | arg::rem -> f arg s; iter_s s f rem
459    
460  exception NotEmpty  
461    let set s =
462      s.status <- NEmpty;
463      notify s.notify;
464    (*  s.notify <- Nothing; *)
465      raise NotEmpty
466    
467    let rec big_conj f l n =
468      match l with
469        | [] -> set n
470        | [arg] -> f arg n
471        | arg::rem ->
472            let s = { status = Maybe; active = false; notify = Do (n,(big_conj f rem), Nothing) } in
473            try
474              f arg s;
475              if s.active then n.active <- true
476            with NotEmpty -> if n.status = NEmpty then raise NotEmpty
477    
478    
479    let rec guard a f n =
480      match slot a with
481        | { status = Empty } -> ()
482        | { status = Maybe } as s -> n.active <- true; s.notify <- Do (n,f,s.notify)
483        | { status = NEmpty } -> f n
484    
485    and slot d =
486      if not ((Intervals.is_empty d.ints) &&
487              (Atoms.is_empty d.atoms) &&
488              (Chars.is_empty d.chars) &&
489              (not d.absent)) then slot_not_empty
490      else try DescrHash.find memo d
491      with Not_found ->
492        let s = { status = Maybe; active = false; notify = Nothing } in
493        DescrHash.add memo d s;
494        (try
495           iter_s s check_times (BoolPair.get d.times);
496           iter_s s check_times (BoolPair.get d.xml);
497           iter_s s check_arrow (BoolPair.get d.arrow);
498           iter_s s check_record (get_record d.record);
499           if s.active then marks := s :: !marks else s.status <- Empty;
500         with
501             NotEmpty -> ());
502        s
503    
504    and check_times (left,right) s =
505      let rec aux accu1 accu2 right s = match right with
506        | (t1,t2)::right ->
507            if trivially_empty (cap_t accu1 t1) ||
508               trivially_empty (cap_t accu2 t2) then
509                 aux accu1 accu2 right s
510            else
511              let accu1' = diff_t accu1 t1 in guard accu1' (aux accu1' accu2 right) s;
512              let accu2' = diff_t accu2 t2 in guard accu2' (aux accu1 accu2' right) s
513        | [] -> set s
514      in
515      let (accu1,accu2) = cap_product left in
516      guard accu1 (guard accu2 (aux accu1 accu2 right)) s
517    
518    and check_arrow (left,right) s =
519      let single_right (s1,s2) s =
520        let rec aux accu1 accu2 left s = match left with
521          | (t1,t2)::left ->
522              let accu1' = diff_t accu1 t1 in guard accu1' (aux accu1' accu2 left) s;
523              let accu2' = cap_t  accu2 t2 in guard accu2' (aux accu1 accu2' left) s
524          | [] -> set s
525        in
526        let accu1 = descr s1 in
527        guard accu1 (aux accu1 (neg (descr s2)) left) s
528      in
529      big_conj single_right right s
530    
531    and check_record (labels,(oleft,left),rights) s =
532      let rec aux rights s = match rights with
533        | [] -> set s
534        | (oright,right)::rights ->
535            let next =
536              (oleft && (not oright)) || (* ggg... why ???  check this line *)
537              exists (Array.length left)
538                (fun i ->
539                   trivially_empty (cap left.(i) right.(i)))
540            in
541            if next then aux rights s
542            else
543              for i = 0 to Array.length left - 1 do
544                let back = left.(i) in
545                let di = diff back right.(i) in
546                guard di (fun s ->
547                            left.(i) <- diff back right.(i);
548                            aux rights s;
549                            left.(i) <- back;
550                         ) s
551              done
552      in
553      let rec start i s =
554        if (i < 0) then aux rights s
555        else
556          guard left.(i) (start (i - 1)) s
557      in
558      start (Array.length left - 1) s
559    
560    
561    let is_empty d =
562      let s = slot d in
563      List.iter
564        (fun s' -> if s'.status = Maybe then s'.status <- Empty; s'.notify <- Nothing)
565        !marks;
566      marks := [];
567      s.status = Empty
568    
569    
570    module Assumptions = Set.Make(struct type t = descr let compare = compare_descr end)
571    let memo = ref Assumptions.empty
572    let cache_false = DescrHash.create 33000
573    
574  let rec empty_rec d =  let rec empty_rec d =
575    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  
576    else if not (Atoms.is_empty d.atoms) then false    else if not (Atoms.is_empty d.atoms) then false
577    else if not (Chars.is_empty d.chars) then false    else if not (Chars.is_empty d.chars) then false
578      else if d.absent then false
579      else if DescrHash.mem cache_false d then false
580      else if Assumptions.mem d !memo then true
581    else (    else (
582      let backup = !memo in      let backup = !memo in
583      memo := Assumptions.add d backup;      memo := Assumptions.add d backup;
584      if      if
585        (empty_rec_times d.times) &&        (empty_rec_times (BoolPair.get d.times)) &&
586        (empty_rec_times d.xml) &&        (empty_rec_times (BoolPair.get d.xml)) &&
587        (empty_rec_arrow d.arrow) &&        (empty_rec_arrow (BoolPair.get d.arrow)) &&
588        (empty_rec_record d.record)        (empty_rec_record d.record)
589      then true      then true
590      else (      else (
591        memo := backup;        memo := backup;
592        cache_false := Assumptions.add d !cache_false;        DescrHash.add cache_false d ();
593        false        false
594      )      )
595    )    )
# Line 254  Line 600 
600  and empty_rec_times_aux (left,right) =  and empty_rec_times_aux (left,right) =
601    let rec aux accu1 accu2 = function    let rec aux accu1 accu2 = function
602      | (t1,t2)::right ->      | (t1,t2)::right ->
603  (* This may avoid explosion with huge rhs ...          if trivially_empty (cap_t accu1 t1) ||
604     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  
605            aux accu1 accu2 right            aux accu1 accu2 right
606          else          else
607            let accu1' = diff_t accu1 t1 in            let accu1' = diff_t accu1 t1 in
# Line 267  Line 611 
611      | [] -> raise NotEmpty      | [] -> raise NotEmpty
612    in    in
613    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  
 *)  
   
614    (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)  
     && *)  
615      (try aux accu1 accu2 right; true with NotEmpty -> false)      (try aux accu1 accu2 right; true with NotEmpty -> false)
616    )  
617    
618  and empty_rec_arrow c =  and empty_rec_arrow c =
619    List.for_all empty_rec_arrow_aux c    List.for_all empty_rec_arrow_aux c
# Line 309  Line 623 
623      let rec aux accu1 accu2 = function      let rec aux accu1 accu2 = function
624        | (t1,t2)::left ->        | (t1,t2)::left ->
625            let accu1' = diff_t accu1 t1 in            let accu1' = diff_t accu1 t1 in
626            if not (empty_rec accu1') then aux accu1 accu2 left;            if not (empty_rec accu1') then aux accu1' accu2 left;
627            let accu2' = cap_t accu2 t2 in            let accu2' = cap_t accu2 t2 in
628            if not (empty_rec accu2') then aux accu1 accu2 left            if not (empty_rec accu2') then aux accu1 accu2' left
629        | [] -> raise NotEmpty        | [] -> raise NotEmpty
630      in      in
631      let accu1 = descr s1 in      let accu1 = descr s1 in
# Line 320  Line 634 
634    in    in
635    List.exists single_right right    List.exists single_right right
636    
637    and empty_rec_record_aux (labels,(oleft,left),rights) =
638      let rec aux = function
639        | [] -> raise NotEmpty
640        | (oright,right)::rights ->
641            let next =
642              (oleft && (not oright)) ||
643              exists (Array.length left)
644                (fun i ->
645                   trivially_empty (cap left.(i) right.(i)))
646            in
647            if next then aux rights
648            else
649              for i = 0 to Array.length left - 1 do
650                let back = left.(i) in
651                let di = diff back right.(i) in
652                if not (empty_rec di) then (
653                  left.(i) <- diff back right.(i);
654                  aux rights;
655                  left.(i) <- back;
656                )
657              done
658      in
659      exists (Array.length left)
660        (fun i -> empty_rec left.(i))
661      ||
662      (try aux rights; true with NotEmpty -> false)
663    
664    
665  and empty_rec_record c =  and empty_rec_record c =
666    let aux = List.exists (fun (_,(opt,t)) -> (not opt) && (empty_rec t)) in    List.for_all empty_rec_record_aux (get_record c)
   List.for_all aux (get_record c)  
667    
668    (*
669  let is_empty d =  let is_empty d =
670  (*  Printf.eprintf "+"; flush stderr; *)    empty_rec d
671    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  
672    
673  let non_empty d =  let non_empty d =
674    not (is_empty d)    not (is_empty d)
# Line 360  Line 697 
697          | [] -> res := (ref (t1,t2)) :: !res          | [] -> res := (ref (t1,t2)) :: !res
698          | ({contents = (d1,d2)} as r)::l ->          | ({contents = (d1,d2)} as r)::l ->
699              (*OPT*)              (*OPT*)
700              if d1 = t1 then r := (d1,cup d2 t2) else  (*          if equal_descr d1 t1 then r := (d1,cup d2 t2) else*)
701    
702                let i = cap t1 d1 in                let i = cap t1 d1 in
703                if is_empty i then loop t1 t2 l                if is_empty i then loop t1 t2 l
# Line 427  Line 764 
764              ) right in              ) right in
765          if non_empty !resid1 then accu := (!resid1, d2) :: !accu          if non_empty !resid1 then accu := (!resid1, d2) :: !accu
766      in      in
767      List.iter line d;      List.iter line (BoolPair.get d);
768      !accu      !accu
769    (* Maybe, can improve this function with:
770         (t,s) \ (t1,s1) = (t&t',s\s') | (t\t',s),
771       don't call normal_aux *)
772    
773    
774    let get ?(kind=`Normal) d =    let get ?(kind=`Normal) d =
775      match kind with      match kind with
# Line 437  Line 778 
778    
779    let pi1 = List.fold_left (fun acc (t1,_) -> cup acc t1) empty    let pi1 = List.fold_left (fun acc (t1,_) -> cup acc t1) empty
780    let pi2 = List.fold_left (fun acc (_,t2) -> cup acc t2) empty    let pi2 = List.fold_left (fun acc (_,t2) -> cup acc t2) empty
781      let pi2_restricted restr =
782        List.fold_left (fun acc (t1,t2) ->
783                          if is_empty (cap t1 restr) then acc
784                          else cup acc t2) empty
785    
786    let restrict_1 rects pi1 =    let restrict_1 rects pi1 =
787      let aux accu (t1,t2) =      let aux acc (t1,t2) =
788        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
789      List.fold_left aux [] rects      List.fold_left aux [] rects
790    
791    type normal = t    type normal = t
792    
793    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)  
   
794    
795    
796    let memo = ref Memo.empty    let memo = ref Memo.empty
# Line 459  Line 801 
801          Not_found ->          Not_found ->
802            let gd = get_aux d in            let gd = get_aux d in
803            let n = normal_aux gd in            let n = normal_aux gd in
804    (* Could optimize this call to normal_aux because one already
805       know that each line is normalized ... *)
806            memo := Memo.add d n !memo;            memo := Memo.add d n !memo;
807            n            n
808    
# Line 474  Line 818 
818      | [h] -> h ppf      | [h] -> h ppf
819      | h::t -> Format.fprintf ppf "@[%t |@ %a@]" h print_union t      | h::t -> Format.fprintf ppf "@[%t |@ %a@]" h print_union t
820    
   let print_atom ppf a =  
     Format.fprintf ppf "`%s" (AtomPool.value a)  
   
821    let print_tag ppf a =    let print_tag ppf a =
822      match Atoms.is_atom a with      match Atoms.is_atom a with
823        | Some a -> Format.fprintf ppf "%s" (AtomPool.value a)        | Some a -> Format.fprintf ppf "%s" (Atoms.value a)
824        | None ->        | None -> Format.fprintf ppf "(%a)" print_union (Atoms.print a)
           Format.fprintf ppf "(%a)"  
             print_union  
                (Atoms.print "Atom" print_atom a)  
825    
826    let print_const ppf = function    let print_const ppf = function
827      | Integer i -> Format.fprintf ppf "%s" (Big_int.string_of_big_int i)      | Integer i -> Intervals.print_v ppf i
828      | Atom a -> print_atom ppf a      | Atom a -> Atoms.print_v ppf a
829      | Char c -> Chars.Unichar.print ppf c      | Char c -> Chars.print_v ppf c
830    
831    let named = State.ref "Types.Printf.named" DescrMap.empty    let named = State.ref "Types.Printf.named" DescrMap.empty
832    let register_global name d =    let register_global name d =
# Line 503  Line 841 
841  (* TODO:  (* TODO:
842     check that these generated names does not conflict with declared types *)     check that these generated names does not conflict with declared types *)
843    
844    let bool_iter f b =    let trivial_rec b = b = BoolRec.empty || b = BoolRec.full
845      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  
846    
847    let worth_abbrev d =    let worth_abbrev d =
848      not (trivial d.times && trivial d.arrow && trivial d.record)      not (trivial_pair d.times && trivial_pair d.xml &&
849             trivial_pair d.arrow && trivial_rec d.record)
850    
851    let rec mark n = mark_descr (descr n)    let rec mark n = mark_descr (descr n)
852    and mark_descr d =    and mark_descr d =
# Line 522  Line 859 
859            wh := (na,d) :: !wh            wh := (na,d) :: !wh
860        with Not_found ->        with Not_found ->
861          DescrHash.add marks d (ref None);          DescrHash.add marks d (ref None);
862          bool_iter (fun (n1,n2) -> mark n1; mark n2) d.times;          BoolPair.iter (fun (n1,n2) -> mark n1; mark n2) d.times;
863          bool_iter          BoolPair.iter
864            (fun (n1,n2) ->            (fun (n1,n2) -> mark n1; mark n2
865    (*
866               List.iter               List.iter
867                 (fun (d1,d2) ->                 (fun (d1,d2) ->
868                    mark_descr d2;                    mark_descr d2;
869                      bool_iter
870                        (fun (o,l) -> List.iter (fun (l,(o,n)) -> mark n) l)
871                        d1.record
872                    let l = get_record d1.record in                    let l = get_record d1.record in
873                    List.iter (List.iter (fun (l,(o,d)) -> mark_descr d)) l                    List.iter (fun labs,(_,(_,p)),ns ->
874                                   Array.iter mark_descr p;
875                                   List.iter (fun (_,(_,n)) ->
876                                                Array.iter mark_descr n) ns
877                                ) l
878                 )                 )
879                 (Product.normal (descr n2))                 (Product.normal (descr n2))
880    *)
881            ) d.xml;            ) d.xml;
882          bool_iter (fun (n1,n2) -> mark n1; mark n2) d.arrow;          BoolPair.iter (fun (n1,n2) -> mark n1; mark n2) d.arrow;
883          bool_iter (fun (l,o,n) -> mark n) d.record          BoolRec.iter
884              (fun (o,l) -> List.iter (fun (l,n) -> mark n) (LabelMap.get l))
885              d.record
886    
887    
888    let rec print ppf n = print_descr ppf (descr n)    let rec print ppf n = print_descr ppf (descr n)
# Line 551  Line 899 
899            Not_found -> assert false            Not_found -> assert false
900    and real_print_descr ppf d =    and real_print_descr ppf d =
901      if d = any then Format.fprintf ppf "Any" else      if d = any then Format.fprintf ppf "Any" else
902          (
903            if d.absent then Format.fprintf ppf "?";
904        print_union ppf        print_union ppf
905          (Intervals.print d.ints @          (Intervals.print d.ints @
906           Chars.print d.chars @           Chars.print d.chars @
907           Atoms.print "Atom" print_atom d.atoms @             Atoms.print d.atoms @
908           Boolean.print "Pair" print_times d.times @             BoolPair.print "Pair" print_times d.times @
909           Boolean.print "XML" print_xml d.xml @             BoolPair.print "XML" print_xml d.xml @
910           Boolean.print "Arrow" print_arrow d.arrow @             BoolPair.print "Arrow" print_arrow d.arrow @
911           Boolean.print "Record" print_record d.record             BoolRec.print "Record" print_record d.record
912              )
913          )          )
914    and print_times ppf (t1,t2) =    and print_times ppf (t1,t2) =
915      Format.fprintf ppf "@[(%a,%a)@]" print t1 print t2      Format.fprintf ppf "@[(%a,%a)@]" print t1 print t2
916    and print_xml ppf (t1,t2) =    and print_xml ppf (t1,t2) =
917        Format.fprintf ppf "@[XML(%a,%a)@]" print t1 print t2
918    (*
919      let l = Product.normal (descr t2) in      let l = Product.normal (descr t2) in
920      let l = List.map      let l = List.map
921                (fun (d1,d2) ppf ->                (fun (d1,d2) ppf ->
# Line 572  Line 925 
925                     print_descr d2) l                     print_descr d2) l
926      in      in
927      print_union ppf l      print_union ppf l
928    *)
929    and print_arrow ppf (t1,t2) =    and print_arrow ppf (t1,t2) =
930      Format.fprintf ppf "@[(%a -> %a)@]" print t1 print t2      Format.fprintf ppf "@[(%a -> %a)@]" print t1 print t2
931    and print_record ppf (l,o,t) =    and print_record ppf (o,r) =
932      Format.fprintf ppf "@[{ %s =%s %a }@]"      let o = if o then "" else "|" in
933        (LabelPool.value l) (if o then "?" else "") print t      Format.fprintf ppf "@[{%s" o;
934        let first = ref true in
935        List.iter (fun (l,t) ->
936                     let sep = if !first then (first := false; "") else ";" in
937                     Format.fprintf ppf "%s@ @[%s =@] %a" sep
938                       (LabelPool.value l) print t
939                  ) (LabelMap.get r);
940        Format.fprintf ppf " %s}@]" o
941    (*
942    and print_attribs ppf r =    and print_attribs ppf r =
943      let l = get_record r in      let l = get_record r in
944      if l <> [ [] ] then      if l <> [ [] ] then
# Line 594  Line 956 
956             Format.fprintf ppf "}"             Format.fprintf ppf "}"
957        ) l in        ) l in
958      print_union ppf l      print_union ppf l
959    *)
960    
961    
962    let end_print ppf =    let end_print ppf =
# Line 667  Line 1030 
1030  module Sample =  module Sample =
1031  struct  struct
1032    
1033    
1034  let rec find f = function  let rec find f = function
1035    | [] -> raise Not_found    | [] -> raise Not_found
1036    | x::r -> try f x with Not_found -> find f r    | x::r -> try f x with Not_found -> find f r
1037    
1038  type t =  type t =
1039    | Int of Big_int.big_int    | Int of Intervals.v
1040    | Atom of atom    | Atom of Atoms.v
1041    | Char of Chars.Unichar.t    | Char of Chars.v
1042    | Pair of (t * t)    | Pair of (t * t)
1043    | Xml of (t * t)    | Xml of (t * t)
1044    | Record of (label * t) list    | Record of (label * t) list
1045    | Fun of (node * node) list    | Fun of (node * node) list
1046      | Other
1047      exception FoundSampleRecord of (label * t) list
1048    
1049  let rec sample_rec memo d =  let rec sample_rec memo d =
1050    if (Assumptions.mem d memo) || (is_empty d) then raise Not_found    if (Assumptions.mem d memo) || (is_empty d) then raise Not_found
1051    else    else
1052      try Int (Intervals.sample d.ints) with Not_found ->      try Int (Intervals.sample d.ints) with Not_found ->
1053      try Atom (Atoms.sample (fun _ -> AtomPool.dummy_min) d.atoms) with      try Atom (Atoms.sample d.atoms) with
1054          Not_found ->          Not_found ->
1055  (* Here: could create a fresh atom ... *)  (* Here: could create a fresh atom ... *)
1056      try Char (Chars.sample d.chars) with Not_found ->      try Char (Chars.sample d.chars) with Not_found ->
1057      try sample_rec_arrow d.arrow with Not_found ->      try sample_rec_arrow (BoolPair.get d.arrow) with Not_found ->
1058    
1059      let memo = Assumptions.add d memo in      let memo = Assumptions.add d memo in
1060      try Pair (sample_rec_times memo d.times) with Not_found ->      try Pair (sample_rec_times memo (BoolPair.get d.times)) with Not_found ->
1061      try Xml (sample_rec_times memo d.xml) with Not_found ->      try Xml (sample_rec_times memo (BoolPair.get d.xml)) with Not_found ->
1062      try sample_rec_record memo d.record with Not_found ->      try sample_rec_record memo d.record with Not_found ->
1063      raise Not_found      raise Not_found
1064    
# Line 703  Line 1069 
1069  and sample_rec_times_aux memo (left,right) =  and sample_rec_times_aux memo (left,right) =
1070    let rec aux accu1 accu2 = function    let rec aux accu1 accu2 = function
1071      | (t1,t2)::right ->      | (t1,t2)::right ->
1072    (*TODO: check: is this correct ?  non_empty could return true
1073      but because of coinduction, the call to aux may raise Not_found, no ? *)
1074          let accu1' = diff_t accu1 t1 in          let accu1' = diff_t accu1 t1 in
1075          if non_empty accu1' then aux accu1' accu2 right else          if non_empty accu1' then aux accu1' accu2 right else
1076            let accu2' = diff_t accu2 t2 in            let accu2' = diff_t accu2 t2 in
# Line 741  Line 1109 
1109  and sample_rec_record memo c =  and sample_rec_record memo c =
1110    Record (find (sample_rec_record_aux memo) (get_record c))    Record (find (sample_rec_record_aux memo) (get_record c))
1111    
1112  and sample_rec_record_aux memo fields =  and sample_rec_record_aux memo (labels,(oleft,left),rights) =
1113    let aux acc (l,(o,t)) = if o then acc else (l, sample_rec memo t) :: acc in    let rec aux = function
1114    List.fold_left aux [] fields      | [] ->
1115            let l = ref labels and fields = ref [] in
1116            for i = 0 to Array.length left - 1 do
1117              fields := (List.hd !l, sample_rec memo left.(i))::!fields;
1118              l := List.tl !l
1119            done;
1120            raise (FoundSampleRecord (List.rev !fields))
1121        | (oright,right)::rights ->
1122            let next = (oleft && (not oright)) in
1123            if next then aux rights
1124            else
1125              for i = 0 to Array.length left - 1 do
1126                let back = left.(i) in
1127                let di = diff back right.(i) in
1128                if not (is_empty di) then (
1129                  left.(i) <- diff back right.(i);
1130                  aux rights;
1131                  left.(i) <- back;
1132                )
1133              done
1134      in
1135      if exists (Array.length left)
1136        (fun i -> is_empty left.(i)) then raise Not_found;
1137      try aux rights; raise Not_found
1138      with FoundSampleRecord r -> r
1139    
1140    
1141    
1142    
1143    
1144  let get x = sample_rec Assumptions.empty x  let get x = try sample_rec Assumptions.empty x with Not_found -> Other
1145    
1146    let rec print_sep f sep ppf = function    let rec print_sep f sep ppf = function
1147      | [] -> ()      | [] -> ()
# Line 754  Line 1150 
1150    
1151    
1152    let rec print ppf = function    let rec print ppf = function
1153      | Int i -> Format.fprintf ppf "%s" (Big_int.string_of_big_int i)      | Int i -> Intervals.print_v ppf i
1154      | Atom a ->      | Atom a -> Atoms.print_v ppf a
1155          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  
1156      | Pair (x1,x2) -> Format.fprintf ppf "(%a,%a)" print x1 print x2      | Pair (x1,x2) -> Format.fprintf ppf "(%a,%a)" print x1 print x2
1157      | 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
1158      | Record r ->      | Record r ->
# Line 782  Line 1174 
1174               )               )
1175               " ; "               " ; "
1176            ) iface            ) iface
1177        | Other ->
1178            Format.fprintf ppf "[cannot determine value]"
1179  end  end
1180    
1181    
1182    
1183  module Record =  module Record =
1184  struct  struct
1185    type t = (label, (bool * descr)) SortedMap.t list    let has_record d = not (is_empty { empty with record = d.record })
1186      let or_absent d = { d with absent = true }
1187      let any_or_absent = or_absent any
1188      let has_absent d = d.absent
1189    
1190    let get d =    let only_absent = {empty with absent = true}
1191      let line r = List.for_all (fun (l,(o,d)) -> o || non_empty d) r in    let only_absent_node = cons only_absent
     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  
1192    
1193    let project d l =    module T = struct
1194      project_field (get_record d.record) l      type t = descr
1195        let any = any_or_absent
1196        let cap = cap
1197        let cup = cup
1198        let diff = diff
1199        let is_empty = is_empty
1200        let empty = empty
1201      end
1202      module R = struct
1203        type t = descr
1204        let any = { empty with record = any.record }
1205        let cap = cap
1206        let cup = cup
1207        let diff = diff
1208        let is_empty = is_empty
1209        let empty = empty
1210      end
1211      module TR = Normal.Make(T)(R)
1212    
1213      let any_record = { empty with record = BoolRec.full }
1214    
1215      let atom o l =
1216        if o && LabelMap.is_empty l then any_record else
1217        { empty with record = BoolRec.atom (o,l) }
1218    
1219      type zor = Pair of descr * descr | Any
1220    
1221    type normal =    let aux_split d l=
1222        [ `Success      let f (o,r) =
1223        | `Fail        try
1224        | `Label of label * (descr * normal) list * normal ]          let (lt,rem) = LabelMap.assoc_remove l r in
1225            Pair (descr lt, atom o rem)
1226    let rec merge_record n r =        with Not_found ->
1227      match (n, r) with          if o then
1228        | (`Success, _) | (_, []) -> `Success            if LabelMap.is_empty r then Any else
1229        | (`Fail, r) ->              Pair (any_or_absent, { empty with record = BoolRec.atom (o,r) })
           let aux (l,(o,t)) n =  
             `Label (l, [t,n], if o then n else `Fail) in  
           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)  
1230            else            else
1231              let res = ref [] in            Pair (only_absent,
1232              let aux a (t,x) =                  { empty with record = BoolRec.atom (o,r) })
               (let t = diff t t2 in  
                if non_empty t then res := (t,x) :: !res);  
               (let t = cap t t2 in  
                if non_empty t then res := (t, merge_record x r') :: !res);  
               diff a t  
1233              in              in
1234              let t2 = List.fold_left aux t2 present in      List.fold_left
1235              let () =        (fun b (p,n) ->
1236                if non_empty t2 then           let rec aux_p accu = function
1237                res := (t2, merge_record `Fail r') :: !res in             | x::p ->
1238              let abs = if o then merge_record absent r' else absent in                 (match f x with
1239              `Label (l1, !res, abs)                    | Pair (t1,t2) -> aux_p ((t1,t2)::accu) p
1240                      | Any -> aux_p accu p)
1241    module Unify = Map.Make(struct type t = normal let compare = compare end)             | [] -> aux_n accu [] n
1242             and aux_n p accu = function
1243    let repository = ref Unify.empty             | x::n ->
1244                   (match f x with
1245    let rec canonize = function                    | Pair (t1,t2) -> aux_n p ((t1,t2)::accu) n
1246      | `Label (l,pr,ab) as x ->                    | Any -> b)
1247          (try Unify.find x !repository             | [] -> (p,accu) :: b in
1248           with Not_found ->           aux_p [] p)
1249             let pr = List.map (fun (t,n) -> canonize n,t) pr in        []
1250             let pr = SortedMap.from_list cup pr in        (BoolRec.get d.record)
1251             let pr = List.map (fun (n,t) -> (t,n)) pr in  
1252             let x = `Label (l, pr, canonize ab) in    let split (d : descr) l =
1253             try Unify.find x !repository      TR.boolean (aux_split d l)
1254             with Not_found -> repository := Unify.add x x !repository; x  
1255          )    let split_normal d l =
1256      | x -> x      TR.boolean_normal (aux_split d l)
1257    
1258    
1259    let normal d =    let project d l =
1260      let r = canonize (List.fold_left merge_record `Fail (get d)) in      let t = TR.pi1 (split d l) in
1261      repository := Unify.empty;      if t.absent then raise Not_found;
1262      r      t
1263    
1264    type normal' =    let project_opt d l =
1265        [ `Success      let t = TR.pi1 (split d l) in
1266        | `Label of label * (descr * descr) list * descr option ] option      { t with absent = false }
1267    
1268      let condition d l t =
1269        TR.pi2_restricted t (split d l)
1270    
1271    (* TODO: eliminate this cap ... (reord l only_absent_node) when
1272       not necessary. eg. {| ..... |} \ l *)
1273    
1274  (* NOTE: this function relies on the fact that generic order    let remove_field d l =
1275           makes smallest labels appear first *)      cap (TR.pi2 (split d l)) (record l only_absent_node)
1276    
1277    let first_label d =    let first_label d =
1278      let d = d.record in      let min = ref LabelPool.dummy_max in
1279      let min = ref None in      let aux (_,r) =
1280      let lab (l,o,t) = match !min with        match LabelMap.get r with
1281        | Some l' when l >= l' -> ()            (l,_)::_ -> if (l:int) < !min then min := l | _ -> () in
1282        | _ -> if o && (descr t = any) then () else min := Some l in      BoolRec.iter aux d.record;
1283      let line (p,n) =      !min
1284        (match p with f::_ -> lab f | _ -> ());  
1285        (match n with f::_ -> lab f | _ -> ()) in    let empty_cases d =
1286      List.iter line d;      let x = BoolRec.compute
1287      match !min with                ~empty:0 ~full:3 ~cup:(lor) ~cap:(land)
1288        | None -> if d = [] then `Empty else `Any                ~diff:(fun a b -> a land lnot b)
1289        | Some l -> `Label l                ~atom:(function (o,r) ->
1290                           assert (LabelMap.get r = []);
1291    let normal' (d : descr) l =                         if o then 3 else 1
1292      let ab = ref empty in                      )
1293      let rec extract f = function                d.record in
1294        | (l',o,t) :: rem when l = l' ->      (x land 2 <> 0, x land 1 <> 0)
1295            f o (descr t); extract f rem  
1296        | x :: rem -> x :: (extract f rem)    let has_empty_record d =
1297        | [] -> [] in      BoolRec.compute
1298      let line (p,n) =        ~empty:false ~full:true ~cup:(||) ~cap:(&&)
1299        let ao = ref true and ad = ref any in        ~diff:(fun a b -> a && not b)
1300        let p =        ~atom:(function (o,r) ->
1301          extract (fun o d -> ao := !ao && o; ad := cap !ad d) p                 List.for_all
1302        and n =                   (fun (l,t) -> (descr t).absent)
1303          extract (fun o d -> ao := !ao && not o; ad := diff !ad d) n                   (LabelMap.get r)
1304        in              )
1305        (* Note: p and n are still sorted *)        d.record
1306        let d = { empty with record = [(p,n)] } in  
1307        if !ao then ab := cup d !ab;  
1308        (!ad, d) in  (*TODO: optimize merge
1309      let pr = List.map line d.record in     - pre-compute the sequence of labels
1310      let pr = Product.normal_aux pr in     - remove empty or full { l = t }
1311      let ab = if is_empty !ab then None else Some !ab in  *)
     (pr, ab)  
1312    
1313      let merge d1 d2 =
1314        let res = ref empty in
1315        let rec aux accu d1 d2 =
1316          let l = min (first_label d1) (first_label d2) in
1317          if l = LabelPool.dummy_max then
1318            let (some1,none1) = empty_cases d1
1319            and (some2,none2) = empty_cases d2 in
1320            let none = none1 && none2 and some = some1 || some2 in
1321            let accu = LabelMap.from_list (fun _ _ -> assert false) accu in
1322            (* approx for the case (some && not none) ... *)
1323            res := cup !res (record' (some, accu))
1324          else
1325            let l1 = split d1 l and l2 = split d2 l in
1326            let loop (t1,d1) (t2,d2) =
1327              let t =
1328                if t2.absent
1329                then cup t1 { t2 with absent = false }
1330                else t2
1331              in
1332              aux ((l,cons t)::accu) d1 d2
1333            in
1334            List.iter (fun x -> List.iter (loop x) l2) l1
1335    
1336        in
1337        aux [] d1 d2;
1338        !res
1339    
1340    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 }  
1341  end  end
1342    
1343    
# Line 954  Line 1351 
1351      let n = make () in      let n = make () in
1352      memo_normalize := DescrMap.add d n !memo_normalize;      memo_normalize := DescrMap.add d n !memo_normalize;
1353      let times =      let times =
1354        map_sort        List.fold_left
1355          (fun (d1,d2) -> [(rec_normalize d1, rec_normalize d2)],[])          (fun accu (d1,d2) -> BoolPair.cup accu (BoolPair.atom (rec_normalize d1, rec_normalize d2)))
1356          (Product.normal d)          BoolPair.empty (Product.normal d)
1357      in      in
1358      let xml =      let xml =
1359        map_sort        List.fold_left
1360          (fun (d1,d2) -> [(rec_normalize d1, rec_normalize d2)],[])          (fun accu (d1,d2) -> BoolPair.cup accu (BoolPair.atom (rec_normalize d1, rec_normalize d2)))
1361          (Product.normal ~kind:`XML d)          BoolPair.empty (Product.normal ~kind:`XML d)
1362      in      in
1363      let record =      let record = d.record
1364    (*
1365        map_sort        map_sort
1366          (fun f -> map_sort (fun (l,(o,d)) -> (l,o,rec_normalize d)) f, [])          (fun f -> map_sort (fun (l,(o,d)) -> (l,o,rec_normalize d)) f, [])
1367          (Record.get d)          (Record.get d)
1368    *)
1369      in      in
1370      define n { d with times = times; xml = xml; record = record };      define n { d with times = times; xml = xml; record = record };
1371      n      n
# Line 990  Line 1389 
1389      (try aux accu1 (diff any (descr s2)) left; true with NotEmpty -> false)      (try aux accu1 (diff any (descr s2)) left; true with NotEmpty -> false)
1390    
1391    let check_strenghten t s =    let check_strenghten t s =
1392      let left = match t.arrow with [ (p,[]) ] -> p | _ -> assert false in      let left = match (BoolPair.get t.arrow) with [ (p,[]) ] -> p | _ -> assert false in
1393      let rec aux = function      let rec aux = function
1394        | [] -> raise Not_found        | [] -> raise Not_found
1395        | (p,n) :: rem ->        | (p,n) :: rem ->
1396            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) &&
1397              (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
1398                { empty with arrow = [ (SortedList.cup left p, n) ] }                { empty with arrow = Obj.magic [ (SortedList.cup left p, n) ] }  (* rework this ! *)
1399            else aux rem            else aux rem
1400      in      in
1401      aux s.arrow      aux (BoolPair.get s.arrow)
1402    
1403    let check_simple_iface left s1 s2 =    let check_simple_iface left s1 s2 =
1404      let rec aux accu1 accu2 = function      let rec aux accu1 accu2 = function
# Line 1022  Line 1421 
1421             (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))
1422            || (aux rem)            || (aux rem)
1423      in      in
1424      aux s.arrow      aux (BoolPair.get s.arrow)
1425    
1426    type t = descr * (descr * descr) list list    type t = descr * (descr * descr) list list
1427    
# Line 1040  Line 1439 
1439           )           )
1440        )        )
1441        (any, [])        (any, [])
1442        t.arrow        (BoolPair.get t.arrow)
1443    
1444    let domain (dom,_) = dom    let domain (dom,_) = dom
1445    
# Line 1093  Line 1492 
1492    
1493  module Atom = struct  module Atom = struct
1494    let has_atom d a = Atoms.contains a d.atoms    let has_atom d a = Atoms.contains a d.atoms
1495      let get d = d.atoms
1496  end  end
1497    
1498  module Char = struct  module Char = struct
1499    let has_char d c = Chars.contains c d.chars    let has_char d c = Chars.contains c d.chars
1500    let any = { empty with chars = Chars.any }    let any = { empty with chars = Chars.any }
1501      let get d = d.chars
1502  end  end
1503    
1504    let print_stat ppf =
1505    (*  Format.fprintf ppf "nb_rec = %i@." !nb_rec;
1506      Format.fprintf ppf "nb_norec = %i@." !nb_norec;
1507    *)
1508      ()
1509    
1510  (*  (*
1511  let rec print_normal_record ppf = function  let rec print_normal_record ppf = function
1512    | Success -> Format.fprintf ppf "Yes"    | Success -> Format.fprintf ppf "Yes"
Legend:
Removed from v.131  
changed lines
  Added in v.245
CVS Admin">CVS Admin
 ViewVC Help
Powered by ViewVC 1.1.5