coq.drv 1.77 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4 5

printer "coq"
filename "%f_%t_%s.v"
call_on_file "coqc %s"

MARCHE Claude's avatar
MARCHE Claude committed
6

MARCHE Claude's avatar
MARCHE Claude committed
7
prelude "(* generated by Why3's Coq driver *)" 
MARCHE Claude's avatar
MARCHE Claude committed
8

MARCHE Claude's avatar
MARCHE Claude committed
9
theory BuiltIn
MARCHE Claude's avatar
MARCHE Claude committed
10 11 12 13

  prelude "Require Import ZArith."
  prelude "Require Import Rbase."

MARCHE Claude's avatar
MARCHE Claude committed
14 15
  syntax type   int     "Z"
  syntax type   real    "R"
MARCHE Claude's avatar
MARCHE Claude committed
16
  syntax logic  (_=_)   "(%1 = %2)" 
MARCHE Claude's avatar
MARCHE Claude committed
17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46
  syntax logic  (_<>_)  "(%1 <> %2)"
end


theory int.Int

  syntax logic zero "0%Z"
  syntax logic one "1%Z"

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

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

  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

end

MARCHE Claude's avatar
MARCHE Claude committed
47 48 49 50 51 52 53 54 55 56 57 58 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
theory int.Abs

  syntax logic abs "(Zabs %1)"

end

theory real.Real

  syntax logic zero "0%R"
  syntax logic one "1%R"

  syntax logic (_+_) "(%1 + %2)%R"
  syntax logic (_-_) "(%1 - %2)%R"
  syntax logic (-_)  "(-%1)%R"
  syntax logic (_*_) "(%1 * %2)%R"
  syntax logic (_/_) "(Rdiv %1 %2)%R"
  syntax logic inv  "(Rinv %1)"

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

  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 Inverse

end


theory real.Abs

  prelude "Require Import Rbasic_fun."

  syntax logic abs "(Rabs %1)"

end