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

Diff of /types/types.ml

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

revision 228 by abate, Tue Jul 10 17:16:34 2007 UTC revision 229 by abate, Tue Jul 10 17:17:01 2007 UTC
# Line 45  Line 45 
45    times : descr BoolPair.t;    times : descr BoolPair.t;
46    xml   : descr BoolPair.t;    xml   : descr BoolPair.t;
47    arrow : descr BoolPair.t;    arrow : descr BoolPair.t;
48    record: (bool * (label, (bool * node)) SortedMap.t) Boolean.t;    record: (bool * (label, node) SortedMap.t) Boolean.t;
49      absent: bool
50  } and node = descr node0  } and node = descr node0
51    
52    
# Line 57  Line 58 
58    ints  = Intervals.empty;    ints  = Intervals.empty;
59    atoms = Atoms.empty;    atoms = Atoms.empty;
60    chars = Chars.empty;    chars = Chars.empty;
61      absent= false;
62  }  }
63    
64  let any =  {  let any =  {
# Line 67  Line 69 
69    ints  = Intervals.any;    ints  = Intervals.any;
70    atoms = Atoms.any;    atoms = Atoms.any;
71    chars = Chars.any;    chars = Chars.any;
72      absent= false;
73  }  }
74    
75    
# Line 74  Line 77 
77  let times x y = { empty with times = BoolPair.atom (x,y) }  let times x y = { empty with times = BoolPair.atom (x,y) }
78  let xml x y = { empty with xml = BoolPair.atom (x,y) }  let xml x y = { empty with xml = BoolPair.atom (x,y) }
79  let arrow x y = { empty with arrow = BoolPair.atom (x,y) }  let arrow x y = { empty with arrow = BoolPair.atom (x,y) }
80  let record label opt t =  let record label t =
81    { empty with record = Boolean.atom (true,[label,(opt,t)]) }    { empty with record = Boolean.atom (true,[label,t]) }
82  let record' x =  let record' x =
83    { empty with record = Boolean.atom x }    { empty with record = Boolean.atom x }
84  let atom a = { empty with atoms = a }  let atom a = { empty with atoms = a }
# Line 94  Line 97 
97      ints  = Intervals.cup x.ints  y.ints;      ints  = Intervals.cup x.ints  y.ints;
98      atoms = Atoms.cup x.atoms y.atoms;      atoms = Atoms.cup x.atoms y.atoms;
99      chars = Chars.cup x.chars y.chars;      chars = Chars.cup x.chars y.chars;
100        absent= x.absent || y.absent;
101    }    }
102    
103  let cap x y =  let cap x y =
# Line 105  Line 109 
109      ints  = Intervals.cap x.ints  y.ints;      ints  = Intervals.cap x.ints  y.ints;
110      atoms = Atoms.cap x.atoms y.atoms;      atoms = Atoms.cap x.atoms y.atoms;
111      chars = Chars.cap x.chars y.chars;      chars = Chars.cap x.chars y.chars;
112        absent= x.absent && y.absent;
113    }    }
114    
115  let diff x y =  let diff x y =
# Line 116  Line 121 
121      ints  = Intervals.diff x.ints  y.ints;      ints  = Intervals.diff x.ints  y.ints;
122      atoms = Atoms.diff x.atoms y.atoms;      atoms = Atoms.diff x.atoms y.atoms;
123      chars = Chars.diff x.chars y.chars;      chars = Chars.diff x.chars y.chars;
124        absent= x.absent && not y.absent;
125    }    }
126    
127  let count = ref 0  let count = ref 0
# Line 129  Line 135 
135  let rec compare_rec r1 r2 =  let rec compare_rec r1 r2 =
136    if r1 == r2 then 0    if r1 == r2 then 0
137    else match (r1,r2) with    else match (r1,r2) with
138      | (l1,(o1,x1))::r1,(l2,(o2,x2))::r2 ->      | (l1,x1)::r1,(l2,x2)::r2 ->
139          if ((l1:int) < l2) then -1          if ((l1:int) < l2) then -1
140          else if (l1 > l2) then 1          else if (l1 > l2) then 1
         else if o2 && not o1 then -1  
         else if o1 && not o2 then 1  
141          else if x1.id < x2.id then -1          else if x1.id < x2.id then -1
142          else if x1.id > x2.id then 1          else if x1.id > x2.id then 1
143          else compare_rec r1 r2          else compare_rec r1 r2
# Line 186  Line 190 
190  let rec equal_rec r1 r2 =  let rec equal_rec r1 r2 =
191    (r1 == r2) ||    (r1 == r2) ||
192    match (r1,r2) with    match (r1,r2) with
193      | (l1,(o1,x1))::r1,(l2,(o2,x2))::r2 ->      | (l1,x1)::r1,(l2,x2)::r2 ->
194          (x1.id = x2.id) && (l1 == l2) && (o1 == o2) && (equal_rec r1 r2)          (x1.id = x2.id) && (l1 == l2) && (equal_rec r1 r2)
195      | _ -> false      | _ -> false
196    
197  let rec equal_rec_list l1 l2  =  let rec equal_rec_list l1 l2  =
# Line 232  Line 236 
236    (BoolPair.equal a.times b.times) &&    (BoolPair.equal a.times b.times) &&
237    (BoolPair.equal a.xml b.xml) &&    (BoolPair.equal a.xml b.xml) &&
238    (BoolPair.equal a.arrow b.arrow) &&    (BoolPair.equal a.arrow b.arrow) &&
239    (equal_rec_bool a.record b.record)    (equal_rec_bool a.record b.record) &&
240      (a.absent == b.absent)
241    
242  let compare_descr a b =  let compare_descr a b =
243    let c = compare a.atoms b.atoms in if c <> 0 then c    let c = compare a.atoms b.atoms in if c <> 0 then c
# Line 242  Line 247 
247    else let c = BoolPair.compare a.xml b.xml in if c <> 0 then c    else let c = BoolPair.compare a.xml b.xml in if c <> 0 then c
248    else let c = BoolPair.compare a.arrow b.arrow in if c <> 0 then c    else let c = BoolPair.compare a.arrow b.arrow in if c <> 0 then c
249    else let c = compare_rec_bool a.record b.record in if c <> 0 then c    else let c = compare_rec_bool a.record b.record in if c <> 0 then c
250      else if a.absent && not b.absent then -1
251      else if b.absent && not a.absent then 1
252    else 0    else 0
253    
254  (*  (*
# Line 263  Line 270 
270    | [] -> accu + 3    | [] -> accu + 3
271    
272  let rec hash_rec accu = function  let rec hash_rec accu = function
273    | (l,(o,x))::rem ->    | (l,x)::rem ->
       let accu = if o then accu else accu + 5 in  
274        hash_rec (257 * accu + 17 * (LabelPool.hash l) + x.id) rem        hash_rec (257 * accu + 17 * (LabelPool.hash l) + x.id) rem
275    | [] -> accu + 5    | [] -> accu + 5
276    
# Line 287  Line 293 
293    let accu = 17 * accu + BoolPair.hash a.xml in    let accu = 17 * accu + BoolPair.hash a.xml in
294    let accu = 17 * accu + BoolPair.hash a.arrow in    let accu = 17 * accu + BoolPair.hash a.arrow in
295    let accu = hash_rec_bool accu a.record in    let accu = hash_rec_bool accu a.record in
296      let accu = if a.absent then accu+5 else accu in
297    accu    accu
298    
299  module DescrHash =  module DescrHash =
# Line 309  Line 316 
316  let get_record r =  let get_record r =
317    let labs accu (_,r) =    let labs accu (_,r) =
318      List.fold_left (fun accu (l,_) -> LabelSet.add l accu) accu r in      List.fold_left (fun accu (l,_) -> LabelSet.add l accu) accu r in
319    let extend (opts,descrs) labs (o,r) =    let extend descrs labs (o,r) =
320      let rec aux i labs r =      let rec aux i labs r =
321        match labs with        match labs with
322          | [] -> ()          | [] -> ()
323          | l1::labs ->          | l1::labs ->
324              match r with              match r with
325                | (l2,(o,x))::r when l1 = l2 ->                | (l2,x)::r when l1 == l2 ->
326                    descrs.(i) <- cap descrs.(i) (descr x);                    descrs.(i) <- cap descrs.(i) (descr x);
                   opts.(i) <- opts.(i) && o;  
327                    aux (i+1) labs r                    aux (i+1) labs r
328                | r ->                | r ->
329                    if not o then descrs.(i) <- empty;                    if not o then descrs.(i) <-
330                        cap descrs.(i) { empty with absent = true };
331                    aux (i+1) labs r                    aux (i+1) labs r
332      in      in
333      aux 0 labs r;      aux 0 labs r;
# Line 331  Line 338 
338        List.fold_left labs (List.fold_left labs LabelSet.empty p) n in        List.fold_left labs (List.fold_left labs LabelSet.empty p) n in
339      let labels = LabelSet.elements labels in      let labels = LabelSet.elements labels in
340      let nlab = List.length labels in      let nlab = List.length labels in
341      let mk () = Array.create nlab true, Array.create nlab any in      let mk () = Array.create nlab { any with absent = true } in
342    
343      let pos = mk () in      let pos = mk () in
344      let opos = List.fold_left      let opos = List.fold_left
# Line 422  Line 429 
429  let rec guard a f n =  let rec guard a f n =
430    match slot a with    match slot a with
431      | { status = Empty } -> ()      | { status = Empty } -> ()
432      | { status = Maybe } as s -> n.active <- true; s.notify <- Do (n,f,s.notify)      | { status = Maybe } as s ->
433            n.active <- true; s.notify <- Do (n,f,s.notify)
434      | { status = NEmpty } -> f n      | { status = NEmpty } -> f n
435    
436  and slot d =  and slot d =
437    if not ((Intervals.is_empty d.ints) &&    if not ((Intervals.is_empty d.ints) &&
438            (Atoms.is_empty d.atoms) &&            (Atoms.is_empty d.atoms) &&
439            (Chars.is_empty d.chars)) then slot_not_empty            (Chars.is_empty d.chars) &&
440              (not d.absent)) then slot_not_empty
441    else try DescrHash.find memo d    else try DescrHash.find memo d
442    with Not_found ->    with Not_found ->
443      let s = { status = Maybe; active = false; notify = Nothing } in      let s = { status = Maybe; active = false; notify = Nothing } in
# Line 470  Line 479 
479    in    in
480    big_conj single_right right s    big_conj single_right right s
481    
482  and check_record (labels,(oleft,(left_opt,left)),rights) s =  and check_record (labels,(oleft,left),rights) s =
483    let rec aux rights s = match rights with    let rec aux rights s = match rights with
484      | [] -> set s      | [] -> set s
485      | (oright,(right_opt,right))::rights ->      | (oright,right)::rights ->
486          let next =          let next =
487            (oleft && (not oright)) ||            (oleft && (not oright)) || (* ggg... why ???  check this line *)
488            exists (Array.length left)            exists (Array.length left)
489              (fun i ->              (fun i ->
490                 (not (left_opt.(i) && right_opt.(i))) &&                 trivially_empty (cap left.(i) right.(i)))
                (trivially_empty (cap left.(i) right.(i))))  
491          in          in
492          if next then aux rights s          if next then aux rights s
493          else          else
494            for i = 0 to Array.length left - 1 do            for i = 0 to Array.length left - 1 do
495              let back = left.(i) in              let back = left.(i) in
             let oback = left_opt.(i) in  
             let odi = oback && (not right_opt.(i)) in  
496              let di = diff back right.(i) in              let di = diff back right.(i) in
             if odi then (  
               left.(i) <- diff back right.(i);  
               left_opt.(i) <- odi;  
               aux rights s;  
               left.(i) <- back;  
               left_opt.(i) <- oback;  
             ) else  
497                guard di (fun s ->                guard di (fun s ->
498                            left.(i) <- diff back right.(i);                            left.(i) <- diff back right.(i);
                           left_opt.(i) <- odi;  
499                            aux rights s;                            aux rights s;
500                            left.(i) <- back;                            left.(i) <- back;
                           left_opt.(i) <- oback;  
501                         ) s                         ) s
502            done            done
503    in    in
504    let rec start i s =    let rec start i s =
505      if (i < 0) then aux rights s      if (i < 0) then aux rights s
506      else      else
507        if left_opt.(i) then start (i - 1) s        guard left.(i) (start (i - 1)) s
       else guard left.(i) (start (i - 1)) s  
508    in    in
509    start (Array.length left - 1) s    start (Array.length left - 1) s
510    
# Line 530  Line 526 
526    if not (Intervals.is_empty d.ints) then false    if not (Intervals.is_empty d.ints) then false
527    else if not (Atoms.is_empty d.atoms) then false    else if not (Atoms.is_empty d.atoms) then false
528    else if not (Chars.is_empty d.chars) then false    else if not (Chars.is_empty d.chars) then false
529      else if d.absent then false
530    else if DescrHash.mem cache_false d then false    else if DescrHash.mem cache_false d then false
531    else if Assumptions.mem d !memo then true    else if Assumptions.mem d !memo then true
532    else (    else (
# Line 588  Line 585 
585    in    in
586    List.exists single_right right    List.exists single_right right
587    
588  and empty_rec_record_aux (labels,(oleft,(left_opt,left)),rights) =  and empty_rec_record_aux (labels,(oleft,left),rights) =
589    let rec aux = function    let rec aux = function
590      | [] -> raise NotEmpty      | [] -> raise NotEmpty
591      | (oright,(right_opt,right))::rights ->      | (oright,right)::rights ->
592          let next =          let next =
593            (oleft && (not oright)) ||            (oleft && (not oright)) ||
594            exists (Array.length left)            exists (Array.length left)
595              (fun i ->              (fun i ->
596                 (not (left_opt.(i) && right_opt.(i))) &&                 trivially_empty (cap left.(i) right.(i)))
                (trivially_empty (cap left.(i) right.(i))))  
597          in          in
598          if next then aux rights          if next then aux rights
599          else          else
600            for i = 0 to Array.length left - 1 do            for i = 0 to Array.length left - 1 do
601              let back = left.(i) in              let back = left.(i) in
             let oback = left_opt.(i) in  
             let odi = oback && (not right_opt.(i)) in  
602              let di = diff back right.(i) in              let di = diff back right.(i) in
603              if odi || not (empty_rec di) then (              if not (empty_rec di) then (
604                left.(i) <- diff back right.(i);                left.(i) <- diff back right.(i);
               left_opt.(i) <- odi;  
605                aux rights;                aux rights;
606                left.(i) <- back;                left.(i) <- back;
               left_opt.(i) <- oback;  
607              )              )
608            done            done
609    in    in
610    exists (Array.length left)    exists (Array.length left)
611      (fun i -> not left_opt.(i) && (empty_rec left.(i)))      (fun i -> empty_rec left.(i))
612    ||    ||
613    (try aux rights; true with NotEmpty -> false)    (try aux rights; true with NotEmpty -> false)
614    
# Line 737  Line 729 
729    
730    let pi1 = List.fold_left (fun acc (t1,_) -> cup acc t1) empty    let pi1 = List.fold_left (fun acc (t1,_) -> cup acc t1) empty
731    let pi2 = List.fold_left (fun acc (_,t2) -> cup acc t2) empty    let pi2 = List.fold_left (fun acc (_,t2) -> cup acc t2) empty
732      let pi2_restricted restr =
733        List.fold_left (fun acc (t1,t2) ->
734                          if is_empty (cap t1 restr) then acc
735                          else cup acc t2) empty
736    
737    let restrict_1 rects pi1 =    let restrict_1 rects pi1 =
738      let aux accu (t1,t2) =      let aux acc (t1,t2) =
739        let t1 = cap t1 pi1 in if is_empty t1 then accu else (t1,t2)::accu in        let t1 = cap t1 pi1 in if is_empty t1 then acc else (t1,t2)::acc in
740      List.fold_left aux [] rects      List.fold_left aux [] rects
741    
742    type normal = t    type normal = t
# Line 834  Line 830 
830  *)  *)
831            ) d.xml;            ) d.xml;
832          BoolPair.iter (fun (n1,n2) -> mark n1; mark n2) d.arrow;          BoolPair.iter (fun (n1,n2) -> mark n1; mark n2) d.arrow;
833          Boolean.iter (fun (o,l) -> List.iter (fun (l,(o,n)) -> mark n) l) d.record          Boolean.iter (fun (o,l) -> List.iter (fun (l,n) -> mark n) l) d.record
834    
835    
836    let rec print ppf n = print_descr ppf (descr n)    let rec print ppf n = print_descr ppf (descr n)
# Line 851  Line 847 
847            Not_found -> assert false            Not_found -> assert false
848    and real_print_descr ppf d =    and real_print_descr ppf d =
849      if d = any then Format.fprintf ppf "Any" else      if d = any then Format.fprintf ppf "Any" else
850          (
851            if d.absent then Format.fprintf ppf "?";
852        print_union ppf        print_union ppf
853          (Intervals.print d.ints @          (Intervals.print d.ints @
854           Chars.print d.chars @           Chars.print d.chars @
# Line 860  Line 858 
858           BoolPair.print "Arrow" print_arrow d.arrow @           BoolPair.print "Arrow" print_arrow d.arrow @
859           Boolean.print "Record" print_record d.record           Boolean.print "Record" print_record d.record
860          )          )
861          )
862    and print_times ppf (t1,t2) =    and print_times ppf (t1,t2) =
863      Format.fprintf ppf "@[(%a,%a)@]" print t1 print t2      Format.fprintf ppf "@[(%a,%a)@]" print t1 print t2
864    and print_xml ppf (t1,t2) =    and print_xml ppf (t1,t2) =
# Line 881  Line 880 
880      let o = if o then "" else "|" in      let o = if o then "" else "|" in
881      Format.fprintf ppf "@[{%s" o;      Format.fprintf ppf "@[{%s" o;
882      let first = ref true in      let first = ref true in
883      List.iter (fun (l,(o,t)) ->      List.iter (fun (l,t) ->
884                   let sep = if !first then (first := false; "") else ";" in                   let sep = if !first then (first := false; "") else ";" in
885                   Format.fprintf ppf "%s@ @[%s =%s@] %a" sep                   Format.fprintf ppf "%s@ @[%s =@] %a" sep
886                     (LabelPool.value l) (if o then "?" else "") print t                     (LabelPool.value l) print t
887                ) r;                ) r;
888      Format.fprintf ppf " %s}@]" o      Format.fprintf ppf " %s}@]" o
889  (*  (*
# Line 1058  Line 1057 
1057  and sample_rec_record memo c =  and sample_rec_record memo c =
1058    Record (find (sample_rec_record_aux memo) (get_record c))    Record (find (sample_rec_record_aux memo) (get_record c))
1059    
1060  and sample_rec_record_aux memo (labels,(oleft,(left_opt,left)),rights) =  and sample_rec_record_aux memo (labels,(oleft,left),rights) =
1061    let rec aux = function    let rec aux = function
1062      | [] ->      | [] ->
1063          let l = ref labels and fields = ref [] in          let l = ref labels and fields = ref [] in
1064          for i = 0 to Array.length left - 1 do          for i = 0 to Array.length left - 1 do
           if not left_opt.(i) then  
1065              fields := (List.hd !l, sample_rec memo left.(i))::!fields;              fields := (List.hd !l, sample_rec memo left.(i))::!fields;
1066            l := List.tl !l            l := List.tl !l
1067          done;          done;
1068          raise (FoundSampleRecord (List.rev !fields))          raise (FoundSampleRecord (List.rev !fields))
1069      | (oright,(right_opt,right))::rights ->      | (oright,right)::rights ->
1070          let next = (oleft && (not oright)) in          let next = (oleft && (not oright)) in
1071          if next then aux rights          if next then aux rights
1072          else          else
1073            for i = 0 to Array.length left - 1 do            for i = 0 to Array.length left - 1 do
1074              let back = left.(i) in              let back = left.(i) in
             let oback = left_opt.(i) in  
             let odi = oback && (not right_opt.(i)) in  
1075              let di = diff back right.(i) in              let di = diff back right.(i) in
1076              if odi || not (is_empty di) then (              if not (is_empty di) then (
1077                left.(i) <- diff back right.(i);                left.(i) <- diff back right.(i);
               left_opt.(i) <- odi;  
1078                aux rights;                aux rights;
1079                left.(i) <- back;                left.(i) <- back;
               left_opt.(i) <- oback;  
1080              )              )
1081            done            done
1082    in    in
1083    if exists (Array.length left)    if exists (Array.length left)
1084      (fun i -> not left_opt.(i) && (is_empty left.(i))) then raise Not_found;      (fun i -> is_empty left.(i)) then raise Not_found;
1085    try aux rights; raise Not_found    try aux rights; raise Not_found
1086    with FoundSampleRecord r -> r    with FoundSampleRecord r -> r
1087    
# Line 1136  Line 1130 
1130    
1131  module Record =  module Record =
1132  struct  struct
1133    type atom = bool * (label, (bool * node)) SortedMap.t    let has_record d = not (is_empty { empty with record = d.record })
1134    type t = atom Boolean.t    let or_absent d = { d with absent = true }
1135      let any_or_absent = or_absent any
1136    let get d = d.record    let has_absent d = d.absent
1137    
1138    module T = struct    module T = struct
1139      type t = descr      type t = descr
1140      let any = any      let any = any_or_absent
1141      let cap = cap      let cap = cap
1142      let cup = cup      let cup = cup
1143      let diff = diff      let diff = diff
1144      let empty = is_empty      let is_empty = is_empty
1145        let empty = empty
1146    end    end
1147    module R = struct    module R = struct
1148      (*Note: Boolean.cap,cup,diff would be ok,      type t = descr
1149        but we add here the simplification rules:      let any = { empty with record = any.record }
1150        { } & r --> r    ; { } | r -> { }      let cap = cap
1151        r \ { } --> Empty *)      let cup = cup
1152        let diff = diff
1153      type t = atom Boolean.t      let is_empty = is_empty
1154      let any = Boolean.full      let empty = empty
     let cap =  Boolean.cap  
     let cup = Boolean.cup  
     let diff = Boolean.diff  
     let empty x = is_empty { empty with record = x }  
1155    end    end
1156    module TR = Normal.Make(T)(R)    module TR = Normal.Make(T)(R)
1157    
1158    let atom = function    let atom = function
1159      | (true,[]) -> Boolean.full      | (true,[]) -> { empty with record = Boolean.full }
1160      | (o,l) -> Boolean.atom (o,l)      | (o,l) -> { empty with record = Boolean.atom (o,l) }
   
   let somefield_possible t =  
     not (R.empty (R.diff t (Boolean.atom (false,[]))))  
   
   let nofield_possible t =  
     not (R.empty (R.cap t (Boolean.atom (false,[]))))  
   
   let restrict_label_absent t l =  
     Boolean.compute_bool  
       (fun ((o,r) as x) ->  
          try  
            let (lo,_) = List.assoc l r in  
            if lo then atom (o,SortedMap.diff r [l])  
            else Boolean.empty  
          with Not_found -> Boolean.atom x  
       )  
       t  
   
   let restrict_field t l d =  
     (* Is it correct ?  Do we need to keep track of "first component"  
        (value of l) as in label_present, then filter at the end ... ? *)  
     Boolean.compute_bool  
       (fun ((o,r) as x) ->  
          try  
            let (lo,lt) = List.assoc l r in  
            if (not lo) && (is_empty (cap d (descr lt))) then Boolean.empty  
            else atom (o, SortedMap.diff r [l])  
          with Not_found ->  
            if o then Boolean.atom x else Boolean.empty  
       )  
       t  
1161    
1162      let aux d l=
   
   let label_present (t:t) l : (descr * t) list =  
     let x =  
1163        Boolean.compute_bool        Boolean.compute_bool
1164          (fun ((o,r) as x) ->          (fun ((o,r) as x) ->
1165             try             try
1166               let (_,lt) = List.assoc l r in             let lt = List.assoc l r in
1167               Boolean.atom (descr lt, atom (o, SortedMap.diff r [l]))               Boolean.atom (descr lt, atom (o, SortedMap.diff r [l]))
1168             with Not_found ->             with Not_found ->
1169               if o then Boolean.atom (any, Boolean.atom x) else Boolean.empty             if o then Boolean.atom (or_absent any, atom x)
         )  
         t  
     in  
     TR.boolean x  
   
   let restrict_label_present t l =  
     Boolean.compute_bool  
       (fun ((o,r) as x) ->  
          try  
            Boolean.atom (o, SortedMap.change_exists l (fun (_,lt) -> (false,lt)) r)  
          with Not_found ->  
            if o then Boolean.atom  
              (true, SortedMap.union_disj [l, (false,any_node)] r)  
1170             else Boolean.empty             else Boolean.empty
1171        )        )
1172        t        d.record
   
   let project_field t l =  
     let r = label_present t l in  
     List.fold_left (fun accu (d,_) -> cup accu d) empty r  
   
   let project t l =  
     let t = get t in  
     let r = label_present t l in  
     if r = [] then raise Not_found else  
       List.fold_left (fun accu (d,_) -> cup accu d) empty r  
   
   type normal =  
       [ `Success  
       | `Fail  
       | `NoField  
       | `SomeField  
       | `Label of label * (descr * normal) list * normal ]  
   
   let first_label t =  
     let min = ref None in  
     let lab l = match !min with  
       | Some l' when l >= l' -> ()  
       | _ -> min := Some l in  
     let aux = function  
       | _,[] -> ()  
       | _,(l,_)::_ -> lab l in  
     Boolean.iter aux t;  
     match !min with  
       | Some l -> `Label l  
       | None ->  
           let n =  
             Boolean.compute  
               ~empty:0  
               ~full:3  
               ~cup:(lor)  
               ~cap:(land)  
               ~diff:(fun a b -> a land lnot b)  
               ~atom:(function (true,[]) -> 3 | (false,[]) -> 1 | _ -> assert false)  
               t in  
           match n with  
             | 0 -> `Fail  
             | 1 -> `NoField  
             | 2 -> `SomeField  
             | _ -> `Success  
   
   
   let normal' t l =  
     let present = label_present t l  
     and absent = restrict_label_absent t l in  
     List.map (fun (d,t) -> d,t) present, absent  
   
   let rec normal_aux t =  
     match first_label t with  
       | `Label l ->  
           let present = label_present t l  
           and absent = restrict_label_absent t l in  
           `Label (l, List.map (fun (d,t) -> d, normal_aux t) present,  
                   normal_aux absent)  
       | `Fail -> `Fail  
       | `Success -> `Success  
       | `NoField -> `NoField  
       | `SomeField -> `SomeField  
   
   let normal t = normal_aux (get t)  
   
1173    
1174      let split (d : descr) l =
1175        TR.boolean (aux d l)
1176    
1177    let descr x = { empty with record = x }    let split_normal d l =
1178    let is_empty x = is_empty (descr x)      TR.boolean_normal (aux d l)
 (*  
   
   type t = (label, (bool * descr)) SortedMap.t list  
1179    
   let get d =  
     let line r = List.for_all (fun (l,(o,d)) -> o || non_empty d) r in  
     List.filter line (get_record d.record)  
   
   let restrict_label_present t l =  
     let restr = function  
       | (true, d) -> if non_empty d then (false,d) else raise Exit  
       | x -> x in  
     let aux accu r =  
       try SortedMap.change l restr (false,any) r :: accu  
       with Exit -> accu in  
     List.fold_left aux [] t  
   
   let restrict_label_absent t l =  
     let restr = function (true, _) -> (true,empty) | _ -> raise Exit in  
     let aux accu r =  
       try SortedMap.change l restr (true,empty) r :: accu  
       with Exit -> accu in  
     List.fold_left aux [] t  
   
   let restrict_field t l d =  
     let restr (_,d1) =  
       let d1 = cap d d1 in  
       if is_empty d1 then raise Exit else (false,d1) in  
     let aux accu r =  
       try SortedMap.change l restr (false,d) r :: accu  
       with Exit -> accu in  
     List.fold_left aux [] t  
   
   let project_field t l =  
     let aux accu x =  
       match List.assoc l x with  
         | (false,t) -> cup accu t  
         | _ -> raise Not_found  
     in  
     List.fold_left aux empty t  
1180    
1181    let project d l =    let project d l =
1182      project_field (get_record d.record) l      let t = TR.pi1 (split d l) in
1183        if t.absent then raise Not_found;
1184    type normal =      t
       [ `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  
             let t = List.fold_left (fun a (t,_) -> diff a t) any present in  
             let pr =  
               if non_empty t then (t, merge_record `Fail r) :: pr  
               else pr in  
             `Label (l1,pr,merge_record absent r)  
           else if (l2 < l1) then  
             let n' = merge_record n r' in  
             `Label (l2, [t2, n'], if o then n' else n)  
           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)  
   
   module Unify = Map.Make(struct type t = normal let compare = compare end)  
   
   let repository = ref Unify.empty  
   
   let rec canonize = function  
     | `Label (l,pr,ab) as x ->  
         (try Unify.find x !repository  
          with Not_found ->  
            let pr = List.map (fun (t,n) -> canonize n,t) pr in  
            let pr = SortedMap.from_list cup pr in  
            let pr = List.map (fun (n,t) -> (t,n)) pr in  
            let x = `Label (l, pr, canonize ab) in  
            try Unify.find x !repository  
            with Not_found -> repository := Unify.add x x !repository; x  
         )  
     | x -> x  
   
   let normal d =  
     let r = canonize (List.fold_left merge_record `Fail (get d)) in  
     repository := Unify.empty;  
     r  
   
   type normal' =  
       [ `Success  
       | `Label of label * (descr * descr) list * descr option ] option  
   
 (* NOTE: this function relies on the fact that generic order  
          makes smallest labels appear first *)  
1185    
1186    let first_label d =    let first_label d =
1187      let d = d.record in      let min = ref LabelPool.dummy_max in
1188      let min = ref None in      let aux =
1189      let lab (l,o,t) = match !min with        function _,(l,_)::_ -> if (l:int) < !min then min := l | _ -> () in
1190        | Some l' when l >= l' -> ()      Boolean.iter aux d.record;
1191        | _ -> if o && (descr t = any) then () else min := Some l in      !min
1192      let line (p,n) =  
1193        (match p with f::_ -> lab f | _ -> ());    let empty_cases d =
1194        (match n with f::_ -> lab f | _ -> ()) in      let x = Boolean.compute
1195      List.iter line d;                ~empty:0 ~full:3 ~cup:(lor) ~cap:(land)
1196      match !min with                ~diff:(fun a b -> a land lnot b)
1197        | None -> if d = [] then `Empty else `Any                ~atom:(function (true,[]) -> 3 | (false,[]) -> 1
1198        | Some l -> `Label l                         | _ -> assert false) d.record in
1199        (x land 2 <> 0, x land 1 <> 0)
   let normal' (d : descr) l =  
     let ab = ref empty in  
     let rec extract f = function  
       | (l',o,t) :: rem when l = l' ->  
           f o (descr t); extract f rem  
       | x :: rem -> x :: (extract f rem)  
       | [] -> [] in  
     let line (p,n) =  
       let ao = ref true and ad = ref any in  
       let p =  
         extract (fun o d -> ao := !ao && o; ad := cap !ad d) p  
       and n =  
         extract (fun o d -> ao := !ao && not o; ad := diff !ad d) n  
       in  
       (* Note: p and n are still sorted *)  
       let d = { empty with record = [(p,n)] } in  
       if !ao then ab := cup d !ab;  
       (!ad, d) in  
     let pr = List.map line d.record in  
     let pr = Product.normal_aux pr in  
     let ab = if is_empty !ab then None else Some !ab in  
     (pr, ab)  
1200    
 *)  
1201    
1202    let any = { empty with record = any.record }    let any = { empty with record = any.record }
 (*  
   let is_empty d = d = []  
   let descr l =  
     let line l = map_sort (fun (l,(o,d)) -> (l,o,cons d)) l, [] in  
     { empty with record = map_sort line l }  
 *)  
1203  end  end
1204    
1205    
Legend:
Removed from v.228  
changed lines
  Added in v.229
CVS Admin">CVS Admin
 ViewVC Help
Powered by ViewVC 1.1.5