Commit 1009c5dc authored by MARCHE Claude's avatar MARCHE Claude

Reals: separate PowerInt and PowerReal, add realization of RealInfix

parent 8b002d87
...@@ -837,7 +837,7 @@ ifeq (@enable_coq_libs@,yes) ...@@ -837,7 +837,7 @@ ifeq (@enable_coq_libs@,yes)
COQLIBS_INT_FILES = Abs ComputerDivision EuclideanDivision Int MinMax COQLIBS_INT_FILES = Abs ComputerDivision EuclideanDivision Int MinMax
COQLIBS_INT = $(addprefix lib/coq/int/, $(COQLIBS_INT_FILES)) COQLIBS_INT = $(addprefix lib/coq/int/, $(COQLIBS_INT_FILES))
COQLIBS_REAL_FILES = Abs ExpLog FromInt MinMax Real Square COQLIBS_REAL_FILES = Abs ExpLog FromInt MinMax Real Square RealInfix
COQLIBS_REAL = $(addprefix lib/coq/real/, $(COQLIBS_REAL_FILES)) COQLIBS_REAL = $(addprefix lib/coq/real/, $(COQLIBS_REAL_FILES))
ifeq (@enable_coq_fp_libs@,yes) ifeq (@enable_coq_fp_libs@,yes)
......
...@@ -133,8 +133,12 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990 ...@@ -133,8 +133,12 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
ne pas oublier de dire que les dependances avec le .why ou .mlw: ne sera pas vérifié ne pas oublier de dire que les dependances avec le .why ou .mlw: ne sera pas vérifié
- (WHO?) revoir documentation du smoke detector - (WHO?) revoir documentation du smoke detector
- (WHO?) Documenter l'utilisation de plusieurs version du meme prouveur comme CVC3 et Z3 - (WHO?) Documenter l'utilisation de plusieurs version du meme prouveur comme CVC3 et Z3
- (CLAUDE) Documenter les popups qui peuvent apparaitre dans why3ide quand les prouveurs ont changé - (CLAUDE) Documenter les popups qui peuvent apparaitre dans why3ide quand les prouveurs ont changé. Et les mettre au point:
ET LES METTRE AU POINT . Lors d'un replay, le dialogue "replace proof" apparait un nombre important de fois,
il faut absolument pouvoir interrompre, ou donner une reponse qui soit appliquée pour le reste.
(le 3e bouton "never replace..." ne semble pas jourer ce role...)
. le dialogue "replace proof" est de toute facon trop large, et les choix possibles sont confus.
- DONE (ANDREI) ajouter option a why3config pour ajouter association ident-executable - DONE (ANDREI) ajouter option a why3config pour ajouter association ident-executable
- (CLAUDE) meme ordre d'idee: ne pas ecraser "default editor" et "timelimit" - (CLAUDE) meme ordre d'idee: ne pas ecraser "default editor" et "timelimit"
- (WHO?) complete api.tex: explain how to build theories, apply - (WHO?) complete api.tex: explain how to build theories, apply
......
...@@ -256,11 +256,20 @@ theory real.ExpLog ...@@ -256,11 +256,20 @@ theory real.ExpLog
end end
theory real.Power theory real.PowerInt
prelude "Require Import Rpower." prelude "Require Import Rpower."
(* no power: R -> R -> R in Coq ? (only powerRZ: R -> Z -> R) *) syntax function power "(powerRZ %1)"
end
theory real.PowerReal
prelude "Require Import Rpower."
syntax function pow "(Rpower %1)"
end end
theory real.Trigonometry theory real.Trigonometry
......
...@@ -242,7 +242,7 @@ theory real.ExpLog ...@@ -242,7 +242,7 @@ theory real.ExpLog
end end
theory real.Power theory real.PowerReal
syntax function pow "(%1 ^ %2)" syntax function pow "(%1 ^ %2)"
......
...@@ -2,5 +2,15 @@ theory Test ...@@ -2,5 +2,15 @@ theory Test
use import real.Real use import real.Real
goal G1 : 5.5 * 10. = 55. goal G1 : 5.5 * 10. = 55.
goal G2 : 9. / 3. = 3. goal G2 : 9. / 3. = 3.
goal G3 : inv(5.) = 0.2 goal G3 : inv 5. = 0.2
end
theory TestInfix
use import real.RealInfix
goal Add : 5.5 +. 10. = 15.5
goal Sub : 9. -. 3. = 6.
goal Neg : -. 5. +. 3.5 = -. 1.5
goal Mul : 5.5 *. 10. = 55.
goal Div : 9. /. 2. = 4.5
goal Inv : inv 5. = 0.2
end end
<?xml version="1.0" encoding="UTF-8"?> <?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd"> <!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session <why3session
name="check-builtin/real/why3session.xml"> name="real/why3session.xml">
<prover <prover
id="0" id="0"
name="Alt-Ergo" name="Alt-Ergo"
...@@ -12,64 +12,86 @@ ...@@ -12,64 +12,86 @@
version="2.2"/> version="2.2"/>
<prover <prover
id="2" id="2"
name="Spass" name="CVC3"
version="3.7"/> version="2.4.1"/>
<prover <prover
id="3" id="3"
name="Gappa"
version="0.16.0"/>
<prover
id="4"
name="Yices" name="Yices"
version="1.0.25"/> version="1.0.25"/>
<prover <prover
id="4" id="5"
name="Z3" name="Z3"
version="2.19"/> version="2.19"/>
<prover
id="6"
name="Z3"
version="3.2"/>
<file <file
name="../real.why" name="../real.why"
verified="true" verified="true"
expanded="false"> expanded="true">
<theory <theory
name="Test" name="Test"
locfile="check-builtin/real/../real.why" locfile="real/../real.why"
loclnum="1" loccnumb="7" loccnume="11" loclnum="1" loccnumb="7" loccnume="11"
verified="true" verified="true"
expanded="true"> expanded="true">
<goal <goal
name="G1" name="G1"
locfile="check-builtin/real/../real.why" locfile="real/../real.why"
loclnum="3" loccnumb="7" loccnume="9" loclnum="3" loccnumb="7" loccnume="9"
sum="7961c96b42f34e5cb3280ce85643dffb" sum="7961c96b42f34e5cb3280ce85643dffb"
proved="true" proved="true"
expanded="true" expanded="true"
shape="ainfix =ainfix *c5.5c10.c55."> shape="ainfix =ainfix *c5.5c10.c55.">
<proof <proof
prover="4" prover="5"
timelimit="10" timelimit="3"
obsolete="false" obsolete="false"
archived="false"> archived="false">
<result status="valid" time="0.00"/> <result status="valid" time="0.00"/>
</proof> </proof>
<proof <proof
prover="2" prover="1"
timelimit="10" timelimit="3"
obsolete="false" obsolete="false"
archived="false"> archived="false">
<result status="timeout" time="10.20"/> <result status="valid" time="0.00"/>
</proof> </proof>
<proof <proof
prover="1" prover="0"
timelimit="10" timelimit="3"
obsolete="false" obsolete="false"
archived="false"> archived="false">
<result status="valid" time="0.00"/> <result status="valid" time="0.00"/>
</proof> </proof>
<proof <proof
prover="0" prover="2"
timelimit="10" timelimit="3"
obsolete="false" obsolete="false"
archived="false"> archived="false">
<result status="valid" time="0.00"/> <result status="valid" time="0.00"/>
</proof> </proof>
<proof <proof
prover="3" prover="3"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
timelimit="10" timelimit="10"
obsolete="false" obsolete="false"
archived="false"> archived="false">
...@@ -78,36 +100,50 @@ ...@@ -78,36 +100,50 @@
</goal> </goal>
<goal <goal
name="G2" name="G2"
locfile="check-builtin/real/../real.why" locfile="real/../real.why"
loclnum="4" loccnumb="7" loccnume="9" loclnum="4" loccnumb="7" loccnume="9"
sum="b18a4b0fb8e663468863ba1c86a7cc64" sum="b18a4b0fb8e663468863ba1c86a7cc64"
proved="true" proved="true"
expanded="true" expanded="true"
shape="ainfix =ainfix /c9.c3.c3."> shape="ainfix =ainfix /c9.c3.c3.">
<proof <proof
prover="4" prover="5"
timelimit="10" timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="1"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="0"
timelimit="3"
obsolete="false" obsolete="false"
archived="false"> archived="false">
<result status="valid" time="0.00"/> <result status="valid" time="0.00"/>
</proof> </proof>
<proof <proof
prover="2" prover="2"
timelimit="10" timelimit="3"
obsolete="false" obsolete="false"
archived="false"> archived="false">
<result status="timeout" time="10.47"/> <result status="valid" time="0.00"/>
</proof> </proof>
<proof <proof
prover="1" prover="3"
timelimit="10" timelimit="3"
obsolete="false" obsolete="false"
archived="false"> archived="false">
<result status="valid" time="0.00"/> <result status="valid" time="0.00"/>
</proof> </proof>
<proof <proof
prover="0" prover="6"
timelimit="10" timelimit="3"
obsolete="false" obsolete="false"
archived="false"> archived="false">
<result status="valid" time="0.00"/> <result status="valid" time="0.00"/>
...@@ -115,36 +151,363 @@ ...@@ -115,36 +151,363 @@
</goal> </goal>
<goal <goal
name="G3" name="G3"
locfile="check-builtin/real/../real.why" locfile="real/../real.why"
loclnum="5" loccnumb="7" loccnume="9" loclnum="5" loccnumb="7" loccnume="9"
sum="297dff92907d47bda80a8ffe2d186396" sum="297dff92907d47bda80a8ffe2d186396"
proved="true" proved="true"
expanded="true" expanded="true"
shape="ainfix =ainvc5.c0.2"> shape="ainfix =ainvc5.c0.2">
<proof <proof
prover="4" prover="5"
timelimit="10" timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="1"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="0"
timelimit="3"
obsolete="false" obsolete="false"
archived="false"> archived="false">
<result status="valid" time="0.00"/> <result status="valid" time="0.00"/>
</proof> </proof>
<proof <proof
prover="2" prover="2"
timelimit="10" timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="3"
timelimit="3"
obsolete="false" obsolete="false"
archived="false"> archived="false">
<result status="timeout" time="10.08"/> <result status="failure" time="0.00"/>
</proof>
<proof
prover="6"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
</theory>
<theory
name="TestInfix"
locfile="real/../real.why"
loclnum="8" loccnumb="7" loccnume="16"
verified="true"
expanded="true">
<goal
name="Add"
locfile="real/../real.why"
loclnum="10" loccnumb="7" loccnume="10"
sum="43afbf3638f15444ec33376879694c6b"
proved="true"
expanded="true"
shape="ainfix =ainfix +.c5.5c10.c15.5">
<proof
prover="5"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof> </proof>
<proof <proof
prover="1" prover="1"
timelimit="10" timelimit="3"
obsolete="false" obsolete="false"
archived="false"> archived="false">
<result status="valid" time="0.00"/> <result status="valid" time="0.00"/>
</proof> </proof>
<proof <proof
prover="0" prover="0"
timelimit="10" timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="3"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Sub"
locfile="real/../real.why"
loclnum="11" loccnumb="7" loccnume="10"
sum="9e26dca43231665f3c20276262e0e4ef"
proved="true"
expanded="true"
shape="ainfix =ainfix -.c9.c3.c6.">
<proof
prover="5"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="1"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="0"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="3"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Neg"
locfile="real/../real.why"
loclnum="12" loccnumb="7" loccnume="10"
sum="4f3a94d0b96c33ec0276c6802921cd6a"
proved="true"
expanded="true"
shape="ainfix =ainfix +.aprefix -.c5.c3.5aprefix -.c1.5">
<proof
prover="5"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="1"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="0"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="3"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Mul"
locfile="real/../real.why"
loclnum="13" loccnumb="7" loccnume="10"
sum="547a086bd1da4bd6a329f80d539f9e4f"
proved="true"
expanded="true"
shape="ainfix =ainfix *.c5.5c10.c55.">
<proof
prover="5"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="1"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="0"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="3"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Div"
locfile="real/../real.why"
loclnum="14" loccnumb="7" loccnume="10"
sum="11f3cf0fd8346c98624030a58cf9940a"
proved="true"