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