typer.ml 35.2 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
  Location.print_loc ppf (loc,`Full);
15
  Location.html_hilight (loc,`Full);
16
  Format.fprintf ppf "Warning: %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
34
35
36
37
type schema = {
  sch_uri: string;
  sch_ns: Ns.Uri.t;
  sch_comps: (Types.t * Schema_validator.t) Ident.Env.t;
}

38
type item =
39
(* These are really exported by CDuce units: *)
40
  | Type of Types.t
41
  | Val of Types.t
42
43
44
45
46
47
48
49
  | ECDuce of Compunit.t
  | ESchema of schema
  | ENamespace of Ns.Uri.t
(* These are only used internally: *)
  | EVal of Compunit.t * id * Types.t
  | EOCaml of string
  | EOCamlComponent of string
  | ESchemaComponent of (Types.t * Schema_validator.t)
50

51
type t = {
52
  ids : item Env.t;
53
  ns: Ns.table;
54
  keep_ns: bool
55
}
56

57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
(* Namespaces *)

let set_ns_table_for_printer env = 
  Ns.InternalPrinter.set_table env.ns

let get_ns_table tenv = tenv.ns


let type_keep_ns env k =
  { env with keep_ns = k }

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))

let qname env loc t = 
  protect_error_ns loc (Ns.map_tag env.ns) t
    
let ident env loc t =
  protect_error_ns loc (Ns.map_attr env.ns) t

let parse_atom env loc t = Atoms.V.mk (qname env loc t)
 
let parse_ns env loc ns =
  protect_error_ns loc (Ns.map_prefix env.ns) ns

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

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



94
95
let load_schema = ref (fun _ _ -> assert false)
let from_comp_unit = ref (fun _ -> assert false)
96
let load_comp_unit = ref (fun _ -> assert false)
97
98
let has_ocaml_unit = ref (fun _ -> false)
let has_static_external = ref (fun _ -> assert false)
99

100
101
102
103
104
let type_schema env loc name uri =
  let x = ident env loc name in
  let (ns,sch) = !load_schema (U.to_string name) uri in
  let sch = { sch_uri = uri; sch_comps = sch; sch_ns = ns } in
  { env with ids = Env.add x (ESchema sch) env.ids }
105

106
107
let empty_env = {
  ids = Env.empty;
108
109
  ns = Ns.def_table;
  keep_ns = false
110
111
}

112
113
let enter_id x i env =
  { env with ids = Env.add x i env.ids }
114
115


116
let type_using env loc x cu = 
117
  try 
118
119
120
121
122
123
    let cu = !load_comp_unit cu in
    enter_id (ident env loc x) (ECDuce cu) env
  with Not_found ->
    error loc ("Cannot find external unit " ^ (U.to_string cu))

let enter_type id t env = enter_id id (Type t) env
124
125
126
127
let enter_types l env =
  { env with ids = 
      List.fold_left (fun accu (id,t) -> Env.add id (Type t) accu) env.ids l }

128
129
130
131
132
133
let find_id env0 env loc head x =
  let id = ident env0 loc x in
  try Env.find id env.ids
  with Not_found when head ->
    try ECDuce (!load_comp_unit x)
    with Not_found ->
134
135
136
137
138
139
140
141
      error loc "Cannot resolve this identifier"

let find_id_comp env0 env loc x =
  if ((match (U.get_str x).[0] with 'A'..'Z' -> true | _ -> false)
    && !has_ocaml_unit x)
  then EOCaml (U.get_str x)
  else find_id env0 env loc true x

142

143
let enter_value id t env = 
144
  { env with ids = Env.add id (Val t) env.ids }
145
146
let enter_values l env =
  { env with ids = 
147
      List.fold_left (fun accu (id,t) -> Env.add id (Val t) accu) env.ids l }
148
149
150
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 }
151

152
153
let value_name_ok id env =
  try match Env.find id env.ids with
154
    | Val _ | EVal _ -> true
155
156
157
    | _ -> false
  with Not_found -> true

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

163

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

169

170
171
172
173
174
175
176
177
178
179

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
180
  | Const c -> c
181
182
183
184
  | _ -> 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 *)
185

186

187
188
let find_schema_component sch name =
  try ESchemaComponent (Env.find name sch.sch_comps)
189
190
  with Not_found ->    
    raise (Error (Printf.sprintf "No component named '%s' found in schema '%s'"
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
		    (Ns.QName.to_string name) sch.sch_uri))


let navig loc env0 (env,comp) id =
  match comp with
    | ECDuce cu ->
	let env = !from_comp_unit cu in
	let c = 
	  try find_id env0 env loc false id
	  with Not_found -> error loc "Unbound identifier" in
	let c = match c with
	  | Val t -> EVal (cu,ident env0 loc id,t)
	  | c -> c in
	env,c
    | EOCaml cu ->
	let s = cu ^ "." ^ (U.get_str id) in
	(match (U.get_str id).[0] with
	   | 'A'..'Z' -> env,EOCaml s
	   | _ -> env,EOCamlComponent s)
    | ESchema sch ->
	env,find_schema_component sch (ident env0 loc id)
212
213
214
215
216
217
    | Type _ -> error loc "Types don't have components"
    | Val _ | EVal _ -> error loc "Values don't have components"
    | ENamespace _ -> error loc "Namespaces don't have components"
    | EOCamlComponent _ -> error loc "Caml values don't have components"
    | ESchemaComponent _ -> error loc "Schema components don't have components"
(*
218
    | _ -> error loc "Invalid dot access"
219
*)
220
	
221

222
223
224
225
226
227
let rec find_global env loc ids =
  match ids with
    | id::rest ->
	let comp = find_id env env loc true id in
	snd (List.fold_left (navig loc env) (env,comp) rest)
    | _ -> assert false
228

229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
let eval_ns env loc = function
  | `Uri ns -> ns
  | `Path ids ->
      match find_global env loc ids with
	| ENamespace ns -> ns
	| ESchema sch -> sch.sch_ns
	| _ -> error loc "This path does not refer to a namespace or schema"

let type_ns env loc p ns =
  (* TODO: check that p has no prefix *)
  let ns = eval_ns env loc ns in
  { env with 
      ns = Ns.add_prefix p ns env.ns;
      ids = Env.add (Ns.empty,p) (ENamespace ns) env.ids }
      


let find_global_type env loc ids =
  match find_global env loc ids with
    | Type t | ESchemaComponent (t,_) -> t
    | _ -> error loc "This path does not refer to a type"

let find_global_schema_component env loc ids =
  match find_global env loc ids with
    | ESchemaComponent c -> c
    | _ -> error loc "This path does not refer to a schema component"
  

let find_local_type env loc id =
  match Env.find id env.ids with
    | Type t -> t
260
    | _ -> raise Not_found
261
262

let find_value id env =
263
  match Env.find id env.ids with
264
    | Val t | EVal (_,_,t) -> t
265
    | _ -> raise Not_found
266

267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
let do_open env cu =
  let env_cu = !from_comp_unit cu in
  let ids = 
    Env.fold
      (fun n d ids ->
	 let d = match d with
	   | Val t -> EVal (cu,n,t)
	   | d -> d in
	 Env.add n d ids)
      env_cu.ids
      env.ids in
  { env with 
      ids = ids;
      ns = Ns.merge_tables env.ns env_cu.ns }
      

let type_open env loc ids =
  match find_global env loc ids with
    | ECDuce cu -> do_open env cu
    | _ -> error loc "This path does not refer to a CDuce unit"

288
module IType = struct
289
  open Typepat
290
291
292
293
294
295
296
297
298
299

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

300
301
  let all_delayed = ref []

302
303
  let clean_on_err () = all_delayed := []

304
305
306
307
308
309
  let delayed loc =
    let s = mk_delayed () in
    all_delayed := (loc,s) :: !all_delayed;
    s

  let check_one_delayed (loc,p) =
310
    if not (check_wf p) then error loc "Ill-formed recursion"
311
312
313
314
315
    
  let check_delayed () =
    let l = !all_delayed in
    all_delayed := []; 
    List.iter check_one_delayed l
316

317
  let rec derecurs env p = match p.descr with
318
    | PatVar ids -> derecurs_var env p.loc ids
319
    | Recurs (p,b) -> derecurs (fst (derecurs_def env b)) p
320
    | Internal t -> mk_type t
321
    | NsT ns -> 
322
323
324
325
326
327
328
329
	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)
330
331
332
333
    | Record (o,r) -> 
	let aux = function
	  | (p,Some e) -> (derecurs env p, Some (derecurs env e))
	  | (p,None) -> derecurs env p, None in
334
335
336
337
338
339
340
	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)
341
	  
342
343
344
345
346
347
348
349
350
  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)
351
	  
352
353
354
355
  and derecurs_var env loc ids =
    match ids with
      | [v] ->
	  let v = ident env.penv_tenv loc v in
356
	  (try Env.find v env.penv_derec 
357
	   with Not_found -> 
358
	     try mk_type (find_local_type env.penv_tenv loc v)
359
	     with Not_found -> mk_capture v)
360
361
      | ids ->
	  mk_type (find_global_type env.penv_tenv loc ids)
362
363
	      
  and derecurs_def env b =
364
365
366
367
368
369
370
371
372
373
374
375
376
    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

377
378
379
    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
380
    List.iter (fun (v,p,s) -> link s (derecurs env p)) b;
381
382
    (env, b)

383
384
  let derec penv p =
    let d = derecurs penv p in
385
    elim_concats ();
386
387
388
    check_delayed ();
    internalize d;
    d
389
390


391
(* API *)
392

393
394
395
396
397
398
399
  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))

400
  let type_defs env b =
401
402
403
404
405
406
    let _,b' = derecurs_def (penv env) b in
    elim_concats ();
    check_delayed ();
    let aux loc d =
      internalize d;
      check_no_fv loc d;
407
      try typ d
408
      with Patterns.Error s -> raise_loc_generic loc s
409
    in
410
    let b = 
411
412
413
      List.map2 
	(fun (loc,v,p) (v',_,d) ->
	   let t = aux loc d in
414
415
416
417
	   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
418
	   (v',t)) b b' in
419
    List.iter (fun (v,t) -> Types.Print.register_global "" v t) b;
420
    enter_types b env
421

422
423
424
425
  let type_defs env b =
    try type_defs env b
    with exn -> clean_on_err (); raise exn

426
  let typ env t = 
427
428
429
430
431
432
    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
433
434

  let pat env t = 
435
436
437
438
439
    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
440

441
end
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457

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



458

459
460
(* II. Build skeleton *)

461

462
type type_fun = Types.t -> bool -> Types.t
463

464
module Fv = IdSet
465

466
467
468
type branch = Branch of Typed.branch * branch list

let cur_branch : branch list ref = ref []
469

470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
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

487

488
let ops = Hashtbl.create 13
489
490
let register_op op arity f = Hashtbl.add ops op (arity,f)
let typ_op op = snd (Hashtbl.find ops op)
491

492
493
494
495
496
let fun_name env a =
  match a.fun_name with
    | None -> None
    | Some (loc,s) -> Some (ident env loc s)

497
let is_op env s = 
498
499
  if (Env.mem s env.ids) then None
  else
500
501
    let (ns,s) = s in
    if Ns.Uri.equal ns Ns.empty then
502
503
504
505
506
507
      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
508

509
510
let rec expr env loc = function
  | LocatedExpr (loc,e) -> expr env loc e
511
  | Forget (e,t) ->
512
      let (fv,e) = expr env loc e and t = typ env t in
513
      exp loc fv (Typed.Forget (e,t))
514
515
  | Check (e,t) ->
      let (fv,e) = expr env loc e and t = typ env t in
516
      exp loc fv (Typed.Check (ref Types.empty,e,t))
517
  | Var s -> var env loc s
518
  | Apply (e1,e2) -> 
519
520
521
522
523
524
525
526
      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
527
  | (Integer _ | Char _ | Atom _ | Const _) as c -> 
528
      exp loc Fv.empty (Typed.Cst (const env loc c))
529
  | Pair (e1,e2) ->
530
      let (fv1,e1) = expr env loc e1 and (fv2,e2) = expr env loc e2 in
531
532
      exp loc (Fv.cup fv1 fv2) (Typed.Pair (e1,e2))
  | Xml (e1,e2) ->
533
      let (fv1,e1) = expr env loc e1 and (fv2,e2) = expr env loc e2 in
534
535
      let n = if env.keep_ns then Some env.ns else None in
      exp loc (Fv.cup fv1 fv2) (Typed.Xml (e1,e2,n))
536
  | Dot _ as e ->
537
538
539
540
541
      dot loc env e []
  | TyArgs (Dot _ as e, args) ->
      dot loc env e args
  | TyArgs _ ->
      error loc "Only OCaml external can have type arguments"
542
  | RemoveField (e,l) ->
543
544
      let (fv,e) = expr env loc e in
      exp loc fv (Typed.RemoveField (e,parse_label env loc l))
545
546
  | RecordLitt r -> 
      let fv = ref Fv.empty in
547
      let r = parse_record env loc
548
		(fun e -> 
549
		   let (fv2,e) = expr env loc e 
550
551
552
		   in fv := Fv.cup !fv fv2; e)
		r in
      exp loc !fv (Typed.RecordLitt r)
553
  | String (i,j,s,e) ->
554
      let (fv,e) = expr env loc e in
555
      exp loc fv (Typed.String (i,j,s,e))
556
  | Match (e,b) -> 
557
558
      let (fv1,e) = expr env loc e
      and (fv2,b) = branches env b in
559
      exp loc (Fv.cup fv1 fv2) (Typed.Match (e, b))
560
  | Map (e,b) ->
561
562
      let (fv1,e) = expr env loc e
      and (fv2,b) = branches env b in
563
564
      exp loc (Fv.cup fv1 fv2) (Typed.Map (e, b))
  | Transform (e,b) ->
565
566
      let (fv1,e) = expr env loc e
      and (fv2,b) = branches env b in
567
      exp loc (Fv.cup fv1 fv2) (Typed.Transform (e, b))
568
  | Xtrans (e,b) ->
569
570
      let (fv1,e) = expr env loc e
      and (fv2,b) = branches env b in
571
      exp loc (Fv.cup fv1 fv2) (Typed.Xtrans (e, b))
572
  | Validate (e,ids) ->
573
      let (fv,e) = expr env loc e in
574
      let (t,v) = find_global_schema_component env loc ids  in
575
      exp loc fv (Typed.Validate (e, t, v))
576
577
  | SelectFW (e,from,where) ->
      select_from_where env loc e from where
578
  | Try (e,b) ->
579
580
      let (fv1,e) = expr env loc e
      and (fv2,b) = branches env b in
581
      exp loc (Fv.cup fv1 fv2) (Typed.Try (e, b))
582
  | NamespaceIn (pr,ns,e) ->
583
      let env = type_ns env loc pr ns in
584
      expr env loc e
585
586
  | KeepNsIn (k,e) ->
      expr (type_keep_ns env k) loc e
587
  | Ref (e,t) ->
588
      let (fv,e) = expr env loc e and t = typ env t in
589
      exp loc fv (Typed.Ref (e,t))
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607

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))
608
609


610
and dot loc env0 e args =
611
  let dot_access loc (fv,e) l =
612
613
614
615
616
617
618
619
620
621
622
623
    exp loc fv (Typed.Dot (e,parse_label env0 loc l)) in

  let no_args () =
    if args <> [] then
      error loc "Only OCaml externals can have type arguments" in
  let rec aux loc = function
    | LocatedExpr (loc,e) -> aux loc e
    | Dot (e,id) ->
	(match aux loc e with
	   | `Val e -> `Val (dot_access loc e id)
	   | `Comp c -> `Comp (navig loc env0 c id))
    | Var id -> 
624
	(match find_id_comp env0 env0 loc id with
625
626
627
628
629
630
631
632
633
634
	   | Val _ -> `Val (var env0 loc id)
	   | c -> `Comp (env0,c))
    | e -> `Val (expr env0 loc e)
  in
  match aux loc e with
    | `Val e -> no_args (); e
    | `Comp (_,EVal (cu,id,t)) -> 
	no_args (); exp loc Fv.empty (Typed.ExtVar (cu,id,t))
    | `Comp (_,EOCamlComponent s) -> extern loc env0 s args
    | _ -> error loc "This dot notation does not refer to a value"
635
636
637
638
	
and extern loc env s args = 
  let args = List.map (typ env) args in
  try
639
640
641
642
643
644
    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
645
646
647
648
    exp loc Fv.empty (Typed.External (t,i))
  with exn -> raise_loc loc exn
    
and var env loc s =
649
650
  let id = ident env loc s in
  match is_op env id with
651
    | Some (s,arity) -> 
652
653
654
655
656
657
658
	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
659
	exp loc Fv.empty e
660
    | None ->
661
662
663
664
665
666
	try match Env.find id env.ids with
	  | Val _ -> exp loc (Fv.singleton id) (Typed.Var id)
	  | EVal (cu,id,t) -> exp loc Fv.empty (Typed.ExtVar (cu,id,t))
	  | _ ->  error loc "This identifier does not refer to a value"
	with Not_found -> error loc "Unbound identifier"

667
668
669
670
671
672
673
674
675
676
677
678
679

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
680
  let fun_name = fun_name env a in
681
  let env' = 
682
    match fun_name with 
683
684
685
686
      | None -> env
      | Some f -> enter_values_dummy [ f ] env
  in
  let (fv0,body) = branches env' a.fun_body in
687
  let fv = match fun_name with
688
689
690
    | None -> fv0
    | Some f -> Fv.remove f fv0 in
  let e = Typed.Abstraction 
691
	    { Typed.fun_name = fun_name;
692
693
694
695
696
697
698
699
700
701
702
703
704
	      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 := [];
705
706
707
708
709
    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
710
711
712
    (match Fv.pick (Fv.diff fvp fv2) with
       | None -> ()
       | Some x ->
713
	   let x = Ident.to_string x in
714
715
716
717
718
	   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;
719
    accept := Types.cup !accept (Types.descr (Patterns.accept p));
720
721
722
    let br = 
      { 
	Typed.br_loc = br_loc;
723
	Typed.br_used = br_loc == noloc;
724
725
	Typed.br_vars_empty = fvp;
	Typed.br_pat = p;
726
727
728
729
730
731
732
733
734
735
736
	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;
   } 
  )
737

738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
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 -> ... *)
763
    let br = { Typed.br_loc = ploc;
764
765
766
	  Typed.br_used = false;
	  Typed.br_vars_empty = fvp;
	  Typed.br_pat = p;
767
768
769
770
771
	  Typed.br_body = rest } in
    cur_branch := [ Branch (br, !cur_branch) ];
    let b = {
      Typed.br_typ = Types.empty;
      Typed.br_branches = [ br ];
772
773
774
775
776
      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
777
778
  let cur_br = !cur_branch in
  cur_branch := [];
779
  let (fv,e) = expr !env noloc (Pair(e,cst_nil)) in
780
  cur_branch := !cur_branch @ cur_br;
781
782
783
784
785
786
787
788
789
790
  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

791
let expr env e = snd (expr env noloc e)
792

793
794
let let_decl env p e =
  { Typed.let_pat = pat env p;
795
    Typed.let_body = expr env e }
796

797
798
799

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

800

801
802
(* III. Type-checks *)

803
804
open Typed

805
806
807
808
809
810
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

811
812
let require loc t s = 
  if not (Types.subtype t s) then raise_loc loc (Constraint (t, s))
813

814
let verify loc t s = 
815
816
  require loc t s; t

817
818
819
820
let verify_noloc t s =
  if not (Types.subtype t s) then raise (Constraint (t, s));
  t

821
822
823
824
825
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 = 
826
827
  raise_loc loc (ShouldHave (constr,s))

828
829
830
let should_have_str loc ofs constr s = 
  raise_loc_str loc ofs (ShouldHave (constr,s))

831
let flatten arg constr precise =
832
833
834
835
836
837
838
839
840
  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
841
    verify_noloc (Sequence.flatten t) constr
842

843
844
let rec type_check env e constr precise = 
  let d = type_check' e.exp_loc env e.exp_descr constr precise in
845
  let d = if precise then d else constr in
846
847
848
  e.exp_typ <- Types.cup e.exp_typ d;
  d

849
and type_check' loc env e constr precise = match e with
850
851
852
  | Forget (e,t) ->
      let t = Types.descr t in
      ignore (type_check env e t false);
853
      verify loc t constr
854

855
856
857
  | Check (t0,e,t) ->
      let te = type_check env e Types.any true in
      t0 := Types.cup !t0 te;
858
      verify loc (Types.cap te (Types.descr t)) constr
859

860
  | Abstraction a ->
861
862
863
      let t =
	try Types.Arrow.check_strenghten a.fun_typ constr 
	with Not_found -> 
864
865
	  should_have loc constr
	    "but the interface of the abstraction is not compatible"
866
      in
867
868
      let env = match a.fun_name with
	| None -> env
869
	| Some f -> enter_value f a.fun_typ env in
870
871
      List.iter 
	(fun (t1,t2) ->
872
873
874
	   let acc = a.fun_body.br_accept in 
	   if not (Types.subtype t1 acc) then
	     raise_loc loc (NonExhaustive (Types.diff t1 acc));
875
	   ignore (type_check_branches loc env t1 a.fun_body t2 false)
876
877
	) a.fun_iface;
      t
878

879
880
  | Match (e,b) ->
      let t = type_check env e b.br_accept true in
881
      type_check_branches loc env t b constr precise
882
883
884

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

888
889
  | Pair (e1,e2) ->
      type_check_pair loc env e1 e2 constr precise
890

891
  | Xml (e1,e2,_) ->
892
      type_check_pair ~kind:`XML loc env e1 e2 constr precise
893

894
  | RecordLitt r ->
895
896
897
898
899
900
      type_record loc env r constr precise

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

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

903
904
905
906
  | 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
907
908
909
910
911
912
913
      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
914
      verify loc res constr
915
916

  | Var s -> 
917
      verify loc (find_value s env) constr
918

919
  | ExtVar (cu,s,t) ->
920
      verify loc t constr
921
  | Cst c -> 
922
      verify loc (Types.constant c) constr
923

924
925
926
  | String (i,j,s,e) ->
      type_check_string loc env 0 s i j e constr precise

927
  | Dot (e,l) ->
928
929
930
931
932
933
934
935
936
937
938
939
940
941
      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)
942
943
944
945

  | RemoveField (e,l) ->
      let t = type_check env e Types.Record.any true in
      let t = Types.Record.remove_field t l in
946
      verify loc t constr
947
948
949
950

  | Xtrans (e,b) ->
      let t = type_check env e Sequence.any true in
      let t = 
951
952
953
954
955
956
957
	try
	  Sequence.map_tree constr
	    (fun cstr t ->
	       let resid = Types.diff t b.br_accept in
	       let res = type_check_branches loc env t b cstr true in
	       (res,resid)
	    ) t
958
959
960
961
962
963
964
965
966
967
968
969
970
971
	with (Sequence.Error _) as exn -> 
	  let rec find_loc = function
	    | Location.Location (loc,precise,exn) ->
		(loc,precise), exn
	    | Sequence.Error (Sequence.UnderTag (t,exn)) ->
		let (l,exn) = find_loc exn in
		l, Sequence.Error (Sequence.UnderTag (t,exn))
	    | exn -> raise Not_found
	  in
	  try 
	    let (loc,precise), exn = find_loc exn in
	    raise (Location.Location (loc,precise,exn))
	  with Not_found ->
	    raise_loc loc exn
972
      in
973
      verify loc t constr
974

975
  | Validate (e, t, _) ->
976
      ignore (type_check env e Types.any false);
977
      verify loc t constr
978

979
980
  | Ref (e,t) ->
      ignore (type_check env e (Types.descr t) false);
981
      verify loc (Builtin_defs.ref_type t) constr
982

983
  | External (t,_) ->
984
985
      verify loc t constr

986
  | Op (op,_,args) ->
987
      let args = List.map (type_check env) args in
988
      let t = localize loc (typ_op op args constr) precise in
989
      verify loc t constr
990
991
992

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

994
and type_check_pair ?(kind=`Normal) loc env e1 e2 constr precise =
995
  let rects = Types.Product.normal ~kind constr in
996
997
  if Types.Product.is_empty rects then 
    (match kind with
998
999
      | `Normal -> should_have loc constr "but it is a pair"
      | `XML -> should_have loc constr "but it is an XML element");
1000
  let need_s = Types.Product.need_second rects in
1001
1002
1003
1004
1005
  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
1006

1007
  if precise then 
1008
1009
1010
    match kind with
      | `Normal -> Types.times (Types.cons t1) (Types.cons t2)
      | `XML -> Types.xml (Types.cons t1) (Types.cons t2)
1011
1012
1013
  else
    constr

1014
1015
1016
1017
1018
1019
1020
1021
1022
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