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

3
prelude "(* this is the prelude for Alt-Ergo, any versions *)"
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 42 43 44 45 46 47 48 49 50 51 52 53 54 55
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification_in_goal"*)

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

  syntax predicate (=)  "(%1 = %2)"
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)"

56 57 58 59 60
  meta "invalid trigger" predicate (<=)
  meta "invalid trigger" predicate (<)
  meta "invalid trigger" predicate (>=)
  meta "invalid trigger" predicate (>)

61 62 63 64 65 66
  syntax predicate (<=) "(%1 <= %2)"
  syntax predicate (<)  "(%1 <  %2)"
  syntax predicate (>=) "(%1 >= %2)"
  syntax predicate (>)  "(%1 >  %2)"

  remove prop CommutativeGroup.Comm.Comm
67 68 69 70 71
  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
72
  remove prop Assoc.Assoc
73 74
  remove prop Mul_distr_l
  remove prop Mul_distr_r
75 76 77 78 79 80 81 82
  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
83
  remove prop ZeroLessOne
84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101

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)"

102 103 104 105 106
  meta "invalid trigger" predicate (<=)
  meta "invalid trigger" predicate (<)
  meta "invalid trigger" predicate (>=)
  meta "invalid trigger" predicate (>)

107 108 109 110 111 112
  syntax predicate (<=) "(%1 <= %2)"
  syntax predicate (<)  "(%1 <  %2)"
  syntax predicate (>=) "(%1 >= %2)"
  syntax predicate (>)  "(%1 >  %2)"

  remove prop CommutativeGroup.Comm.Comm
113 114 115 116 117
  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
118
  remove prop Assoc.Assoc
119 120
  remove prop Mul_distr_l
  remove prop Mul_distr_r
121 122 123 124 125 126 127 128 129
  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
130
  remove prop ZeroLessOne
131 132 133 134 135 136 137 138 139 140 141

end

theory real.RealInfix

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

142 143 144 145 146
  meta "invalid trigger" predicate (<=.)
  meta "invalid trigger" predicate (<.)
  meta "invalid trigger" predicate (>=.)
  meta "invalid trigger" predicate (>.)

147 148 149 150 151 152 153
  syntax predicate (<=.) "(%1 <= %2)"
  syntax predicate (<.)  "(%1 <  %2)"
  syntax predicate (>=.) "(%1 >= %2)"
  syntax predicate (>.)  "(%1 >  %2)"

end

154
theory Bool
155 156 157 158 159 160 161 162 163 164 165
  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
166 167 168
  meta AC function op
  remove prop Comm.Comm
  remove prop Assoc
169
end
170 171 172 173 174 175 176 177 178 179

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