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

14 15 16
type label =
  | Lstr of Ident.label
  | Lpos of Loc.position
17

18 19 20
type ident = {
  id_str : string;
  id_lab : label 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 * ghost
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

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

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

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

67 68 69
and term_desc =
  | Ttrue
  | Tfalse
Andrei Paskevich's avatar
Andrei Paskevich committed
70
  | Tconst of Number.constant
71 72 73 74 75
  | 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
76 77 78
  | Tbinop of term * Dterm.dbinop * term
  | Tbinnop of term * Dterm.dbinop * term
  | Tnot of term
79
  | Tif of term * term * term
Andrei Paskevich's avatar
Andrei Paskevich committed
80
  | Tquant of Dterm.dquant * binder list * term list list * term
81 82 83 84 85 86 87
  | 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
88
  | Tat of term * ident
89

Andrei Paskevich's avatar
Andrei Paskevich committed
90
(*s Program expressions *)
91

92
type invariant = term list
93
type variant = (term * qualid option) list
94

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

type spec = {
100 101 102
  sp_pre     : pre list;
  sp_post    : post list;
  sp_xpost   : xpost list;
103
  sp_reads   : qualid list;
104
  sp_writes  : term list;
105
  sp_variant : variant;
106 107
  sp_checkrw : bool;
  sp_diverge : bool;
108
}
109 110 111

type expr = {
  expr_desc : expr_desc;
Andrei Paskevich's avatar
Andrei Paskevich committed
112
  expr_loc  : Loc.position;
113 114 115
}

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

154 155
and fundef = ident * ghost * Expr.rs_kind *
  binder list * pty option * Ity.mask * spec * expr
156

Andrei Paskevich's avatar
Andrei Paskevich committed
157 158 159 160 161 162 163 164 165 166 167 168 169 170
(*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
171 172
  | TDrange     of BigInt.t * BigInt.t
  | TDfloat     of int * int
Andrei Paskevich's avatar
Andrei Paskevich committed
173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211

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 *)
  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
212 213 214 215
  | CStsym  of qualid * ident list * pty
  | CSfsym  of qualid * qualid
  | CSpsym  of qualid * qualid
  | CSvsym  of qualid * qualid
216
  | CSxsym  of qualid * qualid
217
  | CSaxiom of qualid
Andrei Paskevich's avatar
Andrei Paskevich committed
218 219
  | CSlemma of qualid
  | CSgoal  of qualid
Andrei Paskevich's avatar
Andrei Paskevich committed
220

221 222 223 224 225
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
226
  | Dlet of ident * ghost * Expr.rs_kind * expr
227
  | Drec of fundef list
228
  | Dexn of ident * pty * Ity.mask
Andrei Paskevich's avatar
Andrei Paskevich committed
229 230 231
  | Dmeta of ident * metarg list
  | Dclone of qualid * clone_subst list
  | Duse of qualid