viewcvs.cgi/typing/typer.ml

(* TODO:
 - 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 NonExhaustive of Types.descr
exception Constraint of Types.descr * Types.descr
exception ShouldHave of Types.descr * string
exception ShouldHave2 of Types.descr * string * Types.descr
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 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

let deserialize s =
  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 }


let empty_env = {
  ids = Env.empty;
  ns = Ns.empty_table;
  cu = UEnv.empty;
  schemas = UEnv.empty
}

let from_comp_unit = ref (fun cu -> assert false)

let enter_cu x cu env =
  { env with cu = UEnv.add x cu env.cu }

let find_cu x env =
  try UEnv.find x env.cu
  with Not_found -> Types.CompUnit.mk x


let enter_schema x uri env =
  { env with schemas = UEnv.add x uri env.schemas }
let find_schema x env =
  try UEnv.find x env.schemas
  with Not_found -> raise (Error (Printf.sprintf "%s: no such schema" (U.get_str x)))

let enter_type id t env =
  { env with ids = Env.add id (Type t) env.ids }
let enter_types l env =
  { env with ids = 
      List.fold_left (fun accu (id,t) -> Env.add id (Type t) accu) env.ids l }
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"

(* I. Transform the abstract syntax of types and patterns into
      the internal form *)


(* Schema *)

let is_registered_schema env s = UEnv.mem s env.schemas

(* uri -> schema binding *)
let schemas = State.ref "Typer.schemas" (Hashtbl.create 3)

let schema_types = State.ref "Typer.schema_types" (Hashtbl.create 51)
let schema_elements = State.ref "Typer.schema_elements" (Hashtbl.create 51)
let schema_attributes = State.ref "Typer.schema_attributes" (Hashtbl.create 51)
let schema_attribute_groups =
  State.ref "Typer.schema_attribute_groups" (Hashtbl.create 51)
let schema_model_groups =
  State.ref "Typer.schema_model_groups" (Hashtbl.create 51)


  (* raise Not_found *)


let get_schema_fwd = ref (fun _ -> assert false)

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 (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 *)

let rec seq_vars accu = function
  | Epsilon | Elem _ | Guard _ -> accu
  | Seq (r1,r2) | Alt (r1,r2) -> seq_vars (seq_vars accu r1) r2
  | Star r | WeakStar r -> seq_vars accu r
  | SeqCapture (v,r) -> seq_vars (IdSet.add v accu) r

(* 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 * derecurs
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

let pregexp r q = PRegexp (r,q)


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 -> 
      1 + 17 * (Types.hash t)
  | POr (p1,p2) -> 
      2 + 17 * (hash_derecurs p1) + 257 * (hash_derecurs p2)
  | PAnd (p1,p2) -> 
      3 + 17 * (hash_derecurs p1) + 257 * (hash_derecurs p2)
  | PDiff (p1,p2) -> 
      4 + 17 * (hash_derecurs p1) + 257 * (hash_derecurs p2)
  | PTimes (p1,p2) -> 
      5 + 17 * (hash_derecurs p1) + 257 * (hash_derecurs p2)
  | PXml (p1,p2) -> 
      6 + 17 * (hash_derecurs p1) + 257 * (hash_derecurs p2)
  | PArrow (p1,p2) -> 
      7 + 17 * (hash_derecurs p1) + 257 * (hash_derecurs p2)
  | POptional p -> 
      8 + 17 * (hash_derecurs p)
  | PRecord (o,r) -> 
      (if o then 9 else 10) + 17 * (LabelMap.hash hash_derecurs_field r)
  | PCapture x -> 
      11 + 17 * (Id.hash x)
  | PConstant (x,c) -> 
      12 + 17 * (Id.hash x) + 257 * (Types.Const.hash c)
  | PRegexp (p,q) -> 
      13 + 17 * (hash_derecurs_regexp p) + 257 * (hash_derecurs q)
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 -> 
      1
  | PElem p -> 
      2 + 17 * (hash_derecurs p)
  | PSeq (p1,p2) -> 
      3 + 17 * (hash_derecurs_regexp p1) + 257 * (hash_derecurs_regexp p2)
  | PAlt (p1,p2) -> 
      4 + 17 * (hash_derecurs_regexp p1) + 257 * (hash_derecurs_regexp p2)
  | PStar p -> 
      5 + 17 * (hash_derecurs_regexp p)
  | PWeakStar p -> 
      6 + 17 * (hash_derecurs_regexp p)
  | PGuard p ->
      7 + 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,q1), PRegexp (p2,q2) -> 
      (equal_derecurs_regexp p1 p2) && (equal_derecurs q1 q2)
  | _ -> 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
)

module RE = Hashtbl.Make(
  struct 
    type t = derecurs_regexp * derecurs 
    let hash (p,q) = 
      (hash_derecurs_regexp p) + 17 * (hash_derecurs q)
    let equal (p1,q1) (p2,q2) = 
      (equal_derecurs_regexp p1 p2) && (equal_derecurs q1 q2)
  end
)

let gen = ref 0
let rank = ref 0
             
let rec hash_descr = function
  | IDummy -> assert false
  | IType x -> Types.hash x
  | 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 (
    incr rank;
    s.rank1 <- !rank; s.gen1 <- !gen;
    hash_descr s.d
  )
    
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 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,q) -> 
      let constant_nil t v = 
        PAnd (t, PConstant (v, Types.Atom Sequence.nil_atom)) in
      let vars = seq_vars IdSet.empty r in
      let q = IdSet.fold constant_nil (derecurs env q) vars in
      let r = derecurs_regexp (fun p -> p) env r in
      PRegexp (r, q)
        (* Note: computing remove_regexp here is slower (because
           of caching ?) *)

and derecurs_regexp vars env = function
  | Epsilon -> 
      PEpsilon
  | Elem p -> 
      PElem (vars (derecurs env p))
  | Guard p ->
      PGuard (vars (derecurs env p))
  | Seq (p1,p2) -> 
      PSeq (derecurs_regexp vars env p1, derecurs_regexp vars env p2)
  | Alt (p1,p2) -> 
      PAlt (derecurs_regexp vars env p1, derecurs_regexp vars env p2)
  | Star p -> 
      PStar (derecurs_regexp vars env p)
  | WeakStar p -> 
      PWeakStar (derecurs_regexp vars env p)
  | SeqCapture (x,p) -> 
      derecurs_regexp (fun p -> PAnd (vars p, PCapture x)) env p

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))

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 x -> x
    | None ->
        if s.gen1 = !gen then IdSet.empty 
        else (s.gen1 <- !gen; fv_descr s.d)
and fv_descr = function
  | IDummy -> assert false
  | IType _ -> IdSet.empty
  | IOr (d1,d2)
  | IAnd (d1,d2)  
  | IDiff (d1,d2) -> IdSet.cup (fv_descr d1) (fv_descr d2)
  | IOptional d -> fv_descr d
  | ITimes (s1,s2)  
  | IXml (s1,s2)  
  | IArrow (s1,s2) -> IdSet.cup (fv_slot s1) (fv_slot s2)
  | IRecord (o,r) -> 
      List.fold_left IdSet.cup IdSet.empty (LabelMap.map_to_list fv_field r)
  | ICapture x | IConstant (x,_) -> IdSet.singleton x
and fv_field = function
  | (d,Some e) -> IdSet.cup (fv_slot d) (fv_descr e)
  | (d,None) -> fv_slot d


let compute_fv s =
  match s.fv with
    | Some x -> ()
    | None ->
        incr gen;
        let x = fv_slot s in
        s.fv <- Some 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 compile_slot_hash = DerecursTable.create 67
let compile_hash = DerecursTable.create 67

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,q) -> compile (remove_regexp r q)

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 timer_fv = Stats.Timer.create "Typer.fv"
let rec flush_defs () = 
  match !todo_defs with
    | [] -> 
        Stats.Timer.start timer_fv;
        List.iter compute_fv !todo_fv;
        todo_fv := [];
        Stats.Timer.stop timer_fv ()
    | (s,p)::t -> 
        todo_defs := t; 
        s.d <- compile p; 
        flush_defs ()
        
let typ_nodes = SlotTable.create 67
let pat_nodes = SlotTable.create 67
                  
let rec typ = function
  | IType t -> t
  | IOr (s1,s2) -> Types.cup (typ s1) (typ s2)
  | IAnd (s1,s2) ->  Types.cap (typ s1) (typ s2)
  | IDiff (s1,s2) -> Types.diff (typ s1) (typ s2)
  | ITimes (s1,s2) -> Types.times (typ_node s1) (typ_node s2)
  | IXml (s1,s2) -> Types.xml (typ_node s1) (typ_node s2)
  | IArrow (s1,s2) -> Types.arrow (typ_node s1) (typ_node s2)
  | 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 =
  try SlotTable.find pat_nodes s
  with Not_found ->
    let x = Patterns.make (fv_slot s) in
    try
      SlotTable.add pat_nodes s x;
      Patterns.define x (pat s.d);
      x
    with exn -> SlotTable.remove pat_nodes s; raise exn
      (* For the toplevel ... *)


module Ids = Set.Make(Id)
let type_defs env b =
  ignore 
    (List.fold_left 
       (fun seen (v,p) ->
          if Ids.mem v seen then 
            raise_loc_generic p.loc 
              ("Multiple definitions for the type identifer " ^ 
               (Ident.to_string v));
          Ids.add v seen
       ) Ids.empty b);

  let penv = derecurs_def (penv env) b in
  let b = List.map (fun (v,p) -> (v,p,compile (derecurs penv p))) b in
  flush_defs ();
  let b = 
    List.map 
      (fun (v,p,s) -> 
         check_no_capture p.loc (fv_descr s);
         let t = typ s in
         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 *)


type type_fun = Types.t -> bool -> Types.t

module Fv = IdSet

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 env loc e and t = typ env t in
      exp loc fv (Typed.Forget (e,t))
  | Var s -> var env loc s
  | Apply (e1,e2) -> 
      let (fv1,e1) = expr env loc e1 and (fv2,e2) = expr env loc e2 in
      let fv = Fv.cup fv1 fv2 in
      (match e1.Typed.exp_descr with
         | Typed.Op (op,arity,args) when arity > 0 -> 
             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 
      (fun (t1,t2) -> (Types.descr t1, Types.descr t2)) 
      iface 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
  let e = Typed.Abstraction 
            { Typed.fun_name = a.fun_name;
              Typed.fun_iface = iface;
              Typed.fun_body = body;
              Typed.fun_typ = t;
              Typed.fun_fv = fv
            } in
  exp loc fv e
    
and branches env b = 
  let fv = ref Fv.empty in
  let accept = ref Types.empty in
  let branch (p,e) = 
    let cur_br = !cur_branch in
    cur_branch := [];
    let p' = pat env p in
    let fvp = Patterns.fv p' in
    let env' = enter_values_dummy fvp env in
    let (fv2,e) = expr env' noloc e in
    let br_loc = merge_loc p.loc e.Typed.exp_loc in
    (match Fv.pick (Fv.diff fvp fv2) with
       | None -> ()
       | 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; 
     Typed.br_branches = b; 
     Typed.br_accept = !accept;
     Typed.br_compiled = None;
   } 
  )

let expr env e = snd (expr env noloc e)

let let_decl env p e =
  { Typed.let_pat = pat env p;
    Typed.let_body = expr env e;
    Typed.let_compiled = None }


(* Hide global "typing/parsing" environment *)


(* III. Type-checks *)

open Typed

let localize loc f x =
  try f x
  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 should_have loc constr s = 
  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 = 
  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

and type_check' loc env e constr precise = match e with
  | Forget (e,t) ->
      let t = Types.descr t in
      ignore (type_check env e t false);
      verify loc t constr

  | Abstraction a ->
      let t =
        try Types.Arrow.check_strenghten a.fun_typ constr 
        with Not_found -> 
          should_have loc constr
            "but the interface of the abstraction is not compatible"
      in
      let env = match a.fun_name with
        | None -> env
        | 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

  | Match (e,b) ->
      let t = type_check env e b.br_accept true in
      type_check_branches loc env t b constr precise

  | Try (e,b) ->
      let te = type_check env e constr precise in
      let tb = type_check_branches loc env Types.any b constr precise in
      Types.cup te tb

  | Pair (e1,e2) ->
      type_check_pair loc env e1 e2 constr precise

  | Xml (e1,e2) ->
      type_check_pair ~kind:`XML loc env e1 e2 constr precise

  | RecordLitt r ->
      type_record loc env r constr precise

  | Map (e,b) ->
      type_map loc env false e b constr precise

  | Transform (e,b) ->
      localize loc (flatten (type_map loc env true e b) constr) precise

  | 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)
      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
      let t = 
        try (Types.Record.project t l) 
        with Not_found -> raise_loc loc (WrongLabel(t,l))
      in
      verify loc t constr

  | RemoveField (e,l) ->
      let t = type_check env e Types.Record.any true in
      let t = Types.Record.remove_field t l in
      verify loc t constr

  | 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


and type_check_branches loc env targ brs constr precise =
  if Types.is_empty targ then Types.empty
  else (
    brs.br_typ <- Types.cup brs.br_typ targ;
    branches_aux loc env targ 
      (if precise then Types.empty else constr) 
      constr precise brs.br_branches
  )
    
and branches_aux loc env targ tres constr precise = function
  | [] -> tres
  | b :: rem ->
      let p = b.br_pat in
      let acc = Types.descr (Patterns.accept p) in

      let targ' = Types.cap targ acc in
      if Types.is_empty targ' 
      then branches_aux loc env targ tres constr precise rem
      else 
        ( b.br_used <- true;
          let res = Patterns.filter targ' p in
          let res = List.map (fun (x,t) -> (x,Types.descr t)) res in
          let env' = enter_values res env 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
          if (Types.non_empty targ'') then 
            branches_aux loc env targ'' tres constr precise rem 
          else
            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
  let res = Patterns.filter t l.let_pat in
  List.map (fun (x,t) -> (x, Types.descr t)) res

and type_rec_funs env l =
  let typs = 
    List.fold_left
      (fun accu -> function  
         | { exp_descr=Abstraction { fun_typ = t; fun_name = Some f };
             exp_loc=loc } ->
             if not (value_name_ok f env) then
               error loc "This function name clashes with a type name";
             (f,t)::accu
         | _ -> assert false
      ) [] l
  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
    (fun (Branch (br,s)) -> 
       if not br.br_used 
       then warning br.br_loc "This branch is not used"
       else unused_branches s
    )
    b

let report_unused_branches () =
  unused_branches !cur_branch;
  cur_branch := []
  
let clear_unused_branches () =
  cur_branch := []


(* API *)

let type_expr env e =
  clear_unused_branches ();
  let e = expr env e in
  let t = type_check env e Types.any true in
  report_unused_branches ();
  (e,t)

let type_let_decl env p e =
  clear_unused_branches ();
  let decl = let_decl env p e in
  let typs = type_let_decl env decl in
  report_unused_branches ();
  let env = enter_values typs env in
  (env,decl,typs)

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) nil_type
      | { minLength = Some (v, _); maxLength = None } ->
          pregexp (mk_len_regexp ~min:v base) nil_type
      | { minLength = None; maxLength = Some (v, _) } ->
          pregexp (mk_len_regexp ~max:v base) nil_type
      | _ -> pregexp base nil_type

    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 *)

    let rec cd_type_of_simple_type ~schema = function
      | Primitive name | Derived (Some name, _, _, _)
        when Schema_builtin.is_builtin name ->
          PType (Schema_builtin.cd_type_of_builtin name)
      | Primitive _ -> assert false (* all primitives are built-in *)
      | Derived (_, _, { enumeration = Some values }, _) -> (* enumeration *)
          PType (Types.choice_of_list
            (List.map (fun c -> Types.constant (Value.inv_const c))
              (Value.ValueSet.elements values)))
      | Derived (_, _, ({ maxInclusive = Some _ } as facets), _)(* boundaries *)
      | Derived (_, _, ({ maxExclusive = Some _ } as facets), _)
      | Derived (_, _, ({ minInclusive = Some _ } as facets), _)
      | Derived (_, _, ({ minExclusive = Some _ } as facets), 