typer.ml 33.7 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
  | Dot (LocatedExpr (_,Var cu), id, tyargs) when not (has_value cu env) ->
508
509
      (match find_cu loc cu env with
	 | ECDuce cu ->
510
511
	     if tyargs != [] then
	       error loc "CDuce externals cannot have type argument";
512
513
514
515
	     let id = ident env loc id in
	     let t = find_value_global loc cu id env in
	     exp loc Fv.empty (Typed.ExtVar (cu, id, t))
	 | EOCaml cu ->
516
	     extern loc env (cu ^ "." ^ U.get_str id) tyargs
517
518
519
	       (* TODO: allow nested OCaml modules A.B.C.x *)
	 | ESchema _ ->
	     error loc "Schema don't export values")
520
  | Dot (e,l,[]) ->
521
522
      let (fv,e) = expr env loc e in
      exp loc fv (Typed.Dot (e,parse_label env loc l))
523
524
  | Dot (_,_,_::_) ->
      error loc "Field access cannot have type arguments"
525
  | RemoveField (e,l) ->
526
527
      let (fv,e) = expr env loc e in
      exp loc fv (Typed.RemoveField (e,parse_label env loc l))
528
529
  | RecordLitt r -> 
      let fv = ref Fv.empty in
530
      let r = parse_record env loc
531
		(fun e -> 
532
		   let (fv2,e) = expr env loc e 
533
534
535
		   in fv := Fv.cup !fv fv2; e)
		r in
      exp loc !fv (Typed.RecordLitt r)
536
  | String (i,j,s,e) ->
537
      let (fv,e) = expr env loc e in
538
      exp loc fv (Typed.String (i,j,s,e))
539
  | Match (e,b) -> 
540
541
      let (fv1,e) = expr env loc e
      and (fv2,b) = branches env b in
542
      exp loc (Fv.cup fv1 fv2) (Typed.Match (e, b))
543
  | Map (e,b) ->
544
545
      let (fv1,e) = expr env loc e
      and (fv2,b) = branches env b in
546
547
      exp loc (Fv.cup fv1 fv2) (Typed.Map (e, b))
  | Transform (e,b) ->
548
549
      let (fv1,e) = expr env loc e
      and (fv2,b) = branches env b in
550
      exp loc (Fv.cup fv1 fv2) (Typed.Transform (e, b))
551
  | Xtrans (e,b) ->
552
553
      let (fv1,e) = expr env loc e
      and (fv2,b) = branches env b in
554
      exp loc (Fv.cup fv1 fv2) (Typed.Xtrans (e, b))
555
  | Validate (e,schema,elt) ->
556
      let (fv,e) = expr env loc e in
557
      let uri = find_schema schema env in
558
      exp loc fv (Typed.Validate (e, uri, qname env loc elt))
559
560
  | SelectFW (e,from,where) ->
      select_from_where env loc e from where
561
  | Try (e,b) ->
562
563
      let (fv1,e) = expr env loc e
      and (fv2,b) = branches env b in
564
      exp loc (Fv.cup fv1 fv2) (Typed.Try (e, b))
565
  | NamespaceIn (pr,ns,e) ->
566
      let env = type_ns env pr ns in
567
      expr env loc e
568
569
  | KeepNsIn (k,e) ->
      expr (type_keep_ns env k) loc e
570
  | Ref (e,t) ->
571
      let (fv,e) = expr env loc e and t = typ env t in
572
      exp loc fv (Typed.Ref (e,t))
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590

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))
591
592
593
594
	
and extern loc env s args = 
  let args = List.map (typ env) args in
  try
595
596
597
598
599
600
    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
601
602
603
604
    exp loc Fv.empty (Typed.External (t,i))
  with exn -> raise_loc loc exn
    
and var env loc s =
605
606
  let id = ident env loc s in
  match is_op env id with
607
    | Some (s,arity) -> 
608
609
610
611
612
613
614
	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
615
	exp loc Fv.empty e
616
    | None ->
617
618
619
	(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)
620
621
622
623
624
625
626
627
628
629
630
631
632

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
633
  let fun_name = fun_name env a in
634
  let env' = 
635
    match fun_name with 
636
637
638
639
      | None -> env
      | Some f -> enter_values_dummy [ f ] env
  in
  let (fv0,body) = branches env' a.fun_body in
640
  let fv = match fun_name with
641
642
643
    | None -> fv0
    | Some f -> Fv.remove f fv0 in
  let e = Typed.Abstraction 
644
	    { Typed.fun_name = fun_name;
645
646
647
648
649
650
651
652
653
654
655
656
657
	      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 := [];
658
659
660
661
662
    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
663
664
665
    (match Fv.pick (Fv.diff fvp fv2) with
       | None -> ()
       | Some x ->
666
	   let x = Ident.to_string x in
667
668
669
670
671
	   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;
672
    accept := Types.cup !accept (Types.descr (Patterns.accept p));
673
674
675
    let br = 
      { 
	Typed.br_loc = br_loc;
676
	Typed.br_used = br_loc == noloc;
677
678
	Typed.br_vars_empty = fvp;
	Typed.br_pat = p;
679
680
681
682
683
684
685
686
687
688
689
	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;
   } 
  )
690

691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
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 -> ... *)
    let b = {
      Typed.br_typ = Types.empty;
      Typed.br_branches = [
	{ Typed.br_loc = ploc;
	  Typed.br_used = false;
	  Typed.br_vars_empty = fvp;
	  Typed.br_pat = p;
	  Typed.br_body = rest } ];
      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
729
  let (fv,e) = expr !env noloc (Pair(e,cst_nil)) in
730
731
732
733
734
735
736
737
738
739
  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

740
let expr env e = snd (expr env noloc e)
741

742
743
let let_decl env p e =
  { Typed.let_pat = pat env p;
744
    Typed.let_body = expr env e }
745

746
747
748

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

749

750
751
(* III. Type-checks *)

752
753
open Typed

754
755
756
757
758
759
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

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

763
let verify loc t s = 
764
765
  require loc t s; t

766
767
768
769
let verify_noloc t s =
  if not (Types.subtype t s) then raise (Constraint (t, s));
  t

770
771
772
773
774
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 = 
775
776
  raise_loc loc (ShouldHave (constr,s))

777
778
779
let should_have_str loc ofs constr s = 
  raise_loc_str loc ofs (ShouldHave (constr,s))

780
let flatten arg constr precise =
781
782
783
784
785
786
787
788
789
  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
790
    verify_noloc (Sequence.flatten t) constr
791

792
793
let rec type_check env e constr precise = 
  let d = type_check' e.exp_loc env e.exp_descr constr precise in
794
  let d = if precise then d else constr in
795
796
797
  e.exp_typ <- Types.cup e.exp_typ d;
  d

798
and type_check' loc env e constr precise = match e with
799
800
801
  | Forget (e,t) ->
      let t = Types.descr t in
      ignore (type_check env e t false);
802
      verify loc t constr
803

804
805
806
  | Check (t0,e,t) ->
      let te = type_check env e Types.any true in
      t0 := Types.cup !t0 te;
807
      verify loc (Types.cap te (Types.descr t)) constr
808

809
  | Abstraction a ->
810
811
812
      let t =
	try Types.Arrow.check_strenghten a.fun_typ constr 
	with Not_found -> 
813
814
	  should_have loc constr
	    "but the interface of the abstraction is not compatible"
815
      in
816
817
      let env = match a.fun_name with
	| None -> env
818
	| Some f -> enter_value f a.fun_typ env in
819
820
      List.iter 
	(fun (t1,t2) ->
821
822
823
	   let acc = a.fun_body.br_accept in 
	   if not (Types.subtype t1 acc) then
	     raise_loc loc (NonExhaustive (Types.diff t1 acc));
824
	   ignore (type_check_branches loc env t1 a.fun_body t2 false)
825
826
	) a.fun_iface;
      t
827

828
829
  | Match (e,b) ->
      let t = type_check env e b.br_accept true in
830
      type_check_branches loc env t b constr precise
831
832
833

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

837
838
  | Pair (e1,e2) ->
      type_check_pair loc env e1 e2 constr precise
839

840
  | Xml (e1,e2,_) ->
841
      type_check_pair ~kind:`XML loc env e1 e2 constr precise
842

843
  | RecordLitt r ->
844
845
846
847
848
849
      type_record loc env r constr precise

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

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

852
853
854
855
  | 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
856
857
858
859
860
861
862
      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
863
      verify loc res constr
864
865

  | Var s -> 
866
      verify loc (find_value s env) constr
867

868
  | ExtVar (cu,s,t) ->
869
      verify loc t constr
870
  | Cst c -> 
871
      verify loc (Types.constant c) constr
872

873
874
875
  | String (i,j,s,e) ->
      type_check_string loc env 0 s i j e constr precise

876
  | Dot (e,l) ->
877
878
879
880
881
882
883
884
885
886
887
888
889
890
      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)
891
892
893
894

  | RemoveField (e,l) ->
      let t = type_check env e Types.Record.any true in
      let t = Types.Record.remove_field t l in
895
      verify loc t constr
896
897
898
899
900
901
902
903
904
905

  | 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
906
      verify loc t constr
907

908
  | Validate (e, uri, name) ->
909
      ignore (type_check env e Types.any false);
910
      let t = find_schema_descr uri name in
911
      verify loc t constr
912

913
914
  | Ref (e,t) ->
      ignore (type_check env e (Types.descr t) false);
915
      verify loc (Builtin_defs.ref_type t) constr
916

917
  | External (t,_) ->
918
919
      verify loc t constr

920
  | Op (op,_,args) ->
921
      let args = List.map (type_check env) args in
922
      let t = localize loc (typ_op op args constr) precise in
923
      verify loc t constr
924
925
926

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

928
and type_check_pair ?(kind=`Normal) loc env e1 e2 constr precise =
929
  let rects = Types.Product.normal ~kind constr in
930
931
  if Types.Product.is_empty rects then 
    (match kind with
932
933
      | `Normal -> should_have loc constr "but it is a pair"
      | `XML -> should_have loc constr "but it is an XML element");
Pietro Abate's avatar