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

Diff of /types/types.ml

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

revision 45 by abate, Tue Jul 10 17:00:40 2007 UTC revision 111 by abate, Tue Jul 10 17:07:18 2007 UTC
# Line 2  Line 2 
2  open Printf  open Printf
3    
4    
5    let map_sort f l =
6      SortedList.from_list (List.map f l)
7    
8    module HashedString =
9    struct
10      type t = string
11      let hash = Hashtbl.hash
12      let equal = (=)
13    end
14    
15    module LabelPool = Pool.Make(HashedString)
16    module AtomPool  = Pool.Make(HashedString)
17    
18  type label = int  type label = LabelPool.t
19  type atom  = int  type atom  = AtomPool.t
20    
21  type const = Integer of Big_int.big_int | Atom of atom | Char of Chars.Unichar.t  type const = Integer of Big_int.big_int | Atom of atom | Char of Chars.Unichar.t
22    
23    type pair_kind = [ `Normal | `XML ]
24    
25  module I = struct  module I = struct
26    type 'a t = {    type 'a t = {
27      ints  : Intervals.t;      ints  : Intervals.t;
28      atoms : atom Atoms.t;      atoms : atom Atoms.t;
29      times : ('a * 'a) Boolean.t;      times : ('a * 'a) Boolean.t;
30        xml   : ('a * 'a) Boolean.t;
31      arrow : ('a * 'a) Boolean.t;      arrow : ('a * 'a) Boolean.t;
32      record: (label * bool * 'a) Boolean.t;      record: (label * bool * 'a) Boolean.t;
33      chars : Chars.t;      chars : Chars.t;
# Line 20  Line 35 
35    
36    let empty = {    let empty = {
37      times = Boolean.empty;      times = Boolean.empty;
38        xml   = Boolean.empty;
39      arrow = Boolean.empty;      arrow = Boolean.empty;
40      record= Boolean.empty;      record= Boolean.empty;
41      ints  = Intervals.empty;      ints  = Intervals.empty;
42      atoms = Atoms.empty;      atoms = Atoms.empty;
43      chars = Chars.empty;      chars = Chars.empty;
44    }    }
45    (*
46    let any =  {    let any =  {
47      times = Boolean.full;      times = Boolean.full;
48        xml   = Boolean.full;
49      arrow = Boolean.full;      arrow = Boolean.full;
50      record= Boolean.full;      record= Boolean.full;
51      ints  = Intervals.any;      ints  = Intervals.any;
52      atoms = Atoms.any;      atoms = Atoms.any;
53      chars = Chars.any;      chars = Chars.any;
54    }    }
55    *)
56    
57    let interval i j = { empty with ints = Intervals.atom i j }    let interval i = { empty with ints = i }
58    let times x y = { empty with times = Boolean.atom (x,y) }    let times x y = { empty with times = Boolean.atom (x,y) }
59      let xml x y = { empty with xml = Boolean.atom (x,y) }
60    let arrow x y = { empty with arrow = Boolean.atom (x,y) }    let arrow x y = { empty with arrow = Boolean.atom (x,y) }
61    let record label opt t = { empty with record = Boolean.atom (label,opt,t) }    let record label opt t = { empty with record = Boolean.atom (label,opt,t) }
62    let atom a = { empty with atoms = a }    let atom a = { empty with atoms = a }
63    let char c = { empty with chars = c }    let char c = { empty with chars = c }
64    let constant = function    let constant = function
65      | Integer i -> interval i i      | Integer i -> interval (Intervals.atom i)
66      | Atom a -> atom (Atoms.atom a)      | Atom a -> atom (Atoms.atom a)
67      | Char c -> char (Chars.atom c)      | Char c -> char (Chars.atom c)
68    
69    
   let any_record = { empty with record = any.record }  
   
70    let cup x y =    let cup x y =
71      if x == y then x else {      if x = y then x else {
72        times = Boolean.cup x.times y.times;        times = Boolean.cup x.times y.times;
73          xml   = Boolean.cup x.xml y.xml;
74        arrow = Boolean.cup x.arrow y.arrow;        arrow = Boolean.cup x.arrow y.arrow;
75        record= Boolean.cup x.record y.record;        record= Boolean.cup x.record y.record;
76        ints  = Intervals.cup x.ints  y.ints;        ints  = Intervals.cup x.ints  y.ints;
# Line 61  Line 79 
79      }      }
80    
81    let cap x y =    let cap x y =
82      if x == y then x else {      if x = y then x else {
83        times = Boolean.cap x.times y.times;        times = Boolean.cap x.times y.times;
84          xml   = Boolean.cap x.xml y.xml;
85        record= Boolean.cap x.record y.record;        record= Boolean.cap x.record y.record;
86        arrow = Boolean.cap x.arrow y.arrow;        arrow = Boolean.cap x.arrow y.arrow;
87        ints  = Intervals.cap x.ints  y.ints;        ints  = Intervals.cap x.ints  y.ints;
# Line 71  Line 90 
90      }      }
91    
92    let diff x y =    let diff x y =
93      if x == y then empty else {      if x = y then empty else {
94        times = Boolean.diff x.times y.times;        times = Boolean.diff x.times y.times;
95          xml   = Boolean.diff x.xml y.xml;
96        arrow = Boolean.diff x.arrow y.arrow;        arrow = Boolean.diff x.arrow y.arrow;
97        record= Boolean.diff x.record y.record;        record= Boolean.diff x.record y.record;
98        ints  = Intervals.diff x.ints  y.ints;        ints  = Intervals.diff x.ints  y.ints;
# Line 80  Line 100 
100        chars = Chars.diff x.chars y.chars;        chars = Chars.diff x.chars y.chars;
101      }      }
102    
   let neg x = diff any x  
103    
104    let equal e a b =    let equal e a b =
     if not (Intervals.equal a.ints b.ints) then raise NotEqual;  
105      if a.atoms <> b.atoms then raise NotEqual;      if a.atoms <> b.atoms then raise NotEqual;
106      if a.chars <> b.chars then raise NotEqual;      if a.chars <> b.chars then raise NotEqual;
107        if a.ints <> b.ints then raise NotEqual;
108      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.times b.times;
109        Boolean.equal (fun (x1,x2) (y1,y2) -> e x1 y1; e x2 y2) a.xml b.xml;
110      Boolean.equal (fun (x1,x2) (y1,y2) -> e x1 y1; e x2 y2) a.arrow b.arrow;      Boolean.equal (fun (x1,x2) (y1,y2) -> e x1 y1; e x2 y2) a.arrow b.arrow;
111      Boolean.equal (fun (l1,o1,x1) (l2,o2,x2) ->      Boolean.equal (fun (l1,o1,x1) (l2,o2,x2) ->
112                       if (l1 <> l2) || (o1 <> o2) then raise NotEqual;                       if (l1 <> l2) || (o1 <> o2) then raise NotEqual;
# Line 94  Line 114 
114    
115    let map f a =    let map f a =
116      { times = Boolean.map (fun (x1,x2) -> (f x1, f x2)) a.times;      { times = Boolean.map (fun (x1,x2) -> (f x1, f x2)) a.times;
117          xml   = Boolean.map (fun (x1,x2) -> (f x1, f x2)) a.xml;
118        arrow = Boolean.map (fun (x1,x2) -> (f x1, f x2)) a.arrow;        arrow = Boolean.map (fun (x1,x2) -> (f x1, f x2)) a.arrow;
119        record= Boolean.map (fun (l,o,x) -> (l,o, f x)) a.record;        record= Boolean.map (fun (l,o,x) -> (l,o, f x)) a.record;
120        ints  = a.ints;        ints  = a.ints;
# Line 102  Line 123 
123      }      }
124    
125    let hash h a =    let hash h a =
126      (Hashtbl.hash { map h a with ints = Intervals.empty })      Hashtbl.hash (map h a)
127    (*
128        (Hashtbl.hash { (map h a) with ints = Intervals.empty })
129      + (Intervals.hash a.ints)      + (Intervals.hash a.ints)
130    *)
131    
132    let iter f a =    let iter f a =
133      ignore (map f a)      ignore (map f a)
# Line 112  Line 136 
136  end  end
137    
138    
139  module Algebra = Recursive.Make(I)  module Algebra = Recursive_noshare.Make(I)
140  include I  include I
141  include Algebra  include Algebra
142    module DescrHash =
143  let check d =    Hashtbl.Make(
144    Boolean.check d.times;      struct
145    Boolean.check d.arrow;        type t = descr
146    Boolean.check d.record;        let hash = hash_descr
147    ()        let equal = equal_descr
148        end
149      )
150    
151  (*  (*
152  let define n d = check d; define n d  let define n d = check d; define n d
# Line 131  Line 157 
157    define n d;    define n d;
158    internalize n    internalize n
159    
160    let any_rec = cons { empty with record = Boolean.full }
161    let any_node = make ();;
162    define any_node   {
163      times = Boolean.full;
164      xml   = Boolean.atom
165                (cons { empty with atoms = Atoms.any },
166                 cons (times any_rec any_node));
167      arrow = Boolean.full;
168      record= Boolean.full;
169      ints  = Intervals.any;
170      atoms = Atoms.any;
171      chars = Chars.any;
172    };;
173    internalize any_node;;
174    let any = descr any_node
175    
176  module Positive =  let neg x = diff any x
 struct  
   type rhs = [ `Type of descr | `Cup of v list | `Times of v * v ]  
   and v = { mutable def : rhs; mutable node : node option }  
   
   
   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)  
   
   and make_node v =  
     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  
   
   let forward () = { def = `Cup []; node = None }  
   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])  
   
   let solve v = internalize (make_node v)  
 end  
   
177    
178  let get_record r =  let get_record r =
179    let add = SortedMap.add (fun (o1,t1) (o2,t2) -> (o1&&o2, cap t1 t2)) in    let add = SortedMap.add (fun (o1,t1) (o2,t2) -> (o1&&o2, cap t1 t2)) in
# Line 180  Line 185 
185    List.map line r    List.map line r
186    
187    
188  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  
189    
190  let label s =  let check d =
191    try Hashtbl.find label_table s    Boolean.check d.times;
192    with Not_found ->    Boolean.check d.xml;
193      incr counter_label;    Boolean.check d.arrow;
194      Hashtbl.add label_table s !counter_label;    Boolean.check d.record;
195      Hashtbl.add label_names !counter_label s;    ()
     !counter_label  
   
 let label_name l =  
   Hashtbl.find label_names l  
196    
 let mk_atom = label  
197    
 let atom_name = label_name  
198    
199  (* Subtyping algorithm *)  (* Subtyping algorithm *)
200    
201  let diff_t d t = diff d (descr t)  let diff_t d t = diff d (descr t)
202  let cap_t d t = cap d (descr t)  let cap_t d t = cap d (descr t)
203    let cup_t d t = cup d (descr t)
204  let cap_product l =  let cap_product l =
205    List.fold_left    List.fold_left
206      (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))
# Line 210  Line 208 
208      l      l
209    
210    
211    let cup_product l =
212      List.fold_left
213        (fun (d1,d2) (t1,t2) -> (cup_t d1 t1, cup_t d2 t2))
214        (empty,empty)
215        l
216    
217    
218  module Assumptions = Set.Make(struct type t = descr let compare = compare end)  module Assumptions = Set.Make(struct type t = descr let compare = compare end)
219    
220  let memo = ref Assumptions.empty  let memo = ref Assumptions.empty
# Line 228  Line 233 
233      memo := Assumptions.add d backup;      memo := Assumptions.add d backup;
234      if      if
235        (empty_rec_times d.times) &&        (empty_rec_times d.times) &&
236          (empty_rec_times d.xml) &&
237        (empty_rec_arrow d.arrow) &&        (empty_rec_arrow d.arrow) &&
238        (empty_rec_record d.record)        (empty_rec_record d.record)
239      then true      then true
# Line 252  Line 258 
258    in    in
259    let (accu1,accu2) = cap_product left in    let (accu1,accu2) = cap_product left in
260    (empty_rec accu1) || (empty_rec accu2) ||    (empty_rec accu1) || (empty_rec accu2) ||
261    (* OPT? It does'nt seem so ...  The hope was to return false quickly
262       for large right hand-side *)
263      (
264        ((*if (List length right > 2) then
265           let (cup1,cup2) = cup_product right in
266           (empty_rec (diff accu1 cup1)) && (empty_rec (diff accu2 cup2))
267         else*) true)
268        &&
269    (try aux accu1 accu2 right; true with NotEmpty -> false)    (try aux accu1 accu2 right; true with NotEmpty -> false)
270      )
271    
272  and empty_rec_arrow c =  and empty_rec_arrow c =
273    List.for_all empty_rec_arrow_aux c    List.for_all empty_rec_arrow_aux c
# Line 290  Line 305 
305  let subtype d1 d2 =  let subtype d1 d2 =
306    is_empty (diff d1 d2)    is_empty (diff d1 d2)
307    
308  (* Sample value *)  module Product =
 module Sample =  
309  struct  struct
310      type t = (descr * descr) list
311    
312  let rec find f = function    let other ?(kind=`Normal) d =
313    | [] -> raise Not_found      match kind with
314    | x::r -> try f x with Not_found -> find f r        | `Normal -> { d with times = empty.times }
315          | `XML -> { d with xml = empty.xml }
 type t =  
   | Int of Big_int.big_int  
   | Atom of atom  
   | Char of Chars.Unichar.t  
   | Pair of t * t  
   | Record of (label * t) list  
   | Fun of (node * node) list  
316    
317  let rec gen_atom i l =    let is_product ?kind d = is_empty (other ?kind d)
   if SortedList.mem l i then gen_atom (succ i) l  else i  
318    
319  let rec sample_rec memo d =    let need_second = function _::_::_ -> true | _ -> false
   if (Assumptions.mem d memo) || (is_empty d) then raise Not_found  
   else  
     try Int (Intervals.sample d.ints) with Not_found ->  
     try Atom (Atoms.sample (gen_atom 0) d.atoms) with Not_found ->  
     try Char (Chars.sample d.chars) with Not_found ->  
     try sample_rec_arrow d.arrow with Not_found ->  
320    
321      let memo = Assumptions.add d memo in    let normal_aux d =
322      try sample_rec_times memo d.times with Not_found ->      let res = ref [] in
     try sample_rec_record memo d.record with Not_found ->  
     raise Not_found  
323    
324        let add (t1,t2) =
325          let rec loop t1 t2 = function
326            | [] -> res := (ref (t1,t2)) :: !res
327            | ({contents = (d1,d2)} as r)::l ->
328                (*OPT*)
329                if d1 = t1 then r := (d1,cup d2 t2) else
330    
331  and sample_rec_times memo c =                let i = cap t1 d1 in
332    find (sample_rec_times_aux memo) c                if is_empty i then loop t1 t2 l
333                  else (
334                    r := (i, cup t2 d2);
335                    let k = diff d1 t1 in
336                    if non_empty k then res := (ref (k,d2)) :: !res;
337    
338  and sample_rec_times_aux memo (left,right) =                  let j = diff t1 d1 in
339    let rec aux accu1 accu2 = function                  if non_empty j then loop j t2 l
340      | (t1,t2)::right ->                )
         let accu1' = diff_t accu1 t1 in  
         if non_empty accu1' then aux accu1' accu2 right else  
           let accu2' = diff_t accu2 t2 in  
           if non_empty accu2' then aux accu1 accu2' right else  
             raise Not_found  
     | [] -> Pair (sample_rec memo accu1, sample_rec memo accu2)  
341    in    in
342    let (accu1,accu2) = cap_product left in        loop t1 t2 !res
   if (is_empty accu1) || (is_empty accu2) then raise Not_found;  
   aux accu1 accu2 right  
   
 and sample_rec_arrow c =  
   find sample_rec_arrow_aux c  
   
 and check_empty_simple_arrow_line left (s1,s2) =  
   let rec aux accu1 accu2 = function  
     | (t1,t2)::left ->  
         let accu1' = diff_t accu1 t1 in  
         if non_empty accu1' then aux accu1 accu2 left;  
         let accu2' = cap_t accu2 t2 in  
         if non_empty accu2' then aux accu1 accu2 left  
     | [] -> raise NotEmpty  
343    in    in
344    let accu1 = descr s1 in      List.iter add d;
345    (is_empty accu1) ||      List.map (!) !res
   (try aux accu1 (diff any (descr s2)) left; true with NotEmpty -> false)  
   
 and check_empty_arrow_line left right =  
   List.exists (check_empty_simple_arrow_line left) right  
   
 and sample_rec_arrow_aux (left,right) =  
   if (check_empty_arrow_line left right) then raise Not_found  
   else Fun left  
   
   
 and sample_rec_record memo c =  
   Record (find (sample_rec_record_aux memo) (get_record c))  
   
 and sample_rec_record_aux memo fields =  
   let aux acc (l,(o,t)) = if o then acc else (l, sample_rec memo t) :: acc in  
   List.fold_left aux [] fields  
   
 let get x = sample_rec Assumptions.empty x  
   
 end  
   
   
 module Product =  
 struct  
   type t = (descr * descr) list  
   
   let other d = { d with times = empty.times }  
   let is_product d = is_empty (other d)  
   
   let need_second = function _::_::_ -> true | _ -> false  
346    
347    let get d =  (*
348    This version explodes when dealing with
349       Any - [ t1? t2? t3? ... tn? ]
350    ==> need partitioning
351    *)
352      let get_aux d =
353      let line accu (left,right) =      let line accu (left,right) =
354        let rec aux accu d1 d2 = function        let rec aux accu d1 d2 = function
355          | (t1,t2)::right ->          | (t1,t2)::right ->
# Line 401  Line 365 
365        let (d1,d2) = cap_product left in        let (d1,d2) = cap_product left in
366        if (is_empty d1) || (is_empty d2) then accu else aux accu d1 d2 right        if (is_empty d1) || (is_empty d2) then accu else aux accu d1 d2 right
367      in      in
368      List.fold_left line [] d.times      List.fold_left line [] d
369    
370    (* Partitioning:
371    
372    (t,s) - ((t1,s1) | (t2,s2) | ... | (tn,sn))
373    =
374    (t & t1, s - s1) | ... | (t & tn, s - sn) | (t - (t1|...|tn), s)
375    
376    *)
377    
378      let get_aux d =
379        let accu = ref [] in
380        let line (left,right) =
381          let (d1,d2) = cap_product left in
382          if (non_empty d1) && (non_empty d2) then
383            let right = List.map (fun (t1,t2) -> descr t1, descr t2) right in
384            let right = normal_aux right in
385            let resid1 = ref d1 in
386            let () =
387              List.iter
388                (fun (t1,t2) ->
389                   let t1 = cap d1 t1 in
390                   if (non_empty t1) then
391                     let () = resid1 := diff !resid1 t1 in
392                     let t2 = diff d2 t2 in
393                     if (non_empty t2) then accu := (t1,t2) :: !accu
394                ) right in
395            if non_empty !resid1 then accu := (!resid1, d2) :: !accu
396        in
397        List.iter line d;
398        !accu
399    
400      let get ?(kind=`Normal) d =
401        match kind with
402          | `Normal -> get_aux d.times
403          | `XML -> get_aux d.xml
404    
405    let pi1 = List.fold_left (fun acc (t1,_) -> cup acc t1) empty    let pi1 = List.fold_left (fun acc (t1,_) -> cup acc t1) empty
406    let pi2 = List.fold_left (fun acc (_,t2) -> cup acc t2) empty    let pi2 = List.fold_left (fun acc (_,t2) -> cup acc t2) empty
# Line 413  Line 412 
412    
413    type normal = t    type normal = t
414    
415    let normal d =    module Memo = Map.Make(struct
416      let res = ref [] in                             type t = (node * node) Boolean.t
417                               let compare = compare end)
418    
     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  
419    
               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;  
420    
421                  let j = diff t1 d1 in    let memo = ref Memo.empty
422                  if non_empty j then loop j t2 l    let normal ?(kind=`Normal) d =
423                )      let d = match kind with `Normal -> d.times | `XML -> d.xml in
424        in      try Memo.find d !memo
425        loop t1 t2 !res      with
426      in          Not_found ->
427      List.iter add (get d);            let gd = get_aux d in
428      List.map (!) !res            let n = normal_aux gd in
429              memo := Memo.add d n !memo;
430              n
431    
432    let any = { empty with times = any.times }    let any = { empty with times = any.times }
433      and any_xml = { empty with xml = any.xml }
434    let is_empty d = d = []    let is_empty d = d = []
435  end  end
436    
437    module Print =
 module Record =  
438  struct  struct
439    type t = (label, (bool * descr)) SortedMap.t list    let rec print_union ppf = function
440        | [] -> Format.fprintf ppf "Empty"
441    let get d =      | [h] -> h ppf
442      let line r = List.for_all (fun (l,(o,d)) -> o || non_empty d) r in      | h::t -> Format.fprintf ppf "@[%t |@ %a@]" h print_union t
     List.filter line (get_record d.record)  
443    
444      let print_atom ppf a =
445        Format.fprintf ppf "`%s" (AtomPool.value a)
446    
447    let restrict_label_present t l =    let print_tag ppf a =
448      let restr = function      match Atoms.is_atom a with
449        | (true, d) -> if non_empty d then (false,d) else raise Exit        | Some a -> Format.fprintf ppf "%s" (AtomPool.value a)
450        | x -> x in        | None ->
451      let aux accu r =            Format.fprintf ppf "(%a)"
452        try SortedMap.change l restr (false,any) r :: accu              print_union
453        with Exit -> accu in                 (Atoms.print "Atom" print_atom a)
     List.fold_left aux [] t  
454    
455    let restrict_label_absent t l =    let print_const ppf = function
456      let restr = function (true, _) -> (true,empty) | _ -> raise Exit in      | Integer i -> Format.fprintf ppf "%s" (Big_int.string_of_big_int i)
457      let aux accu r =      | Atom a -> print_atom ppf a
458        try SortedMap.change l restr (true,empty) r :: accu      | Char c -> Chars.Unichar.print ppf c
       with Exit -> accu in  
     List.fold_left aux [] t  
459    
460    let restrict_field t l d =    let named = State.ref "Types.Printf.named" DescrMap.empty
461      let restr (_,d1) =    let register_global name d =
462        let d1 = cap d d1 in      named := DescrMap.add d name !named
       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  
   
   let project d l =  
     project_field (get_record d.record) l  
   
   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)  
           else  
             let res = ref [] in  
             let aux a (t,x) =  
               (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  
             in  
             let t2 = List.fold_left aux t2 present in  
             let () =  
               if non_empty t2 then  
               res := (t2, merge_record `Fail r') :: !res in  
             let abs = if o then merge_record absent r' else absent in  
             `Label (l1, !res, abs)  
   
   
   let normal d =  
     List.fold_left merge_record `Fail (get d)  
   
   
   let any = { empty with record = any.record }  
   let is_empty d = d = []  
 end  
   
   
 module DescrHash =  
   Hashtbl.Make(  
     struct  
       type t = descr  
       let hash = hash_descr  
       let equal = equal_descr  
     end  
   )  
   
 module MapDescr = Map.Make(struct type t = descr let compare = compare end)  
   
 let memo_normalize = DescrHash.create 17  
   
 let map_sort f l =  
   SortedList.from_list (List.map f l)  
   
 let rec rec_normalize d =  
   try DescrHash.find memo_normalize d  
   with Not_found ->  
     let n = make () in  
     DescrHash.add memo_normalize d n;  
     let times =  
       map_sort  
         (fun (d1,d2) -> [(rec_normalize d1, rec_normalize d2)],[])  
         (Product.normal d)  
     in  
     let record =  
       map_sort  
         (fun f -> map_sort (fun (l,(o,d)) -> (l,o,rec_normalize d)) f, [])  
         (Record.get d)  
     in  
     define n { d with times = times; record = record };  
     n  
   
 let normalize n =  
   descr (internalize (rec_normalize n))  
   
 module Print =  
 struct  
   let print_atom ppf a = Format.fprintf ppf "`%s" (atom_name a)  
   
   let print_const ppf = function  
     | Integer i -> Format.fprintf ppf "%s" (Big_int.string_of_big_int i)  
     | Atom a -> print_atom ppf a  
     | Char c -> Chars.Unichar.print ppf c  
   
   let named = DescrHash.create 10  
   let register_global name d = DescrHash.add named d name  
463    
464    let marks = DescrHash.create 63    let marks = DescrHash.create 63
465    let wh = ref []    let wh = ref []
# Line 601  Line 480 
480    
481    let rec mark n = mark_descr (descr n)    let rec mark n = mark_descr (descr n)
482    and mark_descr d =    and mark_descr d =
483      if not (DescrHash.mem named d) then      if not (DescrMap.mem d !named) then
484        try        try
485          let r = DescrHash.find marks d in          let r = DescrHash.find marks d in
486          if (!r = None) && (worth_abbrev d) then          if (!r = None) && (worth_abbrev d) then
# Line 611  Line 490 
490        with Not_found ->        with Not_found ->
491          DescrHash.add marks d (ref None);          DescrHash.add marks d (ref None);
492          bool_iter (fun (n1,n2) -> mark n1; mark n2) d.times;          bool_iter (fun (n1,n2) -> mark n1; mark n2) d.times;
493            bool_iter
494              (fun (n1,n2) ->
495                 List.iter
496                   (fun (d1,d2) ->
497                      mark_descr d2;
498                      let l = get_record d1.record in
499                      List.iter (List.iter (fun (l,(o,d)) -> mark_descr d)) l
500                   )
501                   (Product.normal (descr n2))
502              ) d.xml;
503          bool_iter (fun (n1,n2) -> mark n1; mark n2) d.arrow;          bool_iter (fun (n1,n2) -> mark n1; mark n2) d.arrow;
504          bool_iter (fun (l,o,n) -> mark n) d.record          bool_iter (fun (l,o,n) -> mark n) d.record
505    
506    
   let rec print_union ppf = function  
     | [] -> Format.fprintf ppf "Empty"  
     | [h] -> h ppf  
     | h::t -> Format.fprintf ppf "@[%t |@ %a@]" h print_union t  
   
   
507    let rec print ppf n = print_descr ppf (descr n)    let rec print ppf n = print_descr ppf (descr n)
508    and print_descr ppf d =    and print_descr ppf d =
509      try      try
510        let name = DescrHash.find named d in        let name = DescrMap.find d !named in
511        Format.fprintf ppf "%s" name        Format.fprintf ppf "%s" name
512      with Not_found ->      with Not_found ->
513        try        try
# Line 632  Line 515 
515            | Some n -> Format.fprintf ppf "%s" n            | Some n -> Format.fprintf ppf "%s" n
516            | None -> real_print_descr ppf d            | None -> real_print_descr ppf d
517        with        with
518            Not_found -> Format.fprintf ppf "XXX"            Not_found -> assert false
519    and real_print_descr ppf d =    and real_print_descr ppf d =
520      if d = any then Format.fprintf ppf "Any" else      if d = any then Format.fprintf ppf "Any" else
521        print_union ppf        print_union ppf
# Line 640  Line 523 
523           Chars.print d.chars @           Chars.print d.chars @
524           Atoms.print "Atom" print_atom d.atoms @           Atoms.print "Atom" print_atom d.atoms @
525           Boolean.print "Pair" print_times d.times @           Boolean.print "Pair" print_times d.times @
526             Boolean.print "XML" print_xml d.xml @
527           Boolean.print "Arrow" print_arrow d.arrow @           Boolean.print "Arrow" print_arrow d.arrow @
528           Boolean.print "Record" print_record d.record           Boolean.print "Record" print_record d.record
529          )          )
530    and print_times ppf (t1,t2) =    and print_times ppf (t1,t2) =
531      Format.fprintf ppf "@[(%a,%a)@]" print t1 print t2      Format.fprintf ppf "@[(%a,%a)@]" print t1 print t2
532      and print_xml ppf (t1,t2) =
533        let l = Product.normal (descr t2) in
534        let l = List.map
535                  (fun (d1,d2) ppf ->
536                     Format.fprintf ppf "@[<><%a%a>%a@]"
537                       print_tag (descr t1).atoms
538                       print_attribs d1.record
539                       print_descr d2) l
540        in
541        print_union ppf l
542    and print_arrow ppf (t1,t2) =    and print_arrow ppf (t1,t2) =
543      Format.fprintf ppf "@[(%a -> %a)@]" print t1 print t2      Format.fprintf ppf "@[(%a -> %a)@]" print t1 print t2
544    and print_record ppf (l,o,t) =    and print_record ppf (l,o,t) =
545      Format.fprintf ppf "@[{ %s =%s %a }@]"      Format.fprintf ppf "@[{ %s =%s %a }@]"
546        (label_name l) (if o then "?" else "") print t        (LabelPool.value l) (if o then "?" else "") print t
547      and print_attribs ppf r =
548        let l = get_record r in
549        if l <> [ [] ] then
550        let l = List.map
551          (fun att ppf ->
552             let first = ref true in
553             Format.fprintf ppf "{" ;
554             List.iter (fun (l,(o,d)) ->
555                          Format.fprintf ppf "%s%s=%s%a"
556                            (if !first then "" else " ")
557                            (LabelPool.value l) (if o then "?" else "")
558                            print_descr d;
559                          first := false
560                       ) att;
561               Format.fprintf ppf "}"
562          ) l in
563        print_union ppf l
564    
565    
566    let end_print ppf =    let end_print ppf =
# Line 675  Line 586 
586    
587     let print ppf n = print_descr ppf (descr n)     let print ppf n = print_descr ppf (descr n)
588    
589    end
590    
591    
592    
593    module Positive =
594    struct
595      type rhs = [ `Type of descr | `Cup of v list | `Times of v * v ]
596      and v = { mutable def : rhs; mutable node : node option }
597    
598    
599      let rec make_descr seen v =
600        if List.memq v seen then empty
601        else
602          let seen = v :: seen in
603          match v.def with
604            | `Type d -> d
605            | `Cup vl ->
606                List.fold_left (fun acc v -> cup acc (make_descr seen v)) empty vl
607            | `Times (v1,v2) -> times (make_node v1) (make_node v2)
608    
609      and make_node v =
610        match v.node with
611          | Some n -> n
612          | None ->
613              let n = make () in
614              v.node <- Some n;
615              let d = make_descr [] v in
616              define n d;
617              n
618    
619      let forward () = { def = `Cup []; node = None }
620      let def v d = v.def <- d
621      let cons d = let v = forward () in def v d; v
622      let ty d = cons (`Type d)
623      let cup vl = cons (`Cup vl)
624      let times d1 d2 = cons (`Times (d1,d2))
625      let define v1 v2 = def v1 (`Cup [v2])
626    
627      let solve v = internalize (make_node v)
628    end
629    
630    
631    
632    
633    (* Sample value *)
634    module Sample =
635    struct
636    
637    let rec find f = function
638      | [] -> raise Not_found
639      | x::r -> try f x with Not_found -> find f r
640    
641    type t =
642      | Int of Big_int.big_int
643      | Atom of atom
644      | Char of Chars.Unichar.t
645      | Pair of (t * t)
646      | Xml of (t * t)
647      | Record of (label * t) list
648      | Fun of (node * node) list
649    
650    let rec sample_rec memo d =
651      if (Assumptions.mem d memo) || (is_empty d) then raise Not_found
652      else
653        try Int (Intervals.sample d.ints) with Not_found ->
654        try Atom (Atoms.sample (fun _ -> AtomPool.dummy_min) d.atoms) with
655            Not_found ->
656    (* Here: could create a fresh atom ... *)
657        try Char (Chars.sample d.chars) with Not_found ->
658        try sample_rec_arrow d.arrow with Not_found ->
659    
660        let memo = Assumptions.add d memo in
661        try Pair (sample_rec_times memo d.times) with Not_found ->
662        try Xml (sample_rec_times memo d.xml) with Not_found ->
663        try sample_rec_record memo d.record with Not_found ->
664        raise Not_found
665    
666    
667    and sample_rec_times memo c =
668      find (sample_rec_times_aux memo) c
669    
670    and sample_rec_times_aux memo (left,right) =
671      let rec aux accu1 accu2 = function
672        | (t1,t2)::right ->
673            let accu1' = diff_t accu1 t1 in
674            if non_empty accu1' then aux accu1' accu2 right else
675              let accu2' = diff_t accu2 t2 in
676              if non_empty accu2' then aux accu1 accu2' right else
677                raise Not_found
678        | [] -> (sample_rec memo accu1, sample_rec memo accu2)
679      in
680      let (accu1,accu2) = cap_product left in
681      if (is_empty accu1) || (is_empty accu2) then raise Not_found;
682      aux accu1 accu2 right
683    
684    and sample_rec_arrow c =
685      find sample_rec_arrow_aux c
686    
687    and check_empty_simple_arrow_line left (s1,s2) =
688      let rec aux accu1 accu2 = function
689        | (t1,t2)::left ->
690            let accu1' = diff_t accu1 t1 in
691            if non_empty accu1' then aux accu1 accu2 left;
692            let accu2' = cap_t accu2 t2 in
693            if non_empty accu2' then aux accu1 accu2 left
694        | [] -> raise NotEmpty
695      in
696      let accu1 = descr s1 in
697      (is_empty accu1) ||
698      (try aux accu1 (diff any (descr s2)) left; true with NotEmpty -> false)
699    
700    and check_empty_arrow_line left right =
701      List.exists (check_empty_simple_arrow_line left) right
702    
703    and sample_rec_arrow_aux (left,right) =
704      if (check_empty_arrow_line left right) then raise Not_found
705      else Fun left
706    
707    
708    and sample_rec_record memo c =
709      Record (find (sample_rec_record_aux memo) (get_record c))
710    
711    and sample_rec_record_aux memo fields =
712      let aux acc (l,(o,t)) = if o then acc else (l, sample_rec memo t) :: acc in
713      List.fold_left aux [] fields
714    
715    let get x = sample_rec Assumptions.empty x
716    
717    let rec print_sep f sep ppf = function    let rec print_sep f sep ppf = function
718      | [] -> ()      | [] -> ()
719      | [x] -> f ppf x      | [x] -> f ppf x
720      | x::rem -> f ppf x; Format.fprintf ppf "%s" sep; print_sep f sep ppf rem      | x::rem -> f ppf x; Format.fprintf ppf "%s" sep; print_sep f sep ppf rem
721    
722    
723    let rec print_sample ppf = function    let rec print ppf = function
724      | Sample.Int i -> Format.fprintf ppf "%s" (Big_int.string_of_big_int i)      | Int i -> Format.fprintf ppf "%s" (Big_int.string_of_big_int i)
725      | Sample.Atom a -> Format.fprintf ppf "`%s" (atom_name a)      | Atom a ->
726      | Sample.Char c -> Chars.Unichar.print ppf c          if a = LabelPool.dummy_min then
727      | Sample.Pair (x1,x2) ->            Format.fprintf ppf "(almost any atom)"
728          Format.fprintf ppf "(%a,%a)"          else
729          print_sample x1            Format.fprintf ppf "`%s" (AtomPool.value a)
730          print_sample x2      | Char c -> Chars.Unichar.print ppf c
731      | Sample.Record r ->      | Pair (x1,x2) -> Format.fprintf ppf "(%a,%a)" print x1 print x2
732        | Xml (x1,x2) -> Format.fprintf ppf "XML(%a,%a)" print x1 print x2
733        | Record r ->
734          Format.fprintf ppf "{ %a }"          Format.fprintf ppf "{ %a }"
735            (print_sep            (print_sep
736               (fun ppf (l,x) ->               (fun ppf (l,x) ->
737                  Format.fprintf ppf "%s = %a"                  Format.fprintf ppf "%s = %a"
738                  (label_name l)                  (LabelPool.value l)
739                  print_sample x                  print x
740               )               )
741               " ; "               " ; "
742            ) r            ) r
743      | Sample.Fun iface ->      | Fun iface ->
744          Format.fprintf ppf "(fun ( %a ) x -> ...)"          Format.fprintf ppf "(fun ( %a ) x -> ...)"
745            (print_sep            (print_sep
746               (fun ppf (t1,t2) ->               (fun ppf (t1,t2) ->
747                  Format.fprintf ppf "%a -> %a; "                  Format.fprintf ppf "%a -> %a; "
748                  print t1 print t2                  Print.print t1 Print.print t2
749               )               )
750               " ; "               " ; "
751            ) iface            ) iface
752  end  end
753    
754    
755    
756    module Record =
757    struct
758      type t = (label, (bool * descr)) SortedMap.t list
759    
760      let get d =
761        let line r = List.for_all (fun (l,(o,d)) -> o || non_empty d) r in
762        List.filter line (get_record d.record)
763    
764      let restrict_label_present t l =
765        let restr = function
766          | (true, d) -> if non_empty d then (false,d) else raise Exit
767          | x -> x in
768        let aux accu r =
769          try SortedMap.change l restr (false,any) r :: accu
770          with Exit -> accu in
771        List.fold_left aux [] t
772    
773      let restrict_label_absent t l =
774        let restr = function (true, _) -> (true,empty) | _ -> raise Exit in
775        let aux accu r =
776          try SortedMap.change l restr (true,empty) r :: accu
777          with Exit -> accu in
778        List.fold_left aux [] t
779    
780      let restrict_field t l d =
781        let restr (_,d1) =
782          let d1 = cap d d1 in
783          if is_empty d1 then raise Exit else (false,d1) in
784        let aux accu r =
785          try SortedMap.change l restr (false,d) r :: accu
786          with Exit -> accu in
787        List.fold_left aux [] t
788    
789      let project_field t l =
790        let aux accu x =
791          match List.assoc l x with
792            | (false,t) -> cup accu t
793            | _ -> raise Not_found
794        in
795        List.fold_left aux empty t
796    
797      let project d l =
798        project_field (get_record d.record) l
799    
800      type normal =
801          [ `Success
802          | `Fail
803          | `Label of label * (descr * normal) list * normal ]
804    
805      let rec merge_record n r =
806        match (n, r) with
807          | (`Success, _) | (_, []) -> `Success
808          | (`Fail, r) ->
809              let aux (l,(o,t)) n =
810                `Label (l, [t,n], if o then n else `Fail) in
811              List.fold_right aux r `Success
812          | (`Label (l1,present,absent), (l2,(o,t2))::r') ->
813              if (l1 < l2) then
814                let pr =  List.map (fun (t,x) -> (t, merge_record x r)) present in
815                let t = List.fold_left (fun a (t,_) -> diff a t) any present in
816                let pr =
817                  if non_empty t then (t, merge_record `Fail r) :: pr
818                  else pr in
819                `Label (l1,pr,merge_record absent r)
820              else if (l2 < l1) then
821                let n' = merge_record n r' in
822                `Label (l2, [t2, n'], if o then n' else n)
823              else
824                let res = ref [] in
825                let aux a (t,x) =
826                  (let t = diff t t2 in
827                   if non_empty t then res := (t,x) :: !res);
828                  (let t = cap t t2 in
829                   if non_empty t then res := (t, merge_record x r') :: !res);
830                  diff a t
831                in
832                let t2 = List.fold_left aux t2 present in
833                let () =
834                  if non_empty t2 then
835                  res := (t2, merge_record `Fail r') :: !res in
836                let abs = if o then merge_record absent r' else absent in
837                `Label (l1, !res, abs)
838    
839      module Unify = Map.Make(struct type t = normal let compare = compare end)
840    
841      let repository = ref Unify.empty
842    
843      let rec canonize = function
844        | `Label (l,pr,ab) as x ->
845            (try Unify.find x !repository
846             with Not_found ->
847               let pr = List.map (fun (t,n) -> canonize n,t) pr in
848               let pr = SortedMap.from_list cup pr in
849               let pr = List.map (fun (n,t) -> (t,n)) pr in
850               let x = `Label (l, pr, canonize ab) in
851               try Unify.find x !repository
852               with Not_found -> repository := Unify.add x x !repository; x
853            )
854        | x -> x
855    
856      let normal d =
857        let r = canonize (List.fold_left merge_record `Fail (get d)) in
858        repository := Unify.empty;
859        r
860    
861      type normal' =
862          [ `Success
863          | `Label of label * (descr * descr) list * descr option ] option
864    
865    (* NOTE: this function relies on the fact that generic order
866             makes smallest labels appear first *)
867    
868      let first_label d =
869        let d = d.record in
870        let min = ref None in
871        let lab (l,o,t) = match !min with
872          | Some l' when l >= l' -> ()
873          | _ -> if o && (descr t = any) then () else min := Some l in
874        let line (p,n) =
875          (match p with f::_ -> lab f | _ -> ());
876          (match n with f::_ -> lab f | _ -> ()) in
877        List.iter line d;
878        match !min with
879          | None -> if d = [] then `Empty else `Any
880          | Some l -> `Label l
881    
882      let normal' (d : descr) l =
883        let ab = ref empty in
884        let rec extract f = function
885          | (l',o,t) :: rem when l = l' ->
886              f o (descr t); extract f rem
887          | x :: rem -> x :: (extract f rem)
888          | [] -> [] in
889        let line (p,n) =
890          let ao = ref true and ad = ref any in
891          let p =
892            extract (fun o d -> ao := !ao && o; ad := cap !ad d) p
893          and n =
894            extract (fun o d -> ao := !ao && not o; ad := diff !ad d) n
895          in
896          (* Note: p and n are still sorted *)
897          let d = { empty with record = [(p,n)] } in
898          if !ao then ab := cup d !ab;
899          (!ad, d) in
900        let pr = List.map line d.record in
901        let pr = Product.normal_aux pr in
902        let ab = if is_empty !ab then None else Some !ab in
903        (pr, ab)
904    
905    
906      let any = { empty with record = any.record }
907      let is_empty d = d = []
908      let descr l =
909        let line l = map_sort (fun (l,(o,d)) -> (l,o,cons d)) l, [] in
910        { empty with record = map_sort line l }
911    end
912    
913    
914    
915    let memo_normalize = ref DescrMap.empty
916    
917    
918    let rec rec_normalize d =
919      try DescrMap.find d !memo_normalize
920      with Not_found ->
921        let n = make () in
922        memo_normalize := DescrMap.add d n !memo_normalize;
923        let times =
924          map_sort
925            (fun (d1,d2) -> [(rec_normalize d1, rec_normalize d2)],[])
926            (Product.normal d)
927        in
928        let xml =
929          map_sort
930            (fun (d1,d2) -> [(rec_normalize d1, rec_normalize d2)],[])
931            (Product.normal ~kind:`XML d)
932        in
933        let record =
934          map_sort
935            (fun f -> map_sort (fun (l,(o,d)) -> (l,o,rec_normalize d)) f, [])
936            (Record.get d)
937        in
938        define n { d with times = times; xml = xml; record = record };
939        n
940    
941    let normalize n =
942      descr (internalize (rec_normalize n))
943    
944  module Arrow =  module Arrow =
945  struct  struct
946    let check_simple left s1 s2 =    let check_simple left s1 s2 =
# Line 833  Line 1064 
1064    
1065  module Char = struct  module Char = struct
1066    let has_char d c = Chars.contains c d.chars    let has_char d c = Chars.contains c d.chars
1067      let any = { empty with chars = Chars.any }
1068  end  end
1069    
1070  (*  (*
Legend:
Removed from v.45  
changed lines
  Added in v.111
CVS Admin">CVS Admin
 ViewVC Help
Powered by ViewVC 1.1.5