mlw_ty.ml 12.1 KB
Newer Older
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
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-2011                                               *)
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

open Why3
open Util
open Ident
open Ty

(** region variables *)

type rvsymbol = {
  rv_name : ident;
}

module Rvar = WeakStructMake (struct
  type t = rvsymbol
  let tag rv = rv.rv_name.id_tag
end)

module Srv = Rvar.S
module Mrv = Rvar.M
module Hrv = Rvar.H
module Wrv = Rvar.W

let rv_equal : rvsymbol -> rvsymbol -> bool = (==)

let rv_hash rv = id_hash rv.rv_name

let create_rvsymbol n = { rv_name = id_register n }

(** subregion projections *)

type srsymbol = {
  srs_name : ident;
}

let srs_equal : srsymbol -> srsymbol -> bool = (==)

let srs_hash srs = id_hash srs.srs_name

let create_srsymbol n = { srs_name = id_register n }

(** regions *)

type region = {
  reg_node : reg_node;
  reg_tag  : Hashweak.tag;
}

and reg_node =
  | Rvar of rvsymbol
  | Rsub of srsymbol * region

let reg_equal : region -> region -> bool = (==)

let reg_hash r = Hashweak.tag_hash r.reg_tag

module Hregion = Hashcons.Make (struct
  type t = region

  let equal r1 r2 = match r1.reg_node, r2.reg_node with
    | Rvar n1, Rvar n2 -> rv_equal n1 n2
    | Rsub (s1,r1), Rsub (s2,r2) ->
        srs_equal s1 s2 && reg_equal r1 r2
    | _ -> false

  let hash r = match r.reg_node with
    | Rvar v -> rv_hash v
    | Rsub (s,r) -> Hashcons.combine (srs_hash s) (reg_hash r)

  let tag n r = { r with reg_tag = Hashweak.create_tag n }
end)

module Reg = WeakStructMake (struct
  type t = region
  let tag r = r.reg_tag
end)

module Sreg = Reg.S
module Mreg = Reg.M
module Hreg = Reg.H
module Wreg = Reg.W

let mk_reg n = {
  reg_node = n;
  reg_tag  = Hashweak.dummy_tag;
}

let reg_var n = Hregion.hashcons (mk_reg (Rvar n))
let reg_sub s r = Hregion.hashcons (mk_reg (Rsub (s,r)))

let rec reg_getrv r = match r.reg_node with
  | Rvar v -> v
  | Rsub (_,r) -> reg_getrv r

let rec reg_v_map fn r = match r.reg_node with
  | Rvar v -> fn v
  | Rsub (s,r) -> reg_sub s (reg_v_map fn r)

let reg_full_inst m r = reg_v_map (fun v -> Mrv.find v m) r

(** value types (w/o effects) *)

type vtysymbol = {
  vts_pure  : tysymbol;
  vts_args  : tvsymbol list;
  vts_regs  : rvsymbol list;
  vts_def   : vty option;
  vts_model : bool;
}

and vty = {
  vty_node : vty_node;
  vty_tag  : Hashweak.tag;
}

and vty_node =
  | Vtyvar of tvsymbol
  | Vtypur of tysymbol * vty list
  | Vtyapp of vtysymbol * vty list * region list

module VTsym = WeakStructMake (struct
  type t = vtysymbol
  let tag vts = vts.vts_pure.ts_name.id_tag
end)

module Svts = VTsym.S
module Mvts = VTsym.M
module Hvts = VTsym.H
module Wvts = VTsym.W

let vts_equal : vtysymbol -> vtysymbol -> bool = (==)
let vty_equal : vty       -> vty       -> bool = (==)

let vts_hash vts = id_hash vts.vts_pure.ts_name
let vty_hash vty = Hashweak.tag_hash vty.vty_tag

module Hsvty = Hashcons.Make (struct
  type t = vty

  let equal vty1 vty2 = match vty1.vty_node, vty2.vty_node with
    | Vtyvar n1, Vtyvar n2 -> tv_equal n1 n2
    | Vtypur (s1,l1), Vtypur (s2,l2) ->
        ts_equal s1 s2 && List.for_all2 vty_equal l1 l2
    | Vtyapp (s1,l1,r1), Vtyapp (s2,l2,r2) ->
        vts_equal s1 s2 && List.for_all2 vty_equal l1 l2
          && List.for_all2 reg_equal r1 r2
    | _ -> false

  let hash vty = match vty.vty_node with
    | Vtyvar v -> tv_hash v
    | Vtypur (s,tl) -> Hashcons.combine_list vty_hash (ts_hash s) tl
    | Vtyapp (s,tl,rl) ->
        Hashcons.combine_list reg_hash
          (Hashcons.combine_list vty_hash (vts_hash s) tl) rl

  let tag n vty = { vty with vty_tag = Hashweak.create_tag n }
end)

module Vty = WeakStructMake (struct
  type t = vty
  let tag vty = vty.vty_tag
end)

module Svty = Vty.S
module Mvty = Vty.M
module Hvty = Vty.H
module Wvty = Vty.W

let mk_vty n = {
  vty_node = n;
  vty_tag  = Hashweak.dummy_tag;
}

let vty_var n = Hsvty.hashcons (mk_vty (Vtyvar n))
let vty_pur s tl = Hsvty.hashcons (mk_vty (Vtypur (s,tl)))
let vty_app s tl rl = Hsvty.hashcons (mk_vty (Vtyapp (s,tl,rl)))

(* generic traversal functions *)

let vty_map fn vty = match vty.vty_node with
  | Vtyvar _ -> vty
  | Vtypur (f,tl) -> vty_pur f (List.map fn tl)
  | Vtyapp (f,tl,rl) -> vty_app f (List.map fn tl) rl

let vty_fold fn acc vty = match vty.vty_node with
  | Vtyvar _ -> acc
  | Vtypur (_,tl)
  | Vtyapp (_,tl,_) -> List.fold_left fn acc tl

let vty_all pr vty =
  try vty_fold (all_fn pr) true vty with FoldSkip -> false

let vty_any pr vty =
  try vty_fold (any_fn pr) false vty with FoldSkip -> true

(* traversal functions on type variables and regions *)

let rec vty_v_map fnv fnr vty = match vty.vty_node with
  | Vtyvar v ->
      fnv v
  | Vtypur (f,tl) ->
      vty_pur f (List.map (vty_v_map fnv fnr) tl)
  | Vtyapp (f,tl,rl) ->
      vty_app f (List.map (vty_v_map fnv fnr) tl) (List.map fnr rl)

let rec vty_v_fold fnv fnr acc vty = match vty.vty_node with
  | Vtyvar v ->
      fnv acc v
  | Vtypur (_,tl) ->
      List.fold_left (vty_v_fold fnv fnr) acc tl
  | Vtyapp (_,tl,rl) ->
      List.fold_left (vty_v_fold fnv fnr) (List.fold_left fnr acc rl) tl

let vty_v_all prv prr vty =
  try vty_v_fold (all_fn prv) (all_fn prr) true vty with FoldSkip -> false

let vty_v_any prv prr vty =
  try vty_v_fold (any_fn prv) (any_fn prr) false vty with FoldSkip -> true

let vty_full_inst mv mr vty =
  vty_v_map (fun v -> Mtv.find v mv) (reg_full_inst mr) vty

let vty_freevars s vty = vty_v_fold (fun s v -> Stv.add v s) Util.const s vty

let vty_closed vty = vty_v_all Util.ffalse Util.ttrue vty
let vty_pure vty = vty_v_all Util.ttrue Util.ffalse vty

(* smart constructors *)

exception BadVtyArity of vtysymbol * int * int
exception BadRegArity of vtysymbol * int * int

exception DuplicateRegVar of rvsymbol
exception UnboundRegVar of rvsymbol
exception InvalidRegion of region

let rec ty_of_vty vty = match vty.vty_node with
  | Vtyvar v -> ty_var v
  | Vtypur (s,tl) -> ty_app s (List.map ty_of_vty tl)
  | Vtyapp (s,tl,_) -> ty_app s.vts_pure (List.map ty_of_vty tl)

let rec vty_of_ty ty = match ty.ty_node with
  | Tyvar v -> vty_var v
  | Tyapp (s,tl) -> vty_pur s (List.map vty_of_ty tl)

Andrei Paskevich's avatar
Andrei Paskevich committed
263
let rec vty_app_real s tl rl model =
264
265
266
267
268
269
  let tll = List.length tl in
  let rll = List.length rl in
  let stl = List.length s.vts_args in
  let srl = List.length s.vts_regs in
  if tll <> stl then raise (BadVtyArity (s,stl,tll));
  if rll <> srl then raise (BadRegArity (s,srl,rll));
Andrei Paskevich's avatar
Andrei Paskevich committed
270
271
  let expand = not s.vts_model || model in
  let subexp = not s.vts_model && model in
272
  match s.vts_def with
Andrei Paskevich's avatar
Andrei Paskevich committed
273
  | Some vty when expand ->
274
275
276
277
      let add m v t = Mtv.add v t m in
      let mv = List.fold_left2 add Mtv.empty s.vts_args tl in
      let add m v r = Mrv.add v r m in
      let mr = List.fold_left2 add Mrv.empty s.vts_regs rl in
Andrei Paskevich's avatar
Andrei Paskevich committed
278
279
      (* if s is a model alias, vty is already expanded *)
      let vty = if subexp then vty_model vty else vty in
280
      vty_full_inst mv mr vty
Andrei Paskevich's avatar
Andrei Paskevich committed
281
282
283
284
285
  | None when expand && rll = 0 ->
      (* if a pure non-model vts is an alias, the RHS can contain
         pure model alias types, so we cannot replace vts with ts *)
      (* also, model types should never be replaced with pure types *)
      vty_pur s.vts_pure tl
286
287
288
  | _ ->
      vty_app s tl rl

Andrei Paskevich's avatar
Andrei Paskevich committed
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
and vty_model vty = match vty.vty_node with
  | Vtyvar _ -> vty
  | Vtypur (s,tl) -> vty_pur s (List.map vty_model tl)
  | Vtyapp (s,tl,rl) -> vty_app_real s (List.map vty_model tl) rl true

let vty_pur s tl = match s.ts_def with
  | Some ty ->
      let add m v t = Mtv.add v t m in
      let m = List.fold_left2 add Mtv.empty s.ts_args tl in
      vty_full_inst m Mrv.empty (vty_of_ty ty)
  | None ->
      vty_pur s tl

let vty_app s tl rl = vty_app_real s tl rl false
let vty_app_model s tl rl = vty_app_real s tl rl true

let create_vtysymbol name args regs def model =
  let puredef = option_map ty_of_vty def in
  let purets = create_tysymbol name args puredef in
  let add s v = Srv.add_new v (DuplicateRegVar v) s in
  let s = List.fold_left add Srv.empty regs in
  let check r = match r.reg_node with
    | Rvar v -> Srv.mem v s || raise (UnboundRegVar v)
    | _ -> raise (InvalidRegion r) in
  ignore (option_map (vty_v_all Util.ttrue check) def);
  (* if a type is a model alias, expand everything on the RHS *)
  let def = if model then option_map vty_model def else def in
  { vts_pure  = purets;
    vts_args  = args;
    vts_regs  = regs;
    vts_def   = def;
    vts_model = model; }
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

(*
(* symbol-wise map/fold *)

let rec ty_s_map fn ty = match ty.ty_node with
  | Tyvar _ -> ty
  | Tyapp (f, tl) -> ty_app (fn f) (List.map (ty_s_map fn) tl)

let rec ty_s_fold fn acc ty = match ty.ty_node with
  | Tyvar _ -> acc
  | Tyapp (f, tl) -> List.fold_left (ty_s_fold fn) (fn acc f) tl

let ty_s_all pr ty =
  try ty_s_fold (all_fn pr) true ty with FoldSkip -> false

let ty_s_any pr ty =
  try ty_s_fold (any_fn pr) false ty with FoldSkip -> true

(* type matching *)

let rec ty_inst s ty = match ty.ty_node with
  | Tyvar n -> Mrv.find_default n ty s
  | _ -> ty_map (ty_inst s) ty

let rec ty_match s ty1 ty2 =
  let set = function
    | None -> Some ty2
    | Some ty1 as r when ty_equal ty1 ty2 -> r
    | _ -> raise Exit
  in
  match ty1.ty_node, ty2.ty_node with
    | Tyapp (f1,l1), Tyapp (f2,l2) when ts_equal f1 f2 ->
        List.fold_left2 ty_match s l1 l2
    | Tyvar n1, _ -> Mrv.change n1 set s
    | _ -> raise Exit

exception TypeMismatch of ty * ty

let ty_match s ty1 ty2 =
  try ty_match s ty1 ty2
  with Exit -> raise (TypeMismatch (ty_inst s ty1, ty2))

(* built-in symbols *)

let ts_int  = create_tysymbol (id_fresh "int")  [] None
let ts_real = create_tysymbol (id_fresh "real") [] None

let ty_int  = ty_app ts_int  []
let ty_real = ty_app ts_real []

let ts_func =
  let rv_a = create_rvsymbol (id_fresh "a") in
  let rv_b = create_rvsymbol (id_fresh "b") in
  create_tysymbol (id_fresh "func") [rv_a;rv_b] None

let ts_pred =
  let rv_a = create_rvsymbol (id_fresh "a") in
  create_tysymbol (id_fresh "pred") [rv_a] None

let ty_func ty_a ty_b = ty_app ts_func [ty_a;ty_b]
let ty_pred ty_a = ty_app ts_pred [ty_a]

let ts_tuple_ids = Hid.create 17

let ts_tuple = Util.memo_int 17 (fun n ->
  let vl = ref [] in
  for i = 1 to n do vl := create_rvsymbol (id_fresh "a") :: !vl done;
  let ts = create_tysymbol (id_fresh ("tuple" ^ string_of_int n)) !vl None in
  Hid.add ts_tuple_ids ts.ts_name n;
  ts)

let ty_tuple tyl = ty_app (ts_tuple (List.length tyl)) tyl

let is_ts_tuple ts = ts_equal ts (ts_tuple (List.length ts.ts_args))

let is_ts_tuple_id id =
  try Some (Hid.find ts_tuple_ids id) with Not_found -> None

(** {2 Operations on [ty option]} *)

exception UnexpectedProp

let oty_type = function Some ty -> ty | None -> raise UnexpectedProp

let oty_equal = Util.option_eq ty_equal
let oty_hash = Util.option_apply 1 ty_hash

let oty_match m o1 o2 = match o1,o2 with
  | Some ty1, Some ty2 -> ty_match m ty1 ty2
  | None, None -> m
  | _ -> raise UnexpectedProp

let oty_inst m = Util.option_map (ty_inst m)
let oty_freevars = Util.option_fold ty_freevars
let oty_cons = Util.option_fold (fun tl t -> t::tl)

let ty_equal_check ty1 ty2 =
  if not (ty_equal ty1 ty2) then raise (TypeMismatch (ty1, ty2))
*)