typer.ml 24 KB
Newer Older
1 2
(* I. Transform the abstract syntax of types and patterns into
      the internal form *)
3 4 5 6

open Location
open Ast

7
exception NonExhaustive of Types.descr
8
exception MultipleLabel of Types.label
9
exception Constraint of Types.descr * Types.descr * string
10
exception ShouldHave of Types.descr * string
11
exception WrongLabel of Types.descr * Types.label
12
exception UnboundId of string
13 14

let raise_loc loc exn = raise (Location (loc,exn))
15 16 17 18

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

19
type ti = {
20 21 22 23 24 25 26 27
  id : int; 
  mutable loc' : loc;
  mutable fv : string SortedList.t option; 
  mutable descr': descr;
  mutable type_node: Types.node option;
  mutable pat_node: Patterns.node option
} 
and descr =
28
   [ `Alias of string * ti
29 30
   | `Type of Types.descr
   | `Or of ti * ti
31
   | `And of ti * ti * bool
32 33
   | `Diff of ti * ti
   | `Times of ti * ti
34
   | `Xml of ti * ti
35 36 37 38 39 40 41 42 43 44 45 46
   | `Arrow of ti * ti
   | `Record of Types.label * bool * ti
   | `Capture of Patterns.capture
   | `Constant of Patterns.capture * Types.const
   ]
    


module S = struct type t = string let compare = compare end
module StringMap = Map.Make(S)
module StringSet = Set.Make(S)

47 48
type glb = ti StringMap.t

49 50
let mk' =
  let counter = ref 0 in
51
  fun loc ->
52
    incr counter;
53 54
    let rec x = { 
      id = !counter; 
55
      loc' = loc; 
56 57 58 59 60
      fv = None; 
      descr' = `Alias ("__dummy__", x);  
      type_node = None; 
      pat_node = None 
    } in
61 62 63
    x

let cons loc d =
64
  let x = mk' loc in
65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90
  x.descr' <- d;
  x
    
(* Note:
   Compilation of Regexp is implemented as a ``rewriting'' of
   the parsed syntax, in order to be able to print its result
   (for debugging for instance)
   
   It would be possible (and a little more efficient) to produce
   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 (StringSet.add v accu) r

91 92 93 94 95 96 97 98 99 100
  let uniq_id = let r = ref 0 in fun () -> incr r; !r

  type flat = [ `Epsilon 
	      | `Elem of int * Ast.ppat  (* the int arg is used to
					    to stop generic comparison *)
	      | `Seq of flat * flat
	      | `Alt of flat * flat
	      | `Star of flat
	      | `WeakStar of flat ]

101 102
  let re_loc = ref noloc

103
  let rec propagate vars : regexp -> flat = function
104
    | Epsilon -> `Epsilon
105
    | Elem x -> let p = vars x in `Elem (uniq_id (),p)
106 107 108 109
    | Seq (r1,r2) -> `Seq (propagate vars r1,propagate vars r2)
    | Alt (r1,r2) -> `Alt (propagate vars r1, propagate vars r2)
    | Star r -> `Star (propagate vars r)
    | WeakStar r -> `WeakStar (propagate vars r)
110
    | SeqCapture (v,x) -> 
111 112
	let v= mk !re_loc (Capture v) in
	propagate (fun p -> mk !re_loc (And (vars p,v,true))) x
113 114 115 116 117

  let cup r1 r2 = 
    match (r1,r2) with
      | (_, `Empty) -> r1
      | (`Empty, _) -> r2
118
      | (`Res t1, `Res t2) -> `Res (mk !re_loc (Or (t1,t2)))
119

120 121 122 123 124 125 126
(*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

127
  let rec compile fin e seq : [`Res of Ast.ppat | `Empty] = 
128 129 130
    if Coind.mem seq !e then `Empty
    else (
      e := Coind.add seq !e;
131 132 133 134 135
      match seq with
	| [] ->
	    `Res fin
	| `Epsilon :: rest -> 
	    compile fin e rest
136
	| `Elem (_,p) :: rest -> 
137
	    `Res (mk !re_loc (Prod (p, guard_compile fin rest)))
138 139 140 141
	| `Seq (r1,r2) :: rest -> 
	    compile fin e (r1 :: r2 :: rest)
	| `Alt (r1,r2) :: rest -> 
	    cup (compile fin e (r1::rest)) (compile fin e (r2::rest))
142 143 144 145 146
	| `Star r :: rest -> 
	    cup (compile fin e (r::seq)) (compile fin e rest) 
	| `WeakStar r :: rest -> 
	    cup (compile fin e rest) (compile fin e (r::seq))
    )
147
  and guard_compile fin seq =
148
    try Memo.find seq !memo
149 150 151
    with
	Not_found ->
          let n = name () in
152
	  let v = mk !re_loc (PatVar n) in
153 154
          memo := Memo.add seq v !memo;
	  let d = compile fin (ref Coind.empty) seq in
155 156 157 158 159 160 161
	  (match d with
	     | `Empty -> assert false
	     | `Res d -> defs := (n,d) :: !defs);
	  v


  let constant_nil v t = 
162 163 164
    mk !re_loc 
      (And (t, 
	    (mk !re_loc (Constant (v, Types.Atom Sequence.nil_atom))), true))
165

166 167
  let compile loc regexp queue : ppat =
    re_loc := loc;
168
    let vars = seq_vars StringSet.empty regexp in
169
    let fin = StringSet.fold constant_nil vars queue in
170 171
    let n = guard_compile fin [propagate (fun p -> p) regexp] in
    memo := Memo.empty; 
172 173
    let d = !defs in
    defs := [];
174
    mk !re_loc (Recurs (n,d))
175 176
end

177
let compile_regexp = Regexp.compile noloc
178 179 180 181 182 183


let rec compile env { loc = loc; descr = d } : ti = 
  match (d : Ast.ppat') with
  | PatVar s -> 
      (try StringMap.find s env
184
       with Not_found -> 
185
	 raise_loc_generic loc ("Undefined type variable " ^ s)
186
      )
187
  | Recurs (t, b) -> compile (compile_many env b) t
188
  | Regexp (r,q) -> compile env (Regexp.compile loc r q)
189 190
  | Internal t -> cons loc (`Type t)
  | Or (t1,t2) -> cons loc (`Or (compile env t1, compile env t2))
191
  | And (t1,t2,e) -> cons loc (`And (compile env t1, compile env t2,e))
192 193
  | Diff (t1,t2) -> cons loc (`Diff (compile env t1, compile env t2))
  | Prod (t1,t2) -> cons loc (`Times (compile env t1, compile env t2))
194
  | XmlT (t1,t2) -> cons loc (`Xml (compile env t1, compile env t2))
195 196 197 198 199
  | Arrow (t1,t2) -> cons loc (`Arrow (compile env t1, compile env t2))
  | Record (l,o,t) -> cons loc (`Record (l,o,compile env t))
  | Constant (x,v) -> cons loc (`Constant (x,v))
  | Capture x -> cons loc (`Capture x)

200 201 202 203 204 205 206
and compile_many env b = 
  let b = List.map (fun (v,t) -> (v,t,mk' t.loc)) b in
  let env = 
    List.fold_left (fun env (v,t,x) -> StringMap.add v x env) env b in
  List.iter (fun (v,t,x) -> x.descr' <- `Alias (v, compile env t)) b;
  env

207 208 209 210 211 212
let comp_fv_seen = ref []
let comp_fv_res = ref []
let rec comp_fv s =
  if List.memq s !comp_fv_seen then ()
  else (
    comp_fv_seen := s :: !comp_fv_seen;
213 214 215 216 217 218 219 220 221 222 223 224 225 226 227
    match s.fv with
      | Some fv -> comp_fv_res := List.rev_append fv !comp_fv_res
      | None ->
	  (match s.descr' with
	     | `Alias (_,x) -> comp_fv x
	     | `Or (s1,s2) 
	     | `And (s1,s2,_)
	     | `Diff (s1,s2)
	     | `Times (s1,s2) | `Xml (s1,s2)
	     | `Arrow (s1,s2) -> comp_fv s1; comp_fv s2
	     | `Record (l,opt,s) -> comp_fv s
	     | `Type _ -> ()
	     | `Capture x
	     | `Constant (x,_) -> comp_fv_res := x :: !comp_fv_res
	  )
228 229 230 231 232
  )



let fv s =   
233 234
  match s.fv with
    | Some l -> l
235 236 237 238 239 240
    | None -> 
	comp_fv s;
	let l = SortedList.from_list !comp_fv_res in
	comp_fv_res := [];
	comp_fv_seen := [];
	s.fv <- Some l; 
241 242 243 244
	l

let rec typ seen s : Types.descr =
  match s.descr' with
245 246
    | `Alias (v,x) ->
	if List.memq s seen then 
247 248
	  raise_loc_generic s.loc' 
	    ("Unguarded recursion on variable " ^ v ^ " in this type")
249 250 251
	else typ (s :: seen) x
    | `Type t -> t
    | `Or (s1,s2) -> Types.cup (typ seen s1) (typ seen s2)
252
    | `And (s1,s2,_) ->  Types.cap (typ seen s1) (typ seen s2)
253 254
    | `Diff (s1,s2) -> Types.diff (typ seen s1) (typ seen s2)
    | `Times (s1,s2) ->	Types.times (typ_node s1) (typ_node s2)
255
    | `Xml (s1,s2) ->	Types.xml (typ_node s1) (typ_node s2)
256 257
    | `Arrow (s1,s2) ->	Types.arrow (typ_node s1) (typ_node s2)
    | `Record (l,o,s) -> Types.record l o (typ_node s)
258 259 260 261 262 263
    | `Capture x -> failwith ("bla1:" ^ x)
    | `Constant (x,_) -> 
	(match s.fv with 
	  | Some fv ->
	      List.iter (fun y -> Printf.eprintf "+++%s++++\n" y) fv);
	failwith ("bla:" ^ x); assert false
264 265 266 267 268 269 270 271 272 273 274

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 [] s in
	Types.define x t;
	x

275 276 277 278 279
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
280 281 282

let rec pat seen s : Patterns.descr =
  if fv s = [] then Patterns.constr (type_node s) else
283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302
    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
  | `Alias (v,x) ->
      if List.memq s seen 
      then raise 
	(Patterns.Error
	   ("Unguarded recursion on variable " ^ v ^ " in this pattern"));
      pat (s :: seen) x
  | `Or (s1,s2) -> Patterns.cup (pat seen s1) (pat seen s2)
  | `And (s1,s2,e) -> Patterns.cap (pat seen s1) (pat seen s2) e
  | `Diff (s1,s2) when fv s2 = [] ->
      let s2 = Types.cons (Types.neg (Types.descr (type_node s2)))in
      Patterns.cap (pat seen s1) (Patterns.constr s2) true
  | `Diff _ ->
      raise (Patterns.Error "Difference not allowed in patterns")
  | `Times (s1,s2) -> Patterns.times (pat_node s1) (pat_node s2)
303
  | `Xml (s1,s2) -> Patterns.xml (pat_node s1) (pat_node s2)
304 305 306 307 308 309 310 311
  | `Record (l,false,s) -> Patterns.record l (pat_node s)
  | `Record _ ->
      raise (Patterns.Error "Optional field not allowed in record patterns")
  | `Capture x ->  Patterns.capture x
  | `Constant (x,c) -> Patterns.constant x c
  | `Arrow _ ->
      raise (Patterns.Error "Arrow not allowed in patterns")
  | `Type _ -> assert false
312 313 314 315 316 317 318 319 320 321 322

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 [] s in
	Patterns.define x t;
	x

323
let mk_typ e =
324
  if fv e = [] then type_node e
325
  else raise_loc_generic e.loc' "Capture variables are not allowed in types"
326 327
    

328 329 330 331 332
let typ glb e =
  mk_typ (compile glb e)

let pat glb e =
  pat_node (compile glb e)
333

334 335 336 337 338 339 340 341 342 343 344 345
let register_global_types glb b =
  let env' = compile_many glb b in
  List.fold_left 
    (fun glb (v,{ loc = loc }) -> 
       let t = StringMap.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 StringMap.mem v glb
       then raise_loc_generic loc ("Multiple definition for type " ^ v);
       StringMap.add v t glb
    ) glb b
346 347 348



349 350
(* II. Build skeleton *)

351 352
module Fv = StringSet

353
let rec expr glb { loc = loc; descr = d } = 
354
  let (fv,td) = 
355
    match d with
356
      | Forget (e,t) ->
357
	  let (fv,e) = expr glb e and t = typ glb t in
358
	  (fv, Typed.Forget (e,t))
359 360
      | Var s -> (Fv.singleton s, Typed.Var s)
      | Apply (e1,e2) -> 
361
	  let (fv1,e1) = expr glb e1 and (fv2,e2) = expr glb e2 in
362
	  (Fv.union fv1 fv2, Typed.Apply (e1,e2))
363
      | Abstraction a ->
364 365
	  let iface = List.map (fun (t1,t2) -> (typ glb t1, typ glb t2)) 
			a.fun_iface in
366 367 368
	  let t = List.fold_left 
		    (fun accu (t1,t2) -> Types.cap accu (Types.arrow t1 t2)) 
		    Types.any iface in
369 370 371
	  let iface = List.map 
			(fun (t1,t2) -> (Types.descr t1, Types.descr t2)) 
			iface in
372
	  let (fv0,body) = branches glb a.fun_body in
373 374 375 376 377 378 379 380 381
	  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;
382
	       Typed.fun_fv = Fv.elements fv
383 384 385 386
	     }
	  )
      | Cst c -> (Fv.empty, Typed.Cst c)
      | Pair (e1,e2) ->
387
	  let (fv1,e1) = expr glb e1 and (fv2,e2) = expr glb e2 in
388
	  (Fv.union fv1 fv2, Typed.Pair (e1,e2))
389 390 391
      | Xml (e1,e2) ->
	  let (fv1,e1) = expr glb e1 and (fv2,e2) = expr glb e2 in
	  (Fv.union fv1 fv2, Typed.Xml (e1,e2))
392
      | Dot (e,l) ->
393
	  let (fv,e) = expr glb e in
394
	  (fv,  Typed.Dot (e,l))
395 396
      | RecordLitt r -> 
	  let fv = ref Fv.empty in
397
	  let r  = List.sort (fun (l1,_) (l2,_) -> compare l1 l2) r in
398 399
	  let r = List.map 
		    (fun (l,e) -> 
400
		       let (fv2,e) = expr glb e in fv := Fv.union !fv fv2; (l,e))
401 402 403 404 405 406 407
		    r in
	  let rec check = function
	    | (l1,_) :: (l2,_) :: _ when l1 = l2 -> 
		raise_loc loc (MultipleLabel l1)
	    | _ :: rem -> check rem
	    | _ -> () in
	  check r;
408
	  (!fv, Typed.RecordLitt r)
409
      | Op (op,le) ->
410
	  let (fvs,ltes) = List.split (List.map (expr glb) le) in
411 412
	  let fv = List.fold_left Fv.union Fv.empty fvs in
	  (fv, Typed.Op (op,ltes))
413
      | Match (e,b) -> 
414 415
	  let (fv1,e) = expr glb e
	  and (fv2,b) = branches glb b in
416 417
	  (Fv.union fv1 fv2, Typed.Match (e, b))
      | Map (e,b) ->
418 419
	  let (fv1,e) = expr glb e
	  and (fv2,b) = branches glb b in
420
	  (Fv.union fv1 fv2, Typed.Map (e, b))
421
      | Try (e,b) ->
422 423
	  let (fv1,e) = expr glb e
	  and (fv2,b) = branches glb b in
424
	  (Fv.union fv1 fv2, Typed.Try (e, b))
425
  in
426 427
  fv,
  { Typed.exp_loc = loc;
428 429 430 431
    Typed.exp_typ = Types.empty;
    Typed.exp_descr = td;
  }
	      
432
  and branches glb b = 
433
    let fv = ref Fv.empty in
434
    let accept = ref Types.empty in
435 436
    let b = List.map 
	      (fun (p,e) ->
437 438
		 let (fv2,e) = expr glb e in
		 let p = pat glb p in
439 440
		 let fv2 = List.fold_right Fv.remove (Patterns.fv p) fv2 in
		 fv := Fv.union !fv fv2;
441
		 accept := Types.cup !accept (Types.descr (Patterns.accept p));
442
		 { Typed.br_used = false;
443
		   Typed.br_pat = p;
444 445
		   Typed.br_body = e }
	      ) b in
446 447 448 449
    (!fv, 
     { 
       Typed.br_typ = Types.empty; 
       Typed.br_branches = b; 
450 451
       Typed.br_accept = !accept;
       Typed.br_compiled = None;
452 453
     } 
    )
454

455 456 457
let let_decl glb p e =
  let (_,e) = expr glb e in
  { Typed.let_pat = pat glb p;
458 459 460 461 462
    Typed.let_body = e;
    Typed.let_compiled = None }

(* III. Type-checks *)

463
module Env = StringMap
464
type env = Types.descr Env.t
465 466 467

open Typed

468 469 470
let warning loc msg =
  Format.fprintf Format.std_formatter 
    "Warning %a:@\n%s@\n" Location.print_loc loc msg
471 472 473 474

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

475
let rec type_check env e constr precise = 
476
(*  Format.fprintf Format.std_formatter "constr=%a precise=%b@\n"
477 478
    Types.Print.print_descr constr precise; 
*)
479
  let d = type_check' e.exp_loc env e.exp_descr constr precise in
480 481 482
  e.exp_typ <- Types.cup e.exp_typ d;
  d

483
and type_check' loc env e constr precise = match e with
484 485 486 487
  | Forget (e,t) ->
      let t = Types.descr t in
      ignore (type_check env e t false);
      t
488
  | Abstraction a ->
489 490 491 492 493 494 495
      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
496 497 498
      let env = match a.fun_name with
	| None -> env
	| Some f -> Env.add f a.fun_typ env in
499 500
      List.iter 
	(fun (t1,t2) ->
501
	   ignore (type_check_branches loc env t1 a.fun_body t2 false)
502 503
	) a.fun_iface;
      t
504

505 506
  | Match (e,b) ->
      let t = type_check env e b.br_accept true in
507
      type_check_branches loc env t b constr precise
508 509 510

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

514 515 516 517
  | 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
518 519 520 521 522 523 524 525 526 527 528 529 530 531
  | RecordLitt r ->
      let rconstr = Types.Record.get constr in
      if Types.Record.is_empty rconstr then
	raise_loc loc (ShouldHave (constr,"but it is a record."));

      let (rconstr,res) = 
	List.fold_left 
	  (fun (rconstr,res) (l,e) ->
	     let rconstr = Types.Record.restrict_label_present rconstr l in
	     let pi = Types.Record.project_field rconstr l in
	     if Types.Record.is_empty rconstr then
	       raise_loc loc 
		 (ShouldHave (constr,(Printf.sprintf 
					"Field %s is not allowed here."
532
					(Types.LabelPool.value l)
533 534 535 536 537 538 539 540 541 542 543 544 545 546
				     )
			     ));
	     let t = type_check env e pi true in
	     let rconstr = Types.Record.restrict_field rconstr l t in
	     
	     let res = 
	       if precise 
	       then Types.cap res (Types.record l false (Types.cons t))
	       else res in
	     (rconstr,res)
	  ) (rconstr, if precise then Types.Record.any else constr) r
      in
      res

547 548 549 550 551
  | 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
552 553 554 555 556 557 558
      (* Note: 
	 - could be more precise by integrating the decomposition
	 of constr inside Sequence.map.
      *)
      let res = 
	Sequence.map 
	  (fun t -> 
559
	     type_check_branches loc env t b constr' (precise || (not exact)))
560 561 562
	  t in
      if not exact then check loc res constr "";
      if precise then res else constr
563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579
  | 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
580
  | Apply (e1,e2) ->
581
(*
582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607
      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
608
*)
609 610 611
      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
612 613 614 615 616 617 618 619 620
      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
621 622 623 624 625 626 627 628 629 630 631 632 633
  | 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
634 635 636 637 638
  | _ -> 
      let t : Types.descr = compute_type' loc env e in
      check loc t constr "";
      t

639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658
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


659 660 661 662
and compute_type env e =
  type_check env e Types.any true

and compute_type' loc env = function
663 664 665 666
  | Var s -> 
      (try Env.find s env 
       with Not_found -> raise_loc loc (UnboundId s)
      )
667
  | Cst c -> Types.constant c
668 669 670 671
  | 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)))
672 673 674
  | Op (op, el) ->
      let args = List.map (fun e -> (e.exp_loc, compute_type env e)) el in
      type_op loc op args
675 676
  | Map (e,b) ->
      let t = compute_type env e in
677
      Sequence.map (fun t -> type_check_branches loc env t b Types.any true) t
678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695

(* We keep these cases here to allow comparison and benchmarking ...
   Just comment the corresponding cases in type_check' to
   activate these ones.
*)
  | Pair (e1,e2) -> 
      let t1 = compute_type env e1 
      and t2 = compute_type env e2 in
      Types.times (Types.cons t1) (Types.cons t2)
  | RecordLitt r ->
      List.fold_left 
        (fun accu (l,e) ->
           let t = compute_type env e in
           let t = Types.record l false (Types.cons t) in
           Types.cap accu t
        ) Types.Record.any r


696
  | _ -> assert false
697

698
and type_check_branches loc env targ brs constr precise =
699
  if Types.is_empty targ then Types.empty 
700 701
  else (
    brs.br_typ <- Types.cup brs.br_typ targ;
702
    branches_aux loc env targ 
703 704
      (if precise then Types.empty else constr) 
      constr precise brs.br_branches
705
  )
706
    
707 708
and branches_aux loc env targ tres constr precise = function
  | [] -> raise_loc loc (NonExhaustive targ)
709 710 711 712 713 714
  | 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' 
715
      then branches_aux loc env targ tres constr precise rem
716 717 718 719 720 721
      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
722 723
	  let t = type_check env' b.br_body constr precise in
	  let tres = if precise then Types.cup t tres else tres in
724 725
	  let targ'' = Types.diff targ acc in
	  if (Types.non_empty targ'') then 
726
	    branches_aux loc env targ'' tres constr precise rem 
727 728
	  else
	    tres
729
	)
730

731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756
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


757 758
and type_op loc op args =
  match (op,args) with
759
    | "+", [loc1,t1; loc2,t2] ->
760
	type_int_binop Intervals.add loc1 t1 loc2 t2
761 762 763
    | "-", [loc1,t1; loc2,t2] ->
	type_int_binop Intervals.sub loc1 t1 loc2 t2
    | ("*" | "/"), [loc1,t1; loc2,t2] ->
764
	type_int_binop (fun i1 i2 -> Intervals.any) loc1 t1 loc2 t2
765
    | "@", [loc1,t1; loc2,t2] ->
766 767 768
	check loc1 t1 Sequence.any
	  "The first argument of @ must be a sequence";
	Sequence.concat t1 t2
769
    | "flatten", [loc1,t1] ->
770 771 772
	check loc1 t1 Sequence.seqseq 
	  "The argument of flatten must be a sequence of sequences";
	Sequence.flatten t1
773 774 775 776
    | "load_xml", [loc1,t1] ->
	check loc1 t1 Sequence.string
	  "The argument of load_xml must be a string (filename)";
	Types.any
777 778
    | "raise", [loc1,t1] ->
	Types.empty
779 780
    | "print_xml", [loc1,t1] ->
	Sequence.string
781 782 783 784 785 786
    | "int_of", [loc1,t1] ->
	check loc1 t1 Sequence.string
	  "The argument of int_of must a string";
	if not (Types.subtype t1 Builtin.intstr) then
	  warning loc "This application of int_of may fail";
	Types.interval Intervals.any
787 788 789 790 791 792 793 794 795 796 797
    | _ -> assert false

and type_int_binop f loc1 t1 loc2 t2 =
  if not (Types.Int.is_int t1) then
    raise_loc loc1 
      (Constraint 
	 (t1,Types.Int.any,
	  "The first argument must be an integer"));
  if not (Types.Int.is_int t2) then
    raise_loc loc2
      (Constraint 
798
	       (t2,Types.Int.any,
799 800 801 802 803
		"The second argument must be an integer"));
  Types.Int.put
    (f (Types.Int.get t1) (Types.Int.get t2));