pvs-common.gen 7.36 KB
Newer Older
1

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
2
3
4
unknown "unfinished" "\"\\0\""
unknown "untried" "\"\\0\""
valid "succeeded"
5
6
time "why3cpulimit time : %s s"

7
(*transformation "inline_trivial"*)
8
transformation "eliminate_builtin"
9
10

(* PVS does not support mutual recursion *)
11
transformation "eliminate_mutual_recursion"
12
(* though we could do better, we only use recursion on one argument *)
13
14
transformation "eliminate_non_struct_recursion"

15
16
transformation "eliminate_epsilon"

17
(* PVS only has simple patterns *)
18
transformation "compile_match"
19
transformation "eliminate_projections"
20
21
22
23
24
25
26
27
28

transformation "simplify_formula"

theory BuiltIn
  syntax type   int   "int"
  syntax type   real  "real"
  syntax predicate  (=)   "(%1 = %2)"
end

29
30
31
32
33
theory HighOrd
  syntax type (->) "[%1 -> %2]"
  syntax function (@) "%1(%2)"
end

34
theory map.Map
35
  syntax function get  "%1(%2)"
36
37
38
39
  syntax function ([]) "%1(%2)"

  syntax function set    "(%1 WITH [(%2) |-> %3])"
  syntax function ([<-]) "(%1 WITH [(%2) |-> %3])"
MARCHE Claude's avatar
MARCHE Claude committed
40
41
end

42
theory Bool
43
44
45
46
  syntax type bool   "bool"

  syntax function True  "TRUE"
  syntax function False "FALSE"
47
48
49
end

theory bool.Bool
50
51
52
53
54

  syntax function andb  "(%1 AND %2)"
  syntax function orb   "(%1 OR %2)"
  syntax function xorb  "(%1 XOR %2)"
  syntax function notb  "(NOT %1)"
55
  syntax function implb "(%1 => %2)"
56
57
58
59
60
61
62
63

end

theory int.Int

  syntax function zero "0"
  syntax function one  "1"

64
65
66
67
  syntax function ( + ) "(%1 + %2)"
  syntax function ( - ) "(%1 - %2)"
  syntax function ( * ) "(%1 * %2)"
  syntax function (-_)  "(-%1)"
68
69
70
71
72
73

  syntax predicate (<=) "(%1 <= %2)"
  syntax predicate (<)  "(%1 <  %2)"
  syntax predicate (>=) "(%1 >= %2)"
  syntax predicate (>)  "(%1 >  %2)"

Andrei Paskevich's avatar
Andrei Paskevich committed
74
75
76
77
78
79
80
  remove prop MulComm.Comm
  remove prop MulAssoc.Assoc
  remove prop Unit_def_l
  remove prop Unit_def_r
  remove prop Inv_def_l
  remove prop Inv_def_r
  remove prop Assoc
81
82
  remove prop Mul_distr_l
  remove prop Mul_distr_r
Andrei Paskevich's avatar
Andrei Paskevich committed
83
  remove prop Comm
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
  remove prop Unitary
  remove prop Refl
  remove prop Trans
  remove prop Antisymm
  remove prop Total
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
  remove prop CompatOrderMult
  remove prop ZeroLessOne

end

theory int.Abs

  syntax function abs "abs(%1)"

  remove prop Abs_pos

end

theory int.MinMax

  syntax function min "min(%1, %2)"
  syntax function max "max(%1, %2)"

end

theory real.Real

113
114
  syntax function zero "0"
  syntax function one  "1"
115

116
117
118
119
  syntax function ( + ) "(%1 + %2)"
  syntax function ( - ) "(%1 - %2)"
  syntax function (-_)  "(-%1)"
  syntax function ( * ) "(%1 * %2)"
120
  (* / and inv are defined in the realization *)
121

122
123
124
125
  syntax predicate (<=) "(%1 <= %2)"
  syntax predicate (<)  "(%1 <  %2)"
  syntax predicate (>=) "(%1 >= %2)"
  syntax predicate (>)  "(%1 >  %2)"
126

Andrei Paskevich's avatar
Andrei Paskevich committed
127
128
129
130
131
132
133
  remove prop MulComm.Comm
  remove prop MulAssoc.Assoc
  remove prop Unit_def_l
  remove prop Unit_def_r
  remove prop Inv_def_l
  remove prop Inv_def_r
  remove prop Assoc
134
135
  remove prop Mul_distr_l
  remove prop Mul_distr_r
Andrei Paskevich's avatar
Andrei Paskevich committed
136
  remove prop Comm
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
  remove prop Unitary
  remove prop Inverse
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
  remove prop CompatOrderMult
  remove prop ZeroLessOne
  remove prop Refl
  remove prop Trans
  remove prop Antisymm
  remove prop Total
  remove prop assoc_mul_div
  remove prop assoc_div_mul
  remove prop assoc_div_div

end

153
154
155
156
theory real.MinMax
  syntax function min "min(%1, %2)"
  syntax function max "max(%1, %2)"

157
158
  remove prop Max_l
  remove prop Min_r
159
160
161
162
  remove prop Max_comm
  remove prop Min_comm
  remove prop Max_assoc
  remove prop Min_assoc
163
164
end

165
166
theory real.RealInfix

167
168
169
170
  syntax function (+.)  "(%1 + %2)"
  syntax function (-.)  "(%1 - %2)"
  syntax function (-._) "(-%1)"
  syntax function ( *.) "(%1 * %2)"
171
172
  syntax function (/.)  "real@Real.infix_sl(%1, %2)"
  syntax function inv   "real@Real.inv(%1)"
173

174
175
176
177
  syntax predicate (<=.) "(%1 <= %2)"
  syntax predicate (<.)  "(%1 <  %2)"
  syntax predicate (>=.) "(%1 >= %2)"
  syntax predicate (>.)  "(%1 >  %2)"
178
179
180
181
182

end

theory real.Abs

183
  syntax function abs "abs(%1)"
184
185
186
187
188
189
190
191

  remove prop Abs_le
  remove prop Abs_pos

end

theory real.FromInt

192
  syntax function from_int "(%1 :: real)"
193
194
195
196
197
198
199
200
201
202

  remove prop Zero
  remove prop One
  remove prop Add
  remove prop Sub
  remove prop Mul
  remove prop Neg

end

203
204
205
206
207
208
209
210
211
212
213
theory real.PowerReal

  syntax function pow "(%1 ^ %2)"

  remove prop Pow_x_zero
  remove prop Pow_x_one
  remove prop Pow_one_y

end

(***
214
215
theory real.Square

216
  syntax function sqrt "SQRT(%1)"
217
218
219
220
221

end

theory real.ExpLog

222
223
  syntax function exp "EXP(%1)"
  syntax function log "LOG(%1)"
224
225
226
227
228

end

theory real.Trigonometry

229
230
  syntax function cos "COS(%1)"
  syntax function sin "SIN(%1)"
231
232
233

  syntax function pi "PI"

234
  syntax function tan "TAN(%1)"
235
236

end
237
***)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
238

239
240
241
242
243
244
245
246
247
248
249
theory option.Option
  syntax type option "lift[%1]"

  syntax function None "bottom"
  syntax function Some "up(%1)"
end

theory list.List

  syntax type list "list[%1]"

250
  syntax function Nil  "(null :: %t0)"
251
252
253
254
255
256
257
258
259
260
261
262
  syntax function Cons "cons(%1, %2)"

end

theory list.Length
  syntax function length "length(%1)"
  remove prop Length_nonnegative
  remove prop Length_nil
end

theory list.Mem
  syntax predicate mem "member(%1, %2)"
263

264
265
266
267
268
269
270
271
272
273
274
275
276
end

theory list.Nth
  syntax function nth
    "IF 0 <= %1 AND %1 < length(%2) THEN up(nth(%2, %1)) ELSE bottom ENDIF"
end

theory list.Append
  syntax function (++) "append(%1, %2)"

  remove prop Append_assoc
  remove prop Append_l_nil
  remove prop Append_length
277
278
279
  (* FIXME? the following are not part of PVS prelude *)
  remove prop mem_append
  remove prop mem_decomp
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
end

theory list.Reverse
  syntax function reverse "reverse(%1)"
end

theory set.Set
  syntax type set "set[%1]"

  syntax predicate mem "member(%1, %2)"
  remove prop      extensionality

  syntax predicate subset "subset?(%1, %2)"
  remove prop      subset_trans

  syntax function  empty    "(emptyset :: %t0)"
  syntax predicate is_empty "empty?(%1)"
297
  remove prop      empty_def
298
299

  syntax function add "add(%1, %2)"
300
  remove prop     add_def
301
302
303
  syntax function singleton "singleton(%1)"

  syntax function remove "remove(%1, %2)"
304
  remove prop     remove_def
305
306
307
  remove prop     subset_remove

  syntax function union "union(%1, %2)"
308
  remove prop     union_def
309
310

  syntax function inter "intersection(%1, %2)"
311
  remove prop     inter_def
312
313

  syntax function diff "difference(%1, %2)"
314
  remove prop     diff_def
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
  remove prop     subset_diff

  (* TODO: choose *)

  syntax function all "fullset"
end

theory set.Fset
  syntax type set "finite_set[%1]"

  syntax predicate mem "member(%1, %2)"
  remove prop      extensionality

  syntax predicate subset "subset?(%1, %2)"
  remove prop      subset_trans

  syntax function  empty    "(emptyset :: %t0)"
  syntax predicate is_empty "empty?(%1)"
333
  remove prop      empty_def
334
335

  syntax function add "add(%1, %2)"
336
  remove prop     add_def
337
338
339
  syntax function singleton "singleton(%1)"

  syntax function remove "remove(%1, %2)"
340
  remove prop     remove_def
341
342
343
  remove prop     subset_remove

  syntax function union "union(%1, %2)"
344
  remove prop     union_def
345
346

  syntax function inter "intersection(%1, %2)"
347
  remove prop     inter_def
348
349

  syntax function diff "difference(%1, %2)"
350
  remove prop     diff_def
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
  remove prop     subset_diff

  (* TODO: choose *)

  syntax function cardinal "Card(%1)"
  remove prop     cardinal_nonneg
  remove prop     cardinal_empty
  remove prop     cardinal_add
  remove prop     cardinal_remove
  remove prop     cardinal_subset
  remove prop     cardinal1

  (* TODO: nth *)
end

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
366
367
368
(* this file has an extension .aux rather than .gen
   since it should not be distributed *)
import "pvs-realizations.aux"