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

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

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

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

28
29
30
31
let raise_loc loc exn = raise (Location (loc,`Full,exn))
let raise_loc_str loc ofs exn = raise (Location (loc,`Char ofs,exn))
let error loc msg = raise_loc loc (Error msg)

32
33
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
94
95
96
97
98
99
(* 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 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

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



100
101
let load_schema = ref (fun _ _ -> assert false)
let from_comp_unit = ref (fun _ -> assert false)
102
let load_comp_unit = ref (fun _ -> assert false)
103
104
let has_ocaml_unit = ref (fun _ -> false)
let has_static_external = ref (fun _ -> assert false)
105

106
107
108
109
110
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 }
111

112
113
let empty_env = {
  ids = Env.empty;
114
115
  ns = Ns.def_table;
  keep_ns = false
116
117
}

118
119
let enter_id x i env =
  { env with ids = Env.add x i env.ids }
120
121


122
let type_using env loc x cu = 
123
  try 
124
125
126
127
128
129
    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
130
131
132
133
let enter_types l env =
  { env with ids = 
      List.fold_left (fun accu (id,t) -> Env.add id (Type t) accu) env.ids l }

134
135
136
137
138
139
140
141
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 ->
      if !has_ocaml_unit x then (EOCaml (U.get_str x))
      else error loc "Cannot resolve this identifier"
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
(*
let find_value_global loc cu id =
153
154
  try find_value id (!from_comp_unit cu)
  with Not_found -> raise_loc loc (UnboundExtId (cu,id))
155
	
156
*)
157
158
159
160
161
162
let value_name_ok id env =
  try match Env.find id env.ids with
    | Val t -> true
    | _ -> false
  with Not_found -> true

163
164
165
166
let iter_values env f =
  Env.iter (fun x ->
	      function Val t -> f x t;
		| _ -> ()) env.ids
167

168

169
let register_types cu env =
170
171
172
  Env.iter (fun x t -> match t with
	      | Type t -> Types.Print.register_global cu (Ident.value x) t
	      | _ -> ()) env.ids
173

174

175
176
177
178
179
180
181
182
183
184

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
185
  | Const c -> c
186
187
188
189
  | _ -> 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 *)
190

191

192
193
let find_schema_component sch name =
  try ESchemaComponent (Env.find name sch.sch_comps)
194
195
  with Not_found ->    
    raise (Error (Printf.sprintf "No component named '%s' found in schema '%s'"
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
		    (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)
    | _ -> error loc "Invalid dot access"
	
219

220
221
222
223
224
225
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
226

227
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
260
261
262
263
264
265
266
267
268
269
270
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
    | _ -> error loc "This identifier does not refer to a type"

let check_local_value env loc id =
  try match Env.find id env.ids with
    | Val _ -> ()
    | _ ->  error loc "This identifier does not refer to a value"
  with Not_found -> error loc "Unbound identifier"

let find_value id env =
  try match Env.find id env.ids with
    | Val t -> t
    | _ -> raise Not_found
  with Not_found -> assert false
271

272
module IType = struct
273
  open Typepat
274
275
276
277
278
279
280
281
282
283

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

284
285
  let all_delayed = ref []

286
287
  let clean_on_err () = all_delayed := []

288
289
290
291
292
293
  let delayed loc =
    let s = mk_delayed () in
    all_delayed := (loc,s) :: !all_delayed;
    s

  let check_one_delayed (loc,p) =
294
    if not (check_wf p) then error loc "Ill-formed recursion"
295
296
297
298
299
    
  let check_delayed () =
    let l = !all_delayed in
    all_delayed := []; 
    List.iter check_one_delayed l
300

301
  let rec derecurs env p = match p.descr with
302
    | PatVar ids -> derecurs_var env p.loc ids
303
    | Recurs (p,b) -> derecurs (fst (derecurs_def env b)) p
304
    | Internal t -> mk_type t
305
    | NsT ns -> 
306
307
308
309
310
311
312
313
	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)
314
315
316
317
    | Record (o,r) -> 
	let aux = function
	  | (p,Some e) -> (derecurs env p, Some (derecurs env e))
	  | (p,None) -> derecurs env p, None in
318
319
320
321
322
323
324
	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)
325
	  
326
327
328
329
330
331
332
333
334
  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)
335
	  
336
337
338
339
  and derecurs_var env loc ids =
    match ids with
      | [v] ->
	  let v = ident env.penv_tenv loc v in
340
	  (try Env.find v env.penv_derec 
341
	   with Not_found -> 
342
	     try mk_type (find_local_type env.penv_tenv loc v)
343
	     with Not_found -> mk_capture v)
344
345
      | ids ->
	  mk_type (find_global_type env.penv_tenv loc ids)
346
347
	      
  and derecurs_def env b =
348
349
350
351
352
353
354
355
356
357
358
359
360
    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

361
362
363
    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
364
    List.iter (fun (v,p,s) -> link s (derecurs env p)) b;
365
366
    (env, b)

367
368
  let derec penv p =
    let d = derecurs penv p in
369
    elim_concats ();
370
371
372
    check_delayed ();
    internalize d;
    d
373
374


375
(* API *)
376

377
378
379
380
381
382
383
  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))

384
  let type_defs env b =
385
386
387
388
389
390
    let _,b' = derecurs_def (penv env) b in
    elim_concats ();
    check_delayed ();
    let aux loc d =
      internalize d;
      check_no_fv loc d;
391
      try typ d
392
      with Patterns.Error s -> raise_loc_generic loc s
393
    in
394
    let b = 
395
396
397
      List.map2 
	(fun (loc,v,p) (v',_,d) ->
	   let t = aux loc d in
398
399
400
401
	   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
402
	   (v',t)) b b' in
403
    List.iter (fun (v,t) -> Types.Print.register_global "" v t) b;
404
    enter_types b env
405

406
407
408
409
  let type_defs env b =
    try type_defs env b
    with exn -> clean_on_err (); raise exn

410
  let typ env t = 
411
412
413
414
415
416
    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
417
418

  let pat env t = 
419
420
421
422
423
    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
424

425
end
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441

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



442

443
444
(* II. Build skeleton *)

445

446
type type_fun = Types.t -> bool -> Types.t
447

448
module Fv = IdSet
449

450
451
452
type branch = Branch of Typed.branch * branch list

let cur_branch : branch list ref = ref []
453

454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
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

471

472
let ops = Hashtbl.create 13
473
474
let register_op op arity f = Hashtbl.add ops op (arity,f)
let typ_op op = snd (Hashtbl.find ops op)
475

476
477
478
479
480
let fun_name env a =
  match a.fun_name with
    | None -> None
    | Some (loc,s) -> Some (ident env loc s)

481
let is_op env s = 
482
483
  if (Env.mem s env.ids) then None
  else
484
485
    let (ns,s) = s in
    if Ns.Uri.equal ns Ns.empty then
486
487
488
489
490
491
      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
492

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

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


594
and dot loc env0 e args =
595
  let dot_access loc (fv,e) l =
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
    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 -> 
	(match find_id env0 env0 loc true id with
	   | 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"
(*  
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
  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
648
*)
649
650
651
652
	
and extern loc env s args = 
  let args = List.map (typ env) args in
  try
653
654
655
656
657
658
    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
659
660
661
662
    exp loc Fv.empty (Typed.External (t,i))
  with exn -> raise_loc loc exn
    
and var env loc s =
663
664
  let id = ident env loc s in
  match is_op env id with
665
    | Some (s,arity) -> 
666
667
668
669
670
671
672
	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
673
	exp loc Fv.empty e
674
    | None ->
675
	check_local_value env loc id;
676
	exp loc (Fv.singleton id) (Typed.Var id)
677
678
679
680
681
682
683
684
685
686
687
688
689

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

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

801
let expr env e = snd (expr env noloc e)
802

803
804
let let_decl env p e =
  { Typed.let_pat = pat env p;
805
    Typed.let_body = expr env e }
806

807
808
809

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

810

811
812
(* III. Type-checks *)

813
814
open Typed

815
816
817
818
819
820
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

821
822
let require loc t s = 
  if not (Types.subtype t s) then raise_loc loc (Constraint (t, s))
823

824
let verify loc t s = 
825
826
  require loc t s; t

827
828
829
830
let verify_noloc t s =
  if not (Types.subtype t s) then raise (Constraint (t, s));
  t

831
832
833
834
835
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 = 
836
837
  raise_loc loc (ShouldHave (constr,s))

838
839
840
let should_have_str loc ofs constr s = 
  raise_loc_str loc ofs (ShouldHave (constr,s))

841
let flatten arg constr precise =
842
843
844
845
846
847
848
849
850
  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
851
    verify_noloc (Sequence.flatten t) constr
852

853
854
let rec type_check env e constr precise = 
  let d = type_check' e.exp_loc env e.exp_descr constr precise in
855
  let d = if precise then d else constr in
856
857
858
  e.exp_typ <- Types.cup e.exp_typ d;
  d

859
and type_check' loc env e constr precise = match e with
860
861
862
  | Forget (e,t) ->
      let t = Types.descr t in
      ignore (type_check env e t false);
863
      verify loc t constr
864

865
866
867
  | Check (t0,e,t) ->
      let te = type_check env e Types.any true in
      t0 := Types.cup !t0 te;
868
      verify loc (Types.cap te (Types.descr t)) constr
869

870
  | Abstraction a ->
871
872
873
      let t =
	try Types.Arrow.check_strenghten a.fun_typ constr 
	with Not_found -> 
874
875
	  should_have loc constr
	    "but the interface of the abstraction is not compatible"
876
      in
877
878
      let env = match a.fun_name with
	| None -> env
879
	| Some f -> enter_value f a.fun_typ env in
880
881
      List.iter 
	(fun (t1,t2) ->
882
883
884
	   let acc = a.fun_body.br_accept in 
	   if not (Types.subtype t1 acc) then
	     raise_loc loc (NonExhaustive (Types.diff t1 acc));
885
	   ignore (type_check_branches loc env t1 a.fun_body t2 false)
886
887
	) a.fun_iface;
      t
888

889
890
  | Match (e,b) ->
      let t = type_check env e b.br_accept true in
891
      type_check_branches loc env t b constr precise
892
893
894

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

898
899
  | Pair (e1,e2) ->
      type_check_pair loc env e1 e2 constr precise
900

901
  | Xml (e1,e2,_) ->
902
      type_check_pair ~kind:`XML loc env e1 e2 constr precise
903

904
  | RecordLitt r ->
905
906
907
908
909
910
      type_record loc env r constr precise

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

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

913
914
915
916
  | 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
917
918
919
920
921
922
923
      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
924
      verify loc res constr
925
926

  | Var s -> 
927
      verify loc (find_value s env) constr
928

929
  | ExtVar (cu,s,t) ->
930
      verify loc t constr
931
  | Cst c -> 
932
      verify loc (Types.constant c) constr
933

934
935
936
  | String (i,j,s,e) ->
      type_check_string loc env 0 s i j e constr precise

937
  | Dot (e,l) ->
938
939
940
941
942
943
944
945
946
947
948
949
950
951
      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)
952
953
954
955

  | RemoveField (e,l) ->
      let t = type_check env e Types.Record.any true in
      let t = Types.Record.remove_field t l in
956
      verify loc t constr
957
958
959
960
961
962
963
964
965
966

  | 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
967
      verify loc t constr
968

969
  | Validate (e, t, _) ->
970
      ignore (type_check env e Types.any false);
971
      verify loc t constr
972

973
974
  | Ref (e,t) ->
      ignore (type_check env e (Types.descr t) false);
975
      verify loc (Builtin_defs.ref_type t) constr
976

977
  | External (t,_) ->
978
979
      verify loc t constr

980
  | Op (op,_,args) ->
981
      let args = List.map (type_check env) args in
982
      let t = localize loc (typ_op op args constr) precise in
983
      verify loc t constr
984
985
986

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

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

1001
  if precise then 
1002
1003
1004
    match kind with
      | `Normal -> Types.times (Types.cons t1) (Types.cons t2)
      | `XML -> Types.xml (Types.cons t1) (Types.cons t2)
1005
1006
1007
  else
    constr

1008
1009
1010
1011
1012
1013
1014
1015
1016
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
1017
      let ch = Chars.V.mk_int ch in
1018
1019
1020
1021
1022
1023
1024
      let tch = Types.constant (Types.Char ch) in
      let t1 = check_str loc ofs tch (Types.Product.pi1 rects) in
      let c2 = Types.Product.constraint_on_2 rects t1 in
      let t2 = type_check_string loc env (ofs + 1) s i' j e c2 precise in
      if precise then Types.times (Types.cons t1) (Types.cons t2)
      else constr

1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
and type_record loc env r constr precise =
(* try to get rid of precise = true for values of fields *)
(* also: the use equivalent of need_second to optimize... *)
  if not (Types.Record.has_record constr) then
    should_have loc constr "but it is a record";
  let (rconstr,res) = 
    List.fold_left
      (fun (rconstr,res) (l,e) ->
	 (* could compute (split l e) once... *)
	 let pi = Types.Record.project_opt rconstr l in
	 if Types.is_empty pi then 
1036
	   (let l = Label.string_of_attr l in
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
	    should_have loc constr
	      (Printf.sprintf "Field %s is not allowed here." l));
	 let t = type_check env e pi true in
	 let rconstr = Types.Record.condition rconstr l t in
	 let res = (l,Types.cons t) :: res in
	 (rconstr,res)
      ) (constr, []) (LabelMap.get r)
  in
  if not (Types.Record.has_empty_record rconstr) then
    should_have loc constr "More fields should be present";
  let t = 
1048
    Types.record_fields (false, LabelMap.from_list (fun _ _ -> assert false) res)
1049
  in
1050
  verify loc t constr
1051

Pietro Abate's avatar