typer.ml

(* TODO:
 - rewrite type-checking of operators to propagate constraint
 - rewrite translation of types and patterns -> hash cons
     CONTINUE THIS...
     Problem with same name for recursive binders in different
     recursive type/patterns definitions because of hash-consing
*)


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

open Location
open Ast
open Ident

module S = struct type t = string let compare = compare end
module StringSet = Set.Make(S)
module TypeEnv = Map.Make(S)
module Env = Map.Make(Ident.Id)


exception NonExhaustive of Types.descr
exception Constraint of Types.descr * Types.descr * string
exception ShouldHave of Types.descr * string
exception WrongLabel of Types.descr * label
exception UnboundId of string

let raise_loc loc exn = raise (Location (loc,exn))

(* Note:
   Compilation of Regexp is implemented as a ``rewriting'' of
   the parsed syntax, in order to be able to print its result
   (for debugging for instance)
   
   It would be possible (and a little more efficient) to produce
   directly ti nodes.
*)
    
module Regexp = struct
  let defs = ref []
  let name =
    let c = ref 0 in
    fun () ->
      incr c;
      "#" ^ (string_of_int !c)

  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

  let uniq_id = let r = ref 0 in fun () -> incr r; !r

  type flat =  
    | REpsilon 
    | RElem of int * Ast.ppat  (* the int arg is used
					    to stop generic comparison *)
    | RSeq of flat * flat
    | RAlt of flat * flat
    | RStar of flat
    | RWeakStar of flat

  let re_loc = ref noloc

  let rec propagate vars : regexp -> flat = function
    | Epsilon -> REpsilon
    | Elem x -> let p = vars x in RElem (uniq_id (),p)
    | Seq (r1,r2) -> RSeq (propagate vars r1,propagate vars r2)
    | Alt (r1,r2) -> RAlt (propagate vars r1, propagate vars r2)
    | Star r -> RStar (propagate vars r)
    | WeakStar r -> RWeakStar (propagate vars r)
    | SeqCapture (v,x) -> 
	let v= mk_loc !re_loc (Capture v) in
	propagate (fun p -> mk_loc !re_loc (And (vars p,v))) x

  let dummy_pat = mknoloc (PatVar "DUMMY")
  let cup r1 r2 =
    if r1 == dummy_pat then r2 else
      if r2 == dummy_pat then r1 else
	mk_loc !re_loc (Or (r1,r2))

(*TODO: review this compilation schema to avoid explosion when
  coding (Optional x) by  (Or(Epsilon,x)); memoization ... *)

  module Memo = Map.Make(struct type t = flat list let compare = compare end)
  module Coind = Set.Make(struct type t = flat list let compare = compare end)
  let memo = ref Memo.empty


  let rec compile fin e seq : Ast.ppat = 
    if Coind.mem seq !e then dummy_pat
    else (
      e := Coind.add seq !e;
      match seq with
	| [] ->
	    fin
	| REpsilon :: rest -> 
	    compile fin e rest
	| RElem (_,p) :: rest -> 
	    mk_loc !re_loc (Prod (p, guard_compile fin rest))
	| RSeq (r1,r2) :: rest -> 
	    compile fin e (r1 :: r2 :: rest)
	| RAlt (r1,r2) :: rest -> 
	    cup (compile fin e (r1::rest)) (compile fin e (r2::rest))
	| RStar r :: rest -> 
	    cup (compile fin e (r::seq)) (compile fin e rest) 
	| RWeakStar r :: rest -> 
	    cup (compile fin e rest) (compile fin e (r::seq))
    )
  and guard_compile fin seq =
    try Memo.find seq !memo
    with
	Not_found ->
          let n = name () in
	  let v = mk_loc !re_loc (PatVar n) in
          memo := Memo.add seq v !memo;
	  let d = compile fin (ref Coind.empty) seq in
	  assert (d != dummy_pat);
	  defs := (n,d) :: !defs;
	  v

  let constant_nil t v = 
    mk_loc !re_loc 
      (And (t, (mk_loc !re_loc (Constant (v, Types.Atom Sequence.nil_atom)))))

  let compile loc regexp queue : ppat =
    re_loc := loc;
    let vars = seq_vars IdSet.empty regexp in
    let fin = IdSet.fold constant_nil queue vars in
    let re = propagate (fun p -> p) regexp in
    let n = guard_compile fin [re] in
    memo := Memo.empty; 
    let d = !defs in
    defs := [];
    mk_loc !re_loc (Recurs (n,d))

(*
  module H = Hashtbl.Make(
    struct
      type t = Ast.regexp * Ast.ppat
      let equal (r1,p1) (r2,p2) = 
	(Ast.equal_regexp r1 r2) &&
	(Ast.equal_ppat p1 p2)
      let hash (r,p) = 
	(Ast.hash_regexp r) + 16637 * (Ast.hash_ppat p)
    end)
  let hash = H.create 67

  let compile loc regexp queue : ppat =
    try 
      let c = H.find hash (regexp,queue) in
(*      Printf.eprintf "regexp cached\n"; flush stderr; *)
      c
    with
	Not_found ->
	  let c = compile loc regexp queue in
	  H.add hash (regexp,queue) c;
	  c
*)
end

(*
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 slot 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    : slot 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 = 
  (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 = incr gen; rank := 0; equal_slot s1 s2
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
  | 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
  | _ -> IdSet.empty
      
let compute_fv s =
  match s.fv with
    | Some x -> ()
    | None ->
	incr gen;
	let x = fv_slot s in
	s.fv <- Some x
	  
	  
let counter = ref 0
let todo = ref []
let rec flush_fv () =
  List.iter compute_fv !todo;
  todo := []
    
let mk () =   
  let s = 
    { d = None;
      fv = None;
      hash = None;
      rank1 = 0; rank2 = 0;
      gen1 = 0; gen2 = 0 } in
  todo := s :: !todo;
  s
    
let compile_hash = Ast.PpatTable.create 65
let defs = ref []
let rec compile env { loc = loc; descr = d } = 
  match (d : Ast.ppat') with
    | PatVar v -> 
	let (d,loop) = 
	  try TypeEnv.find v env
	  with Not_found -> 
	    raise_loc_generic loc ("Undefined type variable " ^ v) in
	if !loop then 
	  raise_loc_generic loc ("Unguarded recursion on type/pattern variable " ^ v);
	loop := true;
	let r = compile env d in
	loop := false;
	r
    | Recurs (t, b) -> compile (compile_many env b) t
    | Regexp (r,q) -> compile env (Regexp.compile loc r q)
    | Internal t -> IType t
    | Or (t1,t2) -> IOr (compile env t1, compile env t2)
    | And (t1,t2) -> IAnd (compile env t1, compile env t2)
    | Diff (t1,t2) -> IDiff (compile env t1, compile env t2)
    | Prod (t1,t2) -> ITimes (compile_slot env t1, compile_slot env t2)
    | XmlT (t1,t2) -> IXml (compile_slot env t1, compile_slot env t2)
    | Arrow (t1,t2) -> IArrow (compile_slot env t1, compile_slot env t2)
    | Optional t -> IOptional (compile env t)
    | Record (o,r) ->  IRecord (o, LabelMap.map (compile_slot env) r)
    | Constant (x,v) -> IConstant (x,v)
    | Capture x -> ICapture x
and compile_slot env ({ loc = loc; descr = d } as p) =
  try Ast.PpatTable.find compile_hash p
  with Not_found ->
    let s = mk () in
    defs := (s,p,env) :: !defs;
    Ast.PpatTable.add compile_hash p s;
    s
      
and compile_many env b = 
  List.fold_left (fun env (v,p) -> TypeEnv.add v (p,ref false) env) env b
    
let rec flush_defs () = 
  match !defs with
    | [] -> ()
    | (s,p,env)::t -> defs := t; s.d <- Some (compile env 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 glb = State.ref "Typer.glb_env" TypeEnv.empty
	    
	    
let register_global_types b =
  List.iter (fun (v, { loc = loc }) ->
	       if TypeEnv.mem v !glb
	       then raise_loc_generic loc ("Multiple definition for type " ^ v)
	    ) b;
  glb := compile_many !glb b;
  let b = List.map (fun (v,p) -> (v,p,compile !glb p)) b in
  flush_defs ();
  flush_fv ();
  List.iter (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";
	       Types.Print.register_global v (typ s)) b
    
    
let typ p =
  let s = compile_slot !glb p in
  flush_defs ();
  flush_fv ();
  if IdSet.is_empty (fv_slot s) then typ_node s
  else raise_loc_generic p.loc "Capture variables are not allowed in types"
    
let pat p = 
  let s = compile_slot !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, exn))
	
	
*)

(* Internal representation as a graph (desugar recursive types and regexp),
   to compute freevars, etc... *)

type ti = {
  id : int; 
  mutable seen : bool;
  mutable loc' : loc;
  mutable fv : fv option; 
  mutable descr': descr;
  mutable type_node: Types.node option;
  mutable pat_node: Patterns.node option
} 
and descr =
  | IAlias of string * ti
  | IType of Types.descr
  | IOr of ti * ti
  | IAnd of ti * ti
  | IDiff of ti * ti
  | ITimes of ti * ti
  | IXml of ti * ti
  | IArrow of ti * ti
  | IOptional of ti
  | IRecord of bool * ti label_map
  | ICapture of id
  | IConstant of id * Types.const



type glb = ti TypeEnv.t

let mk' =
  let counter = ref 0 in
  fun loc ->
    incr counter;
    let rec x = { 
      id = !counter; 
      seen = false;
      loc' = loc; 
      fv = None; 
      descr' = IAlias ("__dummy__", x);
      type_node = None; 
      pat_node = None 
    } in
    x

let cons loc d =
  let x = mk' loc in
  x.descr' <- d;
  x
    


let rec compile env { loc = loc; descr = d } : ti = 
  match (d : Ast.ppat') with
  | PatVar s -> 
      (try TypeEnv.find s env
       with Not_found -> 
	 raise_loc_generic loc ("Undefined type variable " ^ s)
      )
  | Recurs (t, b) -> compile (compile_many env b) t
  | Regexp (r,q) -> compile env (Regexp.compile loc r q)
  | Internal t -> cons loc (IType t)
  | Or (t1,t2) -> cons loc (IOr (compile env t1, compile env t2))
  | And (t1,t2) -> cons loc (IAnd (compile env t1, compile env t2))
  | Diff (t1,t2) -> cons loc (IDiff (compile env t1, compile env t2))
  | Prod (t1,t2) -> cons loc (ITimes (compile env t1, compile env t2))
  | XmlT (t1,t2) -> cons loc (IXml (compile env t1, compile env t2))
  | Arrow (t1,t2) -> cons loc (IArrow (compile env t1, compile env t2))
  | Optional t -> cons loc (IOptional (compile env t))
  | Record (o,r) ->  cons loc (IRecord (o, LabelMap.map (compile env) r))
  | Constant (x,v) -> cons loc (IConstant (x,v))
  | Capture x -> cons loc (ICapture x)

and compile_many env b = 
  let b = List.map (fun (v,t) -> (v,t,mk' t.loc)) b in
  let env = 
    List.fold_left (fun env (v,t,x) -> TypeEnv.add v x env) env b in
  List.iter (fun (v,t,x) -> x.descr' <- IAlias (v, compile env t)) b;
  env

module IntSet = 
  Set.Make(struct type t = int let compare (x:int) y = compare x y end)

let comp_fv_seen = ref []
let comp_fv_res = ref IdSet.empty
let rec comp_fv s =
  match s.fv with
    | Some fv -> comp_fv_res := IdSet.cup fv !comp_fv_res
    | None ->
	(match s.descr' with
	   | IAlias (_,x) -> 
	       if x.seen then ()
	       else ( 
		 x.seen <- true;
		 comp_fv_seen := x :: !comp_fv_seen; 
		 comp_fv x
	       ) 
	   | IOr (s1,s2) 
	   | IAnd (s1,s2)
	   | IDiff (s1,s2)
	   | ITimes (s1,s2) | IXml (s1,s2)
	   | IArrow (s1,s2) -> comp_fv s1; comp_fv s2
	   | IOptional r -> comp_fv r
	   | IRecord (_,r) -> LabelMap.iter comp_fv r
	   | IType _ -> ()
	   | ICapture x
	   | IConstant (x,_) -> comp_fv_res := IdSet.add x !comp_fv_res
	)


let fv s =   
  match s.fv with
    | Some l -> l
    | None -> 
	comp_fv s;
	let l = !comp_fv_res in
	comp_fv_res := IdSet.empty;
	List.iter (fun n -> n.seen <- false) !comp_fv_seen;
	comp_fv_seen := [];
	s.fv <- Some l; 
	l

let rec typ seen s : Types.descr =
  match s.descr' with
    | IAlias (v,x) ->
	if IntSet.mem s.id seen then 
	  raise_loc_generic s.loc' 
	    ("Unguarded recursion on variable " ^ v ^ " in this type")
	else typ (IntSet.add s.id seen) x
    | IType t -> t
    | IOr (s1,s2) -> Types.cup (typ seen s1) (typ seen s2)
    | IAnd (s1,s2) ->  Types.cap (typ seen s1) (typ seen s2)
    | IDiff (s1,s2) -> Types.diff (typ seen s1) (typ seen 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 seen s)
    | IRecord (o,r) -> 
	Types.record' 
	  (o, LabelMap.map typ_node r)
    | ICapture x | IConstant (x,_) -> assert false

and typ_node s : Types.node =
  match s.type_node with
    | Some x -> x
    | None ->
	let x = Types.make () in
	s.type_node <- Some x;
	let t = typ IntSet.empty s in
	Types.define x t;
	x

let type_node s = 
  let s = typ_node s in
  let s = Types.internalize s in
(*  Types.define s (Types.normalize (Types.descr s)); *)
  s

let rec pat seen s : Patterns.descr =
  if IdSet.is_empty (fv s) 
  then Patterns.constr (Types.descr (type_node s)) 
  else
    try pat_aux seen s
    with Patterns.Error e -> raise_loc_generic s.loc' e
      | Location (loc,exn) when loc = noloc -> raise (Location (s.loc', exn))


and pat_aux seen s = match s.descr' with
  | IAlias (v,x) ->
      if IntSet.mem s.id seen 
      then raise 
	(Patterns.Error
	   ("Unguarded recursion on variable " ^ v ^ " in this pattern"));
      pat (IntSet.add s.id seen) x
  | IOr (s1,s2) -> Patterns.cup (pat seen s1) (pat seen s2)
  | IAnd (s1,s2) -> Patterns.cap (pat seen s1) (pat seen s2)
  | IDiff (s1,s2) when IdSet.is_empty (fv s2) ->
      let s2 = Types.neg (Types.descr (type_node s2)) in
      Patterns.cap (pat seen 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 s) then type_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 =
  match s.pat_node with
    | Some x -> x
    | None ->
	let x = Patterns.make (fv s) in
	s.pat_node <- Some x;
	let t = pat IntSet.empty s in
	Patterns.define x t;
	x

let mk_typ e =
  if IdSet.is_empty (fv e) then type_node e
  else raise_loc_generic e.loc' "Capture variables are not allowed in types"
    

let glb = State.ref "Typer.glb_env" TypeEnv.empty

let typ e =
  mk_typ (compile !glb e)

let pat e =
  pat_node (compile !glb e)

let register_global_types b =
  let env' = compile_many !glb b in
  List.iter
    (fun (v,{ loc = loc }) -> 
       let t = TypeEnv.find v env' in
       let d = Types.descr (mk_typ t) in
       (*	       let d = Types.normalize d in*)
       Types.Print.register_global v d;
       if TypeEnv.mem v !glb
       then raise_loc_generic loc ("Multiple definition for type " ^ v);
       glb := TypeEnv.add v t !glb
    ) b



(* II. Build skeleton *)

module Fv = IdSet

(* IDEA: introduce a node Loc in the AST to override nolocs
   in sub-expressions *)
   
let rec expr loc' { loc = loc; descr = d } = 
  let loc =  if loc = noloc then loc' else loc in
  let (fv,td) = 
    match d with
      | Forget (e,t) ->
	  let (fv,e) = expr loc e and t = typ t in
	  (fv, Typed.Forget (e,t))
      | Var s -> (Fv.singleton s, Typed.Var s)
      | Apply (e1,e2) -> 
	  let (fv1,e1) = expr loc e1 and (fv2,e2) = expr loc e2 in
	  (Fv.cup fv1 fv2, Typed.Apply (e1,e2))
      | Abstraction a ->
	  let iface = List.map (fun (t1,t2) -> (typ t1, typ 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 loc a.fun_body in
	  let fv = match a.fun_name with
	    | None -> fv0
	    | Some f -> Fv.remove f fv0 in
	  (fv,
	   Typed.Abstraction 
	     { Typed.fun_name = a.fun_name;
	       Typed.fun_iface = iface;
	       Typed.fun_body = body;
	       Typed.fun_typ = t;
	       Typed.fun_fv = fv
	     }
	  )
      | Cst c -> (Fv.empty, Typed.Cst c)
      | Pair (e1,e2) ->
	  let (fv1,e1) = expr loc e1 and (fv2,e2) = expr loc e2 in
	  (Fv.cup fv1 fv2, Typed.Pair (e1,e2))
      | Xml (e1,e2) ->
	  let (fv1,e1) = expr loc e1 and (fv2,e2) = expr loc e2 in
	  (Fv.cup fv1 fv2, Typed.Xml (e1,e2))
      | Dot (e,l) ->
	  let (fv,e) = expr loc e in
	  (fv,  Typed.Dot (e,l))
      | RemoveField (e,l) ->
	  let (fv,e) = expr loc e in
	  (fv,  Typed.RemoveField (e,l))
      | RecordLitt r -> 
	  let fv = ref Fv.empty in
	  let r = LabelMap.map 
		    (fun e -> 
		       let (fv2,e) = expr loc e 
		       in fv := Fv.cup !fv fv2; e)
		    r in
	  (!fv, Typed.RecordLitt r)
      | Op (op,le) ->
	  let (fvs,ltes) = List.split (List.map (expr loc) le) in
	  let fv = List.fold_left Fv.cup Fv.empty fvs in
	  (fv, Typed.Op (op,ltes))
      | Match (e,b) -> 
	  let (fv1,e) = expr loc e
	  and (fv2,b) = branches loc b in
	  (Fv.cup fv1 fv2, Typed.Match (e, b))
      | Map (e,b) ->
	  let (fv1,e) = expr loc e
	  and (fv2,b) = branches loc b in
	  (Fv.cup fv1 fv2, Typed.Map (e, b))
      | Ttree (e,b) ->
	  let b = b @ [ (mknoloc (Internal Types.any)), mknoloc MatchFail ] in
	  let (fv1,e) = expr loc e
	  and (fv2,b) = branches loc b in
	  (Fv.cup fv1 fv2, Typed.Ttree (e, b))
      | MatchFail -> (Fv.empty, Typed.MatchFail)
      | Try (e,b) ->
	  let (fv1,e) = expr loc e
	  and (fv2,b) = branches loc b in
	  (Fv.cup fv1 fv2, Typed.Try (e, b))
  in
  fv,
  { Typed.exp_loc = loc;
    Typed.exp_typ = Types.empty;
    Typed.exp_descr = td;
  }
	      
  and branches loc b = 
    let fv = ref Fv.empty in
    let accept = ref Types.empty in
    let b = List.map 
	      (fun (p,e) ->
		 let (fv2,e) = expr loc e in
		 let p = pat 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));
		 { Typed.br_used = false;
		   Typed.br_pat = p;
		   Typed.br_body = e }
	      ) b in
    (!fv, 
     { 
       Typed.br_typ = Types.empty; 
       Typed.br_branches = b; 
       Typed.br_accept = !accept;
       Typed.br_compiled = None;
     } 
    )

let expr = expr noloc

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

(* III. Type-checks *)

let int_cup_record = Types.cup Types.Int.any Types.Record.any


type env = Types.descr Env.t

let match_fail = ref Types.empty

open Typed

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

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

let rec type_check env e constr precise = 
(*  Format.fprintf Format.std_formatter "constr=%a precise=%b@\n"
    Types.Print.print_descr constr precise; 
*)
  let d = type_check' e.exp_loc env e.exp_descr constr precise in
  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);
      t
  | Abstraction a ->
      let t =
	try Types.Arrow.check_strenghten a.fun_typ constr 
	with Not_found -> 
	  raise_loc loc 
	  (ShouldHave
	     (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) ->
	   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 ->
(* try to get rid of precise = true for values of fields *)
      if not (Types.Record.has_record constr) then
	raise_loc loc (ShouldHave (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 
	       raise_loc loc 
		 (ShouldHave (constr,(Printf.sprintf 
					"Field %s is not allowed here."
					(LabelPool.value l)
				     )
			     ));
	     let t = type_check env e pi true in
	     let rconstr = Types.Record.condition rconstr l t in
	     let res = if precise then (l,Types.cons t) :: res else res in
	     (rconstr,res)
	  ) (constr, []) (LabelMap.get r)
      in
      if not (Types.Record.has_empty_record rconstr) then
	raise_loc loc 
	  (ShouldHave (constr,"More field should be present"));
      if precise then
	Types.record' (false, LabelMap.from_list (fun _ _ -> assert false) res)
      else constr
  | Map (e,b) ->
      let t = type_check env e (Sequence.star b.br_accept) 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 -> 
	     type_check_branches loc env t b constr' (precise || (not exact)))
	  t in
      if not exact then check loc res constr "";
      if precise then res else constr
  | Op ("@", [e1;e2]) ->
      let constr' = Sequence.star 
		      (Sequence.approx (Types.cap Sequence.any constr)) in
      let exact = Types.subtype constr' constr in
      if exact then
	let t1 = type_check env e1 constr' precise
	and t2 = type_check env e2 constr' precise in
	if precise then Sequence.concat t1 t2 else constr
      else
	(* Note:
	   the knownledge of t1 may makes it useless to
	   check t2 with 'precise' ... *)
	let t1 = type_check env e1 constr' true
	and t2 = type_check env e2 constr' true in
	let res = Sequence.concat t1 t2 in
	check loc res constr "";
	if precise then res else constr
  | Apply (e1,e2) ->
(*
      let constr' = Sequence.star 
		      (Sequence.approx (Types.cap Sequence.any constr)) in
      let t1 = type_check env e1 (Types.cup Types.Arrow.any constr') true in
      let t1_fun = Types.Arrow.get t1 in

      let has_fun = not (Types.Arrow.is_empty t1_fun)
      and has_seq = not (Types.subtype t1 Types.Arrow.any) in

      let constr' =
	Types.cap 
	  (if has_fun then Types.Arrow.domain t1_fun else Types.any)
	  (if has_seq then constr' else Types.any)
      in
      let need_arg = has_fun && Types.Arrow.need_arg t1_fun in
      let precise  = need_arg || has_seq in
      let t2 = type_check env e2 constr' precise in
      let res = Types.cup 
		  (if has_fun then 
		     if need_arg then Types.Arrow.apply t1_fun t2
		     else Types.Arrow.apply_noarg t1_fun
		   else Types.empty)
		  (if has_seq then Sequence.concat t1 t2
		   else Types.empty)
      in
      check loc res constr "";
      res
*)
      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 "";
      res
  | Op ("flatten", [e]) ->
      let constr' = Sequence.star 
		      (Sequence.approx (Types.cap Sequence.any constr)) in
      let sconstr' = Sequence.star constr' in
      let exact = Types.subtype constr' constr in
      if exact then
	let t = type_check env e sconstr' precise in
	if precise then Sequence.flatten t else constr
      else
	let t = type_check env e sconstr' true in
	let res = Sequence.flatten t in
	check loc res constr "";
	if precise then res else constr
  | _ -> 
      let t : Types.descr = compute_type' loc env e in
      check loc t constr "";
      t

and type_check_pair ?(kind=`Normal) loc env e1 e2 constr precise =
  let rects = Types.Product.get ~kind constr in
  if Types.Product.is_empty rects then 
    (match kind with
      | `Normal -> raise_loc loc (ShouldHave (constr,"but it is a pair."))
      | `XML -> raise_loc loc (ShouldHave (constr,"but it is an XML element.")));
  let pi1 = Types.Product.pi1 rects in
  
  let t1 = type_check env e1 (Types.Product.pi1 rects) 
	     (precise || (Types.Product.need_second rects))in
  let rects = Types.Product.restrict_1 rects t1 in
  let t2 = type_check env e2 (Types.Product.pi2 rects) 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 compute_type env e =
  type_check env e Types.any true

and compute_type' loc env = function
  | Var s -> 
      (try Env.find s env 
       with Not_found -> raise_loc loc (UnboundId (Id.value s))
      )
  | Cst c -> Types.constant c
  | Dot (e,l) ->
      let t = type_check env e Types.Record.any true in
         (try (Types.Record.project t l) 
          with Not_found -> raise_loc loc (WrongLabel(t,l)))
  | RemoveField (e,l) ->
      let t = type_check env e Types.Record.any true in
      Types.Record.remove_field t l
  | Op (op, el) ->
      let args = List.map (fun e -> (e.exp_loc, compute_type env e)) el in
      type_op loc op args
  | Ttree (e,b) ->
      let t = type_check env e Sequence.any true in
      let r = 
	Sequence.map_tree 
	  (fun t -> 
	     let res = type_check_branches loc env t b Sequence.any true in
	     let resid = !match_fail in
	     match_fail := Types.empty;
	     (res,resid)
	  ) t
      in
      r

(* We keep these cases here to allow comparison and benchmarking ...
   Just comment the corresponding cases in type_check' to
   activate these ones.
*)
  | Map (e,b) ->
      let t = compute_type env e in
      Sequence.map (fun t -> type_check_branches loc env t b Types.any true) t
  | Pair (e1,e2) -> 
      let t1 = compute_type env e1 
      and t2 = compute_type env e2 in
      Types.times (Types.cons t1) (Types.cons t2)
  | RecordLitt r ->
      let r = LabelMap.map (fun e -> Types.cons (compute_type env e)) r in
      Types.record' (false,r)
  | _ -> assert false

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
  | [] -> raise_loc loc (NonExhaustive targ)
  | { br_body = { exp_descr = MatchFail } } :: _ ->
      match_fail := Types.cup !match_fail targ;
      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_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  {let_body={exp_descr=Abstraction a}} as l ->
	 let t = a.fun_typ in
	 let acc = Types.descr (Patterns.accept l.let_pat) in
	 if not (Types.subtype t acc) then
	   raise_loc l.let_body.exp_loc (NonExhaustive (Types.diff t acc));
	 let res = Patterns.filter t l.let_pat in
	 List.fold_left (fun accu (x,t) -> (x, Types.descr t)::accu) accu res
	 | _ -> assert false) [] l
  in
  let env' = List.fold_left (fun env (x,t) -> Env.add x t env) env types in
  List.iter 
    (function  { let_body = { exp_descr = Abstraction a } } as l ->
       ignore (type_check env' l.let_body Types.any false)
       | _ -> assert false) l;
  types


and type_op loc op args =
  match (op,args) with
    | "+", [loc1,t1; loc2,t2] ->
	check loc1 t1 int_cup_record
	"The first argument of + must be an integer or a record";
	let int = Types.Int.get t1 in
	let int = if Intervals.is_empty int then None else Some int in
	let r = if Types.Record.has_record t1 then Some t1 else None in
	(match (int,r) with
	   | Some t1, None ->
	       if not (Types.Int.is_int t2) then
		 raise_loc loc2
		   (Constraint 
		      (t2,Types.Int.any,
		       "The second argument of + must be an integer"));
	       Types.Int.put
		 (Intervals.add t1 (Types.Int.get t2));
	   | None, Some r1 ->
	       check loc2 t2 Types.Record.any 
	       "The second argument of + must be a record";
	       Types.Record.merge r1 t2
	   | None, None ->
	       Types.empty
	   | Some t1, Some r1 ->
	       check loc2 t2 int_cup_record
	       "The second argument of + must be an integer or a record";
	       Types.cup 
		 (Types.Int.put (Intervals.add t1 (Types.Int.get t2)))
		 (Types.Record.merge r1 t2)
	)
    | "-", [loc1,t1; loc2,t2] ->
	type_int_binop Intervals.sub loc1 t1 loc2 t2
    | ("*" | "/" | "mod"), [loc1,t1; loc2,t2] ->
	type_int_binop (fun i1 i2 -> Intervals.any) loc1 t1 loc2 t2
    | "@", [loc1,t1; loc2,t2] ->
	check loc1 t1 Sequence.any
	  "The first argument of @ must be a sequence";
	Sequence.concat t1 t2
    | "flatten", [loc1,t1] ->
	check loc1 t1 Sequence.seqseq 
	  "The argument of flatten must be a sequence of sequences";
	Sequence.flatten t1
    | "load_xml", [loc1,t1] ->
	check loc1 t1 Sequence.string
	  "The argument of load_xml must be a string (filename)";
	Types.any
    | "load_file", [loc1,t1] ->
	check loc1 t1 Sequence.string
	  "The argument of load_file must be a string (filename)";
	Sequence.string
    | "load_html", [loc1,t1] ->
	check loc1 t1 Sequence.string
	  "The argument of load_html must be a string (filename)";
	Types.any
    | "raise", [loc1,t1] ->
	Types.empty