alt_ergo_common.drv 4.73 KB
Newer Older
1
(* Why drivers for Alt-Ergo: common part *)
2

3
prelude "(* this is the prelude for Alt-Ergo, version >= 0.95.2 *)"
4 5 6 7

printer "alt-ergo"
filename "%f-%t-%g.why"

8 9 10 11 12
valid "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:Valid"
invalid "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:Invalid"
unknown "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:I don't know" ""
timeout "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:Timeout"
steplimitexceeded "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:Steps limit reached"
13
outofmemory "Fatal error: out of memory"
14
outofmemory "Fatal error: exception Stack_overflow"
15
fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"
16 17 18 19
time "Valid (%s)"
time "Valid (%s)"
steps "Valid (\\([0-9]+.?[0-9]*\\)) (\\([0-9]+.?[0-9]*\\))" 2
steps "Valid (\\([0-9]+.?[0-9]*\\)) (\\([0-9]+.?[0-9]*\\) steps)" 2
20 21 22 23 24 25 26 27
time "why3cpulimit time : %s s"

(* À discuter *)
transformation "inline_trivial"

transformation "eliminate_builtin"
transformation "eliminate_recursion"
transformation "eliminate_inductive"
28
transformation "eliminate_algebraic"
29
transformation "eliminate_epsilon"
30 31 32
transformation "eliminate_if"
transformation "eliminate_let"

33
transformation "split_premise_right"
34 35 36 37 38 39 40 41
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification_in_goal"*)

theory BuiltIn
  syntax type int   "int"
  syntax type real  "real"

  syntax predicate (=)  "(%1 = %2)"
42 43 44 45

  meta "eliminate_algebraic" "keep_enums"
  meta "eliminate_algebraic" "keep_recs"

46 47 48 49 50 51 52 53 54 55 56 57 58 59
end

theory int.Int

  prelude "(* this is a prelude for Alt-Ergo integer arithmetic *)"

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

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

60 61 62 63 64
  meta "invalid trigger" predicate (<=)
  meta "invalid trigger" predicate (<)
  meta "invalid trigger" predicate (>=)
  meta "invalid trigger" predicate (>)

65 66 67 68 69 70
  syntax predicate (<=) "(%1 <= %2)"
  syntax predicate (<)  "(%1 <  %2)"
  syntax predicate (>=) "(%1 >= %2)"
  syntax predicate (>)  "(%1 >  %2)"

  remove prop CommutativeGroup.Comm.Comm
71 72 73 74 75
  remove prop CommutativeGroup.Assoc
  remove prop CommutativeGroup.Unit_def_l
  remove prop CommutativeGroup.Unit_def_r
  remove prop CommutativeGroup.Inv_def_l
  remove prop CommutativeGroup.Inv_def_r
76
  remove prop Assoc.Assoc
77 78
  remove prop Mul_distr_l
  remove prop Mul_distr_r
79 80 81 82 83 84 85 86
  remove prop Comm.Comm
  remove prop Unitary
  remove prop Refl
  remove prop Trans
  remove prop Total
  remove prop Antisymm
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
87
  remove prop ZeroLessOne
88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105

end


theory real.Real

  prelude "(* this is a prelude for Alt-Ergo real arithmetic *)"

  syntax function zero "0.0"
  syntax function one  "1.0"

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

106 107 108 109 110
  meta "invalid trigger" predicate (<=)
  meta "invalid trigger" predicate (<)
  meta "invalid trigger" predicate (>=)
  meta "invalid trigger" predicate (>)

111 112 113 114 115 116
  syntax predicate (<=) "(%1 <= %2)"
  syntax predicate (<)  "(%1 <  %2)"
  syntax predicate (>=) "(%1 >= %2)"
  syntax predicate (>)  "(%1 >  %2)"

  remove prop CommutativeGroup.Comm.Comm
117 118 119 120 121
  remove prop CommutativeGroup.Assoc
  remove prop CommutativeGroup.Unit_def_l
  remove prop CommutativeGroup.Unit_def_r
  remove prop CommutativeGroup.Inv_def_l
  remove prop CommutativeGroup.Inv_def_r
122
  remove prop Assoc.Assoc
123 124
  remove prop Mul_distr_l
  remove prop Mul_distr_r
125 126 127 128 129 130 131 132 133
  remove prop Comm.Comm
  remove prop Unitary
  remove prop Refl
  remove prop Trans
  remove prop Total
  remove prop Antisymm
  remove prop Inverse
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
134
  remove prop ZeroLessOne
135 136 137 138 139 140 141 142 143 144 145

end

theory real.RealInfix

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

146 147 148 149 150
  meta "invalid trigger" predicate (<=.)
  meta "invalid trigger" predicate (<.)
  meta "invalid trigger" predicate (>=.)
  meta "invalid trigger" predicate (>.)

151 152 153 154 155 156 157
  syntax predicate (<=.) "(%1 <= %2)"
  syntax predicate (<.)  "(%1 <  %2)"
  syntax predicate (>=.) "(%1 >= %2)"
  syntax predicate (>.)  "(%1 >  %2)"

end

158
theory Bool
159 160 161 162 163 164 165 166 167 168 169
  syntax type     bool  "bool"
  syntax function True  "true"
  syntax function False "false"
end

theory Tuple0
  syntax type     tuple0 "unit"
  syntax function Tuple0 "void"
end

theory algebra.AC
170 171 172
  meta AC function op
  remove prop Comm.Comm
  remove prop Assoc
173
end
174 175 176 177 178 179 180 181 182 183

theory map.Map
  syntax type  map "(%1,%2) farray"

  syntax function get "(%1[%2])"
  syntax function set "(%1[%2 <- %3])"

  remove prop Select_eq
  remove prop Select_neq
end