drivers/pvs-common.gen

   1
   2 unknown "unfinished" "\"\\0\""
   3 unknown "untried" "\"\\0\""
   4 valid "succeeded"
   5 time "why3cpulimit time : %s s"
   6
   7 (* Performed introductions depending on whether counterexamples are
   8    requested, as said by the meta "get_counterexmp". When this meta
   9    set, this transformation introduces the model variables that are
  10    still embedded in the goal. When it is not set, it removes all
  11    these unused-ce-related variables, even in the context.  *)
  12 transformation "counterexamples_dependent_intros"
  13
  14 (*transformation "inline_trivial"*)
  15 transformation "eliminate_builtin"
  16
  17 (* PVS does not support mutual recursion *)
  18 transformation "eliminate_mutual_recursion"
  19 (* though we could do better, we only use recursion on one argument *)
  20 transformation "eliminate_non_struct_recursion"
  21
  22 transformation "eliminate_literal"
  23 transformation "eliminate_epsilon"
  24
  25 (* PVS only has simple patterns *)
  26 transformation "compile_match"
  27 transformation "eliminate_projections"
  28
  29 transformation "simplify_formula"
  30
  31 theory BuiltIn
  32   syntax type   int   "int"
  33   syntax type   real  "real"
  34   syntax predicate  (=)   "(%1 = %2)"
  35 end
  36
  37 theory Ignore
  38   syntax predicate ignore'term  "TRUE"
  39 end
  40
  41 theory HighOrd
  42   syntax type (->) "[%1 -> %2]"
  43   syntax function (@) "%1(%2)"
  44 end
  45
  46 theory map.Map
  47   syntax function get  "%1(%2)"
  48   syntax function ([]) "%1(%2)"
  49
  50   syntax function set    "(%1 WITH [(%2) |-> %3])"
  51   syntax function ([<-]) "(%1 WITH [(%2) |-> %3])"
  52 end
  53
  54 theory Bool
  55   syntax type bool   "bool"
  56
  57   syntax function True  "TRUE"
  58   syntax function False "FALSE"
  59 end
  60
  61 theory bool.Bool
  62
  63   syntax function andb  "(%1 AND %2)"
  64   syntax function orb   "(%1 OR %2)"
  65   syntax function xorb  "(%1 XOR %2)"
  66   syntax function notb  "(NOT %1)"
  67   syntax function implb "(%1 => %2)"
  68
  69 end
  70
  71 theory int.Int
  72
  73   syntax function zero "0"
  74   syntax function one  "1"
  75
  76   syntax function ( + ) "(%1 + %2)"
  77   syntax function ( - ) "(%1 - %2)"
  78   syntax function ( * ) "(%1 * %2)"
  79   syntax function (-_)  "(-%1)"
  80
  81   syntax predicate (<=) "(%1 <= %2)"
  82   syntax predicate (<)  "(%1 <  %2)"
  83   syntax predicate (>=) "(%1 >= %2)"
  84   syntax predicate (>)  "(%1 >  %2)"
  85
  86   remove prop MulComm.Comm
  87   remove prop MulAssoc.Assoc
  88   remove prop Unit_def_l
  89   remove prop Unit_def_r
  90   remove prop Inv_def_l
  91   remove prop Inv_def_r
  92   remove prop Assoc
  93   remove prop Mul_distr_l
  94   remove prop Mul_distr_r
  95   remove prop Comm
  96   remove prop Unitary
  97   remove prop Refl
  98   remove prop Trans
  99   remove prop Antisymm
 100   remove prop Total
 101   remove prop NonTrivialRing
 102   remove prop CompatOrderAdd
 103   remove prop CompatOrderMult
 104   remove prop ZeroLessOne
 105
 106 end
 107
 108 theory int.Abs
 109
 110   syntax function abs "abs(%1)"
 111
 112   remove prop Abs_pos
 113
 114 end
 115
 116 theory int.MinMax
 117
 118   syntax function min "min(%1, %2)"
 119   syntax function max "max(%1, %2)"
 120
 121 end
 122
 123 theory real.Real
 124
 125   syntax function zero "0"
 126   syntax function one  "1"
 127
 128   syntax function ( + ) "(%1 + %2)"
 129   syntax function ( - ) "(%1 - %2)"
 130   syntax function (-_)  "(-%1)"
 131   syntax function ( * ) "(%1 * %2)"
 132   (* / and inv are defined in the realization *)
 133
 134   syntax predicate (<=) "(%1 <= %2)"
 135   syntax predicate (<)  "(%1 <  %2)"
 136   syntax predicate (>=) "(%1 >= %2)"
 137   syntax predicate (>)  "(%1 >  %2)"
 138
 139   remove prop MulComm.Comm
 140   remove prop MulAssoc.Assoc
 141   remove prop Unit_def_l
 142   remove prop Unit_def_r
 143   remove prop Inv_def_l
 144   remove prop Inv_def_r
 145   remove prop Assoc
 146   remove prop Mul_distr_l
 147   remove prop Mul_distr_r
 148   remove prop Comm
 149   remove prop Unitary
 150   remove prop Inverse
 151   remove prop NonTrivialRing
 152   remove prop CompatOrderAdd
 153   remove prop CompatOrderMult
 154   remove prop ZeroLessOne
 155   remove prop Refl
 156   remove prop Trans
 157   remove prop Antisymm
 158   remove prop Total
 159   remove prop assoc_mul_div
 160   remove prop assoc_div_mul
 161   remove prop assoc_div_div
 162
 163 end
 164
 165 theory real.MinMax
 166   syntax function min "min(%1, %2)"
 167   syntax function max "max(%1, %2)"
 168
 169   remove prop Max_l
 170   remove prop Min_r
 171   remove prop Max_comm
 172   remove prop Min_comm
 173   remove prop Max_assoc
 174   remove prop Min_assoc
 175 end
 176
 177 theory real.RealInfix
 178
 179   syntax function (+.)  "(%1 + %2)"
 180   syntax function (-.)  "(%1 - %2)"
 181   syntax function (-._) "(-%1)"
 182   syntax function ( *.) "(%1 * %2)"
 183   syntax function (/.)  "real@Real.infix_sl(%1, %2)"
 184   syntax function inv   "real@Real.inv(%1)"
 185
 186   syntax predicate (<=.) "(%1 <= %2)"
 187   syntax predicate (<.)  "(%1 <  %2)"
 188   syntax predicate (>=.) "(%1 >= %2)"
 189   syntax predicate (>.)  "(%1 >  %2)"
 190
 191 end
 192
 193 theory real.Abs
 194
 195   syntax function abs "abs(%1)"
 196
 197   remove prop Abs_le
 198   remove prop Abs_pos
 199
 200 end
 201
 202 theory real.FromInt
 203
 204   syntax function from_int "(%1 :: real)"
 205
 206   remove prop Zero
 207   remove prop One
 208   remove prop Add
 209   remove prop Sub
 210   remove prop Mul
 211   remove prop Neg
 212
 213 end
 214
 215 theory real.PowerReal
 216
 217   syntax function pow "(%1 ^ %2)"
 218
 219   remove prop Pow_x_zero
 220   remove prop Pow_x_one
 221   remove prop Pow_one_y
 222
 223 end
 224
 225 (***
 226 theory real.Square
 227
 228   syntax function sqrt "SQRT(%1)"
 229
 230 end
 231
 232 theory real.ExpLog
 233
 234   syntax function exp "EXP(%1)"
 235   syntax function log "LOG(%1)"
 236
 237 end
 238
 239 theory real.Trigonometry
 240
 241   syntax function cos "COS(%1)"
 242   syntax function sin "SIN(%1)"
 243
 244   syntax function pi "PI"
 245
 246   syntax function tan "TAN(%1)"
 247
 248 end
 249 ***)
 250
 251 theory option.Option
 252   syntax type option "lift[%1]"
 253
 254   syntax function None "bottom"
 255   syntax function Some "up(%1)"
 256 end
 257
 258 theory list.List
 259
 260   syntax type list "list[%1]"
 261
 262   syntax function Nil  "(null :: %t0)"
 263   syntax function Cons "cons(%1, %2)"
 264
 265 end
 266
 267 theory list.Length
 268   syntax function length "length(%1)"
 269   remove prop Length_nonnegative
 270   remove prop Length_nil
 271 end
 272
 273 theory list.Mem
 274   syntax predicate mem "member(%1, %2)"
 275
 276 end
 277
 278 theory list.Nth
 279   syntax function nth
 280     "IF 0 <= %1 AND %1 < length(%2) THEN up(nth(%2, %1)) ELSE bottom ENDIF"
 281 end
 282
 283 theory list.Append
 284   syntax function (++) "append(%1, %2)"
 285
 286   remove prop Append_assoc
 287   remove prop Append_l_nil
 288   remove prop Append_length
 289   (* FIXME? the following are not part of PVS prelude *)
 290   remove prop mem_append
 291   remove prop mem_decomp
 292 end
 293
 294 theory list.Reverse
 295   syntax function reverse "reverse(%1)"
 296 end
 297
 298 theory set.Set
 299   syntax type set "set[%1]"
 300
 301   syntax predicate mem "member(%1, %2)"
 302 (*  remove prop      extensionality not present anymore *)
 303
 304   syntax predicate subset "subset?(%1, %2)"
 305   remove prop      subset_trans
 306
 307   syntax function  empty    "(emptyset :: %t0)"
 308   syntax predicate is_empty "empty?(%1)"
 309   remove prop      is_empty_empty
 310
 311   syntax function add "add(%1, %2)"
 312   syntax function singleton "singleton(%1)"
 313
 314   syntax function remove "remove(%1, %2)"
 315   remove prop     subset_remove
 316
 317   syntax function union "union(%1, %2)"
 318
 319   syntax function inter "intersection(%1, %2)"
 320
 321   syntax function diff "difference(%1, %2)"
 322   remove prop     subset_diff
 323
 324   (* TODO: choose *)
 325
 326   syntax function all "fullset"
 327 end
 328
 329 theory set.Fset
 330   syntax type fset "finite_set[%1]"
 331
 332   syntax predicate mem "member(%1, %2)"
 333   remove prop      extensionality
 334
 335   syntax predicate subset "subset?(%1, %2)"
 336   remove prop      subset_trans
 337
 338   syntax function  empty    "(emptyset :: %t0)"
 339   syntax predicate is_empty "empty?(%1)"
 340   remove prop      is_empty_empty
 341   remove prop      empty_is_empty
 342
 343   syntax function add "add(%1, %2)"
 344   remove prop     add_def
 345   syntax function singleton "singleton(%1)"
 346
 347   syntax function remove "remove(%1, %2)"
 348   remove prop     remove_def
 349   remove prop     subset_remove
 350
 351   syntax function union "union(%1, %2)"
 352   remove prop     union_def
 353
 354   syntax function inter "intersection(%1, %2)"
 355   remove prop     inter_def
 356
 357   syntax function diff "difference(%1, %2)"
 358   remove prop     diff_def
 359   remove prop     subset_diff
 360
 361   (* TODO: choose *)
 362
 363   syntax function cardinal "Card(%1)"
 364   remove prop     cardinal_nonneg
 365   remove prop     cardinal_empty
 366   remove prop     cardinal_add
 367   remove prop     cardinal_remove
 368   remove prop     cardinal_subset
 369   remove prop     cardinal1
 370
 371   (* TODO: nth *)
 372 end
 373
 374 (* this file has an extension .aux rather than .gen
 375    since it should not be distributed *)
 376 import "pvs-realizations.aux"