/[svn]/typing/typer.ml

Diff of /typing/typer.ml

Parent Directory | Revision Log | View Patch Patch

-revision 72 by abate,
Tue Jul 10 17:03:39 2007 UTC
+revision 1401 by abate,
Tue Jul 10 18:46:22 2007 UTC
 Line 1
- (* I. Transform the abstract syntax of types and patterns into
+ (* TODO:
-       the internal form *)
+  - rewrite type-checking of operators to propagate constraint
+  - optimize computation of pattern free variables
+  - check whether it is worth using recursive hash-consing internally
+ *)
  open Location
  open Ast
+ open Ident
+ let debug_schema = false
+ let warning loc msg =
+   Format.fprintf !Location.warning_ppf "Warning %a:@\n%a%s@."
+     Location.print_loc (loc,`Full)
+     Location.html_hilight (loc,`Full)
+     msg
- exception Pattern of string
  exception NonExhaustive of Types.descr
- exception MultipleLabel of Types.label
+ exception Constraint of Types.descr * Types.descr
- exception Constraint of Types.descr * Types.descr * string
  exception ShouldHave of Types.descr * string
- exception WrongLabel of Types.descr * Types.label
+ exception ShouldHave2 of Types.descr * string * Types.descr
- exception UnboundId of string
+ exception WrongLabel of Types.descr * label
+ exception UnboundId of id * bool
+ exception UnboundExtId of Types.CompUnit.t * id
+ exception Error of string
+ exception Warning of string * Types.t
+ let raise_loc loc exn = raise (Location (loc,`Full,exn))
+ let raise_loc_str loc ofs exn = raise (Location (loc,`Char ofs,exn))
+ let error loc msg = raise_loc loc (Error msg)
+ type item =
+   | Type of Types.t
+   | Val of Types.t
+ module UEnv = Map.Make(U)
+ type t = {
+   ids : item Env.t;
+   ns: Ns.table;
+   cu: Types.CompUnit.t UEnv.t;
+   schemas: string UEnv.t
+ }
- let raise_loc loc exn = raise (Location (loc,exn))
+ let hash _ = failwith "Typer.hash"
+ let compare _ _ = failwith "Typer.compare"
+ let dump ppf _ = failwith "Typer.dump"
+ let equal _ _ = failwith "Typer.equal"
+ let check _ = failwith "Typer.check"
+ (* TODO: filter out builtin defs ? *)
+ let serialize_item s = function
+   | Type t -> Serialize.Put.bits 1 s 0; Types.serialize s t
+   | Val t -> Serialize.Put.bits 1 s 1; Types.serialize s t
+ let serialize s env =
+   Serialize.Put.env Id.serialize serialize_item Env.iter s env.ids;
+   Ns.serialize_table s env.ns
+ let deserialize_item s = match Serialize.Get.bits 1 s with
+   | 0 -> Type (Types.deserialize s)
+   | 1 -> Val (Types.deserialize s)
+   | _ -> assert false
- (* Internal representation as a graph (desugar recursive types and regexp),
+ let deserialize s =
-    to compute freevars, etc... *)
+   let ids = Serialize.Get.env Id.deserialize deserialize_item Env.add Env.empty s in
+   let ns = Ns.deserialize_table s in
+   { ids = ids; ns = ns; cu = UEnv.empty; schemas = UEnv.empty }
- type ti = {
-   id : int;
+ let empty_env = {
-   mutable loc' : loc;
+   ids = Env.empty;
-   mutable fv : string SortedList.t option;
+   ns = Ns.empty_table;
-   mutable descr': descr;
+   cu = UEnv.empty;
-   mutable type_node: Types.node option;
+   schemas = UEnv.empty
-   mutable pat_node: Patterns.node option
  }
- and descr =
-    [ `Alias of string * ti
-    | `Type of Types.descr
-    | `Or of ti * ti
-    | `And of ti * ti * bool
-    | `Diff of ti * ti
-    | `Times of ti * ti
-    | `Arrow of ti * ti
-    | `Record of Types.label * bool * ti
-    | `Capture of Patterns.capture
-    | `Constant of Patterns.capture * Types.const
-    ]
+ let from_comp_unit = ref (fun cu -> assert false)
+ let enter_cu x cu env =
+   { env with cu = UEnv.add x cu env.cu }
- module S = struct type t = string let compare = compare end
+ let find_cu x env =
- module StringMap = Map.Make(S)
+   try UEnv.find x env.cu
- module StringSet = Set.Make(S)
+   with Not_found -> Types.CompUnit.mk x
- let mk' =
-   let counter = ref 0 in
+ let enter_schema x uri env =
-   fun loc ->
+   { env with schemas = UEnv.add x uri env.schemas }
-     incr counter;
+ let find_schema x env =
-     let rec x = {
+   try UEnv.find x env.schemas
-       id = !counter;
+   with Not_found -> raise (Error (Printf.sprintf "%s: no such schema" (U.get_str x)))
-       loc' = loc;
-       fv = None;
+ let enter_type id t env =
-       descr' = `Alias ("__dummy__", x);
+   { env with ids = Env.add id (Type t) env.ids }
-       type_node = None;
+ let enter_types l env =
-       pat_node = None
+   { env with ids =
-     } in
+       List.fold_left (fun accu (id,t) -> Env.add id (Type t) accu) env.ids l }
-     x
+ let find_type id env =
+   match Env.find id env.ids with
+     | Type t -> t
+     | Val _ -> raise Not_found
+ let find_type_global loc cu id env =
+   let cu = find_cu cu env in
+   let env = !from_comp_unit cu in
+   find_type id env
+ let enter_value id t env =
+   { env with ids = Env.add id (Val t) env.ids }
+ let enter_values l env =
+   { env with ids =
+       List.fold_left (fun accu (id,t) -> Env.add id (Val t) accu) env.ids l }
+ let enter_values_dummy l env =
+   { env with ids =
+       List.fold_left (fun accu id -> Env.add id (Val Types.empty) accu) env.ids l }
+ let find_value id env =
+   match Env.find id env.ids with
+     | Val t -> t
+     | _ -> raise Not_found
+ let find_value_global cu id env =
+   let env = !from_comp_unit cu in
+   find_value id env
+ let value_name_ok id env =
+   try match Env.find id env.ids with
+     | Val t -> true
+     | _ -> false
+   with Not_found -> true
+ let iter_values env f =
+   Env.iter (fun x ->
+               function Val t -> f x t;
+                 | _ -> ()) env.ids
+ let register_types cu env =
+   let prefix = U.concat (Types.CompUnit.value cu) (U.mk ":") in
+   Env.iter (fun x ->
+               function
+                 | Type t ->
+                     let n = U.concat prefix (Id.value x) in
+                     Types.Print.register_global n t
+                 | _ -> ()) env.ids
+ (* Namespaces *)
+ let set_ns_table_for_printer env =
+   Ns.InternalPrinter.set_table env.ns
+ let get_ns_table tenv = tenv.ns
+ let enter_ns p ns env =
+   { env with ns = Ns.add_prefix p ns env.ns }
+ let protect_error_ns loc f x =
+   try f x
+   with Ns.UnknownPrefix ns ->
+     raise_loc_generic loc
+     ("Undefined namespace prefix " ^ (U.to_string ns))
+ let parse_atom env loc t =
+   let (ns,l) = protect_error_ns loc (Ns.map_tag env.ns) t in
+   Atoms.V.mk ns l
+ let parse_ns env loc ns =
+   protect_error_ns loc (Ns.map_prefix env.ns) ns
+ let parse_label env loc t =
+   let (ns,l) = protect_error_ns loc (Ns.map_attr env.ns) t in
+   LabelPool.mk (ns,l)
+ let parse_record env loc f r =
+   let r = List.map (fun (l,x) -> (parse_label env loc l, f x)) r in
+   LabelMap.from_list (fun _ _ -> raise_loc_generic loc "Duplicated record field") r
+ let rec const env loc = function
+   | LocatedExpr (loc,e) -> const env loc e
+   | Pair (x,y) -> Types.Pair (const env loc x, const env loc y)
+   | Xml (x,y) -> Types.Xml (const env loc x, const env loc y)
+   | RecordLitt x -> Types.Record (parse_record env loc (const env loc) x)
+   | String (i,j,s,c) -> Types.String (i,j,s,const env loc c)
+   | Atom t -> Types.Atom (parse_atom env loc t)
+   | Integer i -> Types.Integer i
+   | Char c -> Types.Char c
+   | Const c -> c
+   | _ -> raise_loc_generic loc "This should be a scalar or structured constant"
- let cons loc d =
+ (* I. Transform the abstract syntax of types and patterns into
-   let x = mk' loc in
+       the internal form *)
-   x.descr' <- d;
-   x
- (* Note:
-    Compilation of Regexp is implemented as a ``rewriting'' of
-    the parsed syntax, in order to be able to print its result
-    (for debugging for instance)
-    It would be possible (and a little more efficient) to produce
+ (* Schema *)
-    directly ti nodes.
- *)
- module Regexp = struct
+ let is_registered_schema env s = UEnv.mem s env.schemas
-   let defs = ref []
-   let name =
+ (* uri -> schema binding *)
-     let c = ref 0 in
+ let schemas = State.ref "Typer.schemas" (Hashtbl.create 3)
-     fun () ->
-       incr c;
+ let schema_types = State.ref "Typer.schema_types" (Hashtbl.create 51)
-       "#" ^ (string_of_int !c)
+ let schema_elements = State.ref "Typer.schema_elements" (Hashtbl.create 51)
+ let schema_attributes = State.ref "Typer.schema_attributes" (Hashtbl.create 51)
-   let rec seq_vars accu = function
+ let schema_attribute_groups =
-     | Epsilon | Elem _ -> accu
+   State.ref "Typer.schema_attribute_groups" (Hashtbl.create 51)
-     | Seq (r1,r2) | Alt (r1,r2) -> seq_vars (seq_vars accu r1) r2
+ let schema_model_groups =
-     | Star r | WeakStar r -> seq_vars accu r
+   State.ref "Typer.schema_model_groups" (Hashtbl.create 51)
-     | SeqCapture (v,r) -> seq_vars (StringSet.add v accu) r
-   let uniq_id = let r = ref 0 in fun () -> incr r; !r
-   type flat = [ `Epsilon
-               | `Elem of int * Ast.ppat  (* the int arg is used to
-                                             to stop generic comparison *)
-               | `Seq of flat * flat
-               | `Alt of flat * flat
-               | `Star of flat
-               | `WeakStar of flat ]
-   let rec propagate vars : regexp -> flat = function
-     | Epsilon -> `Epsilon
-     | Elem x -> let p = vars x in `Elem (uniq_id (),p)
-     | Seq (r1,r2) -> `Seq (propagate vars r1,propagate vars r2)
-     | Alt (r1,r2) -> `Alt (propagate vars r1, propagate vars r2)
-     | Star r -> `Star (propagate vars r)
-     | WeakStar r -> `WeakStar (propagate vars r)
-     | SeqCapture (v,x) ->
-         let v= mk noloc (Capture v) in
-         propagate (fun p -> mk noloc (And (vars p,v,true))) x
-   let cup r1 r2 =
-     match (r1,r2) with
-       | (_, `Empty) -> r1
-       | (`Empty, _) -> r2
-       | (`Res t1, `Res t2) -> `Res (mk noloc (Or (t1,t2)))
- (*TODO: review this compilation schema to avoid explosion when
-   coding (Optional x) by  (Or(Epsilon,x)); memoization ... *)
-   module Memo = Map.Make(struct type t = flat list let compare = compare end)
-   module Coind = Set.Make(struct type t = flat list let compare = compare end)
-   let memo = ref Memo.empty
-   let rec compile fin e seq : [`Res of Ast.ppat | `Empty] =
-     if Coind.mem seq !e then `Empty
-     else (
-       e := Coind.add seq !e;
-       match seq with
-         | [] ->
-             `Res fin
-         | `Epsilon :: rest ->
-             compile fin e rest
-         | `Elem (_,p) :: rest ->
-             `Res (mk noloc (Prod (p, guard_compile fin rest)))
-         | `Seq (r1,r2) :: rest ->
-             compile fin e (r1 :: r2 :: rest)
-         | `Alt (r1,r2) :: rest ->
-             cup (compile fin e (r1::rest)) (compile fin e (r2::rest))
-         | `Star r :: rest ->
-             cup (compile fin e (r::seq)) (compile fin e rest)
-         | `WeakStar r :: rest ->
-             cup (compile fin e rest) (compile fin e (r::seq))
-     )
-   and guard_compile fin seq =
-     try Memo.find seq !memo
-     with
-         Not_found ->
-           let n = name () in
-           let v = mk noloc (PatVar n) in
-           memo := Memo.add seq v !memo;
-           let d = compile fin (ref Coind.empty) seq in
-           (match d with
-              | `Empty -> assert false
-              | `Res d -> defs := (n,d) :: !defs);
-           v
-   let atom_nil = Types.mk_atom "nil"
-   let constant_nil v t =
-     mk noloc (And (t, (mk noloc (Constant (v, Types.Atom atom_nil))), true))
-   let compile regexp queue : ppat =
-     let vars = seq_vars StringSet.empty regexp in
-    let fin = StringSet.fold constant_nil vars queue in
-     let n = guard_compile fin [propagate (fun p -> p) regexp] in
-     memo := Memo.empty;
-     let d = !defs in
-     defs := [];
-     mk noloc (Recurs (n,d))
- end
- let compile_regexp = Regexp.compile
+   (* raise Not_found *)
- let rec compile env { loc = loc; descr = d } : ti =
-   match (d : Ast.ppat') with
+ let get_schema_fwd = ref (fun _ -> assert false)
-   | PatVar s ->
-       (try StringMap.find s env
+ let find_schema_descr_uri kind uri name =
+   try
+     ignore (!get_schema_fwd uri);
+     let elt () = Hashtbl.find !schema_elements (uri, name) in
+     let typ () = Hashtbl.find !schema_types (uri, name) in
+     let att () = Hashtbl.find !schema_attributes (uri, name) in
+     let att_group () = Hashtbl.find !schema_attribute_groups (uri, name) in
+     let mod_group () = Hashtbl.find !schema_model_groups (uri, name) in
+     let rec do_try n = function
+       | [] -> raise Not_found
+       | f :: rem -> (try f () with Not_found -> do_try n rem)
+     in
+     match kind with
+       | Some `Element -> do_try "element" [ elt ]
+       | Some `Type -> do_try "type" [ typ ]
+       | Some `Attribute -> do_try "atttribute" [ att ]
+       | Some `Attribute_group -> do_try "attribute group" [ att_group ]
+       | Some `Model_group -> do_try "model group" [ mod_group ]
+       | None ->
+           (* policy for unqualified schema component resolution. This order should
+            * be consistent with Schema_component.get_component *)
+           do_try "component" [ elt; typ; att; att_group; mod_group ]
         with Not_found ->
-          raise_loc loc (Pattern ("Undefined type variable " ^ s))
+       raise (Error (Printf.sprintf "No %s named '%s' found in schema '%s'"
+                       (Schema_common.string_of_component_kind kind) (U.get_str name) uri))
+ let find_schema_descr env kind schema name =
+   let uri = find_schema schema env in
+   find_schema_descr_uri kind uri name
+ (* Eliminate Recursion, propagate Sequence Capture Variables *)
+ (* We use two intermediate representation from AST types/patterns
+    to internal ones:
+       AST -(1)-> derecurs -(2)-> slot -(3)-> internal
+    (1) eliminate recursion, schema,
+        propagate sequence capture variables, keep regexps
+    (2) stratify, detect ill-formed recursion, compile regexps
+    (3) check additional constraints on types / patterns;
+        deep (recursive) hash-consing
+ *)
+ type derecurs_slot = {
+   ploc : Location.loc;
+   pid  : int;
+   mutable ploop : bool;
+   mutable pdescr : derecurs;
+ } and derecurs =
+   | PDummy
+   | PAlias of derecurs_slot
+   | PType of Types.descr
+   | POr of derecurs * derecurs
+   | PAnd of derecurs * derecurs
+   | PDiff of derecurs * derecurs
+   | PTimes of derecurs * derecurs
+   | PXml of derecurs * derecurs
+   | PArrow of derecurs * derecurs
+   | POptional of derecurs
+   | PRecord of bool * (derecurs * derecurs option) label_map
+   | PCapture of id
+   | PConstant of id * Types.const
+   | PRegexp of derecurs_regexp
+ and derecurs_regexp =
+   | PEpsilon
+   | PElem of derecurs
+   | PGuard of derecurs
+   | PSeq of derecurs_regexp * derecurs_regexp
+   | PAlt of derecurs_regexp * derecurs_regexp
+   | PStar of derecurs_regexp
+   | PWeakStar of derecurs_regexp
+ type descr =
+   | IDummy
+   | IType of Types.descr
+   | IOr of descr * descr
+   | IAnd of descr * descr
+   | IDiff of descr * descr
+   | ITimes of slot * slot
+   | IXml of slot * slot
+   | IArrow of slot * slot
+   | IOptional of descr
+   | IRecord of bool * (slot * descr option) label_map
+   | ICapture of id
+   | IConstant of id * Types.const
+ and slot = {
+   mutable fv : fv option;
+   mutable hash : int option;
+   mutable rank1: int; mutable rank2: int;
+   mutable gen1 : int; mutable gen2: int;
+   mutable d    : descr;
+ }
+ let counter = ref 0
+ let mk_derecurs_slot loc =
+   incr counter;
+   { ploop = false; ploc = loc; pid = !counter; pdescr = PDummy }
+ let mk_slot () =
+   { d=IDummy; fv=None; hash=None; rank1=0; rank2=0; gen1=0; gen2=0 }
+ (* This environment is used in phase (1) to eliminate recursion *)
+ type penv = {
+   penv_tenv : t;
+   penv_derec : derecurs_slot Env.t;
+ }
+ let penv tenv = { penv_tenv = tenv; penv_derec = Env.empty }
+ let rec hash_derecurs = function
+   | PDummy -> assert false
+   | PAlias s ->
+       s.pid
+   | PType t ->
++ 17 * (Types.hash t)
+   | POr (p1,p2) ->
++ 17 * (hash_derecurs p1) + 257 * (hash_derecurs p2)
+   | PAnd (p1,p2) ->
++ 17 * (hash_derecurs p1) + 257 * (hash_derecurs p2)
+   | PDiff (p1,p2) ->
++ 17 * (hash_derecurs p1) + 257 * (hash_derecurs p2)
+   | PTimes (p1,p2) ->
++ 17 * (hash_derecurs p1) + 257 * (hash_derecurs p2)
+   | PXml (p1,p2) ->
++ 17 * (hash_derecurs p1) + 257 * (hash_derecurs p2)
+   | PArrow (p1,p2) ->
++ 17 * (hash_derecurs p1) + 257 * (hash_derecurs p2)
+   | POptional p ->
++ 17 * (hash_derecurs p)
+   | PRecord (o,r) ->
+       (if o then 9 else 10) + 17 * (LabelMap.hash hash_derecurs_field r)
+   | PCapture x ->
++ 17 * (Id.hash x)
+   | PConstant (x,c) ->
++ 17 * (Id.hash x) + 257 * (Types.Const.hash c)
+   | PRegexp p ->
++ 17 * (hash_derecurs_regexp p)
+ and hash_derecurs_field = function
+   | (p, Some e) -> 1 + 17 * hash_derecurs p + 257 * hash_derecurs e
+   | (p, None) -> 2 + 17 * hash_derecurs p
+ and hash_derecurs_regexp = function
+   | PEpsilon ->
+   | PElem p ->
++ 17 * (hash_derecurs p)
+   | PSeq (p1,p2) ->
++ 17 * (hash_derecurs_regexp p1) + 257 * (hash_derecurs_regexp p2)
+   | PAlt (p1,p2) ->
++ 17 * (hash_derecurs_regexp p1) + 257 * (hash_derecurs_regexp p2)
+   | PStar p ->
++ 17 * (hash_derecurs_regexp p)
+   | PWeakStar p ->
++ 17 * (hash_derecurs_regexp p)
+   | PGuard p ->
++ 17 * (hash_derecurs p)
+ let rec equal_derecurs p1 p2 = (p1 == p2) || match p1,p2 with
+   | PAlias s1, PAlias s2 ->
+       s1 == s2
+   | PType t1, PType t2 ->
+       Types.equal t1 t2
+   | POr (p1,q1), POr (p2,q2)
+   | PAnd (p1,q1), PAnd (p2,q2)
+   | PDiff (p1,q1), PDiff (p2,q2)
+   | PTimes (p1,q1), PTimes (p2,q2)
+   | PXml (p1,q1), PXml (p2,q2)
+   | PArrow (p1,q1), PArrow (p2,q2) ->
+       (equal_derecurs p1 p2) && (equal_derecurs q1 q2)
+   | POptional p1, POptional p2 ->
+       equal_derecurs p1 p2
+   | PRecord (o1,r1), PRecord (o2,r2) ->
+       (o1 == o2) && (LabelMap.equal equal_derecurs_field r1 r2)
+   | PCapture x1, PCapture x2 ->
+       Id.equal x1 x2
+   | PConstant (x1,c1), PConstant (x2,c2) ->
+       (Id.equal x1 x2) && (Types.Const.equal c1 c2)
+   | PRegexp p1, PRegexp p2 ->
+       equal_derecurs_regexp p1 p2
+   | _ -> false
+ and equal_derecurs_field r1 r2 = match (r1,r2) with
+   | (p1,None),(p2,None) -> equal_derecurs p1 p2
+   | (p1, Some e1), (p2, Some e2) -> equal_derecurs p1 p2 && equal_derecurs e1 e2
+   | _ -> false
+ and equal_derecurs_regexp r1 r2 = match r1,r2 with
+   | PEpsilon, PEpsilon ->
+       true
+   | PElem p1, PElem p2 ->
+       equal_derecurs p1 p2
+   | PGuard p1, PGuard p2 ->
+       equal_derecurs p1 p2
+   | PSeq (p1,q1), PSeq (p2,q2)
+   | PAlt (p1,q1), PAlt (p2,q2) ->
+       (equal_derecurs_regexp p1 p2) && (equal_derecurs_regexp q1 q2)
+   | PStar p1, PStar p2
+   | PWeakStar p1, PWeakStar p2 ->
+       equal_derecurs_regexp p1 p2
+   | _ -> false
+ module DerecursTable = Hashtbl.Make(
+   struct
+     type t = derecurs
+     let hash = hash_derecurs
+     let equal = equal_derecurs
+   end
        )
-   | Recurs (t, b) -> compile (compile_many env b) t
-   | Regexp (r,q) -> compile env (Regexp.compile r q)
-   | Internal t -> cons loc (`Type t)
-   | Or (t1,t2) -> cons loc (`Or (compile env t1, compile env t2))
-   | And (t1,t2,e) -> cons loc (`And (compile env t1, compile env t2,e))
-   | Diff (t1,t2) -> cons loc (`Diff (compile env t1, compile env t2))
-   | Prod (t1,t2) -> cons loc (`Times (compile env t1, compile env t2))
-   | Arrow (t1,t2) -> cons loc (`Arrow (compile env t1, compile env t2))
-   | Record (l,o,t) -> cons loc (`Record (l,o,compile env t))
-   | Constant (x,v) -> cons loc (`Constant (x,v))
-   | Capture x -> cons loc (`Capture x)
- and compile_many env b =
-   let b = List.map (fun (v,t) -> (v,t,mk' t.loc)) b in
-   let env =
-     List.fold_left (fun env (v,t,x) -> StringMap.add v x env) env b in
-   List.iter (fun (v,t,x) -> x.descr' <- `Alias (v, compile env t)) b;
-   env
+ let gen = ref 0
+ let rank = ref 0
- let comp_fv_seen = ref []
+ let rec hash_descr = function
- let comp_fv_res = ref []
+   | IDummy -> assert false
- let rec comp_fv s =
+   | IType x -> Types.hash x
-   if List.memq s !comp_fv_seen then ()
+   | IOr (d1,d2) -> 1 + 17 * (hash_descr d1) + 257 * (hash_descr d2)
+   | IAnd (d1,d2) -> 2 + 17 * (hash_descr d1) + 257 * (hash_descr d2)
+   | IDiff (d1,d2) -> 3 + 17 * (hash_descr d1) + 257 * (hash_descr d2)
+   | IOptional d -> 4 + 17 * (hash_descr d)
+   | ITimes (s1,s2) -> 5 + 17 * (hash_slot s1) + 257 * (hash_slot s2)
+   | IXml (s1,s2) -> 6 + 17 * (hash_slot s1) + 257 * (hash_slot s2)
+   | IArrow (s1,s2) -> 7 + 17 * (hash_slot s1) + 257 * (hash_slot s2)
+   | IRecord (o,r) -> (if o then 8 else 9) + 17 * (LabelMap.hash hash_descr_field r)
+   | ICapture x -> 10 + 17 * (Id.hash x)
+   | IConstant (x,y) -> 11 + 17 * (Id.hash x) + 257 * (Types.Const.hash y)
+ and hash_descr_field = function
+   | (d, Some e) -> 1 + 17 * hash_slot d + 257 * hash_descr e
+   | (d, None) -> 2 + 17 * hash_slot d
+ and hash_slot s =
+   if s.gen1 = !gen then 13 * s.rank1
    else (
-     comp_fv_seen := s :: !comp_fv_seen;
+     incr rank;
-     (match s.descr' with
+     s.rank1 <- !rank; s.gen1 <- !gen;
-       | `Alias (_,x) -> comp_fv x
+     hash_descr s.d
-       | `Or (s1,s2)
-       | `And (s1,s2,_)
-       | `Diff (s1,s2)
-       | `Times (s1,s2)
-       | `Arrow (s1,s2) -> comp_fv s1; comp_fv s2
-       | `Record (l,opt,s) -> comp_fv s
-       | `Type _ -> ()
-       | `Capture x
-       | `Constant (x,_) -> comp_fv_res := x :: !comp_fv_res);
-     if (!comp_fv_res = []) then s.fv <- Some [];
-     (* TODO: check that the above line is correct *)
    )
+ let rec equal_descr d1 d2 =
+   match (d1,d2) with
+   | IType x1, IType x2 -> Types.equal x1 x2
+   | IOr (x1,y1), IOr (x2,y2)
+   | IAnd (x1,y1), IAnd (x2,y2)
+   | IDiff (x1,y1), IDiff (x2,y2) -> (equal_descr x1 x2) && (equal_descr y1 y2)
+   | IOptional x1, IOptional x2 -> equal_descr x1 x2
+   | ITimes (x1,y1), ITimes (x2,y2)
+   | IXml (x1,y1), IXml (x2,y2)
+   | IArrow (x1,y1), IArrow (x2,y2) -> (equal_slot x1 x2) && (equal_slot y1 y2)
+   | IRecord (o1,r1), IRecord (o2,r2) ->
+       (o1 = o2) && (LabelMap.equal equal_descr_field r1 r2)
+   | ICapture x1, ICapture x2 -> Id.equal x1 x2
+   | IConstant (x1,y1), IConstant (x2,y2) ->
+       (Id.equal x1 x2) && (Types.Const.equal y1 y2)
+   | _ -> false
+ and equal_descr_field d1 d2 = match (d1,d2) with
+   | (d1,None),(d2,None) -> equal_slot d1 d2
+   | (d1, Some e1), (d2, Some e2) -> equal_slot d1 d2 && equal_descr e1 e2
+   | _ -> false
+ and equal_slot s1 s2 =
+   ((s1.gen1 = !gen) && (s2.gen2 = !gen) && (s1.rank1 = s2.rank2))
+   ||
+   ((s1.gen1 <> !gen) && (s2.gen2 <> !gen) && (
+      incr rank;
+      s1.rank1 <- !rank; s1.gen1 <- !gen;
+      s2.rank2 <- !rank; s2.gen2 <- !gen;
+      equal_descr s1.d s2.d
+    ))
+ module SlotTable = Hashtbl.Make(
+   struct
+     type t = slot
+     let hash s =
+       match s.hash with
+         | Some h -> h
+         | None ->
+             incr gen; rank := 0;
+             let h = hash_slot s in
+             s.hash <- Some h;
+             h
+     let equal s1 s2 =
+       (s1 == s2) ||
+       (incr gen; rank := 0;
+        let e = equal_slot s1 s2 in
+        (*     if e then Printf.eprintf "Recursive hash-consing: Equal\n";  *)
+        e)
+   end)
+ let pempty = PType Types.empty
+ let por p1 p2 =
+   if p1 == pempty then p2 else
+     if p2 == pempty then p1 else
+       POr (p1,p2)
+ let pand p1 p2 =
+   if (p1 == pempty) || (p2 == pempty) then pempty else PAnd (p1,p2)
+ let rec remove_regexp r q = match r with
+   | PEpsilon ->
+       q
+   | PElem p ->
+       PTimes (p, q)
+   | PGuard p ->
+       pand p q
+   | PSeq (r1,r2) ->
+       remove_regexp r1 (remove_regexp r2 q)
+   | PAlt (r1,r2) ->
+       por (remove_regexp r1 q) (remove_regexp r2 q)
+   | PStar r ->
+       let x = mk_derecurs_slot noloc in
+       let res = POr (PAlias x, q) in
+       x.pdescr <- remove_regexp2 r res pempty;
+       res
+   | PWeakStar r ->
+       let x = mk_derecurs_slot noloc in
+       let res = POr (q, PAlias x) in
+       x.pdescr <- remove_regexp2 r res pempty;
+       res
+ and remove_regexp2 r q_nonempty q_empty =
+   if q_nonempty == q_empty then remove_regexp r q_empty
+   else match r with
+     | PEpsilon ->
+         q_empty
+     | PElem p ->
+         PTimes (p, q_nonempty)
+     | PGuard p ->
+         pand p q_empty
+     | PSeq (r1,r2) ->
+         remove_regexp2 r1
+         (remove_regexp2 r2 q_nonempty q_nonempty)
+         (remove_regexp2 r2 q_nonempty q_empty)
+     | PAlt (r1,r2) ->
+         por
+         (remove_regexp2 r1 q_nonempty q_empty)
+         (remove_regexp2 r2 q_nonempty q_empty)
+     | PStar r ->
+         let x = mk_derecurs_slot noloc in
+         x.pdescr <- remove_regexp2 r (POr (PAlias x, q_nonempty)) pempty;
+         por (PAlias x) q_empty
+     | PWeakStar r ->
+         let x = mk_derecurs_slot noloc in
+         x.pdescr <- remove_regexp2 r (POr (q_nonempty, PAlias x)) pempty;
+         por q_empty (PAlias x)
+ let cst_nil = Types.Atom Sequence.nil_atom
+ let capture_all vars p = IdSet.fold (fun p x -> PAnd (p, PCapture x)) p vars
+ let termin b vars p =
+   if b then p
+   else IdSet.fold (fun p x -> PSeq (p, PGuard (PConstant (x,cst_nil)))) p vars
+ let rec derecurs env p = match p.descr with
+   | PatVar v -> derecurs_var env p.loc v
+   | SchemaVar (kind, schema_name, component_name) ->
+       PType (find_schema_descr env.penv_tenv kind schema_name component_name)
+   | Recurs (p,b) -> derecurs (derecurs_def env b) p
+   | Internal t -> PType t
+   | NsT ns -> PType (Types.atom (Atoms.any_in_ns (parse_ns env.penv_tenv p.loc ns)))
+   | Or (p1,p2) -> POr (derecurs env p1, derecurs env p2)
+   | And (p1,p2) -> PAnd (derecurs env p1, derecurs env p2)
+   | Diff (p1,p2) -> PDiff (derecurs env p1, derecurs env p2)
+   | Prod (p1,p2) -> PTimes (derecurs env p1, derecurs env p2)
+   | XmlT (p1,p2) -> PXml (derecurs env p1, derecurs env p2)
+   | Arrow (p1,p2) -> PArrow (derecurs env p1, derecurs env p2)
+   | Optional p -> POptional (derecurs env p)
+   | Record (o,r) ->
+       let aux = function
+         | (p,Some e) -> (derecurs env p, Some (derecurs env e))
+         | (p,None) -> derecurs env p, None in
+       PRecord (o, parse_record env.penv_tenv p.loc aux r)
+   | Constant (x,c) -> PConstant (x,const env.penv_tenv p.loc c)
+   | Cst c -> PType (Types.constant (const env.penv_tenv p.loc c))
+   | Regexp r ->
+       let r,_ = derecurs_regexp IdSet.empty false IdSet.empty true env r in
+       PRegexp r
+         (* Note: computing remove_regexp here is slower (because
+            of caching ?) *)
+ and derecurs_regexp vars b rvars f env = function
+ (* - vars: seq variables to be propagated top-down and added
+      to each captured element
+    - b: below a star ?
+    - rvars: seq variables that appear on the right of the regexp
+    - f: tail position
+   returns the set of seq variable of the regexp minus rvars
+   (they have already been terminated if not below a star)
+ *)
+   | Epsilon ->
+       PEpsilon, IdSet.empty
+   | Elem p ->
+       PElem (capture_all vars (derecurs env p)), IdSet.empty
+   | Guard p ->
+       PGuard (derecurs env p), IdSet.empty
+   | Seq (p1,p2) ->
+       let (p2,v2) = derecurs_regexp vars b rvars f env p2 in
+       let (p1,v1) = derecurs_regexp vars b (IdSet.cup rvars v2) false env p1 in
+       PSeq (p1,p2), IdSet.cup v1 v2
+   | Alt (p1,p2) ->
+       let (p1,v1) = derecurs_regexp vars b rvars f env p1
+       and (p2,v2) = derecurs_regexp vars b rvars f env p2 in
+       PAlt (termin b (IdSet.diff v2 v1) p1, termin b (IdSet.diff v1 v2) p2),
+       IdSet.cup v1 v2
+   | Star p ->
+       let (p,v) = derecurs_regexp vars true rvars false env p in
+       termin b v (PStar p), v
+   | WeakStar p ->
+       let (p,v) = derecurs_regexp vars true rvars false env p in
+       termin b v (PWeakStar p), v
+   | SeqCapture (x,p) ->
+       let vars = if f then vars else IdSet.add x vars in
+       let after = IdSet.mem rvars x in
+       let rvars = IdSet.add x rvars in
+       let (p,v) = derecurs_regexp vars b rvars false env p in
+       (if f
+        then PSeq (PGuard (PCapture x), p)
+        else termin (after || b) (IdSet.singleton x) p),
+       (if after then v else IdSet.add x v)
+ and derecurs_var env loc v =
+   match Ns.split_qname v with
+     | "", v ->
+         let v = ident v in
+         (try PAlias (Env.find v env.penv_derec)
+          with Not_found ->
+            try PType (find_type v env.penv_tenv)
+            with Not_found -> PCapture v)
+     | cu, v ->
+         try
+           let cu = U.mk cu in
+           PType (find_type_global loc cu (ident v) env.penv_tenv)
+         with Not_found ->
+           raise_loc_generic loc
+           ("Unbound external type " ^ cu ^ ":" ^ (U.to_string v))
- let fv s =
+ and derecurs_def env b =
+   let b = List.map (fun (v,p) -> (v,p,mk_derecurs_slot p.loc)) b in
+   let n =
+     List.fold_left (fun env (v,p,s) -> Env.add v s env) env.penv_derec b in
+   let env = { env with penv_derec = n } in
+   List.iter (fun (v,p,s) -> s.pdescr <- derecurs env p) b;
+   env
+ let rec fv_slot s =
    match s.fv with
-     | Some l -> l
+     | Some x -> x
      | None ->
-         comp_fv s;
+         if s.gen1 = !gen then IdSet.empty
-         let l = SortedList.from_list !comp_fv_res in
+         else (s.gen1 <- !gen; fv_descr s.d)
-         comp_fv_res := [];
+ and fv_descr = function
-         comp_fv_seen := [];
+   | IDummy -> assert false
-         s.fv <- Some l;
+   | IType _ -> IdSet.empty
-         l
+   | IOr (d1,d2)
+   | IAnd (d1,d2)
- let rec typ seen s : Types.descr =
+   | IDiff (d1,d2) -> IdSet.cup (fv_descr d1) (fv_descr d2)
-   match s.descr' with
+   | IOptional d -> fv_descr d
-     | `Alias (v,x) ->
+   | ITimes (s1,s2)
-         if List.memq s seen then
+   | IXml (s1,s2)
-           raise_loc s.loc'
+   | IArrow (s1,s2) -> IdSet.cup (fv_slot s1) (fv_slot s2)
-             (Pattern
+   | IRecord (o,r) ->
-                ("Unguarded recursion on variable " ^ v ^ " in this type"))
+       List.fold_left IdSet.cup IdSet.empty (LabelMap.map_to_list fv_field r)
-         else typ (s :: seen) x
+   | ICapture x | IConstant (x,_) -> IdSet.singleton x
-     | `Type t -> t
+ and fv_field = function
-     | `Or (s1,s2) -> Types.cup (typ seen s1) (typ seen s2)
+   | (d,Some e) -> IdSet.cup (fv_slot d) (fv_descr e)
-     | `And (s1,s2,_) ->  Types.cap (typ seen s1) (typ seen s2)
+   | (d,None) -> fv_slot d
-     | `Diff (s1,s2) -> Types.diff (typ seen s1) (typ seen s2)
-     | `Times (s1,s2) -> Types.times (typ_node s1) (typ_node s2)
-     | `Arrow (s1,s2) -> Types.arrow (typ_node s1) (typ_node s2)
-     | `Record (l,o,s) -> Types.record l o (typ_node s)
-     | `Capture _ | `Constant _ -> assert false
- and typ_node s : Types.node =
-   match s.type_node with
+ let compute_fv s =
-     | Some x -> x
+   match s.fv with
+     | Some x -> ()
      | None ->
-         let x = Types.make () in
+         incr gen;
-         s.type_node <- Some x;
+         let x = fv_slot s in
-         let t = typ [] s in
+         s.fv <- Some x
-         Types.define x t;
-         x
+ let check_no_capture loc s =
+   match IdSet.pick s with
+     | Some x ->
+         raise_loc_generic loc ("Capture variable not allowed: " ^ (Ident.to_string x))
+     | None -> ()
- let type_node s =
+ let compile_slot_hash = DerecursTable.create 67
-   let s = typ_node s in
+ let compile_hash = DerecursTable.create 67
-   let s = Types.internalize s in
- (*  Types.define s (Types.normalize (Types.descr s)); *)
+ let todo_defs = ref []
+ let todo_fv = ref []
+ let rec compile p =
+   try DerecursTable.find compile_hash p
+   with Not_found ->
+     let c = real_compile p in
+     DerecursTable.replace compile_hash p c;
+     c
+ and real_compile = function
+   | PDummy -> assert false
+   | PAlias v ->
+       if v.ploop then
+         raise_loc_generic v.ploc ("Unguarded recursion on type/pattern");
+       v.ploop <- true;
+       let r = compile v.pdescr in
+       v.ploop <- false;
+       r
+   | PType t -> IType t
+   | POr (t1,t2) -> IOr (compile t1, compile t2)
+   | PAnd (t1,t2) -> IAnd (compile t1, compile t2)
+   | PDiff (t1,t2) -> IDiff (compile t1, compile t2)
+   | PTimes (t1,t2) -> ITimes (compile_slot t1, compile_slot t2)
+   | PXml (t1,t2) -> IXml (compile_slot t1, compile_slot t2)
+   | PArrow (t1,t2) -> IArrow (compile_slot t1, compile_slot t2)
+   | POptional t -> IOptional (compile t)
+   | PRecord (o,r) ->  IRecord (o, LabelMap.map compile_field r)
+   | PConstant (x,v) -> IConstant (x,v)
+   | PCapture x -> ICapture x
+   | PRegexp r -> compile (remove_regexp r (PType Sequence.nil_type))
+ and compile_field = function
+   | (p, Some e) -> (compile_slot p, Some (compile e))
+   | (p, None) -> (compile_slot p, None)
+ and compile_slot p =
+   try DerecursTable.find compile_slot_hash p
+   with Not_found ->
+     let s = mk_slot () in
+     todo_defs := (s,p) :: !todo_defs;
+     todo_fv := s :: !todo_fv;
+     DerecursTable.add compile_slot_hash p s;
    s
- let rec pat seen s : Patterns.descr =
-   if fv s = [] then Patterns.constr (type_node s) else
+ let timer_fv = Stats.Timer.create "Typer.fv"
-   match s.descr' with
+ let rec flush_defs () =
-     | `Alias (v,x) ->
+   match !todo_defs with
-         if List.memq s seen then
+     | [] ->
-           raise_loc s.loc'
+         Stats.Timer.start timer_fv;
-             (Pattern
+         List.iter compute_fv !todo_fv;
-                ("Unguarded recursion on variable " ^ v ^ " in this pattern"))
+         todo_fv := [];
-         else pat (s :: seen) x
+         Stats.Timer.stop timer_fv ()
-     | `Or (s1,s2) -> Patterns.cup (pat seen s1) (pat seen s2)
+     | (s,p)::t ->
-     | `And (s1,s2,e) -> Patterns.cap (pat seen s1) (pat seen s2) e
+         todo_defs := t;
-     | `Diff (s1,s2) when fv s2 = [] ->
+         s.d <- compile p;
-         let s2 = Types.cons (Types.neg (Types.descr (type_node s2)))in
+         flush_defs ()
-         Patterns.cap (pat seen s1) (Patterns.constr s2) true
-     | `Diff _ ->
+ let typ_nodes = SlotTable.create 67
-         raise_loc s.loc' (Pattern "Difference not allowed in patterns")
+ let pat_nodes = SlotTable.create 67
-     | `Times (s1,s2) -> Patterns.times (pat_node s1) (pat_node s2)
-     | `Record (l,false,s) -> Patterns.record l (pat_node s)
+ let rec typ = function
-     | `Record _ ->
+   | IType t -> t
-         raise_loc s.loc'
+   | IOr (s1,s2) -> Types.cup (typ s1) (typ s2)
-           (Pattern "Optional field not allowed in record patterns")
+   | IAnd (s1,s2) ->  Types.cap (typ s1) (typ s2)
-     | `Capture x ->  Patterns.capture x
+   | IDiff (s1,s2) -> Types.diff (typ s1) (typ s2)
-     | `Constant (x,c) -> Patterns.constant x c
+   | ITimes (s1,s2) -> Types.times (typ_node s1) (typ_node s2)
-     | `Arrow _ ->
+   | IXml (s1,s2) -> Types.xml (typ_node s1) (typ_node s2)
-         raise_loc s.loc' (Pattern "Arrow not allowed in patterns")
+   | IArrow (s1,s2) -> Types.arrow (typ_node s1) (typ_node s2)
-     | `Type _ -> assert false
+   | IOptional s -> Types.Record.or_absent (typ s)
+   | IRecord (o,r) ->  Types.record' (o, LabelMap.map typ_field r)
+   | IDummy | ICapture _ | IConstant (_,_) -> assert false
+ and typ_field = function
+   | (s, None) -> typ_node s
+   | (s, Some _) ->
+       raise (Patterns.Error "Or-else clauses are not allowed in types")
+ and typ_node s : Types.Node.t =
+   try SlotTable.find typ_nodes s
+   with Not_found ->
+     let x = Types.make () in
+     SlotTable.add typ_nodes s x;
+     Types.define x (typ s.d);
+     x
+ let rec pat d : Patterns.descr =
+   if IdSet.is_empty (fv_descr d)
+   then Patterns.constr (typ d)
+   else pat_aux d
+ and pat_aux = function
+   | IDummy -> assert false
+   | IOr (s1,s2) -> Patterns.cup (pat s1) (pat s2)
+   | IAnd (s1,s2) -> Patterns.cap (pat s1) (pat s2)
+   | IDiff (s1,s2) when IdSet.is_empty (fv_descr s2) ->
+       let s2 = Types.neg (typ s2) in
+       Patterns.cap (pat s1) (Patterns.constr s2)
+   | IDiff _ ->
+       raise (Patterns.Error "Differences are not allowed in patterns")
+   | ITimes (s1,s2) -> Patterns.times (pat_node s1) (pat_node s2)
+   | IXml (s1,s2) -> Patterns.xml (pat_node s1) (pat_node s2)
+   | IOptional _ ->
+       raise (Patterns.Error "Optional fields are not allowed in record patterns")
+   | IRecord (o,r) ->
+       let pats = ref [] in
+       let aux l = function
+         | (s,None) ->
+             if IdSet.is_empty (fv_slot s) then typ_node s
+             else
+               ( pats := Patterns.record l (pat_node s) :: !pats;
+                 Types.any_node )
+         | (s,Some e) ->
+             if IdSet.is_empty (fv_slot s) then
+               raise (Patterns.Error "Or-else clauses are not allowed in types")
+             else
+               ( pats := Patterns.cup
+                   (Patterns.record l (pat_node s))
+                   (pat e) :: !pats;
+                 Types.Record.any_or_absent_node )
+       in
+       let constr = Types.record' (o,LabelMap.mapi aux r) in
+       List.fold_left Patterns.cap (Patterns.constr constr) !pats
+         (* TODO: can avoid constr when o=true, and all fields have fv *)
+   | ICapture x -> Patterns.capture x
+   | IConstant (x,c) -> Patterns.constant x c
+   | IArrow _ ->
+       raise (Patterns.Error "Arrows are not allowed in patterns")
+   | IType _ -> assert false
  and pat_node s : Patterns.node =
-   match s.pat_node with
+   try SlotTable.find pat_nodes s
-     | Some x -> x
+   with Not_found ->
-     | None ->
+     let x = Patterns.make (fv_slot s) in
-         let x = Patterns.make (fv s) in
+     try
-         s.pat_node <- Some x;
+       SlotTable.add pat_nodes s x;
-         let t = pat [] s in
+       Patterns.define x (pat s.d);
-         Patterns.define x t;
          x
+     with exn -> SlotTable.remove pat_nodes s; raise exn
+       (* For the toplevel ... *)
- let global_types = ref StringMap.empty
- let mk_typ e =
+ module Ids = Set.Make(Id)
-   if fv e = [] then type_node e
+ let type_defs env b =
-   else raise_loc e.loc' (Pattern "Capture variables are not allowed in types")
+   ignore
+     (List.fold_left
+        (fun seen (v,p) ->
- let typ e =
+           if Ids.mem v seen then
-   mk_typ (compile !global_types e)
+             raise_loc_generic p.loc
+               ("Multiple definitions for the type identifer " ^
- let pat e =
+                (Ident.to_string v));
-   let e = compile !global_types e in
+           Ids.add v seen
-   pat_node e
+        ) Ids.empty b);
- let register_global_types b =
+   let penv = derecurs_def (penv env) b in
-   let env = compile_many !global_types b in
+   let b = List.map (fun (v,p) -> (v,p,compile (derecurs penv p))) b in
-   List.iter (fun (v,_) ->
+   flush_defs ();
-                let d = Types.descr (mk_typ (StringMap.find v env)) in
+   let b =
- (*             let d = Types.normalize d in*)
+     List.map
-                Types.Print.register_global v d;
+       (fun (v,p,s) ->
-                ()
+          check_no_capture p.loc (fv_descr s);
-             ) b;
+          let t = typ s in
-   global_types := env
+          if (p.loc <> noloc) && (Types.is_empty t) then
+            warning p.loc
+              ("This definition yields an empty type for " ^ (Ident.to_string v));
+          (v,t)) b in
+   List.iter (fun (v,t) -> Types.Print.register_global (Id.value v) t) b;
+   b
+ let dump_types ppf env =
+   Env.iter (fun v ->
+               function
+                   (Type _) -> Format.fprintf ppf " %a" Ident.print v
+                 | _ -> ()) env.ids
+ let dump_type ppf env name =
+   try
+     (match Env.find (Ident.ident name) env.ids with
+     | Type t -> Types.Print.print ppf t
+     | _ -> raise Not_found)
+   with Not_found ->
+     raise (Error (Printf.sprintf "Type %s not found" (U.get_str name)))
+ let dump_schema_type ppf env (k, s, n) =
+   let uri = find_schema s env in
+   let descr = find_schema_descr_uri k uri n in
+   Types.Print.print ppf descr
+ let dump_ns ppf env =
+   Ns.dump_table ppf env.ns
+ let do_typ loc r =
+   let s = compile_slot r in
+   flush_defs ();
+   check_no_capture loc (fv_slot s);
+   typ_node s
+ let typ env p =
+   do_typ p.loc (derecurs (penv env) p)
+ let pat env p =
+   let s = compile_slot (derecurs (penv env) p) in
+   flush_defs ();
+   try pat_node s
+   with Patterns.Error e -> raise_loc_generic p.loc e
+     | Location (loc,_,exn) when loc = noloc -> raise (Location (p.loc, `Full, exn))
  (* II. Build skeleton *)
- module Fv = StringSet
- let rec expr { loc = loc; descr = d } =
+ type type_fun = Types.t -> bool -> Types.t
-   let (fv,td) =
-     match d with
+ module Fv = IdSet
-       | DebugTyper t -> (Fv.empty, Typed.DebugTyper (typ t))
+ type branch = Branch of Typed.branch * branch list
+ let cur_branch : branch list ref = ref []
+ let exp loc fv e =
+   fv,
+   { Typed.exp_loc = loc;
+     Typed.exp_typ = Types.empty;
+     Typed.exp_descr = e;
+   }
+ let ops = Hashtbl.create 13
+ let register_op op arity f = Hashtbl.add ops op (arity,f)
+ let typ_op op = snd (Hashtbl.find ops op)
+ let is_op env s =
+   if (Env.mem (ident s) env.ids) then None
+   else
+     try let s = U.get_str s in Some (s, fst (Hashtbl.find ops s))
+     with Not_found -> None
+ let rec expr env loc = function
+   | LocatedExpr (loc,e) -> expr env loc e
        | Forget (e,t) ->
-           let (fv,e) = expr e and t = typ t in
+       let (fv,e) = expr env loc e and t = typ env t in
-           (fv, Typed.Forget (e,t))
+       exp loc fv (Typed.Forget (e,t))
-       | Var s -> (Fv.singleton s, Typed.Var s)
+   | Check (e,t) ->
+       let (fv,e) = expr env loc e and t = typ env t in
+       exp loc fv (Typed.Check (ref Types.empty,e,t))
+   | Var s -> var env loc s
        | Apply (e1,e2) ->
-           let (fv1,e1) = expr e1 and (fv2,e2) = expr e2 in
+       let (fv1,e1) = expr env loc e1 and (fv2,e2) = expr env loc e2 in
-           (Fv.union fv1 fv2, Typed.Apply (e1,e2))
+       let fv = Fv.cup fv1 fv2 in
-       | Abstraction a ->
+       (match e1.Typed.exp_descr with
-           let iface = List.map (fun (t1,t2) -> (typ t1, typ t2)) a.fun_iface in
+          | Typed.Op (op,arity,args) when arity > 0 ->
-           let t = List.fold_left
+              exp loc fv (Typed.Op (op,arity - 1,args @ [e2]))
+          | _ ->
+              exp loc fv (Typed.Apply (e1,e2)))
+   | Abstraction a -> abstraction env loc a
+   | (Integer _ | Char _ | Atom _ | Const _) as c ->
+       exp loc Fv.empty (Typed.Cst (const env loc c))
+   | Pair (e1,e2) ->
+       let (fv1,e1) = expr env loc e1 and (fv2,e2) = expr env loc e2 in
+       exp loc (Fv.cup fv1 fv2) (Typed.Pair (e1,e2))
+   | Xml (e1,e2) ->
+       let (fv1,e1) = expr env loc e1 and (fv2,e2) = expr env loc e2 in
+       exp loc (Fv.cup fv1 fv2) (Typed.Xml (e1,e2))
+   | Dot (e,l) ->
+       let (fv,e) = expr env loc e in
+       exp loc fv (Typed.Dot (e,parse_label env loc l))
+   | RemoveField (e,l) ->
+       let (fv,e) = expr env loc e in
+       exp loc fv (Typed.RemoveField (e,parse_label env loc l))
+   | RecordLitt r ->
+       let fv = ref Fv.empty in
+       let r = parse_record env loc
+                 (fun e ->
+                    let (fv2,e) = expr env loc e
+                    in fv := Fv.cup !fv fv2; e)
+                 r in
+       exp loc !fv (Typed.RecordLitt r)
+   | String (i,j,s,e) ->
+       let (fv,e) = expr env loc e in
+       exp loc fv (Typed.String (i,j,s,e))
+   | Match (e,b) ->
+       let (fv1,e) = expr env loc e
+       and (fv2,b) = branches env b in
+       exp loc (Fv.cup fv1 fv2) (Typed.Match (e, b))
+   | Map (e,b) ->
+       let (fv1,e) = expr env loc e
+       and (fv2,b) = branches env b in
+       exp loc (Fv.cup fv1 fv2) (Typed.Map (e, b))
+   | Transform (e,b) ->
+       let (fv1,e) = expr env loc e
+       and (fv2,b) = branches env b in
+       exp loc (Fv.cup fv1 fv2) (Typed.Transform (e, b))
+   | Xtrans (e,b) ->
+       let (fv1,e) = expr env loc e
+       and (fv2,b) = branches env b in
+       exp loc (Fv.cup fv1 fv2) (Typed.Xtrans (e, b))
+   | Validate (e,kind,schema,elt) ->
+       let (fv,e) = expr env loc e in
+       let uri = find_schema schema env in
+       exp loc fv (Typed.Validate (e, kind, uri, elt))
+   | Try (e,b) ->
+       let (fv1,e) = expr env loc e
+       and (fv2,b) = branches env b in
+       exp loc (Fv.cup fv1 fv2) (Typed.Try (e, b))
+   | NamespaceIn (pr,ns,e) ->
+       let env = enter_ns pr ns env in
+       expr env loc e
+   | Ref (e,t) ->
+       let (fv,e) = expr env loc e and t = typ env t in
+       exp loc fv (Typed.Ref (e,t))
+   | External (s,args) ->
+       extern loc env s args
+ and extern loc env s args =
+   let args = List.map (typ env) args in
+   try
+     let (i,t) = Externals.resolve s args in
+     exp loc Fv.empty (Typed.External (t,i))
+   with exn -> raise_loc loc exn
+ and var env loc s =
+   match is_op env s with
+     | Some (s,arity) ->
+         let need_ns = s = "print_xml" || s = "print_xml_utf8" in
+         let e = Typed.Op (s, arity, []) in
+         let e = if need_ns then Typed.NsTable (env.ns,e) else e in
+         exp loc Fv.empty e
+     | None ->
+         match Ns.split_qname s with
+           | "", id ->
+               let s = U.get_str id in
+               if String.contains s '.' then
+                 extern loc env s []
+               else
+                 let id = ident id in
+                 (try ignore (find_value id env)
+                  with Not_found -> raise_loc loc (UnboundId (id, Env.mem id env.ids)));
+           exp loc (Fv.singleton id) (Typed.Var id)
+           | cu, id ->
+               let cu = find_cu (U.mk cu) env in
+               let id = ident id in
+               let t =
+                 try find_value_global cu id env
+                 with Not_found ->
+                   raise_loc loc (UnboundExtId (cu,id) ) in
+               exp loc Fv.empty (Typed.ExtVar (cu, id, t))
+ and abstraction env loc a =
+   let iface =
+     List.map
+       (fun (t1,t2) -> (typ env t1, typ env t2)) a.fun_iface in
+   let t =
+     List.fold_left
                      (fun accu (t1,t2) -> Types.cap accu (Types.arrow t1 t2))
                      Types.any iface in
-           let iface = List.map
+   let iface =
+     List.map
                          (fun (t1,t2) -> (Types.descr t1, Types.descr t2))
                          iface in
-           let (fv0,body) = branches a.fun_body in
+   let env' =
+     match a.fun_name with
+       | None -> env
+       | Some f -> enter_values_dummy [ f ] env
+   in
+   let (fv0,body) = branches env' a.fun_body in
            let fv = match a.fun_name with
              | None -> fv0
              | Some f -> Fv.remove f fv0 in
-           (fv,
+   let e = Typed.Abstraction
-            Typed.Abstraction
               { Typed.fun_name = a.fun_name;
                 Typed.fun_iface = iface;
                 Typed.fun_body = body;
                 Typed.fun_typ = t;
-                Typed.fun_fv = Fv.elements fv
+               Typed.fun_fv = fv
-              }
+             } in
-           )
+   exp loc fv e
-       | Cst c -> (Fv.empty, Typed.Cst c)
-       | Pair (e1,e2) ->
-           let (fv1,e1) = expr e1 and (fv2,e2) = expr e2 in
-           (Fv.union fv1 fv2, Typed.Pair (e1,e2))
-       | Dot (e,l) ->
-           let (fv,e) = expr e in
-           (fv,  Typed.Dot (e,l))
-       | RecordLitt r ->
-           let fv = ref Fv.empty in
-           let r  = List.sort (fun (l1,_) (l2,_) -> compare l1 l2) r in
-           let r = List.map
-                     (fun (l,e) ->
-                        let (fv2,e) = expr e in fv := Fv.union !fv fv2; (l,e))
-                     r in
-           let rec check = function
-             | (l1,_) :: (l2,_) :: _ when l1 = l2 ->
-                 raise_loc loc (MultipleLabel l1)
-             | _ :: rem -> check rem
-             | _ -> () in
-           check r;
-           (!fv, Typed.RecordLitt r)
-       | Op (op,le) ->
-           let (fvs,ltes) = List.split (List.map expr le) in
-           let fv = List.fold_left Fv.union Fv.empty fvs in
-           (fv, Typed.Op (op,ltes))
-       | Match (e,b) ->
-           let (fv1,e) = expr e
-           and (fv2,b) = branches b in
-           (Fv.union fv1 fv2, Typed.Match (e, b))
-       | Map (e,b) ->
-           let (fv1,e) = expr e
-           and (fv2,b) = branches b in
-           (Fv.union fv1 fv2, Typed.Map (e, b))
-       | Try (e,b) ->
-           let (fv1,e) = expr e
-           and (fv2,b) = branches b in
-           (Fv.union fv1 fv2, Typed.Try (e, b))
-   in
-   fv,
-   { Typed.exp_loc = loc;
-     Typed.exp_typ = Types.empty;
-     Typed.exp_descr = td;
-   }
-   and branches b =
+ and branches env b =
      let fv = ref Fv.empty in
      let accept = ref Types.empty in
-     let b = List.map
+   let branch (p,e) =
-               (fun (p,e) ->
+     let cur_br = !cur_branch in
-                  let (fv2,e) = expr e in
+     cur_branch := [];
-                  let p = pat p in
+     let p' = pat env p in
-                  let fv2 = List.fold_right Fv.remove (Patterns.fv p) fv2 in
+     let fvp = Patterns.fv p' in
-                  fv := Fv.union !fv fv2;
+     let env' = enter_values_dummy fvp env in
-                  accept := Types.cup !accept (Types.descr (Patterns.accept p));
+     let (fv2,e) = expr env' noloc e in
-                  { Typed.br_used = false;
+     let br_loc = merge_loc p.loc e.Typed.exp_loc in
-                    Typed.br_pat = p;
+     (match Fv.pick (Fv.diff fvp fv2) with
-                    Typed.br_body = e }
+        | None -> ()
-               ) b in
+        | Some x ->
+            let x = U.to_string (Id.value x) in
+            warning br_loc
+              ("The capture variable " ^ x ^
+               " is declared in the pattern but not used in the body of this branch. It might be a misspelled or undeclared type or name (if it isn't, use _ instead)."));
+     let fv2 = Fv.diff fv2 fvp in
+     fv := Fv.cup !fv fv2;
+     accept := Types.cup !accept (Types.descr (Patterns.accept p'));
+     let br =
+       {
+         Typed.br_loc = br_loc;
+         Typed.br_used = br_loc = noloc;
+         Typed.br_pat = p';
+         Typed.br_body = e } in
+     cur_branch := Branch (br, !cur_branch) :: cur_br;
+     br in
+   let b = List.map branch b in
      (!fv,
       {
         Typed.br_typ = Types.empty;
-Line 430
+Line 1122
       }
      )
- let let_decl p e =
+ let expr env e = snd (expr env noloc e)
-   let (_,e) = expr e in
-   { Typed.let_pat = pat p;
+ let let_decl env p e =
-     Typed.let_body = e;
+   { Typed.let_pat = pat env p;
+     Typed.let_body = expr env e;
      Typed.let_compiled = None }
- (* III. Type-checks *)
- module Env = StringMap
+ (* Hide global "typing/parsing" environment *)
- type env = Types.descr Env.t
+ (* III. Type-checks *)
  open Typed
- let warning loc msg =
+ let localize loc f x =
-   Format.fprintf Format.std_formatter
+   try f x
-     "Warning %a:@\n%s@\n" Location.print_loc loc msg
+   with
+     | (Error _ | Constraint (_,_)) as exn -> raise (Location.Location (loc,`Full,exn))
+     | Warning (s,t) -> warning loc s; t
+ let require loc t s =
+   if not (Types.subtype t s) then raise_loc loc (Constraint (t, s))
+ let verify loc t s =
+   require loc t s; t
+ let verify_noloc t s =
+   if not (Types.subtype t s) then raise (Constraint (t, s));
+   t
+ let check_str loc ofs t s =
+   if not (Types.subtype t s) then raise_loc_str loc ofs (Constraint (t, s));
+   t
- let check loc t s msg =
+ let should_have loc constr s =
-   if not (Types.subtype t s) then raise_loc loc (Constraint (t, s, msg))
+   raise_loc loc (ShouldHave (constr,s))
+ let should_have_str loc ofs constr s =
+   raise_loc_str loc ofs (ShouldHave (constr,s))
+ let flatten arg constr precise =
+   let constr' = Sequence.star
+                   (Sequence.approx (Types.cap Sequence.any constr)) in
+   let sconstr' = Sequence.star constr' in
+   let exact = Types.subtype constr' constr in
+   if exact then
+     let t = arg sconstr' precise in
+     if precise then Sequence.flatten t else constr
+   else
+     let t = arg sconstr' true in
+     verify_noloc (Sequence.flatten t) constr
  let rec type_check env e constr precise =
- (*  Format.fprintf Format.std_formatter "constr=%a precise=%b@\n"
-     Types.Print.print_descr constr precise;
- *)
    let d = type_check' e.exp_loc env e.exp_descr constr precise in
+   let d = if precise then d else constr in
    e.exp_typ <- Types.cup e.exp_typ d;
    d
-Line 462
+Line 1185
    | Forget (e,t) ->
        let t = Types.descr t in
        ignore (type_check env e t false);
-       t
+       verify loc t constr
+   | Check (t0,e,t) ->
+       let te = type_check env e Types.any true in
+       t0 := Types.cup !t0 te;
+       verify loc (Types.descr t) constr
    | Abstraction a ->
        let t =
          try Types.Arrow.check_strenghten a.fun_typ constr
          with Not_found ->
-           raise_loc loc
+           should_have loc constr
-           (ShouldHave
+             "but the interface of the abstraction is not compatible"
-              (constr, "but the interface of the abstraction is not compatible"))
        in
        let env = match a.fun_name with
          | None -> env
-         | Some f -> Env.add f a.fun_typ env in
+         | Some f -> enter_value f a.fun_typ env in
        List.iter
          (fun (t1,t2) ->
+            let acc = a.fun_body.br_accept in
+            if not (Types.subtype t1 acc) then
+              raise_loc loc (NonExhaustive (Types.diff t1 acc));
             ignore (type_check_branches loc env t1 a.fun_body t2 false)
          ) a.fun_iface;
        t
-Line 490
+Line 1221
        Types.cup te tb
    | Pair (e1,e2) ->
-       let rects = Types.Product.get constr in
+       type_check_pair loc env e1 e2 constr precise
-       if Types.Product.is_empty rects then
-         raise_loc loc (ShouldHave (constr,"but it is a pair."));
-       let pi1 = Types.Product.pi1 rects in
-       let t1 = type_check env e1 (Types.Product.pi1 rects)
+   | Xml (e1,e2) ->
-                  (precise || (Types.Product.need_second rects))in
+       type_check_pair ~kind:`XML loc env e1 e2 constr precise
-       let rects = Types.Product.restrict_1 rects t1 in
-       let t2 = type_check env e2 (Types.Product.pi2 rects) precise in
-       if precise then
-         Types.times (Types.cons t1) (Types.cons t2)
-       else
-         constr
    | RecordLitt r ->
-       let rconstr = Types.Record.get constr in
+       type_record loc env r constr precise
-       if Types.Record.is_empty rconstr then
-         raise_loc loc (ShouldHave (constr,"but it is a record."));
-       let (rconstr,res) =
-         List.fold_left
-           (fun (rconstr,res) (l,e) ->
-              let rconstr = Types.Record.restrict_label_present rconstr l in
-              let pi = Types.Record.project_field rconstr l in
-              if Types.Record.is_empty rconstr then
-                raise_loc loc
-                  (ShouldHave (constr,(Printf.sprintf
-                                         "Field %s is not allowed here."
-                                         (Types.label_name l)
-                                      )
-                              ));
-              let t = type_check env e pi true in
-              let rconstr = Types.Record.restrict_field rconstr l t in
-              let res =
-                if precise
-                then Types.cap res (Types.record l false (Types.cons t))
-                else res in
-              (rconstr,res)
-           ) (rconstr, if precise then Types.Record.any else constr) r
-       in
-       res
    | Map (e,b) ->
-       let t = type_check env e (Sequence.star b.br_accept) true in
+       type_map loc env false e b constr precise
-       let constr' = Sequence.approx (Types.cap Sequence.any constr) in
+   | Transform (e,b) ->
-       let exact = Types.subtype (Sequence.star constr') constr in
+       localize loc (flatten (type_map loc env true e b) constr) precise
-       (* Note:
-          - could be more precise by integrating the decomposition
-          of constr inside Sequence.map.
-       *)
-       let res =
-         Sequence.map
-           (fun t ->
-              type_check_branches loc env t b constr' (precise || (not exact)))
-           t in
-       if not exact then check loc res constr "";
-       if precise then res else constr
-   | Op ("@", [e1;e2]) ->
-       let constr' = Sequence.star
-                       (Sequence.approx (Types.cap Sequence.any constr)) in
-       let exact = Types.subtype constr' constr in
-       if exact then
-         let t1 = type_check env e1 constr' precise
-         and t2 = type_check env e2 constr' precise in
-         if precise then Sequence.concat t1 t2 else constr
-       else
-         (* Note:
-            the knownledge of t1 may makes it useless to
-            check t2 with 'precise' ... *)
-         let t1 = type_check env e1 constr' true
-         and t2 = type_check env e2 constr' true in
-         let res = Sequence.concat t1 t2 in
-         check loc res constr "";
-         if precise then res else constr
-   | Op ("flatten", [e]) ->
-       let constr' = Sequence.star
-                       (Sequence.approx (Types.cap Sequence.any constr)) in
-       let sconstr' = Sequence.star constr' in
-       let exact = Types.subtype constr' constr in
-       if exact then
-         let t = type_check env e sconstr' precise in
-         if precise then Sequence.flatten t else constr
-       else
-         let t = type_check env e sconstr' true in
-         let res = Sequence.flatten t in
-         check loc res constr "";
-         if precise then res else constr
-   | _ ->
-       let t : Types.descr = compute_type' loc env e in
-       check loc t constr "";
-       t
- and compute_type env e =
-   type_check env e Types.any true
- and compute_type' loc env = function
-   | DebugTyper t -> Types.descr t
-   | Var s ->
-       (try Env.find s env
-        with Not_found -> raise_loc loc (UnboundId s)
-       )
    | Apply (e1,e2) ->
        let t1 = type_check env e1 Types.Arrow.any true in
        let t1 = Types.Arrow.get t1 in
        let dom = Types.Arrow.domain t1 in
+       let res =
        if Types.Arrow.need_arg t1 then
          let t2 = type_check env e2 dom true in
          Types.Arrow.apply t1 t2
        else
          (ignore (type_check env e2 dom false); Types.Arrow.apply_noarg t1)
-   | Cst c -> Types.constant c
+       in
+       verify loc res constr
+   | Var s ->
+       verify loc (find_value s env) constr
+   | ExtVar (cu,s,t) ->
+       verify loc t constr
+   | Cst c ->
+       verify loc (Types.constant c) constr
+   | String (i,j,s,e) ->
+       type_check_string loc env 0 s i j e constr precise
    | Dot (e,l) ->
        let t = type_check env e Types.Record.any true in
-          (try (Types.Record.project t l)
+       let t =
-           with Not_found -> raise_loc loc (WrongLabel(t,l)))
+         try (Types.Record.project t l)
-   | Op (op, el) ->
+         with Not_found -> raise_loc loc (WrongLabel(t,l))
-       let args = List.map (fun e -> (e.exp_loc, compute_type env e)) el in
+       in
-       type_op loc op args
+       verify loc t constr
-   | Map (e,b) ->
-       let t = compute_type env e in
-       Sequence.map (fun t -> type_check_branches loc env t b Types.any true) t
- (* We keep these cases here to allow comparison and benchmarking ...
+   | RemoveField (e,l) ->
-    Just comment the corresponding cases in type_check' to
+       let t = type_check env e Types.Record.any true in
-    activate these ones.
+       let t = Types.Record.remove_field t l in
- *)
+       verify loc t constr
-   | Pair (e1,e2) ->
-       let t1 = compute_type env e1
-       and t2 = compute_type env e2 in
-       Types.times (Types.cons t1) (Types.cons t2)
-   | RecordLitt r ->
-       List.fold_left
-         (fun accu (l,e) ->
-            let t = compute_type env e in
-            let t = Types.record l false (Types.cons t) in
-            Types.cap accu t
-         ) Types.Record.any r
+   | Xtrans (e,b) ->
+       let t = type_check env e Sequence.any true in
+       let t =
+         Sequence.map_tree
+           (fun t ->
+              let resid = Types.diff t b.br_accept in
+              let res = type_check_branches loc env t b Sequence.any true in
+              (res,resid)
+           ) t in
+       verify loc t constr
+   | Validate (e, kind, uri, name) ->
+       ignore (type_check env e Types.any false);
+       let t = find_schema_descr_uri kind uri name in
+       verify loc t constr
+   | Ref (e,t) ->
+       ignore (type_check env e (Types.descr t) false);
+       verify loc (Builtin_defs.ref_type t) constr
+   | External (t,i) ->
+       verify loc t constr
+   | Op (op,_,args) ->
+       let args = List.map (type_check env) args in
+       let t = localize loc (typ_op op args constr) precise in
+       verify loc t constr
+   | NsTable (ns,e) ->
+       type_check' loc env e constr precise
+ and type_check_pair ?(kind=`Normal) loc env e1 e2 constr precise =
+   let rects = Types.Product.normal ~kind constr in
+   if Types.Product.is_empty rects then
+     (match kind with
+       | `Normal -> should_have loc constr "but it is a pair"
+       | `XML -> should_have loc constr "but it is an XML element");
+   let need_s = Types.Product.need_second rects in
+   let t1 = type_check env e1 (Types.Product.pi1 rects) (precise || need_s) in
+   let c2 = Types.Product.constraint_on_2 rects t1 in
+   if Types.is_empty c2 then
+     raise_loc loc (ShouldHave2 (constr,"but the first component has type",t1));
+   let t2 = type_check env e2 c2 precise in
+   if precise then
+     match kind with
+       | `Normal -> Types.times (Types.cons t1) (Types.cons t2)
+       | `XML -> Types.xml (Types.cons t1) (Types.cons t2)
+   else
+     constr
+ and type_check_string loc env ofs s i j e constr precise =
+   if U.equal_index i j then type_check env e constr precise
+   else
+     let rects = Types.Product.normal constr in
+     if Types.Product.is_empty rects
+     then should_have_str loc ofs constr "but it is a string"
+     else
+       let need_s = Types.Product.need_second rects in
+       let (ch,i') = U.next s i in
+       let ch = Chars.V.mk_int ch in
+       let tch = Types.constant (Types.Char ch) in
+       let t1 = check_str loc ofs tch (Types.Product.pi1 rects) in
+       let c2 = Types.Product.constraint_on_2 rects t1 in
+       let t2 = type_check_string loc env (ofs + 1) s i' j e c2 precise in
+       if precise then Types.times (Types.cons t1) (Types.cons t2)
+       else constr
+ and type_record loc env r constr precise =
+ (* try to get rid of precise = true for values of fields *)
+ (* also: the use equivalent of need_second to optimize... *)
+   if not (Types.Record.has_record constr) then
+     should_have loc constr "but it is a record";
+   let (rconstr,res) =
+     List.fold_left
+       (fun (rconstr,res) (l,e) ->
+          (* could compute (split l e) once... *)
+          let pi = Types.Record.project_opt rconstr l in
+          if Types.is_empty pi then
+            (let l = Label.to_string (LabelPool.value l) in
+             should_have loc constr
+               (Printf.sprintf "Field %s is not allowed here." l));
+          let t = type_check env e pi true in
+          let rconstr = Types.Record.condition rconstr l t in
+          let res = (l,Types.cons t) :: res in
+          (rconstr,res)
+       ) (constr, []) (LabelMap.get r)
+   in
+   if not (Types.Record.has_empty_record rconstr) then
+     should_have loc constr "More fields should be present";
+   let t =
+     Types.record' (false, LabelMap.from_list (fun _ _ -> assert false) res)
+   in
+   verify loc t constr
-   | _ -> assert false
  and type_check_branches loc env targ brs constr precise =
    if Types.is_empty targ then Types.empty
-Line 643
+Line 1378
    )
  and branches_aux loc env targ tres constr precise = function
-   | [] -> raise_loc loc (NonExhaustive targ)
+   | [] -> tres
    | b :: rem ->
        let p = b.br_pat in
        let acc = Types.descr (Patterns.accept p) in
-Line 654
+Line 1389
        else
          ( b.br_used <- true;
            let res = Patterns.filter targ' p in
-           let env' = List.fold_left
+           let res = List.map (fun (x,t) -> (x,Types.descr t)) res in
-                        (fun env (x,t) -> Env.add x (Types.descr t) env)
+           let env' = enter_values res env in
-                        env res in
            let t = type_check env' b.br_body constr precise in
            let tres = if precise then Types.cup t tres else tres in
            let targ'' = Types.diff targ acc in
-Line 666
+Line 1400
              tres
          )
+ and type_map loc env def e b constr precise =
+   let acc = if def then Sequence.any else Sequence.star b.br_accept in
+   let t = type_check env e acc true in
+   let constr' = Sequence.approx (Types.cap Sequence.any constr) in
+   let exact = Types.subtype (Sequence.star constr') constr in
+   (* Note:
+      - could be more precise by integrating the decomposition
+      of constr inside Sequence.map.
+   *)
+   let res =
+     Sequence.map
+       (fun t ->
+          let res =
+            type_check_branches loc env t b constr' (precise || (not exact)) in
+          if def && not (Types.subtype t b.br_accept)
+          then (require loc Sequence.nil_type constr'; Types.cup res Sequence.nil_type)
+          else res)
+       t in
+   if exact then res else verify loc res constr
  and type_let_decl env l =
    let acc = Types.descr (Patterns.accept l.let_pat) in
    let t = type_check env l.let_body acc true in
-Line 673
+Line 1428
    List.map (fun (x,t) -> (x, Types.descr t)) res
  and type_rec_funs env l =
-   let types =
+   let typs =
      List.fold_left
-       (fun accu -> function  {let_body={exp_descr=Abstraction a}} as l ->
+       (fun accu -> function
-          let t = a.fun_typ in
+          | { exp_descr=Abstraction { fun_typ = t; fun_name = Some f };
-          let acc = Types.descr (Patterns.accept l.let_pat) in
+              exp_loc=loc } ->
-          if not (Types.subtype t acc) then
+              if not (value_name_ok f env) then
-            raise_loc l.let_body.exp_loc (NonExhaustive (Types.diff t acc));
+                error loc "This function name clashes with a type name";
-          let res = Patterns.filter t l.let_pat in
+              (f,t)::accu
-          List.fold_left (fun accu (x,t) -> (x, Types.descr t)::accu) accu res
+          | _ -> assert false
-          | _ -> assert false) [] l
+       ) [] l
    in
-   let env' = List.fold_left (fun env (x,t) -> Env.add x t env) env types in
+   let env = enter_values typs env in
+   List.iter (fun e -> ignore (type_check env e Types.any false)) l;
+   typs
+ let rec unused_branches b =
    List.iter
-     (function  { let_body = { exp_descr = Abstraction a } } as l ->
+     (fun (Branch (br,s)) ->
-        ignore (type_check env' l.let_body Types.any false)
+        if not br.br_used
-        | _ -> assert false) l;
+        then warning br.br_loc "This branch is not used"
-   types
+        else unused_branches s
+     )
+     b
- and type_op loc op args =
-   match (op,args) with
+ let report_unused_branches () =
-     | "+", [loc1,t1; loc2,t2] ->
+   unused_branches !cur_branch;
-         type_int_binop Intervals.add loc1 t1 loc2 t2
+   cur_branch := []
-     | "-", [loc1,t1; loc2,t2] ->
-         type_int_binop Intervals.sub loc1 t1 loc2 t2
+ let clear_unused_branches () =
-     | ("*" | "/"), [loc1,t1; loc2,t2] ->
+   cur_branch := []
-         type_int_binop (fun i1 i2 -> Intervals.any) loc1 t1 loc2 t2
-     | "@", [loc1,t1; loc2,t2] ->
-         check loc1 t1 Sequence.any
-           "The first argument of @ must be a sequence";
+ (* API *)
-         Sequence.concat t1 t2
-     | "flatten", [loc1,t1] ->
+ let type_expr env e =
-         check loc1 t1 Sequence.seqseq
+   clear_unused_branches ();
-           "The argument of flatten must be a sequence of sequences";
+   let e = expr env e in
-         Sequence.flatten t1
+   let t = type_check env e Types.any true in
-     | "load_xml", [loc1,t1] ->
+   report_unused_branches ();
-         check loc1 t1 Sequence.string
+   (e,t)
-           "The argument of load_xml must be a string (filename)";
-         Types.any
+ let type_let_decl env p e =
-     | "raise", [loc1,t1] ->
+   clear_unused_branches ();
-         Types.empty
+   let decl = let_decl env p e in
-     | "int_of", [loc1,t1] ->
+   let typs = type_let_decl env decl in
-         check loc1 t1 Sequence.string
+   report_unused_branches ();
-           "The argument of int_of must a string";
+   let env = enter_values typs env in
-         if not (Types.subtype t1 Builtin.intstr) then
+   (env,decl,typs)
-           warning loc "This application of int_of may fail";
-         Types.interval Intervals.any
+ let type_let_funs env funs =
+   clear_unused_branches ();
+   let rec id = function
+     | Ast.LocatedExpr (_,e) -> id e
+     | Ast.Abstraction a -> a.Ast.fun_name
      | _ -> assert false
+   in
+   let ids =
+     List.fold_left (fun accu f -> match id f with Some x -> x::accu | None -> accu)
+       [] funs in
+   let env' = enter_values_dummy ids env in
+   let funs = List.map (expr env') funs in
+   let typs = type_rec_funs env funs in
+   report_unused_branches ();
+   let env = enter_values typs env in
+   (env,funs,typs)
+   (* Schema stuff from now on ... *)
+   (** convertion from XML Schema types (including global elements and
+   attributes) to CDuce Types.descr *)
+ module Schema_converter =
+   struct
+     open Printf
+     open Schema_types
+     (* auxiliary functions *)
+     let nil_type = PType Sequence.nil_type
+     let mk_len_regexp ?min ?max base =
+       let rec repeat_regexp re = function
+         | z when Intervals.V.is_zero z -> PEpsilon
+         | n when Intervals.V.gt n Intervals.V.zero ->
+             PSeq (re, repeat_regexp re (Intervals.V.pred n))
+         | _ -> assert false
+       in
+       let min = match min with Some min -> min | _ -> Intervals.V.one in
+       let min_regexp = repeat_regexp base min in
+       match max with
+       | Some max ->
+           (*  assert (max >= min);   Need to use Bigint comparison ! -- AF *)
+           let rec aux acc = function
+             | z when Intervals.V.is_zero z -> acc
+             | n ->
+                 aux (PAlt (PEpsilon, (PSeq (base, acc)))) (Intervals.V.pred n)
+           in
+           PSeq (min_regexp, aux PEpsilon (Intervals.V.sub max min))
+       | None -> PSeq (min_regexp, PStar base)
+       (* given a base derecurs create a derecurs value representing a sequence
+        * type according to length constraints members of facets *)
+     let mk_seq_derecurs ~base facets =
+       match facets with
+       | { length = Some (v, _) } ->
+           PRegexp (mk_len_regexp ~min:v ~max:v base)
+       | { minLength = Some (v, _); maxLength = None } ->
+           PRegexp (mk_len_regexp ~min:v base)
+       | { minLength = None; maxLength = Some (v, _) } ->
+           PRegexp (mk_len_regexp ~max:v base)
+       | _ -> PRegexp base
+     let mix_regexp =
+       let pcdata = PStar (PElem (PType Builtin_defs.string)) in
+       let rec aux = function
+         | PEpsilon -> PEpsilon
+         | PElem re -> PElem re
+         | PGuard re -> PGuard re
+         | PSeq (re1, re2) -> PSeq (aux re1, PSeq (pcdata, aux re2))
+         | PAlt (re1, re2) -> PAlt (aux re1, aux re2)
+         | PStar re -> PStar (aux re)
+         | PWeakStar re -> PWeakStar (aux re)
+       in
+       let rec simplify = function
+         | PSeq (x1, PSeq (x2, y)) when x1 = pcdata && x2 = pcdata ->
+             simplify (PSeq (x2, y))
+         | re -> re
+       in
+       fun regexp -> simplify (PSeq (pcdata, aux regexp))
+     (* conversion functions *)
- and type_int_binop f loc1 t1 loc2 t2 =
+     let rec cd_type_of_simple_type ~schema = function
-   if not (Types.Int.is_int t1) then
+       | Primitive name | Derived (Some name, _, _, _)
-     raise_loc loc1
+         when Schema_builtin.is_builtin name ->
-       (Constraint
+           PType (Schema_builtin.cd_type_of_builtin name)
-          (t1,Types.Int.any,
+       | Primitive _ -> assert false (* all primitives are built-in *)
-           "The first argument must be an integer"));
+       | Derived (_, _, { enumeration = Some values }, _) -> (* enumeration *)
-   if not (Types.Int.is_int t2) then
+           PType (Types.choice_of_list
-     raise_loc loc2
+             (List.map (fun c -> Types.constant (Value.inv_const c))
-       (Constraint
+               (Value.ValueSet.elements values)))
-                (t2,Types.Int.any,
+       | Derived (_, _, ({ maxInclusive = Some _ } as facets), _)(* boundaries *)
-                 "The second argument must be an integer"));
+       | Derived (_, _, ({ maxExclusive = Some _ } as facets), _)
-   Types.Int.put
+       | Derived (_, _, ({ minInclusive = Some _ } as facets), _)
-     (f (Types.Int.get t1) (Types.Int.get t2));
+       | Derived (_, _, ({ minExclusive = Some _ } as facets), _) ->
+           PType (Types.interval (Schema_common.get_interval facets))
+       | Derived (_, Atomic (Primitive name), facets, _) ->
+           if name = U.mk "xsd:string" || name = U.mk "xsd:anyURI" then
+             (* length *)
+             mk_seq_derecurs ~base:(PElem (PType Builtin_defs.char)) facets
+           else if name = U.mk "xsd:hexBinary" ||
+             name = U.mk "xsd:base64Binary"
+           then (* length *)
+             mk_seq_derecurs ~base:(PElem (PType Builtin_defs.char_latin1))
+               facets
+           else (* no other interesting facet *)
+             PType (Schema_builtin.cd_type_of_builtin name)
+       | Derived (_, Atomic _, facets, _) -> assert false
+       | Derived (_, List item, facets, _) ->
+           mk_seq_derecurs
+             ~base:(PElem (cd_type_of_simple_type ~schema item)) facets
+       | Derived (_, Union items, facets, _) ->
+           (match List.map (cd_type_of_simple_type ~schema) items with
+           | [] -> assert false  (* vacuum union *)
+           | [t] -> t            (* useless union *)
+           | hd::tl -> List.fold_left (fun acc x -> POr (x, acc)) hd tl)
+     let complex_memo = Hashtbl.create 213
+     let element_memo = Hashtbl.create 213
+     let rec regexp_of_term ~schema = function
+       | Model group -> regexp_of_model_group ~schema group
+       | Elt decl -> PElem (cd_type_of_elt_decl ~schema !decl)
+     and regexp_of_model_group ~schema = function
+       | All [] | Choice [] | Sequence [] -> PEpsilon
+       | Choice (hd :: tl) ->
+           List.fold_left
+             (fun acc particle ->
+               PAlt (acc, regexp_of_particle ~schema particle))
+             (regexp_of_particle ~schema hd) tl
+       | All (hd :: tl) | Sequence (hd :: tl) ->
+           List.fold_left
+             (fun acc particle ->
+               PSeq (acc, regexp_of_particle ~schema particle))
+             (regexp_of_particle ~schema hd) tl
+ (*
+     and regexp_of_content_type ~schema = function
+       | CT_empty -> PEpsilon
+       | CT_simple st -> PElem (cd_type_of_simple_type ~schema st)
+       | CT_model (particle, mixed) ->
+           let regexp = regexp_of_particle ~schema particle in
+           if mixed then begin (* TODO mixed *)
+             Value.failwith' "Mixed content models aren't supported";
+             mix_regexp regexp
+           end else
+             regexp
+ *)
+     and regexp_of_particle ~schema (min, max, term, _) =
+       mk_len_regexp ?min:(Some min) ?max (regexp_of_term ~schema term)
+       (** @return a pair composed by a type for the attributes (a record) and a
+       type for the content model (a sequence) *)
+     and cd_type_of_complex_type' ~schema ct =
+       try
+         PAlias (Hashtbl.find complex_memo ct.ct_uid)
+       with Not_found ->
+         let slot = mk_derecurs_slot noloc in
+         Hashtbl.add complex_memo ct.ct_uid slot;
+ (*        let content_re = regexp_of_content_type ~schema ct.ct_content in*)
+         let content_ast_node =
+           match ct.ct_content with
+           | CT_empty -> PType Sequence.nil_type
+           | CT_simple st -> cd_type_of_simple_type ~schema st
+           | CT_model (particle, mixed) ->
+               if mixed then
+                 Value.failwith' "Mixed content models aren't supported";
+               let regexp = regexp_of_particle ~schema particle in
+               PRegexp regexp
+         in
+         slot.pdescr <-
+           PTimes (cd_type_of_attr_uses ~schema ct.ct_attrs, content_ast_node);
+         PAlias slot
+       (** @return a closed record *)
+     and cd_type_of_attr_uses ~schema attr_uses =
+       let fields =
+         List.map
+           (fun at ->
+             let r =
+               match at.attr_use_cstr with
+               | Some (`Fixed v) -> PType (Types.constant (Value.inv_const v))
+               | _ -> cd_type_of_simple_type ~schema at.attr_decl.attr_typdef
+             in
+             let r = if at.attr_required then r else POptional r in
+             (LabelPool.mk (Ns.empty, at.attr_decl.attr_name), (r,None)))
+           attr_uses in
+       PRecord (false, LabelMap.from_list_disj fields)
+     and cd_type_of_att_decl ~schema att =
+       let r = cd_type_of_simple_type ~schema att.attr_typdef in
+       PRecord (false,
+         LabelMap.from_list_disj
+           [(LabelPool.mk (schema.targetNamespace, att.attr_name), (r,None))])
+     and cd_type_of_elt_decl ~schema elt =
+       let atom_type =
+         PType (Types.atom (Atoms.atom (Atoms.V.mk
+                                          schema.targetNamespace
+                                          elt.elt_name)))
+       in
+       let content =
+         match elt.elt_cstr with
+         | Some (`Fixed v) -> PType (Types.constant (Value.inv_const v))
+         | _ ->
+           (match elt.elt_typdef with
+           | AnyType ->
+               PType (Schema_builtin.cd_type_of_builtin (U.mk "xsd:anyType"))
+           | Simple st ->
+               PTimes
+                 (PType Types.empty_closed_record,
+                  cd_type_of_simple_type ~schema st)
+           | Complex ct -> cd_type_of_complex_type' ~schema ct)
+       in
+       PXml (atom_type, content)
+     let cd_type_of_complex_type ~schema ct =
+       PXml (PType Types.any, cd_type_of_complex_type' ~schema ct)
+     let cd_type_of_model_group ~schema g =
+       PRegexp (regexp_of_model_group ~schema g)
+     let typ r = Types.descr (do_typ noloc r)
+       (* Schema_converter interface implementation.
+        * Shadows previous definitions.
+        *)
+     let cd_type_of_type_def ~schema = function
+       | AnyType -> Schema_builtin.cd_type_of_builtin (U.mk "xsd:anyType")
+       | Simple st -> typ (cd_type_of_simple_type ~schema st)
+       | Complex ct -> typ (cd_type_of_complex_type ~schema ct)
+     let cd_type_of_elt_decl ~schema x = typ (cd_type_of_elt_decl ~schema x)
+     let cd_type_of_att_decl ~schema x = typ (cd_type_of_att_decl ~schema x)
+     let cd_type_of_attr_uses ~schema x = typ (cd_type_of_attr_uses ~schema x)
+     let cd_type_of_model_group ~schema x =
+       typ (cd_type_of_model_group ~schema x)
+   end
+ let get_schema_names env = UEnv.fold (fun n _ acc -> n :: acc) env.schemas []
+ open Schema_types
+ let get_schema uri =
+   try Hashtbl.find !schemas uri
+   with Not_found ->
+     let schema = match Url.process uri with
+       | Url.Filename s -> Schema_parser.schema_of_file s
+       | Url.Url s ->  Schema_parser.schema_of_string s in
+     let log_schema_component kind uri name cd_type =
+       (*      if not (Schema_builtin.is_builtin name) then begin
+               Format.fprintf Format.std_formatter
+               "Registering schema %s: %s # %s"
+               kind uri (U.get_str name);
+               if debug_schema then
+               Types.Print.print Format.std_formatter cd_type;
+               Format.fprintf Format.std_formatter "@."
+               end *)
+       ()
+     in
+     Hashtbl.add !schemas uri schema;
+     List.iter (* Schema types -> CDuce types *)
+       (fun type_def ->
+          let name = Schema_common.name_of_type_definition type_def in
+          let cd_type = Schema_converter.cd_type_of_type_def ~schema type_def in
+          log_schema_component "type" uri name cd_type;
+          Hashtbl.add !schema_types (uri, name) cd_type)
+       schema.Schema_types.types;
+     List.iter (* Schema attributes -> CDuce types *)
+       (fun att_decl ->
+          let cd_type = Schema_converter.cd_type_of_att_decl ~schema att_decl in
+          let name = Schema_common.name_of_attribute_declaration att_decl in
+          log_schema_component "attribute" uri name cd_type;
+          Hashtbl.add !schema_attributes (uri, name) cd_type)
+       schema.Schema_types.attributes;
+     List.iter (* Schema elements -> CDuce types *)
+       (fun elt_decl ->
+          let cd_type = Schema_converter.cd_type_of_elt_decl ~schema elt_decl in
+          let name = Schema_common.name_of_element_declaration elt_decl in
+          log_schema_component "element" uri name cd_type;
+          Hashtbl.add !schema_elements (uri, name) cd_type)
+       schema.Schema_types.elements;
+     List.iter (* Schema attribute groups -> CDuce types *)
+       (fun ag ->
+          let cd_type = Schema_converter.cd_type_of_attr_uses ~schema ag.ag_def
+          in
+          log_schema_component "attribute group" uri ag.ag_name cd_type;
+          Hashtbl.add !schema_attribute_groups (uri, ag.ag_name) cd_type)
+       schema.Schema_types.attribute_groups;
+     List.iter (* Schema model groups -> CDuce types *)
+       (fun mg ->
+          let cd_type = Schema_converter.cd_type_of_model_group ~schema mg.mg_def         in
+          log_schema_component "model group" uri mg.mg_name cd_type;
+          Hashtbl.add !schema_model_groups (uri, mg.mg_name) cd_type)
+       schema.Schema_types.model_groups;
+     schema
+ let () = get_schema_fwd := get_schema

 Legend:



Removed from v.72
 


changed lines


 
Added in v.1401
 Legend:



Removed from v.72
 


changed lines


 
Added in v.1401
-Removed from v.72
+Added in v.1401

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