typer.ml 48.8 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
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.t) 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
  let rec comp_var_pat vl pl =
    match vl, pl with
      [], [] -> true
    | v :: vll, { descr = Internal (p); _ } :: pll ->
      Types.is_var p
457
      && (U.equal v (U.mk(Var.(ident (Set.choose (Types.all_vars p))))))
458
459
460
      && 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)
Pietro Abate's avatar
Pietro Abate committed
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.Subst.full_list 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
Pietro Abate's avatar
Pietro Abate committed
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.refresh 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.Subst.full_list 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)
Pietro Abate's avatar
Pietro Abate committed
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