pvs-common.gen 5.12 KB
Newer Older
1
2
3
4
5
6
7
8

valid 0
unknown "Error: \\(.*\\)$" "\\1"
fail "Syntax error: \\(.*\\)$" "\\1"
time "why3cpulimit time : %s s"

transformation "inline_trivial"
transformation "eliminate_builtin"
9
10

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

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

transformation "simplify_formula"

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

28
29
30
31
32
theory Tuple0
  syntax type     tuple0 "tuple0"
  syntax function Tuple0 "Tuple0"
end

33
34
35
36
37
38
39
40
41
theory map.Map
  syntax type  map "[%1 -> %2]"

  syntax function get "%1(%2)"
  syntax function set "(%1 WITH [(%2) |-> %3])"

  remove prop Select_eq
  remove prop Select_neq

42
43
44
45
46
  (* %t0 is "map a b"
     %t1 is the type of const's argument, that is "b"
     but we need type "a" instead, i.e. the first type argument

  syntax function const "(LAMBDA (x:%t1): %1)"
47
48
49
50
  remove prop Const
  *)
end

51
theory Bool
52
53
54
55
  syntax type bool   "bool"

  syntax function True  "TRUE"
  syntax function False "FALSE"
56
57
58
end

theory bool.Bool
59
60
61
62
63

  syntax function andb  "(%1 AND %2)"
  syntax function orb   "(%1 OR %2)"
  syntax function xorb  "(%1 XOR %2)"
  syntax function notb  "(NOT %1)"
64
  syntax function implb "(%1 => %2)"
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
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
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130

end


theory int.Int

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

  syntax function (+)  "(%1 + %2)"
  syntax function (-)  "(%1 - %2)"
  syntax function (*)  "(%1 * %2)"
  syntax function (-_) "(-%1)"

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

  remove prop CommutativeGroup.Comm.Comm
  remove prop CommutativeGroup.Assoc.Assoc
  remove prop CommutativeGroup.Unit_def
  remove prop CommutativeGroup.Inv_def
  remove prop Assoc.Assoc
  remove prop Mul_distr
  remove prop Comm.Comm
  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 int.EuclideanDivision

  syntax function div "ndiv(%1, %2)"
  syntax function mod "mod(%1, %2)"

  remove prop Div_mod
  remove prop Div_bound
  remove prop Mod_bound
  remove prop Mod_1
  remove prop Div_1

end

131
(***
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
theory int.ComputerDivision

  syntax function div "(ZOdiv %1 %2)"
  syntax function mod "(ZOmod %1 %2)"

  remove prop Div_mod
  remove prop Div_bound
  remove prop Mod_bound
  remove prop Div_sign_pos
  remove prop Div_sign_neg
  remove prop Mod_sign_pos
  remove prop Mod_sign_neg
  remove prop Rounds_toward_zero
  remove prop Div_1
  remove prop Mod_1
  remove prop Div_inf
  remove prop Mod_inf
  remove prop Div_mult
  remove prop Mod_mult

end
153
***)
154
155
156

theory real.Real

157
158
  syntax function zero "0"
  syntax function one  "1"
159

160
161
162
163
164
165
  syntax function (+)  "(%1 + %2)"
  syntax function (-)  "(%1 - %2)"
  syntax function (-_) "(-%1)"
  syntax function (*)  "(%1 * %2)"
  syntax function (/)  "(%1 / %2)"
  syntax function inv  "(1 / %1)"
166

167
168
169
170
  syntax predicate (<=) "(%1 <= %2)"
  syntax predicate (<)  "(%1 <  %2)"
  syntax predicate (>=) "(%1 >= %2)"
  syntax predicate (>)  "(%1 >  %2)"
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196

  remove prop CommutativeGroup.Comm.Comm
  remove prop CommutativeGroup.Assoc.Assoc
  remove prop CommutativeGroup.Unit_def
  remove prop CommutativeGroup.Inv_def
  remove prop Assoc.Assoc
  remove prop Mul_distr
  remove prop Comm.Comm
  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

theory real.RealInfix

197
198
199
200
201
  syntax function (+.)  "(%1 + %2)"
  syntax function (-.)  "(%1 - %2)"
  syntax function (-._) "(-%1)"
  syntax function ( *.) "(%1 * %2)"
  syntax function (/.)  "(%1 / %2)"
202

203
204
205
206
  syntax predicate (<=.) "(%1 <= %2)"
  syntax predicate (<.)  "(%1 <  %2)"
  syntax predicate (>=.) "(%1 >= %2)"
  syntax predicate (>.)  "(%1 >  %2)"
207
208
209
210
211

end

theory real.Abs

212
  syntax function abs "abs(%1)"
213
214
215
216
217
218
219
220

  remove prop Abs_le
  remove prop Abs_pos

end

theory real.FromInt

221
  syntax function from_int "(%1 :: real)"
222
223
224
225
226
227
228
229
230
231
232
233

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

end

theory real.Square

234
  syntax function sqrt "SQRT(%1)"
235
236
237
238
239

end

theory real.ExpLog

240
241
  syntax function exp "EXP(%1)"
  syntax function log "LOG(%1)"
242
243
244
245
246

end

theory real.Power

247
248
249
250
251
  syntax function pow "(%1 ^ %2)"

  remove prop Pow_x_zero
  remove prop Pow_x_one
  remove prop Pow_one_y
252
253
254
255
256

end

theory real.Trigonometry

257
258
  syntax function cos "COS(%1)"
  syntax function sin "SIN(%1)"
259
260
261

  syntax function pi "PI"

262
  syntax function tan "TAN(%1)"
263
264

end