alt_ergo.drv 3.36 KB
Newer Older
1
2
3
4
5
(* Why driver for Alt-Ergo *)

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

printer "alt-ergo"
6
filename "%f-%t-%g.why"
7
8
9
10
11
12
13

valid "Valid"
invalid "Invalid"
unknown "I don't know" "Unknown"
fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"

(* À discuter *)
14
transformation "simplify_recursive_definition"
15
16
transformation "inline_trivial"

17
transformation "eliminate_builtin"
Andrei Paskevich's avatar
Andrei Paskevich committed
18
transformation "eliminate_recursion"
19
transformation "eliminate_inductive"
20
transformation "eliminate_algebraic"
21
transformation "eliminate_if"
22
transformation "eliminate_let"
23

24
transformation "simplify_formula"
25
transformation "simplify_trivial_quantification_in_goal"
26
27

theory BuiltIn
28
29
30
  syntax type int   "int"
  syntax type real  "real"
  syntax logic (=)  "(%1 = %2)"
31
32
end

33
theory int.Int
34

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

  syntax logic zero "0"
38
  syntax logic one  "1"
39

40
41
42
43
  syntax logic (+)  "(%1 + %2)"
  syntax logic (-)  "(%1 - %2)"
  syntax logic (*)  "(%1 * %2)"
  syntax logic (-_) "(-%1)"
44

45
46
47
48
  syntax logic (<=) "(%1 <= %2)"
  syntax logic (<)  "(%1 <  %2)"
  syntax logic (>=) "(%1 >= %2)"
  syntax logic (>)  "(%1 >  %2)"
49

50
51
52
53
54
  remove prop CommutativeGroup.Comm.Comm
  remove prop CommutativeGroup.Assoc.Assoc
  remove prop CommutativeGroup.Unit_def
  remove prop CommutativeGroup.Inv_def
  remove prop Assoc.Assoc
55
  remove prop Mul_distr
56
57
  remove prop Comm.Comm
  remove prop Unitary
58
59
60
61
  remove prop Refl
  remove prop Trans
  remove prop Total
  remove prop Antisymm
62
63
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
64
65
66

end

MARCHE Claude's avatar
MARCHE Claude committed
67
68
69
theory int.EuclideanDivision

  syntax logic div "(%1 / %2)"
70
  syntax logic mod "(%1 % %2)"
MARCHE Claude's avatar
MARCHE Claude committed
71
72
73
74

end


75
76
77
78
79
80
81
theory real.Real

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

  syntax logic zero "0.0"
  syntax logic one  "1.0"

82
83
84
85
86
87
  syntax logic (+)  "(%1 + %2)"
  syntax logic (-)  "(%1 - %2)"
  syntax logic (*)  "(%1 * %2)"
  syntax logic (/)  "(%1 / %2)"
  syntax logic (-_) "(-%1)"
  syntax logic inv  "(1.0 / %1)"
88

89
90
91
92
  syntax logic (<=) "(%1 <= %2)"
  syntax logic (<)  "(%1 <  %2)"
  syntax logic (>=) "(%1 >= %2)"
  syntax logic (>)  "(%1 >  %2)"
93
94
95
96
97
98
99
100
101
102
103
104
105
106

  remove prop CommutativeGroup.Comm.Comm
  remove prop CommutativeGroup.Assoc.Assoc
  remove prop CommutativeGroup.Unit_def
  remove prop CommutativeGroup.Inv_def
  remove prop Assoc.Assoc
  remove prop Mul_distr
  remove prop Comm.Comm
  remove prop Unitary
  remove prop Refl
  remove prop Trans
  remove prop Total
  remove prop Antisymm
  remove prop Inverse
107
108
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
109
110
111

end

MARCHE Claude's avatar
MARCHE Claude committed
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
theory real.RealInfix

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

  syntax logic (<=.) "(%1 <= %2)"
  syntax logic (<.)  "(%1 <  %2)"
  syntax logic (>=.) "(%1 >= %2)"
  syntax logic (>.)  "(%1 >  %2)"

end

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
127
128
129
130
131
132
theory bool.Bool
  syntax type  bool  "bool"
  syntax logic True  "true"
  syntax logic False "false"
end

133
134
135
theory Tuple0
  syntax type  tuple0 "unit"
  syntax logic Tuple0 "void"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
136
137
end

138
theory algebra.AC
139
  meta cloned AC logic op
140
141
  remove cloned prop Comm.Comm
  remove cloned prop Assoc.Assoc
142
143
end

144
145
146
147
148
149
150
151
152
153
(*
theory array.ArrayLength
  syntax type  t      "%1 farray"
  syntax logic select "(%1[%2])"
  syntax logic store  "(%1[%2 <- %3])"
  remove prop  Select_eq
  remove prop  Select_neq
end
*)

154
(*
155
Local Variables:
156
mode: why
157
compile-command: "make -C .. bench"
158
End:
159
*)