typer.ml 48.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 12 13 14 15 16
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
17
exception UnboundExtId of Compunit.t * id
18
exception Error of string
19 20
exception Warning of string * Types.t

21 22 23 24
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)

25 26 27 28 29 30
type schema = {
  sch_uri: string;
  sch_ns: Ns.Uri.t;
  sch_comps: (Types.t * Schema_validator.t) Ident.Env.t;
}

31
type item =
32
  (* These are really exported by CDuce units: *)
33
| Type of (Types.t * Var.t list)
34 35 36 37 38 39 40 41 42
| 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)
43

44
type t = {
45
  ids : item Env.t;
46
  delta : Var.Set.t;
47
  ns: Ns.table;
48
  keep_ns: bool
49
}
50

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

78 79
(* Namespaces *)

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

94
let qname env loc t =
95
  protect_error_ns loc (Ns.map_tag env.ns) t
96

97 98 99 100
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)
101

102 103 104 105 106 107 108 109 110 111
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

112 113
let load_schema = ref (fun _ _ -> assert false)
let from_comp_unit = ref (fun _ -> assert false)
114
let load_comp_unit = ref (fun _ -> assert false)
115 116
let has_ocaml_unit = ref (fun _ -> false)
let has_static_external = ref (fun _ -> assert false)
117

118 119 120 121 122
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 }
123

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

131 132
let enter_id x i env =
  { env with ids = Env.add x i env.ids }
133

134 135
let type_using env loc x cu =
  try
136 137 138 139 140
    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))

141
let enter_type id t env = enter_id id (Type (t,[])) env
142
let enter_types l env =
143
  { env with ids =
144
      List.fold_left (fun accu (id,t,al) ->
145
        Env.add id (Type (t,List.map fst al)) accu
146 147
      ) env.ids l
  }
148

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

let find_id_comp env0 env loc x =
  if ((match (U.get_str x).[0] with 'A'..'Z' -> true | _ -> false)
159
      && !has_ocaml_unit x)
160 161 162
  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
      List.fold_left (fun accu (id,t) -> Env.add id (Val t) accu) env.ids l;
170 171
  }

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 179
  | Val _ | EVal _ -> true
  | _ -> false
180 181
  with Not_found -> true

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

187
let register_types cu env =
188
  Env.iter (fun x -> function
189 190 191
  | Type (t,vars) ->
    let subst = List.map (fun x -> x, Types.var x) vars in
    Types.Print.register_global (cu,(Ident.value x), subst) t
192
  | _ -> ()
193
  ) env.ids
194

195 196 197 198 199 200 201 202 203
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
204
  | Const c -> c
205 206 207
  | _ -> raise_loc_generic loc "This should be a scalar or structured constant"

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

210 211
let find_schema_component sch name =
  try ESchemaComponent (Env.find name sch.sch_comps)
212
  with Not_found ->
213
    raise (Error (Printf.sprintf "No component named '%s' found in schema '%s'"
214 215 216 217
		    (Ns.QName.to_string name) sch.sch_uri))

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

245 246
let rec find_global env loc ids =
  match ids with
247
  | id::rest ->
248
    let comp = find_id env env loc (*true*) (rest != []) id in
249 250
    snd (List.fold_left (navig loc env) (env,comp) rest)
  | _ -> assert false
251

252 253 254
let eval_ns env loc = function
  | `Uri ns -> ns
  | `Path ids ->
255 256 257 258
    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"
259 260 261 262

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

267 268
let find_global_type env loc ids =
  match find_global env loc ids with
269
  | Type (t,pargs) -> (t,pargs)
270
  | ESchemaComponent (t,_) -> (t,[]) (* XXX *)
271
  | _ -> error loc "This path does not refer to a type"
272 273 274

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

278 279
let find_local_type env loc id =
  match Env.find id env.ids with
280 281
  | Type (t,pargs) -> (t,pargs)
  | _ -> raise Not_found
282 283

let find_value id env =
284
  match Env.find id env.ids with
285 286
  | Val t | EVal (_,_,t) -> t
  | _ -> raise Not_found
287

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

303 304 305

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

309
module IType = struct
310
  open Typepat
311

312
  (* From AST to the intermediate representation *)
313

314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389
  (* We need to be careful about the order of type definitions in case
     of polymorphic types.  Mutually recursive polymorphic types
     cannot be recursively called with different parameters within
     their recursive groups. We build a graph from the type
     definitions and use Tarjan's algorithm to find all strongly
     connected components in topological order.  Then we translate the
     AST into intermediate representation in that order. *)

  let scc defs =
    let module Info =
          struct
            type t =
              { mutable index : int;
                mutable lowlink : int;
                mutable is_removed : bool;
                def : (loc * U.t) * U.t list * ppat;
              }
            let empty = { index = -1; lowlink = -1;
                          is_removed = false;
                          def = ((noloc,U.empty), [],
                                 (mknoloc (Internal(Types.empty)))) }
          end
    in
    let open Info in
    let index = ref 0 and stack = ref [] in
    let res = ref [] and map = Hashtbl.create 17 and rank = ref ~-1 in
    let g = Hashtbl.create 17 in
    List.iter (fun (((_, v), _, _) as def) ->
      Hashtbl.add g v { empty with def = def }) defs;
    let rec strong_connect v vinfo =
      vinfo.index <- !index;
      vinfo.lowlink <- !index;
      incr index;
      stack := v :: !stack;
      vinfo.is_removed <- false;
      let _,_, vdef = vinfo.def in
      pat_iter (fun p ->
        match p.descr with
        | PatVar ([ w ], _) ->
          let winfo = try Some (Hashtbl.find g w) with Not_found -> None in begin
          match winfo with Some winfo ->
            if winfo.index == -1 then begin
              strong_connect w winfo;
              vinfo.lowlink <- min vinfo.lowlink winfo.lowlink
            end else if not winfo.is_removed then
                vinfo.lowlink <- min vinfo.lowlink winfo.index
          | _ -> ()
          end
        | _ -> ()
      ) vdef;
      if vinfo.lowlink == vinfo.index then
        let cc = ref [] in incr rank;
        while let w = List.hd !stack in
              stack := List.tl !stack;
              let winfo = Hashtbl.find g w in
              let _, params, _ = winfo.def in
              Hashtbl.add map w (!rank, params);
              cc := winfo.def :: !cc;
              winfo.is_removed <- true;
              not (U.equal w v) do () done;
        res := !cc :: !res
    in
    let () = List.iter
      (fun ((_, v), _, _) ->
        let vinfo = Hashtbl.find g v in
        if vinfo.index == -1 then
          strong_connect v vinfo) defs
    in
    (*
    Format.eprintf "SCC of type definitions are :@\n";
    List.iter (fun l ->
      Format.eprintf "%a@\n"
        (Utils.pp_list (fun ppf ((_,v),_,_) -> U.print ppf v)) l ) res;
    *)
    List.rev !res, map

390 391
  type penv = {
    penv_tenv : t;
392
    penv_derec : (node * U.t list) Env.t;
393
    penv_var : (string, Var.var) Hashtbl.t;
394 395
  }

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

398
  let all_delayed = ref []
399 400
  let dummy_params = (-1, [], Hashtbl.create 0)
  let current_params = ref dummy_params
401

402 403 404 405
  let clean_params () = current_params := dummy_params
  let clean_on_err () =
    all_delayed := [];
    clean_params ()
406

407 408 409 410 411 412
  let delayed loc =
    let s = mk_delayed () in
    all_delayed := (loc,s) :: !all_delayed;
    s

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

415 416
  let check_delayed () =
    let l = !all_delayed in
417
    all_delayed := [];
418
    List.iter check_one_delayed l
419

420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451
  let seq_to_list e =
    let rec loop e acc =
      match e with
      | Seq(e1, e2) -> loop e1 (loop e2 acc)
      | _ -> e :: acc
    in
    loop e []

  let list_to_seq l =
    let rec loop l acc =
    match l with
      [] -> acc
    | ((Elem { descr = PatVar(_, []); _} ) as var) ::
      ((Arg _) as arg) :: rest -> loop rest (re_seq acc (re_seq var arg))
    | (Arg r) :: rest | r :: rest -> loop rest (re_seq acc r)
    in
    loop l Epsilon

  let rec clean_re e =
    match e with
    | Seq(_,_) -> let l = seq_to_list e in
      let l =
        List.map (function Arg e -> Arg (clean_re e) | e -> clean_re e) l
      in
      list_to_seq l
    | Alt(e1, e2) -> Alt (clean_re e1, clean_re e2)
    | Star e0 -> Star (clean_re e0)
    | WeakStar e0 -> WeakStar (clean_re e0)
    | SeqCapture (i, e0) -> SeqCapture (i, clean_re e0)
    | Arg e0 -> clean_re e0
    | _ -> e

452 453 454 455 456 457 458 459 460
  let rec comp_var_pat vl pl =
    match vl, pl with
      [], [] -> true
    | v :: vll, { descr = Internal (p); _ } :: pll ->
      Types.is_var p
      && (U.equal v (U.mk(Var.(id (Set.choose (Types.all_vars p))))))
      && comp_var_pat vll pll
    | _ -> false

Pietro Abate's avatar
Pietro Abate committed
461
  (* Ast -> symbolic type *)
462
  let rec derecurs env p =
Pietro Abate's avatar
Pietro Abate committed
463
    match p.descr with
464
    | PatVar ids -> derecurs_var env p.loc ids
465
    | Recurs (p,b) -> derecurs (fst (derecurs_def env b)) p
466
    | Internal t -> mk_type t
467
    | NsT ns ->
468
      mk_type (Types.atom (Atoms.any_in_ns (parse_ns env.penv_tenv p.loc ns)))
469 470 471 472 473 474 475
    | 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)
476
    | Record (o,r) ->
477 478 479 480
      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)
481
    | Constant (x,c) ->
482
      mk_constant (ident env.penv_tenv p.loc x) (const env.penv_tenv p.loc c)
483
    | Cst c -> mk_type (Types.constant (const env.penv_tenv p.loc c))
484
    | Regexp r -> rexp (derecurs_regexp env (clean_re r))
485 486
    | Concat (p1,p2) ->  mk_concat (derecurs env p1) (derecurs env p2)
    | Merge (p1,p2) -> mk_merge (derecurs env p1) (derecurs env p2)
487

488
  and derecurs_regexp env = function
489
    | Epsilon -> mk_epsilon
490 491
    | Elem p -> mk_elem (derecurs env p)
    | Guard p -> mk_guard (derecurs env p)
492 493 494 495 496 497 498 499 500 501 502
    | Seq (p1,p2) -> (* we need to disambiguate between sequence concatenation in regexp
                       and type instantiation *)
      begin
        match p1, p2 with
        Elem { loc; descr = PatVar ((id :: rest as ids), []) }, Arg (Elem t2) ->
          let nargs =
            try
              if rest == [] then (* local identifier *)
                let id = ident env.penv_tenv loc id in
                try List.length (snd (Env.find id env.penv_derec))
                with Not_found ->
503
                  List.length (snd (find_local_type env.penv_tenv loc id))
504
              else
505
                List.length (snd (find_global_type env.penv_tenv loc ids))
506
            with _ -> 0
507 508 509 510 511 512 513 514
          in
          if nargs != 0 then (* instantiation *)
            mk_elem (derecurs env { loc; descr = PatVar(ids, prod_to_list t2) })
          else
            mk_seq (derecurs_regexp env p1) (derecurs_regexp env p2)
        | _ ->
          mk_seq (derecurs_regexp env p1) (derecurs_regexp env p2)
      end
515 516 517
    | 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)
518
    | SeqCapture ((loc,x),p) -> mk_seqcapt (ident env.penv_tenv loc x) (derecurs_regexp env p)
519
    | Arg r -> derecurs_regexp env r
520

521 522
  and derecurs_var env loc ids =
    match ids with
523 524 525
    | ((id :: rest) as ids, args) ->
      let cidx, cparams, cmap = !current_params in
      let v = ident env.penv_tenv loc id in
526
      begin
527 528 529 530
        try
          let node = fst (Env.find v env.penv_derec) in
          if args == [] || comp_var_pat cparams args then node else
            raise_loc_generic loc (Printf.sprintf "Invalid instantiation of type %s during its recursive definition" (U.to_string id))
531
	with Not_found ->
532 533 534 535 536 537 538 539 540
          try
            let (t, pargs), tidx =
              if rest == [] then
                (find_local_type env.penv_tenv loc v,
                 try fst (Hashtbl.find cmap id) with Not_found -> ~-1)
              else (find_global_type env.penv_tenv loc ids, ~-1)
            in
            if cidx >= 0 && tidx == cidx && not (comp_var_pat cparams args) then
              raise_loc_generic loc (Printf.sprintf "Invalid instantiation of type %s during its recursive definition" (U.to_string id));
541 542
            let err s = Error s in
            let l =
543
              try
544 545 546 547 548 549 550
                List.map2
                  (fun v p -> (v, typ ~err (derecurs env p))) pargs args
              with Invalid_argument _ ->
              raise_loc_generic loc
                (Printf.sprintf "Wrong number of parameters for parametric type %s" (U.to_string id));
                 | Error s -> raise_loc_generic loc s
            in
551
            mk_type (Types.Substitution.full t l)
552
	  with Not_found ->
553 554
            assert (rest == []);
            if args != [] then
555
              raise_loc_generic loc
556
                (Printf.sprintf "Unknown parametric type %s" (U.to_string id))
557 558 559
            else
              mk_capture v
      end
560
    | _ -> assert false
561

562
  and derecurs_def env b =
563
    let seen = ref IdSet.empty in
564
    let b =
565
      List.map (fun ((loc,v),args,p) ->
566 567 568 569 570 571
	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;
572
	(v,loc,args,p,delayed loc)
573
      ) b
574
    in
575
    let n = List.fold_left
576
        (fun env (v,_,a,p,s) -> Env.add v (s,a) env)
577 578
        env.penv_derec b
    in
579
    let env = { env with penv_derec = n } in
580
    List.iter (fun (v,_,_, p,s) -> link s (derecurs env p)) b;
581 582
    (env, b)

583 584
  let derec penv p =
    let d = derecurs penv p in
585
    elim_concats ();
586
    check_delayed ();
587
    internalize d;
588
    d
589

590
  (* API *)
591

592 593
  let check_no_fv loc n =
    match peek_fv n with
594 595 596 597
    | None -> ()
    | Some x ->
      raise_loc_generic loc
	("Capture variable not allowed: " ^ (Ident.to_string x))
598

599
  let type_defs env b =
600
    let _, b = derecurs_def (penv env) b in
601 602 603 604 605
    elim_concats ();
    check_delayed ();
    let aux loc d =
      internalize d;
      check_no_fv loc d;
606
      try typ d
607
      with Patterns.Error s -> raise_loc_generic loc s
608
    in
609
    let b =
610
      List.map (fun (v, loc, args, _, d) ->
611 612
        let t_rhs = aux loc d in
        if (loc <> noloc) && (Types.is_empty t_rhs) then
613
          warning loc
614
            ("This definition yields an empty type for " ^ (Ident.to_string v));
615 616

        let vars_rhs = Types.all_vars t_rhs in
617
        if List.exists (fun x -> not (Var.Set.mem vars_rhs (Var.mk (U.to_string x)) )) args then
618 619 620
          raise_loc_generic loc
            (Printf.sprintf "Definition of type %s contains unbound type variables"
               (Ident.to_string v));
621
        let vars_mapping = (* create a sequence 'a -> 'a_0 for all variables *)
622
          List.map (fun v -> let vv =  Var.mk (U.to_string v) in vv, Var.fresh vv) args
623
        in
624
        let sub_list = List.map (fun (v,vt) -> v, Types.var vt) vars_mapping in
625
        let t_rhs =
626
          Types.Substitution.full t_rhs sub_list
627
        in
628
        let nargs = List.map2 (fun (_, v) (_, vt) -> v, vt) vars_mapping sub_list
629
        in
630 631
        (v,t_rhs,nargs)
      ) (List.rev b)
632
    in
633
    List.iter (fun (v,t,al) ->
634
      Types.Print.register_global ("",v, al) t
635
    ) b;
636
    enter_types b env
637

638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655
  let equal_params l1 l2 =
    try
      List.for_all2 U.equal l1 l2
    with _ -> false

  let check_params l =
    match l with
    | [] -> assert false
    | [ ((_, u),_,_) ] -> u
    | ((loc1,u),p,_) :: r ->
      try
        let (loc2,v),_,_ =
          List.find (fun (_,q,_) -> not (equal_params p q)) r
        in
        let loc = merge_loc loc1 loc2 in
        error loc (Printf.sprintf "mutually recursive types %s and %s have different type parameters" (U.to_string u) (U.to_string v))
      with Not_found -> u

656
  let type_defs env b =
657 658 659 660 661 662 663 664
    try
      let b, map = scc b in
      let r = List.fold_left (fun env b ->
        let u = check_params b in
        let idx, params = Hashtbl.find map u in
        current_params := (idx,params,map);
        type_defs env b
      ) env b in
665
      clean_params (); r
666 667
    with exn -> clean_on_err (); raise exn

668
  let typ env t =
669
    try
670
      let d = derec (penv env) t in
671 672 673 674
      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
675

676
  let pat env t =
677 678 679 680 681
    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
682

683
end
684 685 686 687 688 689

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

let dump_types ppf env =
690
  Env.iter (fun v ->
691 692 693
    function
  (Type _) -> Format.fprintf ppf " %a" Ident.print v
    | _ -> ()) env.ids
694 695 696 697 698 699

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



700

701 702
(* II. Build skeleton *)

703

704
type type_fun = Types.t -> bool -> Types.t
705

706
module Fv = IdSet
707

708 709 710
type branch = Branch of Typed.branch * branch list

let cur_branch : branch list ref = ref []
711

712
let exp' loc e =
Pietro Abate's avatar
Pietro Abate committed
713 714 715 716
  { Typed.exp_loc = loc;
    Typed.exp_typ = Types.empty;
    Typed.exp_descr = e
  }
717 718 719 720 721

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

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

722
let pat_true =
723 724 725 726
  let n = Patterns.make Fv.empty in
  Patterns.define n (Patterns.constr Builtin_defs.true_type);
  n

727
let pat_false =
728 729 730 731
  let n = Patterns.make Fv.empty in
  Patterns.define n (Patterns.constr Builtin_defs.false_type);
  n

732
let ops = Hashtbl.create 13
733 734
let register_op op arity f = Hashtbl.add ops op (arity,f)
let typ_op op = snd (Hashtbl.find ops op)
735

736 737
let fun_name env a =
  match a.fun_name with
738 739
  | None -> None
  | Some (loc,s) -> Some (ident env loc s)
740

741 742
let count_arg_name = ref 0
let fresh_arg_name () =
743 744
  incr count_arg_name;
  "__abstr_arg" ^ (string_of_int !count_arg_name)
745

746
let is_op env s =
747 748
  if (Env.mem s env.ids) then None
  else
749 750
    let (ns,s) = s in
    if Ns.Uri.equal ns Ns.empty then
751
      let s = U.get_str s in
752
      try
753 754 755 756
	let o = Hashtbl.find ops s in
	Some (s, fst o)
      with Not_found -> None
    else None
757

758 759
let rec expr env loc = function
  | LocatedExpr (loc,e) -> expr env loc e
760
  | Forget (e,t) ->
761 762
    let (fv,e) = expr env loc e and t = typ env t in
    exp loc fv (Typed.Forget (e,t))
763
  | Check (e,t) ->
764 765
    let (fv,e) = expr env loc e and t = typ env t in
    exp loc fv (Typed.Check (ref Types.empty,e,t))
766
  | Var s -> var env loc s
767
  | Apply (e1,e2) ->
768 769 770 771 772 773 774
    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)))
775
  | Abstraction a -> abstraction env loc a
776
  | (Integer _ | Char _ | Atom _ | Const _ ) as c ->
777
    exp loc Fv.empty (Typed.Cst (const env loc c))
778
  | Pair (e1,e2) ->
779 780
    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))
781
  | Xml (e1,e2) ->
782 783 784
    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))
785
  | Dot _ as e ->
786
    dot loc env e []
787
  | TyArgs (Dot _ as e, args) ->
788
    dot loc env e args
789
  | TyArgs _ ->
790
    error loc "Only OCaml external can have type arguments"
791
  | RemoveField (e,l) ->
792 793
    let (fv,e) = expr env loc e in
    exp loc fv (Typed.RemoveField (e,parse_label env loc l))
794
  | RecordLitt r ->
795 796 797 798 799 800 801
    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)
802
  | String (i,j,s,e) ->
803 804
    let (fv,e) = expr env loc e in
    exp loc fv (Typed.String (i,j,s,e))
805
  | Match (e,b) ->
806 807 808
    let (fv1,e) = expr env loc e
    and (fv2,b) = branches env b in
    exp loc (Fv.cup fv1 fv2) (Typed.Match (e, b))
809
  | Map (e,b) ->
810 811 812
    let (fv1,e) = expr env loc e
    and (fv2,b) = branches env b in
    exp loc (Fv.cup fv1 fv2) (Typed.Map (e, b))
813
  | Transform (e,b) ->
814 815 816
    let (fv1,e) = expr env loc e
    and (fv2,b) = branches env b in
    exp loc (Fv.cup fv1 fv2) (Typed.Transform (e, b))
817
  | Xtrans (e,b) ->
818 819 820
    let (fv1,e) = expr env loc e
    and (fv2,b) = branches env b in
    exp loc (Fv.cup fv1 fv2) (Typed.Xtrans (e, b))
821
  | Validate (e,ids) ->
822 823 824
    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))
825
  | SelectFW (e,from,where) ->
826
    select_from_where env loc e from where
827
  | Try (e,b) ->
828 829 830
    let (fv1,e) = expr env loc e
    and (fv2,b) = branches env b in
    exp loc (Fv.cup fv1 fv2) (Typed.Try (e, b))
831
  | NamespaceIn (pr,ns,e) ->
832 833
    let env = type_ns env loc pr ns in
    expr env loc e
834
  | KeepNsIn (k,e) ->
835
    expr (type_keep_ns env k) loc e
836
  | Ref (e,t) ->
837 838
    let (fv,e) = expr env loc e and t = typ env t in
    exp loc fv (Typed.Ref (e,t))
839 840 841 842 843 844 845

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;
846
	Typed.br_ghost = false;
847
	Typed.br_vars_empty = Fv.empty;
848
	Typed.br_vars_poly = IdMap.empty;
849 850 851 852
	Typed.br_pat = pat_true;
	Typed.br_body = yes };
      { Typed.br_loc = no.Typed.exp_loc;
	Typed.br_used = false;
853
	Typed.br_ghost = false;
854
	Typed.br_vars_empty = Fv.empty;
855
	Typed.br_vars_poly = IdMap.empty;
856 857 858 859 860
	Typed.br_pat = pat_false;
	Typed.br_body = no } ];
    Typed.br_accept = Builtin_defs.bool;
  } in
  exp' loc (Typed.Match (cond,b))
861 862


863
and dot loc env0 e args =
864
  let dot_access loc (fv,e) l =
865 866 867 868 869 870 871 872
    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) ->
873 874 875
      (match aux loc e with
      | `Val e -> `Val (dot_access loc e id)
      | `Comp c -> `Comp (navig loc env0 c id))
876
    | Var id ->
877 878 879
      (match find_id_comp env0 env0 loc id with
      | Val _ -> `Val (var env0 loc id)
      | c -> `Comp (env0,c))
880 881 882
    | e -> `Val (expr env0 loc e)
  in
  match aux loc e with
883 884 885 886 887
  | `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"
888 889

and extern loc env s args =
890 891
  let args = List.map (typ env) args in
  try
892 893 894 895 896 897
    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
898 899
    exp loc Fv.empty (Typed.External (t,i))
  with exn -> raise_loc loc exn
900

901
and var env loc s =
902 903
  let id = ident env loc s in
  match is_op env id with
904 905 906 907 908 909 910 911 912 913 914 915 916 917 918
  | 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"
919

920
and abstraction env loc a =
921 922
  let iface =
    List.map
923 924
      (fun (t1,t2) -> (typ env t1, typ env t2)) a.fun_iface
  in
925 926 927
  let t =
    List.fold_left
      (fun accu (t1,t2) -> Types.cap accu (Types.arrow t1 t2))
928
      Types.any iface in
929 930 931
  let iface =
    List.map
      (fun (t1,t2) -> (Types.descr t1, Types.descr t2))
932
      iface in
933
  let fun_name = fun_name env a in
934 935
  let env' =
    match fun_name with
936 937
    | None -> env
    | Some f -> enter_values_dummy [ f ] env
938 939
  in
  let (fv0,body) = branches env' a.fun_body in
940
  let fv = match fun_name with
941 942
    | None -> fv0
    | Some f -> Fv.remove f fv0 in
943
  let e = Typed.Abstraction
944 945 946 947 948 949
    { Typed.fun_name = fun_name;
      Typed.fun_iface = iface;
      Typed.fun_body = body;
      Typed.fun_typ = t;
      Typed.fun_fv = fv
    } in
950
  exp loc fv e
951 952

and branches env b =
953 954
  let fv = ref Fv.empty in
  let accept = ref Types.empty in
955
  let branch (p,e) =
956 957
    let cur_br = !cur_branch in
    cur_branch := [];
958 959 960
    let ploc = p.loc in
    let p = pat env p in
    let fvp = Patterns.fv p in
961
    let (fv2,e) = expr (enter_values_dummy (fvp :> Id.t list) env) noloc e in
962
    let br_loc = merge_loc ploc e.Typed.exp_loc in
963
    (match Fv.pick (Fv.diff fvp fv2) with
964 965 966 967 968 969
    | None -> ()
    | Some x ->
      let x = Ident.to_string x in
      warning br_loc
	("The capture variable " ^ x ^
	    " is declared in the pattern but not used in the body of this branch." ^
Pietro Abate's avatar
Pietro Abate committed
970
            " It might be a misspelled or undeclared type or name (if it isn't, use _ instead)."));
971 972
    let fv2 = Fv.diff fv2 fvp in
    fv := Fv.cup !fv fv2;
973 974 975 976
    let p_accept = Types.descr (Patterns.accept p) in
    if not (Var.Set.is_empty (Types.all_vars p_accept)) then
      error br_loc "Type variables cannot occur in patterns";
    accept := Types.cup !accept p_accept;
977
    let ghost = br_loc == noloc in
978 979
    let br =
      {
980
	Typed.br_loc = br_loc;
981 982
	Typed.br_used = ghost;
	Typed.br_ghost = ghost;
983
	Typed.br_vars_empty = fvp;
984
	Typed.br_vars_poly = IdMap.empty;
985
	Typed.br_pat = p;
986 987 988 989
	Typed.br_body = e } in
    cur_branch := Branch (br, !cur_branch) :: cur_br;
    br in
  let b = List.map branch b in
990 991 992 993
  (!fv,
   {
     Typed.br_typ = Types.empty;
     Typed.br_branches = b;
994
     Typed.br_accept = !accept;
995
   }
996
  )
997

998 999 1000 1001 1002 1003 1004 1005 1006
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
1007
    env := enter_values_dummy (fvp :> Id.t list) !env;
1008 1009 1010 1011 1012 1013
    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

1014
  let put_cond rest (fv,cond) =
1015 1016
    all_fv := Fv.cup (Fv.diff fv !bound_fv) !all_fv;
    if_then_else loc cond rest exp_nil in
1017
  let aux (ploc,p,fvp,e) (where,rest) =
1018 1019 1020 1021 1022
    (* 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 -> ... *)
1023
    let br = { Typed.br_loc = ploc;
1024 1025 1026 1027 1028 1029
	       Typed.br_used = false;
	       Typed.br_ghost = false;
	       Typed.br_vars_empty = fvp;
               Typed.br_vars_poly = IdMap.empty;
	       Typed.br_pat = p;
	       Typed.br_body = rest } in
1030 1031 1032 1033
    cur_branch := [ Branch (br, !cur_branch) ];
    let b = {
      Typed.br_typ = Types.empty;
      Typed.br_branches = [ br ];
1034 1035 1036 1037 1038
      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
1039 1040
  let cur_br = !cur_branch in
  cur_branch := [];
1041
  let (fv,e) = expr !env noloc (Pair(e,cst_nil)) in
1042
  cur_branch := !cur_branch @ cur_br;
1043 1044 1045
  let (where,rest) = List.fold_right aux from (where,e) in
  (* The remaining conditions are constant. Gives a warning for that. *)
  (match where with
1046 1047 1048 1049
  | (_,e) :: _ ->
    warning e.Typed.exp_loc
      "This 'where' condition does not depend on any captured variable"
  | _ -> ());
1050 1051 1052
  let rest = List.fold_left put_cond rest where in
  (Fv.cup !all_fv (Fv.diff fv !bound_fv)), rest

1053
let expr env e = snd (expr env noloc e)
1054

1055 1056
let let_decl env p e =
  { Typed.let_pat = pat env p;
1057
    Typed.let_body = expr env e }
1058

1059 1060 1061

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

1062

1063 1064
(* III. Type-checks *)

1065 1066
open Typed

1067
let localize loc f x =
1068 1069
  try f x with
  | (Error _ | Constraint (_,_)) as exn ->
1070
    raise (Cduce_loc.Location (loc,`Full,exn))
Pietro Abate's avatar
Pietro Abate committed
1071
  | Warning (s,t) -> warning loc s; t
1072

1073
let require loc t s =
1074
  if not (Types.subtype t s) then raise_loc loc (Constraint (t, s))
1075

1076
let verify loc t s =
Pietro Abate's avatar
Pietro Abate committed
1077
  require loc t s;
1078
  t
1079

Pietro Abate's avatar
Pietro Abate committed
1080
let squareverify loc delta t s =
1081
  if not (Type_tallying.is_squaresubtype delta t s) then
Pietro Abate's avatar
Pietro Abate committed
1082 1083
    raise_loc loc (Constraint (t, s));
  t
1084

1085 1086 1087 1088
let verify_noloc t s =
  if not (Types.subtype t s) then raise (Constraint (t, s));
  t

1089
let check_str loc ofs t s =
1090 1091 1092
  if not (Types.subtype t s) then raise_loc_str loc ofs (Constraint (t, s));
  t

1093
let should_have loc constr s =
1094 1095
  raise_loc loc (ShouldHave (constr,s))

1096
let should_have_str loc ofs constr s =
1097 1098
  raise_loc_str loc ofs (ShouldHave (constr,s))

1099
let flatten arg constr precise =
1100
  let constr' = Sequence.star
1101
    (Sequence.approx (Types.cap Sequence.any constr)) in
1102 1103 1104 1105 1106 1107 1108
  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
1109
    verify_noloc (Sequence.flatten t) constr
1110