drivers/alt_ergo_common.drv

   1 (* Why drivers for Alt-Ergo: common part *)
   2
   3 printer "alt-ergo"
   4
   5 valid "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+: ?Valid"
   6 invalid "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+: ?Invalid"
   7 unknown "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+: ?I don't know" ""
   8 timeout "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+: ?Timeout"
   9 timeout "^Timeout$"
  10 steplimitexceeded "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+: ?Steps limit reached"
  11 steplimitexceeded "^Steps limit reached"
  12 steplimitexceeded "^\\[Error\\]Fatal Error: Steps limit reached"
  13 outofmemory "Fatal error: out of memory"
  14 outofmemory "Fatal error: Out of memory"
  15 outofmemory "Fatal error: exception Stack_overflow"
  16 outofmemory "Fatal error: exception Out of memory"
  17
  18 fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"
  19 steps "Valid (\\([0-9]+.?[0-9]*\\)) (\\([0-9]+.?[0-9]*\\))" 2
  20 steps "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:.*(\\([0-9]+.?[0-9]*\\) steps)" 1
  21 steps "^Steps limit reached: \\([0-9]+.?[0-9]*\\)" 1
  22 steps "^\\[Error\\]Fatal Error: Steps limit reached: \\([0-9]+.?[0-9]*\\)" 1
  23
  24 theory BuiltIn
  25   syntax type int   "int"
  26   syntax type real  "real"
  27
  28   syntax predicate (=)  "(%1 = %2)"
  29
  30   meta "eliminate_algebraic" "keep_enums"
  31   meta "eliminate_algebraic" "keep_recs"
  32
  33 end
  34
  35 theory Ignore
  36   syntax predicate ignore'term  "true"
  37 end
  38
  39 theory int.Int
  40
  41   prelude "(* this is a prelude for Alt-Ergo integer arithmetic *)"
  42
  43   syntax function zero "0"
  44   syntax function one  "1"
  45
  46   syntax function (+)  "(%1 + %2)"
  47   syntax function (-)  "(%1 - %2)"
  48   syntax function (*)  "(%1 * %2)"
  49   syntax function (-_) "(-%1)"
  50
  51   meta "invalid trigger" predicate (<=)
  52   meta "invalid trigger" predicate (<)
  53   meta "invalid trigger" predicate (>=)
  54   meta "invalid trigger" predicate (>)
  55
  56   syntax predicate (<=) "(%1 <= %2)"
  57   syntax predicate (<)  "(%1 <  %2)"
  58   syntax predicate (>=) "(%1 >= %2)"
  59   syntax predicate (>)  "(%1 >  %2)"
  60
  61   remove prop MulComm.Comm
  62   remove prop MulAssoc.Assoc
  63   remove prop Unit_def_l
  64   remove prop Unit_def_r
  65   remove prop Inv_def_l
  66   remove prop Inv_def_r
  67   remove prop Assoc
  68   remove prop Mul_distr_l
  69   remove prop Mul_distr_r
  70   remove prop Comm
  71   remove prop Unitary
  72   remove prop Refl
  73   remove prop Trans
  74   remove prop Total
  75   remove prop Antisymm
  76   remove prop NonTrivialRing
  77   remove prop CompatOrderAdd
  78   remove prop ZeroLessOne
  79
  80 end
  81
  82 theory int.EuclideanDivision
  83
  84   syntax function div "(%1 / %2)"
  85   syntax function mod "(%1 % %2)"
  86
  87 end
  88
  89 theory int.ComputerDivision
  90
  91   use for_drivers.ComputerOfEuclideanDivision
  92
  93 end
  94
  95
  96 theory real.Real
  97
  98   prelude "(* this is a prelude for Alt-Ergo real arithmetic *)"
  99
 100   syntax function zero "0.0"
 101   syntax function one  "1.0"
 102
 103   syntax function (+)  "(%1 + %2)"
 104   syntax function (-)  "(%1 - %2)"
 105   syntax function (*)  "(%1 * %2)"
 106   syntax function (/)  "(%1 / %2)"
 107   syntax function (-_) "(-%1)"
 108   syntax function inv  "(1.0 / %1)"
 109
 110   meta "invalid trigger" predicate (<=)
 111   meta "invalid trigger" predicate (<)
 112   meta "invalid trigger" predicate (>=)
 113   meta "invalid trigger" predicate (>)
 114
 115   syntax predicate (<=) "(%1 <= %2)"
 116   syntax predicate (<)  "(%1 <  %2)"
 117   syntax predicate (>=) "(%1 >= %2)"
 118   syntax predicate (>)  "(%1 >  %2)"
 119
 120   remove prop MulComm.Comm
 121   remove prop MulAssoc.Assoc
 122   remove prop Unit_def_l
 123   remove prop Unit_def_r
 124   remove prop Inv_def_l
 125   remove prop Inv_def_r
 126   remove prop Assoc
 127   remove prop Mul_distr_l
 128   remove prop Mul_distr_r
 129   remove prop Comm
 130   remove prop Unitary
 131   remove prop Refl
 132   remove prop Trans
 133   remove prop Total
 134   remove prop Antisymm
 135   remove prop Inverse
 136   remove prop NonTrivialRing
 137   remove prop CompatOrderAdd
 138   remove prop ZeroLessOne
 139
 140 end
 141
 142 theory real.RealInfix
 143
 144   syntax function (+.)  "(%1 + %2)"
 145   syntax function (-.)  "(%1 - %2)"
 146   syntax function ( *.) "(%1 * %2)"
 147   syntax function (/.)  "(%1 / %2)"
 148   syntax function (-._) "(-%1)"
 149
 150   meta "invalid trigger" predicate (<=.)
 151   meta "invalid trigger" predicate (<.)
 152   meta "invalid trigger" predicate (>=.)
 153   meta "invalid trigger" predicate (>.)
 154
 155   syntax predicate (<=.) "(%1 <= %2)"
 156   syntax predicate (<.)  "(%1 <  %2)"
 157   syntax predicate (>=.) "(%1 >= %2)"
 158   syntax predicate (>.)  "(%1 >  %2)"
 159
 160 end
 161
 162 theory Bool
 163   syntax type     bool  "bool"
 164   syntax function True  "true"
 165   syntax function False "false"
 166 end
 167
 168 theory Tuple0
 169   syntax type     tuple0 "unit"
 170   syntax function Tuple0 "void"
 171 end
 172
 173 theory algebra.AC
 174   meta AC function op
 175   remove prop Comm
 176   remove prop Assoc
 177 end
 178
 179 theory HighOrd
 180   syntax type     (->) "(%1,%2) farray"
 181   syntax function (@)  "(%1[%2])"
 182 end
 183
 184 theory map.Map
 185   syntax function get  "(%1[%2])"
 186   syntax function set  "(%1[%2 <- %3])"
 187 end