1. camlspotter
  2. olfend

Source

olfend / typed.ml

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
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
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
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
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
(* Very weak sort of static typing *)

open Spotlib.Spot
open Sexplib.Conv
open Sexplib.Sexp

module IdentSet = Set.Make(Ident)
module PathSet = Set.Make(Path)

open Types
type 'a typed = { desc: 'a; typ: Type.t } with sexp
 
module O = Olf.Expr
module OT = Olf.Top

module TyEnv = struct
  type t = {
    env      : Env.t;
    subst     : (int * Type.t) list;
  } with sexp

  let initial = { env = Predef.Env.predef; subst = [] } (* need to have the prim types *)

  let unify t t1 t2 =
    let ty, sub = Type.unify t.subst t1 t2 in
    ty, {t with subst = sub }


  let format ppf t = pp_hum ppf (sexp_of_t t)

  let search p path tyEnv = 
    let env, path, desc = Env.search p path tyEnv.env in
    path, desc, { tyEnv with env = env } 

  let add_vars vars tyEnv = { tyEnv with env = { tyEnv.env with Env.vars = vars @ tyEnv.env.Env.vars  } }
  let globals tyEnv = tyEnv.env.Env.globals
  let set_globals globals tyEnv = { tyEnv with env = { tyEnv.env with Env.globals = globals } }
  let set_subst subst tyEnv = { tyEnv with subst = subst }
end

open TyEnv

module Expr = struct
  type t = t_ typed
      
  and t_ =
    | Var     of Path.t
    | Abs     of pattern list * t
    | Let     of pattern * (Ident.t * Poly.t) list * t * t (* App (Abs ([x], t), e) *)
    | Letrec  of Ident.t * (Ident.t * Poly.t) list * t * t
    | App     of t list
    | If      of t * t * t
    | Const   of Const.t
    | Prim    of Prim.t
    | Tuple   of t list 
    | Match   of t * case list
    | Constr  of Path.t * Tag.t * int (* arity *)
    | Field   of Path.t * Tag.t
    | Record  of (Path.t * Tag.t * t) list
        
  and case = pattern * t (* action *)
      
  and pattern = pattern_ typed

  and pattern_ = 
    | PAny
    | PVar   of Ident.t
    | PConst of Const.t
    | PTuple of pattern list
    | PConstructed of Path.t * Tag.t * pattern list
    | PRecord of (Path.t * Tag.t * pattern) list (* NOTE! All are listed and sorted *)

  with sexp

  let rec sexp_of_pattern p = match p.desc with
    | PAny -> Atom "_"
    | PVar ident -> Ident.sexp_of_t ident
    | PConst c -> Const.sexp_of_t c
    | PTuple ps -> List ( Atom "tuple" :: List.map sexp_of_pattern ps )
    | PRecord fps -> List ( Atom "record" :: List.map (fun (f,_,p) -> List [ Path.sexp_of_t f; sexp_of_pattern p ]) fps )
    | PConstructed (p, _, ps) -> List ( Path.sexp_of_t p :: List.map sexp_of_pattern ps )
  
  let rec pattern_vars p = match p.desc with
    | PAny -> []
    | PVar _ -> [p]
    | PConst _ -> []
    | PTuple ps | PConstructed (_, _, ps) -> List.concat_map pattern_vars ps
    | PRecord fps -> List.concat_map (fun (_,_,p) -> pattern_vars p) fps
  
  let pattern_idents p = 
    pattern_vars p
    |> List.map (function
        | { desc= PVar id } -> id
        | _ -> assert false)
    |> IdentSet.of_list
  
  let pattern_paths p = 
    pattern_idents p |> IdentSet.to_list |> List.map Path.of_ident |> PathSet.of_list
      
  let pattern_env p =
    pattern_vars p
    |> List.map (function
        | { desc = PVar id; typ = ty } -> (id, Env.Value (Poly.of_type ty))
        | _ -> assert false)

  let free_vars exp = 
    let open PathSet in
    let rec fvars e = match e.desc with
      | Var p -> one p
      | Abs (pats, t) -> fvars t - unions ( List.map pattern_paths pats )
      | Let (pat, _env, t1, t2) -> fvars t1 + (fvars t2 - pattern_paths pat)
      | Letrec (ident, _env, t1, t2) -> fvars t1 + fvars t2 - one (Path.of_ident ident)
      | App ts | Tuple ts -> unions (List.map fvars ts)
      | If (t1, t2, t3) -> unions (List.map fvars [t1; t2; t3])
      | Const _ | Prim _ | Constr _ | Field _ -> empty
      | Match (t, cases) -> unions (fvars t :: List.map fvars_case cases)
      | Record path_tag_expr_list -> unions (List.map (fun (_,_,e) -> fvars e) path_tag_expr_list)
  
    and fvars_case (p, t) =fvars t - pattern_paths p
    in
    to_list (fvars exp)
  
  let rec sexp_of_t t = match t.desc with
    | Var v -> Path.sexp_of_t v
    | Field (p, _tag) -> Path.sexp_of_t p
    | Abs (pats, t) -> 
        List [ Atom "fun"
    	     ; List (List.map sexp_of_pattern pats)
    	     ; sexp_of_t t ]
    | Let (pat, _env, t1, t2) ->
        List [ Atom "let"
    	     ; List [ sexp_of_pattern pat; sexp_of_t t1 ]
    	     ; sexp_of_t t2 ]
    | Letrec (v, _env, t1, t2) ->
        List [ Atom "letrec"
    	     ; List [ Ident.sexp_of_t v; sexp_of_t t1 ]
    	     ; sexp_of_t t2 ]
    | App ts ->
        List (List.map sexp_of_t ts)
    | If (t1, t2, t3) ->
        List [ Atom "if"; sexp_of_t t1; sexp_of_t t2; sexp_of_t t3 ]
    | Prim p -> Prim.sexp_of_t p
    | Const c -> Const.sexp_of_t c
    | Tuple args ->
        List ( Atom "tuple" :: List.map sexp_of_t args )
    | Match (e, cases) ->
        List ( Atom "match"
               :: sexp_of_t e
               :: List.map sexp_of_case cases )
    | Constr (p, _, _) -> Path.sexp_of_t p
    | Record  path_tag_expr_list ->
        List ( Atom "record" ::
                 List.map (fun (path,_,e) ->
                   List [ Path.sexp_of_t path; sexp_of_t e ]) path_tag_expr_list )
          
  and sexp_of_case (pat, action) =
    List [ sexp_of_pattern pat;
           sexp_of_t action ]
    
  let format ppf t = Sexplib.Sexp.pp_hum ppf (sexp_of_t t)
  let format_pattern ppf t = Sexplib.Sexp.pp_hum ppf (sexp_of_pattern t)
  
  (** e => \x y z -> e x y z *)
  let eta_expand e = function
    | 0 -> e
    | n ->
        let targs, trest = 
          let rec get_nargs n ty =
            match n with
            | 0 -> [], ty
            | n ->
                match ty with
                | Arrow (t1, t2) ->
                    let args, rest = get_nargs (n-1) t2 in
                    t1::args, rest
                | _ -> assert false
          in
          get_nargs n e.typ
        in
        let vars = List.init_from_to 1 n (fun i -> "eta" ^ string_of_int i) in
        let ids = List.map Ident.create vars in
        let pats = List.map2 (fun v t -> { desc = PVar v; typ= t }) ids targs in
        let args = List.map2 (fun id t -> { desc = Var (Path.of_ident id); typ = t } ) ids targs in
        { desc= Abs (pats, { desc = App (e :: args); typ = trest });
          typ= e.typ }

  (* typing *)
        
  let typeof_const = function
    | Const.Int _    -> Predef.Type.int
    | Const.Float _  -> Predef.Type.float
    | Const.Bool _   -> Predef.Type.bool
    | Const.String _ -> Predef.Type.string
    | Const.Char _   -> Predef.Type.char
    
  (* No unification happens inside so far *)  
  let rec of_pattern tyEnv = function
    | O.PAny -> 
        { desc= PAny; typ= Type.create_var () }, tyEnv
    | O.PConst c -> 
        { desc= PConst c; typ= typeof_const c }, tyEnv
    | O.PVar s -> 
        let id = Ident.create s in
        let ty = Type.create_var () in
        { desc= PVar id; typ= ty }, 
        { tyEnv with env = { tyEnv.env with Env.vars = (id, Path.of_ident id, Env.Value (Poly.of_type ty)) :: tyEnv.env.Env.vars } }
    | O.PTuple ps ->
        let rev_ps, tyEnv = List.fold_left (fun (rev_ps, tyEnv) p ->
          let p, tyEnv = of_pattern tyEnv p in
          p::rev_ps, tyEnv) ([], tyEnv) ps
        in
        let ps = List.rev rev_ps in
        let tys = List.map (fun p -> p.typ) ps in
        { desc= PTuple ps; typ= Types.Tuple tys }, tyEnv
    | O.PRecord [] -> assert false (* I cannot fix the type! *)
    | O.PRecord ((l,_)::_ as label_pats) ->
        (* CR jfuruse: sharing with typing of Record *)
        let dt_p, decl, tyEnv = match TyEnv.search (function Env.Field _ -> true | _ -> false) l tyEnv with
          | _p, Env.Field (_tag, dt_p, decl, _rty), tyEnv -> dt_p, decl, tyEnv
          | _ -> assert false
        in 
        let i_tyvars, i_kind = Decl.inst decl in
        let ifields = match i_kind with
          | Types.Record fields -> List.mapi (fun n (id, ty) -> Ident.name id, Tag.of_int n, ty) fields
          | _ -> assert false
        in
        let res_ty = Types.Constr (dt_p, decl, i_tyvars) in

        (* field typing. No unification with rty yet (it should be done with ifields) *)
        let used_fields, tyEnv = List.fold_left (fun (pats, tyEnv) (l,pat) ->
          match Env.search (function Env.Field _ -> true | _ -> false) l tyEnv.env with
          | env, p, Env.Field (tag, dt_p', _decl, _rty) ->
              if dt_p <> dt_p' then failwithf "label %s is for a different record type %s" (Path.name p) (Path.name dt_p');
              let tyEnv = { tyEnv with env = env } in
              let pat, tyEnv = of_pattern tyEnv pat in
              let get_label = function
                | Path.Ident id -> Ident.name id
                | Path.Dot (_, id, _) -> Ident.name id
              in
              (get_label p, p, tag, pat)::pats, tyEnv
          | _ -> assert false) ([], tyEnv) label_pats
        in

        (* check fields are unique *)
        begin match List.is_unique (fun (x,_,_,_) -> x) used_fields with
        | None -> ()
        | Some ((l, _, _, _),_) -> failwithf "Record label %s is used more than once" l
        end;

        (* unused labels are filled with PAny *)
        let fields =  
         List.map (fun (name, tag, ty) -> 
            try
              List.find (fun (name', _, _, _) -> name = name') used_fields
            with
            | Not_found -> (name, 
                            Path.of_ident (Ident.create name) (* CR jfuruse : it is not right! *),
                            tag,
                            { desc = PAny; typ = Type.subst tyEnv.subst ty })
          ) ifields
        in

        (* unify the member types against ifields *)
        let tyEnv = List.fold_left (fun tyEnv (l,_p,_tag,pat) ->
          try 
            let (_,_,ty) = List.find (fun (l',_,_) -> l = l') ifields in
            let _, tyEnv = TyEnv.unify tyEnv (Type.subst tyEnv.subst pat.typ) (Type.subst tyEnv.subst ty) in
            tyEnv
          with Not_found -> assert false (* already checked *) (* CR jfuruse: but we can have nicer error message here *))
          tyEnv fields
        in

        { desc = PRecord (List.sort (fun (_,t1,_) (_,t2,_) -> compare t1 t2) (List.map (fun (_l,p,tag,e) -> (p,tag,e)) fields));
          typ = Type.subst tyEnv.subst res_ty },
        tyEnv

    | O.PConstructed (p, ps) ->
        match Env.search (function Env.Constr _ -> true | _ -> false) p tyEnv.env with
        | env, p, Env.Constr (tag, pty) ->
            let tyEnv = { tyEnv with env = env } in
            let _, pty = Poly.inst pty in
            let arity, argtys, retty = Type.arity [] pty in
            if List.length ps <> arity then failwithf "Arity mismatch of %s" (Path.name p);
            let rev_ps, tyEnv = List.fold_left (fun (rev_ps, tyEnv) (p, argty) ->
              let p, tyEnv = of_pattern tyEnv p in
              let _, tyEnv = TyEnv.unify tyEnv p.typ (Type.subst tyEnv.subst argty) in
              p::rev_ps, tyEnv) ([], tyEnv) (List.combine ps argtys)
            in
            let ps = List.rev rev_ps in
            { desc= PConstructed (p, tag, ps); typ= Type.subst tyEnv.subst retty }, tyEnv
        | _ -> assert false

  let generalize_pattern tyEnv pattern = 
    let env = pattern_env pattern in
    List.map (fun (id, envdesc) ->
      (id, 
       match envdesc with
       | Env.Value (Types.Poly ([], ty)) -> 
           let pty = Poly.generalize (Type.subst tyEnv.subst ty) in
           (* Format.eprintf "(lev %d) %a : %a@." !Types.current_level Ident.format id Poly.format pty; *)
           pty
       | _ -> assert false)) env

  let rec of_olf tyEnv0 = function
    | O.Var p -> 
        (* Format.eprintf "var %s@." (Rawname.Path.name p); *)
        begin match TyEnv.search (function Env.Value _ | Env.Field _ -> true | _ -> false) p tyEnv0 with
        | p, Env.Value pty, tyEnv -> 
(* Format.eprintf "  typing value done %a@." Path.format p; *)
            let ty = snd (Poly.inst pty) in
            { desc= Var p; typ = ty }, tyEnv
        | p, Env.Field (tag, dt_p, decl, rty), tyEnv ->
(* Format.eprintf "  field %a@." Path.format p; *)
            let pty = Env.record_accessor_poly_type dt_p decl rty in
            let ty = snd (Poly.inst pty) in
            { desc= Field (p, tag); typ = ty }, tyEnv
        | _ -> assert false
        end

    | O.Abs (patterns, t) ->
        let rev_patterns, tyEnv = 
          List.fold_left (fun (rev_patterns, tyEnv) p ->
            let p, tyEnv = of_pattern tyEnv p in
            p::rev_patterns, tyEnv) ([], tyEnv0) patterns
        in
        let patterns = List.rev rev_patterns in
        let t, tyEnv = of_olf tyEnv t in
        let ty = Type.subst tyEnv.subst (List.fold_right (fun p ty -> Arrow (p.typ, ty)) patterns t.typ) in
        { desc= Abs (patterns, t); typ= ty }, { env = { tyEnv0.env with Env.globals = tyEnv.env.Env.globals };
                                                subst = tyEnv.subst}

    | O.Let (pattern, t1, t2) ->

        Types.incr_level ();

        let pattern, tyEnv = of_pattern tyEnv0 pattern in
        let t1,tyEnv = of_olf {tyEnv0 with subst = tyEnv.subst} t1 in
        let _ty, tyEnv = 
          try TyEnv.unify tyEnv (Type.subst tyEnv.subst pattern.typ) t1.typ with 
          | e ->
              Format.eprintf "@[<2>Pattern %a has type@ %a which is incompatible with the definition type@ %a@]@."
                format_pattern pattern
                Type.format (Type.subst tyEnv.subst pattern.typ)
                Type.format t1.typ;
              raise e
        in

        Types.decr_level ();

        let bind_env = generalize_pattern tyEnv pattern in
        let env = List.map (fun (id,pty) -> id,Path.of_ident id, Env.Value pty) bind_env in
        let tyEnv = { tyEnv with env = { tyEnv.env with Env.vars = env @ tyEnv0.env.Env.vars } } in

        let t2, tyEnv = of_olf tyEnv t2 in
        { desc= Let (pattern, bind_env, t1, t2); typ= t2.typ }, 
        tyEnv0 |> TyEnv.set_globals (TyEnv.globals tyEnv)
               |> TyEnv.set_subst tyEnv.subst

    | O.Letrec (name, t1, t2) ->

        Types.incr_level ();

        let ident = Ident.create name in
        let tv = Type.create_var () in
        let tyEnv = TyEnv.add_vars [(ident, Path.of_ident ident, Env.Value (Poly.of_type tv))] tyEnv0 in
        let t1, tyEnv = of_olf tyEnv t1 in
        let _ty, tyEnv = 
          try TyEnv.unify tyEnv (Type.subst tyEnv.subst tv) t1.typ with
          | e ->
              Format.eprintf "@[<2>Pattern %a has type@ %a which is incompatible with the definition type@ %a@]@."
                Ident.format ident
                Type.format (Type.subst tyEnv.subst tv)
                Type.format t1.typ;
              raise e
        in

        Types.decr_level ();

        let pattern = { desc = PVar ident; typ = tv } in 
        let bind_env = generalize_pattern tyEnv pattern in
        let env = List.map (fun (id,pty) -> (id, Path.of_ident id, Env.Value pty)) bind_env in
        let tyEnv = TyEnv.add_vars env tyEnv0 in

        let t2, tyEnv = of_olf tyEnv t2 in
        { desc= Letrec (ident, bind_env, t1, t2); typ = t2.typ }, 
        tyEnv0 |> TyEnv.set_globals (TyEnv.globals tyEnv)
               |> TyEnv.set_subst tyEnv.subst

    | O.Prim p -> { desc= Prim p; typ= Typrim.typeof_prim p }, tyEnv0

    | O.App ts -> 
        let ts, tyEnv = List.fold_right (fun t (ts,tyEnv) -> 
          let t, tyEnv = of_olf tyEnv t in
          (t::ts, tyEnv)) ts ([],tyEnv0)
        in
        begin match ts with
        | [t] -> t, tyEnv
        | t::ts ->
            let tres = Type.create_var () in
            let ty1 = Type.subst tyEnv.subst t.typ in
            let ty2 = Type.subst tyEnv.subst (List.fold_right (fun arg funt -> Arrow (arg.typ, funt)) ts tres) in
            let _, tyEnv = 
              try TyEnv.unify tyEnv ty1 ty2 with
              | e ->
                  Format.eprintf "@[<2>Function %a has type@ %a which is incompatible with the application context@ %a@]@."
                    format t
                    Type.format ty1
                    Type.format ty2;
                  raise e
            in
            let tres = Type.subst tyEnv.subst tres in
            { desc= App (t::ts); typ= tres }, tyEnv
        | [] -> assert false
        end
    | O.If (t1, t2, t3) -> 
        let t1, tyEnv = of_olf tyEnv0 t1 in
        let _, tyEnv = 
          try TyEnv.unify tyEnv t1.typ Predef.Type.bool with
          | e ->
              Format.eprintf "@[<2>If condition %a has type@ %a which is incompatible with bool@]@."
                format t1
                Type.format t1.typ;
              raise e
        in
        let t2, tyEnv = of_olf tyEnv t2 in
        let t3, tyEnv = of_olf tyEnv t3 in
        let resty, tyEnv = 
          try TyEnv.unify tyEnv t2.typ t3.typ with
          | e ->
              Format.eprintf "@[<2>Then-else have incompatible types:@ %a@ and@ %a@]@."
                Type.format (Type.subst tyEnv.subst t2.typ)
                Type.format t3.typ;
              raise e
        in
        { desc= If (t1, t2, t3); typ= resty }, tyEnv
    | O.Const c -> { desc= Const c; typ= typeof_const c }, tyEnv0
    | O.Tuple args ->
        let args, tyEnv = List.fold_right (fun arg (args,tyEnv) ->
          let arg, tyEnv = of_olf tyEnv arg in
          arg::args, tyEnv) args ([],tyEnv0)
        in
        let ty = Types.Tuple (List.map (fun arg -> Type.subst tyEnv.subst arg.typ) args) in
        { desc= Tuple args; typ= ty }, tyEnv

    | O.Match (e, cases) -> 
        let retty = Type.create_var () in
        let e, tyEnv = of_olf tyEnv0 e in
        let cases, tyEnv = List.fold_right (fun case (cases,tyEnv) ->
          let case, tyEnv = of_case tyEnv e.typ retty case in
          case::cases, tyEnv) cases ([], tyEnv)
        in
        { desc= Match (e, cases);
          typ= Type.subst tyEnv.subst retty }, 
        tyEnv

    | O.Constr p -> 
        let p, tag, arity, ty, tyEnv = 
          match TyEnv.search (function Env.Constr _ -> true | _ -> false) p tyEnv0 with
          | p, Env.Constr (tag, pty), tyEnv -> 
(* Format.eprintf "  typing constr %a@." Path.format p; *)
             let arity, _, _ = Poly.arity [] pty in
              p, tag, arity, snd (Poly.inst pty), tyEnv
          | _ -> assert false
        in
        { desc= Constr (p, tag, arity); typ = Type.subst tyEnv0.subst ty }, 
        tyEnv0 |> TyEnv.set_globals (TyEnv.globals tyEnv)

    | O.Record [] -> assert false

    | O.Record ((l,_)::_ as label_exprs) ->
        let tyEnv = tyEnv0 in
        let dt_p, decl, tyEnv = match TyEnv.search (function Env.Field _ -> true | _ -> false) l tyEnv with
          | _p, Env.Field (_tag, dt_p, decl, _rty), tyEnv -> dt_p, decl, tyEnv
          | p, _, _ -> failwithf "This is not a record label: %s" (Path.name p)
        in 
        let i_tyvars, i_kind = Decl.inst decl in
        let ifields = match i_kind with
          | Types.Record fields -> List.map (fun (id, ty) -> Ident.name id, ty) fields
          | _ -> assert false
        in
        let res_ty = Types.Constr (dt_p, decl, i_tyvars) in

        (* field typing. No unification with rty yet (it should be done with ifields) *)
        let used_fields, tyEnv = List.fold_left (fun (es, tyEnv) (l,expr) ->
          match TyEnv.search (function Env.Field _ -> true | _ -> false) l tyEnv with
          | p, Env.Field (tag, dt_p', _decl, _rty), tyEnv -> 
              if dt_p <> dt_p' then failwithf "label %s is for a different record type %s" (Path.name p) (Path.name dt_p');
              let e, tyEnv = of_olf tyEnv expr in
              (Path.postfix p, p, tag, e)::es, tyEnv
          | p, _, _ -> failwithf "This is not a record label: %s" (Path.name p)) ([], tyEnv) label_exprs
        in

        (* check fields are unique *)
        begin match List.is_unique (fun (x,_,_,_) -> x) used_fields with
        | None -> ()
        | Some ((l, _, _, _),_) -> failwithf "Record label %s is used more than once" l
        end;

        (* check all fields are used *)
        if List.length used_fields <> List.length ifields then failwithf "Some record labels are missing";

        (* unify the member types against ifields *)
        let tyEnv = List.fold_left (fun tyEnv (l,_p,_tag,e) ->
          try 
            let ty = List.assoc l ifields in
            let _, tyEnv = TyEnv.unify tyEnv (Type.subst tyEnv.subst e.typ) (Type.subst tyEnv.subst ty) in
            tyEnv
          with Not_found -> assert false (* already checked *) (* CR jfuruse: but we can have nicer error message here *))
          tyEnv used_fields
        in

        { desc = Record (List.map (fun (_l,p,tag,e) -> (p,tag,e)) used_fields);
          typ = Type.subst tyEnv.subst res_ty },
        tyEnv

  and of_case tyEnv0 ty retty (pattern, action) =
    let pattern, tyEnv = of_pattern tyEnv0 pattern in
    let _, tyEnv = 
      try TyEnv.unify tyEnv pattern.typ ty with
      | e ->
          Format.eprintf "@[<2>Pattern %a has type@ %a@ which is incompatible with the target type@ %a@]@."
            format_pattern pattern
            Type.format pattern.typ
            Type.format (Type.subst tyEnv.subst ty);
          raise e
    in
    let action, tyEnv = of_olf tyEnv action in
    let _, tyEnv = 
      try TyEnv.unify tyEnv action.typ retty with
      | e ->
          Format.eprintf "@[<2>Pattern action %a has type@ %a@ which is incompatible with the expected result type@ %a@]@."
            format action
            Type.format action.typ
            Type.format (Type.subst tyEnv.subst retty);
          raise e

    in
    (pattern, action), 
    tyEnv0 |> TyEnv.set_globals (TyEnv.globals tyEnv)
           |> TyEnv.set_subst tyEnv.subst
    
    let of_olf tyEnv l =
      try of_olf tyEnv l with
      | e -> 
          Format.eprintf "Ast.of_olf failed: %a@." O.format  l;
          raise e
end
  
module Top = struct

  type t = 
    | Let    of Expr.pattern * (Ident.t * Poly.t) list * Expr.t
    | Letrec of Ident.t * (Ident.t * Poly.t) list * Expr.t
    | Expr   of Expr.t * Poly.t
    | Open   of Path.t
    | Prim   of Ident.t * Poly.t (* must be closed ... *) * string list
    | Type   of Types.Decl.t list

  let sexp_of_t = function
    | Let (pat, _env, t1) ->
        List [ Atom "let"
  	   ; List [ Expr.sexp_of_pattern pat; Expr.sexp_of_t t1 ] ]
    | Letrec (v, _env, t1) ->
        List [ Atom "letrec"
  	   ; List [ Ident.sexp_of_t v; Expr.sexp_of_t t1 ] ]
    | Expr (e, _) -> Expr.sexp_of_t e
    | Open s -> List [ Atom "open"; Path.sexp_of_t s ]
    | Prim (id, ty, attrs) -> List ( Atom "prim" :: Ident.sexp_of_t id :: Poly.sexp_of_t ty :: List.map (fun s -> Atom s) attrs) 
    | Type decls -> List ( Atom "type" :: List.map Types.Decl.sexp_of_t decls ) 
  
  let of_string s = t_of_sexp (Sexplib.Sexp.of_string s)
  let format ppf t = Sexplib.Sexp.pp_hum ppf (sexp_of_t t)

  let load path =
    let ic = open_in path in
    let rec loop st =
      try
	let top = t_of_sexp (Sexplib.Sexp.input_sexp ic) in
	loop (top :: st)
      with
        | End_of_file -> 
          close_in ic;
          List.rev st
    in
    loop []
    
  let get_signature s tops = 
    let get_sigitem = function
      | Let (_, env, _) | Letrec (_, env, _) -> 
          List.map (fun (id, pty) -> Types.Value (id, Poly.subst s pty)) env
      | Expr _      -> []
      | Open _id    -> []
      | Prim (ident, pty, _attrs) -> [Types.Value (ident, Poly.subst s pty)]
      | Type decls -> [Types.Type decls]
    in
    let items = List.concat_map get_sigitem tops in
    (* we need filter out overridden sig items *)
    List.fold_right (fun item items ->
      match item with
      | Types.Value (id, _) -> 
          if 
            List.exists (function 
              | Types.Value (id', _) -> Ident.name id = Ident.name id'
              | Types.Type _ -> false) items
          then
            items
          else 
            item::items
      | Types.Type decls ->
          let ids = List.map (fun decl -> decl.Types.name) decls in
          let names = List.map Ident.name ids in
          if 
            List.exists (function
              | Types.Value _ -> false
              | Types.Type decls' ->
                  List.exists (fun decl -> List.mem (Ident.name (decl.Types.name)) names) decls') items
          then
            failwith "doubly defined type names"
          else item::items) items []

  let of_olf tyEnv0 = function
    | OT.Expr e -> 
        
        Types.incr_level ();
        let e, tyEnv = Expr.of_olf tyEnv0 e in
        Types.decr_level ();

        let pty = Poly.generalize (Type.subst tyEnv.subst e.typ) in

        tyEnv, Expr (e, pty)
  
    | OT.Let (pattern, e) -> 

        Types.incr_level ();

        let pattern, tyEnv = Expr.of_pattern tyEnv0 pattern in
        let e, tyEnv = Expr.of_olf tyEnv e in
        let _, tyEnv = 
          try TyEnv.unify tyEnv pattern.typ e.typ with
          | exn ->
              Format.eprintf "@[<2>Pattern %a has type@ %a which is incompatible with the definition type@ %a@]@."
                Expr.format_pattern pattern
                Type.format (Type.subst tyEnv.subst pattern.typ)
                Type.format e.typ;
                raise exn
        in

        Types.decr_level ();

        let bind_env = Expr.generalize_pattern tyEnv pattern in
        let env = List.map (fun (id,pty) -> (id,Path.of_ident id, Env.Value pty)) bind_env in
        let tyEnv = TyEnv.add_vars env tyEnv in

        tyEnv, Let (pattern, bind_env, e)
  
    | OT.Letrec (name, e) -> 

        let e, tyEnv = Expr.of_olf tyEnv0 (Olf.Expr.Letrec (name, e, Olf.Expr.Const (Const.Int 0))) in
        begin match e.desc with
        | Expr.Letrec (ident, bind_env, t, _) -> 
            let env = List.map (fun (id,pty) -> (id, Path.of_ident id, Env.Value pty)) bind_env in
            TyEnv.add_vars env tyEnv,
            Letrec (ident, bind_env, t)
        | _ -> assert false
        end
  
    | OT.Open path ->
        (* CR jfuruse: bug: open A; open B do not open A.B *)
        let path, desc, tyEnv = TyEnv.search (function Env.Module _ -> true | _ -> false) path tyEnv0 in
        begin match desc with
        | Env.Module (_sg, env) ->
(* Format.eprintf "OPEN: @[%a@]@." Env.format env; *)
            TyEnv.add_vars env.Env.vars tyEnv, Open path
        | _ -> failwith "not a module"
        end

    | OT.Prim (ident, pty, attrs) -> 
        let ident = Ident.create ident in
        let pty, env, _ = Ttypes.Poly.of_raw tyEnv0.env pty in
        let tyEnv = { tyEnv0 with env = env } in
        tyEnv |> TyEnv.add_vars [(ident, Path.of_ident ident, Env.Value pty)], 
        Prim (ident, pty, attrs)
  
    | OT.Type rdecls -> 
        let decls, env = Ttypes.Decl.of_raws tyEnv0.env rdecls in
        let tyEnv = { tyEnv0 with env = env } in
        let datatypes = List.map (fun decl -> 
          let path = Path.of_ident decl.name in
          decl.name, path, Env.Typedecl decl) decls
        in
        let constructors_accessors = List.flatten (List.rev_map Env.decl_pseudo_values decls) in
        tyEnv |> TyEnv.add_vars (datatypes @ constructors_accessors),
        Type decls
end