typer.ml 33.1 KB
Newer Older
1
2
3
open Location
open Ast
open Ident
4

5
6
7
8
9
10
let (=) (x:int) y = x = y
let (<=) (x:int) y = x <= y
let (<) (x:int) y = x < y
let (>=) (x:int) y = x >= y
let (>) (x:int) y = x > y

11
let warning loc msg =
12
  let v = Location.get_viewport () in
13
  let ppf = if Html.is_html v then Html.ppf v else Format.err_formatter in
14
15
16
  Format.fprintf ppf "Warning %a:@\n" Location.print_loc (loc,`Full);
  Location.html_hilight (loc,`Full);
  Format.fprintf ppf "%s@." msg
17

18
19
20
21
22
23
exception NonExhaustive of Types.descr
exception Constraint of Types.descr * Types.descr
exception ShouldHave of Types.descr * string
exception ShouldHave2 of Types.descr * string * Types.descr
exception WrongLabel of Types.descr * label
exception UnboundId of id * bool
24
exception UnboundExtId of Compunit.t * id
25
exception Error of string
26
27
exception Warning of string * Types.t

28
29
30
31
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)

32
33
type item =
  | Type of Types.t
34
  | Val of Types.t
35

36
type ext =
37
  | ECDuce of Compunit.t         (* CDuce unit *)
38
39
40
  | EOCaml of string             (* OCaml module *)
  | ESchema of string            (* XML Schema *)

41
42
module UEnv = Map.Make(U)

43
type t = {
44
  ids : item Env.t;
45
  ns: Ns.table;
46
  cu: ext UEnv.t;
47
  keep_ns: bool
48
}
49

50
51
let load_schema = ref (fun _ _ -> assert false)
let from_comp_unit = ref (fun _ -> assert false)
52
let load_comp_unit = ref (fun _ -> assert false)
53
54
let has_ocaml_unit = ref (fun _ -> false)
let has_static_external = ref (fun _ -> assert false)
55

56
let schemas = Hashtbl.create 13
57

58
let type_schema env x uri =
59
60
  if not (Hashtbl.mem schemas uri) then
    Hashtbl.add schemas uri (!load_schema x uri);
61
  { env with cu = UEnv.add x (ESchema uri) env.cu }
62

63
64
let empty_env = {
  ids = Env.empty;
65
  ns = Ns.def_table;
66
  cu = UEnv.empty;
67
  keep_ns = false
68
69
}

70
let enter_cu x cu env =
71
  { env with cu = UEnv.add x (ECDuce cu) env.cu }
72

73
let find_cu loc x env =
74
  try UEnv.find x env.cu
75
  with Not_found ->
76
77
78
79
    try ECDuce (!load_comp_unit x)
    with Not_found ->
      if !has_ocaml_unit x then (EOCaml (U.get_str x))
      else error loc ("Cannot find external unit " ^ (U.to_string x))
80
81


82
let find_schema x env =
83
84
85
86
87
88
  try 
    (match UEnv.find x env.cu with
      | ESchema s -> s 
      | _ -> raise Not_found)
  with Not_found -> 
    raise (Error (Printf.sprintf "%s: no such schema" (U.to_string x)))
89

90
91
92
93
94
95
96
97
let enter_type id t env =
  { env with ids = Env.add id (Type t) env.ids }
let enter_types l env =
  { env with ids = 
      List.fold_left (fun accu (id,t) -> Env.add id (Type t) accu) env.ids l }
let find_type id env =
  match Env.find id env.ids with
    | Type t -> t
98
    | Val _ -> raise Not_found
99

100

101
let enter_value id t env = 
102
  { env with ids = Env.add id (Val t) env.ids }
103
104
let enter_values l env =
  { env with ids = 
105
      List.fold_left (fun accu (id,t) -> Env.add id (Val t) accu) env.ids l }
106
107
108
let enter_values_dummy l env =
  { env with ids = 
      List.fold_left (fun accu id -> Env.add id (Val Types.empty) accu) env.ids l }
109
110
let find_value id env =
  match Env.find id env.ids with
111
    | Val t -> t
112
    | _ -> raise Not_found
113
114
115
let find_value_global loc cu id env =
  try find_value id (!from_comp_unit cu)
  with Not_found -> raise_loc loc (UnboundExtId (cu,id))
116
	
117
118
119
120
121
122
let value_name_ok id env =
  try match Env.find id env.ids with
    | Val t -> true
    | _ -> false
  with Not_found -> true

123
124
125
126
let iter_values env f =
  Env.iter (fun x ->
	      function Val t -> f x t;
		| _ -> ()) env.ids
127

128

129
let register_types cu env =
130
131
132
  Env.iter (fun x t -> match t with
	      | Type t -> Types.Print.register_global cu (Ident.value x) t
	      | _ -> ()) env.ids
133

134

135
(* Namespaces *)
136

137
let set_ns_table_for_printer env = 
138
  Ns.InternalPrinter.set_table env.ns
139

140
let get_ns_table tenv = tenv.ns
141

142
let type_ns env p ns =
143
  { env with ns = Ns.add_prefix p ns env.ns }
144

145
146
147
let type_keep_ns env k =
  { env with keep_ns = k }

148
149
150
151
152
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))
153

154
155
156
let qname env loc t = 
  protect_error_ns loc (Ns.map_tag env.ns) t
    
157
let ident env loc t =
158
  protect_error_ns loc (Ns.map_attr env.ns) t
159
160
161
162
163
164
165

let has_value id env =
  try match Env.find (Ident.ident (Ns.map_attr env.ns id)) env.ids with
    | Val t -> true
    | _ -> false
  with Not_found | Ns.UnknownPrefix _ -> false

166
let parse_atom env loc t = Atoms.V.mk (qname env loc t)
167
168
 
let parse_ns env loc ns =
169
  protect_error_ns loc (Ns.map_prefix env.ns) ns
170

171
let parse_label env loc t =
172
  Label.mk (protect_error_ns loc (Ns.map_attr env.ns) t)
173

174
175
176
177
178
179
180
181
182
183
184
185
186
let parse_record env loc f r =
  let r = List.map (fun (l,x) -> (parse_label env loc l, f x)) r in
  LabelMap.from_list (fun _ _ -> raise_loc_generic loc "Duplicated record field") r

let rec const env loc = function
  | LocatedExpr (loc,e) -> const env loc e
  | Pair (x,y) -> Types.Pair (const env loc x, const env loc y)
  | Xml (x,y) -> Types.Xml (const env loc x, const env loc y)
  | RecordLitt x -> Types.Record (parse_record env loc (const env loc) x)
  | String (i,j,s,c) -> Types.String (i,j,s,const env loc c)
  | Atom t -> Types.Atom (parse_atom env loc t)
  | Integer i -> Types.Integer i
  | Char c -> Types.Char c
187
  | Const c -> c
188
189
190
191
  | _ -> raise_loc_generic loc "This should be a scalar or structured constant"

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

193

194
195
196
197
let get_schema_names env = 
  UEnv.fold 
    (fun n cu acc -> match cu with ESchema _ -> n :: acc | _ -> acc) env.cu []
    
198
199
let find_schema_component uri name =
  Env.find (Ident.ident name) (Hashtbl.find schemas uri)
200

201
202
let find_schema_descr uri (name : Ns.QName.t) =
  try find_schema_component uri name
203
204
205
  with Not_found ->    
    raise (Error (Printf.sprintf "No component named '%s' found in schema '%s'"
		    (Ns.QName.to_string name) uri))
206
207


208
209
210
211
let find_type_global loc cu id env =
  match find_cu loc cu env with
    | ECDuce cu -> find_type id (!from_comp_unit cu)
    | EOCaml _ -> error loc "OCaml units don't export types" (* TODO *)
212
    | ESchema s -> fst (find_schema_descr s (Ident.value id))
213
	
214

215
module IType = struct
216
  open Typepat
217
218
219
220
221
222
223
224
225
226

(* From AST to the intermediate representation *)

  type penv = {
    penv_tenv : t;
    penv_derec : node Env.t;
  }

  let penv tenv = { penv_tenv = tenv; penv_derec = Env.empty }

227
228
  let all_delayed = ref []

229
230
  let clean_on_err () = all_delayed := []

231
232
233
234
235
236
  let delayed loc =
    let s = mk_delayed () in
    all_delayed := (loc,s) :: !all_delayed;
    s

  let check_one_delayed (loc,p) =
237
    if not (check_wf p) then error loc "Ill-formed recursion"
238
239
240
241
242
    
  let check_delayed () =
    let l = !all_delayed in
    all_delayed := []; 
    List.iter check_one_delayed l
243

244
  let rec derecurs env p = match p.descr with
245
    | PatVar (cu,v) -> derecurs_var env p.loc cu v
246
    | Recurs (p,b) -> derecurs (fst (derecurs_def env b)) p
247
    | Internal t -> mk_type t
248
    | NsT ns -> 
249
250
251
252
253
254
255
256
	mk_type (Types.atom (Atoms.any_in_ns (parse_ns env.penv_tenv p.loc ns)))
    | Or (p1,p2) -> mk_or (derecurs env p1) (derecurs env p2)
    | And (p1,p2) -> mk_and (derecurs env p1) (derecurs env p2)
    | Diff (p1,p2) -> mk_diff (derecurs env p1) (derecurs env p2)
    | Prod (p1,p2) -> mk_prod (derecurs env p1) (derecurs env p2)
    | XmlT (p1,p2) -> mk_xml (derecurs env p1) (derecurs env p2)
    | Arrow (p1,p2) -> mk_arrow (derecurs env p1) (derecurs env p2)
    | Optional p -> mk_optional (derecurs env p)
257
258
259
260
    | Record (o,r) -> 
	let aux = function
	  | (p,Some e) -> (derecurs env p, Some (derecurs env e))
	  | (p,None) -> derecurs env p, None in
261
262
263
264
265
266
267
	mk_record o (parse_record env.penv_tenv p.loc aux r)
    | Constant (x,c) -> 
	mk_constant (ident env.penv_tenv p.loc x) (const env.penv_tenv p.loc c)
    | Cst c -> mk_type (Types.constant (const env.penv_tenv p.loc c))
    | Regexp r -> rexp (derecurs_regexp env r)
    | Concat (p1,p2) ->  mk_concat (derecurs env p1) (derecurs env p2)
    | Merge (p1,p2) -> mk_merge (derecurs env p1) (derecurs env p2)
268
	  
269
270
271
272
273
274
275
276
277
  and derecurs_regexp env = function
    | Epsilon -> mk_epsilon
    | Elem p -> mk_elem (derecurs env p)
    | Guard p -> mk_guard (derecurs env p)
    | Seq (p1,p2) -> mk_seq (derecurs_regexp env p1) (derecurs_regexp env p2)
    | Alt (p1,p2) -> mk_alt (derecurs_regexp env p1) (derecurs_regexp env p2)
    | Star p -> mk_star (derecurs_regexp env p)
    | WeakStar p -> mk_weakstar (derecurs_regexp env p)
    | SeqCapture (loc,x,p) -> mk_seqcapt (ident env.penv_tenv loc x) (derecurs_regexp env p)
278
	  
279
280
281
282
283
  and derecurs_var env loc cu v =
    let v = ident env.penv_tenv loc v in
    match cu with
      | None ->
	  (try Env.find v env.penv_derec 
284
	   with Not_found -> 
285
286
	     try mk_type (find_type v env.penv_tenv)
	     with Not_found -> mk_capture v)
287
      | Some cu ->
288
	  (try mk_type (find_type_global loc cu v env.penv_tenv)
289
290
291
292
	   with Not_found ->
	     raise_loc_generic loc 
	       ("Unbound external type " ^ (U.get_str cu) ^ "." ^ 
		  (Ident.to_string v)))
293
294
	      
  and derecurs_def env b =
295
296
297
298
299
300
301
302
303
304
305
306
307
    let seen = ref IdSet.empty in
    let b = 
      List.map 
	(fun (loc,v,p) -> 
	   let v = ident env.penv_tenv loc v in
	   if IdSet.mem !seen v then 
	     raise_loc_generic loc
	       ("Multiple definitions for the type identifer " ^ 
		  (Ident.to_string v));
	   seen := IdSet.add v !seen;
	   (v,p,delayed loc))
	b in

308
309
310
    let n = 
      List.fold_left (fun env (v,p,s) -> Env.add v s env) env.penv_derec b in
    let env = { env with penv_derec = n } in
311
    List.iter (fun (v,p,s) -> link s (derecurs env p)) b;
312
313
    (env, b)

314
315
  let derec penv p =
    let d = derecurs penv p in
316
    elim_concats ();
317
318
319
    check_delayed ();
    internalize d;
    d
320
321


322
(* API *)
323

324
325
326
327
328
329
330
  let check_no_fv loc n =
    match peek_fv n with
      | None -> ()
      | Some x ->
	  raise_loc_generic loc 
	    ("Capture variable not allowed: " ^ (Ident.to_string x))

331
  let type_defs env b =
332
333
334
335
336
337
    let _,b' = derecurs_def (penv env) b in
    elim_concats ();
    check_delayed ();
    let aux loc d =
      internalize d;
      check_no_fv loc d;
338
      try typ d
339
      with Patterns.Error s -> raise_loc_generic loc s
340
    in
341
    let b = 
342
343
344
      List.map2 
	(fun (loc,v,p) (v',_,d) ->
	   let t = aux loc d in
345
346
347
348
	   if (loc <> noloc) && (Types.is_empty t) then
	     warning loc 
	       ("This definition yields an empty type for " ^ (U.to_string v));
	   let v = ident env loc v in
349
	   (v',t)) b b' in
350
    List.iter (fun (v,t) -> Types.Print.register_global "" v t) b;
351
    enter_types b env
352

353
354
355
356
  let type_defs env b =
    try type_defs env b
    with exn -> clean_on_err (); raise exn

357
  let typ env t = 
358
359
360
361
362
363
    try
      let d = derec (penv env) t in
      check_no_fv t.loc d;
      try typ_node d
      with Patterns.Error s -> raise_loc_generic t.loc s
    with exn -> clean_on_err (); raise exn
364
365

  let pat env t = 
366
367
368
369
370
    try
      let d = derec (penv env) t in
      try pat_node d
      with Patterns.Error s -> raise_loc_generic t.loc s
    with exn -> clean_on_err (); raise exn
371

372
end
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388

let typ = IType.typ
let pat = IType.pat
let type_defs = IType.type_defs

let dump_types ppf env =
  Env.iter (fun v -> 
	      function 
		  (Type _) -> Format.fprintf ppf " %a" Ident.print v
		| _ -> ()) env.ids

let dump_ns ppf env =
  Ns.dump_table ppf env.ns



389

390
391
(* II. Build skeleton *)

392

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

395
module Fv = IdSet
396

397
398
399
type branch = Branch of Typed.branch * branch list

let cur_branch : branch list ref = ref []
400

401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
let exp' loc e = 
  { Typed.exp_loc = loc; Typed.exp_typ = Types.empty; Typed.exp_descr = e; }

let exp loc fv e = fv, exp' loc e

let exp_nil = exp' noloc (Typed.Cst Sequence.nil_cst)

let pat_true = 
  let n = Patterns.make Fv.empty in
  Patterns.define n (Patterns.constr Builtin_defs.true_type);
  n

let pat_false =   
  let n = Patterns.make Fv.empty in
  Patterns.define n (Patterns.constr Builtin_defs.false_type);
  n

418

419
let ops = Hashtbl.create 13
420
421
let register_op op arity f = Hashtbl.add ops op (arity,f)
let typ_op op = snd (Hashtbl.find ops op)
422

423
424
425
426
427
let fun_name env a =
  match a.fun_name with
    | None -> None
    | Some (loc,s) -> Some (ident env loc s)

428
let is_op env s = 
429
430
  if (Env.mem s env.ids) then None
  else
431
432
    let (ns,s) = s in
    if Ns.Uri.equal ns Ns.empty then
433
434
435
436
437
438
      let s = U.get_str s in
      try 
	let o = Hashtbl.find ops s in
	Some (s, fst o)
      with Not_found -> None
    else None
439

440
441
let rec expr env loc = function
  | LocatedExpr (loc,e) -> expr env loc e
442
  | Forget (e,t) ->
443
      let (fv,e) = expr env loc e and t = typ env t in
444
      exp loc fv (Typed.Forget (e,t))
445
446
  | Check (e,t) ->
      let (fv,e) = expr env loc e and t = typ env t in
447
      exp loc fv (Typed.Check (ref Types.empty,e,t))
448
  | Var s -> var env loc s
449
  | Apply (e1,e2) -> 
450
451
452
453
454
455
456
457
      let (fv1,e1) = expr env loc e1 and (fv2,e2) = expr env loc e2 in
      let fv = Fv.cup fv1 fv2 in
      (match e1.Typed.exp_descr with
	 | Typed.Op (op,arity,args) when arity > 0 -> 
	     exp loc fv (Typed.Op (op,arity - 1,args @ [e2]))
	 | _ ->
	     exp loc fv (Typed.Apply (e1,e2)))
  | Abstraction a -> abstraction env loc a
458
  | (Integer _ | Char _ | Atom _ | Const _) as c -> 
459
      exp loc Fv.empty (Typed.Cst (const env loc c))
460
  | Pair (e1,e2) ->
461
      let (fv1,e1) = expr env loc e1 and (fv2,e2) = expr env loc e2 in
462
463
      exp loc (Fv.cup fv1 fv2) (Typed.Pair (e1,e2))
  | Xml (e1,e2) ->
464
      let (fv1,e1) = expr env loc e1 and (fv2,e2) = expr env loc e2 in
465
466
      let n = if env.keep_ns then Some env.ns else None in
      exp loc (Fv.cup fv1 fv2) (Typed.Xml (e1,e2,n))
467
468
  | Dot _ as e ->
      dot loc env e
469
  | RemoveField (e,l) ->
470
471
      let (fv,e) = expr env loc e in
      exp loc fv (Typed.RemoveField (e,parse_label env loc l))
472
473
  | RecordLitt r -> 
      let fv = ref Fv.empty in
474
      let r = parse_record env loc
475
		(fun e -> 
476
		   let (fv2,e) = expr env loc e 
477
478
479
		   in fv := Fv.cup !fv fv2; e)
		r in
      exp loc !fv (Typed.RecordLitt r)
480
  | String (i,j,s,e) ->
481
      let (fv,e) = expr env loc e in
482
      exp loc fv (Typed.String (i,j,s,e))
483
  | Match (e,b) -> 
484
485
      let (fv1,e) = expr env loc e
      and (fv2,b) = branches env b in
486
      exp loc (Fv.cup fv1 fv2) (Typed.Match (e, b))
487
  | Map (e,b) ->
488
489
      let (fv1,e) = expr env loc e
      and (fv2,b) = branches env b in
490
491
      exp loc (Fv.cup fv1 fv2) (Typed.Map (e, b))
  | Transform (e,b) ->
492
493
      let (fv1,e) = expr env loc e
      and (fv2,b) = branches env b in
494
      exp loc (Fv.cup fv1 fv2) (Typed.Transform (e, b))
495
  | Xtrans (e,b) ->
496
497
      let (fv1,e) = expr env loc e
      and (fv2,b) = branches env b in
498
      exp loc (Fv.cup fv1 fv2) (Typed.Xtrans (e, b))
499
  | Validate (e,schema,elt) ->
500
      let (fv,e) = expr env loc e in
501
      let uri = find_schema schema env in
502
503
      let (t,v) = find_schema_descr uri (qname env loc elt) in
      exp loc fv (Typed.Validate (e, t, v))
504
505
  | SelectFW (e,from,where) ->
      select_from_where env loc e from where
506
  | Try (e,b) ->
507
508
      let (fv1,e) = expr env loc e
      and (fv2,b) = branches env b in
509
      exp loc (Fv.cup fv1 fv2) (Typed.Try (e, b))
510
  | NamespaceIn (pr,ns,e) ->
511
      let env = type_ns env pr ns in
512
      expr env loc e
513
514
  | KeepNsIn (k,e) ->
      expr (type_keep_ns env k) loc e
515
  | Ref (e,t) ->
516
      let (fv,e) = expr env loc e and t = typ env t in
517
      exp loc fv (Typed.Ref (e,t))
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535

and if_then_else loc cond yes no =
  let b = {
    Typed.br_typ = Types.empty;
    Typed.br_branches = [
      { Typed.br_loc = yes.Typed.exp_loc;
	Typed.br_used = false;
	Typed.br_vars_empty = Fv.empty;
	Typed.br_pat = pat_true;
	Typed.br_body = yes };
      { Typed.br_loc = no.Typed.exp_loc;
	Typed.br_used = false;
	Typed.br_vars_empty = Fv.empty;
	Typed.br_pat = pat_false;
	Typed.br_body = no } ];
    Typed.br_accept = Builtin_defs.bool;
  } in
  exp' loc (Typed.Match (cond,b))
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568


and dot loc env e =
  let dot_access loc (fv,e) l =
    exp loc fv (Typed.Dot (e,parse_label env loc l)) in
  let rec aux loc fields args = function
    | Var cu when not (has_value cu env) -> 
	(match find_cu loc cu env with
	   | ECDuce cu ->
	       if args != [] then
		 error loc "CDuce externals cannot have type argument";
	       let id,fields = 
		 (match fields with (hd,_)::tl -> hd,tl | _ -> assert false) in
	       let id = ident env loc id in
	       let t = find_value_global loc cu id env in
	       let e = exp loc Fv.empty (Typed.ExtVar (cu, id, t)) in
	       List.fold_left (fun e (x,loc) -> dot_access loc e x) e fields
	   | EOCaml cu ->
	       let fields = List.map fst fields in
	       let s = String.concat "." (cu :: List.map U.get_str fields) in
	       extern loc env s args
	   | ESchema _ ->
 	       error loc "Schema don't export values")
    | LocatedExpr (loc,e) -> aux loc fields args e
    | Dot (e,id,a) -> aux loc ((id,loc) :: fields) (a @ args) e
    | e ->
	if args != [] then
	  error loc "Field access cannot have type arguments"
	else
	  let e = expr env loc e in
	  List.fold_left (fun e (x,loc) -> dot_access loc e x) e fields
  in
  aux loc [] [] e
569
570
571
572
	
and extern loc env s args = 
  let args = List.map (typ env) args in
  try
573
574
575
576
577
578
    let (i,t) =
      if !has_static_external s then
	(`Builtin s, Externals.typ s args)
      else
	let (i,t) = Externals.resolve s args in
	(`Ext i, t) in
579
580
581
582
    exp loc Fv.empty (Typed.External (t,i))
  with exn -> raise_loc loc exn
    
and var env loc s =
583
584
  let id = ident env loc s in
  match is_op env id with
585
    | Some (s,arity) -> 
586
587
588
589
590
591
592
	let e = match s with 
	  | "print_xml" | "print_xml_utf8" ->
	      Typed.NsTable (env.ns,Typed.Op (s, arity, []))
	  | "load_xml" when env.keep_ns ->
	      Typed.Op ("!load_xml",arity,[])
	  | _ -> Typed.Op (s, arity, []) 
	in
593
	exp loc Fv.empty e
594
    | None ->
595
596
597
	(try ignore (find_value id env)
	 with Not_found -> raise_loc loc (UnboundId (id, Env.mem id env.ids)));
	exp loc (Fv.singleton id) (Typed.Var id)
598
599
600
601
602
603
604
605
606
607
608
609
610

and abstraction env loc a =
  let iface = 
    List.map 
      (fun (t1,t2) -> (typ env t1, typ env t2)) a.fun_iface in
  let t = 
    List.fold_left 
      (fun accu (t1,t2) -> Types.cap accu (Types.arrow t1 t2)) 
      Types.any iface in
  let iface = 
    List.map 
      (fun (t1,t2) -> (Types.descr t1, Types.descr t2)) 
      iface in
611
  let fun_name = fun_name env a in
612
  let env' = 
613
    match fun_name with 
614
615
616
617
      | None -> env
      | Some f -> enter_values_dummy [ f ] env
  in
  let (fv0,body) = branches env' a.fun_body in
618
  let fv = match fun_name with
619
620
621
    | None -> fv0
    | Some f -> Fv.remove f fv0 in
  let e = Typed.Abstraction 
622
	    { Typed.fun_name = fun_name;
623
624
625
626
627
628
629
630
631
632
633
634
635
	      Typed.fun_iface = iface;
	      Typed.fun_body = body;
	      Typed.fun_typ = t;
	      Typed.fun_fv = fv
	    } in
  exp loc fv e
    
and branches env b = 
  let fv = ref Fv.empty in
  let accept = ref Types.empty in
  let branch (p,e) = 
    let cur_br = !cur_branch in
    cur_branch := [];
636
637
638
639
640
    let ploc = p.loc in
    let p = pat env p in
    let fvp = Patterns.fv p in
    let (fv2,e) = expr (enter_values_dummy fvp env) noloc e in
    let br_loc = merge_loc ploc e.Typed.exp_loc in
641
642
643
    (match Fv.pick (Fv.diff fvp fv2) with
       | None -> ()
       | Some x ->
644
	   let x = Ident.to_string x in
645
646
647
648
649
	   warning br_loc 
	     ("The capture variable " ^ x ^ 
	      " is declared in the pattern but not used in the body of this branch. It might be a misspelled or undeclared type or name (if it isn't, use _ instead)."));
    let fv2 = Fv.diff fv2 fvp in
    fv := Fv.cup !fv fv2;
650
    accept := Types.cup !accept (Types.descr (Patterns.accept p));
651
652
653
    let br = 
      { 
	Typed.br_loc = br_loc;
654
	Typed.br_used = br_loc == noloc;
655
656
	Typed.br_vars_empty = fvp;
	Typed.br_pat = p;
657
658
659
660
661
662
663
664
665
666
667
	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;
   } 
  )
668

669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
and select_from_where env loc e from where =
  let env = ref env in
  let all_fv = ref Fv.empty in
  let bound_fv = ref Fv.empty in
  let clause (p,e) =
    let ploc = p.loc in
    let p = pat !env p in
    let fvp = Patterns.fv p in
    let (fv2,e) = expr !env noloc e in
    env := enter_values_dummy fvp !env;
    all_fv := Fv.cup (Fv.diff fv2 !bound_fv) !all_fv;
    bound_fv := Fv.cup fvp !bound_fv;
    (ploc,p,fvp,e) in
  let from = List.map clause from in
  let where = List.map (expr !env noloc) where in

  let put_cond rest (fv,cond) = 
    all_fv := Fv.cup (Fv.diff fv !bound_fv) !all_fv;
    if_then_else loc cond rest exp_nil in
  let aux (ploc,p,fvp,e) (where,rest) = 
    (* Put here the conditions that depends on variables in fvp *)
    let (above,here) = List.partition (fun (v,_) -> Fv.disjoint v fvp) where in
    (* if cond then ... else [] *)
    let rest = List.fold_left put_cond rest here in
    (* transform e with p -> ... *)
694
    let br = { Typed.br_loc = ploc;
695
696
697
	  Typed.br_used = false;
	  Typed.br_vars_empty = fvp;
	  Typed.br_pat = p;
698
699
700
701
702
	  Typed.br_body = rest } in
    cur_branch := [ Branch (br, !cur_branch) ];
    let b = {
      Typed.br_typ = Types.empty;
      Typed.br_branches = [ br ];
703
704
705
706
707
      Typed.br_accept = Types.descr (Patterns.accept p);
    } in
    let br_loc = merge_loc ploc e.Typed.exp_loc in
    (above,exp' br_loc (Typed.Transform (e, b)))
  in
708
709
  let cur_br = !cur_branch in
  cur_branch := [];
710
  let (fv,e) = expr !env noloc (Pair(e,cst_nil)) in
711
  cur_branch := !cur_branch @ cur_br;
712
713
714
715
716
717
718
719
720
721
  let (where,rest) = List.fold_right aux from (where,e) in
  (* The remaining conditions are constant. Gives a warning for that. *)
  (match where with
     | (_,e) :: _ ->
	 warning e.Typed.exp_loc
	   "This 'where' condition does not depend on any captured variable"
     | _ -> ());
  let rest = List.fold_left put_cond rest where in
  (Fv.cup !all_fv (Fv.diff fv !bound_fv)), rest

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

724
725
let let_decl env p e =
  { Typed.let_pat = pat env p;
726
    Typed.let_body = expr env e }
727

728
729
730

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

731

732
733
(* III. Type-checks *)

734
735
open Typed

736
737
738
739
740
741
let localize loc f x =
  try f x
  with 
    | (Error _ | Constraint (_,_)) as exn -> raise (Location.Location (loc,`Full,exn))
    | Warning (s,t) -> warning loc s; t

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

745
let verify loc t s = 
746
747
  require loc t s; t

748
749
750
751
let verify_noloc t s =
  if not (Types.subtype t s) then raise (Constraint (t, s));
  t

752
753
754
755
756
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 = 
757
758
  raise_loc loc (ShouldHave (constr,s))

759
760
761
let should_have_str loc ofs constr s = 
  raise_loc_str loc ofs (ShouldHave (constr,s))

762
let flatten arg constr precise =
763
764
765
766
767
768
769
770
771
  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
772
    verify_noloc (Sequence.flatten t) constr
773

774
775
let rec type_check env e constr precise = 
  let d = type_check' e.exp_loc env e.exp_descr constr precise in
776
  let d = if precise then d else constr in
777
778
779
  e.exp_typ <- Types.cup e.exp_typ d;
  d

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

786
787
788
  | Check (t0,e,t) ->
      let te = type_check env e Types.any true in
      t0 := Types.cup !t0 te;
789
      verify loc (Types.cap te (Types.descr t)) constr
790

791
  | Abstraction a ->
792
793
794
      let t =
	try Types.Arrow.check_strenghten a.fun_typ constr 
	with Not_found -> 
795
796
	  should_have loc constr
	    "but the interface of the abstraction is not compatible"
797
      in
798
799
      let env = match a.fun_name with
	| None -> env
800
	| Some f -> enter_value f a.fun_typ env in
801
802
      List.iter 
	(fun (t1,t2) ->
803
804
805
	   let acc = a.fun_body.br_accept in 
	   if not (Types.subtype t1 acc) then
	     raise_loc loc (NonExhaustive (Types.diff t1 acc));
806
	   ignore (type_check_branches loc env t1 a.fun_body t2 false)
807
808
	) a.fun_iface;
      t
809

810
811
  | Match (e,b) ->
      let t = type_check env e b.br_accept true in
812
      type_check_branches loc env t b constr precise
813
814
815

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

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

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

825
  | RecordLitt r ->
826
827
828
829
830
831
      type_record loc env r constr precise

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

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

834
835
836
837
  | 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
838
839
840
841
842
843
844
      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
845
      verify loc res constr
846
847

  | Var s -> 
848
      verify loc (find_value s env) constr
849

850
  | ExtVar (cu,s,t) ->
851
      verify loc t constr
852
  | Cst c -> 
853
      verify loc (Types.constant c) constr
854

855
856
857
  | String (i,j,s,e) ->
      type_check_string loc env 0 s i j e constr precise

858
  | Dot (e,l) ->
859
860
861
862
863
864
865
866
867
868
869
870
871
872
      let expect_rec = Types.record l (Types.cons constr) in
      let expect_elt = 
	Types.xml 
	  Types.any_node 
	  (Types.cons (Types.times (Types.cons expect_rec) Types.any_node)) in
      let t = type_check env e (Types.cup expect_rec expect_elt) precise in
      let t_elt =
	let t = Types.Product.pi2 (Types.Product.get ~kind:`XML t) in
	let t = Types.Product.pi1 (Types.Product.get t) in
	t in
      if not precise then constr
      else
	(try Types.Record.project (Types.cup t t_elt) l
	 with Not_found -> assert false)
873
874
875
876

  | RemoveField (e,l) ->
      let t = type_check env e Types.Record.any true in
      let t = Types.Record.remove_field t l in
877
      verify loc t constr
878
879
880
881
882
883
884
885
886
887

  | 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
888
      verify loc t constr
889

890
  | Validate (e, t, _) ->
891
      ignore (type_check env e Types.any false);
892
      verify loc t constr
893

894
895
  | Ref (e,t) ->
      ignore (type_check env e (Types.descr t) false);
896
      verify loc (Builtin_defs.ref_type t) constr
897

898
  | External (t,_) ->
899
900
      verify loc t constr

901
  | Op (op,_,args) ->
902
      let args = List.map (type_check env) args in
903
      let t = localize loc (typ_op op args constr) precise in
904
      verify loc t constr
905
906
907

  | NsTable (ns,e) ->
      type_check' loc env e constr precise
908

909
and type_check_pair ?(kind=`Normal) loc env e1 e2 constr precise =
910
  let rects = Types.Product.normal ~kind constr in
911
912
  if Types.Product.is_empty rects then 
    (match kind with
913
914
      | `Normal -> should_have loc constr "but it is a pair"
      | `XML -> should_have loc constr "but it is an XML element");
915
  let need_s = Types.Product.need_second rects in
916
917
918
919
920
  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
921

922
  if precise then 
923
924
925
    match kind with
      | `Normal -> Types.times (Types.cons t1) (Types.cons t2)
      | `XML -> Types.xml (Types.cons t1) (Types.cons t2)
926
927
928
  else
    constr

929
930
931
932
933
934
935
936
937
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
938
      let ch = Chars.V.mk_int ch in