pgm_types.mli 5.58 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
(**************************************************************************)
(*                                                                        *)
(*  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.                  *)
(*                                                                        *)
(**************************************************************************)
19 20 21 22 23 24 25 26 27

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

28
(* program type symbols *)
29 30

type mtsymbol = private {
31 32 33 34 35
  mt_impure   : tysymbol;
  mt_effect   : tysymbol;
  mt_pure     : tysymbol;
  mt_regions  : int;
  mt_singleton: bool;
36 37
}

38 39 40
val create_mtsymbol :
  impure:tysymbol -> effect:tysymbol -> pure:tysymbol -> singleton:bool ->
  mtsymbol
41 42 43 44

val mt_equal : mtsymbol -> mtsymbol -> bool

val get_mtsymbol : tysymbol -> mtsymbol
45 46

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

48 49
val is_mutable_ts : tysymbol -> bool
val is_mutable_ty : ty       -> bool
50

51 52
val is_singleton_ts : tysymbol -> bool
val is_singleton_ty : ty       -> bool
53 54 55

(* builtin logic symbols for programs *)

56
val ts_arrow : tysymbol
57
val make_arrow_type : ty list -> ty -> ty
58

59 60 61
val ts_exn : tysymbol
val ty_exn : ty

62 63
(* val ts_label : tysymbol *)

64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84
(* regions *)
module R : sig

  type t = private {
    r_tv : tvsymbol;
    r_ty : Ty.ty;    (* effect type *)
  }

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

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

end

module Mreg : Stdlib.Map.S with type key = R.t

module Sreg : Mreg.Set

(* exception sets *)
module Sexn : Set.S with type elt = lsymbol

85
(* program types *)
86

87
module rec T : sig
88

89
  type pre = Term.term
90

91 92
  type post_fmla = Term.vsymbol (* result *) * Term.term
  type exn_post_fmla = Term.vsymbol (* result *) option * Term.term
93

94
  type esymbol = lsymbol
95

96
  type post = post_fmla * (esymbol * exn_post_fmla) list
97

98 99 100
  type type_v = private
  | Tpure    of ty
  | Tarrow   of pvsymbol list * type_c
101

102
  and type_c = {
103 104 105
    c_result_type : type_v;
    c_effect      : E.t;
    c_pre         : pre;
106
    c_post        : post;
107
  }
108

109
  and pvsymbol = private {
110 111
    pv_name   : ident;
    pv_tv     : type_v;
112
    pv_effect : vsymbol;
113 114
    pv_pure   : vsymbol;
    pv_regions: Sreg.t;
115
  }
116

117 118
  val tpure  : ty -> type_v
  val tarrow : pvsymbol list -> type_c -> type_v
119

120 121
  val create_pvsymbol :
    preid -> type_v ->
122
    effect:vsymbol -> pure:vsymbol -> regions:Sreg.t -> pvsymbol
123

124
  (* program symbols *)
125

126 127 128 129 130 131 132 133 134
  type psymbol_kind =
    | PSvar   of pvsymbol
    | PSfun   of type_v
    | PSlogic

  type psymbol = {
    ps_effect : lsymbol;
    ps_pure   : lsymbol;
    ps_kind   : psymbol_kind;
135
  }
136

137
  val create_psymbol:
138
    ?impure:lsymbol -> effect:lsymbol -> pure:lsymbol -> kind:psymbol_kind ->
139
    psymbol
140 141
  val create_psymbol_fun: preid -> type_v -> lsymbol * psymbol
  val create_psymbol_var: pvsymbol -> lsymbol * psymbol
142

143
  val get_psymbol: lsymbol -> psymbol
144 145 146

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

148
  (* program types -> logic types *)
149

150
  val purify : ty -> ty
151 152
  val effectify : ty -> ty

153
  val trans_type_v : ?effect:bool -> ?pure:bool -> type_v -> ty
154

155
  (* operations on program types *)
156

157
  val apply_type_v_var : type_v -> pvsymbol -> type_c
158 159

  val subst_type_v : ty Mtv.t -> term Mvs.t -> type_v -> type_v
160

161
  val occur_type_v : R.t -> type_v -> bool
162

163 164
  val v_result : ty -> vsymbol
  val exn_v_result : Why.Term.lsymbol -> Why.Term.vsymbol option
165

166
  val post_map : (term -> term) -> post -> post
167

168
  val subst1 : vsymbol -> term -> term Mvs.t
169

170
  val eq_type_v : type_v -> type_v -> bool
171

172
  (* pretty-printers *)
173

174 175
  val print_type_v : Format.formatter -> type_v -> unit
  val print_type_c : Format.formatter -> type_c -> unit
176
  val print_pre    : Format.formatter -> pre    -> unit
177
  val print_post   : Format.formatter -> post   -> unit
178
  val print_pvsymbol : Format.formatter -> pvsymbol -> unit
179

180
end
181

182
and Spv :  sig include Set.S with type elt = T.pvsymbol end
183 184 185 186
and Mpv :  sig include Map.S with type key = T.pvsymbol end

(* effects *)
and E : sig
187

188
  type t = private {
189 190
    reads  : Sreg.t;
    writes : Sreg.t;
191
    raises : Sexn.t;
192
    globals: Spv.t;
193
  }
194

195
  val empty : t
196

197
  val add_read  : R.t -> t -> t
198
  val add_glob  : T.pvsymbol -> t -> t
199 200
  val add_write : R.t -> t -> t
  val add_raise : T.esymbol -> t -> t
201

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
202
  val remove : Sreg.t -> t -> t
203
  val filter : (R.t -> bool) -> t -> t
204

205
  val remove_raise : T.esymbol -> t -> t
206

207
  val union : t -> t -> t
208

209
  val equal : t -> t -> bool
210

211
  val no_side_effect : t -> bool
212 213

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

215
  val occur : R.t -> t -> bool
216

217 218
  val print : Format.formatter -> t -> unit

219
end
220

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
221
(* ghost code *)
222
(****
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
223 224 225
val mt_ghost   : mtsymbol
val ps_ghost   : T.psymbol
val ps_unghost : T.psymbol
226
****)