Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

mlw_expr.mli 7.45 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
MARCHE Claude's avatar
MARCHE Claude committed
3
(*  Copyright (C) 2010-2012                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
MARCHE Claude's avatar
MARCHE Claude committed
7
(*    Guillaume Melquiond                                                 *)
8 9 10 11 12 13 14 15 16 17 18 19 20 21
(*    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
22
open Util
23 24
open Ident
open Ty
25
open Term
26
open Mlw_ty
27
open Mlw_ty.T
28

29 30
(** program variables *)

31
(* pvsymbols represent function arguments and pattern variables *)
32 33

type pvsymbol = private {
34 35
  pv_vs  : vsymbol;
  pv_vtv : vty_value;
36 37
}

38 39 40 41 42 43 44 45 46 47 48
val pv_equal : pvsymbol -> pvsymbol -> bool

val create_pvsymbol : preid -> vty_value -> pvsymbol

(** program symbols *)

(* psymbols represent lambda-abstractions. They are polymorphic and
   can be type-instantiated in some type variables and regions of
   their type signature. *)

type psymbol = private {
49 50
  ps_name  : ident;
  ps_vta   : vty_arrow;
51 52
  ps_vars  : varset;
  (* this varset covers the type variables and regions of the defining
53 54
     lambda that cannot be instantiated. Every other type variable
     and region in ps_vty is generalized and can be instantiated. *)
55 56
  ps_subst : ity_subst;
  (* this substitution instantiates every type variable and region
57
     in ps_vars to itself *)
58
}
59

60
val ps_equal : psymbol -> psymbol -> bool
61

Andrei Paskevich's avatar
Andrei Paskevich committed
62 63
val create_psymbol : preid -> vty_arrow -> varset -> psymbol

64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83
(** program/logic symbols *)

(* plymbols represent algebraic type constructors and projections.
   They must be fully applied and the result is equal to the application of
   the lsymbol. We need this kind of symbols to cover nullary constructors,
   such as Nil, which cannot be given a post-condition. They cannot be
   locally defined and therefore every type variable and region in their
   type signature can be instantiated. *)

type plsymbol = private {
  pl_ls     : lsymbol;
  pl_args   : vty_value list;
  pl_value  : vty_value;
  pl_effect : effect;
}

val pl_equal : plsymbol -> plsymbol -> bool

val create_plsymbol : preid -> vty_value list -> vty_value -> plsymbol
  (* FIXME? Effect calculation is hardwired to correspond to constructors
84
     and projections: mutable arguments are reset, mutable result is read. *)
85

Andrei Paskevich's avatar
Andrei Paskevich committed
86 87 88 89 90 91 92 93 94 95 96 97 98 99
(** patterns *)

type ppattern = private {
  ppat_pattern : pattern;
  ppat_vtv     : vty_value;
  ppat_effect  : effect;
}

val ppat_wild : vty_value -> ppattern
val ppat_var : pvsymbol -> ppattern
val ppat_plapp : plsymbol -> ppattern list -> vty_value -> ppattern
val ppat_lapp : lsymbol -> ppattern list -> vty_value -> ppattern
val ppat_or : ppattern -> ppattern -> ppattern
val ppat_as : ppattern -> pvsymbol -> ppattern
100

101 102
type pre_ppattern =
  | PPwild
103
  | PPvar  of preid
104 105
  | PPlapp of lsymbol * pre_ppattern list
  | PPpapp of plsymbol * pre_ppattern list
106 107
  | PPor   of pre_ppattern * pre_ppattern
  | PPas   of pre_ppattern * preid
108 109 110

val make_ppattern : pre_ppattern -> vty_value -> pvsymbol Mstr.t * ppattern

111 112
(** program expressions *)

Andrei Paskevich's avatar
Andrei Paskevich committed
113 114
type assertion_kind = Aassert | Aassume | Acheck

115 116
type pre = term          (* precondition *)
type post                (* postcondition: a formula with a bound variable *)
Andrei Paskevich's avatar
Andrei Paskevich committed
117 118
type xpost = post Mexn.t (* exceptional postconditions *)

119 120
val create_post : vsymbol -> term -> post
val open_post : post -> vsymbol * term
121

122 123 124 125 126
type variant = {
  v_term : term;           (* : tau *)
  v_rel  : lsymbol option; (* tau tau : prop *)
}

127
type expr = private {
128 129 130
  e_node   : expr_node;
  e_vty    : vty;
  e_effect : effect;
131
  e_vars   : varset Mid.t;
132 133
  e_label  : Slab.t;
  e_loc    : Loc.position option;
134 135
}

136 137
and expr_node = private
  | Elogic  of term
Andrei Paskevich's avatar
Andrei Paskevich committed
138
  | Evalue  of pvsymbol
139 140
  | Earrow  of psymbol
  | Eapp    of expr * pvsymbol
141 142
  | Elet    of let_defn * expr
  | Erec    of rec_defn list * expr
143 144 145
  | Eif     of expr * expr * expr
  | Ecase   of expr * (ppattern * expr) list
  | Eassign of expr * region * pvsymbol
Andrei Paskevich's avatar
Andrei Paskevich committed
146
  | Eghost  of expr
Andrei Paskevich's avatar
Andrei Paskevich committed
147
  | Eany    of any_effect
148
  | Eraise  of xsymbol * expr
Andrei Paskevich's avatar
Andrei Paskevich committed
149
  | Etry    of expr * (xsymbol * pvsymbol * expr) list
150 151
  | Eassert of assertion_kind * term
  | Eabsurd
152

153
and let_defn = private {
154 155
  let_var  : let_var;
  let_expr : expr;
156
}
157

158 159
and let_var =
  | LetV of pvsymbol
160
  | LetA of psymbol
161

162
and rec_defn = private {
163 164
  rec_ps     : psymbol;
  rec_lambda : lambda;
165
  rec_vars   : varset Mid.t;
166 167 168
}

and lambda = {
169 170
  l_args    : pvsymbol list;
  l_variant : variant list; (* lexicographic order *)
171 172 173
  l_pre     : pre;
  l_expr    : expr;
  l_post    : post;
174 175
  l_xpost   : xpost;
}
176

Andrei Paskevich's avatar
Andrei Paskevich committed
177 178 179 180 181 182 183 184 185
(* TODO? Every top region in the type of Eany is reset.
   This is enough for our current purposes, but we might
   need to be more flexible later. *)
and any_effect = {
  aeff_reads  : expr list; (* for a ghost read, use a ghost expression *)
  aeff_writes : expr list; (* for a ghost write, use a ghost expression *)
  aeff_raises : (bool * xsymbol) list; (* ghost raise * exception symbol *)
}

186 187 188 189
val e_label : ?loc:Loc.position -> Slab.t -> expr -> expr
val e_label_add : label -> expr -> expr
val e_label_copy : expr -> expr -> expr

190
val e_value : pvsymbol -> expr
191

192
val e_inst : psymbol -> ity_subst -> expr
Andrei Paskevich's avatar
Andrei Paskevich committed
193
val e_cast : psymbol -> vty -> expr
194

Andrei Paskevich's avatar
Andrei Paskevich committed
195 196 197
exception ValueExpected of expr
exception ArrowExpected of expr

198 199
val vtv_of_expr : expr -> vty_value

200 201 202 203
exception GhostWrite of expr * region
exception GhostRaise of expr * xsymbol
(* a ghost expression writes in a non-ghost region or raises an exception *)

Andrei Paskevich's avatar
Andrei Paskevich committed
204
val e_app : expr -> expr list -> expr
Andrei Paskevich's avatar
Andrei Paskevich committed
205 206 207
val e_lapp : lsymbol -> expr list -> ity -> expr
val e_plapp : plsymbol -> expr list -> ity -> expr

208
val create_let_defn : preid -> expr -> let_defn
Andrei Paskevich's avatar
Andrei Paskevich committed
209
val create_fun_defn : preid -> lambda -> rec_defn
210
val create_rec_defn : (psymbol * lambda) list -> rec_defn list
211

212 213
exception StaleRegion of region * ident
(* freshness violation: a previously reset region is associated to an ident *)
214 215

val e_let : let_defn -> expr -> expr
Andrei Paskevich's avatar
Andrei Paskevich committed
216
val e_rec : rec_defn list -> expr -> expr
217

Andrei Paskevich's avatar
Andrei Paskevich committed
218
val e_if : expr -> expr -> expr -> expr
219
val e_case : expr -> (ppattern * expr) list -> expr
Andrei Paskevich's avatar
Andrei Paskevich committed
220

Andrei Paskevich's avatar
Andrei Paskevich committed
221
exception Immutable of expr
Andrei Paskevich's avatar
Andrei Paskevich committed
222 223

val e_assign : expr -> expr -> expr
Andrei Paskevich's avatar
Andrei Paskevich committed
224
val e_ghost : expr -> expr
Andrei Paskevich's avatar
Andrei Paskevich committed
225 226
val e_any : any_effect -> ity -> expr

Andrei Paskevich's avatar
Andrei Paskevich committed
227 228
val e_void : expr

229 230 231 232 233 234 235 236
val e_const : constant -> expr
val e_int_const : string -> expr
val e_real_const : real_constant -> expr

val e_lazy_and : expr -> expr -> expr
val e_lazy_or : expr -> expr -> expr
val e_not : expr -> expr

Andrei Paskevich's avatar
Andrei Paskevich committed
237
val e_raise : xsymbol -> expr -> ity -> expr
Andrei Paskevich's avatar
Andrei Paskevich committed
238
val e_try : expr -> (xsymbol * pvsymbol * expr) list -> expr
239

240 241 242
val e_absurd : ity -> expr
val e_assert : assertion_kind -> term -> expr