pgm_types.mli 4.22 KB
Newer Older
1 2 3 4 5 6 7 8 9

open Why
open Util
open Ident
open Ty
open Theory
open Term
open Decl

10
(* program type symbols *)
11 12

type mtsymbol = private {
13 14 15 16 17
  mt_impure   : tysymbol;
  mt_effect   : tysymbol;
  mt_pure     : tysymbol;
  mt_regions  : int;
  mt_singleton: bool;
18 19
}

20 21 22
val create_mtsymbol :
  impure:tysymbol -> effect:tysymbol -> pure:tysymbol -> singleton:bool ->
  mtsymbol
23 24 25 26

val mt_equal : mtsymbol -> mtsymbol -> bool

val get_mtsymbol : tysymbol -> mtsymbol
27 28

val print_mt_symbol : Format.formatter -> mtsymbol -> unit
29

30 31
val is_mutable_ts : tysymbol -> bool
val is_mutable_ty : ty       -> bool
32

33 34
val is_singleton_ts : tysymbol -> bool
val is_singleton_ty : ty       -> bool
35 36 37

(* builtin logic symbols for programs *)

38
val ts_arrow : tysymbol
39
val make_arrow_type : ty list -> ty -> ty
40

41 42 43
val ts_exn : tysymbol
val ty_exn : ty

44 45
(* val ts_label : tysymbol *)

46
(* program types *)
47

48
module rec T : sig
49

50
  type pre = Term.fmla
51

52 53
  type post_fmla = Term.vsymbol (* result *) * Term.fmla
  type exn_post_fmla = Term.vsymbol (* result *) option * Term.fmla
54

55
  type esymbol = lsymbol
56

57
  type post = post_fmla * (esymbol * exn_post_fmla) list
58

59 60 61
  type type_v = private
  | Tpure    of ty
  | Tarrow   of pvsymbol list * type_c
62

63
  and type_c = {
64 65 66
    c_result_type : type_v;
    c_effect      : E.t;
    c_pre         : pre;
67
    c_post        : post;
68
  }
69

70
  and pvsymbol = private {
71 72 73 74 75
    pv_name   : ident;
    pv_tv     : type_v;
    pv_effect : vsymbol; 
    pv_pure   : vsymbol;
    pv_regions: Sreg.t;
76
  }
77

78 79
  val tpure  : ty -> type_v
  val tarrow : pvsymbol list -> type_c -> type_v
80

81 82 83
  val create_pvsymbol : 
    preid -> type_v -> 
    effect:vsymbol -> pure:vsymbol -> regions:Sreg.t -> pvsymbol
84

85
  (* program symbols *)
86

87
  type psymbol_fun = private {
88 89 90
    p_name : ident;
    p_tv   : type_v;
    p_ty   : ty;      (* as a logic type, for typing purposes only *)
91
    p_ls   : lsymbol; (* for use in the logic *)
92
  }
93

94 95 96 97 98 99 100 101
  type psymbol =
    | PSvar of pvsymbol
    | PSfun of psymbol_fun

  val create_psymbol_fun : preid -> type_v -> psymbol_fun

  val ps_name : psymbol -> ident
  val ps_equal : psymbol -> psymbol -> bool
102

103
  (* program types -> logic types *)
104

105
  val purify : ty -> ty
106 107
  val effectify : ty -> ty

108 109
  val purify_type_v : ?logic:bool -> type_v -> ty
    (** when [logic] is [true], mutable types are turned into their models *)
110

111
  (* operations on program types *)
112

113
  val apply_type_v_var : type_v -> pvsymbol -> type_c
114 115 116
(*   val apply_type_v_sym : type_v -> psymbol  -> type_c *)
(*   val apply_type_v_ref : type_v -> R.t      -> type_c *)

117
  val occur_type_v : R.t -> type_v -> bool
118

119 120
  val v_result : ty -> vsymbol
  val exn_v_result : Why.Term.lsymbol -> Why.Term.vsymbol option
121

122
  val post_map : (fmla -> fmla) -> post -> post
123

124
  val subst1 : vsymbol -> term -> term Mvs.t
125

126
  val eq_type_v : type_v -> type_v -> bool
127

128
  (* pretty-printers *)
129

130 131
  val print_type_v : Format.formatter -> type_v -> unit
  val print_type_c : Format.formatter -> type_c -> unit
132
  val print_pre    : Format.formatter -> pre    -> unit
133
  val print_post   : Format.formatter -> post   -> unit
134
  val print_pvsymbol : Format.formatter -> pvsymbol -> unit
135

136
end
137

138
and Spv :  sig include Set.S with type elt = T.pvsymbol end
139 140
and Mpv :  sig include Map.S with type key = T.pvsymbol end

141
(* regions *)
142 143
and R : sig

144 145 146 147
  type t = private {
    r_tv : tvsymbol;
    r_ty : Ty.ty;
  }
148

149
  val create : tvsymbol -> Ty.ty -> t
150

151 152
  val print : Format.formatter -> t -> unit

153 154 155
end
and Sreg : sig include Set.S with type elt = R.t end
and Mreg : sig include Map.S with type key = R.t end
156 157 158 159
and Sexn : sig include Set.S with type elt = T.esymbol end

(* effects *)
and E : sig
160

161
  type t = private {
162 163
    reads  : Sreg.t;
    writes : Sreg.t;
164
    raises : Sexn.t;
165
    globals: Spv.t;
166
  }
167

168
  val empty : t
169

170
  val add_read  : R.t -> t -> t
171
  val add_glob  : T.pvsymbol -> t -> t
172 173
  val add_write : R.t -> t -> t
  val add_raise : T.esymbol -> t -> t
174

175
  val remove_reference : R.t -> t -> t
176
  val filter : (R.t -> bool) -> t -> t
177

178
  val remove_raise : T.esymbol -> t -> t
179

180
  val union : t -> t -> t
181

182
  val equal : t -> t -> bool
183

184
  val no_side_effect : t -> bool
185 186

  val subst : Ty.ty Mtv.t -> t -> t
187

188
  val occur : R.t -> t -> bool
189

190 191
  val print : Format.formatter -> t -> unit

192
end
193

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
194
(* ghost code *)
195
(****
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
196 197 198
val mt_ghost   : mtsymbol
val ps_ghost   : T.psymbol
val ps_unghost : T.psymbol
199
****)