Commit babd2215 authored by MARCHE Claude's avatar MARCHE Claude

coq driver

parent 1f8b1e1a
......@@ -178,10 +178,12 @@ test: bin/why.byte $(TOOLS)
--output-file tmp.v --goal Test.G src/test.why
echo bin/why.byte --call --timeout 1 --driver drivers/alt_ergo.drv -I theories/ \
--all-goals theories/real.why
@rm -rf theories/coq
@mkdir -p theories/coq
@printf "*** Checking Coq file generation ***\\n"
@for i in int.Abs int.EuclideanDivision int.ComputerDivision \
real.Abs real.FromIntTest real.ExpLog real.Trigonometric \
real.Abs real.FromIntTest real.SquareTest \
real.ExpLogTest real.PowerTest real.TrigonometryTest \
floating_point.Test array.TestBv32 \
; do \
printf "Generating Coq file for $$i\\n" && bin/why.byte \
......
......@@ -108,3 +108,47 @@ theory real.FromInt
end
theory real.Square
prelude "Require Import R_sqrt."
syntax logic sqr "(Rsqr %1)"
syntax logic sqrt "(sqrt %1)" (* and not Rsqrt *)
end
theory real.ExpLog
prelude "Require Import Rtrigo_def."
prelude "Require Import Rpower."
syntax logic exp "(exp %1)"
syntax logic log "(ln %1)"
end
theory real.Power
prelude "Require Import Rpower."
(* no power: R -> R -> R in Coq ? (only powerRZ: R -> Z -> R) *)
end
theory real.Trigonometry
prelude "Require Import Rtrigo."
prelude "Require Import AltSeries." (* for def of pi *)
syntax logic cos "(cos %1)"
syntax logic sin "(sin %1)"
syntax logic pi "PI"
syntax logic tan "(tan %1)"
(* syntax logic atan "atan not defined in Coq ?" *)
end
......@@ -86,6 +86,7 @@ theory BV32
end
theory TestBv32
use import BV32
......
......@@ -151,6 +151,16 @@ theory Square
end
theory SquareTest
use import Square
lemma Sqrt_zero: sqrt(0.0) = 0.0
lemma Sqrt_one: sqrt(1.0) = 1.0
lemma Sqrt_four: sqrt(4.0) = 2.0
end
theory ExpLog
use import Real
......@@ -168,8 +178,6 @@ theory ExpLog
axiom Log_exp: forall x:real. log(exp(x)) = x
lemma Log_e : log(e) = 1.0
axiom Exp_log: forall x:real. x > 0.0 -> exp(log(x)) = x
logic log2(x:real) : real = log(x)/log(2.0)
......@@ -177,6 +185,15 @@ theory ExpLog
end
theory ExpLogTest
use import ExpLog
lemma Log_e : log(e) = 1.0
end
theory Power
use import Real
......@@ -208,10 +225,20 @@ theory Power
end
theory PowerTest
use import Power
lemma Pow_2_2 : pow(2.0,2.0) = 4.0
end
(** Trigonometric functions
[http://en.wikipedia.org/wiki/Trigonometric_function]
*)
theory Trigonometric
theory Trigonometry
use import Real
use import Square
......@@ -260,6 +287,19 @@ theory Trigonometric
end
theory TrigonometryTest
use import Real
use import Trigonometry
use import Square
lemma Cos_2_pi : cos(2.0 * pi) = 1.0
lemma Sin_2_pi : cos(2.0 * pi) = 0.
lemma Tan_pi_3 : tan(pi / 2.0) = sqrt(3.0)
lemma Atan_1 : atan(1.0) = pi / 4.0
end
(** hyperbolic functions
[http://en.wikipedia.org/wiki/Hyperbolic_function]
*)
......@@ -290,7 +330,7 @@ theory Polar
use import Real
use import Square
use import Trigonometric
use import Trigonometry
logic hypot(x:real,y:real) : real = sqrt(sqr(x)+sqr(y))
logic atan2(real,real) : real
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment