typer.ml 36.5 KB
Newer Older
1
open Cduce_loc
2
3
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 = Cduce_loc.get_viewport () in
13
  let ppf = if Html.is_html v then Html.ppf v else Format.err_formatter in
14
15
  Cduce_loc.print_loc ppf (loc,`Full);
  Cduce_loc.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 ->
Pietro Abate's avatar
Pietro Abate committed
134
      error loc "Cannot resolve this identifier"
135
136
137
138
139
140
141

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

184

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

let find_value id env =
258
  match Env.find id env.ids with
259
    | Val t | EVal (_,_,t) -> t
260
    | _ -> raise Not_found
261

262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
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"

283
module IType = struct
284
  open Typepat
285
286
287
288
289
290

(* From AST to the intermediate representation *)

  type penv = {
    penv_tenv : t;
    penv_derec : node Env.t;
291
    penv_var : (string, Var.var) Hashtbl.t;
292
293
  }

294
  let penv tenv = { penv_tenv = tenv; penv_derec = Env.empty ; penv_var = Hashtbl.create 17 }
295

296
297
  let all_delayed = ref []

298
299
  let clean_on_err () = all_delayed := []

300
301
302
303
304
305
  let delayed loc =
    let s = mk_delayed () in
    all_delayed := (loc,s) :: !all_delayed;
    s

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

313
  let rec derecurs variance env p =
Pietro Abate's avatar
Pietro Abate committed
314
315
316
317
318
319
    let neg = function
      |`Covariant -> `ContraVariant
      |`ContraVariant -> `Covariant
      |cv -> cv
    in
    match p.descr with
320
321
322
    | TVar s -> begin
        try
          let v = Hashtbl.find env.penv_var s in
323
324
          Var.ch_variance variance v;
          mk_type (Types.var v)
325
        with Not_found -> begin
326
          let v = Var.mk ~variance s in
327
328
329
330
          Hashtbl.add env.penv_var s v;
          mk_type (Types.var v)
        end
    end
331
    | PatVar ids -> derecurs_var env p.loc ids
Pietro Abate's avatar
Pietro Abate committed
332
    | Recurs (p,b) -> derecurs variance (fst (derecurs_def variance env b)) p
333
    | Internal t -> mk_type t
334
    | NsT ns -> 
335
	mk_type (Types.atom (Atoms.any_in_ns (parse_ns env.penv_tenv p.loc ns)))
Pietro Abate's avatar
Pietro Abate committed
336
337
338
339
340
341
342
    | Or (p1,p2) -> mk_or (derecurs variance env p1) (derecurs variance env p2)
    | And (p1,p2) -> mk_and (derecurs variance env p1) (derecurs variance env p2)
    | Diff (p1,p2) -> mk_diff (derecurs variance env p1) (derecurs (neg variance) env p2)
    | Prod (p1,p2) -> mk_prod (derecurs variance env p1) (derecurs variance env p2)
    | XmlT (p1,p2) -> mk_xml (derecurs variance env p1) (derecurs variance env p2)
    | Arrow (p1,p2) -> mk_arrow (derecurs (neg variance) env p1) (derecurs variance env p2)
    | Optional p -> mk_optional (derecurs variance env p)
343
344
    | Record (o,r) -> 
	let aux = function
Pietro Abate's avatar
Pietro Abate committed
345
346
	  | (p,Some e) -> (derecurs variance env p, Some (derecurs variance env e))
	  | (p,None) -> derecurs variance env p, None in
347
348
349
350
	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))
Pietro Abate's avatar
Pietro Abate committed
351
352
353
    | Regexp r -> rexp (derecurs_regexp variance env r)
    | Concat (p1,p2) ->  mk_concat (derecurs variance env p1) (derecurs variance env p2)
    | Merge (p1,p2) -> mk_merge (derecurs variance env p1) (derecurs variance env p2)
354
	  
Pietro Abate's avatar
Pietro Abate committed
355
  and derecurs_regexp variance env = function
356
    | Epsilon -> mk_epsilon
Pietro Abate's avatar
Pietro Abate committed
357
358
359
360
361
362
363
    | Elem p -> mk_elem (derecurs variance env p)
    | Guard p -> mk_guard (derecurs variance env p)
    | Seq (p1,p2) -> mk_seq (derecurs_regexp variance env p1) (derecurs_regexp variance env p2)
    | Alt (p1,p2) -> mk_alt (derecurs_regexp variance env p1) (derecurs_regexp variance env p2)
    | Star p -> mk_star (derecurs_regexp variance env p)
    | WeakStar p -> mk_weakstar (derecurs_regexp variance env p)
    | SeqCapture (loc,x,p) -> mk_seqcapt (ident env.penv_tenv loc x) (derecurs_regexp variance env p)
364
	  
365
366
367
368
  and derecurs_var env loc ids =
    match ids with
      | [v] ->
	  let v = ident env.penv_tenv loc v in
369
	  (try Env.find v env.penv_derec 
370
	   with Not_found -> 
371
	     try mk_type (find_local_type env.penv_tenv loc v)
372
	     with Not_found -> mk_capture v)
373
374
      | ids ->
	  mk_type (find_global_type env.penv_tenv loc ids)
375
	      
Pietro Abate's avatar
Pietro Abate committed
376
  and derecurs_def variance env b =
377
378
379
380
381
382
383
384
385
386
387
388
389
    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

390
    let n = List.fold_left (fun env (v,p,s) -> Env.add v s env) env.penv_derec b in
391
    let env = { env with penv_derec = n } in
Pietro Abate's avatar
Pietro Abate committed
392
    List.iter (fun (v,p,s) -> link s (derecurs variance env p)) b;
393
394
    (env, b)

Pietro Abate's avatar
Pietro Abate committed
395
396
  let derec ?(variance=`Covariant) penv p =
    let d = derecurs variance penv p in
397
    elim_concats ();
398
    check_delayed ();
399
    internalize d;
400
    d
401

402
(* API *)
403

404
405
406
407
408
409
410
  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))

411
  let type_defs env b =
Pietro Abate's avatar
Pietro Abate committed
412
    let _,b' = derecurs_def `Covariant (penv env) b in
413
414
415
416
417
    elim_concats ();
    check_delayed ();
    let aux loc d =
      internalize d;
      check_no_fv loc d;
418
      try typ d
419
      with Patterns.Error s -> raise_loc_generic loc s
420
    in
421
    let b = 
422
423
424
      List.map2 
	(fun (loc,v,p) (v',_,d) ->
	   let t = aux loc d in
425
426
427
	   if (loc <> noloc) && (Types.is_empty t) then
	     warning loc 
	       ("This definition yields an empty type for " ^ (U.to_string v));
428
	   (v',t)) b b' in
429
    List.iter (fun (v,t) -> Types.Print.register_global "" v t) b;
430
    enter_types b env
431

432
433
434
435
  let type_defs env b =
    try type_defs env b
    with exn -> clean_on_err (); raise exn

Pietro Abate's avatar
Pietro Abate committed
436
  let typ ?(variance=`Covariant) env t = 
437
    try
Pietro Abate's avatar
Pietro Abate committed
438
      let d = derec ~variance (penv env) t in
439
440
441
442
      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
443
444

  let pat env t = 
445
446
447
448
449
    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
450

451
end
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467

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



468

469
470
(* II. Build skeleton *)

471

472
type type_fun = Types.t -> bool -> Types.t
473

474
module Fv = IdSet
475

476
477
478
type branch = Branch of Typed.branch * branch list

let cur_branch : branch list ref = ref []
479

480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
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

497

498
let ops = Hashtbl.create 13
499
500
let register_op op arity f = Hashtbl.add ops op (arity,f)
let typ_op op = snd (Hashtbl.find ops op)
501

502
503
504
505
506
let fun_name env a =
  match a.fun_name with
    | None -> None
    | Some (loc,s) -> Some (ident env loc s)

507
let is_op env s = 
508
509
  if (Env.mem s env.ids) then None
  else
510
511
    let (ns,s) = s in
    if Ns.Uri.equal ns Ns.empty then
512
513
514
515
516
517
      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
518

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

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;
607
	Typed.br_ghost = false;
608
609
610
611
612
	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;
613
	Typed.br_ghost = false;
614
615
616
617
618
619
	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))
620
621


622
and dot loc env0 e args =
623
  let dot_access loc (fv,e) l =
624
625
626
627
628
629
630
631
632
633
634
635
    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 -> 
636
	(match find_id_comp env0 env0 loc id with
637
638
639
640
641
642
643
644
645
646
	   | 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"
647
648
649
650
	
and extern loc env s args = 
  let args = List.map (typ env) args in
  try
651
652
653
654
655
656
    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
657
658
659
660
    exp loc Fv.empty (Typed.External (t,i))
  with exn -> raise_loc loc exn
    
and var env loc s =
661
662
  let id = ident env loc s in
  match is_op env id with
663
    | Some (s,arity) -> 
664
665
666
667
668
669
670
	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
671
	exp loc Fv.empty e
672
    | None ->
673
674
675
676
677
678
	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"

679
680
681
682
683
684
685
686
687
688
689
690
691

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

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

806
let expr env e = snd (expr env noloc e)
807

808
809
let let_decl env p e =
  { Typed.let_pat = pat env p;
810
    Typed.let_body = expr env e }
811

812
813
814

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

815

816
817
(* III. Type-checks *)

818
819
open Typed

820
821
822
let localize loc f x =
  try f x
  with 
823
    | (Error _ | Constraint (_,_)) as exn -> raise (Cduce_loc.Location (loc,`Full,exn))
824
825
    | Warning (s,t) -> warning loc s; t

826
827
let require loc t s = 
  if not (Types.subtype t s) then raise_loc loc (Constraint (t, s))
828

829
let verify loc t s = 
830
831
  require loc t s; t

832
833
834
835
let verify_noloc t s =
  if not (Types.subtype t s) then raise (Constraint (t, s));
  t

836
837
838
839
840
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 = 
841
842
  raise_loc loc (ShouldHave (constr,s))

843
844
845
let should_have_str loc ofs constr s = 
  raise_loc_str loc ofs (ShouldHave (constr,s))

846
let flatten arg constr precise =
847
848
849
850
851
852
853
854
855
  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
856
    verify_noloc (Sequence.flatten t) constr
857

858

859
860
let rec type_check env e constr precise = 
  let d = type_check' e.exp_loc env e.exp_descr constr precise in
861
  let d = if precise then d else constr in
862
863
864
  e.exp_typ <- Types.cup e.exp_typ d;
  d

865
and type_check' loc env e constr precise = match e with
866
867
868
  | Forget (e,t) ->
      let t = Types.descr t in
      ignore (type_check env e t false);
869
      verify loc t constr
870

871
872
873
  | Check (t0,e,t) ->
      let te = type_check env e Types.any true in
      t0 := Types.cup !t0 te;
874
      verify loc (Types.cap te (Types.descr t)) constr
875

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

895
896
  | Match (e,b) ->
      let t = type_check env e b.br_accept true in
897
      type_check_branches loc env t b constr precise
898
899
900

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

904
905
  | Pair (e1,e2) ->
      type_check_pair loc env e1 e2 constr precise
906

907
  | Xml (e1,e2,_) ->
908
      type_check_pair ~kind:`XML loc env e1 e2 constr precise
909

910
  | RecordLitt r ->
911
912
913
914
915
916
      type_record loc env r constr precise

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

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

919
920
921
922
  | 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
923
      let res =
924
925
926
927
928
        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)
929
      in
930
      verify loc res constr
931
932

  | Var s -> 
933
      verify loc (find_value s env) constr
934

935
936
937
  | TVar s -> 
      verify loc (find_value s env) constr

938
  | ExtVar (cu,s,t) ->
939
      verify loc t constr
940

941
  | Cst c -> 
942
      verify loc (Types.constant c) constr
943

944
945
946
  | String (i,j,s,e) ->
      type_check_string loc env 0 s i j e constr precise

947
  | Dot (e,l) ->
948
949
      let expect_rec = Types.record l (Types.cons constr) in
      let expect_elt = 
950
951
952
        Types.xml 
          Types.any_node 
          (Types.cons (Types.times (Types.cons expect_rec) Types.any_node)) in
953
954
955
956
957
958
959
960
961
      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)
962
963
964
965

  | RemoveField (e,l) ->
      let t = type_check env e Types.Record.any true in
      let t = Types.Record.remove_field t l in
966
      verify loc t constr
967
968
969
970

  | Xtrans (e,b) ->
      let t = type_check env e Sequence.any true in
      let t = 
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
        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
        with (Sequence.Error _) as exn -> 
          let rec find_loc = function
            | Cduce_loc.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 (Cduce_loc.Location (loc,precise,exn))
          with Not_found ->
            raise_loc loc exn
        in
        verify loc t constr
994

995
  | Validate (e, t, _) ->
996
      ignore (type_check env e Types.any false);
997
      verify loc t constr
998

999
1000
  | Ref (e,t) ->
      ignore (type_check env e (Types.descr t) false);
1001
      verify loc (Builtin_defs.ref_type t) constr
1002

1003
  | External (t,_) ->
1004
1005
      verify loc t constr

1006
  | Op (op,_,args) ->
1007
      let args = List.map (type_check env) args in
1008
      let t = localize loc (typ_op op args constr) precise in