alt_ergo.drv

(* Why driver for Alt-Ergo *)

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

printer "alt-ergo"

call_on_file  "alt-ergo %s"


theory BuiltIn
  syntax type int "int"
  syntax type real "real"

  syntax logic (_=_) "(%1 = %1)"

 (* inutile car  "<>" devient "not =" *)
  syntax logic (_<>_) "(%1 = %1)"

end


theory prelude.Int

  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 / %2)"
  syntax logic (-_)  "(-%1)"

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

  remove prop One_neutral
  remove prop Add_assoc
  remove prop Add_comm
  remove prop Zero_neutral
  remove prop Neg
  remove prop Mul_comm
  remove prop Mul_assoc
  remove prop Mul_distr

end

theory algebra.AC
  tag logic cloned op "AC"
  remove prop cloned Comm
  remove prop cloned Assoc
end

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