ptree.ml 6.09 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
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  *)
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

(*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 35
  | PTtyapp of qualid * pty list
  | PTtuple of pty list
  | PTarrow of pty * pty
  | PTparen of pty
Andrei Paskevich's avatar
Andrei Paskevich committed
36
  | PTpure  of pty
37

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

40 41
type ghost = bool

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

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

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

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

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

69 70 71
and term_desc =
  | Ttrue
  | Tfalse
Andrei Paskevich's avatar
Andrei Paskevich committed
72
  | Tconst of Number.constant
73 74 75 76 77
  | Tident of qualid
  | Tidapp of qualid * term list
  | Tapply of term * term
  | Tinfix of term * ident * term
  | Tinnfix of term * ident * term
Andrei Paskevich's avatar
Andrei Paskevich committed
78 79 80
  | Tbinop of term * Dterm.dbinop * term
  | Tbinnop of term * Dterm.dbinop * term
  | Tnot of term
81
  | Tif of term * term * term
Andrei Paskevich's avatar
Andrei Paskevich committed
82
  | Tquant of Dterm.dquant * binder list * term list list * term
Andrei Paskevich's avatar
Andrei Paskevich committed
83
  | Tattr of attr * term
84
  | Tlet of ident * term * term
85
  | Tcase of term * (pattern * term) list
86 87 88 89
  | 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
90
  | Tscope of qualid * term
91
  | Tat of term * ident
92

Andrei Paskevich's avatar
Andrei Paskevich committed
93
(*s Program expressions *)
94

95
type invariant = term list
96
type variant = (term * qualid option) list
97

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

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

type expr = {
  expr_desc : expr_desc;
Andrei Paskevich's avatar
Andrei Paskevich committed
116
  expr_loc  : Loc.position;
117 118 119
}

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

160 161 162 163
and reg_branch = pattern * expr

and exn_branch = qualid * pattern option * expr

164 165
and fundef = ident * ghost * Expr.rs_kind *
  binder list * pty option * Ity.mask * spec * expr
166

Andrei Paskevich's avatar
Andrei Paskevich committed
167 168 169 170 171 172 173 174 175 176 177 178 179 180
(*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
181
  | TDrange     of BigInt.t * BigInt.t
182
  | TDfloat     of int * int
Andrei Paskevich's avatar
Andrei Paskevich committed
183 184 185 186 187 188 189 190 191 192

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 *)
193
  td_wit    : (qualid * expr) list;
Andrei Paskevich's avatar
Andrei Paskevich committed
194 195 196 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
  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
223 224 225 226
  | CStsym  of qualid * ident list * pty
  | CSfsym  of qualid * qualid
  | CSpsym  of qualid * qualid
  | CSvsym  of qualid * qualid
227
  | CSxsym  of qualid * qualid
228
  | CSprop  of Decl.prop_kind
229
  | CSaxiom of qualid
Andrei Paskevich's avatar
Andrei Paskevich committed
230 231
  | CSlemma of qualid
  | CSgoal  of qualid
Andrei Paskevich's avatar
Andrei Paskevich committed
232

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