ptree.ml 6.16 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   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 12 13

(*s Parse trees. *)

Andrei Paskevich's avatar
Andrei Paskevich committed
14 15 16
type attr =
  | ATstr of Ident.attribute
  | ATpos of Loc.position
17

18 19
type ident = {
  id_str : string;
Andrei Paskevich's avatar
Andrei Paskevich committed
20
  id_ats : attr list;
Andrei Paskevich's avatar
Andrei Paskevich committed
21
  id_loc : Loc.position;
22
}
23

Andrei Paskevich's avatar
Andrei Paskevich committed
24 25
(*s Types *)

26 27
type qualid =
  | Qident of ident
28
  | Qdot of qualid * ident
29

30
type pty =
31
  | PTtyvar of ident
32 33 34
  | PTtyapp of qualid * pty list
  | PTtuple of pty list
  | PTarrow of pty * pty
35
  | PTscope of qualid * pty
36
  | PTparen of pty
Andrei Paskevich's avatar
Andrei Paskevich committed
37
  | PTpure  of pty
38

Andrei Paskevich's avatar
Andrei Paskevich committed
39
(*s Patterns *)
40

41 42
type ghost = bool

43 44
type pattern = {
  pat_desc : pat_desc;
Andrei Paskevich's avatar
Andrei Paskevich committed
45
  pat_loc  : Loc.position;
46
}
Andrei Paskevich's avatar
Andrei Paskevich committed
47 48

and pat_desc =
49
  | Pwild
50
  | Pvar of ident
51 52 53
  | Papp of qualid * pattern list
  | Prec of (qualid * pattern) list
  | Ptuple of pattern list
54
  | Pas of pattern * ident * ghost
55
  | Por of pattern * pattern
56
  | Pcast of pattern * pty
57
  | Pscope of qualid * pattern
58
  | Pparen of pattern
59
  | Pghost of pattern
60

Andrei Paskevich's avatar
Andrei Paskevich committed
61 62 63 64 65
(*s Logical terms and formulas *)

type binder = Loc.position * ident option * ghost * pty option
type param  = Loc.position * ident option * ghost * pty

66 67
type term = {
  term_desc : term_desc;
Andrei Paskevich's avatar
Andrei Paskevich committed
68
  term_loc  : Loc.position;
69
}
70

71 72 73
and term_desc =
  | Ttrue
  | Tfalse
Andrei Paskevich's avatar
Andrei Paskevich committed
74
  | Tconst of Number.constant
75 76 77 78 79
  | Tident of qualid
  | Tidapp of qualid * term list
  | Tapply of term * term
  | Tinfix of term * ident * term
  | Tinnfix of term * ident * term
80 81 82
  | Tbinop of term * Dterm.dbinop * term
  | Tbinnop of term * Dterm.dbinop * term
  | Tnot of term
83
  | Tif of term * term * term
84
  | Tquant of Dterm.dquant * binder list * term list list * term
Andrei Paskevich's avatar
Andrei Paskevich committed
85
  | Tattr of attr * term
86
  | Tlet of ident * term * term
87
  | Tcase of term * (pattern * term) list
88 89 90 91
  | Tcast of term * pty
  | Ttuple of term list
  | Trecord of (qualid * term) list
  | Tupdate of term * (qualid * term) list
Andrei Paskevich's avatar
M.()  
Andrei Paskevich committed
92
  | Tscope of qualid * term
93
  | Tat of term * ident
94

Andrei Paskevich's avatar
Andrei Paskevich committed
95
(*s Program expressions *)
96

97
type invariant = term list
98
type variant = (term * qualid option) list
99

100
type pre = term
Andrei Paskevich's avatar
Andrei Paskevich committed
101
type post = Loc.position * (pattern * term) list
Andrei Paskevich's avatar
Andrei Paskevich committed
102
type xpost = Loc.position * (qualid * (pattern * term) option) list
103 104

type spec = {
105 106 107
  sp_pre     : pre list;
  sp_post    : post list;
  sp_xpost   : xpost list;
108
  sp_reads   : qualid list;
109
  sp_writes  : term list;
110
  sp_alias   : (term * term) list;
111
  sp_variant : variant;
112 113
  sp_checkrw : bool;
  sp_diverge : bool;
114
  sp_partial : bool;
115
}
116 117 118

type expr = {
  expr_desc : expr_desc;
Andrei Paskevich's avatar
Andrei Paskevich committed
119
  expr_loc  : Loc.position;
120 121 122
}

and expr_desc =
123 124
  | Etrue
  | Efalse
Andrei Paskevich's avatar
Andrei Paskevich committed
125
  | Econst of Number.constant
126 127
  (* lambda-calculus *)
  | Eident of qualid
128
  | Eidapp of qualid * expr list
129
  | Eapply of expr * expr
130 131
  | Einfix of expr * ident * expr
  | Einnfix of expr * ident * expr
132
  | Elet of ident * ghost * Expr.rs_kind * expr * expr
133
  | Erec of fundef list * expr
134 135
  | Efun of binder list * pty option * Ity.mask * spec * expr
  | Eany of param list * Expr.rs_kind * pty option * Ity.mask * spec
136
  | Etuple of expr list
137
  | Erecord of (qualid * expr) list
138
  | Eupdate of expr * (qualid * expr) list
139
  | Eassign of (expr * qualid * expr) list
140 141 142
  (* control *)
  | Esequence of expr * expr
  | Eif of expr * expr * expr
143 144 145
  | Ewhile of expr * invariant * variant * expr
  | Eand of expr * expr
  | Eor of expr * expr
Andrei Paskevich's avatar
Andrei Paskevich committed
146
  | Enot of expr
147
  | Ematch of expr * reg_branch list * exn_branch list
148
  | Eabsurd
149
  | Epure of term
150
  | Eidpur of qualid
151
  | Eraise of qualid * expr option
152
  | Eexn of ident * pty * Ity.mask * expr
Andrei Paskevich's avatar
Andrei Paskevich committed
153
  | Eoptexn of ident * Ity.mask * expr
154
  | Efor of ident * expr * Expr.for_direction * expr * invariant * expr
155
  (* annotations *)
156
  | Eassert of Expr.assertion_kind * term
Andrei Paskevich's avatar
Andrei Paskevich committed
157 158
  | Escope of qualid * expr
  | Elabel of ident * expr
159
  | Ecast of expr * pty
160
  | Eghost of expr
Andrei Paskevich's avatar
Andrei Paskevich committed
161
  | Eattr of attr * expr
162

163 164 165 166
and reg_branch = pattern * expr

and exn_branch = qualid * pattern option * expr

167 168
and fundef = ident * ghost * Expr.rs_kind *
  binder list * pty option * Ity.mask * spec * expr
169

Andrei Paskevich's avatar
Andrei Paskevich committed
170 171 172 173 174 175 176 177 178 179 180 181 182 183
(*s Declarations *)

type field = {
  f_loc     : Loc.position;
  f_ident   : ident;
  f_pty     : pty;
  f_mutable : bool;
  f_ghost   : bool
}

type type_def =
  | TDalias     of pty
  | TDalgebraic of (Loc.position * ident * param list) list
  | TDrecord    of field list
184
  | TDrange     of BigInt.t * BigInt.t
185
  | TDfloat     of int * int
Andrei Paskevich's avatar
Andrei Paskevich committed
186 187 188 189 190 191 192 193 194 195

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

type type_decl = {
  td_loc    : Loc.position;
  td_ident  : ident;
  td_params : ident list;
  td_vis    : visibility; (* records only *)
  td_mut    : bool;       (* records or abstract types *)
  td_inv    : invariant;  (* records only *)
196
  td_wit    : (qualid * expr) list;
Andrei Paskevich's avatar
Andrei Paskevich committed
197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225
  td_def    : type_def;
}

type logic_decl = {
  ld_loc    : Loc.position;
  ld_ident  : ident;
  ld_params : param list;
  ld_type   : pty option;
  ld_def    : term option;
}

type ind_decl = {
  in_loc    : Loc.position;
  in_ident  : ident;
  in_params : param list;
  in_def    : (Loc.position * ident * term) list;
}

type metarg =
  | Mty  of pty
  | Mfs  of qualid
  | Mps  of qualid
  | Max  of qualid
  | Mlm  of qualid
  | Mgl  of qualid
  | Mstr of string
  | Mint of int

type clone_subst =
Andrei Paskevich's avatar
Andrei Paskevich committed
226 227 228 229
  | CStsym  of qualid * ident list * pty
  | CSfsym  of qualid * qualid
  | CSpsym  of qualid * qualid
  | CSvsym  of qualid * qualid
230
  | CSxsym  of qualid * qualid
231
  | CSprop  of Decl.prop_kind
232
  | CSaxiom of qualid
Andrei Paskevich's avatar
Andrei Paskevich committed
233 234
  | CSlemma of qualid
  | CSgoal  of qualid
Andrei Paskevich's avatar
Andrei Paskevich committed
235

236 237 238 239 240
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
241
  | Dlet of ident * ghost * Expr.rs_kind * expr
242
  | Drec of fundef list
243
  | Dexn of ident * pty * Ity.mask
Andrei Paskevich's avatar
Andrei Paskevich committed
244 245 246
  | Dmeta of ident * metarg list
  | Dclone of qualid * clone_subst list
  | Duse of qualid