Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

coq.drv 2.06 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
  syntax logic  (_<>_)  "(%1 <> %2)"
end

MARCHE Claude's avatar
MARCHE Claude committed
20 21 22 23 24 25 26 27 28 29 30 31 32 33
theory bool.Bool

  syntax type bool "bool"

  syntax logic True "true"
  syntax logic False "false"

  syntax logic andb "(andb %1 %2)"
  syntax logic orb "(orb %1 %2)"
  syntax logic xorb "(xorb %1 %2)"
  syntax logic notb "(negb %1)"

end

MARCHE Claude's avatar
MARCHE Claude committed
34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60

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
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 98 99 100 101 102 103 104
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

MARCHE Claude's avatar
MARCHE Claude committed
105 106 107 108 109 110
theory real.FromInt

  syntax logic from_int "(IZR %1)"

end