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


let warning loc msg =
  Format.fprintf !Location.warning_ppf "Warning %a:@\n%a%s@\n" 
    Location.print_loc (loc,`Full)
    Location.html_hilight (loc,`Full)
    msg


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

open Location
open Ast
open Ident

module TypeEnv = Map.Make(U)

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
exception Error of string

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)

  (* Schema datastructures *)

module StringSet = Set.Make (String)

  (* just to remember imported schemas *)
let schemas = State.ref "Typer.schemas" StringSet.empty

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)

(* Eliminate Recursion, propagate Sequence Capture Variables *)

let rec seq_vars accu = function
  | Epsilon | Elem _ -> 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

type derecurs_slot = {
  ploc : Location.loc;
  pid  : int;
  mutable ploop : bool;
  mutable pdescr : derecurs option
} and derecurs =
  | 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 label_map
  | PCapture of id
  | PConstant of id * Types.const
  | PRegexp of derecurs_regexp * derecurs
and derecurs_regexp =
  | PEpsilon
  | PElem of derecurs
  | PSeq of derecurs_regexp * derecurs_regexp
  | PAlt of derecurs_regexp * derecurs_regexp
  | PStar of derecurs_regexp
  | PWeakStar of derecurs_regexp

type tenv = {
  tenv_names : derecurs_slot TypeEnv.t;
  tenv_nspref: Ns.table;
  tenv_loc   : Location.loc
}
let get_ns_table tenv = tenv.tenv_nspref

let rec hash_derecurs = function
  | PAlias s -> 
      s.pid
  | PType t -> 
      1 + 17 * (Types.hash_descr 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 r)
  | PCapture x -> 
      11 + 17 * (Id.hash x)
  | PConstant (x,c) -> 
      12 + 17 * (Id.hash x) + 257 * (Types.hash_const c)
  | PRegexp (p,q) -> 
      13 + 17 * (hash_derecurs_regexp p) + 257 * (hash_derecurs q)
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)

let rec equal_derecurs p1 p2 = (p1 == p2) || match p1,p2 with
  | PAlias s1, PAlias s2 -> 
      s1 == s2
  | PType t1, PType t2 -> 
      Types.equal_descr 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 r1 r2)
  | PCapture x1, PCapture x2 -> 
      Id.equal x1 x2
  | PConstant (x1,c1), PConstant (x2,c2) -> 
      (Id.equal x1 x2) && (Types.equal_const c1 c2)
  | PRegexp (p1,q1), PRegexp (p2,q2) -> 
      (equal_derecurs_regexp p1 p2) && (equal_derecurs q1 q2)
  | _ -> false
and equal_derecurs_regexp r1 r2 = match r1,r2 with
  | PEpsilon, PEpsilon -> 
      true
  | PElem p1, PElem 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 counter = State.ref "Typer.counter - derecurs" 0
let mk_slot loc = 
  incr counter; 
  { ploop = false; ploc = loc; pid = !counter; pdescr = None }

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.tenv_nspref) t in
  Atoms.mk ns l
 
let parse_ns env loc ns =
  protect_error_ns loc (Ns.map_prefix env.tenv_nspref) ns

let const env loc = function
  | Const_internal c -> c
  | Const_atom t -> Types.Atom (parse_atom env loc t)

let parse_label env loc t =
  let (ns,l) = protect_error_ns loc (Ns.map_attr env.tenv_nspref) 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 derecurs env p = match p.descr with
  | PatVar v ->
      (try PAlias (TypeEnv.find v env.tenv_names)
       with Not_found -> 
         raise_loc_generic p.loc ("Undefined type/pattern " ^ (U.to_string v)))
  | SchemaVar (kind, schema, item) ->
      let try_elt () = fst (Hashtbl.find !schema_elements (schema, item)) in
      let try_typ () = Hashtbl.find !schema_types (schema, item) in
      let try_att () = Hashtbl.find !schema_attributes (schema, item) in
      (match kind with
      | `Element ->
          (try
            PType (try_elt ())
          with Not_found ->
            failwith (Printf.sprintf
              "No element named '%s' found in schema '%s'" item schema))
      | `Type ->
          (try
            PType (try_typ ())
          with Not_found ->
            failwith (Printf.sprintf
              "No type named '%s' found in schema '%s'" item schema))
      | `Attribute ->
          (try
            PType (try_att ())
          with Not_found ->
            failwith (Printf.sprintf
              "No attribute named '%s' found in schema '%s'" item schema))
      | `Any ->
          PType
            (try try_elt () with Not_found ->
              (try try_typ () with Not_found ->
                (try try_att () with Not_found ->
                  failwith (Printf.sprintf
                    "No item named '%s' found in schema '%s'" item schema)))))
  | Recurs (p,b) -> derecurs (derecurs_def env b) p
  | Internal t -> PType t
  | AtomT t -> PType (Types.atom (Atoms.atom (parse_atom env p.loc t)))
  | NsT ns -> PType (Types.atom (Atoms.any_in_ns (parse_ns env 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) -> PRecord (o, parse_record env p.loc (derecurs env) r)
  | Capture x -> PCapture x
  | Constant (x,c) -> PConstant (x,const env 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)
and derecurs_regexp vars env = function
  | Epsilon -> 
      PEpsilon
  | Elem p -> 
      PElem (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_def env b =
  let b = List.map (fun (v,p) -> (v,p,mk_slot p.loc)) b in
  let n = 
    List.fold_left (fun env (v,p,s) -> TypeEnv.add v s env) env.tenv_names b in
  let env = { env with tenv_names = n } in
  List.iter (fun (v,p,s) -> s.pdescr <- Some (derecurs env p)) b;
  env

(* Stratification and recursive hash-consing *)

type descr = 
  | 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 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 option
}
    
let descr s = 
  match s.d with
    | Some d -> d
    | None -> assert false
        
let gen = ref 0
let rank = ref 0
             
let rec hash_descr = function
  | IType x -> Types.hash_descr 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_slot r)
  | ICapture x -> 10 + 17 * (Id.hash x)
  | IConstant (x,y) -> 11 + 17 * (Id.hash x) + 257 * (Types.hash_const y)
and hash_slot s =
  if s.gen1 = !gen then 13 * s.rank1
  else (
    incr rank;
    s.rank1 <- !rank; s.gen1 <- !gen;
    hash_descr (descr s)
  )
    
let rec equal_descr d1 d2 = 
  match (d1,d2) with
  | IType x1, IType x2 -> Types.equal_descr 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_slot r1 r2)
  | ICapture x1, ICapture x2 -> Id.equal x1 x2
  | IConstant (x1,y1), IConstant (x2,y2) -> 
      (Id.equal x1 x2) && (Types.equal_const y1 y2)
  | _ -> 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 (descr s1) (descr s2)
   ))
  
module Arg = 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-consig: Equal\n";  *)
     e)
end
module SlotTable = Hashtbl.Make(Arg)
  
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 (descr s))
and fv_descr = function
  | 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_slot r)
  | ICapture x | IConstant (x,_) -> IdSet.singleton x

      
let compute_fv s =
  match s.fv with
    | Some x -> ()
    | None ->
        incr gen;
        let x = fv_slot s in
        s.fv <- Some x
          

let todo_fv = ref []
          
let mk () =   
  let s = 
    { d = None;
      fv = None;
      hash = None;
      rank1 = 0; rank2 = 0;
      gen1 = 0; gen2 = 0 } in
  todo_fv := s :: !todo_fv;
  s

let flush_fv () =
  List.iter compute_fv !todo_fv;
  todo_fv := []
    
let compile_slot_hash = DerecursTable.create 67
let compile_hash = DerecursTable.create 67

let defs = 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
  | PAlias v ->
      if v.ploop then
        raise_loc_generic v.ploc ("Unguarded recursion on type/pattern");
      v.ploop <- true;
      let r = match v.pdescr with Some x -> compile x | _ -> assert false 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_slot r)
  | PConstant (x,v) -> IConstant (x,v)
  | PCapture x -> ICapture x
  | PRegexp (r,q) -> compile_regexp r q
and compile_regexp r q =
  let memo = RE.create 17 in
  let rec aux accu r q =
    if RE.mem memo (r,q) then accu
    else (
      RE.add memo (r,q) ();
      match r with
        | PEpsilon -> 
            (match q with 
               | PRegexp (r,q) -> aux accu r q 
               | _ -> (compile q) :: accu)
        | PElem p -> ITimes (compile_slot p, compile_slot q) :: accu
        | PSeq (r1,r2) -> aux accu r1 (PRegexp (r2,q))
        | PAlt (r1,r2) -> aux (aux accu r1 q) r2 q
        | PStar r1 -> aux (aux accu r1 (PRegexp (r,q))) PEpsilon q
        | PWeakStar r1 -> aux (aux accu PEpsilon q) r1 (PRegexp (r,q))
    )
  in
  let accu = aux [] r q in
  match accu with
    | [] -> assert false
    | p::l -> List.fold_left (fun acc p -> IOr (p,acc)) p l
and compile_slot p =
  try DerecursTable.find compile_slot_hash p
  with Not_found ->
    let s = mk () in
    defs := (s,p) :: !defs;
    DerecursTable.add compile_slot_hash p s;
    s

      
let rec flush_defs () = 
  match !defs with
    | [] -> ()
    | (s,p)::t -> defs := t; s.d <- Some (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_node r)
  | ICapture x | IConstant (x,_) -> assert false
      
and typ_node s : Types.node =
  try SlotTable.find typ_nodes s
  with Not_found ->
    let x = Types.make () in
    SlotTable.add typ_nodes s x;
    Types.define x (typ (descr s));
    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
  | 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 "Difference 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 field not allowed in record patterns")
  | IRecord (o,r) ->
      let pats = ref [] in
      let aux l s = 
        if IdSet.is_empty (fv_slot s) then typ_node s
        else
          ( pats := Patterns.record l (pat_node s) :: !pats;
            Types.any_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 "Arrow 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
    SlotTable.add pat_nodes s x;
    Patterns.define x (pat (descr s));
    x

let register_global_types glb b =
  List.iter 
    (fun (v,p) ->
       if TypeEnv.mem v glb.tenv_names
       then raise_loc_generic p.loc ("Multiple definition for type " ^ (U.to_string v))
    ) b;
  let glb = derecurs_def glb b in
  let b = List.map (fun (v,p) -> (v,p,compile (derecurs glb p))) b in
  flush_defs ();
  flush_fv ();
  let b = 
    List.map 
      (fun (v,p,s) -> 
         if not (IdSet.is_empty (fv_descr s)) then
           raise_loc_generic p.loc 
             "Capture variables are not allowed in types";
         let t = typ s in
         if (p.loc <> noloc) && (Types.is_empty t) then
           warning p.loc 
             ("This definition yields an empty type for " ^ (U.to_string v));
         (v,t)) b in
  List.iter (fun (v,t) -> Types.Print.register_global v t) b;
  glb

let register_ns_prefix glb p ns =
  { glb with tenv_nspref = Ns.add_prefix p ns glb.tenv_nspref }

let dump_global_types ppf glb =
  TypeEnv.iter (fun v _ -> Format.fprintf ppf " %a" U.print v) glb.tenv_names

let do_typ loc r = 
  let s = compile_slot r in
  flush_defs ();
  flush_fv ();
  if IdSet.is_empty (fv_slot s) then typ_node s
  else raise_loc_generic loc "Capture variables are not allowed in types"
   
let typ glb p =
  do_typ p.loc (derecurs glb p)
    
let pat glb p = 
  let s = compile_slot (derecurs glb p) in
  flush_defs ();
  flush_fv ();
  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 op = [ `Unary of tenv -> Typed.unary_op | `Binary of tenv -> Typed.binary_op ]
let op_table : (string,op) Hashtbl.t = Hashtbl.create 31
let register_unary_op s f = Hashtbl.add op_table s (`Unary f)
let register_binary_op s f = Hashtbl.add op_table s (`Binary f)
let find_op s = Hashtbl.find op_table s


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 rec expr glb loc = function
  | LocatedExpr (loc,e) -> expr glb loc e
  | Forget (e,t) ->
      let (fv,e) = expr glb loc e and t = typ glb t in
      exp loc fv (Typed.Forget (e,t))
  | Var s -> 
      exp loc (Fv.singleton s) (Typed.Var s)
  | Apply (e1,e2) -> 
      let (fv1,e1) = expr glb loc e1 and (fv2,e2) = expr glb loc e2 in
      exp loc (Fv.cup fv1 fv2) (Typed.Apply (e1,e2))
  | Abstraction a ->
      let iface = List.map (fun (t1,t2) -> (typ glb t1, typ glb 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 (fv0,body) = branches glb 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
  | Cst c -> 
      exp loc Fv.empty (Typed.Cst (const glb loc c))
  | Pair (e1,e2) ->
      let (fv1,e1) = expr glb loc e1 and (fv2,e2) = expr glb loc e2 in
      exp loc (Fv.cup fv1 fv2) (Typed.Pair (e1,e2))
  | Xml (e1,e2) ->
      let (fv1,e1) = expr glb loc e1 and (fv2,e2) = expr glb loc e2 in
      exp loc (Fv.cup fv1 fv2) (Typed.Xml (e1,e2))
  | Dot (e,l) ->
      let (fv,e) = expr glb loc e in
      exp loc fv (Typed.Dot (e,parse_label glb loc l))
  | RemoveField (e,l) ->
      let (fv,e) = expr glb loc e in
      exp loc fv (Typed.RemoveField (e,parse_label glb loc l))
  | RecordLitt r -> 
      let fv = ref Fv.empty in
      let r = parse_record glb loc
                (fun e -> 
                   let (fv2,e) = expr glb 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 glb loc e in
      exp loc fv (Typed.String (i,j,s,e))
  | Op (op,le) ->
      let (fvs,ltes) = List.split (List.map (expr glb loc) le) in
      let fv = List.fold_left Fv.cup Fv.empty fvs in
      (try
         (match (ltes,find_op op) with
            | [e], `Unary op -> exp loc fv (Typed.UnaryOp (op glb, e))
            | [e1;e2], `Binary op -> exp loc fv (Typed.BinaryOp (op glb, e1,e2))
            | _ -> assert false)
       with Not_found -> assert false)

  | Match (e,b) -> 
      let (fv1,e) = expr glb loc e
      and (fv2,b) = branches glb b in
      exp loc (Fv.cup fv1 fv2) (Typed.Match (e, b))
  | Map (e,b) ->
      let (fv1,e) = expr glb loc e
      and (fv2,b) = branches glb b in
      exp loc (Fv.cup fv1 fv2) (Typed.Map (e, b))
  | Transform (e,b) ->
      let (fv1,e) = expr glb loc e
      and (fv2,b) = branches glb b in
      exp loc (Fv.cup fv1 fv2) (Typed.Transform (e, b))
  | Xtrans (e,b) ->
      let (fv1,e) = expr glb loc e
      and (fv2,b) = branches glb b in
      exp loc (Fv.cup fv1 fv2) (Typed.Xtrans (e, b))
  | Validate (e,schema,elt) ->
      let (fv,e) = expr glb loc e in
      exp loc fv (Typed.Validate (e, schema, elt))
  | Try (e,b) ->
      let (fv1,e) = expr glb loc e
      and (fv2,b) = branches glb b in
      exp loc (Fv.cup fv1 fv2) (Typed.Try (e, b))
  | NamespaceIn (pr,ns,e) ->
      let glb = register_ns_prefix glb pr ns in
      expr glb loc e

              
  and branches glb 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 (fv2,e) = expr glb noloc e in
      let br_loc = merge_loc p.loc e.Typed.exp_loc in
      let p = pat glb p in
      let fv2 = Fv.diff fv2 (Patterns.fv p) 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 glb = expr glb noloc

let let_decl glb p e =
  let (_,e) = expr glb e in
  { Typed.let_pat = pat glb p;
    Typed.let_body = e;
    Typed.let_compiled = None }


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

let glb = State.ref "Typer.glb_env" 
            { tenv_names = TypeEnv.empty;
              tenv_nspref = Ns.empty_table;
              tenv_loc = noloc }

let pat p = pat !glb p
let typ t = typ !glb t
let expr e = expr !glb e
let let_decl p e = let_decl !glb p e

let register_global_types l = glb := register_global_types !glb l
let dump_global_types ppf = dump_global_types ppf !glb

let register_ns_prefix p ns = glb := register_ns_prefix !glb p ns

(* III. Type-checks *)

type env = Types.descr Env.t

open Typed

let require loc t s = 
  if not (Types.subtype t s) then raise_loc loc (Constraint (t, s))

let check loc t s = 
  require loc 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 loc 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
    Sequence.flatten t

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);
      check 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 -> Env.add 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) ->
      flatten loc (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
      check loc res constr

  | UnaryOp (o,e) ->
      let t = o.un_op_typer loc 
                (type_check env e) constr precise in
      check loc t constr

  | BinaryOp (o,e1,e2) ->
      let t = o.bin_op_typer loc 
                (type_check env e1) 
                (type_check env e2) constr precise in
      check loc t constr

  | Var s -> 
      let t = 
        try Env.find s env
        with Not_found -> raise_loc loc (UnboundId s) in
      check loc t constr
      
  | Cst c -> 
      check 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
      check 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
      check 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
      check loc t constr

  | Validate (e, schema_name, elt_name) ->
      ignore (type_check env e Types.any false);
      let t = fst (Hashtbl.find !schema_elements (schema_name, elt_name)) in
      check loc t constr

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.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
  check 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 env' = List.fold_left 
                       (fun env (x,t) -> Env.add x (Types.descr t) env) 
                       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
          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 Types.cup res Sequence.nil_type
         else res)
      t in
  if exact then res else check 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 types = 
    List.fold_left
      (fun accu -> function  
         | { exp_descr=Abstraction { fun_typ = t; fun_name = Some f } } ->
             (f,t) :: accu
         | _ -> assert false
      ) [] l
  in
  let env' = List.fold_left (fun env (x,t) -> Env.add x t env) env types in
  List.iter (fun e -> ignore (type_check env' e Types.any false)) l;
  types


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 := []

  (* Schema stuff from now on ... *)

let debug = true

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

      (* build a regexp Elem from a Types.descr *)
    let mk_re_elt descr = PElem descr

    (* conversion functions *)

    let cd_type_of_simple_type = function
      | SBuilt_in name -> PType (Schema_builtin.cd_type_of_builtin name)
      | SUser_defined (_, _, _, _) -> assert false (* TODO *)

    let complex_memo = Hashtbl.create 213

    let rec regexp_of_term = function
      | All [] | Choice [] | Sequence [] -> PEpsilon
      | Choice (hd :: tl) ->
          List.fold_left
            (fun acc particle -> PAlt (acc, regexp_of_particle particle))
            (regexp_of_particle hd) tl
      | All (hd :: tl) | Sequence (hd :: tl) ->
          List.fold_left
            (fun acc particle -> PSeq (acc, regexp_of_particle particle))
            (regexp_of_particle hd) tl
      | Elt decl -> mk_re_elt (cd_type_of_elt_decl !decl)

    and regexp_of_content_type = function
      | CT_empty -> PEpsilon
      | CT_simple st -> mk_re_elt (cd_type_of_simple_type st)
      | CT_model (particle, mixed) ->
          assert (not mixed); (* TODO mixed support *)
          regexp_of_particle particle

    and regexp_of_particle =
        (* given a regexp re and a (non negative) integer n create a regexp
        matching exactly n times re *)
      let rec repeat_regexp re = function
        | 0 -> PEpsilon
        | n when n > 0 -> PSeq (re, repeat_regexp re (n - 1))
        | _ -> assert false
      in
      fun (min, max, term) ->
        let term_regexp = regexp_of_term term in
        let min_regexp = repeat_regexp term_regexp min in
        match max with
        | Some max ->
            assert (max >= min);
            let rec aux acc = function
              | 0 -> acc
              | n ->
                  aux
                    (PAlt (PEpsilon, (PSeq (term_regexp, acc))))
                    (n - 1)
            in
            PSeq (min_regexp, aux PEpsilon (max - min))
        | None -> PSeq (min_regexp, PStar term_regexp)

      (** @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' = function
      | CBuilt_in name -> assert false
      | CUser_defined (id, name, _, _, attr_uses, content) ->
          try PAlias (Hashtbl.find complex_memo id)
          with Not_found -> 
            let slot = mk_slot noloc in
            Hashtbl.add complex_memo id slot;
            let content_re = regexp_of_content_type content in
            let content_ast_node = PRegexp (content_re, PType Sequence.nil_type) in
            slot.pdescr <- Some 
              (PTimes (cd_type_of_attr_uses attr_uses, content_ast_node));
            PAlias slot
            

(* TODO if constraint is Fixed we can give a more precise CDuce type *)

      (** @return a closed record *)
    and cd_type_of_attr_uses attr_uses =
      let fields = 
        List.map 
          (fun (required, (name, st, _), _) ->
             let r = cd_type_of_simple_type st in
             let r = if required then r else POptional r in
             (LabelPool.mk (Ns.empty, U.mk name), r)  (* TODO: NS *)
          ) attr_uses in
      PRecord (false, LabelMap.from_list_disj fields)

    and cd_type_of_att_decl (name, st, _) =
      let r = cd_type_of_simple_type st in
      PRecord (false, LabelMap.from_list_disj [(LabelPool.mk (Ns.empty, U.mk name), r)])
        (* TODO: NS *)

    and cd_type_of_elt_decl (name, typ, _) =
      let atom_type = PType (Types.atom (Atoms.atom (Atoms.mk Ns.empty (U.mk name)))) in
      let content = match !typ with
        | S st ->
            PTimes (PType Types.empty_closed_record, cd_type_of_simple_type st)
        | C ct -> cd_type_of_complex_type' ct
      in
      PXml (atom_type, content)

    let typ r = Types.descr (do_typ noloc r)

    let cd_type_of_complex_type = function
      | CBuilt_in name -> Schema_builtin.cd_type_of_builtin name
      | ct -> typ (PXml (PType Types.any, cd_type_of_complex_type' ct))

    let cd_type_of_type_def = function
      | S st -> typ (cd_type_of_simple_type st)
      | C ct -> cd_type_of_complex_type ct

    let cd_type_of_elt_decl x = typ (cd_type_of_elt_decl x)
    let cd_type_of_att_decl x = typ (cd_type_of_att_decl x)

  end

let get_schema_validator (schema_name, elt_name) =
  snd (Hashtbl.find !schema_elements (schema_name, elt_name))

let register_schema schema_name schema =
  if StringSet.mem schema_name !schemas then
    failwith ("Redefinition of schema " ^ schema_name)
  else begin
    schemas := StringSet.add schema_name !schemas;
    List.iter (* Schema types -> CDuce types *)
      (fun type_def ->
        let cd_type = Schema_converter.cd_type_of_type_def type_def in
        Hashtbl.add !schema_types
          (schema_name, Schema_types.name_of_type_def type_def)
          cd_type)
      schema.Schema_types.type_defs;
    List.iter (* Schema attributes -> CDuce types *)
      (fun (att_name, _, _) as att_decl ->
        let cd_type = Schema_converter.cd_type_of_att_decl att_decl in
        Hashtbl.add !schema_attributes (schema_name, att_name) cd_type)
      schema.Schema_types.att_decls;
    List.iter (* Schema elements -> CDuce types * validators *)
      (fun elt_decl ->
        let cd_type = Schema_converter.cd_type_of_elt_decl elt_decl in
        if debug then
          (Types.Print.print Format.std_formatter cd_type;
          Format.fprintf Format.std_formatter "\n";
          Format.pp_print_flush Format.std_formatter ());
        let validator = Schema_validator.validator_of_elt_decl elt_decl in
        Hashtbl.add !schema_elements
          (schema_name, Schema_types.name_of_elt_decl elt_decl)
          (cd_type, validator))
      schema.Schema_types.elt_decls
  end

(* DEBUGGING ONLY *)

let get_schema_type x = fst (Hashtbl.find !schema_elements x)