typer.ml 38.1 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
  delta : Var.Set.t;
Pietro Abate's avatar
Pietro Abate committed
54
  gamma : Types.Node.t id_map;
55
  ns: Ns.table;
56
  keep_ns: bool
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
(* 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

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

99
100
101
102
103
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 }
104

105
106
let empty_env = {
  ids = Env.empty;
107
  delta = Var.Set.empty; (* set of bounded type variables *)
Pietro Abate's avatar
Pietro Abate committed
108
  gamma = IdMap.empty; (* map from expression variables to types *)
109
110
  ns = Ns.def_table;
  keep_ns = false
111
112
}

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


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

129
130
131
132
133
134
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
135
      error loc "Cannot resolve this identifier"
136
137
138
139
140
141
142

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

143

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

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

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

164

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

170
171
172
173
174
175
176
177
178
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
179
  | Const c -> c
180
181
182
183
  | _ -> 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 *)
184

185

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

221
222
223
224
225
226
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
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
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
256
    | _ -> raise Not_found
257
258

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

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

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

(* From AST to the intermediate representation *)

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

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

297
298
  let all_delayed = ref []

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

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

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

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

376
    let n = List.fold_left (fun env (v,p,s) -> Env.add v s env) env.penv_derec b in
377
    let env = { env with penv_derec = n } in
378
    List.iter (fun (v,p,s) -> link s (derecurs env p)) b;
379
380
    (env, b)

381
382
  let derec penv p =
    let d = derecurs penv p in
383
    elim_concats ();
384
    check_delayed ();
385
    internalize d;
386
    d
387

388
(* API *)
389

390
391
392
393
394
395
396
  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))

397
  let type_defs env b =
398
    let _,b' = derecurs_def (penv env) b in
399
400
401
402
403
    elim_concats ();
    check_delayed ();
    let aux loc d =
      internalize d;
      check_no_fv loc d;
404
      try typ d
405
      with Patterns.Error s -> raise_loc_generic loc s
406
    in
407
    let b = 
408
409
410
      List.map2 
	(fun (loc,v,p) (v',_,d) ->
	   let t = aux loc d in
411
412
413
	   if (loc <> noloc) && (Types.is_empty t) then
	     warning loc 
	       ("This definition yields an empty type for " ^ (U.to_string v));
414
	   (v',t)) b b' in
415
    List.iter (fun (v,t) -> Types.Print.register_global "" v t) b;
416
    enter_types b env
417

418
419
420
421
  let type_defs env b =
    try type_defs env b
    with exn -> clean_on_err (); raise exn

422
  let typ env t = 
423
    try
424
      let d = derec (penv env) t in
425
426
427
428
      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
429
430

  let pat env t = 
431
432
433
434
435
    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
436

437
end
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453

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



454

455
456
(* II. Build skeleton *)

457

458
type type_fun = Types.t -> bool -> Types.t
459

460
module Fv = IdSet
461

462
463
464
type branch = Branch of Typed.branch * branch list

let cur_branch : branch list ref = ref []
465

466
let exp' loc e = 
Pietro Abate's avatar
Pietro Abate committed
467
  { Typed.exp_loc = loc; Typed.exp_typ = Types.empty; Typed.exp_descr = e }
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482

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

483

484
let ops = Hashtbl.create 13
485
486
let register_op op arity f = Hashtbl.add ops op (arity,f)
let typ_op op = snd (Hashtbl.find ops op)
487

488
489
490
491
492
let fun_name env a =
  match a.fun_name with
    | None -> None
    | Some (loc,s) -> Some (ident env loc s)

493
494
495
496
497
let count_arg_name = ref 0
let fresh_arg_name () =
    incr count_arg_name;
    "__abstr_arg" ^ (string_of_int !count_arg_name)

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

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

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;
598
	Typed.br_ghost = false;
599
	Typed.br_vars_empty = Fv.empty;
600
	Typed.br_vars_poly = IdMap.empty;
601
602
603
604
	Typed.br_pat = pat_true;
	Typed.br_body = yes };
      { Typed.br_loc = no.Typed.exp_loc;
	Typed.br_used = false;
605
	Typed.br_ghost = false;
606
	Typed.br_vars_empty = Fv.empty;
607
	Typed.br_vars_poly = IdMap.empty;
608
609
610
611
612
	Typed.br_pat = pat_false;
	Typed.br_body = no } ];
    Typed.br_accept = Builtin_defs.bool;
  } in
  exp' loc (Typed.Match (cond,b))
613
614


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

672
673
674
675
676
677
678
679
680
681
682
683
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
684
  let fun_name = fun_name env a in
685
  let env' = 
686
    match fun_name with 
687
688
689
690
      | None -> env
      | Some f -> enter_values_dummy [ f ] env
  in
  let (fv0,body) = branches env' a.fun_body in
691
  let fv = match fun_name with
692
693
694
    | None -> fv0
    | Some f -> Fv.remove f fv0 in
  let e = Typed.Abstraction 
695
	    { Typed.fun_name = fun_name;
696
697
698
699
700
701
702
703
704
705
706
707
708
	      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 := [];
709
710
711
712
713
    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
714
715
716
    (match Fv.pick (Fv.diff fvp fv2) with
       | None -> ()
       | Some x ->
717
	   let x = Ident.to_string x in
718
719
	   warning br_loc 
	     ("The capture variable " ^ x ^ 
Pietro Abate's avatar
Pietro Abate committed
720
721
	      " 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)."));
722
723
    let fv2 = Fv.diff fv2 fvp in
    fv := Fv.cup !fv fv2;
724
    accept := Types.cup !accept (Types.descr (Patterns.accept p));
725
    let ghost = br_loc == noloc in
726
727
728
    let br = 
      { 
	Typed.br_loc = br_loc;
729
730
	Typed.br_used = ghost;
	Typed.br_ghost = ghost;
731
	Typed.br_vars_empty = fvp;
732
	Typed.br_vars_poly = IdMap.empty;
733
	Typed.br_pat = p;
734
735
736
737
738
739
740
741
742
743
744
	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;
   } 
  )
745

746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
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 -> ... *)
771
    let br = { Typed.br_loc = ploc;
772
	  Typed.br_used = false;
773
	  Typed.br_ghost = false;
774
	  Typed.br_vars_empty = fvp;
775
        Typed.br_vars_poly = IdMap.empty;
776
	  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
let localize loc f x =
Pietro Abate's avatar
Pietro Abate committed
816
817
818
819
  try f x with 
  | (Error _ | Constraint (_,_)) as exn -> 
      raise (Cduce_loc.Location (loc,`Full,exn))
  | Warning (s,t) -> warning loc s; t
820

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
831
let verify_noloc t s =
  if not (Types.subtype t s) then raise (Constraint (t, s));
  t

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

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

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

854
(* Typed -> Typed *)
855
let rec type_check env e constr precise = 
Pietro Abate's avatar
Pietro Abate committed
856
  let (ed,d) = type_check' e.exp_loc env e.exp_descr constr precise in
857
  let d = if precise then d else constr in
858
  e.exp_typ <- Types.cup e.exp_typ d;
Pietro Abate's avatar
Pietro Abate committed
859
  e.exp_descr <- ed;
860
861
  d

Pietro Abate's avatar
Pietro Abate committed
862
and type_check' loc env ed constr precise = match ed with
863
864
865
  | Forget (e,t) ->
      let t = Types.descr t in
      ignore (type_check env e t false);
Pietro Abate's avatar
Pietro Abate committed
866
      (ed,verify loc t constr)
867
868

  | Subst (e, sigma) -> (* (ed,type_check env e constr precise) *) assert false
869

870
871
872
  | Check (t0,e,t) ->
      let te = type_check env e Types.any true in
      t0 := Types.cup !t0 te;
Pietro Abate's avatar
Pietro Abate committed
873
      (ed,verify loc (Types.cap te (Types.descr t)) constr)
874

875
  | Abstraction a ->
876
      let t =
Pietro Abate's avatar
Pietro Abate committed
877
878
879
880
        try Types.Arrow.check_strenghten a.fun_typ constr 
        with Not_found -> 
          should_have loc constr
            "but the interface of the abstraction is not compatible"
881
      in
882
      let env = match a.fun_name with
Pietro Abate's avatar
Pietro Abate committed
883
884
885
        | None -> env
        | Some f -> enter_value f a.fun_typ env 
      in
886
887
      (* update \delta with all variables in t1 -> t2 *)

Pietro Abate's avatar
Pietro Abate committed
888
889
890
891
892
893
894
895
896
897
898
899
      let deltaintf =
        let union (t1,t2) = Var.Set.union (Types.all_vars(t1)) (Types.all_vars(t2)) in
        match a.fun_iface with
        |[] -> Var.Set.empty
        |head::tail ->
            List.fold_left (fun acc inf ->
              Var.Set.inter (union inf) acc
            ) (union head) tail
      in

      let env = {env with delta = Var.Set.union env.delta deltaintf } in

Pietro Abate's avatar
WIP    
Pietro Abate committed
900
      (* I check the body with all possible t1 -> t2 types *)
901
      let sll = 
902
903
904
905
906
        List.fold_left (fun tacc (t1,t2) ->
          let acc = a.fun_body.br_accept in
          if not (Types.subtype t1 acc) then
            raise_loc loc (NonExhaustive (Types.diff t1 acc));
          let t = type_check_branches loc env t1 a.fun_body t2 false in
Pietro Abate's avatar
Pietro Abate committed
907
          (fst(Types.squaresubtype env.delta t t2))::tacc (* H_j *)
908
909
        ) [] a.fun_iface
      in
910
911
912
913
914
915
916
917
      List.iter (fun sl ->
        if not(Types.Tallying.is_identity sl) then
          List.iter (fun br ->
            let e = br.br_body in
            let loc = br.br_body.exp_loc in
            br.br_body <- exp' loc (Subst(e,sl)); 
          ) a.fun_body.br_branches
      ) (List.rev sll);
Pietro Abate's avatar
WIP    
Pietro Abate committed
918
      (ed,t)
919

920
921
  | Match (e,b) ->
      let t = type_check env e b.br_accept true in
Pietro Abate's avatar
Pietro Abate committed
922
      (ed,type_check_branches loc env t b constr precise)
923
924
925

  | Try (e,b) ->
      let te = type_check env e constr precise in
926
      let tb = type_check_branches loc env Types.any b constr precise in
Pietro Abate's avatar
Pietro Abate committed
927
      (ed,Types.cup te tb)
928

929
  | Pair (e1,e2) ->
Pietro Abate's avatar
Pietro Abate committed
930
      (ed,type_check_pair loc env e1 e2 constr precise)
931

932
  | Xml (e1,e2,_) ->
Pietro Abate's avatar
Pietro Abate committed
933
      (ed,type_check_pair ~kind:`XML loc env e1 e2 constr precise)
934

935
  | RecordLitt r ->
Pietro Abate's avatar
Pietro Abate committed
936
      (ed,type_record loc env r constr precise)
937
938

  | Map (e,b) ->
Pietro Abate's avatar
Pietro Abate committed
939
      (ed,type_map loc env false e b constr precise)
940
941

  | Transform (e,b) ->
Pietro Abate's avatar
Pietro Abate committed
942
      (ed,localize loc (flatten (type_map loc env true e b) constr) precise)
943

944
  | Apply (e1,e2) ->
Pietro Abate's avatar
Pietro Abate committed
945
946
      let t1_t = type_check env e1 Types.Arrow.any true in
      let t1 = Types.Arrow.get t1_t in
947
      let dom = Types.Arrow.domain t1 in
948
      let res =
949
950
951
        if Types.Arrow.need_arg t1 then
          let t2 = type_check env e2 dom true in
          Types.Arrow.apply t1 t2
Pietro Abate's avatar
WIP    
Pietro Abate committed
952
953
954
955
        else begin
          ignore (type_check env e2 dom false); 
          Types.Arrow.apply_noarg t1
        end
956
      in
Pietro Abate's avatar
WIP    
Pietro Abate committed
957
      (ed,verify loc res constr)
958
959

  | Var s -> 
Pietro Abate's avatar
Pietro Abate committed
960
      (ed,verify loc (find_value s env) constr)
961

962
  | TVar s -> 
Pietro Abate's avatar
Pietro Abate committed
963
      (ed,verify loc (find_value s env) constr)
964

965
  | ExtVar (cu,s,t) ->
Pietro Abate's avatar
Pietro Abate committed
966
      (ed,verify loc t constr)
967

968
  | Cst c -> 
Pietro Abate's avatar
Pietro Abate committed
969
      (ed,verify loc (Types.constant c) constr)
970

971
  | String (i,j,s,e) ->
Pietro Abate's avatar
Pietro Abate committed
972
      (ed,type_check_string loc env 0 s i j e constr precise)