typer.ml 33.9 KB
Newer Older
1 2 3
open Location
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 = Location.get_viewport () in
13
  let ppf = if Html.is_html v then Html.ppf v else Format.err_formatter in
14 15 16
  Format.fprintf ppf "Warning %a:@\n" Location.print_loc (loc,`Full);
  Location.html_hilight (loc,`Full);
  Format.fprintf ppf "%s@." msg
17

18 19 20 21 22 23 24 25
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
exception UnboundExtId of Types.CompUnit.t * id
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
type item =
  | Type of Types.t
34
  | Val of Types.t
35

36 37 38 39 40
type ext =
  | ECDuce of Types.CompUnit.t   (* CDuce unit *)
  | EOCaml of string             (* OCaml module *)
  | ESchema of string            (* XML Schema *)

41 42
module UEnv = Map.Make(U)

43
type t = {
44
  ids : item Env.t;
45
  ns: Ns.table;
46
  cu: ext UEnv.t;
47
  keep_ns: bool
48
}
49

50 51 52 53 54
let load_schema = ref (fun _ _ -> assert false)
let from_comp_unit = ref (fun _ -> assert false)
let has_comp_unit = ref (fun _ -> assert false)
let has_ocaml_unit = ref (fun _ -> false)
let has_static_external = ref (fun _ -> assert false)
55

56
let schemas = Hashtbl.create 13
57

58
let type_schema env x uri =
59 60
  if not (Hashtbl.mem schemas uri) then
    Hashtbl.add schemas uri (!load_schema x uri);
61
  { env with cu = UEnv.add x (ESchema uri) env.cu }
62

63
(* TODO: filter out builtin defs ? *)
64 65 66 67
let serialize_item s = function
  | Type t -> Serialize.Put.bits 1 s 0; Types.serialize s t
  | Val t -> Serialize.Put.bits 1 s 1; Types.serialize s t

68
let serialize s env =
69
  Serialize.Put.env Id.serialize serialize_item Env.iter s env.ids;
70 71 72
  Ns.serialize_table s env.ns;

  let schs =
73 74 75
    UEnv.fold 
      (fun name cu accu -> 
	 match cu with ESchema uri -> (name,uri)::accu | _ -> accu) 
76
      env.cu [] in
77 78
  Serialize.Put.list 
    (Serialize.Put.pair U.serialize Serialize.Put.string) s schs
79

80 81 82 83 84
let deserialize_item s = match Serialize.Get.bits 1 s with
  | 0 -> Type (Types.deserialize s)
  | 1 -> Val (Types.deserialize s)
  | _ -> assert false

85
let deserialize s =
86 87
  let ids = 
    Serialize.Get.env Id.deserialize deserialize_item Env.add Env.empty s in
88
  let ns = Ns.deserialize_table s in
89 90 91 92
  let schs = 
    Serialize.Get.list 
      (Serialize.Get.pair U.deserialize Serialize.Get.string) s in
  let env = 
93
    { ids = ids; ns = ns; cu = UEnv.empty; keep_ns = false } in
94
  List.fold_left (fun env (name,uri) -> type_schema env name uri) env schs
95 96


97 98
let empty_env = {
  ids = Env.empty;
99
  ns = Ns.def_table;
100
  cu = UEnv.empty;
101
  keep_ns = false
102 103
}

104
let enter_cu x cu env =
105
  { env with cu = UEnv.add x (ECDuce cu) env.cu }
106

107
let find_cu loc x env =
108
  try UEnv.find x env.cu
109 110 111 112
  with Not_found ->
    if !has_comp_unit x then (ECDuce (Types.CompUnit.mk x))
    else if !has_ocaml_unit x then (EOCaml (U.get_str x))
    else error loc ("Cannot find external unit " ^ (U.to_string x))
113 114


115
let find_schema x env =
116 117 118 119 120 121
  try 
    (match UEnv.find x env.cu with
      | ESchema s -> s 
      | _ -> raise Not_found)
  with Not_found -> 
    raise (Error (Printf.sprintf "%s: no such schema" (U.to_string x)))
122

123 124 125 126 127 128 129 130
let enter_type id t env =
  { env with ids = Env.add id (Type t) env.ids }
let enter_types l env =
  { env with ids = 
      List.fold_left (fun accu (id,t) -> Env.add id (Type t) accu) env.ids l }
let find_type id env =
  match Env.find id env.ids with
    | Type t -> t
131
    | Val _ -> raise Not_found
132

133

134
let enter_value id t env = 
135
  { env with ids = Env.add id (Val t) env.ids }
136 137
let enter_values l env =
  { env with ids = 
138
      List.fold_left (fun accu (id,t) -> Env.add id (Val t) accu) env.ids l }
139 140 141
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 }
142 143
let find_value id env =
  match Env.find id env.ids with
144
    | Val t -> t
145
    | _ -> raise Not_found
146 147 148
let find_value_global loc cu id env =
  try find_value id (!from_comp_unit cu)
  with Not_found -> raise_loc loc (UnboundExtId (cu,id))
149
	
150 151 152 153 154 155
let value_name_ok id env =
  try match Env.find id env.ids with
    | Val t -> true
    | _ -> false
  with Not_found -> true

156 157 158 159
let iter_values env f =
  Env.iter (fun x ->
	      function Val t -> f x t;
		| _ -> ()) env.ids
160

161

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

167

168
(* Namespaces *)
169

170
let set_ns_table_for_printer env = 
171
  Ns.InternalPrinter.set_table env.ns
172

173
let get_ns_table tenv = tenv.ns
174

175
let type_ns env p ns =
176
  { env with ns = Ns.add_prefix p ns env.ns }
177

178 179 180
let type_keep_ns env k =
  { env with keep_ns = k }

181 182 183 184 185
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))
186

187 188 189
let qname env loc t = 
  protect_error_ns loc (Ns.map_tag env.ns) t
    
190 191 192 193 194 195 196 197 198 199
let ident env loc t =
  let q = protect_error_ns loc (Ns.map_attr env.ns) t in
  Ident.ident q

let has_value id env =
  try match Env.find (Ident.ident (Ns.map_attr env.ns id)) env.ids with
    | Val t -> true
    | _ -> false
  with Not_found | Ns.UnknownPrefix _ -> false

200
let parse_atom env loc t =
201
  Atoms.V.of_qname (qname env loc t)
202 203
 
let parse_ns env loc ns =
204
  protect_error_ns loc (Ns.map_prefix env.ns) ns
205

206
let parse_label env loc t =
207
  let (ns,l) = protect_error_ns loc (Ns.map_attr env.ns) t in
208
  LabelPool.mk (ns,l)
209

210 211 212 213 214 215 216 217 218 219 220 221 222
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

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
223
  | Const c -> c
224 225 226 227
  | _ -> 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 *)
228

229

230 231 232 233
let get_schema_names env = 
  UEnv.fold 
    (fun n cu acc -> match cu with ESchema _ -> n :: acc | _ -> acc) env.cu []
    
234 235
let find_schema_component uri name =
  Env.find (Ident.ident name) (Hashtbl.find schemas uri)
236

237 238 239
let get_schema_validator uri name =
  snd (find_schema_component uri name)

240
let find_schema_descr uri (name : Ns.qname) =
241
  try fst (find_schema_component uri name)
242 243 244
  with Not_found ->    
    raise (Error (Printf.sprintf "No component named '%s' found in schema '%s'"
		    (Ns.QName.to_string name) uri))
245 246


247 248 249 250 251 252
let find_type_global loc cu id env =
  match find_cu loc cu env with
    | ECDuce cu -> find_type id (!from_comp_unit cu)
    | EOCaml _ -> error loc "OCaml units don't export types" (* TODO *)
    | ESchema s -> find_schema_descr s (Ident.value id)
	
253

254
module IType = struct
255
  open Typepat
256 257 258 259 260 261 262 263 264 265

(* From AST to the intermediate representation *)

  type penv = {
    penv_tenv : t;
    penv_derec : node Env.t;
  }

  let penv tenv = { penv_tenv = tenv; penv_derec = Env.empty }

266 267
  let all_delayed = ref []

268 269
  let clean_on_err () = all_delayed := []

270 271 272 273 274 275
  let delayed loc =
    let s = mk_delayed () in
    all_delayed := (loc,s) :: !all_delayed;
    s

  let check_one_delayed (loc,p) =
276
    if not (check_wf p) then error loc "Ill-formed recursion"
277 278 279 280 281
    
  let check_delayed () =
    let l = !all_delayed in
    all_delayed := []; 
    List.iter check_one_delayed l
282

283
  let rec derecurs env p = match p.descr with
284
    | PatVar (cu,v) -> derecurs_var env p.loc cu v
285
    | Recurs (p,b) -> derecurs (fst (derecurs_def env b)) p
286
    | Internal t -> mk_type t
287
    | NsT ns -> 
288 289 290 291 292 293 294 295
	mk_type (Types.atom (Atoms.any_in_ns (parse_ns env.penv_tenv p.loc ns)))
    | 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)
296 297 298 299
    | Record (o,r) -> 
	let aux = function
	  | (p,Some e) -> (derecurs env p, Some (derecurs env e))
	  | (p,None) -> derecurs env p, None in
300 301 302 303 304 305 306
	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))
    | 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)
307
	  
308 309 310 311 312 313 314 315 316
  and derecurs_regexp env = function
    | Epsilon -> mk_epsilon
    | 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)
317
	  
318 319 320 321 322
  and derecurs_var env loc cu v =
    let v = ident env.penv_tenv loc v in
    match cu with
      | None ->
	  (try Env.find v env.penv_derec 
323
	   with Not_found -> 
324 325
	     try mk_type (find_type v env.penv_tenv)
	     with Not_found -> mk_capture v)
326
      | Some cu ->
327
	  (try mk_type (find_type_global loc cu v env.penv_tenv)
328 329 330 331
	   with Not_found ->
	     raise_loc_generic loc 
	       ("Unbound external type " ^ (U.get_str cu) ^ "." ^ 
		  (Ident.to_string v)))
332 333
	      
  and derecurs_def env b =
334 335 336 337 338 339 340 341 342 343 344 345 346
    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

347 348 349
    let n = 
      List.fold_left (fun env (v,p,s) -> Env.add v s env) env.penv_derec b in
    let env = { env with penv_derec = n } in
350
    List.iter (fun (v,p,s) -> link s (derecurs env p)) b;
351 352
    (env, b)

353 354
  let derec penv p =
    let d = derecurs penv p in
355
    elim_concats ();
356 357 358
    check_delayed ();
    internalize d;
    d
359 360


361
(* API *)
362

363 364 365 366 367 368 369
  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))

370
  let type_defs env b =
371 372 373 374 375 376
    let _,b' = derecurs_def (penv env) b in
    elim_concats ();
    check_delayed ();
    let aux loc d =
      internalize d;
      check_no_fv loc d;
377
      try typ d
378
      with Patterns.Error s -> raise_loc_generic loc s
379
    in
380
    let b = 
381 382 383
      List.map2 
	(fun (loc,v,p) (v',_,d) ->
	   let t = aux loc d in
384 385 386 387
	   if (loc <> noloc) && (Types.is_empty t) then
	     warning loc 
	       ("This definition yields an empty type for " ^ (U.to_string v));
	   let v = ident env loc v in
388
	   (v',t)) b b' in
389 390
    List.iter (fun (v,t) -> Types.Print.register_global 
		 (Types.CompUnit.get_current ()) (Id.value v) t) b;
391
    enter_types b env
392

393 394 395 396
  let type_defs env b =
    try type_defs env b
    with exn -> clean_on_err (); raise exn

397
  let typ env t = 
398 399 400 401 402 403
    try
      let d = derec (penv env) t in
      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
404 405

  let pat env t = 
406 407 408 409 410
    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
411

412
end
413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428

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



429

430 431
(* II. Build skeleton *)

432

433
type type_fun = Types.t -> bool -> Types.t
434

435
module Fv = IdSet
436

437 438 439
type branch = Branch of Typed.branch * branch list

let cur_branch : branch list ref = ref []
440

441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457
let exp' loc e = 
  { Typed.exp_loc = loc; Typed.exp_typ = Types.empty; Typed.exp_descr = e; }

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

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

let pat_true = 
  let n = Patterns.make Fv.empty in
  Patterns.define n (Patterns.constr Builtin_defs.true_type);
  n

let pat_false =   
  let n = Patterns.make Fv.empty in
  Patterns.define n (Patterns.constr Builtin_defs.false_type);
  n

458

459
let ops = Hashtbl.create 13
460 461
let register_op op arity f = Hashtbl.add ops op (arity,f)
let typ_op op = snd (Hashtbl.find ops op)
462

463 464 465 466 467
let fun_name env a =
  match a.fun_name with
    | None -> None
    | Some (loc,s) -> Some (ident env loc s)

468
let is_op env s = 
469 470 471 472 473 474 475 476 477 478
  if (Env.mem s env.ids) then None
  else
    let (ns,s) = Id.value s in
    if Ns.equal ns Ns.empty then
      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
479

480 481
let rec expr env loc = function
  | LocatedExpr (loc,e) -> expr env loc e
482
  | Forget (e,t) ->
483
      let (fv,e) = expr env loc e and t = typ env t in
484
      exp loc fv (Typed.Forget (e,t))
485 486
  | Check (e,t) ->
      let (fv,e) = expr env loc e and t = typ env t in
487
      exp loc fv (Typed.Check (ref Types.empty,e,t))
488
  | Var s -> var env loc s
489
  | Apply (e1,e2) -> 
490 491 492 493 494 495 496 497
      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
498
  | (Integer _ | Char _ | Atom _ | Const _) as c -> 
499
      exp loc Fv.empty (Typed.Cst (const env loc c))
500
  | Pair (e1,e2) ->
501
      let (fv1,e1) = expr env loc e1 and (fv2,e2) = expr env loc e2 in
502 503
      exp loc (Fv.cup fv1 fv2) (Typed.Pair (e1,e2))
  | Xml (e1,e2) ->
504
      let (fv1,e1) = expr env loc e1 and (fv2,e2) = expr env loc e2 in
505 506
      let n = if env.keep_ns then Some env.ns else None in
      exp loc (Fv.cup fv1 fv2) (Typed.Xml (e1,e2,n))
507
  | Dot (LocatedExpr (_,Var cu), id, tyargs) when not (has_value cu env) ->
508 509
      (match find_cu loc cu env with
	 | ECDuce cu ->
510 511
	     if tyargs != [] then
	       error loc "CDuce externals cannot have type argument";
512 513 514 515
	     let id = ident env loc id in
	     let t = find_value_global loc cu id env in
	     exp loc Fv.empty (Typed.ExtVar (cu, id, t))
	 | EOCaml cu ->
516
	     extern loc env (cu ^ "." ^ U.get_str id) tyargs
517 518 519
	       (* TODO: allow nested OCaml modules A.B.C.x *)
	 | ESchema _ ->
	     error loc "Schema don't export values")
520
  | Dot (e,l,[]) ->
521 522
      let (fv,e) = expr env loc e in
      exp loc fv (Typed.Dot (e,parse_label env loc l))
523 524
  | Dot (_,_,_::_) ->
      error loc "Field access cannot have type arguments"
525
  | RemoveField (e,l) ->
526 527
      let (fv,e) = expr env loc e in
      exp loc fv (Typed.RemoveField (e,parse_label env loc l))
528 529
  | RecordLitt r -> 
      let fv = ref Fv.empty in
530
      let r = parse_record env loc
531
		(fun e -> 
532
		   let (fv2,e) = expr env loc e 
533 534 535
		   in fv := Fv.cup !fv fv2; e)
		r in
      exp loc !fv (Typed.RecordLitt r)
536
  | String (i,j,s,e) ->
537
      let (fv,e) = expr env loc e in
538
      exp loc fv (Typed.String (i,j,s,e))
539
  | Match (e,b) -> 
540 541
      let (fv1,e) = expr env loc e
      and (fv2,b) = branches env b in
542
      exp loc (Fv.cup fv1 fv2) (Typed.Match (e, b))
543
  | Map (e,b) ->
544 545
      let (fv1,e) = expr env loc e
      and (fv2,b) = branches env b in
546 547
      exp loc (Fv.cup fv1 fv2) (Typed.Map (e, b))
  | Transform (e,b) ->
548 549
      let (fv1,e) = expr env loc e
      and (fv2,b) = branches env b in
550
      exp loc (Fv.cup fv1 fv2) (Typed.Transform (e, b))
551
  | Xtrans (e,b) ->
552 553
      let (fv1,e) = expr env loc e
      and (fv2,b) = branches env b in
554
      exp loc (Fv.cup fv1 fv2) (Typed.Xtrans (e, b))
555
  | Validate (e,schema,elt) ->
556
      let (fv,e) = expr env loc e in
557
      let uri = find_schema schema env in
558
      exp loc fv (Typed.Validate (e, uri, qname env loc elt))
559 560
  | SelectFW (e,from,where) ->
      select_from_where env loc e from where
561
  | Try (e,b) ->
562 563
      let (fv1,e) = expr env loc e
      and (fv2,b) = branches env b in
564
      exp loc (Fv.cup fv1 fv2) (Typed.Try (e, b))
565
  | NamespaceIn (pr,ns,e) ->
566
      let env = type_ns env pr ns in
567
      expr env loc e
568 569
  | KeepNsIn (k,e) ->
      expr (type_keep_ns env k) loc e
570
  | Ref (e,t) ->
571
      let (fv,e) = expr env loc e and t = typ env t in
572
      exp loc fv (Typed.Ref (e,t))
573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590

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;
	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;
	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))
591 592 593 594
	
and extern loc env s args = 
  let args = List.map (typ env) args in
  try
595 596 597 598 599 600
    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
601 602 603 604
    exp loc Fv.empty (Typed.External (t,i))
  with exn -> raise_loc loc exn
    
and var env loc s =
605 606
  let id = ident env loc s in
  match is_op env id with
607
    | Some (s,arity) -> 
608 609 610 611 612 613 614
	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
615
	exp loc Fv.empty e
616
    | None ->
617 618 619
	(try ignore (find_value id env)
	 with Not_found -> raise_loc loc (UnboundId (id, Env.mem id env.ids)));
	exp loc (Fv.singleton id) (Typed.Var id)
620 621 622 623 624 625 626 627 628 629 630 631 632

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
633
  let fun_name = fun_name env a in
634
  let env' = 
635
    match fun_name with 
636 637 638 639
      | None -> env
      | Some f -> enter_values_dummy [ f ] env
  in
  let (fv0,body) = branches env' a.fun_body in
640
  let fv = match fun_name with
641 642 643
    | None -> fv0
    | Some f -> Fv.remove f fv0 in
  let e = Typed.Abstraction 
644
	    { Typed.fun_name = fun_name;
645 646 647 648 649 650 651 652 653 654 655 656 657
	      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 := [];
658 659 660 661 662
    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
663 664 665
    (match Fv.pick (Fv.diff fvp fv2) with
       | None -> ()
       | Some x ->
666
	   let x = Ident.to_string x in
667 668 669 670 671
	   warning br_loc 
	     ("The capture variable " ^ x ^ 
	      " is declared in the pattern but not used in the body of this branch. It might be a misspelled or undeclared type or name (if it isn't, use _ instead)."));
    let fv2 = Fv.diff fv2 fvp in
    fv := Fv.cup !fv fv2;
672
    accept := Types.cup !accept (Types.descr (Patterns.accept p));
673 674 675
    let br = 
      { 
	Typed.br_loc = br_loc;
676
	Typed.br_used = br_loc == noloc;
677 678
	Typed.br_vars_empty = fvp;
	Typed.br_pat = p;
679 680 681 682 683 684 685 686 687 688 689
	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;
   } 
  )
690

691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715
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 -> ... *)
716
    let br = { Typed.br_loc = ploc;
717 718 719
	  Typed.br_used = false;
	  Typed.br_vars_empty = fvp;
	  Typed.br_pat = p;
720 721 722 723 724
	  Typed.br_body = rest } in
    cur_branch := [ Branch (br, !cur_branch) ];
    let b = {
      Typed.br_typ = Types.empty;
      Typed.br_branches = [ br ];
725 726 727 728 729
      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
730 731
  let cur_br = !cur_branch in
  cur_branch := [];
732
  let (fv,e) = expr !env noloc (Pair(e,cst_nil)) in
733
  cur_branch := !cur_branch @ cur_br;
734 735 736 737 738 739 740 741 742 743
  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

744
let expr env e = snd (expr env noloc e)
745

746 747
let let_decl env p e =
  { Typed.let_pat = pat env p;
748
    Typed.let_body = expr env e }
749

750 751 752

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

753

754 755
(* III. Type-checks *)

756 757
open Typed

758 759 760 761 762 763
let localize loc f x =
  try f x
  with 
    | (Error _ | Constraint (_,_)) as exn -> raise (Location.Location (loc,`Full,exn))
    | Warning (s,t) -> warning loc s; t

764 765
let require loc t s = 
  if not (Types.subtype t s) then raise_loc loc (Constraint (t, s))
766

767
let verify loc t s = 
768 769
  require loc t s; t

770 771 772 773
let verify_noloc t s =
  if not (Types.subtype t s) then raise (Constraint (t, s));
  t

774 775 776 777 778
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 = 
779 780
  raise_loc loc (ShouldHave (constr,s))

781 782 783
let should_have_str loc ofs constr s = 
  raise_loc_str loc ofs (ShouldHave (constr,s))

784
let flatten arg constr precise =
785 786 787 788 789 790 791 792 793
  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
794
    verify_noloc (Sequence.flatten t) constr
795

796 797
let rec type_check env e constr precise = 
  let d = type_check' e.exp_loc env e.exp_descr constr precise in
798
  let d = if precise then d else constr in
799 800 801
  e.exp_typ <- Types.cup e.exp_typ d;
  d

802
and type_check' loc env e constr precise = match e with
803 804 805
  | Forget (e,t) ->
      let t = Types.descr t in
      ignore (type_check env e t false);
806
      verify loc t constr
807

808 809 810
  | Check (t0,e,t) ->
      let te = type_check env e Types.any true in
      t0 := Types.cup !t0 te;
811
      verify loc (Types.cap te (Types.descr t)) constr
812

813
  | Abstraction a ->
814 815 816
      let t =
	try Types.Arrow.check_strenghten a.fun_typ constr 
	with Not_found -> 
817 818
	  should_have loc constr
	    "but the interface of the abstraction is not compatible"
819
      in
820 821
      let env = match a.fun_name with
	| None -> env
822
	| Some f -> enter_value f a.fun_typ env in
823 824
      List.iter 
	(fun (t1,t2) ->
825 826 827
	   let acc = a.fun_body.br_accept in 
	   if not (Types.subtype t1 acc) then
	     raise_loc loc (NonExhaustive (Types.diff t1 acc));
828
	   ignore (type_check_branches loc env t1 a.fun_body t2 false)
Pietro Abate's avatar