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

Diff of /types/types.ml

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

revision 19 by abate, Tue Jul 10 16:58:37 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  type label = int      ---> more compact representation, more sharing, ...
 type atom  = int  
14    
15  type const = Integer of Big_int.big_int | Atom of atom | Char of Chars.Unichar.t    * re-consider using BDD-like representation instead of dnf
16    *)
17    
18    
19    let map_sort f l =
20      SortedList.from_list (List.map f l)
21    
22    module HashedString =
23    struct
24      type t = string
25      let hash = Hashtbl.hash
26      let equal = (=)
27    end
28    
29    
30    type const =
31      | Integer of Intervals.v
32      | Atom of Atoms.v
33      | Char of Chars.v
34    
35    type pair_kind = [ `Normal | `XML ]
36    
37    type 'a node0 = { id : int; mutable descr : 'a }
38    
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 I = struct  module RecArg = struct
50    type 'a t = {    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;  
     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      arrow = Boolean.empty;    xml   = BoolPair.empty;
104      record= Boolean.empty;    arrow = BoolPair.empty;
105      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      arrow = Boolean.full;    xml   = BoolPair.full;
115      record= Boolean.full;    arrow = BoolPair.full;
116      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    let interval i j = { empty with ints = Intervals.atom i j }  
124    let times x y = { empty with times = Boolean.atom (x,y) }  let interval i = { empty with ints = i }
125    let arrow x y = { empty with arrow = Boolean.atom (x,y) }  let times x y = { empty with times = BoolPair.atom (x,y) }
126    let record label opt t = { empty with record = Boolean.atom (label,opt,t) }  let xml x y = { empty with xml = BoolPair.atom (x,y) }
127    let arrow x y = { empty with arrow = BoolPair.atom (x,y) }
128    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
135      | Integer i -> interval i i    | Integer i -> interval (Intervals.atom i)
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    
   
   let any_record = { empty with record = any.record }  
   
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        arrow = Boolean.cup x.arrow y.arrow;      xml   = BoolPair.cup x.xml y.xml;
143        record= Boolean.cup x.record y.record;      arrow = BoolPair.cup x.arrow y.arrow;
144        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        record= Boolean.cap x.record y.record;      xml   = BoolPair.cap x.xml y.xml;
155        arrow = Boolean.cap x.arrow y.arrow;      record= BoolRec.cap x.record y.record;
156        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        arrow = Boolean.diff x.arrow y.arrow;      xml   = BoolPair.diff x.xml y.xml;
167        record= Boolean.diff x.record y.record;      arrow = BoolPair.diff x.arrow y.arrow;
168        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 neg x = diff any x  let count = ref 0
176    let make () = incr count; { id = !count; descr = empty }
177    let equal e a b =  let define n d = n.descr <- d
178      if not (Intervals.equal a.ints b.ints) then raise NotEqual;  let cons d = incr count; { id = !count; descr = d }
179      if a.atoms <> b.atoms then raise NotEqual;  let descr n = n.descr
180      if a.chars <> b.chars then raise NotEqual;  let internalize n = n
181      Boolean.equal (fun (x1,x2) (y1,y2) -> e x1 y1; e x2 y2) a.times b.times;  let id n = n.id
182      Boolean.equal (fun (x1,x2) (y1,y2) -> e x1 y1; e x2 y2) a.arrow b.arrow;  
183      Boolean.equal (fun (l1,o1,x1) (l2,o2,x2) ->  let rec compare_rec r1 r2 =
184                       if (l1 <> l2) || (o1 <> o2) then raise NotEqual;    if r1 == r2 then 0
185                       e x1 x2) a.record b.record    else match (r1,r2) with
186        | (l1,x1)::r1,(l2,x2)::r2 ->
187    let map f a =          if ((l1:int) < l2) then -1
188      { times = Boolean.map (fun (x1,x2) -> (f x1, f x2)) a.times;          else if (l1 > l2) then 1
189        arrow = Boolean.map (fun (x1,x2) -> (f x1, f x2)) a.arrow;          else if x1.id < x2.id then -1
190        record= Boolean.map (fun (l,o,x) -> (l,o, f x)) a.record;          else if x1.id > x2.id then 1
191        ints  = a.ints;          else compare_rec r1 r2
192        atoms = a.atoms;      | ([],_) -> -1
193        chars = a.chars;      | _ -> 1
194      }  
195    let rec compare_rec_list l1 l2  =
196    let hash h a =    if l1 == l2 then 0
197      (Hashtbl.hash { map h a with ints = Intervals.empty })    else match (l1,l2) with
198      + (Intervals.hash a.ints)      | (o1,r1)::l1, (o2,r2)::l2 ->
199            if o2 && not o1 then -1
200    let iter f a =          else if o1 && not o2 then 1
201      ignore (map f a)          else let c = compare_rec r1 r2 in if c <> 0 then c
202            else compare_rec_list l1 l2
203    let deep = 4      | ([],_) -> -1
204  end      | _ -> 1
205    
206    let rec compare_rec_bool l1 l2  =
207  module Algebra = Recursive.Make(I)    if l1 == l2 then 0
208  include I    else match (l1,l2) with
209  include Algebra      | (p1,n1)::l1, (p2,n2)::l2 ->
210            let c = compare_rec_list p1 p2 in if c <> 0 then c
211  let check d =          else let c = compare_rec_list n1 n2 in if c <> 0 then c
212    Boolean.check d.times;          else compare_rec_bool l1 l2
213    Boolean.check d.arrow;      | ([],_) -> -1
214    Boolean.check d.record;      | _ -> 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    
302  (*  (*
303  let define n d = check d; define n d  let compare_descr a b =
304      let c = compare_descr a b in
305      assert (c = compare a b);
306      c
307  *)  *)
308    
 let cons d =  
   let n = make () in  
   define n d;  
   internalize n  
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    
347  module Positive =  module DescrHash =
348      Hashtbl.Make(
349  struct  struct
350    type rhs = [ `Type of descr | `Cup of v list | `Times of v * v ]        type t = descr
351    and v = { mutable def : rhs; mutable node : node option }        let hash = hash_descr
352          let equal = equal_descr
353        end
354    let rec make_descr seen v =    )
     if List.memq v seen then empty  
     else  
       let seen = v :: seen in  
       match v.def with  
         | `Type d -> d  
         | `Cup vl ->  
             List.fold_left (fun acc v -> cup acc (make_descr seen v)) empty vl  
         | `Times (v1,v2) -> times (make_node v1) (make_node v2)  
355    
356    and make_node v =  let print_descr = ref (fun _ _  -> assert false)
     match v.node with  
       | Some n -> n  
       | None ->  
           let n = make () in  
           v.node <- Some n;  
           let d = make_descr [] v in  
           define n d;  
           n  
357    
358    let forward () = { def = `Cup []; node = None }  let neg x = diff any x
   let def v d = v.def <- d  
   let cons d = let v = forward () in def v d; v  
   let ty d = cons (`Type d)  
   let cup vl = cons (`Cup vl)  
   let times d1 d2 = cons (`Times (d1,d2))  
   let define v1 v2 = def v1 (`Cup [v2])  
359    
360    let solve v = internalize (make_node v)  let any_node = cons any
 end  
361    
362    module LabelS = Set.Make(LabelPool)
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  let counter_label = ref 0  module DescrMap = Map.Make(struct type t = descr let compare = compare end)
 let label_table = Hashtbl.create 63  
 let label_names = Hashtbl.create 63  
410    
411  let label s =  let check d =
412    try Hashtbl.find label_table s    BoolPair.check d.times;
413    with Not_found ->    BoolPair.check d.xml;
414      incr counter_label;    BoolPair.check d.arrow;
415      Hashtbl.add label_table s !counter_label;    BoolRec.check d.record;
416      Hashtbl.add label_names !counter_label s;    ()
     !counter_label  
   
 let label_name l =  
   Hashtbl.find label_names l  
417    
 let mk_atom = label  
418    
 let atom_name = label_name  
419    
420  (* Subtyping algorithm *)  (* Subtyping algorithm *)
421    
422  let diff_t d t = diff d (descr t)  let diff_t d t = diff d (descr t)
423  let cap_t d t = cap d (descr t)  let cap_t d t = cap d (descr t)
424    let cup_t d t = cup d (descr t)
425  let cap_product l =  let cap_product l =
426    List.fold_left    List.fold_left
427      (fun (d1,d2) (t1,t2) -> (cap_t d1 t1, cap_t d2 t2))      (fun (d1,d2) (t1,t2) -> (cap_t d1 t1, cap_t d2 t2))
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  module Assumptions = Set.Make(struct type t = descr let compare = compare end)  let trivially_empty d = equal_descr d empty
   
 let memo = ref Assumptions.empty  
 let cache_false = ref Assumptions.empty  
435    
436  exception NotEmpty  exception NotEmpty
437    
438    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 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    
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_arrow d.arrow) &&        (empty_rec_times (BoolPair.get d.xml)) &&
586          (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 244  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            if trivially_empty (cap_t accu1 t1) ||
603               trivially_empty (cap_t accu2 t2) then
604              aux accu1 accu2 right
605            else
606          let accu1' = diff_t accu1 t1 in          let accu1' = diff_t accu1 t1 in
607          if not (empty_rec accu1') then aux accu1' accu2 right;          if not (empty_rec accu1') then aux accu1' accu2 right;
608          let accu2' = diff_t accu2 t2 in          let accu2' = diff_t accu2 t2 in
# Line 254  Line 613 
613    (empty_rec accu1) || (empty_rec accu2) ||    (empty_rec accu1) || (empty_rec accu2) ||
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
619    
# Line 262  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 273  Line 633 
633    in    in
634    List.exists single_right right    List.exists single_right right
635    
636  and empty_rec_record c =  and empty_rec_record_aux (labels,(oleft,left),rights) =
637    let aux = List.exists (fun (_,(opt,t)) -> (not opt) && (empty_rec t)) in    let rec aux = function
638    List.for_all aux (get_record c)      | [] -> raise NotEmpty
639        | (oright,right)::rights ->
640            let next =
641              (oleft && (not oright)) ||
642              exists (Array.length left)
643                (fun i ->
644                   trivially_empty (cap left.(i) right.(i)))
645            in
646            if next then aux rights
647            else
648              for i = 0 to Array.length left - 1 do
649                let back = left.(i) in
650                let di = diff back right.(i) in
651                if not (empty_rec di) then (
652                  left.(i) <- diff back right.(i);
653                  aux rights;
654                  left.(i) <- back;
655                )
656              done
657      in
658      exists (Array.length left)
659        (fun i -> empty_rec left.(i))
660      ||
661      (try aux rights; true with NotEmpty -> false)
662    
663    
664    and empty_rec_record c =
665      List.for_all empty_rec_record_aux (get_record c)
666    
667    (*
668    let is_empty d =
669      empty_rec d
670      *)
671    
672    let non_empty d =
673      not (is_empty d)
674    
675    let subtype d1 d2 =
676      is_empty (diff d1 d2)
677    
678    module Product =
679    struct
680      type t = (descr * descr) list
681    
682      let other ?(kind=`Normal) d =
683        match kind with
684          | `Normal -> { d with times = empty.times }
685          | `XML -> { d with xml = empty.xml }
686    
687      let is_product ?kind d = is_empty (other ?kind d)
688    
689      let need_second = function _::_::_ -> true | _ -> false
690    
691      let normal_aux d =
692        let res = ref [] in
693    
694        let add (t1,t2) =
695          let rec loop t1 t2 = function
696            | [] -> res := (ref (t1,t2)) :: !res
697            | ({contents = (d1,d2)} as r)::l ->
698                (*OPT*)
699    (*          if equal_descr d1 t1 then r := (d1,cup d2 t2) else*)
700    
701                  let i = cap t1 d1 in
702                  if is_empty i then loop t1 t2 l
703                  else (
704                    r := (i, cup t2 d2);
705                    let k = diff d1 t1 in
706                    if non_empty k then res := (ref (k,d2)) :: !res;
707    
708                    let j = diff t1 d1 in
709                    if non_empty j then loop j t2 l
710                  )
711          in
712          loop t1 t2 !res
713        in
714        List.iter add d;
715        List.map (!) !res
716    
717    (*
718    This version explodes when dealing with
719       Any - [ t1? t2? t3? ... tn? ]
720    ==> need partitioning
721    *)
722      let get_aux d =
723        let line accu (left,right) =
724          let rec aux accu d1 d2 = function
725            | (t1,t2)::right ->
726                let accu =
727                  let d1 = diff_t d1 t1 in
728                  if is_empty d1 then accu else aux accu d1 d2 right in
729                let accu =
730                  let d2 = diff_t d2 t2 in
731                  if is_empty d2 then accu else aux accu d1 d2 right in
732                accu
733            | [] -> (d1,d2) :: accu
734          in
735          let (d1,d2) = cap_product left in
736          if (is_empty d1) || (is_empty d2) then accu else aux accu d1 d2 right
737        in
738        List.fold_left line [] d
739    
740    (* Partitioning:
741    
742    (t,s) - ((t1,s1) | (t2,s2) | ... | (tn,sn))
743    =
744    (t & t1, s - s1) | ... | (t & tn, s - sn) | (t - (t1|...|tn), s)
745    
746    *)
747      let get_aux d =
748        let accu = ref [] in
749        let line (left,right) =
750          let (d1,d2) = cap_product left in
751          if (non_empty d1) && (non_empty d2) then
752            let right = List.map (fun (t1,t2) -> descr t1, descr t2) right in
753            let right = normal_aux right in
754            let resid1 = ref d1 in
755            let () =
756              List.iter
757                (fun (t1,t2) ->
758                   let t1 = cap d1 t1 in
759                   if (non_empty t1) then
760                     let () = resid1 := diff !resid1 t1 in
761                     let t2 = diff d2 t2 in
762                     if (non_empty t2) then accu := (t1,t2) :: !accu
763                ) right in
764            if non_empty !resid1 then accu := (!resid1, d2) :: !accu
765        in
766        List.iter line (BoolPair.get d);
767        !accu
768    (* Maybe, can improve this function with:
769         (t,s) \ (t1,s1) = (t&t',s\s') | (t\t',s),
770       don't call normal_aux *)
771    
772    
773      let get ?(kind=`Normal) d =
774        match kind with
775          | `Normal -> get_aux d.times
776          | `XML -> get_aux d.xml
777    
778      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
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 =
786        let aux acc (t1,t2) =
787          let t1 = cap t1 pi1 in if is_empty t1 then acc else (t1,t2)::acc in
788        List.fold_left aux [] rects
789    
790      type normal = t
791    
792      module Memo = Map.Make(struct type t = descr BoolPair.t let compare = BoolPair.compare end)
793    
794    
795      let memo = ref Memo.empty
796      let normal ?(kind=`Normal) d =
797        let d = match kind with `Normal -> d.times | `XML -> d.xml in
798        try Memo.find d !memo
799        with
800            Not_found ->
801              let gd = get_aux d in
802              let n = normal_aux gd in
803    (* Could optimize this call to normal_aux because one already
804       know that each line is normalized ... *)
805              memo := Memo.add d n !memo;
806              n
807    
808      let any = { empty with times = any.times }
809      and any_xml = { empty with xml = any.xml }
810      let is_empty d = d = []
811    end
812    
813    module Print =
814    struct
815      let rec print_union ppf = function
816        | [] -> Format.fprintf ppf "Empty"
817        | [h] -> h ppf
818        | h::t -> Format.fprintf ppf "@[%t |@ %a@]" h print_union t
819    
820      let print_tag ppf a =
821        match Atoms.is_atom a with
822          | Some a -> Format.fprintf ppf "%s" (Atoms.value a)
823          | None -> Format.fprintf ppf "(%a)" print_union (Atoms.print a)
824    
825      let print_const ppf = function
826        | Integer i -> Intervals.print_v ppf i
827        | Atom a -> Atoms.print_v ppf a
828        | Char c -> Chars.print_v ppf c
829    
830      let named = State.ref "Types.Printf.named" DescrMap.empty
831      let register_global name d =
832        named := DescrMap.add d name !named
833    
834      let marks = DescrHash.create 63
835      let wh = ref []
836      let count_name = ref 0
837      let name () =
838        incr count_name;
839        "X" ^ (string_of_int !count_name)
840    (* TODO:
841       check that these generated names does not conflict with declared types *)
842    
843      let trivial_rec b = b = BoolRec.empty || b = BoolRec.full
844      let trivial_pair b = b = BoolPair.empty || b = BoolPair.full
845    
846      let worth_abbrev d =
847        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)
851      and mark_descr d =
852        if not (DescrMap.mem d !named) then
853          try
854            let r = DescrHash.find marks d in
855            if (!r = None) && (worth_abbrev d) then
856              let na = name () in
857              r := Some na;
858              wh := (na,d) :: !wh
859          with Not_found ->
860            DescrHash.add marks d (ref None);
861            BoolPair.iter (fun (n1,n2) -> mark n1; mark n2) d.times;
862            BoolPair.iter
863              (fun (n1,n2) -> mark n1; mark n2
864    (*
865                 List.iter
866                   (fun (d1,d2) ->
867                      mark_descr d2;
868                      bool_iter
869                        (fun (o,l) -> List.iter (fun (l,(o,n)) -> mark n) l)
870                        d1.record
871                      let l = get_record d1.record in
872                      List.iter (fun labs,(_,(_,p)),ns ->
873                                   Array.iter mark_descr p;
874                                   List.iter (fun (_,(_,n)) ->
875                                                Array.iter mark_descr n) ns
876                                ) l
877                   )
878                   (Product.normal (descr n2))
879    *)
880              ) d.xml;
881            BoolPair.iter (fun (n1,n2) -> mark n1; mark n2) d.arrow;
882            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)
888      and print_descr ppf d =
889        try
890          let name = DescrMap.find d !named in
891          Format.fprintf ppf "%s" name
892        with Not_found ->
893          try
894            match !(DescrHash.find marks d) with
895              | Some n -> Format.fprintf ppf "%s" n
896              | None -> real_print_descr ppf d
897          with
898              Not_found -> assert false
899      and real_print_descr ppf d =
900        if d = any then Format.fprintf ppf "Any" else
901          (
902            if d.absent then Format.fprintf ppf "?";
903            print_union ppf
904              (Intervals.print d.ints @
905               Chars.print d.chars @
906               Atoms.print d.atoms @
907               BoolPair.print "Pair" print_times d.times @
908               BoolPair.print "XML" print_xml d.xml @
909               BoolPair.print "Arrow" print_arrow d.arrow @
910               BoolRec.print "Record" print_record d.record
911              )
912          )
913      and print_times ppf (t1,t2) =
914        Format.fprintf ppf "@[(%a,%a)@]" print t1 print t2
915      and print_xml ppf (t1,t2) =
916        Format.fprintf ppf "@[XML(%a,%a)@]" print t1 print t2
917    (*
918        let l = Product.normal (descr t2) in
919        let l = List.map
920                  (fun (d1,d2) ppf ->
921                     Format.fprintf ppf "@[<><%a%a>%a@]"
922                       print_tag (descr t1).atoms
923                       print_attribs d1.record
924                       print_descr d2) l
925        in
926        print_union ppf l
927    *)
928      and print_arrow ppf (t1,t2) =
929        Format.fprintf ppf "@[(%a -> %a)@]" print t1 print t2
930      and print_record ppf (o,r) =
931        let o = if o then "" else "|" in
932        Format.fprintf ppf "@[{%s" o;
933        let first = ref true in
934        List.iter (fun (l,t) ->
935                     let sep = if !first then (first := false; "") else ";" in
936                     Format.fprintf ppf "%s@ @[%s =@] %a" sep
937                       (LabelPool.value l) print t
938                  ) (LabelMap.get r);
939        Format.fprintf ppf " %s}@]" o
940    (*
941      and print_attribs ppf r =
942        let l = get_record r in
943        if l <> [ [] ] then
944        let l = List.map
945          (fun att ppf ->
946             let first = ref true in
947             Format.fprintf ppf "{" ;
948             List.iter (fun (l,(o,d)) ->
949                          Format.fprintf ppf "%s%s=%s%a"
950                            (if !first then "" else " ")
951                            (LabelPool.value l) (if o then "?" else "")
952                            print_descr d;
953                          first := false
954                       ) att;
955               Format.fprintf ppf "}"
956          ) l in
957        print_union ppf l
958    *)
959    
960    
961      let end_print ppf =
962        (match List.rev !wh with
963           | [] -> ()
964           | (na,d)::t ->
965               Format.fprintf ppf " where@ @[%s = %a" na real_print_descr d;
966               List.iter
967                 (fun (na,d) ->
968                    Format.fprintf ppf " and@ %s = %a" na real_print_descr d)
969                 t;
970               Format.fprintf ppf "@]"
971        );
972        Format.fprintf ppf "@]";
973        count_name := 0;
974        wh := [];
975        DescrHash.clear marks
976    
977      let print_descr ppf d =
978        mark_descr d;
979        Format.fprintf ppf "@[%a" print_descr d;
980        end_print ppf
981    
982       let print ppf n = print_descr ppf (descr n)
983    
984    end
985    
986    let () = print_descr := Print.print_descr
987    
988    module Positive =
989    struct
990      type rhs = [ `Type of descr | `Cup of v list | `Times of v * v ]
991      and v = { mutable def : rhs; mutable node : node option }
992    
993    
994      let rec make_descr seen v =
995        if List.memq v seen then empty
996        else
997          let seen = v :: seen in
998          match v.def with
999            | `Type d -> d
1000            | `Cup vl ->
1001                List.fold_left (fun acc v -> cup acc (make_descr seen v)) empty vl
1002            | `Times (v1,v2) -> times (make_node v1) (make_node v2)
1003    
1004      and make_node v =
1005        match v.node with
1006          | Some n -> n
1007          | None ->
1008              let n = make () in
1009              v.node <- Some n;
1010              let d = make_descr [] v in
1011              define n d;
1012              n
1013    
1014      let forward () = { def = `Cup []; node = None }
1015      let def v d = v.def <- d
1016      let cons d = let v = forward () in def v d; v
1017      let ty d = cons (`Type d)
1018      let cup vl = cons (`Cup vl)
1019      let times d1 d2 = cons (`Times (d1,d2))
1020      let define v1 v2 = def v1 (`Cup [v2])
1021    
1022      let solve v = internalize (make_node v)
1023    end
1024    
 let is_empty d =  
   let r = empty_rec d in  
   memo := Assumptions.empty;  
   cache_false := Assumptions.empty;  
   r  
1025    
 let non_empty d =  
   not (is_empty d)  
1026    
 let subtype d1 d2 =  
   is_empty (diff d1 d2)  
1027    
1028  (* Sample value *)  (* Sample value *)
1029  module Sample =  module Sample =
1030  struct  struct
1031    
1032    
1033  let rec find f = function  let rec find f = function
1034    | [] -> raise Not_found    | [] -> raise Not_found
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)
1043    | Record of (label * t) list    | Record of (label * t) list
1044    | Fun of (node * node) list    | Fun of (node * node) list
1045      | Other
1046  let rec gen_atom i l =    exception FoundSampleRecord of (label * t) list
   if SortedList.mem l i then gen_atom (succ i) l  else i  
1047    
1048  let rec sample_rec memo d =  let rec sample_rec memo d =
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 (gen_atom 0) d.atoms) with Not_found ->      try Atom (Atoms.sample d.atoms) with
1053            Not_found ->
1054    (* 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 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 (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 328  Line 1068 
1068  and sample_rec_times_aux memo (left,right) =  and sample_rec_times_aux memo (left,right) =
1069    let rec aux accu1 accu2 = function    let rec aux accu1 accu2 = function
1070      | (t1,t2)::right ->      | (t1,t2)::right ->
1071    (*TODO: check: is this correct ?  non_empty could return true
1072      but because of coinduction, the call to aux may raise Not_found, no ? *)
1073          let accu1' = diff_t accu1 t1 in          let accu1' = diff_t accu1 t1 in
1074          if non_empty accu1' then aux accu1' accu2 right else          if non_empty accu1' then aux accu1' accu2 right else
1075            let accu2' = diff_t accu2 t2 in            let accu2' = diff_t accu2 t2 in
1076            if non_empty accu2' then aux accu1 accu2' right else            if non_empty accu2' then aux accu1 accu2' right else
1077              raise Not_found              raise Not_found
1078      | [] -> Pair (sample_rec memo accu1, sample_rec memo accu2)      | [] -> (sample_rec memo accu1, sample_rec memo accu2)
1079    in    in
1080    let (accu1,accu2) = cap_product left in    let (accu1,accu2) = cap_product left in
1081    if (is_empty accu1) || (is_empty accu2) then raise Not_found;    if (is_empty accu1) || (is_empty accu2) then raise Not_found;
# Line 366  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 fields =  and sample_rec_record_aux memo (labels,(oleft,left),rights) =
1112    let aux acc (l,(o,t)) = if o then acc else (l, sample_rec memo t) :: acc in    let rec aux = function
1113    List.fold_left aux [] fields      | [] ->
1114            let l = ref labels and fields = ref [] in
1115  let get x = sample_rec Assumptions.empty x          for i = 0 to Array.length left - 1 do
1116              fields := (List.hd !l, sample_rec memo left.(i))::!fields;
1117  end            l := List.tl !l
1118            done;
1119            raise (FoundSampleRecord (List.rev !fields))
1120        | (oright,right)::rights ->
1121            let next = (oleft && (not oright)) in
1122            if next then aux rights
1123            else
1124              for i = 0 to Array.length left - 1 do
1125                let back = left.(i) in
1126                let di = diff back right.(i) in
1127                if not (is_empty di) then (
1128                  left.(i) <- diff back right.(i);
1129                  aux rights;
1130                  left.(i) <- back;
1131                )
1132              done
1133      in
1134      if exists (Array.length left)
1135        (fun i -> is_empty left.(i)) then raise Not_found;
1136      try aux rights; raise Not_found
1137      with FoundSampleRecord r -> r
1138    
 module Product =  
 struct  
   type t = (descr * descr) list  
1139    
   let other d = { d with times = empty.times }  
   let is_product d = is_empty (other d)  
1140    
   let need_second = function _::_::_ -> true | _ -> false  
1141    
   let get d =  
     let line accu (left,right) =  
       let rec aux accu d1 d2 = function  
         | (t1,t2)::right ->  
             let accu =  
               let d1 = diff_t d1 t1 in  
               if is_empty d1 then accu else aux accu d1 d2 right in  
             let accu =  
               let d2 = diff_t d2 t2 in  
               if is_empty d2 then accu else aux accu d1 d2 right in  
             accu  
         | [] ->  (d1,d2) :: accu  
       in  
       let (d1,d2) = cap_product left in  
       if (is_empty d1) || (is_empty d2) then accu else aux accu d1 d2 right  
     in  
     List.fold_left line [] d.times  
1142    
1143    let pi1 = List.fold_left (fun acc (t1,_) -> cup acc t1) empty  let get x = try sample_rec Assumptions.empty x with Not_found -> Other
   let pi2 = List.fold_left (fun acc (_,t2) -> cup acc t2) empty  
1144    
1145    let restrict_1 rects pi1 =    let rec print_sep f sep ppf = function
1146      let aux accu (t1,t2) =      | [] -> ()
1147        let t1 = cap t1 pi1 in if is_empty t1 then accu else (t1,t2)::accu in      | [x] -> f ppf x
1148      List.fold_left aux [] rects      | x::rem -> f ppf x; Format.fprintf ppf "%s" sep; print_sep f sep ppf rem
1149    
   type normal = t  
1150    
1151    let normal d =    let rec print ppf = function
1152      let res = ref [] in      | Int i -> Intervals.print_v ppf i
1153        | Atom a -> Atoms.print_v ppf a
1154        | Char c -> Chars.print_v ppf c
1155        | 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
1157        | Record r ->
1158            Format.fprintf ppf "{ %a }"
1159              (print_sep
1160                 (fun ppf (l,x) ->
1161                    Format.fprintf ppf "%s = %a"
1162                    (LabelPool.value l)
1163                    print x
1164                 )
1165                 " ; "
1166              ) r
1167        | Fun iface ->
1168            Format.fprintf ppf "(fun ( %a ) x -> ...)"
1169              (print_sep
1170                 (fun ppf (t1,t2) ->
1171                    Format.fprintf ppf "%a -> %a; "
1172                    Print.print t1 Print.print t2
1173                 )
1174                 " ; "
1175              ) iface
1176        | Other ->
1177            Format.fprintf ppf "[cannot determine value]"
1178    end
1179    
     let add (t1,t2) =  
       let rec loop t1 t2 = function  
         | [] -> res := (ref (t1,t2)) :: !res  
         | ({contents = (d1,d2)} as r)::l ->  
             (*OPT*)  
             if d1 = t1 then r := (d1,cup d2 t2) else  
1180    
               let i = cap t1 d1 in  
               if is_empty i then loop t1 t2 l  
               else (  
                 r := (i, cup t2 d2);  
                 let k = diff d1 t1 in  
                 if non_empty k then res := (ref (k,d2)) :: !res;  
1181    
1182                  let j = diff t1 d1 in  module Record =
1183                  if non_empty j then loop j t2 l  struct
1184                )    let has_record d = not (is_empty { empty with record = d.record })
1185        in    let or_absent d = { d with absent = true }
1186        loop t1 t2 !res    let any_or_absent = or_absent any
1187      in    let has_absent d = d.absent
     List.iter add (get d);  
     List.map (!) !res  
1188    
1189    let any = { empty with times = any.times }    module T = struct
1190    let is_empty d = d = []      type t = descr
1191        let any = any_or_absent
1192        let cap = cap
1193        let cup = cup
1194        let diff = diff
1195        let is_empty = is_empty
1196        let empty = empty
1197      end
1198      module R = struct
1199        type t = descr
1200        let any = { empty with record = any.record }
1201        let cap = cap
1202        let cup = cup
1203        let diff = diff
1204        let is_empty = is_empty
1205        let empty = empty
1206  end  end
1207      module TR = Normal.Make(T)(R)
1208    
1209      let any_record = { empty with record = BoolRec.full }
1210    
1211  module Record =    let atom o l =
1212  struct      if o && LabelMap.is_empty l then any_record else
1213    type t = (label, (bool * descr)) SortedMap.t list      { empty with record = BoolRec.atom (o,l) }
1214    
1215      type zor = Pair of descr * descr | Any
1216    
1217    let get d =    let aux_split d l=
1218      let line r = List.for_all (fun (l,(o,d)) -> o || non_empty d) r in      let f (o,r) =
1219      List.filter line (get_record d.record)        try
1220            let (lt,rem) = LabelMap.assoc_remove l r in
1221            Pair (descr lt, atom o rem)
1222    let restrict_label_present t l =        with Not_found ->
1223      let aux = SortedMap.change l (fun (_,d) -> (false,d)) (false,any) in          if o then
1224      List.map aux t            if LabelMap.is_empty r then Any else
1225                Pair (any_or_absent, { empty with record = BoolRec.atom (o,r) })
   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  
   
   type normal =  
       [ `Success  
       | `Fail  
       | `Label of label * (descr * normal) list * normal ]  
   
   let rec merge_record n r =  
     match (n, r) with  
       | (`Success, _) | (_, []) -> `Success  
       | (`Fail, 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  
             `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)  
1226            else            else
1227              let res = ref [] in            Pair ({empty with absent = true},
1228              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  
1229              in              in
1230              let t2 = List.fold_left aux t2 present in      List.fold_left
1231              let () =        (fun b (p,n) ->
1232                if non_empty t2 then           let rec aux_p accu = function
1233                res := (t2, merge_record `Fail r') :: !res in             | x::p ->
1234              let abs = if o then merge_record absent r' else absent in                 (match f x with
1235              `Label (l1, !res, abs)                    | Pair (t1,t2) -> aux_p ((t1,t2)::accu) p
1236                      | Any -> aux_p accu p)
1237               | [] -> aux_n accu [] n
1238             and aux_n p accu = function
1239               | x::n ->
1240                   (match f x with
1241                      | Pair (t1,t2) -> aux_n p ((t1,t2)::accu) n
1242                      | Any -> b)
1243               | [] -> (p,accu) :: b in
1244             aux_p [] p)
1245          []
1246          (BoolRec.get d.record)
1247    
1248      let split (d : descr) l =
1249        TR.boolean (aux_split d l)
1250    
1251      let split_normal d l =
1252        TR.boolean_normal (aux_split d l)
1253    
   let normal d =  
     List.fold_left merge_record `Fail (get d)  
1254    
1255    let project d l =    let project d l =
1256      let aux accu x =      let t = TR.pi1 (split d l) in
1257        match List.assoc l x with      if t.absent then raise Not_found;
1258          | (false,t) -> cup accu t      t
1259          | _ -> raise Not_found  
1260      let remove_field d l =
1261        TR.pi2 (split d l)
1262    
1263      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    
1282    
1283    (*TODO: optimize merge
1284       - pre-compute the sequence of labels
1285       - remove empty or full { l = t }
1286    *)
1287    
1288      let merge d1 d2 =
1289        let res = ref empty in
1290        let rec aux accu d1 d2 =
1291          let l = min (first_label d1) (first_label d2) in
1292          if l = LabelPool.dummy_max then
1293            let (some1,none1) = empty_cases d1
1294            and (some2,none2) = empty_cases d2 in
1295            let none = none1 && none2 and some = some1 || some2 in
1296            let accu = LabelMap.from_list (fun _ _ -> assert false) accu in
1297            (* approx for the case (some && not none) ... *)
1298            res := cup !res (record' (some, accu))
1299          else
1300            let l1 = split d1 l and l2 = split d2 l in
1301            let loop (t1,d1) (t2,d2) =
1302              let t =
1303                if t2.absent
1304                then cup t1 { t2 with absent = false }
1305                else t2
1306      in      in
1307      List.fold_left aux empty (get_record d.record)            aux ((l,cons t)::accu) d1 d2
1308            in
1309            List.iter (fun x -> List.iter (loop x) l2) l1
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 = []  
1316  end  end
1317    
1318    
 module MapDescr = Map.Make(struct type t = descr let compare = compare end)  
1319    
1320  let memo_normalize = ref MapDescr.empty  let memo_normalize = ref DescrMap.empty
1321    
 let map_sort f l =  
   SortedList.from_list (List.map f l)  
1322    
1323  let rec rec_normalize d =  let rec rec_normalize d =
1324    try MapDescr.find d !memo_normalize    try DescrMap.find d !memo_normalize
1325    with Not_found ->    with Not_found ->
1326      let n = make () in      let n = make () in
1327      memo_normalize := MapDescr.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 record =      let xml =
1334          List.fold_left
1335            (fun accu (d1,d2) -> BoolPair.cup accu (BoolPair.atom (rec_normalize d1, rec_normalize d2)))
1336            BoolPair.empty (Product.normal ~kind:`XML d)
1337        in
1338        let record = d.record
1339    (*
1340        map_sort        map_sort
1341          (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, [])
1342          (Record.get d)          (Record.get d)
1343    *)
1344      in      in
1345      define n { d with times = times; record = record };      define n { d with times = times; xml = xml; record = record };
1346      n      n
1347    
1348  let normalize n =  let normalize n =
1349    internalize (rec_normalize (descr n))    descr (internalize (rec_normalize n))
   
 module DescrHash =  
   Hashtbl.Make(  
     struct  
       type t = descr  
       let hash = hash_descr  
       let equal = equal_descr  
     end  
   )  
   
 module Print =  
 struct  
   let named = DescrHash.create 10  
   let register_global name d = DescrHash.add named d name  
   
   let marks = DescrHash.create 63  
   let wh = ref []  
   let count_name = ref 0  
   let name () =  
     incr count_name;  
     "X" ^ (string_of_int !count_name)  
 (* TODO:  
    check that these generated names does not conflict with declared types *)  
   
   let bool_iter f b =  
     List.iter (fun (p,n) -> List.iter f p; List.iter f n) b  
   
   let trivial b = b = Boolean.empty || b = Boolean.full  
   
   let worth_abbrev d =  
     not (trivial d.times && trivial d.arrow && trivial d.record)  
   
   let rec mark n = mark_descr (descr n)  
   and mark_descr d =  
     if not (DescrHash.mem named d) then  
       try  
         let r = DescrHash.find marks d in  
         if (!r = None) && (worth_abbrev d) then  
           let na = name () in  
           r := Some na;  
           wh := (na,d) :: !wh  
       with Not_found ->  
         DescrHash.add marks d (ref None);  
         bool_iter (fun (n1,n2) -> mark n1; mark n2) d.times;  
         bool_iter (fun (n1,n2) -> mark n1; mark n2) d.arrow;  
         bool_iter (fun (l,o,n) -> mark n) d.record  
   
   
   let rec print_union ppf = function  
     | [] -> Format.fprintf ppf "Empty"  
     | [h] -> h ppf  
     | h::t -> Format.fprintf ppf "@[%t |@ %a@]" h print_union t  
   
   let print_atom ppf a = Format.fprintf ppf "`%s" (atom_name a)  
   
   let rec print ppf n = print_descr ppf (descr n)  
   and print_descr ppf d =  
     try  
       let name = DescrHash.find named d in  
       Format.fprintf ppf "%s" name  
     with Not_found ->  
       try  
         match !(DescrHash.find marks d) with  
           | Some n -> Format.fprintf ppf "%s" n  
           | None -> real_print_descr ppf d  
       with  
           Not_found -> Format.fprintf ppf "XXX"  
   and real_print_descr ppf d =  
     if d = any then Format.fprintf ppf "Any" else  
       print_union ppf  
         (Intervals.print d.ints @  
          Chars.print d.chars @  
          Atoms.print "AnyAtom" print_atom d.atoms @  
          Boolean.print "(Any,Any)" print_times d.times @  
          Boolean.print "(Empty -> Any)" print_arrow d.arrow @  
          Boolean.print "{ }" print_record d.record  
         )  
   and print_times ppf (t1,t2) =  
     Format.fprintf ppf "@[(%a,%a)@]" print t1 print t2  
   and print_arrow ppf (t1,t2) =  
     Format.fprintf ppf "@[(%a -> %a)@]" print t1 print t2  
   and print_record ppf (l,o,t) =  
     Format.fprintf ppf "@[{ %s =%s %a }@]"  
       (label_name l) (if o then "?" else "") print t  
   
   
   let end_print ppf =  
     (match List.rev !wh with  
        | [] -> ()  
        | (na,d)::t ->  
            Format.fprintf ppf " where@ @[%s = %a" na real_print_descr d;  
            List.iter  
              (fun (na,d) ->  
                 Format.fprintf ppf " and@ %s = %a" na real_print_descr d)  
              t;  
            Format.fprintf ppf "@]"  
     );  
     Format.fprintf ppf "@]";  
     count_name := 0;  
     wh := [];  
     DescrHash.clear marks  
   
   let print_descr ppf d =  
     mark_descr d;  
     Format.fprintf ppf "@[%a" print_descr d;  
     end_print ppf  
   
    let print ppf n = print_descr ppf (descr n)  
   
   let rec print_sep f sep ppf = function  
     | [] -> ()  
     | [x] -> f ppf x  
     | x::rem -> f ppf x; Format.fprintf ppf "%s" sep; print_sep f sep ppf rem  
   
   
   let rec print_sample ppf = function  
     | Sample.Int i -> Format.fprintf ppf "%s" (Big_int.string_of_big_int i)  
     | Sample.Atom a -> Format.fprintf ppf "`%s" (atom_name a)  
     | Sample.Char c -> Chars.Unichar.print ppf c  
     | Sample.Pair (x1,x2) ->  
         Format.fprintf ppf "(%a,%a)"  
         print_sample x1  
         print_sample x2  
     | Sample.Record r ->  
         Format.fprintf ppf "{ %a }"  
           (print_sep  
              (fun ppf (l,x) ->  
                 Format.fprintf ppf "%s = %a"  
                 (label_name l)  
                 print_sample x  
              )  
              " ; "  
           ) r  
     | Sample.Fun iface ->  
         Format.fprintf ppf "(fun ( %a ) x -> ...)"  
           (print_sep  
              (fun ppf (t1,t2) ->  
                 Format.fprintf ppf "%a -> %a; "  
                 print t1 print t2  
              )  
              " ; "  
           ) iface  
 end  
1350    
1351  module Arrow =  module Arrow =
1352  struct  struct
# Line 708  Line 1354 
1354      let rec aux accu1 accu2 = function      let rec aux accu1 accu2 = function
1355        | (t1,t2)::left ->        | (t1,t2)::left ->
1356            let accu1' = diff_t accu1 t1 in            let accu1' = diff_t accu1 t1 in
1357            if not (empty_rec accu1') then aux accu1 accu2 left;            if non_empty accu1' then aux accu1 accu2 left;
1358            let accu2' = cap_t accu2 t2 in            let accu2' = cap_t accu2 t2 in
1359            if not (empty_rec accu2') then aux accu1 accu2 left            if non_empty accu2' then aux accu1 accu2 left
1360        | [] -> raise NotEmpty        | [] -> raise NotEmpty
1361      in      in
1362      let accu1 = descr s1 in      let accu1 = descr s1 in
# Line 718  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 =
1379        let rec aux accu1 accu2 = function
1380          | (t1,t2)::left ->
1381              let accu1' = diff accu1 t1 in
1382              if non_empty accu1' then aux accu1 accu2 left;
1383              let accu2' = cap accu2 t2 in
1384              if non_empty accu2' then aux accu1 accu2 left
1385          | [] -> raise NotEmpty
1386        in
1387        let accu1 = descr s1 in
1388        (is_empty accu1) ||
1389        (try aux accu1 (diff any (descr s2)) left; true with NotEmpty -> false)
1390    
1391      let check_iface iface s =
1392        let rec aux = function
1393          | [] -> false
1394          | (p,n) :: rem ->
1395              ((List.for_all (fun (a,b) -> check_simple_iface iface a b) p) &&
1396               (List.for_all (fun (a,b) -> not (check_simple_iface iface a b)) n))
1397              || (aux rem)
1398        in
1399        aux (BoolPair.get s.arrow)
1400    
1401    type t = descr * (descr * descr) list list    type t = descr * (descr * descr) list list
1402    
# Line 745  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 788  Line 1457 
1457    
1458    
1459  module Int = struct  module Int = struct
1460      let has_int d i = Intervals.contains i d.ints
1461    
1462    let get d = d.ints    let get d = d.ints
1463    let put i = { empty with ints = i }    let put i = { empty with ints = i }
1464    let is_int d = is_empty { d with ints = Intervals.empty }    let is_int d = is_empty { d with ints = Intervals.empty }
# Line 798  Line 1469 
1469    let has_atom d a = Atoms.contains a d.atoms    let has_atom d a = Atoms.contains a d.atoms
1470  end  end
1471    
1472    module Char = struct
1473      let has_char d c = Chars.contains c d.chars
1474      let any = { empty with chars = Chars.any }
1475    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.19  
changed lines
  Added in v.240
CVS Admin">CVS Admin
 ViewVC Help
Powered by ViewVC 1.1.5