typer.ml 49.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.print) 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
    (Ident.pp_env pp_item) ids
75
    Var.Set.print 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

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

312
module IType = struct
313
  open Typepat
314

315
  (* From AST to the intermediate representation *)
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 390 391 392
  (* 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

393 394
  type penv = {
    penv_tenv : t;
395
    penv_derec : (node * U.t list) Env.t;
396
    penv_var : (string, Var.t) Hashtbl.t;
397 398
  }

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

401
  let all_delayed = ref []
402 403
  let dummy_params = (-1, [], Hashtbl.create 0)
  let current_params = ref dummy_params
404

405 406 407 408
  let clean_params () = current_params := dummy_params
  let clean_on_err () =
    all_delayed := [];
    clean_params ()
409

410 411 412 413 414 415
  let delayed loc =
    let s = mk_delayed () in
    all_delayed := (loc,s) :: !all_delayed;
    s

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

418 419
  let check_delayed () =
    let l = !all_delayed in
420
    all_delayed := [];
421
    List.iter check_one_delayed l
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 452 453 454
  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

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

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

491
  and derecurs_regexp env = function
492
    | Epsilon -> mk_epsilon
493 494
    | Elem p -> mk_elem (derecurs env p)
    | Guard p -> mk_guard (derecurs env p)
495 496 497 498 499 500 501 502 503 504 505
    | 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 ->
506
                  List.length (snd (find_local_type env.penv_tenv loc id))
507
              else
508
                List.length (snd (find_global_type env.penv_tenv loc ids))
509
            with _ -> 0
510 511 512 513 514 515 516 517
          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
518 519 520
    | 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)
521
    | SeqCapture ((loc,x),p) -> mk_seqcapt (ident env.penv_tenv loc x) (derecurs_regexp env p)
522
    | Arg r -> derecurs_regexp env r
523

524 525
  and derecurs_var env loc ids =
    match ids with
526 527 528
    | ((id :: rest) as ids, args) ->
      let cidx, cparams, cmap = !current_params in
      let v = ident env.penv_tenv loc id in
529
      begin
530 531 532 533
        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))
534
	with Not_found ->
535 536 537 538 539 540 541 542 543
          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));
544 545
            let err s = Error s in
            let l =
546
              try
547 548 549 550 551 552 553
                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
554
            mk_type (Types.Subst.full_list t l)
555
	  with Not_found ->
556 557
            assert (rest == []);
            if args != [] then
558
              raise_loc_generic loc
559
                (Printf.sprintf "Unknown parametric type %s" (U.to_string id))
560 561 562
            else
              mk_capture v
      end
563
    | _ -> assert false
564

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

586 587
  let derec penv p =
    let d = derecurs penv p in
588
    elim_concats ();
589
    check_delayed ();
590
    internalize d;
591
    d
592

593
  (* API *)
594

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

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

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

641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658
  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

659
  let type_defs env b =
660 661 662 663 664 665 666 667
    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
668
      clean_params (); r
669 670
    with exn -> clean_on_err (); raise exn

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

679
  let pat env t =
680 681 682 683 684
    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
685

686
end
687 688 689 690 691 692

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

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

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



703

704 705
(* II. Build skeleton *)

706

707
type type_fun = Types.t -> bool -> Types.t
708

709
module Fv = IdSet
710

711 712 713
type branch = Branch of Typed.branch * branch list

let cur_branch : branch list ref = ref []
714

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

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

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

725
let pat_true =
726 727 728 729
  let n = Patterns.make Fv.empty in
  Patterns.define n (Patterns.constr Builtin_defs.true_type);
  n

730
let pat_false =
731 732 733 734
  let n = Patterns.make Fv.empty in
  Patterns.define n (Patterns.constr Builtin_defs.false_type);
  n

735
let ops = Hashtbl.create 13
736 737
let register_op op arity f = Hashtbl.add ops op (arity,f)
let typ_op op = snd (Hashtbl.find ops op)
738

739 740
let fun_name env a =
  match a.fun_name with
741 742
  | None -> None
  | Some (loc,s) -> Some (ident env loc s)
743

744 745
let count_arg_name = ref 0
let fresh_arg_name () =
746 747
  incr count_arg_name;
  "__abstr_arg" ^ (string_of_int !count_arg_name)
748

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

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

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


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

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

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

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

and branches env b =
956 957
  let fv = ref Fv.empty in
  let accept = ref Types.empty in
958
  let branch (p,e) =
959 960
    let cur_br = !cur_branch in
    cur_branch := [];
961 962 963
    let ploc = p.loc in
    let p = pat env p in
    let fvp = Patterns.fv p in
964
    let (fv2,e) = expr (enter_values_dummy (fvp :> Id.t list) env) noloc e in
965
    let br_loc = merge_loc ploc e.Typed.exp_loc in
966
    (match Fv.pick (Fv.diff fvp fv2) with
967 968 969 970 971 972
    | 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
973
            " It might be a misspelled or undeclared type or name (if it isn't, use _ instead)."));
974 975
    let fv2 = Fv.diff fv2 fvp in
    fv := Fv.cup !fv fv2;
976 977 978 979
    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;
980
    let ghost = br_loc == noloc in
981 982
    let br =
      {
983
	Typed.br_loc = br_loc;
984 985
	Typed.br_used = ghost;
	Typed.br_ghost = ghost;
986
	Typed.br_vars_empty = fvp;
987
	Typed.br_vars_poly = IdMap.empty;
988
	Typed.br_pat = p;
989 990 991 992
	Typed.br_body = e } in
    cur_branch := Branch (br, !cur_branch) :: cur_br;
    br in
  let b = List.map branch b in
993 994 995 996
  (!fv,
   {
     Typed.br_typ = Types.empty;
     Typed.br_branches = b;
997
     Typed.br_accept = !accept;
998
   }
999
  )
1000

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

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

1056
let expr env e = snd (expr env noloc e)
1057

1058 1059
let let_decl env p e =
  { Typed.let_pat = pat env p;
1060
    Typed.let_body = expr env e }
1061

1062 1063 1064

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

1065

1066 1067
(* III. Type-checks *)

1068 1069
open Typed

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

1076
let require loc t s =
1077
  if not (Types.subtype t s) then raise_loc loc (Constraint (t, s))
1078

1079
let verify loc t s =
Pietro Abate's avatar
Pietro Abate committed
1080
  require loc t s;
1081
  t
1082

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

1088 1089 1090 1091
let verify_noloc t s =
  if not (Types.subtype t s) then raise (Constraint (t, s));
  t

1092
let check_str loc ofs t s =
1093 1094 1095
  if not (Types.subtype t s) then raise_loc_str loc ofs (Constraint (t, s));
  t

1096
let should_have loc constr s =
1097 1098
  raise_loc loc (ShouldHave (constr,s))

1099
let should_have_str loc ofs constr s =
1100 1101
  raise_loc_str loc ofs (ShouldHave (constr,s))

1102
let flatten arg constr precise =
1103
  let constr' = Sequence.star
1104