typer.ml 40.8 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;
54
  ns: Ns.table;
55
  keep_ns: bool
56
}
57

58
let pp_env ppf env =
Pietro Abate's avatar
Pietro Abate committed
59
60
61
  let pp_item ppf (s,t) = match t with
    |Val t -> Format.fprintf ppf "val %s : %a" s Types.Print.pp_type t
    |Type t -> Format.fprintf ppf "type %s = %a" s Types.Print.pp_type t
62
63
    |_ -> ()
  in
Pietro Abate's avatar
Pietro Abate committed
64
65
66
67
68
69
70
71
72
73
74
75
  let t = [ 
    "Empty";"Any";"Int";"Char";"Byte";"Atom";
    "Pair";"Arrow";"Record";
    "String";"Latin1";
    "Bool";"Float";"AnyXml";
    "Namespaces";"Caml_int" ]
  in
  let ids = 
    Env.filter (fun n _ ->
      not(List.mem (Id.to_string n) t)
    ) env.ids 
  in
Pietro Abate's avatar
Pietro Abate committed
76
  Format.printf "{ids=%a;delta=%a}"
Pietro Abate's avatar
Pietro Abate committed
77
  (Ident.pp_env pp_item) ids
Pietro Abate's avatar
Pietro Abate committed
78
  Var.Set.pp env.delta
79
80
;;

81
82
(* Namespaces *)

83
let set_ns_table_for_printer env =
84
85
86
87
88
89
90
91
92
93
  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 ->
94
    raise_loc_generic loc
95
96
    ("Undefined namespace prefix " ^ (U.to_string ns))

97
let qname env loc t =
98
  protect_error_ns loc (Ns.map_tag env.ns) t
99

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

105
106
107
108
109
110
111
112
113
114
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

115
116
let load_schema = ref (fun _ _ -> assert false)
let from_comp_unit = ref (fun _ -> assert false)
117
let load_comp_unit = ref (fun _ -> assert false)
118
119
let has_ocaml_unit = ref (fun _ -> false)
let has_static_external = ref (fun _ -> assert false)
120

121
122
123
124
125
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 }
126

127
let empty_env = {
Pietro Abate's avatar
Pietro Abate committed
128
  ids = Env.empty; (* map from expression variables to items *)
129
  delta = Var.Set.empty; (* set of bounded type variables *)
130
131
  ns = Ns.def_table;
  keep_ns = false
132
133
}

134
135
let enter_id x i env =
  { env with ids = Env.add x i env.ids }
136

137
138
let type_using env loc x cu =
  try
139
140
141
142
143
144
    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
145
let enter_types l env =
146
  { env with ids =
147
148
      List.fold_left (fun accu (id,t) -> Env.add id (Type t) accu) env.ids l }

149
150
151
152
153
154
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
155
      error loc "Cannot resolve this identifier"
156
157
158
159
160
161
162

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

163

164
let enter_value id t env =
165
  { env with ids = Env.add id (Val t) env.ids }
166

167
let enter_values l env =
168
  { env with ids =
169
170
171
    List.fold_left (fun accu (id,t) -> Env.add id (Val t) accu) env.ids l;
  }

172
let enter_values_dummy l env =
173
  { env with ids =
174
      List.fold_left (fun accu id -> Env.add id (Val Types.empty) accu) env.ids l }
175

176
177
let value_name_ok id env =
  try match Env.find id env.ids with
178
    | Val _ | EVal _ -> true
179
180
181
    | _ -> false
  with Not_found -> true

182
183
184
185
let iter_values env f =
  Env.iter (fun x ->
	      function Val t -> f x t;
		| _ -> ()) env.ids
186

187
let register_types cu env =
188
189
190
  Env.iter (fun x t -> match t with
	      | Type t -> Types.Print.register_global cu (Ident.value x) t
	      | _ -> ()) env.ids
191

192
193
194
195
196
197
198
199
200
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
201
  | Const c -> c
202
203
204
205
  | _ -> 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 *)
206

207
208
let find_schema_component sch name =
  try ESchemaComponent (Env.find name sch.sch_comps)
209
  with Not_found ->
210
    raise (Error (Printf.sprintf "No component named '%s' found in schema '%s'"
211
212
213
214
215
216
		    (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
217
	let c =
218
219
220
221
222
223
224
225
226
227
228
229
230
	  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)
231
232
233
234
235
236
    | 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"
(*
237
    | _ -> error loc "Invalid dot access"
238
*)
239

240
241
242
243
244
245
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
246

247
248
249
250
251
252
253
254
255
256
257
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
258
  { env with
259
260
      ns = Ns.add_prefix p ns env.ns;
      ids = Env.add (Ns.empty,p) (ENamespace ns) env.ids }
261

262
263
264
265
266
267
268
269
270
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"
271

272
273
274
let find_local_type env loc id =
  match Env.find id env.ids with
    | Type t -> t
275
    | _ -> raise Not_found
276
277

let find_value id env =
278
  match Env.find id env.ids with
279
    | Val t | EVal (_,_,t) -> t
280
    | _ -> raise Not_found
281

282
283
let do_open env cu =
  let env_cu = !from_comp_unit cu in
284
  let ids =
285
286
287
288
289
290
291
292
    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
293
  { env with
294
295
      ids = ids;
      ns = Ns.merge_tables env.ns env_cu.ns }
296

297
298
299
300
301
302

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"

303
module IType = struct
304
  open Typepat
305
306
307
308
309
310

(* From AST to the intermediate representation *)

  type penv = {
    penv_tenv : t;
    penv_derec : node Env.t;
311
    penv_var : (string, Var.var) Hashtbl.t;
312
313
  }

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

316
317
  let all_delayed = ref []

318
319
  let clean_on_err () = all_delayed := []

320
321
322
323
324
325
  let delayed loc =
    let s = mk_delayed () in
    all_delayed := (loc,s) :: !all_delayed;
    s

  let check_one_delayed (loc,p) =
326
    if not (check_wf p) then error loc "Ill-formed recursion"
327

328
329
  let check_delayed () =
    let l = !all_delayed in
330
    all_delayed := [];
331
    List.iter check_one_delayed l
332

Pietro Abate's avatar
Pietro Abate committed
333
  (* Ast -> symbolic type *)
334
  let rec derecurs env p =
Pietro Abate's avatar
Pietro Abate committed
335
    match p.descr with
336
    | PatVar ids -> derecurs_var env p.loc ids
337
    | Recurs (p,b) -> derecurs (fst (derecurs_def env b)) p
338
    | Internal t -> mk_type t
339
    | NsT ns ->
340
	mk_type (Types.atom (Atoms.any_in_ns (parse_ns env.penv_tenv p.loc ns)))
341
342
343
344
345
346
347
    | 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)
348
    | Record (o,r) ->
349
	let aux = function
350
351
	  | (p,Some e) -> (derecurs env p, Some (derecurs env e))
	  | (p,None) -> derecurs env p, None in
352
	mk_record o (parse_record env.penv_tenv p.loc aux r)
353
    | Constant (x,c) ->
354
355
	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))
356
357
358
    | 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)
359

360
  and derecurs_regexp env = function
361
    | Epsilon -> mk_epsilon
362
363
364
365
366
367
368
    | 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)
369

370
371
372
373
  and derecurs_var env loc ids =
    match ids with
      | [v] ->
	  let v = ident env.penv_tenv loc v in
374
375
	  (try Env.find v env.penv_derec
	   with Not_found ->
376
	     try mk_type (find_local_type env.penv_tenv loc v)
377
	     with Not_found -> mk_capture v)
378
379
      | ids ->
	  mk_type (find_global_type env.penv_tenv loc ids)
380

381
  and derecurs_def env b =
382
    let seen = ref IdSet.empty in
383
384
385
    let b =
      List.map
	(fun (loc,v,p) ->
386
	   let v = ident env.penv_tenv loc v in
387
	   if IdSet.mem !seen v then
388
	     raise_loc_generic loc
389
	       ("Multiple definitions for the type identifer " ^
390
391
392
393
394
		  (Ident.to_string v));
	   seen := IdSet.add v !seen;
	   (v,p,delayed loc))
	b in

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

400
401
  let derec penv p =
    let d = derecurs penv p in
402
    elim_concats ();
403
    check_delayed ();
404
    internalize d;
405
    d
406

407
(* API *)
408

409
410
411
412
  let check_no_fv loc n =
    match peek_fv n with
      | None -> ()
      | Some x ->
413
	  raise_loc_generic loc
414
415
	    ("Capture variable not allowed: " ^ (Ident.to_string x))

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

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

441
  let typ env t =
442
    try
443
      let d = derec (penv env) t in
444
445
446
447
      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
448

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

456
end
457
458
459
460
461
462

let typ = IType.typ
let pat = IType.pat
let type_defs = IType.type_defs

let dump_types ppf env =
463
464
  Env.iter (fun v ->
	      function
465
466
467
468
469
470
471
472
		  (Type _) -> Format.fprintf ppf " %a" Ident.print v
		| _ -> ()) env.ids

let dump_ns ppf env =
  Ns.dump_table ppf env.ns



473

474
475
(* II. Build skeleton *)

476

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

479
module Fv = IdSet
480

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

let cur_branch : branch list ref = ref []
484

485
let exp' loc e =
Pietro Abate's avatar
Pietro Abate committed
486
487
488
489
  { Typed.exp_loc = loc;
    Typed.exp_typ = Types.empty;
    Typed.exp_descr = e
  }
490
491
492
493
494

let exp loc fv e = fv, exp' loc e

let exp_nil = exp' noloc (Typed.Cst Sequence.nil_cst)

495
let pat_true =
496
497
498
499
  let n = Patterns.make Fv.empty in
  Patterns.define n (Patterns.constr Builtin_defs.true_type);
  n

500
let pat_false =
501
502
503
504
  let n = Patterns.make Fv.empty in
  Patterns.define n (Patterns.constr Builtin_defs.false_type);
  n

505

506
let ops = Hashtbl.create 13
507
508
let register_op op arity f = Hashtbl.add ops op (arity,f)
let typ_op op = snd (Hashtbl.find ops op)
509

510
511
512
513
514
let fun_name env a =
  match a.fun_name with
    | None -> None
    | Some (loc,s) -> Some (ident env loc s)

515
516
517
518
519
let count_arg_name = ref 0
let fresh_arg_name () =
    incr count_arg_name;
    "__abstr_arg" ^ (string_of_int !count_arg_name)

520
let is_op env s =
521
522
  if (Env.mem s env.ids) then None
  else
523
524
    let (ns,s) = s in
    if Ns.Uri.equal ns Ns.empty then
525
      let s = U.get_str s in
526
      try
527
528
529
530
	let o = Hashtbl.find ops s in
	Some (s, fst o)
      with Not_found -> None
    else None
531

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

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;
620
	Typed.br_ghost = false;
621
	Typed.br_vars_empty = Fv.empty;
622
	Typed.br_vars_poly = IdMap.empty;
623
624
625
626
	Typed.br_pat = pat_true;
	Typed.br_body = yes };
      { Typed.br_loc = no.Typed.exp_loc;
	Typed.br_used = false;
627
	Typed.br_ghost = false;
628
	Typed.br_vars_empty = Fv.empty;
629
	Typed.br_vars_poly = IdMap.empty;
630
631
632
633
634
	Typed.br_pat = pat_false;
	Typed.br_body = no } ];
    Typed.br_accept = Builtin_defs.bool;
  } in
  exp' loc (Typed.Match (cond,b))
635
636


637
and dot loc env0 e args =
638
  let dot_access loc (fv,e) l =
639
640
641
642
643
644
645
646
647
648
649
    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))
650
    | Var id ->
651
	(match find_id_comp env0 env0 loc id with
652
653
654
655
656
657
	   | 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
658
    | `Comp (_,EVal (cu,id,t)) ->
659
660
661
	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"
662
663

and extern loc env s args =
664
665
  let args = List.map (typ env) args in
  try
666
667
668
669
670
671
    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
672
673
    exp loc Fv.empty (Typed.External (t,i))
  with exn -> raise_loc loc exn
674

675
and var env loc s =
676
677
  let id = ident env loc s in
  match is_op env id with
678
679
    | Some (s,arity) ->
	let e = match s with
680
681
682
683
	  | "print_xml" | "print_xml_utf8" ->
	      Typed.NsTable (env.ns,Typed.Op (s, arity, []))
	  | "load_xml" when env.keep_ns ->
	      Typed.Op ("!load_xml",arity,[])
684
	  | _ -> Typed.Op (s, arity, [])
685
	in
686
	exp loc Fv.empty e
687
    | None ->
688
689
690
691
692
693
	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"

694
and abstraction env loc a =
695
696
  let iface =
    List.map
697
      (fun (t1,t2) -> (typ env t1, typ env t2)) a.fun_iface in
698
699
700
  let t =
    List.fold_left
      (fun accu (t1,t2) -> Types.cap accu (Types.arrow t1 t2))
701
      Types.any iface in
702
703
704
  let iface =
    List.map
      (fun (t1,t2) -> (Types.descr t1, Types.descr t2))
705
      iface in
706
  let fun_name = fun_name env a in
707
708
  let env' =
    match fun_name with
709
710
711
712
      | None -> env
      | Some f -> enter_values_dummy [ f ] env
  in
  let (fv0,body) = branches env' a.fun_body in
713
  let fv = match fun_name with
714
715
    | None -> fv0
    | Some f -> Fv.remove f fv0 in
716
  let e = Typed.Abstraction
717
	    { Typed.fun_name = fun_name;
718
719
720
721
722
723
	      Typed.fun_iface = iface;
	      Typed.fun_body = body;
	      Typed.fun_typ = t;
	      Typed.fun_fv = fv
	    } in
  exp loc fv e
724
725

and branches env b =
726
727
  let fv = ref Fv.empty in
  let accept = ref Types.empty in
728
  let branch (p,e) =
729
730
    let cur_br = !cur_branch in
    cur_branch := [];
731
732
    let ploc = p.loc in
    let p = pat env p in
733
734
735
736
    let () =
      let t = Types.descr (Patterns.accept p) in
      if not (Types.no_var t) then error ploc "Type variables cannot occur in patterns"
    in
737
738
739
    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
740
741
742
    (match Fv.pick (Fv.diff fvp fv2) with
       | None -> ()
       | Some x ->
743
	   let x = Ident.to_string x in
744
745
	   warning br_loc
	     ("The capture variable " ^ x ^
Pietro Abate's avatar
Pietro Abate committed
746
747
	      " 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)."));
748
749
    let fv2 = Fv.diff fv2 fvp in
    fv := Fv.cup !fv fv2;
750
    accept := Types.cup !accept (Types.descr (Patterns.accept p));
751
    let ghost = br_loc == noloc in
752
753
    let br =
      {
754
	Typed.br_loc = br_loc;
755
756
	Typed.br_used = ghost;
	Typed.br_ghost = ghost;
757
	Typed.br_vars_empty = fvp;
758
	Typed.br_vars_poly = IdMap.empty;
759
	Typed.br_pat = p;
760
761
762
763
	Typed.br_body = e } in
    cur_branch := Branch (br, !cur_branch) :: cur_br;
    br in
  let b = List.map branch b in
764
765
766
767
  (!fv,
   {
     Typed.br_typ = Types.empty;
     Typed.br_branches = b;
768
     Typed.br_accept = !accept;
769
   }
770
  )
771

772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
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

788
  let put_cond rest (fv,cond) =
789
790
    all_fv := Fv.cup (Fv.diff fv !bound_fv) !all_fv;
    if_then_else loc cond rest exp_nil in
791
  let aux (ploc,p,fvp,e) (where,rest) =
792
793
794
795
796
    (* 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 -> ... *)
797
    let br = { Typed.br_loc = ploc;
798
	  Typed.br_used = false;
799
	  Typed.br_ghost = false;
800
	  Typed.br_vars_empty = fvp;
801
        Typed.br_vars_poly = IdMap.empty;
802
	  Typed.br_pat = p;
803
804
805
806
807
	  Typed.br_body = rest } in
    cur_branch := [ Branch (br, !cur_branch) ];
    let b = {
      Typed.br_typ = Types.empty;
      Typed.br_branches = [ br ];
808
809
810
811
812
      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
813
814
  let cur_br = !cur_branch in
  cur_branch := [];
815
  let (fv,e) = expr !env noloc (Pair(e,cst_nil)) in
816
  cur_branch := !cur_branch @ cur_br;
817
818
819
820
821
822
823
824
825
826
  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

827
let expr env e = snd (expr env noloc e)
828

829
830
let let_decl env p e =
  { Typed.let_pat = pat env p;
831
    Typed.let_body = expr env e }
832

833
834
835

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

836

837
838
(* III. Type-checks *)

839
840
open Typed

841
let localize loc f x =
842
843
  try f x with
  | (Error _ | Constraint (_,_)) as exn ->
Pietro Abate's avatar
Pietro Abate committed
844
845
      raise (Cduce_loc.Location (loc,`Full,exn))
  | Warning (s,t) -> warning loc s; t
846

847
let require loc t s =
848
  if not (Types.subtype t s) then raise_loc loc (Constraint (t, s))
849

850
let verify loc t s =
Pietro Abate's avatar
Pietro Abate committed
851
  require loc t s;
852
  t
853

Pietro Abate's avatar
Pietro Abate committed
854
let squareverify loc delta t s =
855
  if not (Types.is_squaresubtype delta t s) then