expr.mli 8.13 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
MARCHE Claude's avatar
MARCHE Claude committed
4
(*  Copyright 2010-2017   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
10 11
(********************************************************************)

Andrei Paskevich's avatar
Andrei Paskevich committed
12
open Stdlib
13 14 15 16
open Ident
open Term
open Ity

17 18 19 20 21 22 23
(** {2 Routine symbols} *)

type rsymbol = private {
  rs_name  : ident;
  rs_cty   : cty;
  rs_logic : rs_logic;
  rs_field : pvsymbol option;
24 25
}

26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41
and rs_logic =
  | RLnone            (* non-pure symbol *)
  | RLpv of pvsymbol  (* local let-function *)
  | RLls of lsymbol   (* top-level let-function or let-predicate *)
  | RLlemma           (* top-level or local let-lemma *)

module Mrs : Extmap.S with type key = rsymbol
module Srs : Extset.S with module M = Mrs
module Hrs : Exthtbl.S with type key = rsymbol
module Wrs : Weakhtbl.S with type key = rsymbol

val rs_compare : rsymbol -> rsymbol -> int
val rs_equal : rsymbol -> rsymbol -> bool
val rs_hash : rsymbol -> int

type rs_kind =
42 43 44 45 46
  | RKnone    (* non-pure symbol *)
  | RKlocal   (* local let-function *)
  | RKfunc    (* top-level let-function *)
  | RKpred    (* top-level let-predicate *)
  | RKlemma   (* top-level or local let-lemma *)
47 48 49

val create_rsymbol : preid -> ?ghost:bool -> ?kind:rs_kind -> cty -> rsymbol
(** If [?kind] is supplied and is not [RKnone], then [cty]
50
    must have no effects except for resets which are ignored.
51
    If [?kind] is [RKnone] or [RKlemma], external mutable reads
52
    are allowed, otherwise [cty.cty_freeze.isb_reg] must be empty.
53 54 55
    If [?kind] is [RKlocal], the type variables in [cty] are frozen
    but regions are instantiable. If [?kind] is [RKpred] the result
    type must be [ity_bool]. If [?kind] is [RKlemma] and the result
56
    type is not [ity_unit], an existential premise is generated. *)
57

58 59 60
val create_constructor :
  constr:int -> preid -> itysymbol -> pvsymbol list -> rsymbol

Andrei Paskevich's avatar
Andrei Paskevich committed
61
val create_projection : itysymbol -> pvsymbol -> rsymbol
62

63 64
val restore_rs : lsymbol -> rsymbol
(** raises [Not_found] if the argument is not a [rs_logic] *)
Andrei Paskevich's avatar
Andrei Paskevich committed
65

66 67
val rs_ghost : rsymbol -> bool

Andrei Paskevich's avatar
Andrei Paskevich committed
68 69
(** {2 Program patterns} *)

70 71 72 73 74
type pat_ghost =
  | PGfail  (* refutable ghost subpattern before "|" *)
  | PGlast  (* refutable ghost subpattern otherwise  *)
  | PGnone  (* every ghost subpattern is irrefutable *)

Andrei Paskevich's avatar
Andrei Paskevich committed
75
type prog_pattern = private {
76 77 78 79
  pp_pat  : pattern;    (* pure pattern *)
  pp_ity  : ity;        (* type of the matched value *)
  pp_mask : mask;       (* mask of the matched value *)
  pp_fail : pat_ghost;  (* refutable ghost subpattern *)
Andrei Paskevich's avatar
Andrei Paskevich committed
80 81 82 83
}

type pre_pattern =
  | PPwild
84
  | PPvar of preid * bool
85
  | PPapp of rsymbol * pre_pattern list
86
  | PPas  of pre_pattern * preid * bool
Andrei Paskevich's avatar
Andrei Paskevich committed
87 88
  | PPor  of pre_pattern * pre_pattern

89
exception ConstructorExpected of rsymbol
Andrei Paskevich's avatar
Andrei Paskevich committed
90

Andrei Paskevich's avatar
Andrei Paskevich committed
91
val create_prog_pattern :
92
  pre_pattern -> ity -> mask -> pvsymbol Mstr.t * prog_pattern
Andrei Paskevich's avatar
Andrei Paskevich committed
93 94 95 96 97 98 99 100 101 102 103 104 105

(** {2 Program expressions} *)

type assertion_kind = Assert | Assume | Check

type for_direction = To | DownTo

type for_bounds = pvsymbol * for_direction * pvsymbol

type invariant = term

type variant = term * lsymbol option (** tau * (tau -> tau -> prop) *)

106
type assign = pvsymbol * rsymbol * pvsymbol (* region * field * value *)
107

Andrei Paskevich's avatar
Andrei Paskevich committed
108 109
type expr = private {
  e_node   : expr_node;
110
  e_ity    : ity;
111
  e_mask   : mask;
Andrei Paskevich's avatar
Andrei Paskevich committed
112 113 114 115 116
  e_effect : effect;
  e_label  : Slab.t;
  e_loc    : Loc.position option;
}

117
and expr_node =
Andrei Paskevich's avatar
Andrei Paskevich committed
118
  | Evar    of pvsymbol
119
  | Econst  of Number.constant
120
  | Eexec   of cexp * cty
121
  | Eassign of assign list
Andrei Paskevich's avatar
Andrei Paskevich committed
122 123 124
  | Elet    of let_defn * expr
  | Eif     of expr * expr * expr
  | Ecase   of expr * (prog_pattern * expr) list
Andrei Paskevich's avatar
Andrei Paskevich committed
125 126
  | Ewhile  of expr * invariant list * variant list * expr
  | Efor    of pvsymbol * for_bounds * invariant list * expr
127
  | Etry    of expr * (pvsymbol list * expr) Mxs.t
Andrei Paskevich's avatar
Andrei Paskevich committed
128 129
  | Eraise  of xsymbol * expr
  | Eassert of assertion_kind * term
130
  | Eghost  of expr
Andrei Paskevich's avatar
Andrei Paskevich committed
131
  | Epure   of term
Andrei Paskevich's avatar
Andrei Paskevich committed
132 133
  | Eabsurd

134 135 136
and cexp = private {
  c_node : cexp_node;
  c_cty  : cty;
Andrei Paskevich's avatar
Andrei Paskevich committed
137 138
}

139
and cexp_node =
140
  | Capp of rsymbol * pvsymbol list
141
  | Cpur of lsymbol * pvsymbol list
142 143 144 145 146 147 148 149
  | Cfun of expr
  | Cany

and let_defn = private
  | LDvar of pvsymbol * expr
  | LDsym of rsymbol * cexp
  | LDrec of rec_defn list

Andrei Paskevich's avatar
Andrei Paskevich committed
150
and rec_defn = private {
151 152
  rec_sym  : rsymbol; (* exported symbol *)
  rec_rsym : rsymbol; (* internal symbol *)
153
  rec_fun  : cexp;    (* necessary a Cfun *)
154
  rec_varl : variant list;
Andrei Paskevich's avatar
Andrei Paskevich committed
155 156
}

157
(** {2 Expressions} *)
158 159

val e_label : ?loc:Loc.position -> Slab.t -> expr -> expr
160
val e_label_push : ?loc:Loc.position -> Slab.t -> expr -> expr
161 162 163
val e_label_add : label -> expr -> expr
val e_label_copy : expr -> expr -> expr

164
(** {2 Definitions} *)
165

166 167
val let_var :
  preid -> ?ghost:bool -> expr -> let_defn * pvsymbol
Andrei Paskevich's avatar
Andrei Paskevich committed
168

169 170
val let_sym :
  preid -> ?ghost:bool -> ?kind:rs_kind -> cexp -> let_defn * rsymbol
171

172 173
val let_rec :
  (rsymbol * cexp * variant list * rs_kind) list -> let_defn * rec_defn list
Andrei Paskevich's avatar
Andrei Paskevich committed
174

175
val ls_decr_of_rec_defn : rec_defn -> lsymbol option
176 177 178
(* returns the dummy predicate symbol used in the precondition of
   the rec_rsym rsymbol to store the instantiated variant list *)

179
(** {2 Callable expressions} *)
180

181
val c_app : rsymbol -> pvsymbol list -> ity list -> ity -> cexp
182 183
val c_pur : lsymbol -> pvsymbol list -> ity list -> ity -> cexp

184
val c_fun : ?mask:mask -> pvsymbol list ->
185
  pre list -> post list -> post list Mxs.t -> pvsymbol Mpv.t -> expr -> cexp
186

187 188 189
val c_any : cty -> cexp

(** {2 Expression constructors} *)
190

191 192
val e_var : pvsymbol -> expr

193
val e_const : Number.constant -> ity -> expr
194 195 196 197 198
val e_nat_const : int -> expr

val e_exec : cexp -> expr

val e_app : rsymbol -> expr list -> ity list -> ity -> expr
199
val e_pur : lsymbol -> expr list -> ity list -> ity -> expr
200

Andrei Paskevich's avatar
Andrei Paskevich committed
201
val e_let : let_defn -> expr -> expr
202

203
exception FieldExpected of rsymbol
204

205
val e_assign : (expr * rsymbol * expr) list -> expr
206 207

val e_if : expr -> expr -> expr -> expr
208 209 210

val e_and : expr -> expr -> expr
val e_or  : expr -> expr -> expr
211
val e_not : expr -> expr
212 213

val e_true  : expr
214 215
val e_false : expr

216 217 218
val is_e_true  : expr -> bool
val is_e_false : expr -> bool

219 220
val e_raise : xsymbol -> expr -> ity -> expr

221
val e_try : expr -> (pvsymbol list * expr) Mxs.t -> expr
222 223 224

val e_case : expr -> (prog_pattern * expr) list -> expr

Andrei Paskevich's avatar
Andrei Paskevich committed
225
val e_while : expr -> invariant list -> variant list -> expr -> expr
226

227 228
val e_for : pvsymbol ->
  expr -> for_direction -> expr -> invariant list -> expr -> expr
229

230
val e_assert : assertion_kind -> term -> expr
231

232 233 234 235
val e_ghostify : bool -> expr -> expr

val e_pure : term -> expr

236 237
val e_absurd : ity -> expr

238
(** {2 Expression manipulation tools} *)
Andrei Paskevich's avatar
Andrei Paskevich committed
239

240 241 242 243 244 245
val e_fold : ('a -> expr -> 'a) -> 'a -> expr -> 'a
(** [e_fold] does not descend into Cfun *)

val e_locate_effect : (effect -> bool) -> expr -> Loc.position option
(** [e_locate_effect pr e] looks for a minimal sub-expression of
    [e] whose effect satisfies [pr] and returns its location *)
Andrei Paskevich's avatar
Andrei Paskevich committed
246

247 248
val proxy_label : label

249 250 251
val e_rs_subst : rsymbol Mrs.t -> expr -> expr
val c_rs_subst : rsymbol Mrs.t -> cexp -> cexp

252 253
val term_of_post : prop:bool -> vsymbol -> term -> (term * term) option

254 255
val term_of_expr : prop:bool -> expr -> term option
val post_of_expr : term -> expr -> term option
256

257 258 259
val e_ghost : expr -> bool
val c_ghost : cexp -> bool

260
(** {2 Built-in symbols} *)
Andrei Paskevich's avatar
Andrei Paskevich committed
261

262 263
val rs_true  : rsymbol
val rs_false : rsymbol
Andrei Paskevich's avatar
Andrei Paskevich committed
264

265
val rs_tuple : int -> rsymbol
Andrei Paskevich's avatar
Andrei Paskevich committed
266 267
val e_tuple : expr list -> expr

268
val rs_void : rsymbol
269
val fs_void : lsymbol
270
val e_void : expr
271
val t_void : term
272

273
val is_e_void : expr -> bool
274
val is_rs_tuple : rsymbol -> bool
Andrei Paskevich's avatar
Andrei Paskevich committed
275

276
val rs_func_app : rsymbol
277
val ld_func_app : let_defn
Andrei Paskevich's avatar
Andrei Paskevich committed
278 279
val e_func_app : expr -> expr -> expr
val e_func_app_l : expr -> expr list -> expr
Andrei Paskevich's avatar
Andrei Paskevich committed
280 281 282

(** {2 Pretty-printing} *)

283 284
val forget_rs  : rsymbol -> unit (* flush id_unique for a program symbol *)
val print_rs   : Format.formatter -> rsymbol -> unit  (* program symbol *)
Andrei Paskevich's avatar
Andrei Paskevich committed
285 286
val print_expr : Format.formatter -> expr -> unit     (* expression *)
val print_let_defn : Format.formatter -> let_defn -> unit