typer.ml 42.2 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 40 41 42 43 44 45 46 47 48 49
  (* These are really exported by CDuce units: *)
| Type of (Types.t * Var.t array)
| Val of Types.t
| 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
  let pp_item ppf (s,t) = match t with
    |Val t -> Format.fprintf ppf "val %s : %a" s Types.Print.pp_type t
Pietro Abate's avatar
Pietro Abate committed
61 62
    |Type (t,[||]) -> Format.fprintf ppf "type %s = %a" s Types.Print.pp_noname t
    |Type (t,al) ->
63 64 65
      Format.fprintf ppf "type %s(%a) = %a" s
        (Utils.pp_list ~delim:("","") Var.pp) (Array.to_list al)
        Types.Print.pp_noname t
66 67
    |_ -> ()
  in
68
  let t = [
Pietro Abate's avatar
Pietro Abate committed
69 70 71 72 73 74
    "Empty";"Any";"Int";"Char";"Byte";"Atom";
    "Pair";"Arrow";"Record";
    "String";"Latin1";
    "Bool";"Float";"AnyXml";
    "Namespaces";"Caml_int" ]
  in
75
  let ids =
Pietro Abate's avatar
Pietro Abate committed
76 77
    Env.filter (fun n _ ->
      not(List.mem (Id.to_string n) t)
78
    ) env.ids
Pietro Abate's avatar
Pietro Abate committed
79
  in
Pietro Abate's avatar
Pietro Abate committed
80
  Format.printf "{ids=%a;delta=%a}"
81 82
    (Ident.pp_env pp_item) ids
    Var.Set.pp env.delta
83 84
;;

85 86
(* Namespaces *)

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

101
let qname env loc t =
102
  protect_error_ns loc (Ns.map_tag env.ns) t
103

104 105 106 107
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)
108

109 110 111 112 113 114 115 116 117 118
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

119 120
let load_schema = ref (fun _ _ -> assert false)
let from_comp_unit = ref (fun _ -> assert false)
121
let load_comp_unit = ref (fun _ -> assert false)
122 123
let has_ocaml_unit = ref (fun _ -> false)
let has_static_external = ref (fun _ -> assert false)
124

125 126 127 128 129
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 }
130

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

138 139
let enter_id x i env =
  { env with ids = Env.add x i env.ids }
140

141 142
let type_using env loc x cu =
  try
143 144 145 146 147
    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))

Pietro Abate's avatar
Pietro Abate committed
148
let enter_type id t env = enter_id id (Type (t,[||])) env
149
let enter_types l env =
150
  { env with ids =
Pietro Abate's avatar
Pietro Abate committed
151 152 153 154
      List.fold_left (fun accu (id,t,al) ->
        Env.add id (Type (t,al)) accu
      ) env.ids l
  }
155

156 157 158 159 160 161
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
162
      error loc "Cannot resolve this identifier"
163 164 165

let find_id_comp env0 env loc x =
  if ((match (U.get_str x).[0] with 'A'..'Z' -> true | _ -> false)
166
      && !has_ocaml_unit x)
167 168 169
  then EOCaml (U.get_str x)
  else find_id env0 env loc true x

170

171
let enter_value id t env =
172
  { env with ids = Env.add id (Val t) env.ids }
173

174
let enter_values l env =
175
  { env with ids =
176
      List.fold_left (fun accu (id,t) -> Env.add id (Val t) accu) env.ids l;
177 178
  }

179
let enter_values_dummy l env =
180
  { env with ids =
181
      List.fold_left (fun accu id -> Env.add id (Val Types.empty) accu) env.ids l }
182

183 184
let value_name_ok id env =
  try match Env.find id env.ids with
185 186
  | Val _ | EVal _ -> true
  | _ -> false
187 188
  with Not_found -> true

189 190
let iter_values env f =
  Env.iter (fun x ->
191 192
    function Val t -> f x t;
    | _ -> ()) env.ids
193

194
let register_types cu env =
Pietro Abate's avatar
Pietro Abate committed
195
  Env.iter (fun x -> function
196 197
  | Type (t,_) -> Types.Print.register_global (cu,(Ident.value x),[||]) t
  | _ -> ()
Pietro Abate's avatar
Pietro Abate committed
198
  ) env.ids
199

200 201 202 203 204 205 206 207 208
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
209
  | Const c -> c
210 211 212
  | _ -> raise_loc_generic loc "This should be a scalar or structured constant"

(* I. Transform the abstract syntax of types and patterns into
213
   the internal form *)
214

215 216
let find_schema_component sch name =
  try ESchemaComponent (Env.find name sch.sch_comps)
217
  with Not_found ->
218
    raise (Error (Printf.sprintf "No component named '%s' found in schema '%s'"
219 220 221 222
		    (Ns.QName.to_string name) sch.sch_uri))

let navig loc env0 (env,comp) id =
  match comp with
223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245
  | 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)
  | 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"
246
(*
247
  | _ -> error loc "Invalid dot access"
248
*)
249

250 251
let rec find_global env loc ids =
  match ids with
252 253 254 255
  | id::rest ->
    let comp = find_id env env loc true id in
    snd (List.fold_left (navig loc env) (env,comp) rest)
  | _ -> assert false
256

257 258 259
let eval_ns env loc = function
  | `Uri ns -> ns
  | `Path ids ->
260 261 262 263
    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"
264 265 266 267

let type_ns env loc p ns =
  (* TODO: check that p has no prefix *)
  let ns = eval_ns env loc ns in
268
  { env with
269 270
    ns = Ns.add_prefix p ns env.ns;
    ids = Env.add (Ns.empty,p) (ENamespace ns) env.ids }
271

272 273
let find_global_type env loc ids =
  match find_global env loc ids with
274 275 276
  | Type (t,pargs) -> (t,pargs)
  | ESchemaComponent (t,_) -> (t,[||]) (* XXX *)
  | _ -> error loc "This path does not refer to a type"
277 278 279

let find_global_schema_component env loc ids =
  match find_global env loc ids with
280 281
  | ESchemaComponent c -> c
  | _ -> error loc "This path does not refer to a schema component"
282

283 284
let find_local_type env loc id =
  match Env.find id env.ids with
285 286
  | Type (t,pargs) -> (t,pargs)
  | _ -> raise Not_found
287 288

let find_value id env =
289
  match Env.find id env.ids with
290 291
  | Val t | EVal (_,_,t) -> t
  | _ -> raise Not_found
292

293 294
let do_open env cu =
  let env_cu = !from_comp_unit cu in
295
  let ids =
296 297
    Env.fold
      (fun n d ids ->
298 299 300 301
	let d = match d with
	  | Val t -> EVal (cu,n,t)
	  | d -> d in
	Env.add n d ids)
302 303
      env_cu.ids
      env.ids in
304
  { env with
305 306
    ids = ids;
    ns = Ns.merge_tables env.ns env_cu.ns }
307

308 309 310

let type_open env loc ids =
  match find_global env loc ids with
311 312
  | ECDuce cu -> do_open env cu
  | _ -> error loc "This path does not refer to a CDuce unit"
313

314
module IType = struct
315
  open Typepat
316

317
  (* From AST to the intermediate representation *)
318 319 320 321

  type penv = {
    penv_tenv : t;
    penv_derec : node Env.t;
322
    penv_var : (string, Var.var) Hashtbl.t;
323 324
  }

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

327 328
  let all_delayed = ref []

329 330
  let clean_on_err () = all_delayed := []

331 332 333 334 335 336
  let delayed loc =
    let s = mk_delayed () in
    all_delayed := (loc,s) :: !all_delayed;
    s

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

339 340
  let check_delayed () =
    let l = !all_delayed in
341
    all_delayed := [];
342
    List.iter check_one_delayed l
343

Pietro Abate's avatar
Pietro Abate committed
344
  (* Ast -> symbolic type *)
345
  let rec derecurs env p =
Pietro Abate's avatar
Pietro Abate committed
346
    match p.descr with
347
    | PatVar ids -> derecurs_var env p.loc ids
348
    | Recurs (p,b) -> derecurs (fst (derecurs_def env b)) p
349
    | Internal t -> mk_type t
350
    | NsT ns ->
351
      mk_type (Types.atom (Atoms.any_in_ns (parse_ns env.penv_tenv p.loc ns)))
352 353 354 355 356 357 358
    | 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)
359
    | Record (o,r) ->
360 361 362 363
      let aux = function
	| (p,Some e) -> (derecurs env p, Some (derecurs env e))
	| (p,None) -> derecurs env p, None in
      mk_record o (parse_record env.penv_tenv p.loc aux r)
364
    | Constant (x,c) ->
365
      mk_constant (ident env.penv_tenv p.loc x) (const env.penv_tenv p.loc c)
366
    | Cst c -> mk_type (Types.constant (const env.penv_tenv p.loc c))
367 368 369
    | 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)
370

371
  and derecurs_regexp env = function
372
    | Epsilon -> mk_epsilon
373 374 375 376 377 378
    | 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)
Pietro Abate's avatar
Pietro Abate committed
379
    | SeqCapture ((loc,x),p) -> mk_seqcapt (ident env.penv_tenv loc x) (derecurs_regexp env p)
380

381 382
  and derecurs_var env loc ids =
    match ids with
383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408
    | ([v],a) ->
      let v = ident env.penv_tenv loc v in
      begin
        try Env.find v env.penv_derec
	with Not_found ->
	  try
            let (t,pargs) = find_local_type env.penv_tenv loc v in
            let palen = Array.length pargs in
            if palen <> List.length a then
              raise_loc_generic loc
                (Printf.sprintf "Parametric type %s is not fully instanciated" (Ident.to_string v));
            let a = Array.of_list a in
            let l = ref [] in
            for i=0 to (Array.length pargs) - 1 do
              try
                let err s = Error s in
                let tai = typ ~err (derecurs env a.(i)) in
                l := (pargs.(i), tai )::!l
              with
              |Error s -> raise_loc_generic loc s
              |_ -> assert false
            done;
            mk_type (Types.Positive.substitute_list t !l)
	  with Not_found ->
            if List.length a >= 1 then
              raise_loc_generic loc
409
                (Printf.sprintf "Parametric type %s does not exists" (Ident.to_string v))
410 411 412 413 414
            else
              mk_capture v
      end
    | (ids,_) ->
      mk_type (fst(find_global_type env.penv_tenv loc ids))
415

416
  and derecurs_def env b =
417
    let seen = ref IdSet.empty in
418
    let b =
Pietro Abate's avatar
Pietro Abate committed
419
      List.map (fun ((loc,v),_,p) ->
420 421 422 423 424 425 426 427
	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
Pietro Abate's avatar
Pietro Abate committed
428
    in
429
    let n = List.fold_left (fun env (v,p,s) -> Env.add v s env) env.penv_derec b in
430
    let env = { env with penv_derec = n } in
431
    List.iter (fun (v,p,s) -> link s (derecurs env p)) b;
432 433
    (env, b)

434 435
  let derec penv p =
    let d = derecurs penv p in
436
    elim_concats ();
437
    check_delayed ();
438
    internalize d;
439
    d
440

441
  (* API *)
442

443 444
  let check_no_fv loc n =
    match peek_fv n with
445 446 447 448
    | None -> ()
    | Some x ->
      raise_loc_generic loc
	("Capture variable not allowed: " ^ (Ident.to_string x))
449

450
  let type_defs env b =
451
    let _,b' = derecurs_def (penv env) b in
452 453 454 455 456
    elim_concats ();
    check_delayed ();
    let aux loc d =
      internalize d;
      check_no_fv loc d;
457
      try typ d
458
      with Patterns.Error s -> raise_loc_generic loc s
459
    in
460
    let b =
Pietro Abate's avatar
Pietro Abate committed
461
      List.map2 (fun ((loc,v),pl,p) (v',_,d) ->
462 463 464

        let t_rhs = aux loc d in
        if (loc <> noloc) && (Types.is_empty t_rhs) then
465 466
          warning loc
            ("This definition yields an empty type for " ^ (U.to_string v));
467 468 469 470 471 472 473 474 475

        let vars_rhs = Types.all_vars t_rhs in
        let vars_mapping = (* create a sequence 'a -> 'a_0 for all variables *)
          List.map (fun v -> let vv =  Var.mk (Ident.U.to_string v) in vv, Var.fresh vv) pl
        in
        let vars_lhs =
          List.fold_left (fun acc (v, _) -> Var.Set.add v acc) Var.Set.empty vars_mapping
        in
        if not (Var.Set.subset vars_rhs vars_lhs) then
476
          error loc
477 478 479 480 481 482 483
            (Printf.sprintf "Definition of type %s contains unbound type variables"
               (U.to_string v));

        let t_rhs =
          Types.Positive.substitute_list t_rhs
            (List.map (fun (v,vt) -> v, Types.var vt) vars_mapping)
        in
Pietro Abate's avatar
Pietro Abate committed
484
        let al =
485
          let a = Array.make (List.length pl) (Var.mk "dummy") in
486
          List.iteri (fun i (_,v) -> a.(i) <- v) vars_mapping;
Pietro Abate's avatar
Pietro Abate committed
487
          a
488
        in
489
        (v',t_rhs,al)
490
      ) (List.rev b) (List.rev b')
Pietro Abate's avatar
Pietro Abate committed
491
    in
492 493 494
    List.iter (fun (v,t,al) ->
      Types.Print.register_global ("",v,Array.map Types.var al) t
    ) b;
495
    enter_types b env
496

497 498 499 500
  let type_defs env b =
    try type_defs env b
    with exn -> clean_on_err (); raise exn

501
  let typ env t =
502
    try
503
      let d = derec (penv env) t in
504 505 506 507
      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
508

509
  let pat env t =
510 511 512 513 514
    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
515

516
end
517 518 519 520 521 522

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

let dump_types ppf env =
523
  Env.iter (fun v ->
524 525 526
    function
  (Type _) -> Format.fprintf ppf " %a" Ident.print v
    | _ -> ()) env.ids
527 528 529 530 531 532

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



533

534 535
(* II. Build skeleton *)

536

537
type type_fun = Types.t -> bool -> Types.t
538

539
module Fv = IdSet
540

541 542 543
type branch = Branch of Typed.branch * branch list

let cur_branch : branch list ref = ref []
544

545
let exp' loc e =
Pietro Abate's avatar
Pietro Abate committed
546 547 548 549
  { Typed.exp_loc = loc;
    Typed.exp_typ = Types.empty;
    Typed.exp_descr = e
  }
550 551 552 553 554

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

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

555
let pat_true =
556 557 558 559
  let n = Patterns.make Fv.empty in
  Patterns.define n (Patterns.constr Builtin_defs.true_type);
  n

560
let pat_false =
561 562 563 564
  let n = Patterns.make Fv.empty in
  Patterns.define n (Patterns.constr Builtin_defs.false_type);
  n

565
let ops = Hashtbl.create 13
566 567
let register_op op arity f = Hashtbl.add ops op (arity,f)
let typ_op op = snd (Hashtbl.find ops op)
568

569 570
let fun_name env a =
  match a.fun_name with
571 572
  | None -> None
  | Some (loc,s) -> Some (ident env loc s)
573

574 575
let count_arg_name = ref 0
let fresh_arg_name () =
576 577
  incr count_arg_name;
  "__abstr_arg" ^ (string_of_int !count_arg_name)
578

579
let is_op env s =
580 581
  if (Env.mem s env.ids) then None
  else
582 583
    let (ns,s) = s in
    if Ns.Uri.equal ns Ns.empty then
584
      let s = U.get_str s in
585
      try
586 587 588 589
	let o = Hashtbl.find ops s in
	Some (s, fst o)
      with Not_found -> None
    else None
590

591 592
let rec expr env loc = function
  | LocatedExpr (loc,e) -> expr env loc e
593
  | Forget (e,t) ->
594 595
    let (fv,e) = expr env loc e and t = typ env t in
    exp loc fv (Typed.Forget (e,t))
596
  | Check (e,t) ->
597 598
    let (fv,e) = expr env loc e and t = typ env t in
    exp loc fv (Typed.Check (ref Types.empty,e,t))
599
  | Var s -> var env loc s
600
  | Apply (e1,e2) ->
601 602 603 604 605 606 607
    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)))
608
  | Abstraction a -> abstraction env loc a
609
  | (Integer _ | Char _ | Atom _ | Const _ ) as c ->
610
    exp loc Fv.empty (Typed.Cst (const env loc c))
611
  | Pair (e1,e2) ->
612 613
    let (fv1,e1) = expr env loc e1 and (fv2,e2) = expr env loc e2 in
    exp loc (Fv.cup fv1 fv2) (Typed.Pair (e1,e2))
614
  | Xml (e1,e2) ->
615 616 617
    let (fv1,e1) = expr env loc e1 and (fv2,e2) = expr env loc e2 in
    let n = if env.keep_ns then Some env.ns else None in
    exp loc (Fv.cup fv1 fv2) (Typed.Xml (e1,e2,n))
618
  | Dot _ as e ->
619
    dot loc env e []
620
  | TyArgs (Dot _ as e, args) ->
621
    dot loc env e args
622
  | TyArgs _ ->
623
    error loc "Only OCaml external can have type arguments"
624
  | RemoveField (e,l) ->
625 626
    let (fv,e) = expr env loc e in
    exp loc fv (Typed.RemoveField (e,parse_label env loc l))
627
  | RecordLitt r ->
628 629 630 631 632 633 634
    let fv = ref Fv.empty in
    let r = parse_record env loc
      (fun e ->
	let (fv2,e) = expr env loc e
	in fv := Fv.cup !fv fv2; e)
      r in
    exp loc !fv (Typed.RecordLitt r)
635
  | String (i,j,s,e) ->
636 637
    let (fv,e) = expr env loc e in
    exp loc fv (Typed.String (i,j,s,e))
638
  | Match (e,b) ->
639 640 641
    let (fv1,e) = expr env loc e
    and (fv2,b) = branches env b in
    exp loc (Fv.cup fv1 fv2) (Typed.Match (e, b))
642
  | Map (e,b) ->
643 644 645
    let (fv1,e) = expr env loc e
    and (fv2,b) = branches env b in
    exp loc (Fv.cup fv1 fv2) (Typed.Map (e, b))
646
  | Transform (e,b) ->
647 648 649
    let (fv1,e) = expr env loc e
    and (fv2,b) = branches env b in
    exp loc (Fv.cup fv1 fv2) (Typed.Transform (e, b))
650
  | Xtrans (e,b) ->
651 652 653
    let (fv1,e) = expr env loc e
    and (fv2,b) = branches env b in
    exp loc (Fv.cup fv1 fv2) (Typed.Xtrans (e, b))
654
  | Validate (e,ids) ->
655 656 657
    let (fv,e) = expr env loc e in
    let (t,v) = find_global_schema_component env loc ids  in
    exp loc fv (Typed.Validate (e, t, v))
658
  | SelectFW (e,from,where) ->
659
    select_from_where env loc e from where
660
  | Try (e,b) ->
661 662 663
    let (fv1,e) = expr env loc e
    and (fv2,b) = branches env b in
    exp loc (Fv.cup fv1 fv2) (Typed.Try (e, b))
664
  | NamespaceIn (pr,ns,e) ->
665 666
    let env = type_ns env loc pr ns in
    expr env loc e
667
  | KeepNsIn (k,e) ->
668
    expr (type_keep_ns env k) loc e
669
  | Ref (e,t) ->
670 671
    let (fv,e) = expr env loc e and t = typ env t in
    exp loc fv (Typed.Ref (e,t))
672 673 674 675 676 677 678

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;
679
	Typed.br_ghost = false;
680
	Typed.br_vars_empty = Fv.empty;
681
	Typed.br_vars_poly = IdMap.empty;
682 683 684 685
	Typed.br_pat = pat_true;
	Typed.br_body = yes };
      { Typed.br_loc = no.Typed.exp_loc;
	Typed.br_used = false;
686
	Typed.br_ghost = false;
687
	Typed.br_vars_empty = Fv.empty;
688
	Typed.br_vars_poly = IdMap.empty;
689 690 691 692 693
	Typed.br_pat = pat_false;
	Typed.br_body = no } ];
    Typed.br_accept = Builtin_defs.bool;
  } in
  exp' loc (Typed.Match (cond,b))
694 695


696
and dot loc env0 e args =
697
  let dot_access loc (fv,e) l =
698 699 700 701 702 703 704 705
    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) ->
706 707 708
      (match aux loc e with
      | `Val e -> `Val (dot_access loc e id)
      | `Comp c -> `Comp (navig loc env0 c id))
709
    | Var id ->
710 711 712
      (match find_id_comp env0 env0 loc id with
      | Val _ -> `Val (var env0 loc id)
      | c -> `Comp (env0,c))
713 714 715
    | e -> `Val (expr env0 loc e)
  in
  match aux loc e with
716 717 718 719 720
  | `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"
721 722

and extern loc env s args =
723 724
  let args = List.map (typ env) args in
  try
725 726 727 728 729 730
    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
731 732
    exp loc Fv.empty (Typed.External (t,i))
  with exn -> raise_loc loc exn
733

734
and var env loc s =
735 736
  let id = ident env loc s in
  match is_op env id with
737 738 739 740 741 742 743 744 745 746 747 748 749 750 751
  | Some (s,arity) ->
    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
    exp loc Fv.empty e
  | None ->
    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"
752

753
and abstraction env loc a =
754 755
  let iface =
    List.map
756 757
      (fun (t1,t2) -> (typ env t1, typ env t2)) a.fun_iface
  in
758 759 760
  let t =
    List.fold_left
      (fun accu (t1,t2) -> Types.cap accu (Types.arrow t1 t2))
761
      Types.any iface in
762 763 764
  let iface =
    List.map
      (fun (t1,t2) -> (Types.descr t1, Types.descr t2))
765
      iface in
766
  let fun_name = fun_name env a in
767 768
  let env' =
    match fun_name with
769 770
    | None -> env
    | Some f -> enter_values_dummy [ f ] env
771 772
  in
  let (fv0,body) = branches env' a.fun_body in
773
  let fv = match fun_name with
774 7