pgm_types.mli 4.32 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
(* model type symbols *)
11 12

type mtsymbol = private {
13 14 15 16 17
  mt_name   : ident;
  mt_args   : tvsymbol list;
  mt_model  : ty option;
  mt_abstr  : tysymbol;
  mt_mutable: bool;
18 19
}

20 21
val create_mtsymbol : 
  mut:bool -> preid -> tvsymbol list -> ty option -> mtsymbol
22 23 24

val mt_equal : mtsymbol -> mtsymbol -> bool

25
exception NotModelType
26 27

val get_mtsymbol : tysymbol -> mtsymbol
28
  (** raises [NotModelType] if [ts] is not a model type *)
29

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

33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54
(* record type symbols *)

type rt_field = private {
  rf_name   : ident;
  rf_region : tvsymbol option;
  rf_type   : ty;
}

type rtsymbol = private {
  rt_name   : ident;
  rt_args   : tvsymbol list;
  rt_abstr  : tysymbol;
  rt_fields : rt_field Mstr.t; 
}

val create_rtsymbol : 
  preid -> tvsymbol list -> (bool * preid * ty) list -> rtsymbol

val rt_equal : rtsymbol -> rtsymbol -> bool

(* builtin logic symbols for programs *)

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

58 59 60
val ts_exn : tysymbol
val ty_exn : ty

61 62
(* val ts_label : tysymbol *)

63
(* program types *)
64

65
module rec T : sig
66

67
  type pre = Term.fmla
68

69 70 71 72
  type post_fmla = Term.vsymbol (* result *) * Term.fmla
  type exn_post_fmla = Term.vsymbol (* result *) option * Term.fmla
      
  type esymbol = lsymbol
73

74 75 76 77 78
  type post = post_fmla * (esymbol * exn_post_fmla) list
      
  type type_v = private
  | Tpure    of ty
  | Tarrow   of pvsymbol list * type_c
79

80 81 82 83 84 85
  and type_c = { 
    c_result_type : type_v;
    c_effect      : E.t;
    c_pre         : pre;
    c_post        : post; 
  }
86

87 88 89 90 91 92
  and pvsymbol = private {
    pv_name : ident;
    pv_tv   : type_v;
    pv_ty   : ty;      (* as a logic type, for typing purposes only *)
    pv_vs   : vsymbol; (* for use in the logic *)
  }
93

94 95
  val tpure  : ty -> type_v
  val tarrow : pvsymbol list -> type_c -> type_v
96

97
  val create_pvsymbol : preid -> ?vs:vsymbol -> type_v -> pvsymbol
98

99
  (* program symbols *)
100

101 102 103 104 105 106 107 108
  type psymbol = private {
    p_name : ident;
    p_tv   : type_v;
    p_ty   : ty;      (* as a logic type, for typing purposes only *)
    p_ls   : lsymbol; (* for use in the logic *) 
  }
      
  val create_psymbol : preid -> type_v -> psymbol
109

110
  val p_equal : psymbol -> psymbol -> bool
111

112
  (* program types -> logic types *)
113

114 115 116 117 118 119 120 121
  val purify : ty -> ty
  val purify_type_v : ?logic:bool -> type_v -> ty
    (** when [logic] is [true], mutable types are turned into their models *)
    
  (* operations on program types *)
    
  val apply_type_v_var : type_v -> pvsymbol -> type_c
  val apply_type_v_sym : type_v -> psymbol  -> type_c
122
  val apply_type_v_ref : type_v -> R.t      -> type_c
123 124 125 126 127 128 129 130 131 132 133
    
  val occur_type_v : R.t -> type_v -> bool
    
  val v_result : ty -> vsymbol
  val exn_v_result : Why.Term.lsymbol -> Why.Term.vsymbol option
    
  val post_map : (fmla -> fmla) -> post -> post
    
  val subst1 : vsymbol -> term -> term Mvs.t
    
  val eq_type_v : type_v -> type_v -> bool
134

135
  (* pretty-printers *)
136

137 138
  val print_type_v : Format.formatter -> type_v -> unit
  val print_type_c : Format.formatter -> type_c -> unit
139
  val print_pre    : Format.formatter -> pre    -> unit
140
  val print_post   : Format.formatter -> post   -> unit
141

142 143
end 

144
and Spv :  sig include Set.S with type elt = T.pvsymbol end
145 146 147 148 149 150 151 152 153 154 155 156 157
and Mpv :  sig include Map.S with type key = T.pvsymbol end

(* references *)
and R : sig

  type t = 
    | Rlocal  of T.pvsymbol
    | Rglobal of T.psymbol

  val type_of : t -> ty

  val name_of : t -> ident

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

160 161 162 163 164 165 166
end 
and Sref : sig include Set.S with type elt = R.t end
and Mref : sig include Map.S with type key = R.t end
and Sexn : sig include Set.S with type elt = T.esymbol end

(* effects *)
and E : sig
167

168 169 170 171 172
  type t = private {
    reads  : Sref.t;
    writes : Sref.t;
    raises : Sexn.t;
  }
173

174
  val empty : t
175

176 177 178
  val add_read  : R.t -> t -> t
  val add_write : R.t -> t -> t
  val add_raise : T.esymbol -> t -> t
179

180 181
  val remove_reference : R.t -> t -> t    
  val filter : (R.t -> bool) -> t -> t
182

183
  val remove_raise : T.esymbol -> t -> t
184

185
  val union : t -> t -> t
186

187 188 189 190 191
  val equal : t -> t -> bool
    
  val no_side_effect : t -> bool
    
  val subst : R.t Mpv.t -> t -> t
192

193
  val occur : R.t -> t -> bool
194

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

197
end 
198

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
199
(* ghost code *)
200

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
201 202 203
val mt_ghost   : mtsymbol
val ps_ghost   : T.psymbol
val ps_unghost : T.psymbol