/[svn]/types/types.ml

Diff of /types/types.ml

Parent Directory | Revision Log | View Patch Patch

-revision 71 by abate,
Tue Jul 10 17:03:32 2007 UTC
+revision 698 by abate,
Tue Jul 10 17:56:40 2007 UTC
 Line 1
- open Recursive
+ open Ident
- open Printf
+ open Encodings
+ (* TODO:
+    - I store hash in types to avoid computing it several times.
+      Does not seem to help a lot.
+ *)
+ (*
+ To be sure not to use generic comparison ...
+ *)
+ let (=) : int -> int -> bool = (==)
+ let (<) : int -> int -> bool = (<)
+ let (<=) : int -> int -> bool = (<=)
+ let (<>) : int -> int -> bool = (<>)
+ let compare = 1
+ type const =
+   | Integer of Intervals.V.t
+   | Atom of Atoms.V.t
+   | Char of Chars.V.t
+   | Pair of const * const
+   | Xml of const * const
+   | Record of const label_map
+   | String of U.uindex * U.uindex * U.t * const
+ module Const = struct
+   type t = const
+   let rec check = function
+     | Integer i -> Intervals.V.check i
+     | Atom i -> Atoms.V.check i
+     | Char i -> Chars.V.check i
+     | Pair (x,y) | Xml (x,y) -> check x; check y
+     | Record l -> LabelMap.iter check l
+     | String (i,j,s,q) -> U.check s; check q
+   let dump ppf _ =
+     Format.fprintf ppf "<Types.Const.t>"
+   let rec serialize s = function
+     | Integer x ->
+         Serialize.Put.bits 3 s 0;
+         Intervals.V.serialize s x
+     | Atom x ->
+         Serialize.Put.bits 3 s 1;
+         Atoms.V.serialize s x
+     | Char x ->
+         Serialize.Put.bits 3 s 2;
+         Chars.V.serialize s x
+     | Pair (x,y) ->
+         Serialize.Put.bits 3 s 3;
+         serialize s x;
+         serialize s y
+     | Xml (x,y) ->
+         Serialize.Put.bits 3 s 4;
+         serialize s x;
+         serialize s y
+     | Record r ->
+         Serialize.Put.bits 3 s 5;
+         LabelMap.serialize serialize s r
+     | String (i,j,st,q) ->
+         Serialize.Put.bits 3 s 6;
+         U.serialize_sub s st i j;
+         serialize s q
+   let rec deserialize s =
+     match Serialize.Get.bits 3 s with
+       | 0 ->
+           Integer (Intervals.V.deserialize s)
+       | 1 ->
+           Atom (Atoms.V.deserialize s)
+       | 2 ->
+           Char (Chars.V.deserialize s)
+       | 3 ->
+           let x = deserialize s in
+           let y = deserialize s in
+           Pair (x,y)
+       | 4 ->
+           let x = deserialize s in
+           let y = deserialize s in
+           Xml (x,y)
+       | 5 ->
+           Record (LabelMap.deserialize deserialize s)
+       | 6 ->
+           let st = U.deserialize s in
+           let q = deserialize s in
+           String (U.start_index st, U.end_index st, st, q)
+       | _ ->
+           assert false
+   let rec compare c1 c2 = match (c1,c2) with
+     | Integer x, Integer y -> Intervals.V.compare x y
+     | Integer _, _ -> -1
+     | _, Integer _ -> 1
+     | Atom x, Atom y -> Atoms.V.compare x y
+     | Atom _, _ -> -1
+     | _, Atom _ -> 1
+     | Char x, Char y -> Chars.V.compare x y
+     | Char _, _ -> -1
+     | _, Char _ -> 1
+     | Pair (x1,x2), Pair (y1,y2) ->
+         let c = compare x1 y1 in
+         if c <> 0 then c else compare x2 y2
+     | Pair (_,_), _ -> -1
+     | _, Pair (_,_) -> 1
+     | Xml (x1,x2), Xml (y1,y2) ->
+         let c = compare x1 y1 in
+         if c <> 0 then c else compare x2 y2
+     | Xml (_,_), _ -> -1
+     | _, Xml (_,_) -> 1
+     | Record x, Record y ->
+         LabelMap.compare compare x y
+     | Record _, _ -> -1
+     | _, Record _ -> 1
+     | String (i1,j1,s1,r1), String (i2,j2,s2,r2) ->
+         let c = Pervasives.compare i1 i2 in if c <> 0 then c
+         else let c = Pervasives.compare j1 j2 in if c <> 0 then c
+         else let c = U.compare s1 s2 in if c <> 0 then c (* Should compare
+                                                             only the substring *)
+         else compare r1 r2
+   let rec hash = function
+     | Integer x -> 1 + 17 * (Intervals.V.hash x)
+     | Atom x -> 2 + 17 * (Atoms.V.hash x)
+     | Char x -> 3 + 17 * (Chars.V.hash x)
+     | Pair (x,y) -> 4 + 17 * (hash x) + 257 * (hash y)
+     | Xml (x,y) -> 5 + 17 * (hash x) + 257 * (hash y)
+     | Record x -> 6 + 17 * (LabelMap.hash hash x)
+     | String (i,j,s,r) -> 7 + 17 * (U.hash s) + 257 * hash r
+       (* Note: improve hash for String *)
- type label = int
+   let equal c1 c2 = compare c1 c2 = 0
- type atom  = int
+ end
- let counter_label = ref 0
- let label_table = Hashtbl.create 63
- let label_names = Hashtbl.create 63
- let label s =
-   try Hashtbl.find label_table s
-   with Not_found ->
-     incr counter_label;
-     Hashtbl.add label_table s !counter_label;
-     Hashtbl.add label_names !counter_label s;
-     !counter_label
- let label_name l =
+ type pair_kind = [ `Normal | `XML ]
-   Hashtbl.find label_names l
- let mk_atom = label
+ let count = State.ref "Types.count" 0
- let atom_name = label_name
+ let () =
+   Stats.register Stats.Summary
+     (fun ppf -> Format.fprintf ppf "Allocated type nodes:%i@\n" !count)
- type const = Integer of Big_int.big_int | Atom of atom | Char of Chars.Unichar.t
- module I = struct
+ module rec Descr :
-   type 'a t = {
+ sig
+ (*
+   Want to write:
+     type s = { ... }
+     include Custom.T with type t = s
+   but a  bug in OCaml 3.07+beta 2 makes it impossible
+ *)
+   type t = {
+     mutable hash: int;
+     atoms : Atoms.t;
      ints  : Intervals.t;
-     atoms : atom Atoms.t;
-     times : ('a * 'a) Boolean.t;
-     arrow : ('a * 'a) Boolean.t;
-     record: (label * bool * 'a) Boolean.t;
      chars : Chars.t;
+     times : BoolPair.t;
+     xml   : BoolPair.t;
+     arrow : BoolPair.t;
+     record: BoolRec.t;
+     absent: bool
+   }
+   val empty: t
+   val dump: Format.formatter -> t -> unit
+   val check: t -> unit
+   val equal: t -> t -> bool
+   val hash: t -> int
+   val compare:t -> t -> int
+   val serialize: t Serialize.Put.f
+   val deserialize: t Serialize.Get.f
+ end =
+ struct
+   type t = {
+     mutable hash: int;
+     atoms : Atoms.t;
+     ints  : Intervals.t;
+     chars : Chars.t;
+     times : BoolPair.t;
+     xml   : BoolPair.t;
+     arrow : BoolPair.t;
+     record: BoolRec.t;
+     absent: bool
    }
+   let dump ppf _ =
+     Format.fprintf ppf "<Types.Descr.t>"
    let empty = {
-     times = Boolean.empty;
+     hash = 0;
-     arrow = Boolean.empty;
+     times = BoolPair.empty;
-     record= Boolean.empty;
+     xml   = BoolPair.empty;
+     arrow = BoolPair.empty;
+     record= BoolRec.empty;
      ints  = Intervals.empty;
      atoms = Atoms.empty;
      chars = Chars.empty;
+     absent= false;
    }
+   let equal a b =
+     (a == b) || (
+       (Atoms.equal a.atoms b.atoms) &&
+       (Chars.equal a.chars b.chars) &&
+       (Intervals.equal a.ints  b.ints) &&
+       (BoolPair.equal a.times b.times) &&
+       (BoolPair.equal a.xml b.xml) &&
+       (BoolPair.equal a.arrow b.arrow) &&
+       (BoolRec.equal a.record b.record) &&
+       (a.absent == b.absent)
+     )
+   let compare a b =
+     if a == b then 0
+     else let c = Atoms.compare a.atoms b.atoms in if c <> 0 then c
+     else let c = Chars.compare a.chars b.chars in if c <> 0 then c
+     else let c = Intervals.compare a.ints b.ints in if c <> 0 then c
+     else let c = BoolPair.compare a.times b.times in if c <> 0 then c
+     else let c = BoolPair.compare a.xml b.xml in if c <> 0 then c
+     else let c = BoolPair.compare a.arrow b.arrow in if c <> 0 then c
+     else let c = BoolRec.compare a.record b.record in if c <> 0 then c
+     else if a.absent && not b.absent then -1
+     else if b.absent && not a.absent then 1
+     else 0
+   let hash a =
+     if a.hash <> 0 then a.hash else (
+       let accu = Chars.hash a.chars in
+       let accu = 17 * accu + Intervals.hash a.ints in
+       let accu = 17 * accu + Atoms.hash a.atoms in
+       let accu = 17 * accu + BoolPair.hash a.times in
+       let accu = 17 * accu + BoolPair.hash a.xml in
+       let accu = 17 * accu + BoolPair.hash a.arrow in
+       let accu = 17 * accu + BoolRec.hash a.record in
+       let accu = if a.absent then accu+5 else accu in
+       a.hash <- accu;
+       accu
+     )
+   let check a =
+     Chars.check a.chars;
+     Intervals.check a.ints;
+     Atoms.check a.atoms;
+     BoolPair.check a.times;
+     BoolPair.check a.xml;
+     BoolPair.check a.arrow;
+     BoolRec.check a.record;
+     ()
+   let serialize t a =
+     Chars.serialize t a.chars;
+     Intervals.serialize t a.ints;
+     Atoms.serialize t a.atoms;
+     BoolPair.serialize t a.times;
+     BoolPair.serialize t a.xml;
+     BoolPair.serialize t a.arrow;
+     BoolRec.serialize t a.record;
+     Serialize.Put.bool t a.absent
+   let deserialize t =
+     let chars = Chars.deserialize t in
+     let ints = Intervals.deserialize t in
+     let atoms = Atoms.deserialize t in
+     let times = BoolPair.deserialize t in
+     let xml = BoolPair.deserialize t in
+     let arrow = BoolPair.deserialize t in
+     let record = BoolRec.deserialize t in
+     let absent = Serialize.Get.bool t in
+     let d = { hash=0;
+       chars = chars; ints = ints; atoms = atoms; times = times; xml = xml;
+       arrow = arrow; record = record; absent = absent } in
+     check d;
+     d
+ end
+ and Node :
+ sig
+   type t = { id : int; mutable descr : Descr.t }
+   val dump: Format.formatter -> t -> unit
+   val check: t -> unit
+   val equal: t -> t -> bool
+   val hash: t -> int
+   val compare:t -> t -> int
+   val serialize: t Serialize.Put.f
+   val deserialize: t Serialize.Get.f
+ end =
+ struct
+   type t = { id : int; mutable descr : Descr.t }
+   let check n = ()
+   let dump ppf n = failwith "Types.Node.dump"
+   let hash x = x.id
+   let compare x y = x.id - y.id  (* ids are small enough ! *)
+   let equal x y = x == y
+   module SMemo = Set.Make(Custom.Int)
+   let memo = Serialize.Put.mk_property (fun t -> ref SMemo.empty)
+   let serialize t n =
+     Serialize.Put.int t n.id;
+     let l = Serialize.Put.get_property memo t in
+     if not (SMemo.mem n.id !l) then (
+       l := SMemo.add n.id !l;
+       Descr.serialize t n.descr
+     )
+   module DMemo = Map.Make(Custom.Int)
+   let memo = Serialize.Get.mk_property (fun t -> ref DMemo.empty)
+   let deserialize t =
+     let l = Serialize.Get.get_property memo t in
+     let id = Serialize.Get.int t in
+     try DMemo.find id !l
+     with Not_found ->
+       (* TODO: hash-consing ? *)
+       incr count;
+       let n = { id = !count; descr = Descr.empty } in
+       l := DMemo.add id n !l;
+       n.descr <- Descr.deserialize t;
+       n
+ end
+ (* It is also possible to use Boolean instead of Bool here;
+    need to analyze when each one is more efficient *)
+ and BoolPair : Bool.S with type elem = Node.t * Node.t =
+ Bool.Make(Custom.Pair(Node)(Node))
+ and BoolRec : Bool.S with type elem = bool * Node.t label_map =
+ Bool.Make(Custom.Pair(Custom.Bool)(LabelSet.MakeMap(Node)))
+ module DescrHash = Hashtbl.Make(Descr)
+ module DescrMap = Map.Make(Descr)
+ module DescrSet = Set.Make(Descr)
+ module DescrSList = SortedList.Make(Descr)
+ type descr = Descr.t
+ type node = Node.t
+ include Descr
+ let hash_cons = DescrHash.create 17000
+ let make () = incr count; { Node.id = !count; Node.descr = empty }
+ let define n d =
+   DescrHash.add hash_cons d n;
+   n.Node.descr <- d
+ let cons d =
+   try DescrHash.find hash_cons d
+   with Not_found ->
+     incr count;
+     let n = { Node.id = !count; Node.descr = d } in
+     DescrHash.add hash_cons d n; n
    let any =  {
-     times = Boolean.full;
+   hash = 0;
-     arrow = Boolean.full;
+   times = BoolPair.full;
-     record= Boolean.full;
+   xml   = BoolPair.full;
+   arrow = BoolPair.full;
+   record= BoolRec.full;
      ints  = Intervals.any;
      atoms = Atoms.any;
      chars = Chars.any;
+   absent= false;
    }
-   let interval i = { empty with ints = i }
+ let non_constructed =
-   let times x y = { empty with times = Boolean.atom (x,y) }
+   { any with
-   let arrow x y = { empty with arrow = Boolean.atom (x,y) }
+       hash = 0;
-   let record label opt t = { empty with record = Boolean.atom (label,opt,t) }
+       times = empty.times; xml = empty.xml; record = empty.record }
-   let atom a = { empty with atoms = a }
-   let char c = { empty with chars = c }
-   let constant = function
+ let interval i = { empty with hash = 0; ints = i }
-     | Integer i -> interval (Intervals.atom i)
+ let times x y = { empty with hash = 0; times = BoolPair.atom (x,y) }
-     | Atom a -> atom (Atoms.atom a)
+ let xml x y = { empty with hash = 0; xml = BoolPair.atom (x,y) }
-     | Char c -> char (Chars.atom c)
+ let arrow x y = { empty with hash = 0; arrow = BoolPair.atom (x,y) }
+ let record label t =
+   { empty with hash = 0;
-   let any_record = { empty with record = any.record }
+       record = BoolRec.atom (true,LabelMap.singleton label t) }
+ let record' (x : bool * node Ident.label_map) =
+   { empty with hash = 0; record = BoolRec.atom x }
+ let atom a = { empty with hash = 0; atoms = a }
+ let char c = { empty with hash = 0; chars = c }
    let cup x y =
-     if x = y then x else {
+   if x == y then x else {
-       times = Boolean.cup x.times y.times;
+     hash = 0;
-       arrow = Boolean.cup x.arrow y.arrow;
+     times = BoolPair.cup x.times y.times;
-       record= Boolean.cup x.record y.record;
+     xml   = BoolPair.cup x.xml y.xml;
+     arrow = BoolPair.cup x.arrow y.arrow;
+     record= BoolRec.cup x.record y.record;
        ints  = Intervals.cup x.ints  y.ints;
        atoms = Atoms.cup x.atoms y.atoms;
        chars = Chars.cup x.chars y.chars;
+     absent= x.absent || y.absent;
      }
    let cap x y =
-     if x = y then x else {
+   if x == y then x else {
-       times = Boolean.cap x.times y.times;
+     hash = 0;
-       record= Boolean.cap x.record y.record;
+     times = BoolPair.cap x.times y.times;
-       arrow = Boolean.cap x.arrow y.arrow;
+     xml   = BoolPair.cap x.xml y.xml;
+     record= BoolRec.cap x.record y.record;
+     arrow = BoolPair.cap x.arrow y.arrow;
        ints  = Intervals.cap x.ints  y.ints;
        atoms = Atoms.cap x.atoms y.atoms;
        chars = Chars.cap x.chars y.chars;
+     absent= x.absent && y.absent;
      }
    let diff x y =
-     if x = y then empty else {
+   if x == y then empty else {
-       times = Boolean.diff x.times y.times;
+     hash = 0;
-       arrow = Boolean.diff x.arrow y.arrow;
+     times = BoolPair.diff x.times y.times;
-       record= Boolean.diff x.record y.record;
+     xml   = BoolPair.diff x.xml y.xml;
+     arrow = BoolPair.diff x.arrow y.arrow;
+     record= BoolRec.diff x.record y.record;
        ints  = Intervals.diff x.ints  y.ints;
        atoms = Atoms.diff x.atoms y.atoms;
        chars = Chars.diff x.chars y.chars;
+     absent= x.absent && not y.absent;
      }
-   let neg x = diff any x
-   let equal e a b =
-     if a.atoms <> b.atoms then raise NotEqual;
-     if a.chars <> b.chars then raise NotEqual;
-     if a.ints <> b.ints then raise NotEqual;
-     Boolean.equal (fun (x1,x2) (y1,y2) -> e x1 y1; e x2 y2) a.times b.times;
-     Boolean.equal (fun (x1,x2) (y1,y2) -> e x1 y1; e x2 y2) a.arrow b.arrow;
-     Boolean.equal (fun (l1,o1,x1) (l2,o2,x2) ->
-                      if (l1 <> l2) || (o1 <> o2) then raise NotEqual;
-                      e x1 x2) a.record b.record
-   let map f a =
-     { times = Boolean.map (fun (x1,x2) -> (f x1, f x2)) a.times;
-       arrow = Boolean.map (fun (x1,x2) -> (f x1, f x2)) a.arrow;
-       record= Boolean.map (fun (l,o,x) -> (l,o, f x)) a.record;
-       ints  = a.ints;
-       atoms = a.atoms;
-       chars = a.chars;
-     }
-   let hash h a =
-     Hashtbl.hash (map h a)
- (*
-     (Hashtbl.hash { (map h a) with ints = Intervals.empty })
-     + (Intervals.hash a.ints)
- *)
-   let iter f a =
-     ignore (map f a)
-   let deep = 4
- end
- module Algebra = Recursive_noshare.Make(I)
- include I
- include Algebra
- module DescrHash =
-   Hashtbl.Make(
-     struct
-       type t = descr
-       let hash = hash_descr
-       let equal = equal_descr
-     end
-   )
- module DescrMap = Map.Make(struct type t = descr let compare = compare end)
- let check d =
-   Boolean.check d.times;
-   Boolean.check d.arrow;
-   Boolean.check d.record;
-   ()
- (*
- let define n d = check d; define n d
- *)
- let cons d =
-   let n = make () in
-   define n d;
-   internalize 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
-   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 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 "Atom" print_atom d.atoms @
-          Boolean.print "Pair" print_times d.times @
-          Boolean.print "Arrow" print_arrow d.arrow @
-          Boolean.print "Record" 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)
- end
+ (* TODO: optimize disjoint check for boolean combinations *)
+ let trivially_disjoint a b =
+   (Chars.disjoint a.chars b.chars) &&
+   (Intervals.disjoint a.ints b.ints) &&
+   (Atoms.disjoint a.atoms b.atoms) &&
+   (BoolPair.trivially_disjoint a.times b.times) &&
+   (BoolPair.trivially_disjoint a.xml b.xml) &&
+   (BoolPair.trivially_disjoint a.arrow b.arrow) &&
+   (BoolRec.trivially_disjoint a.record b.record) &&
+   (not (a.absent && b.absent))
- module Positive =
+ let descr n = n.Node.descr
- struct
+ let internalize n = n
-   type rhs = [ `Type of descr | `Cup of v list | `Times of v * v ]
+ let id n = n.Node.id
-   and v = { mutable def : rhs; mutable node : node option }
-   let rec make_descr seen v =
+ let rec constant = function
-     if List.memq v seen then empty
+   | Integer i -> interval (Intervals.atom i)
+   | Atom a -> atom (Atoms.atom a)
+   | Char c -> char (Chars.atom c)
+   | Pair (x,y) -> times (const_node x) (const_node y)
+   | Xml (x,y) -> times (const_node x) (const_node y)
+   | Record x -> record' (false ,LabelMap.map const_node x)
+   | String (i,j,s,c) ->
+       if U.equal_index i j then constant c
      else
-       let seen = v :: seen in
+         let (ch,i') = U.next s i in
-       match v.def with
+         constant (Pair (Char (Chars.V.mk_int ch), String (i',j,s,c)))
-         | `Type d -> d
+ and const_node c = cons (constant c)
-         | `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 =
+ let neg x = diff any x
-     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 any_node = cons any
-   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)
+ module LabelS = Set.Make(LabelPool)
- end
+ let any_or_absent = { any with hash=0; absent = true }
+ let only_absent = { empty with hash=0; absent = true }
  let get_record r =
-   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
      List.fold_left
-       (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
-   List.map line r
+   let extend descrs labs (o,r) =
+     let rec aux i labs r =
+       match labs with
+         | [] -> ()
+         | l1::labs ->
+             match r with
+               | (l2,x)::r when l1 == l2 ->
+                   descrs.(i) <- cap descrs.(i) (descr x);
+                   aux (i+1) labs r
+               | r ->
+                   if not o then
+                     descrs.(i) <- cap descrs.(i) only_absent; (* TODO:OPT *)
+                   aux (i+1) labs r
+     in
+     aux 0 labs (LabelMap.get r);
+     o
+   in
+   let line (p,n) =
+     let labels =
+       List.fold_left labs (List.fold_left labs LabelS.empty p) n in
+     let labels = LabelS.elements labels in
+     let nlab = List.length labels in
+     let mk () = Array.create nlab any_or_absent in
+     let pos = mk () in
+     let opos = List.fold_left
+                  (fun accu x ->
+                     (extend pos labels x) && accu)
+                  true p in
+     let p = (opos, pos) in
+     let n = List.map (fun x ->
+                         let neg = mk () in
+                         let o = extend neg labels x in
+                         (o,neg)
+                      ) n in
+     (labels,p,n)
+   in
+   List.map line (BoolRec.get r)
-Line 326
+Line 518
  let diff_t d t = diff d (descr t)
  let cap_t d t = cap d (descr t)
- let cap_product l =
+ let cup_t d t = cup d (descr t)
+ let cap_product any_left any_right l =
    List.fold_left
      (fun (d1,d2) (t1,t2) -> (cap_t d1 t1, cap_t d2 t2))
-     (any,any)
+     (any_left,any_right)
      l
+ let any_pair = { empty with hash = 0; times = any.times }
- module Assumptions = Set.Make(struct type t = descr let compare = compare end)
+ let rec exists max f =
+   (max > 0) && (f (max - 1) || exists (max - 1) f)
- let memo = ref Assumptions.empty
- let cache_false = ref Assumptions.empty
  exception NotEmpty
- let rec empty_rec d =
+ type slot = { mutable status : status;
-   if Assumptions.mem d !cache_false then false
+                mutable notify : notify;
-   else if Assumptions.mem d !memo then true
+                mutable active : bool }
-   else if not (Intervals.is_empty d.ints) then false
+ and status = Empty | NEmpty | Maybe
-   else if not (Atoms.is_empty d.atoms) then false
+ and notify = Nothing | Do of slot * (slot -> unit) * notify
-   else if not (Chars.is_empty d.chars) then false
-   else (
+ let slot_empty = { status = Empty; active = false; notify = Nothing }
-     let backup = !memo in
+ let slot_not_empty = { status = NEmpty; active = false; notify = Nothing }
-     memo := Assumptions.add d backup;
-     if
+ let rec notify = function
-       (empty_rec_times d.times) &&
+   | Nothing -> ()
-       (empty_rec_arrow d.arrow) &&
+   | Do (n,f,rem) ->
-       (empty_rec_record d.record)
+       if n.status == Maybe then (try f n with NotEmpty -> ());
-     then true
+       notify rem
-     else (
-       memo := backup;
-       cache_false := Assumptions.add d !cache_false;
-       false
-     )
-   )
- and empty_rec_times c =
+ let rec iter_s s f = function
-   List.for_all empty_rec_times_aux c
+   | [] -> ()
+   | arg::rem -> f arg s; iter_s s f rem
- and empty_rec_times_aux (left,right) =
-   let rec aux accu1 accu2 = function
-     | (t1,t2)::right ->
-         let accu1' = diff_t accu1 t1 in
-         if not (empty_rec accu1') then aux accu1' accu2 right;
-         let accu2' = diff_t accu2 t2 in
-         if not (empty_rec accu2') then aux accu1 accu2' right
-     | [] -> raise NotEmpty
-   in
-   let (accu1,accu2) = cap_product left in
-   (empty_rec accu1) || (empty_rec accu2) ||
-   (try aux accu1 accu2 right; true with NotEmpty -> false)
- and empty_rec_arrow c =
+ let set s =
-   List.for_all empty_rec_arrow_aux c
+   s.status <- NEmpty;
+   notify s.notify;
+   s.notify <- Nothing;
+   raise NotEmpty
+ let rec big_conj f l n =
+   match l with
+     | [] -> set n
+     | [arg] -> f arg n
+     | arg::rem ->
+         let s =
+           { status = Maybe; active = false;
+             notify = Do (n,(big_conj f rem), Nothing) } in
+         try
+           f arg s;
+           if s.active then n.active <- true
+         with NotEmpty -> if n.status == NEmpty then raise NotEmpty
+ let guard a f n =
+   match a with
+     | { status = Empty } -> ()
+     | { status = Maybe } as s ->
+         n.active <- true;
+         s.notify <- Do (n,f,s.notify)
+     | { status = NEmpty } -> f n
- and empty_rec_arrow_aux (left,right) =
-   let single_right (s1,s2) =
-     let rec aux accu1 accu2 = function
-       | (t1,t2)::left ->
-           let accu1' = diff_t accu1 t1 in
-           if not (empty_rec accu1') then aux accu1 accu2 left;
-           let accu2' = cap_t accu2 t2 in
-           if not (empty_rec accu2') then aux accu1 accu2 left
-       | [] -> raise NotEmpty
-     in
-     let accu1 = descr s1 in
-     (empty_rec accu1) ||
-     (try aux accu1 (diff any (descr s2)) left; true with NotEmpty -> false)
-   in
-   List.exists single_right right
- and empty_rec_record c =
+ (* Fast approximation *)
-   let aux = List.exists (fun (_,(opt,t)) -> (not opt) && (empty_rec t)) in
-   List.for_all aux (get_record c)
- let is_empty d =
+ module ClearlyEmpty =
-   let old = !memo in
+ struct
-   let r = empty_rec d in
-   if not r then memo := old;
- (*  cache_false := Assumptions.empty;  *)
-   r
- let non_empty d =
+ let memo = DescrHash.create 33000
-   not (is_empty d)
+ let marks = ref []
- let subtype d1 d2 =
+ let rec slot d =
-   is_empty (diff d1 d2)
+   if not ((Intervals.is_empty d.ints) &&
+           (Atoms.is_empty d.atoms) &&
+           (Chars.is_empty d.chars) &&
+           (not d.absent)) then slot_not_empty
+   else try DescrHash.find memo d
+   with Not_found ->
+     let s = { status = Maybe; active = false; notify = Nothing } in
+     DescrHash.add memo d s;
+     (try
+        iter_s s check_times (BoolPair.get d.times);
+        iter_s s check_xml (BoolPair.get d.xml);
+        iter_s s check_arrow (BoolPair.get d.arrow);
+        iter_s s check_record (get_record d.record);
+        if s.active then marks := s :: !marks else s.status <- Empty;
+      with
+          NotEmpty -> ());
+     s
- (* Sample value *)
+ and check_times (left,right) s =
- module Sample =
+   let (accu1,accu2) = cap_product any any left in
- struct
+   let single_right (t1,t2) s =
+     let t1 = descr t1 and t2 = descr t2 in
+     if trivially_disjoint accu1 t1 || trivially_disjoint accu2 t2 then set s
+     else
+       let accu1 = diff accu1 t1 in guard (slot accu1) set s;
+       let accu2 = diff accu2 t2 in guard (slot accu2) set s in
+   guard (slot accu1) (guard (slot accu2) (big_conj single_right right)) s
+ and check_xml (left,right) s =
+   let (accu1,accu2) = cap_product any any_pair left in
+   let single_right (t1,t2) s =
+     let t1 = descr t1 and t2 = descr t2 in
+     if trivially_disjoint accu1 t1 || trivially_disjoint accu2 t2 then set s
+     else
+       let accu1 = diff accu1 t1 in guard (slot accu1) set s;
+       let accu2 = diff accu2 t2 in guard (slot accu2) set s in
+   guard (slot accu1) (guard (slot accu2) (big_conj single_right right)) s
+ and check_arrow (left,right) s =
+   let single_right (s1,s2) s =
+     let accu1 = descr s1 and accu2 = neg (descr s2) in
+     let single_left (t1,t2) s =
+       let accu1 = diff_t accu1 t1 in guard (slot accu1) set s;
+       let accu2 = cap_t  accu2 t2 in guard (slot accu2) set s
+     in
+     guard (slot accu1) (big_conj single_left left) s
+   in
+   big_conj single_right right s
- let rec find f = function
+ and check_record (labels,(oleft,left),rights) s =
-   | [] -> raise Not_found
+   let rec single_right (oright,right) s =
-   | x::r -> try f x with Not_found -> find f r
+     let next =
+       (oleft && (not oright)) ||
+       exists (Array.length left)
+         (fun i -> trivially_disjoint left.(i) right.(i))
+     in
+     if next then set s
+     else
+       for i = 0 to Array.length left - 1 do
+         let di = diff left.(i) right.(i) in guard (slot di) set s
+       done
+   in
+   let rec start i s =
+     if (i < 0) then big_conj single_right rights s
+     else guard (slot left.(i)) (start (i - 1)) s
+   in
+   start (Array.length left - 1) s
- 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
- let rec gen_atom i l =
+ let is_empty d =
-   if SortedList.mem l i then gen_atom (succ i) l  else i
+   let s = slot d in
+   List.iter
+     (fun s' ->
+        if s'.status == Maybe then s'.status <- Empty; s'.notify <- Nothing)
+     !marks;
+   marks := [];
+   s.status == Empty
+ end
- let rec sample_rec memo d =
+ let clearly_disjoint t1 t2 =
-   if (Assumptions.mem d memo) || (is_empty d) then raise Not_found
+ (*
+   if trivially_disjoint t1 t2 then true
    else
-     try Int (Intervals.sample d.ints) with Not_found ->
+     if ClearlyEmpty.is_empty (cap t1 t2) then
-     try Atom (Atoms.sample (gen_atom 0) d.atoms) with Not_found ->
+       (Printf.eprintf "!\n"; true) else false
-     try Char (Chars.sample d.chars) with Not_found ->
+ *)
-     try sample_rec_arrow d.arrow with Not_found ->
+   trivially_disjoint t1 t2 || ClearlyEmpty.is_empty (cap t1 t2)
-     let memo = Assumptions.add d memo in
+ (* TODO: need to invesigate when ClearEmpty is a good thing... *)
-     try sample_rec_times memo d.times with Not_found ->
-     try sample_rec_record memo d.record with Not_found ->
-     raise Not_found
+ let memo = DescrHash.create 33000
+ let marks = ref []
- and sample_rec_times memo c =
+ let rec slot d =
-   find (sample_rec_times_aux memo) c
+   if not ((Intervals.is_empty d.ints) &&
+           (Atoms.is_empty d.atoms) &&
+           (Chars.is_empty d.chars) &&
+           (not d.absent)) then slot_not_empty
+   else try DescrHash.find memo d
+   with Not_found ->
+     let s = { status = Maybe; active = false; notify = Nothing } in
+     DescrHash.add memo d s;
+     (try
+        iter_s s check_times (BoolPair.get d.times);
+        iter_s s check_xml (BoolPair.get d.xml);
+        iter_s s check_arrow (BoolPair.get d.arrow);
+        iter_s s check_record (get_record d.record);
+        if s.active then marks := s :: !marks else s.status <- Empty;
+      with
+          NotEmpty -> ());
+     s
- and sample_rec_times_aux memo (left,right) =
+ and check_times (left,right) s =
-   let rec aux accu1 accu2 = function
+   let rec aux accu1 accu2 right s = match right with
      | (t1,t2)::right ->
-         let accu1' = diff_t accu1 t1 in
+         let t1 = descr t1 and t2 = descr t2 in
-         if non_empty accu1' then aux accu1' accu2 right else
+         if trivially_disjoint accu1 t1 ||
-           let accu2' = diff_t accu2 t2 in
+            trivially_disjoint accu2 t2 then (
-           if non_empty accu2' then aux accu1 accu2' right else
+              aux accu1 accu2 right s )
-             raise Not_found
+         else (
-     | [] -> Pair (sample_rec memo accu1, sample_rec memo accu2)
+           let accu1' = diff accu1 t1 in
-   in
+           guard (slot accu1') (aux accu1' accu2 right) s;
-   let (accu1,accu2) = cap_product left in
-   if (is_empty accu1) || (is_empty accu2) then raise Not_found;
-   aux accu1 accu2 right
- and sample_rec_arrow c =
+           let accu2' = diff accu2 t2 in
-   find sample_rec_arrow_aux c
+           guard (slot accu2') (aux accu1 accu2' right) s
+         )
+     | [] -> set s
+   in
+   let (accu1,accu2) = cap_product any any left in
+   guard (slot accu1) (guard (slot accu2) (aux accu1 accu2 right)) s
- and check_empty_simple_arrow_line left (s1,s2) =
+ and check_xml (left,right) s =
-   let rec aux accu1 accu2 = function
+   let rec aux accu1 accu2 right s = match right with
+     | (t1,t2)::right ->
+         let t1 = descr t1 and t2 = descr t2 in
+         if clearly_disjoint accu1 t1 ||
+            trivially_disjoint accu2 t2 then (
+              aux accu1 accu2 right s )
+         else (
+           let accu1' = diff accu1 t1 in
+           guard (slot accu1') (aux accu1' accu2 right) s;
+           let accu2' = diff accu2 t2 in
+           guard (slot accu2') (aux accu1 accu2' right) s
+         )
+     | [] -> set s
+   in
+   let (accu1,accu2) = cap_product any any_pair left in
+   guard (slot accu1) (guard (slot accu2) (aux accu1 accu2 right)) s
+ and check_arrow (left,right) s =
+   let single_right (s1,s2) s =
+     let rec aux accu1 accu2 left s = match left with
      | (t1,t2)::left ->
          let accu1' = diff_t accu1 t1 in
-         if non_empty accu1' then aux accu1 accu2 left;
+           guard (slot accu1') (aux accu1' accu2 left) s;
          let accu2' = cap_t accu2 t2 in
-         if non_empty accu2' then aux accu1 accu2 left
+           guard (slot accu2') (aux accu1 accu2' left) s
-     | [] -> raise NotEmpty
+       | [] -> set s
    in
    let accu1 = descr s1 in
-   (is_empty accu1) ||
+     guard (slot accu1) (aux accu1 (neg (descr s2)) left) s
-   (try aux accu1 (diff any (descr s2)) left; true with NotEmpty -> false)
+   in
+   big_conj single_right right s
- 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 =
+ and check_record (labels,(oleft,left),rights) s =
-   Record (find (sample_rec_record_aux memo) (get_record c))
+   let rec aux rights s = match rights with
+     | [] -> set s
+     | (oright,right)::rights ->
+         let next =
+           (oleft && (not oright)) ||
+           exists (Array.length left)
+             (fun i -> trivially_disjoint left.(i) right.(i))
+         in
+         if next then aux rights s
+         else
+           for i = 0 to Array.length left - 1 do
+             let back = left.(i) in
+             let di = diff back right.(i) in
+             guard (slot di) (fun s ->
+                         left.(i) <- di;
+                         aux rights s;
+                         left.(i) <- back;
+                      ) s
+ (* TODO: are side effects correct ? *)
+           done
+   in
+   let rec start i s =
+     if (i < 0) then aux rights s
+     else
+       guard (slot left.(i)) (start (i - 1)) s
+   in
+   start (Array.length left - 1) s
- 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
+ let timer_subtype = Stats.Timer.create "Types.is_empty"
-   let rec print_sep f sep ppf = function
+ let is_empty d =
-     | [] -> ()
+   Stats.Timer.start timer_subtype;
-     | [x] -> f ppf x
+   let s = slot d in
-     | x::rem -> f ppf x; Format.fprintf ppf "%s" sep; print_sep f sep ppf rem
+   List.iter
+     (fun s' ->
+        if s'.status == Maybe then s'.status <- Empty; s'.notify <- Nothing)
+     !marks;
+   marks := [];
+   Stats.Timer.stop timer_subtype
+     (s.status == Empty)
+ (*
+ let is_empty d =
+ (*  let b1 = ClearlyEmpty.is_empty d in
+   let b2 = is_empty d in
+   assert (b2 || not b1);
+   Printf.eprintf "b1 = %b; b2 = %b\n" b1 b2;
+   b2  *)
+   if ClearlyEmpty.is_empty d then (Printf.eprintf "!\n"; true) else is_empty d
+ *)
-   let rec print ppf = function
+ let non_empty d =
-     | Int i -> Format.fprintf ppf "%s" (Big_int.string_of_big_int i)
+   not (is_empty d)
-     | Atom a -> Format.fprintf ppf "`%s" (atom_name a)
-     | Char c -> Chars.Unichar.print ppf c
-     | Pair (x1,x2) -> Format.fprintf ppf "(%a,%a)" print x1 print x2
-     | Record r ->
-         Format.fprintf ppf "{ %a }"
-           (print_sep
-              (fun ppf (l,x) ->
-                 Format.fprintf ppf "%s = %a"
-                 (label_name l)
-                 print x
-              )
-              " ; "
-           ) r
-     | Fun iface ->
-         Format.fprintf ppf "(fun ( %a ) x -> ...)"
-           (print_sep
-              (fun ppf (t1,t2) ->
-                 Format.fprintf ppf "%a -> %a; "
-                 Print.print t1 Print.print t2
-              )
-              " ; "
-           ) iface
- end
+ let subtype d1 d2 =
+   is_empty (diff d1 d2)
  module Product =
  struct
    type t = (descr * descr) list
-   let other d = { d with times = empty.times }
+   let other ?(kind=`Normal) d =
-   let is_product d = is_empty (other d)
+     match kind with
+       | `Normal -> { d with hash = 0; times = empty.times }
+       | `XML -> { d with hash = 0; xml = empty.xml }
+   let is_product ?kind d = is_empty (other ?kind d)
    let need_second = function _::_::_ -> true | _ -> false
-   let normal_aux d =
+   let normal_aux = function
+     | ([] | [ _ ]) as d -> d
+     | d ->
      let res = ref [] in
      let add (t1,t2) =
-Line 546
+Line 838
          | [] -> res := (ref (t1,t2)) :: !res
          | ({contents = (d1,d2)} as r)::l ->
              (*OPT*)
-             if d1 = t1 then r := (d1,cup d2 t2) else
+ (*          if equal_descr d1 t1 then r := (d1,cup d2 t2) else*)
                let i = cap t1 d1 in
                if is_empty i then loop t1 t2 l
-Line 564
+Line 856
      List.iter add d;
      List.map (!) !res
- (*
- This version explodes when dealing with
-    Any - [ t1? t2? t3? ... tn? ]
- ==> need partitioning
- *)
-   let get_aux d =
-     let line accu (left,right) =
-       let debug = List.length right = 28 in
-       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
- (* Partitioning *)
+ (* Partitioning:
-   let get_aux d =
+ (t,s) - ((t1,s1) | (t2,s2) | ... | (tn,sn))
+ =
+ (t & t1, s - s1) | ... | (t & tn, s - sn) | (t - (t1|...|tn), s)
+ *)
+   let get_aux any_right d =
      let accu = ref [] in
      let line (left,right) =
-       let (d1,d2) = cap_product left in
+       let (d1,d2) = cap_product any any_right left in
        if (non_empty d1) && (non_empty d2) then
          let right = List.map (fun (t1,t2) -> descr t1, descr t2) right in
          let right = normal_aux right in
-Line 609
+Line 883
              ) right in
          if non_empty !resid1 then accu := (!resid1, d2) :: !accu
      in
-     List.iter line d;
+     List.iter line (BoolPair.get d);
      !accu
+ (* Maybe, can improve this function with:
+      (t,s) \ (t1,s1) = (t&t',s\s') | (t\t',s),
+    don't call normal_aux *)
-   let get d = get_aux d.times
+   let get ?(kind=`Normal) d =
+     match kind with
+       | `Normal -> get_aux any d.times
+       | `XML -> get_aux any_pair d.xml
    let pi1 = List.fold_left (fun acc (t1,_) -> cup acc t1) empty
    let pi2 = List.fold_left (fun acc (_,t2) -> cup acc t2) empty
+   let pi2_restricted restr =
+     List.fold_left (fun acc (t1,t2) ->
+                       if is_empty (cap t1 restr) then acc
+                       else cup acc t2) empty
    let restrict_1 rects pi1 =
-     let aux accu (t1,t2) =
+     let aux acc (t1,t2) =
-       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
      List.fold_left aux [] rects
    type normal = t
-   module Memo = Map.Make(struct
+   module Memo = Map.Make(BoolPair)
-                            type t = (node * node) Boolean.t
-                            let compare = compare end)
+   (* TODO: try with an hashtable *)
+   (* Also, avoid lookup for simple products (t1,t2) *)
    let memo = ref Memo.empty
-   let normal d =
+   let normal_times d =
-     let d = d.times in
      try Memo.find d !memo
      with
          Not_found ->
-           let gd = get_aux d in
+           let gd = get_aux any d in
            let n = normal_aux gd in
+ (* Could optimize this call to normal_aux because one already
+    know that each line is normalized ... *)
            memo := Memo.add d n !memo;
            n
-   let any = { empty with times = any.times }
+   let memo_xml = ref Memo.empty
-   let is_empty d = d = []
+   let normal_xml d =
- end
+     try Memo.find d !memo_xml
+     with
+         Not_found ->
+           let gd = get_aux any_pair d in
+           let n = normal_aux gd in
+           memo_xml := Memo.add d n !memo_xml;
+           n
+   let normal ?(kind=`Normal) d =
+     match kind with
+       | `Normal -> normal_times d.times
+       | `XML -> normal_xml d.xml
+   let merge_same_2 r =
+     let r =
+       List.fold_left
+         (fun accu (t1,t2) ->
+            let t = try DescrMap.find t2 accu with Not_found -> empty in
+            DescrMap.add t2 (cup t t1) accu
+         ) DescrMap.empty r in
+     DescrMap.fold (fun t2 t1 accu -> (t1,t2)::accu) r []
+   let constraint_on_2 n t1 =
+     List.fold_left
+       (fun accu (d1,d2) ->
+          if is_empty (cap d1 t1) then accu else cap accu d2)
+       any
+       n
+   let any = { empty with hash = 0; times = any.times }
+   and any_xml = { empty with hash = 0; xml = any.xml }
+   let is_empty d = d == []
+ end
  module Record =
  struct
-   type t = (label, (bool * descr)) SortedMap.t list
+   let has_record d = not (is_empty { empty with hash= 0; record = d.record })
+   let or_absent d = { d with hash = 0; absent = true }
+   let any_or_absent = or_absent any
+   let has_absent d = d.absent
-   let get d =
+   let only_absent = {empty with hash = 0; absent = true}
-     let line r = List.for_all (fun (l,(o,d)) -> o || non_empty d) r in
+   let only_absent_node = cons only_absent
-     List.filter line (get_record d.record)
+   module T = struct
+     type t = descr
+     let any = any_or_absent
+     let cap = cap
+     let cup = cup
+     let diff = diff
+     let is_empty = is_empty
+     let empty = empty
+   end
+   module R = struct
+     type t = descr
+     let any = { empty with hash = 0; record = any.record }
+     let cap = cap
+     let cup = cup
+     let diff = diff
+     let is_empty = is_empty
+     let empty = empty
+   end
+   module TR = Normal.Make(T)(R)
+   let any_record = { empty with hash = 0; record = BoolRec.full }
+   let atom o l =
+     if o && LabelMap.is_empty l then any_record else
+     { empty with hash = 0; record = BoolRec.atom (o,l) }
-   let restrict_label_present t l =
+   type zor = Pair of descr * descr | Any
-     let restr = function
-       | (true, d) -> if non_empty d then (false,d) else raise Exit
+   let aux_split d l=
-       | x -> x in
+     let f (o,r) =
-     let aux accu r =
+       try
-       try SortedMap.change l restr (false,any) r :: accu
+         let (lt,rem) = LabelMap.assoc_remove l r in
-       with Exit -> accu in
+         Pair (descr lt, atom o rem)
-     List.fold_left aux [] t
+       with Not_found ->
+         if o then
-   let restrict_label_absent t l =
+           if LabelMap.is_empty r then Any else
-     let restr = function (true, _) -> (true,empty) | _ -> raise Exit in
+             Pair (any_or_absent, { empty with hash=0; record = BoolRec.atom (o,r) })
-     let aux accu r =
+         else
-       try SortedMap.change l restr (true,empty) r :: accu
+           Pair (only_absent,
-       with Exit -> accu in
+                 { empty with hash = 0; record = BoolRec.atom (o,r) })
-     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
+     List.fold_left
+       (fun b (p,n) ->
+          let rec aux_p accu = function
+            | x::p ->
+                (match f x with
+                   | Pair (t1,t2) -> aux_p ((t1,t2)::accu) p
+                   | Any -> aux_p accu p)
+            | [] -> aux_n accu [] n
+          and aux_n p accu = function
+            | x::n ->
+                (match f x with
+                   | Pair (t1,t2) -> aux_n p ((t1,t2)::accu) n
+                   | Any -> b)
+            | [] -> (p,accu) :: b in
+          aux_p [] p)
+       []
+       (BoolRec.get d.record)
+   let split (d : descr) l =
+     TR.boolean (aux_split d l)
+   let split_normal d l =
+     TR.boolean_normal (aux_split d l)
    let project d l =
-     project_field (get_record d.record) l
+     let t = TR.pi1 (split d l) in
+     if t.absent then raise Not_found;
+     t
+   let project_opt d l =
+     let t = TR.pi1 (split d l) in
+     { t with hash = 0; absent = false }
+   let condition d l t =
+     TR.pi2_restricted t (split d l)
+ (* TODO: eliminate this cap ... (reord l only_absent_node) when
+    not necessary. eg. {| ..... |} \ l *)
+   let remove_field d l =
+     cap (TR.pi2 (split d l)) (record l only_absent_node)
+   let first_label d =
+     let min = ref LabelPool.dummy_max in
+     let aux (_,r) =
+       match LabelMap.get r with
+           (l,_)::_ -> if (l:int) < !min then min := l | _ -> () in
+     BoolRec.iter aux d.record;
+     !min
+   let empty_cases d =
+     let x = BoolRec.compute
+               ~empty:0 ~full:3 ~cup:(lor) ~cap:(land)
+               ~diff:(fun a b -> a land lnot b)
+               ~atom:(function (o,r) ->
+                        assert (LabelMap.get r == []);
+                        if o then 3 else 1
+                     )
+               d.record in
+     (x land 2 <> 0, x land 1 <> 0)
+   let has_empty_record d =
+     BoolRec.compute
+       ~empty:false ~full:true ~cup:(||) ~cap:(&&)
+       ~diff:(fun a b -> a && not b)
+       ~atom:(function (o,r) ->
+                List.for_all
+                  (fun (l,t) -> (descr t).absent)
+                  (LabelMap.get r)
+             )
+       d.record
+ (*TODO: optimize merge
+    - pre-compute the sequence of labels
+    - remove empty or full { l = t }
+ *)
-   type normal =
+   let merge d1 d2 =
-       [ `Success
+     let res = ref empty in
-       | `Fail
+     let rec aux accu d1 d2 =
-       | `Label of label * (descr * normal) list * normal ]
+       let l = min (first_label d1) (first_label d2) in
+       if l = LabelPool.dummy_max then
-   let rec merge_record n r =
+         let (some1,none1) = empty_cases d1
-     match (n, r) with
+         and (some2,none2) = empty_cases d2 in
-       | (`Success, _) | (_, []) -> `Success
+         let none = none1 && none2 and some = some1 || some2 in
-       | (`Fail, r) ->
+         let accu = LabelMap.from_list (fun _ _ -> assert false) accu in
-           let aux (l,(o,t)) n = `Label (l, [t,n], if o then n else `Fail) in
+         (* approx for the case (some && not none) ... *)
-           List.fold_right aux r `Success
+         res := cup !res (record' (some, accu))
-       | (`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 l1 = split d1 l and l2 = split d2 l in
-             let aux a (t,x) =
+         let loop (t1,d1) (t2,d2) =
-               (let t = diff t t2 in
+           let t =
-                if non_empty t then res := (t,x) :: !res);
+             if t2.absent
-               (let t = cap t t2 in
+             then cup t1 { t2 with hash = 0; absent = false }
-                if non_empty t then res := (t, merge_record x r') :: !res);
+             else t2
-               diff a t
              in
-             let t2 = List.fold_left aux t2 present in
+           aux ((l,cons t)::accu) d1 d2
-             let () =
+         in
-               if non_empty t2 then
+         List.iter (fun x -> List.iter (loop x) l2) l1
-               res := (t2, merge_record `Fail r') :: !res in
-             let abs = if o then merge_record absent r' else absent in
+     in
-             `Label (l1, !res, abs)
+     aux [] d1 d2;
+     !res
+   let any = { empty with hash = 0; record = any.record }
+   let get d =
+     let rec aux r accu d =
+       let l = first_label d in
+       if l == LabelPool.dummy_max then
+         let (o1,o2) = empty_cases d in
+         if o1 || o2 then (LabelMap.from_list_disj r,o1,o2)::accu else accu
+       else
+         List.fold_left
+           (fun accu (t1,t2) ->
+              let x = (t1.absent, { t1 with hash = 0; absent = false }) in
+              aux ((l,x)::r) accu t2)
+           accu
+           (split d l)
+     in
+     aux [] [] d
+ end
-   let normal d =
+ module Print =
-     List.fold_left merge_record `Fail (get d)
+ struct
+   let rec print_const ppf = function
+     | Integer i -> Intervals.V.print ppf i
+     | Atom a -> Atoms.V.print_quote ppf a
+     | Char c -> Chars.V.print ppf c
+     | Pair (x,y) -> Format.fprintf ppf "(%a,%a)" print_const x print_const y
+     | Xml (x,y) -> Format.fprintf ppf "XML(%a,%a)" print_const x print_const y
+     | Record r ->
+         Format.fprintf ppf "Record{";
+         List.iter
+           (fun (l,c) ->
+              Format.fprintf ppf "%a : %a; "
+              Label.print (LabelPool.value l)
+              print_const c)
+           (LabelMap.get r);
+         Format.fprintf ppf "}"
+     | String (i,j,s,c) ->
+         Format.fprintf ppf "\"%a\" @ %a"
+         U.print (U.mk (U.get_substr s i j))
+         print_const c
+   let nil_atom = Atoms.V.mk_ascii "nil"
+   let nil_type = atom (Atoms.atom nil_atom)
+   let (seqs_node,seqs_descr) =
+     let n = make () in
+     let d = cup nil_type (times any_node n) in
+     define n d;
+     (n, d)
+   let is_regexp t = subtype t seqs_descr
-   let any = { empty with record = any.record }
+   module S = struct
-   let is_empty d = d = []
+   type t = { id : int;
+              mutable def : d list;
+              mutable state : [ `Expand | `None | `Marked | `Named of U.t ] }
+   and  d =
+     | Name of U.t
+     | Regexp of t Pretty.regexp
+     | Atomic of (Format.formatter -> unit)
+     | Pair of t * t
+     | Char of Chars.V.t
+     | Xml of [ `Tag of (Format.formatter -> unit) | `Type of t ] * t * t
+     | Record of (bool * t) label_map * bool * bool
+     | Arrows of (t * t) list * (t * t) list
+     | Neg of t
+   let compare x y = x.id - y.id
  end
+   module Decompile = Pretty.Decompile(DescrHash)(S)
+   open S
+   module DescrPairMap = Map.Make(Custom.Pair(Descr)(Descr))
+   let named = State.ref "Types.Print.named" DescrMap.empty
+   let named_xml = State.ref "Types.Print.named_xml"  DescrPairMap.empty
+   let register_global (name : U.t) d =
+     if equal { d with hash = 0; xml = BoolPair.empty } empty then
+       (let l = (*Product.merge_same_2*) (Product.get ~kind:`XML d) in
+       match l with
+         | [(t1,t2)] -> named_xml := DescrPairMap.add (t1,t2) name !named_xml
+         | _ -> ());
+     named := DescrMap.add d name !named
+   let memo = DescrHash.create 63
+   let counter = ref 0
+   let alloc def = { id = (incr counter; !counter); def = def; state = `None }
+   let count_name = ref 0
+   let name () =
+     incr count_name;
+     U.mk ("X" ^ (string_of_int !count_name))
+   let to_print = ref []
+   let trivial_rec b =
+     b == BoolRec.empty ||
+     (is_empty { empty with hash = 0; record = BoolRec.diff BoolRec.full b})
+   let trivial_pair b = b == BoolPair.empty || b == BoolPair.full
+   let worth_abbrev d =
+     not (trivial_pair d.times && trivial_pair d.xml &&
+          trivial_pair d.arrow && trivial_rec d.record)
+   let worth_complement d =
+     let aux f x y = if f x y = 0 then 1 else 0 in
+     let n =
+       aux Atoms.compare d.atoms any.atoms +
+       aux Chars.compare d.chars any.chars +
+       aux Intervals.compare d.ints any.ints +
+       aux BoolPair.compare d.times any.times +
+       aux BoolPair.compare d.xml any.xml +
+       aux BoolPair.compare d.arrow any.arrow +
+       aux BoolRec.compare d.record any.record in
+     n >= 4
+   let rec prepare d =
+     try DescrHash.find memo d
+     with Not_found ->
+       try
+         let n = DescrMap.find d !named in
+         let s = alloc [] in
+         s.state <- `Named n;
+         DescrHash.add memo d s;
+         s
+       with Not_found ->
+         if worth_complement d then
+           alloc [Neg (prepare (neg d))]
+         else
+         let slot = alloc [] in
+         if not (worth_abbrev d) then slot.state <- `Expand;
+         DescrHash.add memo d slot;
+         let (seq,not_seq) =
+           if (subtype { empty with hash = 0; times = d.times } seqs_descr) then
+             (cap d seqs_descr, diff d seqs_descr)
+           else
+             (empty, d) in
+         let add u = slot.def <- u :: slot.def in
+         if (non_empty seq) then
+           add (Regexp (decompile seq));
+         List.iter
+           (fun (t1,t2) -> add (Pair (prepare t1, prepare t2)))
+           (Product.get not_seq);
+         List.iter
+           (fun (t1,t2) ->
+              try
+                let n = DescrPairMap.find (t1,t2) !named_xml in
+                add (Name n)
+              with
+                  Not_found ->
+              let tag =
+                match Atoms.print_tag t1.atoms with
+                  | Some a when is_empty { t1 with hash=0; atoms = Atoms.empty } -> `Tag a
+                  | _ -> `Type (prepare t1) in
+              assert (equal { t2 with hash=0; times = empty.times } empty);
+              List.iter
+                (fun (ta,tb) -> add (Xml (tag, prepare ta, prepare tb)))
+                (Product.get t2)
+           )
+           ((*Product.merge_same_2*) (Product.get ~kind:`XML not_seq));
+         List.iter
+           (fun (r,some,none) ->
+              let r = LabelMap.map (fun (o,t) -> (o, prepare t)) r in
+              add (Record (r,some,none)))
+           (Record.get not_seq);
+         (match Chars.is_char not_seq.chars with
+           | Some c -> add (Char c)
+           | None ->
+               List.iter (fun x -> add (Atomic x)) (Chars.print not_seq.chars));
+         List.iter (fun x -> add (Atomic x)) (Intervals.print not_seq.ints);
+         List.iter (fun x -> add (Atomic x)) (Atoms.print not_seq.atoms);
+         List.iter
+           (fun (p,n) ->
+              let aux (t,s) = prepare (descr t), prepare (descr s) in
+              let p = List.map aux p and n = List.map aux n in
+              add (Arrows (p,n)))
+           (BoolPair.get not_seq.arrow);
+         slot.def <- List.rev slot.def;
+         slot
+   and decompile d =
+     Decompile.decompile
+       (fun t ->
+          let tr = Product.get t in
+          let tr = List.map (fun (l,t) -> prepare l, t) tr in
+          tr, Atoms.contains nil_atom t.atoms)
+       d
+   let gen = ref 0
+   let rec assign_name s =
+     incr gen;
+     match s.state with
+       | `None ->
+           let g = !gen in
+           s.state <- `Marked;
+           List.iter assign_name_rec s.def;
+           if (s.state == `Marked) && (!gen == g) then s.state <- `None
+       | `Marked -> s.state <- `Named (name ()); to_print := s :: !to_print
+       | _ -> ()
+   and assign_name_rec = function
+     | Neg t -> assign_name t
+     | Name _ | Char _ | Atomic _ -> ()
+     | Regexp r -> assign_name_regexp r
+     | Pair (t1,t2) -> assign_name t1; assign_name t2
+     | Xml (tag,t2,t3) ->
+         (match tag with `Type t -> assign_name t | _ -> ());
+         assign_name t2;
+         assign_name t3
+     | Record (r,_,_) ->
+         List.iter (fun (_,(_,t)) -> assign_name t) (LabelMap.get r)
+     | Arrows (p,n) ->
+         List.iter (fun (t1,t2) -> assign_name t1; assign_name t2) p;
+         List.iter (fun (t1,t2) -> assign_name t1; assign_name t2) n
+   and assign_name_regexp = function
+     | Pretty.Epsilon | Pretty.Empty -> ()
+     | Pretty.Alt (r1,r2)
+     | Pretty.Seq (r1,r2) -> assign_name_regexp r1; assign_name_regexp r2
+     | Pretty.Star r | Pretty.Plus r -> assign_name_regexp r
+     | Pretty.Trans t -> assign_name t
+   let rec do_print_slot pri ppf s =
+     match s.state with
+       | `Named n -> Format.fprintf ppf "%a" U.print n
+       | _ -> do_print_slot_real pri ppf s.def
+   and do_print_slot_real pri ppf def =
+     let rec aux ppf = function
+       | [] -> Format.fprintf ppf "Empty"
+       | [ h ] -> do_print ppf h
+       | h :: t -> Format.fprintf ppf "%a |@ %a" do_print h aux t
+     in
+     if (pri >= 2) && (List.length def >= 2)
+     then Format.fprintf ppf "@[(%a)@]" aux def
+     else aux ppf def
+   and do_print ppf = function
+     | Neg t -> Format.fprintf ppf "Any \\ (@[%a@])" (do_print_slot 0) t
+     | Name n -> Format.fprintf ppf "%a" U.print n
+     | Char c -> Chars.V.print ppf c
+     | Regexp r -> Format.fprintf ppf "@[[ %a ]@]" (do_print_regexp 0) r
+     | Atomic a -> a ppf
+     | Pair (t1,t2) ->
+         Format.fprintf ppf "@[(%a,%a)@]"
+           (do_print_slot 0) t1
+           (do_print_slot 0) t2
+     | Xml (tag,attr,t) ->
+         Format.fprintf ppf "<%a%a>%a"
+           do_print_tag tag
+           do_print_attr attr
+           (do_print_slot 0) t
+     | Record (r,some,none) ->
+         if some then Format.fprintf ppf "@[{"
+         else Format.fprintf ppf "@[{|";
+         do_print_record ppf r;
+         if not none then  Format.fprintf ppf ";@ ...";
+         if some then Format.fprintf ppf " }@]"
+         else Format.fprintf ppf " |}@]"
+     | Arrows (p,n) ->
+         (match p with
+            | [] -> Format.fprintf ppf "Arrow"
+            | (t,s)::l ->
+                Format.fprintf ppf "%a" do_print_arrow (t,s);
+                List.iter
+                  (fun (t,s) ->
+                     Format.fprintf ppf " &@ %a" do_print_arrow (t,s)
+                  ) l);
+         List.iter
+           (fun (t,s) ->
+              Format.fprintf ppf " \\@ %a" do_print_arrow (t,s)
+           ) n
+   and do_print_arrow ppf (t,s) =
+     Format.fprintf ppf "%a -> %a"
+       (do_print_slot 0) t
+       (do_print_slot 0) s
+   and do_print_tag ppf = function
+     | `Tag s -> s ppf
+     | `Type t -> Format.fprintf ppf "(%a)" (do_print_slot 0) t
+   and do_print_attr ppf = function
+     | { state = `Marked|`Expand;
+         def = [ Record (r,true,true) ] } -> do_print_record ppf r
+     | t -> Format.fprintf ppf " %a" (do_print_slot 2) t
+   and do_print_record ppf r =
+     let first = ref true in
+     List.iter
+       (fun (l,(o,t)) ->
+          let sep = if !first then (first := false; "") else ";" in
+          let opt = if o then "?" else "" in
+          Format.fprintf ppf "%s@ @[%a =%s@] %a" sep
+            Label.print (LabelPool.value l) opt (do_print_slot 0) t
+       ) (LabelMap.get r)
+   and do_print_regexp pri ppf = function
+     | Pretty.Empty ->  Format.fprintf ppf "Empty" (*assert false *)
+     | Pretty.Epsilon -> ()
+     | Pretty.Seq (Pretty.Trans { def = [ Char _ ] }, _) as r->
+         (match extract_string [] r with
+           | s, None ->
+               Format.fprintf ppf "'";
+               List.iter (Chars.V.print_in_string ppf) s;
+               Format.fprintf ppf "'"
+           | s, Some r ->
+               if pri >= 3 then Format.fprintf ppf "@[(";
+               Format.fprintf ppf "'";
+               List.iter (Chars.V.print_in_string ppf) s;
+               Format.fprintf ppf "' %a" (do_print_regexp 2) r;
+               if pri >= 3 then Format.fprintf ppf ")@]")
+     | Pretty.Seq (r1,r2) ->
+         if pri >= 3 then Format.fprintf ppf "@[(";
+         Format.fprintf ppf "%a@ %a"
+           (do_print_regexp 2) r1
+           (do_print_regexp 2) r2;
+         if pri >= 3 then Format.fprintf ppf ")@]"
+     | Pretty.Alt (r,Pretty.Epsilon) | Pretty.Alt (Pretty.Epsilon,r) ->
+         Format.fprintf ppf "@[%a@]?" (do_print_regexp 3) r
+     | Pretty.Alt (r1,r2) ->
+         if pri >= 2 then Format.fprintf ppf "@[(";
+         Format.fprintf ppf "%a |@ %a"
+           (do_print_regexp 1) r1
+           (do_print_regexp 1) r2;
+         if pri >= 2 then Format.fprintf ppf ")@]"
+     | Pretty.Star r ->
+         Format.fprintf ppf "@[%a@]*" (do_print_regexp 3) r
+     | Pretty.Plus r ->
+         Format.fprintf ppf "@[%a@]+" (do_print_regexp 3) r
+     | Pretty.Trans t ->
+         do_print_slot pri ppf t
+   and extract_string accu = function
+     | Pretty.Seq (Pretty.Trans { def = [ Char c ] }, r) ->
+         extract_string (c :: accu) r
+     | Pretty.Trans { def = [ Char c ] } ->
+         (List.rev (c :: accu), None)
+     | r -> (List.rev accu,Some r)
+   let get_name = function
+     | { state = `Named n } -> n
+     | _ -> assert false
+   let print ppf d =
+     let t = prepare d in
+     assign_name t;
+     Format.fprintf ppf "@[@[%a@]" (do_print_slot 0) t;
+     (match List.rev !to_print with
+        | [] -> ()
+        | s::t ->
+            Format.fprintf ppf
+              " where@ @[<v>%a = @[%a@]" U.print (get_name s)
+            (do_print_slot_real 0) s.def;
+            List.iter
+              (fun s ->
+                 Format.fprintf ppf " and@ %a = @[%a@]"  U.print
+                   (get_name s) (do_print_slot_real 0) s.def)
+              t;
+            Format.fprintf ppf "@]"
+     );
+     Format.fprintf ppf "@]";
+     count_name := 0;
+     to_print := [];
+     DescrHash.clear memo
+ end
+ module Positive =
+ struct
+   type rhs = [ `Type of descr | `Cup of v list | `Times of v * v | `Xml 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)
+         | `Xml (v1,v2) -> xml (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 xml d1 d2 = cons (`Xml (d1,d2))
+   let define v1 v2 = def v1 (`Cup [v2])
+   let solve v = internalize (make_node v)
+ end
  let memo_normalize = ref DescrMap.empty
- let map_sort f l =
-   SortedList.from_list (List.map f l)
  let rec rec_normalize d =
    try DescrMap.find d !memo_normalize
-Line 747
+Line 1530
      let n = make () in
      memo_normalize := DescrMap.add d n !memo_normalize;
      let times =
-       map_sort
+       List.fold_left
-         (fun (d1,d2) -> [(rec_normalize d1, rec_normalize d2)],[])
+         (fun accu (d1,d2) -> BoolPair.cup accu (BoolPair.atom (rec_normalize d1, rec_normalize d2)))
-         (Product.normal d)
+         BoolPair.empty (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 };
+     let xml =
+       List.fold_left
+         (fun accu (d1,d2) -> BoolPair.cup accu (BoolPair.atom (rec_normalize d1, rec_normalize d2)))
+         BoolPair.empty (Product.normal ~kind:`XML d)
+     in
+     let record = d.record
+     in
+     define n { d with hash=0; times = times; xml = xml; record = record };
      n
  let normalize n =
-Line 764
+Line 1549
  module Arrow =
  struct
-   let check_simple left s1 s2 =
+   let check_simple left (s1,s2) =
      let rec aux accu1 accu2 = function
        | (t1,t2)::left ->
            let accu1' = diff_t accu1 t1 in
-Line 777
+Line 1562
      (is_empty accu1) ||
      (try aux accu1 (diff any (descr s2)) left; true with NotEmpty -> false)
+   let check_line_non_empty (left,right) =
+     not (List.exists (check_simple left) right)
+   let sample t =
+     let (left,right) = List.find check_line_non_empty (BoolPair.get t.arrow) in
+     List.fold_left (fun accu (t,s) -> cap accu (arrow t s))
+       { empty with hash=0; arrow = any.arrow } left
    let check_strenghten t s =
-     let left = match t.arrow with [ (p,[]) ] -> p | _ -> assert false in
+ (*
+     let left = match (BoolPair.get t.arrow) with [ (p,[]) ] -> p | _ -> assert false in
      let rec aux = function
        | [] -> raise Not_found
        | (p,n) :: rem ->
            if (List.for_all (fun (a,b) -> check_simple left a b) p) &&
              (List.for_all (fun (a,b) -> not (check_simple left a b)) n) then
-               { empty with arrow = [ (SortedList.cup left p, n) ] }
+               { empty with hash=0; arrow = Obj.magic [ (SortedList.cup left p, n) ] }  (* rework this ! *)
            else aux rem
      in
-     aux s.arrow
+     aux (BoolPair.get s.arrow)
+ *)
+     if subtype t s then t else raise Not_found
    let check_simple_iface left s1 s2 =
      let rec aux accu1 accu2 = function
-Line 810
+Line 1607
             (List.for_all (fun (a,b) -> not (check_simple_iface iface a b)) n))
            || (aux rem)
      in
-     aux s.arrow
+     aux (BoolPair.get s.arrow)
    type t = descr * (descr * descr) list list
    let get t =
      List.fold_left
        (fun ((dom,arr) as accu) (left,right) ->
-          if Sample.check_empty_arrow_line left right
+          if check_line_non_empty (left,right)
-          then accu
+          then
-          else (
+            let left = List.map (fun (t,s) -> (descr t, descr s)) left in
-            let left =
-              List.map
-                (fun (t,s) -> (descr t, descr s)) left in
             let d = List.fold_left (fun d (t,_) -> cup d t) empty left in
             (cap dom d, left :: arr)
-          )
+          else accu
        )
        (any, [])
-       t.arrow
+       (BoolPair.get t.arrow)
    let domain (dom,_) = dom
-Line 865
+Line 1659
        )
        empty arr
-   let any = { empty with arrow = any.arrow }
+   let any = { empty with hash=0; arrow = any.arrow }
-   let is_empty (_,arr) = arr = []
+   let is_empty (_,arr) = arr == []
  end
  module Int = struct
    let has_int d i = Intervals.contains i d.ints
    let get d = d.ints
-   let put i = { empty with ints = i }
+   let any = { empty with hash=0; ints = any.ints }
-   let is_int d = is_empty { d with ints = Intervals.empty }
-   let any = { empty with ints = Intervals.any }
  end
  module Atom = struct
    let has_atom d a = Atoms.contains a d.atoms
+   let get d = d.atoms
+   let any = { empty with hash=0; atoms = any.atoms }
  end
  module Char = struct
    let has_char d c = Chars.contains c d.chars
-   let any = { empty with chars = Chars.any }
+   let is_empty d = Chars.is_empty d.chars
+   let get d = d.chars
+   let any = { empty with hash=0; chars = any.chars }
  end
- (*
+   (* <helpers> *)
- let rec print_normal_record ppf = function
-   | Success -> Format.fprintf ppf "Yes"
-   | Fail -> Format.fprintf ppf "No"
-   | FirstLabel (l,present,absent) ->
-       Format.fprintf ppf "%s?@[<v>@\n" (label_name l);
-       List.iter
-         (fun (t,n) ->
-            Format.fprintf ppf "(%a)=>@[%a@]@\n"
-              Print.print_descr t
-              print_normal_record n
-         ) present;
-       if absent <> Fail then
-         Format.fprintf ppf "(absent)=>@[%a@]@\n" print_normal_record absent;
-       Format.fprintf ppf "@]"
- *)
+ let choice_of_list = List.fold_left cup empty
- (*
+ let xml' tag attrs cont = xml (cons tag) (cons (times (cons attrs) (cons cont)))
- let pr s = Types.Print.print Format.std_formatter (Syntax.make_type (Syntax.parse s));;
- let pr' s = Types.Print.print Format.std_formatter
+ let rec_of_list ?(opened=true) l =
-    (Types.normalize (Syntax.make_type (Syntax.parse s)));;
+   let map =
+     List.fold_left
+       (fun acc (name,typ) ->
+         LabelMap.union_disj acc
+           (LabelMap.singleton (LabelPool.mk (Ns.empty,Utf8.mk name)) (cons typ)))
+       LabelMap.empty
+       l
+   in
+   record' (opened, map)
- BUG:
+ let rec_of_list' ?(opened=true) l =
- pr "'a | 'b where 'a = ('a , 'a) and 'b= ('b , 'b)";;
+   let map =
- *)
+     List.fold_left
+       (fun acc (opt,name,typ) ->
+         LabelMap.union_disj acc
+           (LabelMap.singleton (LabelPool.mk (Ns.empty,Utf8.mk name))
+             (if opt then cons (Record.or_absent typ) else (cons typ))))
+       LabelMap.empty
+       l
+   in
+   record' (opened, map)
+ let empty_closed_record = rec_of_list ~opened:false []
+ let empty_opened_record = rec_of_list ~opened:true []
+   (* </helpers> *)
- (*
-   let nr s =
-     let t = Types.descr (Syntax.make_type (Syntax.parse s)) in
-     let n = Types.normal_record' t.Types.record in
-     Types.print_normal_record Format.std_formatter n;;
- *)

 Legend:



Removed from v.71
 


changed lines


 
Added in v.698
 Legend:



Removed from v.71
 


changed lines


 
Added in v.698
-Removed from v.71
+Added in v.698

CVS Admin">CVS Admin	ViewVC Help
Powered by ViewVC 1.1.5