alt_ergo.drv 2.7 KB
Newer Older
1 2 3 4 5 6

(* Why driver for Alt-Ergo *)

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

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

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

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

18
transformation "eliminate_builtin"
19
transformation "eliminate_mutual_recursion"
20
transformation "eliminate_inductive"
21
transformation "eliminate_algebraic"
22
transformation "eliminate_if"
23
transformation "eliminate_let"
24
transformation "simplify_formula"
25
transformation "simplify_trivial_quantification_in_goal"
26 27 28 29 30 31 32 33

theory BuiltIn
  syntax type int "int"
  syntax type real "real"
  syntax logic (_=_) "(%1 = %2)"
  syntax logic (_<>_) "(%1 <> %2)"
end

34
theory int.Int
35

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

  syntax logic zero "0"
39
  syntax logic one  "1"
40 41 42 43 44 45 46

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

  syntax logic (_<=_) "(%1 <= %2)"
47
  syntax logic (_<_) "(%1 <  %2)"
48
  syntax logic (_>=_) "(%1 >= %2)"
49
  syntax logic (_>_) "(%1 >  %2)"
50

51 52 53 54 55
  remove prop CommutativeGroup.Comm.Comm
  remove prop CommutativeGroup.Assoc.Assoc
  remove prop CommutativeGroup.Unit_def
  remove prop CommutativeGroup.Inv_def
  remove prop Assoc.Assoc
56
  remove prop Mul_distr
57 58
  remove prop Comm.Comm
  remove prop Unitary
59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97
  remove prop Refl
  remove prop Trans
  remove prop Total
  remove prop Antisymm

end

theory real.Real

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

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

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

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

  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
98 99 100

end

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
101 102 103 104 105 106 107 108 109 110 111
theory bool.Bool
  syntax type  bool  "bool"
  syntax logic True  "true"
  syntax logic False "false"
end

theory unit.Unit
  syntax type  unit "unit"
  syntax logic Unit "void"
end

112 113
theory algebra.AC
  tag cloned logic op "AC"
114 115
  remove cloned prop Comm.Comm
  remove cloned prop Assoc.Assoc
116 117 118 119 120
end

(*
Local Variables: 
mode: why
121
compile-command: "make -C .. bench"
122 123
End: 
*)