ptree.ml 5.89 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
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
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
10
(********************************************************************)
11 12 13 14 15

(*s Parse trees. *)

type loc = Loc.position

16
(*s Logical terms and formulas *)
17

18 19 20
type integer_constant = Number.integer_constant
type real_constant = Number.real_constant
type constant = Number.constant
21 22 23 24

type label =
  | Lstr of Ident.label
  | Lpos of Loc.position
25

26 27
type quant =
  | Tforall | Texists | Tlambda
28

29 30
type binop =
  | Tand | Tand_asym | Tor | Tor_asym | Timplies | Tiff
31

32 33
type unop =
  | Tnot
34

35 36 37 38 39
type ident = {
  id_str : string;
  id_lab : label list;
  id_loc : loc;
}
40 41 42

type qualid =
  | Qident of ident
43
  | Qdot of qualid * ident
44

45
type pty =
46
  | PTtyvar of ident
47 48 49 50
  | PTtyapp of qualid * pty list
  | PTtuple of pty list
  | PTarrow of pty * pty
  | PTparen of pty
51

52 53 54 55
type ghost = bool

type binder = loc * ident option * ghost * pty option
type param  = loc * ident option * ghost * pty
56

57 58 59 60
type pattern = {
  pat_desc : pat_desc;
  pat_loc  : loc;
}
Andrei Paskevich's avatar
Andrei Paskevich committed
61 62

and pat_desc =
63 64 65 66 67 68 69
  | Pwild
  | Pvar of ident
  | Papp of qualid * pattern list
  | Prec of (qualid * pattern) list
  | Ptuple of pattern list
  | Por of pattern * pattern
  | Pas of pattern * ident
70
  | Pcast of pattern * pty
71 72 73 74 75

type term = {
  term_desc : term_desc;
  term_loc  : loc;
}
76

77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96
and term_desc =
  | Ttrue
  | Tfalse
  | Tconst of constant
  | Tident of qualid
  | Tidapp of qualid * term list
  | Tapply of term * term
  | Tinfix of term * ident * term
  | Tinnfix of term * ident * term
  | Tbinop of term * binop * term
  | Tunop of unop * term
  | Tif of term * term * term
  | Tquant of quant * binder list * term list list * term
  | Tnamed of label * term
  | Tlet of ident * term * term
  | Tmatch of term * (pattern * term) list
  | Tcast of term * pty
  | Ttuple of term list
  | Trecord of (qualid * term) list
  | Tupdate of term * (qualid * term) list
97

98
(*s Declarations. *)
99

100
type use = {
Andrei Paskevich's avatar
Andrei Paskevich committed
101
  use_module : qualid;
102
  use_import : (bool (* import *) * string (* as *)) option;
Jean-Christophe Filliâtre's avatar
uses  
Jean-Christophe Filliâtre committed
103 104
}

105
type clone_subst =
106
  | CSns    of loc * qualid option * qualid option
107
  | CStsym  of loc * qualid * ident list * pty
108 109
  | CSfsym  of loc * qualid * qualid
  | CSpsym  of loc * qualid * qualid
Andrei Paskevich's avatar
Andrei Paskevich committed
110
  | CSvsym  of loc * qualid * qualid
111 112
  | CSlemma of loc * qualid
  | CSgoal  of loc * qualid
113

114 115 116 117 118 119 120
type field = {
  f_loc     : loc;
  f_ident   : ident;
  f_pty     : pty;
  f_mutable : bool;
  f_ghost   : bool
}
121

122
type type_def =
123
  | TDabstract
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
124
  | TDalias     of pty
125
  | TDalgebraic of (loc * ident * param list) list
126 127
  | TDrecord    of field list

128
type visibility = Public | Private | Abstract (* = Private + ghost fields *)
129

130
type invariant = term list
131

132
type type_decl = {
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
133 134
  td_loc    : loc;
  td_ident  : ident;
135
  td_params : ident list;
136 137 138
  td_vis    : visibility; (* records only *)
  td_mut    : bool;       (* records or abstract types *)
  td_inv    : invariant;  (* records only *)
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
139
  td_def    : type_def;
140 141
}

142
type logic_decl = {
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
143 144
  ld_loc    : loc;
  ld_ident  : ident;
145
  ld_params : param list;
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
146
  ld_type   : pty option;
147
  ld_def    : term option;
148 149
}

150 151 152
type ind_decl = {
  in_loc    : loc;
  in_ident  : ident;
153
  in_params : param list;
154
  in_def    : (loc * ident * term) list;
155 156
}

157
type metarg =
158 159 160 161 162 163
  | Mty  of pty
  | Mfs  of qualid
  | Mps  of qualid
  | Mpr  of qualid
  | Mstr of string
  | Mint of int
164

165
type use_clone = use * clone_subst list option
166

167 168
(* program files *)

169
type variant = (term * qualid option) list
170

171 172 173
type pre = term
type post = loc * (pattern * term) list
type xpost = loc * (qualid * pattern * term) list
174 175

type spec = {
176 177 178
  sp_pre     : pre list;
  sp_post    : post list;
  sp_xpost   : xpost list;
179
  sp_reads   : qualid list;
180
  sp_writes  : term list;
181
  sp_variant : variant;
182 183
  sp_checkrw : bool;
  sp_diverge : bool;
184
}
185

186 187
type top_ghost = Gnone | Gghost | Glemma

188 189 190 191 192 193
type expr = {
  expr_desc : expr_desc;
  expr_loc  : loc;
}

and expr_desc =
194 195
  | Etrue
  | Efalse
196
  | Econst of constant
197 198
  (* lambda-calculus *)
  | Eident of qualid
199
  | Eidapp of qualid * expr list
200
  | Eapply of expr * expr
201 202
  | Einfix of expr * ident * expr
  | Einnfix of expr * ident * expr
203
  | Elet of ident * top_ghost * expr * expr
204 205 206
  | Efun of ident * top_ghost * lambda * expr
  | Erec of fundef list * expr
  | Elam of lambda
207
  | Etuple of expr list
208
  | Erecord of (qualid * expr) list
209
  | Eupdate of expr * (qualid * expr) list
210
  | Eassign of expr * qualid * expr
211 212 213
  (* control *)
  | Esequence of expr * expr
  | Eif of expr * expr * expr
214 215 216 217
  | Eloop of invariant * variant * expr
  | Ewhile of expr * invariant * variant * expr
  | Eand of expr * expr
  | Eor of expr * expr
Andrei Paskevich's avatar
Andrei Paskevich committed
218
  | Enot of expr
219 220 221
  | Ematch of expr * (pattern * expr) list
  | Eabsurd
  | Eraise of qualid * expr option
222
  | Etry of expr * (qualid * pattern option * expr) list
223
  | Efor of ident * expr * Expr.for_direction * expr * invariant * expr
224
  (* annotations *)
225
  | Eassert of Expr.assertion_kind * term
226
  | Emark of ident * expr
227
  | Ecast of expr * pty
228
  | Eany of any
229
  | Eghost of expr
230
  | Eabstract of spec * expr
231
  | Enamed of label * expr
232

233
and fundef = ident * top_ghost * lambda
234

235 236 237
and lambda = binder list * pty option * spec * expr

and any = param list * pty * spec
238

239 240 241 242 243 244
type decl =
  | Dtype of type_decl list
  | Dlogic of logic_decl list
  | Dind of Decl.ind_sign * ind_decl list
  | Dprop of Decl.prop_kind * ident * term
  | Dmeta of ident * metarg list
245
  | Dval of ident * top_ghost * any
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
246
  | Dlet of ident * top_ghost * expr
247 248
  | Dfun of ident * top_ghost * lambda
  | Drec of fundef list
249
  | Dexn of ident * pty