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
Pietro Abate's avatar
Pietro Abate committed
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 =
Pietro Abate's avatar
Pietro Abate committed
144
      List.fold_left (fun accu (id,t,al) ->
145
        Env.add id (Type (t,List.map fst al)) accu
Pietro Abate's avatar
Pietro Abate committed
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 =
Pietro Abate's avatar
Pietro Abate committed
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
  | _ -> ()
Pietro Abate's avatar
Pietro Abate committed
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)
Pietro Abate's avatar
Pietro Abate committed
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
Pietro Abate's avatar
Pietro Abate committed
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)
Pietro Abate's avatar
Pietro Abate committed
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 (