alt_ergo.drv 1.38 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17

(* Why driver for Alt-Ergo *)

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

printer "alt-ergo"
filename "%f-%t-%s.why"
call_on_file  "alt-ergo %s"

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

(* À discuter *)
transformations
  "simplify_recursive_definition"      
18
  (*"split_goal_pos_neg_goal"*) "split_goal_pos_neg_all"
19 20 21 22 23 24 25 26 27 28 29 30 31 32 33
  "inline_trivial"
end


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 37 38 39 40 41 42 43 44 45

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

  syntax logic zero "0"

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

  syntax logic (_<=_) "(%1 <= %2)"
46
  syntax logic (_<_) "(%1 <  %2)"
47
  syntax logic (_>=_) "(%1 >= %2)"
48
  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 62

end

theory algebra.AC
  tag cloned logic op "AC"
63 64
  remove cloned prop Comm.Comm
  remove cloned prop Assoc.Assoc
65 66 67 68 69 70 71 72
end

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