1. camlspotter
  2. olfend

Source

olfend / types.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
open Sexplib.Conv
open Spotlib.Spot

module R = Rawtype

(* They are mutual recursive so impossible to put them into the corresponding implementation modules. *)  
type typ = 
  | Var    of int (* id *) * int (* let level *)       (* lev 3 *)
  | Arrow  of typ * typ                                (* lev 1, rassoc *)
  | Tuple  of typ list                                 (* lev 2, noassoc: a * b * c <> (a * b) * c or a * (b * c) *)
  | Constr of Path.t * decl * typ list                 (* lev2, noassoc *)

and decl = {
  name   : Ident.t;
  params : int list;
  kind   : kind
}

and kind = 
  | Variant of (Ident.t * typ list) list
  | Record  of (Ident.t * typ) list
  | Alias   of typ
  | Abstract
  | Rec
 
and poly = Poly of int list *typ

and sigitem = 
  | Type of decl list
  | Value of Ident.t * poly
  (* | Module of signature *) (* no nested module yet *)

and signature = sigitem list

with sexp

module VarSet = Set.Make(struct 
  type t = typ 
  let compare x y = match x, y with
    | Var (id1, _),  Var (id2, _) -> compare id1 id2
    | _ -> assert false
end)

let current_level = ref 0

let with_level lev f = 
  let clev = !current_level in
  current_level := lev;
  let res = f () in
  current_level := clev;
  res 

let incr_level () = incr current_level
let decr_level () = decr current_level

let cntr = ref 0
let create_var = 
  fun () -> incr cntr; Var (!cntr, !current_level)

let reset () = 
  current_level := 0;
  cntr := 0

(** Type variable renaming *)

let renames s f xs = List.fold_right (fun x (s,xs) -> let s, x = f s x in s, x::xs) xs (s, [])

let rec rename_typ s = function
  | Arrow (t1, t2) -> 
      let s,t1 = rename_typ s t1 in
      let s,t2 = rename_typ s t2 in
      s, Arrow (t1, t2)
  | Tuple ts -> 
      let s,ts = rename_typs s ts in
      s, Tuple ts
  | Constr (p, decl, ts) -> 
      let s, desl = rename_decl s decl in
      let s, ts = rename_typs s ts in
      s, Constr (p, desl, ts)
  | Var (n,lev) -> 
      try s, Var (List.assoc n s, lev) with Not_found -> 
        let v = match create_var () with 
          | Var (v,_) -> v
          | _ -> assert false
        in
        let s = (n, v) :: s in
        s, Var (v, lev)

and rename_typs s ts = renames s rename_typ ts

and rename_params s params = 
  let s, params = rename_typs s (List.map (fun p -> Var (p, -1 (* dummy *))) params) in
  s, List.map (function (Var (n, _)) -> n | _ -> assert false) params

and rename_decl s decl = 
  let s, params = rename_params s decl.params in
  let s, kind = rename_kind s decl.kind in
  s, { decl with params; kind }

and rename_poly s (Poly (vars, ty)) =
  let s, vars = rename_params s vars in
  let s, ty = rename_typ s ty in
  s, Poly (vars, ty)

and rename_kind s = function
  | Variant id_tyargs_list ->
      let s, id_tyargs_list =
        List.fold_right (fun (id,typs) (s,id_typs_list) ->
          let s, typs = rename_typs s typs in
          s, (id,typs)::id_typs_list) id_tyargs_list (s,[])
      in
      s, Variant (id_tyargs_list)
  | Record idtyps -> 
      let ids = List.map fst idtyps in
      let typs = List.map snd idtyps in
      let s, typs = rename_typs s typs in
      s, Record (List.combine ids typs)
  | Alias ty -> 
      let s, ty = rename_typ s ty in
      s, Alias ty
  | Abstract -> s, Abstract
  | Rec -> s, Rec

and rename_sigitem s = function
  | Type decls -> 
      let s, decls = renames s rename_decl decls in
      s, Type decls
  | Value (id, pty) -> 
      let s, pty = rename_poly s pty in
      s, Value (id, pty)

and rename_signature s = renames s rename_sigitem

(** Valid only fully substituted types *)    
let rec localize_typ path = function
  | (Var _ as v) -> v
  | Arrow (t1, t2) -> Arrow (localize_typ path t1, localize_typ path t2)
  | Tuple ts -> Tuple (List.map (localize_typ path) ts)
  | Constr (p, decl, typs) -> 
      (* Data types have no object code, so no need of having id_pos_tbl *)
      Constr (Path.localize path [] p, localize_decl path decl, List.map (localize_typ path) typs)

and localize_decl path decl = 
  { name   = decl.name; (* it is kept *)
    params = decl.params;
    kind   = localize_kind path decl.kind }

and localize_kind path = function
  | Variant constrs -> Variant (List.map (fun (id, typs) -> id, List.map (localize_typ path) typs) constrs)
  | Record fields -> Record (List.map (fun (id, typ) -> id, localize_typ path typ) fields)
  | Alias typ -> Alias (localize_typ path typ)
  | Abstract -> Abstract
  | Rec -> Rec

module Type = struct
  (* type expression, or mono type *)
  type t = typ with sexp

  let create_var = create_var
  let create_name n env =
    let cand = function
      | 0 -> sprintf "'a%d" n
      | y -> sprintf "'a%d_%d" n y
    in
    let rec f y = 
      let cand_name = cand y in
      if List.exists (fun (_,name) -> cand_name = name) env then f (y+1)
      else cand_name
    in
    f 0
  
  let rec to_raw env = function
    | Var (n,_) -> 
        begin try R.Var (List.assoc n env), env with Not_found -> 
          let name = create_name n env in
          R.Var name, (n,name)::env
        end
    | Arrow (t1, t2) ->
        let t1, env = to_raw env t1 in
        let t2, env = to_raw env t2 in
        R.Arrow (t1, t2), env
    | Tuple ts ->
        let rev_ts, env = List.fold_left (fun (rev_ts,env) t -> 
          let t, env = to_raw env t in t::rev_ts, env) ([],env) ts in
        R.Tuple (List.rev rev_ts), env
    | Constr (p, _desc, ts) ->
        let rev_ts, env = List.fold_left (fun (rev_ts,env) t -> 
          let t, env = to_raw env t in t::rev_ts, env) ([],env) ts in
        R.Constr (Path.name p, List.rev rev_ts), env
 
  let rec ppr = 
    let open Treeprint.Printer in 
    let open Treeprint.Printer.OCaml in 
    function
      | Var (n,lev) when lev < 0 -> string (Printf.sprintf "'a%d" n)
      | Var (n,lev) -> string (Printf.sprintf "'a%d_%d" n lev)
      | Arrow (t1, t2) -> ppr t1 ^-> ppr t2
      | Tuple ts -> list 1.0 (space ++ string "*" ++ space) (List.map ppr ts)
      | Constr (name, _, []) -> string (Path.name name)
      | Constr (name, _, ts) -> list 2.0 space (string (Path.name name):: List.map ppr ts)

  include Treeprint.Printer.MakeDrivers(struct type t = typ let ppr = ppr end)

  let rec vars t = 
    let open VarSet in
    match t with
    | Var _ -> one t
    | Arrow (t1, t2) -> vars t1 + vars t2
    | Tuple ts | Constr (_, _, ts) -> unions (List.map vars ts)
  
  let rec occur v = function
    | Var (n,_) -> v = n
    | Arrow (t1, t2) -> occur v t1 || occur v t2
    | Tuple ts | Constr (_, _, ts) -> List.exists (occur v) ts
  
  let rec subst s = function
    | Arrow (t1, t2) -> Arrow (subst s t1, subst s t2)
    | Tuple ts -> Tuple (List.map (subst s) ts)
    | Constr (p, desc, ts) -> Constr (p, desc, List.map (subst s) ts)
    | (Var (n,_) as t) -> try subst s (List.assoc n s) with Not_found -> t
  
  let arity sub ty =
    let ty = subst sub ty in
    let rec count st = function
      | Arrow (t, t2) -> count (t::st) t2
      | ty -> st, ty
    in
    let rev_argtys, retty = count [] ty in
    List.length rev_argtys, List.rev rev_argtys, retty

  let rec create_arrows tyargs retty = match tyargs with
    | [] -> retty
    | x::xs -> Arrow (x, create_arrows xs retty)

  let rec fix_level f = function
    | Var (n,lev) -> Var (n, f lev)
    | Arrow (t1, t2) -> Arrow (fix_level f t1, fix_level f t2)
    | Tuple ts -> Tuple (List.map (fix_level f) ts)
    | Constr (p1, desc, ts1) -> 
        (* suppose desc is closed *)
        Constr (p1, desc, List.map (fix_level f) ts1)

  let rec unify sub t1 t2 = 
    let t1 = subst sub t1 in
    let t2 = subst sub t2 in
    if t1 = t2 then t1, sub
    else match t1, t2 with
    | Var (n, lev), _ -> 
        if occur n t2 then failwith "occur check"
        else 
          let t2_fixed = fix_level (min lev) t2 in
          t2_fixed, ( n, t2_fixed ) :: sub
    | _, Var _ -> unify sub t2 t1
    | Arrow (t11, t12), Arrow (t21, t22) ->
        let t1, sub = unify sub t11 t21 in
        let t2, sub = unify sub t12 t22 in
        Arrow (subst sub t1, subst sub t2) , sub
    | Tuple ts1, Tuple ts2 ->
        let ts, sub = unifies sub ts1 ts2 in
        Tuple ts, sub
    | Constr (p1, desc, ts1), Constr (p2, _, ts2) when p1 = p2 ->
        let ts, sub = unifies sub ts1 ts2 in
        Constr (p1, desc, ts), sub
    | _ -> failwith "head"
  
  and unifies sub ts1 ts2 =
    if List.length ts1 = List.length ts2 then
      let _, sub = 
        List.fold_left (fun (ts, sub) (t, t') ->
          let t, sub = unify sub t t' in
          t::ts, sub) ([], sub) (List.combine ts1 ts2)
      in
      List.map (subst sub) ts1, sub 
    else failwith "unifies"
  
  let free_vars (qs, t) =
    let open VarSet in
    vars t - of_list qs

  let insts vars ts =
    let sub = List.map (fun v -> v, create_var ()) vars in
    sub, List.map (subst sub) ts

  let inst vars t = match insts vars [t] with
    | sub, [t] -> sub, t
    | _ -> assert false

  let rename = rename_typ
  let localize = localize_typ
end

module Poly = struct

  (* type scheme, or poly type *)
  type t = poly with sexp

  let of_type t = Poly ([], t)

  let to_raw env (Poly (rvars, t)) = 
    let rev_vars, env = List.fold_left (fun (rev_vars, env) v ->
      let var = Type.create_name v env in
      let env = (v,var)::env in
      var::rev_vars, env) ([],env) rvars 
    in
    let vars = List.rev rev_vars in
    let t, env = Type.to_raw env t in 
    R.Poly.Poly (vars, t), env
  
  let ppr (Poly (vars, ty)) = 
    let open Treeprint.Printer in 
    match vars with
    | [] -> Type.ppr ty
    | _ -> list 0.9 space [string "forall"; 
                           list 1.0 space (List.map (fun v -> string (sprintf "'a%d" v)) vars) ; 
                           string "."; Type.ppr ty]

  include Treeprint.Printer.MakeDrivers(struct type t = poly let ppr = ppr end)

  let subst s (Poly (vars, t)) =
    let alpha = with_level (-1) & fun () -> List.map (fun v -> v, Type.create_var ()) vars in
    let vars = List.map (function (_, Var (v,_)) -> v | _ -> assert false) alpha in
    let t = Type.subst alpha t in
    let t = Type.subst s t in
    Poly (vars, t)
  
  let inst (Poly (vars, t)) = Type.inst vars t

  let arity sub = function
    | Poly (_, ty) -> Type.arity sub ty

  let vars (Poly (params, ty)) = 
    VarSet.union (VarSet.of_list (List.map (fun n -> Var (n,-1)) params)) (Type.vars ty)

  let free_vars (Poly (params, ty)) = Type.free_vars (List.map (fun n -> Var (n,-1)) params, ty)

  let rename s (Poly (params, ty)) = 
    let s, params = rename_params s params in
    let s, ty = rename_typ s ty in
    s, Poly (params, ty)

  (** Types must be fully substituted, otherwise the result is wrong *)      
  let generalize ty = 
    let rec gen = function
      | Var (n, lev) when lev > !current_level -> Var (n, -1)
      | (Var _ as v) -> v
      | Arrow (t1, t2) -> Arrow (gen t1, gen t2)
      | Tuple ts -> Tuple (List.map gen ts)
      | Constr (p, decl, ts) -> Constr (p, decl, List.map gen ts)
    in
    let ty = gen ty in
    let params = List.filter_map (function
      | Var (n, -1) -> Some n
      | _ -> None) 
      & VarSet.to_list & Type.vars ty 
    in
    Poly (params, ty)

   let localize path (Poly (params, ty)) = Poly (params, Type.localize path ty)
end
  
module Decl = struct
  module R = Rawtype.Decl

  type t = decl with sexp
  
  let inst decl = 
    let sub, _ = Type.insts decl.params [] in
    List.map (Type.subst sub) (List.map (fun x -> Var (x,-1)) decl.params),
    match decl.kind with
    | Alias ty -> Alias (Type.subst sub ty)
    | Variant constrs -> Variant (List.map (fun (c, typs) -> c, List.map (Type.subst sub) typs) constrs)
    | Record fields -> Record (List.map (fun (f, typ) -> f, Type.subst sub typ) fields)
    | Abstract -> Abstract
    | Rec -> Rec

  let rename = rename_decl
  let localize = localize_decl

  module Ppr = struct
    open Treeprint.Printer
    let ppr_kind = function
      | Variant constrs ->
          list 0.3 (* CR jfuruse *) (space ++ cut ++ string "| ")
            (List.map (fun (id, typs) -> match typs with
              | [] -> Ident.ppr id
              | _ -> Ident.ppr id ++ string " of " ++ list 2.0 space (List.map Type.ppr typs)) constrs)
      | Record fields -> 
          reset (box 0 (string "{ " 
                 ++ box 0 (list 1.0 (string "; " ++ cut) 
                             (List.map (fun (id, typ) -> Ident.ppr id ++ string " : " ++ Type.ppr typ) fields))
                 ++ string " }"))
      | Alias typ -> Type.ppr typ
      | Abstract -> nop
      | Rec -> string "*REC*"


    let ppr decl = match decl.params with
      | [] -> 
          Ident.ppr decl.name ++ space ++ box 0 (string "=" ++ space ++ cut ++ ppr_kind decl.kind)
      | params -> 
          list 0.2 (* CR jfuruse *) space ( Ident.ppr decl.name :: List.map (fun v -> Type.ppr (Var (v,-1))) params)
          ++ space
          ++ box 0 (string "=" ++ space ++ cut ++ ppr_kind decl.kind)

    include MakeDrivers(struct type t = decl let ppr = ppr end)
    module Kind = MakeDrivers(struct type t = kind let ppr = ppr_kind end)
  end

  include Ppr

end