typer.ml 34.4 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
24
25
exception NonExhaustive of Types.descr
exception Constraint of Types.descr * Types.descr
exception ShouldHave of Types.descr * string
exception ShouldHave2 of Types.descr * string * Types.descr
exception WrongLabel of Types.descr * label
exception UnboundId of id * bool
exception UnboundExtId of Types.CompUnit.t * id
exception Error of string
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
37
38
39
40
type ext =
  | ECDuce of Types.CompUnit.t   (* CDuce unit *)
  | 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
52
53
54
let load_schema = ref (fun _ _ -> assert false)
let from_comp_unit = ref (fun _ -> assert false)
let has_comp_unit = ref (fun _ -> assert false)
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
(* TODO: filter out builtin defs ? *)
64
65
66
67
let serialize_item s = function
  | Type t -> Serialize.Put.bits 1 s 0; Types.serialize s t
  | Val t -> Serialize.Put.bits 1 s 1; Types.serialize s t

68
let serialize s env =
69
  Serialize.Put.env Id.serialize serialize_item Env.iter s env.ids;
70
71
72
  Ns.serialize_table s env.ns;

  let schs =
73
74
75
    UEnv.fold 
      (fun name cu accu -> 
	 match cu with ESchema uri -> (name,uri)::accu | _ -> accu) 
76
      env.cu [] in
77
78
  Serialize.Put.list 
    (Serialize.Put.pair U.serialize Serialize.Put.string) s schs
79

80
81
82
83
84
let deserialize_item s = match Serialize.Get.bits 1 s with
  | 0 -> Type (Types.deserialize s)
  | 1 -> Val (Types.deserialize s)
  | _ -> assert false

85
let deserialize s =
86
87
  let ids = 
    Serialize.Get.env Id.deserialize deserialize_item Env.add Env.empty s in
88
  let ns = Ns.deserialize_table s in
89
90
91
92
  let schs = 
    Serialize.Get.list 
      (Serialize.Get.pair U.deserialize Serialize.Get.string) s in
  let env = 
93
    { ids = ids; ns = ns; cu = UEnv.empty; keep_ns = false } in
94
  List.fold_left (fun env (name,uri) -> type_schema env name uri) env schs
95
96


97
98
let empty_env = {
  ids = Env.empty;
99
  ns = Ns.def_table;
100
  cu = UEnv.empty;
101
  keep_ns = false
102
103
}

104
let enter_cu x cu env =
105
  { env with cu = UEnv.add x (ECDuce cu) env.cu }
106

107
let find_cu loc x env =
108
  try UEnv.find x env.cu
109
110
111
112
  with Not_found ->
    if !has_comp_unit x then (ECDuce (Types.CompUnit.mk x))
    else if !has_ocaml_unit x then (EOCaml (U.get_str x))
    else error loc ("Cannot find external unit " ^ (U.to_string x))
113
114


115
let find_schema x env =
116
117
118
119
120
121
  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)))
122

123
124
125
126
127
128
129
130
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
131
    | Val _ -> raise Not_found
132

133

134
let enter_value id t env = 
135
  { env with ids = Env.add id (Val t) env.ids }
136
137
let enter_values l env =
  { env with ids = 
138
      List.fold_left (fun accu (id,t) -> Env.add id (Val t) accu) env.ids l }
139
140
141
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 }
142
143
let find_value id env =
  match Env.find id env.ids with
144
    | Val t -> t
145
    | _ -> raise Not_found
146
147
148
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))
149
	
150
151
152
153
154
155
let value_name_ok id env =
  try match Env.find id env.ids with
    | Val t -> true
    | _ -> false
  with Not_found -> true

156
157
158
159
let iter_values env f =
  Env.iter (fun x ->
	      function Val t -> f x t;
		| _ -> ()) env.ids
160

161

162
let register_types cu env =
163
164
165
  Env.iter (fun x t -> match t with
	      | Type t -> Types.Print.register_global cu (Ident.value x) t
	      | _ -> ()) env.ids
166

167

168
(* Namespaces *)
169

170
let set_ns_table_for_printer env = 
171
  Ns.InternalPrinter.set_table env.ns
172

173
let get_ns_table tenv = tenv.ns
174

175
let type_ns env p ns =
176
  { env with ns = Ns.add_prefix p ns env.ns }
177

178
179
180
let type_keep_ns env k =
  { env with keep_ns = k }

181
182
183
184
185
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))
186

187
188
189
let qname env loc t = 
  protect_error_ns loc (Ns.map_tag env.ns) t
    
190
191
192
193
194
195
196
197
198
199
let ident env loc t =
  let q = protect_error_ns loc (Ns.map_attr env.ns) t in
  Ident.ident q

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

200
let parse_atom env loc t =
201
  Atoms.V.of_qname (qname env loc t)
202
203
 
let parse_ns env loc ns =
204
  protect_error_ns loc (Ns.map_prefix env.ns) ns
205

206
let parse_label env loc t =
207
  let (ns,l) = protect_error_ns loc (Ns.map_attr env.ns) t in
208
  LabelPool.mk (ns,l)
209

210
211
212
213
214
215
216
217
218
219
220
221
222
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
223
  | Const c -> c
224
225
226
227
  | _ -> 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 *)
228

229

230
231
232
233
let get_schema_names env = 
  UEnv.fold 
    (fun n cu acc -> match cu with ESchema _ -> n :: acc | _ -> acc) env.cu []
    
234
235
let find_schema_component uri name =
  Env.find (Ident.ident name) (Hashtbl.find schemas uri)
236

237
238
239
let get_schema_validator uri name =
  snd (find_schema_component uri name)

240
let find_schema_descr uri (name : Ns.qname) =
241
  try fst (find_schema_component uri name)
242
243
244
  with Not_found ->    
    raise (Error (Printf.sprintf "No component named '%s' found in schema '%s'"
		    (Ns.QName.to_string name) uri))
245
246


247
248
249
250
251
252
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 *)
    | ESchema s -> find_schema_descr s (Ident.value id)
	
253

254
module IType = struct
255
  open Typepat
256
257
258
259
260
261
262
263
264
265

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

266
267
  let all_delayed = ref []

268
269
  let clean_on_err () = all_delayed := []

270
271
272
273
274
275
  let delayed loc =
    let s = mk_delayed () in
    all_delayed := (loc,s) :: !all_delayed;
    s

  let check_one_delayed (loc,p) =
276
    if not (check_wf p) then error loc "Ill-formed recursion"
277
278
279
280
281
    
  let check_delayed () =
    let l = !all_delayed in
    all_delayed := []; 
    List.iter check_one_delayed l
282

283
  let rec derecurs env p = match p.descr with
284
    | PatVar (cu,v) -> derecurs_var env p.loc cu v
285
    | Recurs (p,b) -> derecurs (fst (derecurs_def env b)) p
286
    | Internal t -> mk_type t
287
    | NsT ns -> 
288
289
290
291
292
293
294
295
	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)
296
297
298
299
    | Record (o,r) -> 
	let aux = function
	  | (p,Some e) -> (derecurs env p, Some (derecurs env e))
	  | (p,None) -> derecurs env p, None in
300
301
302
303
304
305
306
	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)
307
	  
308
309
310
311
312
313
314
315
316
  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)
317
	  
318
319
320
321
322
  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 
323
	   with Not_found -> 
324
325
	     try mk_type (find_type v env.penv_tenv)
	     with Not_found -> mk_capture v)
326
      | Some cu ->
327
	  (try mk_type (find_type_global loc cu v env.penv_tenv)
328
329
330
331
	   with Not_found ->
	     raise_loc_generic loc 
	       ("Unbound external type " ^ (U.get_str cu) ^ "." ^ 
		  (Ident.to_string v)))
332
333
	      
  and derecurs_def env b =
334
335
336
337
338
339
340
341
342
343
344
345
346
    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

347
348
349
    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
350
    List.iter (fun (v,p,s) -> link s (derecurs env p)) b;
351
352
    (env, b)

353
354
  let derec penv p =
    let d = derecurs penv p in
355
    elim_concats ();
356
357
358
    check_delayed ();
    internalize d;
    d
359
360


361
(* API *)
362

363
364
365
366
367
368
369
  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))

370
  let type_defs env b =
371
372
373
374
375
376
    let _,b' = derecurs_def (penv env) b in
    elim_concats ();
    check_delayed ();
    let aux loc d =
      internalize d;
      check_no_fv loc d;
377
      try typ d
378
      with Patterns.Error s -> raise_loc_generic loc s
379
    in
380
    let b = 
381
382
383
      List.map2 
	(fun (loc,v,p) (v',_,d) ->
	   let t = aux loc d in
384
385
386
387
	   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
388
	   (v',t)) b b' in
389
390
    List.iter (fun (v,t) -> Types.Print.register_global 
		 (Types.CompUnit.get_current ()) (Id.value v) t) b;
391
    enter_types b env
392

393
394
395
396
  let type_defs env b =
    try type_defs env b
    with exn -> clean_on_err (); raise exn

397
  let typ env t = 
398
399
400
401
402
403
    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
404
405

  let pat env t = 
406
407
408
409
410
    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
411

412
end
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428

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



429

430
431
(* II. Build skeleton *)

432

433
type type_fun = Types.t -> bool -> Types.t
434

435
module Fv = IdSet
436

437
438
439
type branch = Branch of Typed.branch * branch list

let cur_branch : branch list ref = ref []
440

441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
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

458

459
let ops = Hashtbl.create 13
460
461
let register_op op arity f = Hashtbl.add ops op (arity,f)
let typ_op op = snd (Hashtbl.find ops op)
462

463
464
465
466
467
let fun_name env a =
  match a.fun_name with
    | None -> None
    | Some (loc,s) -> Some (ident env loc s)

468
let is_op env s = 
469
470
471
472
473
474
475
476
477
478
  if (Env.mem s env.ids) then None
  else
    let (ns,s) = Id.value s in
    if Ns.equal ns Ns.empty then
      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
479

480
481
let rec expr env loc = function
  | LocatedExpr (loc,e) -> expr env loc e
482
  | Forget (e,t) ->
483
      let (fv,e) = expr env loc e and t = typ env t in
484
      exp loc fv (Typed.Forget (e,t))
485
486
  | Check (e,t) ->
      let (fv,e) = expr env loc e and t = typ env t in
487
      exp loc fv (Typed.Check (ref Types.empty,e,t))
488
  | Var s -> var env loc s
489
  | Apply (e1,e2) -> 
490
491
492
493
494
495
496
497
      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
498
  | (Integer _ | Char _ | Atom _ | Const _) as c -> 
499
      exp loc Fv.empty (Typed.Cst (const env loc c))
500
  | Pair (e1,e2) ->
501
      let (fv1,e1) = expr env loc e1 and (fv2,e2) = expr env loc e2 in
502
503
      exp loc (Fv.cup fv1 fv2) (Typed.Pair (e1,e2))
  | Xml (e1,e2) ->
504
      let (fv1,e1) = expr env loc e1 and (fv2,e2) = expr env loc e2 in
505
506
      let n = if env.keep_ns then Some env.ns else None in
      exp loc (Fv.cup fv1 fv2) (Typed.Xml (e1,e2,n))
507
508
  | Dot _ as e ->
      dot loc env e
509
  | RemoveField (e,l) ->
510
511
      let (fv,e) = expr env loc e in
      exp loc fv (Typed.RemoveField (e,parse_label env loc l))
512
513
  | RecordLitt r -> 
      let fv = ref Fv.empty in
514
      let r = parse_record env loc
515
		(fun e -> 
516
		   let (fv2,e) = expr env loc e 
517
518
519
		   in fv := Fv.cup !fv fv2; e)
		r in
      exp loc !fv (Typed.RecordLitt r)
520
  | String (i,j,s,e) ->
521
      let (fv,e) = expr env loc e in
522
      exp loc fv (Typed.String (i,j,s,e))
523
  | Match (e,b) -> 
524
525
      let (fv1,e) = expr env loc e
      and (fv2,b) = branches env b in
526
      exp loc (Fv.cup fv1 fv2) (Typed.Match (e, b))
527
  | Map (e,b) ->
528
529
      let (fv1,e) = expr env loc e
      and (fv2,b) = branches env b in
530
531
      exp loc (Fv.cup fv1 fv2) (Typed.Map (e, b))
  | Transform (e,b) ->
532
533
      let (fv1,e) = expr env loc e
      and (fv2,b) = branches env b in
534
      exp loc (Fv.cup fv1 fv2) (Typed.Transform (e, b))
535
  | Xtrans (e,b) ->
536
537
      let (fv1,e) = expr env loc e
      and (fv2,b) = branches env b in
538
      exp loc (Fv.cup fv1 fv2) (Typed.Xtrans (e, b))
539
  | Validate (e,schema,elt) ->
540
      let (fv,e) = expr env loc e in
541
      let uri = find_schema schema env in
542
      exp loc fv (Typed.Validate (e, uri, qname env loc elt))
543
544
  | SelectFW (e,from,where) ->
      select_from_where env loc e from where
545
  | Try (e,b) ->
546
547
      let (fv1,e) = expr env loc e
      and (fv2,b) = branches env b in
548
      exp loc (Fv.cup fv1 fv2) (Typed.Try (e, b))
549
  | NamespaceIn (pr,ns,e) ->
550
      let env = type_ns env pr ns in
551
      expr env loc e
552
553
  | KeepNsIn (k,e) ->
      expr (type_keep_ns env k) loc e
554
  | Ref (e,t) ->
555
      let (fv,e) = expr env loc e and t = typ env t in
556
      exp loc fv (Typed.Ref (e,t))
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574

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))
575
576
577
578
579
580
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


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
608
609
610
611
	
and extern loc env s args = 
  let args = List.map (typ env) args in
  try
612
613
614
615
616
617
    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
618
619
620
621
    exp loc Fv.empty (Typed.External (t,i))
  with exn -> raise_loc loc exn
    
and var env loc s =
622
623
  let id = ident env loc s in
  match is_op env id with
624
    | Some (s,arity) -> 
625
626
627
628
629
630
631
	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
632
	exp loc Fv.empty e
633
    | None ->
634
635
636
	(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)
637
638
639
640
641
642
643
644
645
646
647
648
649

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
650
  let fun_name = fun_name env a in
651
  let env' = 
652
    match fun_name with 
653
654
655
656
      | None -> env
      | Some f -> enter_values_dummy [ f ] env
  in
  let (fv0,body) = branches env' a.fun_body in
657
  let fv = match fun_name with
658
659
660
    | None -> fv0
    | Some f -> Fv.remove f fv0 in
  let e = Typed.Abstraction 
661
	    { Typed.fun_name = fun_name;
662
663
664
665
666
667
668
669
670
671
672
673
674
	      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 := [];
675
676
677
678
679
    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
680
681
682
    (match Fv.pick (Fv.diff fvp fv2) with
       | None -> ()
       | Some x ->
683
	   let x = Ident.to_string x in
684
685
686
687
688
	   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;
689
    accept := Types.cup !accept (Types.descr (Patterns.accept p));
690
691
692
    let br = 
      { 
	Typed.br_loc = br_loc;
693
	Typed.br_used = br_loc == noloc;
694
695
	Typed.br_vars_empty = fvp;
	Typed.br_pat = p;
696
697
698
699
700
701
702
703
704
705
706
	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;
   } 
  )
707

708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
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 -> ... *)
733
    let br = { Typed.br_loc = ploc;
734
735
736
	  Typed.br_used = false;
	  Typed.br_vars_empty = fvp;
	  Typed.br_pat = p;
737
738
739
740
741
	  Typed.br_body = rest } in
    cur_branch := [ Branch (br, !cur_branch) ];
    let b = {
      Typed.br_typ = Types.empty;
      Typed.br_branches = [ br ];
742
743
744
745
746
      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
747
748
  let cur_br = !cur_branch in
  cur_branch := [];
749
  let (fv,e) = expr !env noloc (Pair(e,cst_nil)) in
750
  cur_branch := !cur_branch @ cur_br;
751
752
753
754
755
756
757
758
759
760
  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

761
let expr env e = snd (expr env noloc e)
762

763
764
let let_decl env p e =
  { Typed.let_pat = pat env p;
765
    Typed.let_body = expr env e }
766

767
768
769

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

770

771
772
(* III. Type-checks *)

773
774
open Typed

775
776
777
778
779
780
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

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

784
let verify loc t s = 
785
786
  require loc t s; t

787
788
789
790
let verify_noloc t s =
  if not (Types.subtype t s) then raise (Constraint (t, s));
  t

791
792
793
794
795
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 = 
796
797
  raise_loc loc (ShouldHave (constr,s))

798
799
800
let should_have_str loc ofs constr s = 
  raise_loc_str loc ofs (ShouldHave (constr,s))

801
let flatten arg constr precise =
802
803
804
805
806
807
808
809
810
  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
811
    verify_noloc (Sequence.flatten t) constr
812

813
814
let rec type_check env e constr precise = 
  let d = type_check' e.exp_loc env e.exp_descr constr precise in
815
  let d = if precise then d else constr in
816
817
818
  e.exp_typ <- Types.cup e.exp_typ d;
  d

819
and type_check' loc env e constr precise = match e with
820
821
822
  | Forget (e,t) ->
      let t = Types.descr t in
      ignore (type_check env e t false);
823
      verify loc t constr
824

825
826
827
  | Check (t0,e,t) ->
      let te = type_check env e Types.any true in
      t0 := Types.cup !t0 te;
828
      verify loc (Types.cap te (Types.descr t)) constr
829

830
  | Abstraction a ->
831
832
833
      let t =
	try Types.Arrow.check_strenghten a.fun_typ constr 
	with Not_found -> 
834
835
	  should_have loc constr
	    "but the interface of the abstraction is not compatible"
836
      in
837
838
      let env = match a.fun_name with
	| None -> env
839
	| Some f -> enter_value f a.fun_typ env in
840
841
      List.iter 
	(fun (t1,t2) ->
842
843
844
	   let acc = a.fun_body.br_accept in 
	   if not (Types.subtype t1 acc) then
	     raise_loc loc (NonExhaustive (Types.diff t1 acc));
845
	   ignore (type_check_branches loc env t1 a.fun_body t2 false)
846
847
	) a.fun_iface;
      t
848

849
850
  | Match (e,b) ->
      let t = type_check env e b.br_accept true in
851
      type_check_branches loc env t b constr precise
852
853
854

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

858
859
  | Pair (e1,e2) ->
      type_check_pair loc env e1 e2 constr precise
860

861
  | Xml (e1,e2,_) ->
862
      type_check_pair ~kind:`XML loc env e1 e2 constr precise
863

864
  | RecordLitt r ->
865
866
867
868
869
870
      type_record loc env r constr precise

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

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

873
874
875
876
  | 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
877
878
879
880
881
882
883
      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
884
      verify loc res constr
885
886

  | Var s -> 
887
      verify loc (find_value s env) constr
888

889
  | ExtVar (cu,s,t) ->
890
      verify loc t constr
891
  | Cst c -> 
892
      verify loc (Types.constant c) constr
893

894
895
896
  | String (i,j,s,e) ->
      type_check_string loc env 0 s i j e constr precise

897
  | Dot (e,l) ->
898
899
900
901
902
903
904
905
906
907
908
909
910
911
      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)
912
913
914
915

  | RemoveField (e,l) ->
      let t = type_check env e Types.Record.any true in
      let t = Types.Record.remove_field t l in
916
      verify loc t constr
917
918
919
920
921
922
923
924
925
926

  | 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
927
      verify loc t constr
928

929
  | Validate (e, uri, name) ->
930
      ignore (type_check env e Types.any false);
931
      let t = find_schema_descr uri name in
932
      verify loc t constr
933

934
935
  | Ref (e,t) ->
      ignore (type_check env e (Types.descr t) false);
936
      verify loc (Builtin_defs.ref_type t) constr
937

938
  | External (t,_) ->
939
940
      verify loc t constr

941
  | Op (op,_,args) ->
942
      let args = List.map (type_check env) args in
943
      let t = localize loc (typ_op op args constr) precise in
944
      verify loc t constr
945
946
947

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