Commit b62e0ffd authored by MARCHE Claude's avatar MARCHE Claude

Merge branch 'master' into claude

parents e1b4522b 48c6b603
......@@ -137,8 +137,7 @@ why3.conf
/src/config.sh
# Coq tactic
/src/coq-tactic/coqCompat.ml
/src/coq-tactic/g_why3tac.ml
/src/coq-tactic/why3tac.ml
/src/coq-tactic/.why3-vo-*
# PVS
......
......@@ -753,9 +753,9 @@ install_local:: bin/why3session
ifeq (@enable_coq_tactic@,yes)
COQPGENERATED = src/coq-tactic/coqCompat.ml src/coq-tactic/g_why3tac.ml
COQPGENERATED = src/coq-tactic/why3tac.ml
COQP_FILES = coqCompat why3tac g_why3tac
COQP_FILES = why3tac
COQPMODULES = $(addprefix src/coq-tactic/, $(COQP_FILES))
......@@ -763,7 +763,7 @@ COQPDEP = $(addsuffix .dep, $(COQPMODULES))
COQPCMO = $(addsuffix .cmo, $(COQPMODULES))
COQPCMX = $(addsuffix .cmx, $(COQPMODULES))
COQPTREES = kernel lib interp parsing proofs pretyping tactics library toplevel
COQPTREES = kernel interp intf lib library parsing pretyping proofs printing tactics toplevel
COQPINCLUDES = -I src/coq-tactic -I +camlp5 $(addprefix -I @COQLIB@/, $(COQPTREES)) @ZIPINCLUDE@
$(COQPDEP): DEPFLAGS += -I src/coq-tactic
......@@ -776,9 +776,6 @@ $(COQPDEP): $(COQPGENERATED)
byte: src/coq-tactic/.why3-vo-byte
opt: src/coq-tactic/.why3-vo-opt
src/coq-tactic/coqCompat.ml: src/coq-tactic/coqCompat@coq_compat_version@.ml
cp -f $< $@
lib/coq-tactic/why3tac.cmxs: OFLAGS += $(addsuffix .cmxa, @ZIPLIB@)
lib/coq-tactic/why3tac.cmxs: OFLAGS += $(addsuffix .cmx, @MENHIRLIB@)
......@@ -793,18 +790,18 @@ lib/coq-tactic/why3tac.cma: lib/why3/why3.cma $(COQPCMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) -a $(BFLAGS) -o $@ $^
src/coq-tactic/g_why3tac.ml: src/coq-tactic/g_why3tac.ml4
src/coq-tactic/why3tac.ml: src/coq-tactic/why3tac.ml4
$(if $(QUIET),@echo 'Camlp5 $<' &&) \
$(CAMLP5O) pr_o.cmo @COQLIB@/parsing/grammar.cma -impl $^ -o $@
$(CAMLP5O) pr_dump.cmo @COQPPLIBS@ pa_macro.cmo -D@coq_compat_version@ -impl $^ -o $@
src/coq-tactic/.why3-vo-byte: lib/coq-tactic/Why3.v lib/coq-tactic/why3tac.cma
$(if $(QUIET),@echo 'Coqc $<' &&) \
WHY3CONFIG="" $(COQC) -byte -I lib/coq-tactic/ $< && \
WHY3CONFIG="" $(COQC) -byte -R lib/coq-tactic Why3 -R lib/coq Why3 $< && \
touch src/coq-tactic/.why3-vo-byte
src/coq-tactic/.why3-vo-opt: lib/coq-tactic/Why3.v lib/coq-tactic/why3tac.cmxs
$(if $(QUIET),@echo 'Coqc $<' &&) \
WHY3CONFIG="" $(COQC) -opt -I lib/coq-tactic/ $< && \
WHY3CONFIG="" $(COQC) -opt -R lib/coq-tactic Why3 -R lib/coq Why3 $< && \
touch src/coq-tactic/.why3-vo-opt
# depend and clean targets
......@@ -878,7 +875,7 @@ COQVD = $(addsuffix .vd, $(COQLIBS_FILES))
%.vd: %.v
$(if $(QUIET),@echo 'Coqdep $<' &&) \
$(COQDEP) -slash -R lib/coq Why3 $< > $@
$(COQDEP) -R lib/coq Why3 $< > $@
drivers/coq-realizations.aux: Makefile
$(if $(QUIET),@echo 'Generate $@' &&) \
......@@ -1436,10 +1433,10 @@ test-session.opt: examples/use_api/create_session.ml lib/why3/why3.cmxa
@rm -f test-session.opt why3session.xml why3shapes why3shapes.gz
test-coq-tactic.byte: src/coq-tactic/.why3-vo-byte
$(COQC) -byte -I lib/coq-tactic/ bench/coq-tactic/test.v
$(COQC) -byte -R lib/coq-tactic Why3 -R lib/coq Why3 bench/coq-tactic/test.v
test-coq-tactic.opt: src/coq-tactic/.why3-vo-opt
$(COQC) -opt -I lib/coq-tactic/ bench/coq-tactic/test.v
$(COQC) -opt -R lib/coq-tactic Why3 -R lib/coq Why3 bench/coq-tactic/test.v
#only test the compilation of runstrat
test-runstrat.byte: lib/why3/why3.cma lib/why3/META
......
......@@ -254,15 +254,15 @@ Qed.
(* Polymorphic, Mutually inductive types *)
Inductive ptree (a:Set) : Set :=
| PLeaf : ptree a
| PNode : a -> pforest a -> ptree a
Inductive ptree {a:Set} : Set :=
| PLeaf : ptree
| PNode : a -> pforest -> ptree
with pforest (a:Set) : Set :=
| PNil : pforest a
| PCons : ptree a -> pforest a -> pforest a.
with pforest {a:Set} : Set :=
| PNil : pforest
| PCons : ptree -> pforest -> pforest.
Goal forall x : ptree Z, x=x.
Goal forall x : @ptree Z, x=x.
ae.
Qed.
......@@ -277,18 +277,18 @@ Goal bb=0.
ae.
Qed.
Fixpoint ptree_size (a:Set) (t:ptree a) : Z := match t with
Fixpoint ptree_size {a:Set} (t:@ptree a) : Z := match t with
| PLeaf => 0
| PNode _ f => 1 + pforest_size _ f end
with pforest_size (a:Set) (f:pforest a) : Z := match f with
| PNode _ f => 1 + pforest_size f end
with pforest_size {a:Set} (f:@pforest a) : Z := match f with
| PNil => 0
| PCons t f => ptree_size _ t + pforest_size _ f end.
| PCons t f => ptree_size t + pforest_size f end.
Goal ptree_size _ (@PLeaf Z) = 0.
Goal ptree_size (@PLeaf Z) = 0.
ae.
Qed.
Goal forall (a:Set), ptree_size a (PLeaf a) = 0.
Goal forall (a:Set), ptree_size (@PLeaf a) = 0.
intros.
ae.
Qed.
......
......@@ -497,9 +497,16 @@ else
COQVERSION=`$COQC -v | sed -n -e 's|.*version* *\([[^ ]]*\) .*$|\1|p' `
case $COQVERSION in
8.4*|trunk)
8.4*)
enable_coq_support=yes
coq_compat_version=".8.4"
coq_compat_version="COQ84"
COQPPLIBS="$COQLIB/parsing/grammar.cma"
AC_MSG_RESULT($COQVERSION)
;;
8.5*|trunk)
enable_coq_support=yes
coq_compat_version="COQ85"
COQPPLIBS="$OCAMLLIB/unix.cma $OCAMLLIB/threads/threads.cma $COQLIB/grammar/grammar.cma"
AC_MSG_RESULT($COQVERSION)
;;
*)
......@@ -543,7 +550,7 @@ fi
if test "$enable_coq_libs" = yes; then
AC_MSG_CHECKING([for Flocq])
AS_IF(
[ echo "Require Import Flocq_version BinNat." \
[ echo "Require Import Flocq.Flocq_version BinNat." \
"Goal (20200 <= Flocq_version)%N. easy. Qed." > conftest.v
"$COQC" conftest.v > conftest.err ],
[ AC_MSG_RESULT(yes) ],
......@@ -755,7 +762,7 @@ AC_SUBST(coq_compat_version)
AC_SUBST(COQC)
AC_SUBST(COQDEP)
AC_SUBST(COQLIB)
AC_SUBST(COQVERSION)
AC_SUBST(COQPPLIBS)
AC_SUBST(COMPILETIMECOQ)
AC_SUBST(enable_pvs_libs)
......
Require Import ZArith Reals Why3.BuiltIn.
Declare ML Module "why3tac".
......@@ -10,8 +10,8 @@ Require real.Abs.
Require real.FromInt.
Require floating_point.Rounding.
Require Import Fcore.
Require Import Fappli_IEEE.
Require Import Flocq.Core.Fcore.
Require Import Flocq.Appli.Fappli_IEEE.
Require Import int.Abs.
Section GenFloat.
......@@ -82,7 +82,7 @@ intros H _ _.
now injection H.
clear.
destruct (Bool.bool_dec xs ys) as [->|Hs].
destruct (Z_eq_dec (Zpos (projT1 xm')) (Zpos (projT1 ym'))) as [Hm'|Hm'].
destruct (Z_eq_dec (Zpos (proj1_sig xm')) (Zpos (proj1_sig ym'))) as [Hm'|Hm'].
left.
apply f_equal3 ; try easy.
apply f_equal2 ; try easy.
......@@ -293,7 +293,7 @@ apply generic_format_abs.
apply generic_format_B2R.
apply generic_format_bpow.
unfold FLT_exp, emin.
clear ; zify ; generalize Hprec' Hemax' ; omega.
zify ; generalize Hprec' Hemax' ; omega.
apply bpow_gt_0.
apply abs_B2R_lt_emax.
unfold pred.
......@@ -310,7 +310,7 @@ rewrite Z2R_minus, Z2R_Zpower.
simpl; ring.
apply Zlt_le_weak.
exact Hprec'.
clear; generalize Hprec' Hemax' ; omega.
generalize Hprec' Hemax' ; omega.
Qed.
(* Why3 goal *)
......@@ -335,14 +335,14 @@ split.
rewrite Z2R_IZR.
now rewrite Rmult_1_r.
split. easy.
clear;unfold emin; generalize Hprec' Hemax'; omega.
unfold emin; generalize Hprec' Hemax'; omega.
unfold max_representable_integer in Bz.
change 2%Z with (radix_val radix2) in Bz.
apply generic_format_abs_inv.
rewrite <- Z2R_IZR, <- Z2R_abs, Bz, Z2R_Zpower.
apply generic_format_bpow.
unfold FLT_exp, emin.
clear; generalize Hprec' Hemax'; zify.
clear Bz; generalize Hprec' Hemax'; zify.
omega.
apply Zlt_le_weak.
apply Hprec'.
......
......@@ -462,7 +462,7 @@ version_ok = "8.4pl3"
version_ok = "8.4pl2"
version_ok = "8.4pl1"
version_ok = "8.4"
command = "%l/why3-cpulimit 0 %m -s %e -I %l/coq-tactic -R %l/coq Why3 -l %f"
command = "%l/why3-cpulimit 0 %m -s %e -R %l/coq-tactic Why3 -R %l/coq Why3 -l %f"
driver = "drivers/coq.drv"
editor = "coqide"
......@@ -503,7 +503,7 @@ command = "coqide -I %l/coq-tactic -R %l/coq Why3 %f"
[editor proofgeneral-coq]
name = "Emacs/ProofGeneral/Coq"
command = "emacs --eval \"(setq coq-load-path '(\\\"%l/coq-tactic\\\" \
command = "emacs --eval \"(setq coq-load-path '((\\\"%l/coq-tactic\\\" \\\"Why3\\\") \
(\\\"%l/coq\\\" \\\"Why3\\\")))\" %f"
[editor isabelle-jedit]
......
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2014 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
let body_of_constant c = c.Declarations.const_body
let on_leaf_node node f =
match node with
| Lib.Leaf lobj -> f lobj
| Lib.CompilingLibrary _
| Lib.OpenedModule _
| Lib.ClosedModule _
| Lib.OpenedModtype _
| Lib.ClosedModtype _
| Lib.OpenedSection _
| Lib.ClosedSection _
| Lib.FrozenState _ -> ()
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2014 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
let body_of_constant = Declarations.body_of_constant
let on_leaf_node node f =
match node with
| Lib.Leaf lobj -> f lobj
| Lib.CompilingLibrary _
| Lib.OpenedModule _
| Lib.ClosedModule _
| Lib.OpenedSection _
| Lib.ClosedSection _
| Lib.FrozenState _ -> ()
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2014 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
val body_of_constant :
Declarations.constant_body -> Declarations.constr_substituted option
val on_leaf_node : Lib.node -> (Libobject.obj -> unit) -> unit
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
(*i camlp4deps: "parsing/grammar.cma" i*)
open Why3tac
TACTIC EXTEND Why3
[ "why3" string(s) ] -> [ why3tac s ]
| [ "why3" string(s) "timelimit" integer(n) ] -> [ why3tac ~timelimit:n s ]
END
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