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 =
  let v = Location.get_viewport () in
  let ppf = if Html.is_html v then Html.ppf v else Format.err_formatter in
  Format.fprintf ppf "Warning %a:@\n" Location.print_loc (loc,`Full);
  Location.html_hilight (loc,`Full);
  Format.fprintf ppf "%s@." 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 *)

(* 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 -> 
      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 -> 
      13 + 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 -> 
      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, 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
)

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

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