Merge branch 'fix_proofs_with_coq_8_19' into 'master'
[why3.git] / drivers / alt_ergo_common.drv
blob7445327fbe78765ab93949a52036cd52a6383e95
1 (* Why drivers for Alt-Ergo: common part *)
3 printer "alt-ergo"
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"
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
24 theory BuiltIn
25   syntax type int   "int"
26   syntax type real  "real"
28   syntax predicate (=)  "(%1 = %2)"
30   meta "eliminate_algebraic" "keep_enums"
31   meta "eliminate_algebraic" "keep_recs"
33 end
35 theory Ignore
36   syntax predicate ignore'term  "true"
37 end
39 theory int.Int
41   prelude "(* this is a prelude for Alt-Ergo integer arithmetic *)"
43   syntax function zero "0"
44   syntax function one  "1"
46   syntax function (+)  "(%1 + %2)"
47   syntax function (-)  "(%1 - %2)"
48   syntax function (*)  "(%1 * %2)"
49   syntax function (-_) "(-%1)"
51   meta "invalid trigger" predicate (<=)
52   meta "invalid trigger" predicate (<)
53   meta "invalid trigger" predicate (>=)
54   meta "invalid trigger" predicate (>)
56   syntax predicate (<=) "(%1 <= %2)"
57   syntax predicate (<)  "(%1 <  %2)"
58   syntax predicate (>=) "(%1 >= %2)"
59   syntax predicate (>)  "(%1 >  %2)"
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
80 end
82 theory int.EuclideanDivision
84   syntax function div "(%1 / %2)"
85   syntax function mod "(%1 % %2)"
87 end
89 theory int.ComputerDivision
91   use for_drivers.ComputerOfEuclideanDivision
93 end
96 theory real.Real
98   prelude "(* this is a prelude for Alt-Ergo real arithmetic *)"
100   syntax function zero "0.0"
101   syntax function one  "1.0"
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)"
110   meta "invalid trigger" predicate (<=)
111   meta "invalid trigger" predicate (<)
112   meta "invalid trigger" predicate (>=)
113   meta "invalid trigger" predicate (>)
115   syntax predicate (<=) "(%1 <= %2)"
116   syntax predicate (<)  "(%1 <  %2)"
117   syntax predicate (>=) "(%1 >= %2)"
118   syntax predicate (>)  "(%1 >  %2)"
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
142 theory real.RealInfix
144   syntax function (+.)  "(%1 + %2)"
145   syntax function (-.)  "(%1 - %2)"
146   syntax function ( *.) "(%1 * %2)"
147   syntax function (/.)  "(%1 / %2)"
148   syntax function (-._) "(-%1)"
150   meta "invalid trigger" predicate (<=.)
151   meta "invalid trigger" predicate (<.)
152   meta "invalid trigger" predicate (>=.)
153   meta "invalid trigger" predicate (>.)
155   syntax predicate (<=.) "(%1 <= %2)"
156   syntax predicate (<.)  "(%1 <  %2)"
157   syntax predicate (>=.) "(%1 >= %2)"
158   syntax predicate (>.)  "(%1 >  %2)"
162 theory Bool
163   syntax type     bool  "bool"
164   syntax function True  "true"
165   syntax function False "false"
168 theory Tuple0
169   syntax type     tuple0 "unit"
170   syntax function Tuple0 "void"
173 theory algebra.AC
174   meta AC function op
175   remove prop Comm
176   remove prop Assoc
179 theory HighOrd
180   syntax type     (->) "(%1,%2) farray"
181   syntax function (@)  "(%1[%2])"
184 theory map.Map
185   syntax function get  "(%1[%2])"
186   syntax function set  "(%1[%2 <- %3])"