typer.ml 37 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;
Pietro Abate's avatar
WIP    
Pietro Abate committed
53
54
  delta : Var.Set.t;
  gamma : Var.var Env.t;
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
93
94
95
(* 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



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

102
103
104
105
106
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 }
107

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

116
117
let enter_id x i env =
  { env with ids = Env.add x i env.ids }
118
119


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

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

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

146

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

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

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

167

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

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

188

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

224
225
226
227
228
229
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
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
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
259
    | _ -> raise Not_found
260
261

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

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

287
module IType = struct
288
  open Typepat
289
290
291
292
293
294

(* From AST to the intermediate representation *)

  type penv = {
    penv_tenv : t;
    penv_derec : node Env.t;
295
    penv_var : (string, Var.var) Hashtbl.t;
296
297
  }

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

300
301
  let all_delayed = ref []

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

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

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

317
  let rec derecurs variance env p =
Pietro Abate's avatar
Pietro Abate committed
318
319
320
321
322
323
    let neg = function
      |`Covariant -> `ContraVariant
      |`ContraVariant -> `Covariant
      |cv -> cv
    in
    match p.descr with
324
325
326
    | TVar s -> begin
        try
          let v = Hashtbl.find env.penv_var s in
327
328
          Var.ch_variance variance v;
          mk_type (Types.var v)
329
        with Not_found -> begin
330
          let v = Var.mk ~variance s in
331
332
333
334
          Hashtbl.add env.penv_var s v;
          mk_type (Types.var v)
        end
    end
335
    | PatVar ids -> derecurs_var env p.loc ids
Pietro Abate's avatar
Pietro Abate committed
336
    | Recurs (p,b) -> derecurs variance (fst (derecurs_def variance env b)) p
337
    | Internal t -> mk_type t
338
    | NsT ns -> 
339
	mk_type (Types.atom (Atoms.any_in_ns (parse_ns env.penv_tenv p.loc ns)))
Pietro Abate's avatar
Pietro Abate committed
340
341
342
343
344
345
346
    | 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)
347
348
    | Record (o,r) -> 
	let aux = function
Pietro Abate's avatar
Pietro Abate committed
349
350
	  | (p,Some e) -> (derecurs variance env p, Some (derecurs variance env e))
	  | (p,None) -> derecurs variance env p, None in
351
352
353
354
	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
355
356
357
    | 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)
358
	  
Pietro Abate's avatar
Pietro Abate committed
359
  and derecurs_regexp variance env = function
360
    | Epsilon -> mk_epsilon
Pietro Abate's avatar
Pietro Abate committed
361
362
363
364
365
366
367
    | 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)
368
	  
369
370
371
372
  and derecurs_var env loc ids =
    match ids with
      | [v] ->
	  let v = ident env.penv_tenv loc v in
373
	  (try Env.find v env.penv_derec 
374
	   with Not_found -> 
375
	     try mk_type (find_local_type env.penv_tenv loc v)
376
	     with Not_found -> mk_capture v)
377
378
      | ids ->
	  mk_type (find_global_type env.penv_tenv loc ids)
379
	      
Pietro Abate's avatar
Pietro Abate committed
380
  and derecurs_def variance env b =
381
382
383
384
385
386
387
388
389
390
391
392
393
    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

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

Pietro Abate's avatar
Pietro Abate committed
399
400
  let derec ?(variance=`Covariant) penv p =
    let d = derecurs variance penv p in
401
    elim_concats ();
402
    check_delayed ();
403
    internalize d;
404
    d
405

406
(* API *)
407

408
409
410
411
412
413
414
  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))

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

436
437
438
439
  let type_defs env b =
    try type_defs env b
    with exn -> clean_on_err (); raise exn

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

  let pat env t = 
449
450
451
452
453
    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
454

455
end
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471

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



472

473
474
(* II. Build skeleton *)

475

476
type type_fun = Types.t -> bool -> Types.t
477

478
module Fv = IdSet
479

480
481
482
type branch = Branch of Typed.branch * branch list

let cur_branch : branch list ref = ref []
483

484
let exp' loc e = 
Pietro Abate's avatar
WIP    
Pietro Abate committed
485
  { Typed.exp_loc = loc; Typed.exp_typ = Types.empty; Typed.exp_descr = e }
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500

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

501

502
let ops = Hashtbl.create 13
503
504
let register_op op arity f = Hashtbl.add ops op (arity,f)
let typ_op op = snd (Hashtbl.find ops op)
505

506
507
508
509
510
let fun_name env a =
  match a.fun_name with
    | None -> None
    | Some (loc,s) -> Some (ident env loc s)

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

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

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;
611
	Typed.br_ghost = false;
612
613
614
615
616
	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;
617
	Typed.br_ghost = false;
618
619
620
621
622
623
	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))
624
625


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

683
684
685
686
687
688
689
690
691
692
693
694
695

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

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

811
let expr env e = snd (expr env noloc e)
812

813
814
let let_decl env p e =
  { Typed.let_pat = pat env p;
815
    Typed.let_body = expr env e }
816

817
818
819

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

820

821
822
(* III. Type-checks *)

823
824
open Typed

825
let localize loc f x =
Pietro Abate's avatar
WIP    
Pietro Abate committed
826
827
828
829
  try f x with 
  | (Error _ | Constraint (_,_)) as exn -> 
      raise (Cduce_loc.Location (loc,`Full,exn))
  | Warning (s,t) -> warning loc s; t
830

831
832
let require loc t s = 
  if not (Types.subtype t s) then raise_loc loc (Constraint (t, s))
833

834
let verify loc t s = 
835
836
  require loc t s; t

837
838
839
840
let verify_noloc t s =
  if not (Types.subtype t s) then raise (Constraint (t, s));
  t

841
842
843
844
845
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 = 
846
847
  raise_loc loc (ShouldHave (constr,s))

848
849
850
let should_have_str loc ofs constr s = 
  raise_loc_str loc ofs (ShouldHave (constr,s))

851
let flatten arg constr precise =
852
853
854
855
856
857
858
859
860
  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
861
    verify_noloc (Sequence.flatten t) constr
862

863

864
let rec type_check env e constr precise = 
Pietro Abate's avatar
WIP    
Pietro Abate committed
865
  let (ed,d) = type_check' e.exp_loc env e.exp_descr constr precise in
866
  let d = if precise then d else constr in
867
  e.exp_typ <- Types.cup e.exp_typ d;
Pietro Abate's avatar
WIP    
Pietro Abate committed
868
  e.exp_descr <- ed;
869
870
  d

Pietro Abate's avatar
WIP    
Pietro Abate committed
871
and type_check' loc env ed constr precise = match ed with
872
873
874
  | Forget (e,t) ->
      let t = Types.descr t in
      ignore (type_check env e t false);
Pietro Abate's avatar
WIP    
Pietro Abate committed
875
      (ed,verify loc t constr)
876

877
878
879
  | Check (t0,e,t) ->
      let te = type_check env e Types.any true in
      t0 := Types.cup !t0 te;
Pietro Abate's avatar
WIP    
Pietro Abate committed
880
      (ed,verify loc (Types.cap te (Types.descr t)) constr)
881

882
  | Abstraction a ->
883
      let t =
Pietro Abate's avatar
WIP    
Pietro Abate committed
884
885
886
887
        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"
888
      in
Pietro Abate's avatar
WIP    
Pietro Abate committed
889
      let env = match a.fun_name with
Pietro Abate's avatar
Pietro Abate committed
890
891
892
893
        | None -> env
        | Some f -> enter_value f a.fun_typ env 
      in
      List.iter (fun (t1,t2) ->
894
895
896
	   let acc = a.fun_body.br_accept in 
	   if not (Types.subtype t1 acc) then
	     raise_loc loc (NonExhaustive (Types.diff t1 acc));
897
	   ignore (type_check_branches loc env t1 a.fun_body t2 false)
898
	) a.fun_iface;
Pietro Abate's avatar
WIP    
Pietro Abate committed
899
      (ed,t)
900

901
902
  | Match (e,b) ->
      let t = type_check env e b.br_accept true in
Pietro Abate's avatar
WIP    
Pietro Abate committed
903
      (Match(e.exp_descr,b),type_check_branches loc env t b constr precise)
904
905
906

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

910
  | Pair (e1,e2) ->
Pietro Abate's avatar
WIP    
Pietro Abate committed
911
      (ed,type_check_pair loc env e1 e2 constr precise)
912

913
  | Xml (e1,e2,_) ->
Pietro Abate's avatar
WIP    
Pietro Abate committed
914
      (ed,type_check_pair ~kind:`XML loc env e1 e2 constr precise)
915

916
  | RecordLitt r ->
Pietro Abate's avatar
WIP    
Pietro Abate committed
917
      (ed,type_record loc env r constr precise)
918
919

  | Map (e,b) ->
Pietro Abate's avatar
WIP    
Pietro Abate committed
920
      (ed,type_map loc env false e b constr precise)
921
922

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

925
926
927
928
  | 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
929
      let res =
930
931
932
        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
933
934
935
936
        else begin
          ignore (type_check env e2 dom false); 
          Types.Arrow.apply_noarg t1
        end
937
      in
Pietro Abate's avatar
WIP    
Pietro Abate committed
938
      (ed,verify loc res constr)
939
940

  | Var s -> 
Pietro Abate's avatar
WIP    
Pietro Abate committed
941
      (ed,verify loc (find_value s env) constr)
942

943
  | TVar s -> 
Pietro Abate's avatar
WIP    
Pietro Abate committed
944
      (ed,verify loc (find_value s env) constr)
945

946
  | ExtVar (cu,s,t) ->
Pietro Abate's avatar
WIP    
Pietro Abate committed
947
      (ed,verify loc t constr)
948

949
  | Cst c -> 
Pietro Abate's avatar
WIP    
Pietro Abate committed
950
      (ed,verify loc (Types.constant c) constr)
951

952
  | String (i,j,s,e) ->
Pietro Abate's avatar
WIP    
Pietro Abate committed
953
      (ed,type_check_string loc env 0 s i j e constr precise)
954

955
  | Dot (e,l) ->
956
957
      let expect_rec = Types.record l (Types.cons constr) in
      let expect_elt = 
958
959
        Types.xml 
          Types.any_node 
Pietro Abate's avatar
WIP    
Pietro Abate committed
960
961
          (Types.cons (Types.times (Types.cons expect_rec) Types.any_node)) 
      in
962
963
      let t = type_check env e (Types.cup expect_rec expect_elt) precise in
      let t_elt =
Pietro Abate's avatar
WIP    
Pietro Abate committed
964
965
966
967
968
969
970
971
972
        let t = Types.Product.pi2 (Types.Product.get ~kind:`XML t) in
        let t = Types.Product.pi1 (Types.Product.get t)
	  in t 
        in
      let t' = 
        if not precise then constr else
        (try Types.Record.project (Types.cup t t_elt) l
         with Not_found -> assert false)
      in (ed,t')
973
974
975
976

  | RemoveField (e,l) ->
      let t = type_check env e Types.Record.any true in
      let t = Types.Record.remove_field t l in
Pietro Abate's avatar
WIP    
Pietro Abate committed
977
      (ed,verify loc t constr)
978
979
980
981

  | Xtrans (e,b) ->
      let t = type_check env e Sequence.any true in
      let t = 
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
        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,<