Commit 99349928 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

Coq plug-in in lib/coq-plugin/, and added to Coq load path

parent 4b235d82
...@@ -127,8 +127,8 @@ why3.conf ...@@ -127,8 +127,8 @@ why3.conf
/src/*.a /src/*.a
# /src/coq-plugin/ # /src/coq-plugin/
/src/coq-plugin/g_whytac.ml /src/coq-plugin/g_why3tac.ml
/src/coq-plugin/whytac.cma /src/coq-plugin/why3tac.cma
# /src/driver/ # /src/driver/
/src/driver/driver_lexer.ml /src/driver/driver_lexer.ml
......
...@@ -797,9 +797,9 @@ endif ...@@ -797,9 +797,9 @@ endif
ifeq (@enable_coq_plugin@,yes) ifeq (@enable_coq_plugin@,yes)
COQPGENERATED = src/coq-plugin/g_whytac.ml COQPGENERATED = src/coq-plugin/g_why3tac.ml
COQP_FILES = whytac g_whytac COQP_FILES = why3tac g_why3tac
COQPMODULES = $(addprefix src/coq-plugin/, $(COQP_FILES)) COQPMODULES = $(addprefix src/coq-plugin/, $(COQP_FILES))
...@@ -815,21 +815,30 @@ $(COQPCMO) $(COQPCMX): INCLUDES += $(COQPINCLUDES) ...@@ -815,21 +815,30 @@ $(COQPCMO) $(COQPCMX): INCLUDES += $(COQPINCLUDES)
$(COQPDEP): $(COQPGENERATED) $(COQPDEP): $(COQPGENERATED)
byte: src/coq-plugin/whytac.cma byte: lib/coq-plugin/why3tac.cma lib/coq-plugin/Why3.vo
opt: src/coq-plugin/whytac.cmxs opt: lib/coq-plugin/why3tac.cmxs lib/coq-plugin/Why3.vo
src/coq-plugin/whytac.cma: BFLAGS+=-rectypes -I +camlp5 byte: WHY3TAC = lib/coq-plugin/why3tac.cma
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes -I +camlp5 opt: WHY3TAC = lib/coq-plugin/why3tac.cmxs
src/coq-plugin/whytac.cmxs: src/why3.cmxa $(COQPCMX) byte: WHY3COQ = $(COQC) -byte
opt: WHY3COQ = $(COQC) -opt
lib/coq-plugin/why3tac.cma: BFLAGS+=-rectypes -I +camlp5
lib/coq-plugin/why3tac.cmxs: OFLAGS+=-rectypes -I +camlp5
lib/coq-plugin/why3tac.cmxs: src/why3.cmxa $(COQPCMX)
$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^ $(OCAMLOPT) $(OFLAGS) -o $@ -shared $^
src/coq-plugin/whytac.cma: src/why3.cma $(COQPCMO) lib/coq-plugin/why3tac.cma: src/why3.cma $(COQPCMO)
$(OCAMLC) -a $(BFLAGS) -o $@ $^ $(OCAMLC) -a $(BFLAGS) -o $@ $^
src/coq-plugin/g_whytac.ml: src/coq-plugin/g_whytac.ml4 src/coq-plugin/g_why3tac.ml: src/coq-plugin/g_why3tac.ml4
$(CAMLP5O) pr_o.cmo @COQLIB@/parsing/grammar.cma -impl $^ -o $@ $(CAMLP5O) pr_o.cmo @COQLIB@/parsing/grammar.cma -impl $^ -o $@
lib/coq-plugin/Why3.vo: lib/coq-plugin/Why3.v $(WHY3TAC)
$(WHY3COQ) -I lib/coq-plugin/ $<
# depend and clean targets # depend and clean targets
ifneq "$(MAKECMDGOALS)" "clean" ifneq "$(MAKECMDGOALS)" "clean"
...@@ -840,10 +849,14 @@ depend: $(COQPDEP) ...@@ -840,10 +849,14 @@ depend: $(COQPDEP)
clean:: clean::
rm -f src/coq-plugin/*.cm[iox] src/coq-plugin/*.o rm -f src/coq-plugin/*.cm[iox] src/coq-plugin/*.o
rm -f src/coq-plugin/*.cma src/coq-plugin/*.cmxs rm -f lib/coq-plugin/*.cma lib/coq-plugin/*.cmxs
rm -f src/coq-plugin/*.annot src/coq-plugin/*.dep src/coq-plugin/*~ rm -f src/coq-plugin/*.annot src/coq-plugin/*.dep src/coq-plugin/*~
rm -f $(COQPGENERATED) rm -f $(COQPGENERATED)
install_no_local::
mkdir -p $(LIBDIR)/why3/coq-plugin
cp -f lib/coq-plugin/* $(LIBDIR)/why3/coq-plugin
endif endif
#################### ####################
...@@ -1226,7 +1239,7 @@ DISTRIB_FILES = Version Makefile.in configure.in META.in configure \ ...@@ -1226,7 +1239,7 @@ DISTRIB_FILES = Version Makefile.in configure.in META.in configure \
examples/use_api.ml \ examples/use_api.ml \
theories/*.why \ theories/*.why \
modules/*.mlw \ modules/*.mlw \
lib/coq/*/*.v \ lib/coq/*/*.v lib/coq-plugin/*.v \
share/provers-detection-data.conf.in \ share/provers-detection-data.conf.in \
share/emacs/why.el share/images/*.png share/lang/*.lang \ share/emacs/why.el share/images/*.png share/lang/*.lang \
share/bash/why3 share/zsh/_why3 share/vim/why3.vim share/bash/why3 share/zsh/_why3 share/vim/why3.vim
...@@ -1253,6 +1266,7 @@ $(DISTRIB_TAR): doc/manual.pdf ...@@ -1253,6 +1266,7 @@ $(DISTRIB_TAR): doc/manual.pdf
mkdir -p $(DISTRIB_DIR)/lib mkdir -p $(DISTRIB_DIR)/lib
mkdir -p $(DISTRIB_DIR)/lib/plugins mkdir -p $(DISTRIB_DIR)/lib/plugins
mkdir -p $(DISTRIB_DIR)/lib/coq mkdir -p $(DISTRIB_DIR)/lib/coq
mkdir -p $(DISTRIB_DIR)/lib/coq-plugin
ln -s ../drivers $(DISTRIB_DIR)/share/drivers ln -s ../drivers $(DISTRIB_DIR)/share/drivers
ln -s ../modules $(DISTRIB_DIR)/share/modules ln -s ../modules $(DISTRIB_DIR)/share/modules
ln -s ../theories $(DISTRIB_DIR)/share/theories ln -s ../theories $(DISTRIB_DIR)/share/theories
......
...@@ -166,6 +166,8 @@ Declare ML Module "whytac". ...@@ -166,6 +166,8 @@ Declare ML Module "whytac".
Ltac ae := why3 "alt-ergo". Ltac ae := why3 "alt-ergo".
*) *)
Require Import Why3.
(* Why3 goal *) (* Why3 goal *)
Theorem permutation : forall (a:Type), forall (a1:(sparse_array a)), Theorem permutation : forall (a:Type), forall (a1:(sparse_array a)),
(sa_inv a1) -> (((card a1) = (length1 a1)) -> forall (i:Z), (sa_inv a1) -> (((card a1) = (length1 a1)) -> forall (i:Z),
...@@ -177,35 +179,11 @@ intro H; decompose [and] H; clear H. ...@@ -177,35 +179,11 @@ intro H; decompose [and] H; clear H.
clear a_values a_def H0 H3 H4. clear a_values a_def H0 H3 H4.
subst n1 n2. subst n1 n2.
intros. subst a_card. intros. subst a_card.
assert (inj: injective a_back n0) (* by ae *). assert (inj: injective a_back n0) by ae.
assert (rng: range a_back n0) by ae.
red; intros.
red; intro.
generalize (H5 i0 H).
generalize (H5 j H1).
intuition.
apply H2.
rewrite <- H11.
rewrite <- H12.
apply f_equal; assumption.
assert (rng: range a_back n0) (* by ae *).
red; intros.
generalize (H5 i0); intuition.
generalize (injective_surjective a_back n0 inj rng); intro surj. generalize (injective_surjective a_back n0 inj rng); intro surj.
destruct (surj i H0) as (j, (hj1, hj2)). destruct (surj i H0) as (j, (hj1, hj2)).
(* ae. *) ae.
generalize (H5 j hj1); intros (hi1, hi2).
split.
rewrite <- hj2.
rewrite hi2; auto.
rewrite <- hj2.
generalize (H5 j hj1); intuition.
rewrite H8; auto.
Qed. Qed.
Declare ML Module "why3tac".
Ltac ae := why3 "alt-ergo".
Ltac Z3 := why3 "z3-2".
Ltac spass := why3 "spass".
...@@ -268,9 +268,9 @@ version_old = "8.2pl1" ...@@ -268,9 +268,9 @@ version_old = "8.2pl1"
version_old = "8.2" version_old = "8.2"
version_old = "8.1" version_old = "8.1"
version_old = "8.0" version_old = "8.0"
command = "@LOCALBIN@why3-cpulimit 0 %m -s %e -R %l/coq Why3 -l %f" command = "@LOCALBIN@why3-cpulimit 0 %m -s %e -I %l/coq-plugin -R %l/coq Why3 -l %f"
driver = "drivers/coq.drv" driver = "drivers/coq.drv"
editor = "coqide -R %l/coq Why3 %f" editor = "coqide -I %l/coq-plugin -R %l/coq Why3 %f"
[ITP pvs] [ITP pvs]
name = "PVS" name = "PVS"
......
...@@ -19,8 +19,8 @@ ...@@ -19,8 +19,8 @@
(*i camlp4deps: "parsing/grammar.cma" i*) (*i camlp4deps: "parsing/grammar.cma" i*)
open Whytac open Why3tac
TACTIC EXTEND Why3 TACTIC EXTEND Why3
[ "why3" string(s) ] -> [ whytac s ] [ "why3" string(s) ] -> [ why3tac s ]
END END
Declare ML Module "whytac". Require Import Why3.
Require Export ZArith. Require Export ZArith.
Open Scope Z_scope. Open Scope Z_scope.
Require Export List. Require Export List.
Ltac ae := why3 "alt-ergo".
Ltac Z3 := why3 "z3-2".
Ltac spass := why3 "spass".
Section S0. Section S0.
Variable a:Set->Set. Variable a:Set->Set.
......
...@@ -1084,7 +1084,7 @@ let tr_top_decl = function ...@@ -1084,7 +1084,7 @@ let tr_top_decl = function
| _, Lib.ClosedSection _ | _, Lib.ClosedSection _
| _, Lib.FrozenState _ -> () | _, Lib.FrozenState _ -> ()
let whytac s gl = let why3tac s gl =
(* print_dep Format.err_formatter; *) (* print_dep Format.err_formatter; *)
let concl_type = pf_type_of gl (pf_concl gl) in let concl_type = pf_type_of gl (pf_concl gl) in
if not (is_Prop concl_type) then error "Conclusion is not a Prop"; if not (is_Prop concl_type) then error "Conclusion is not a Prop";
...@@ -1117,10 +1117,8 @@ let whytac s gl = ...@@ -1117,10 +1117,8 @@ let whytac s gl =
Format.eprintf "@[exception: %a@]@." Exn_printer.exn_printer e; Format.eprintf "@[exception: %a@]@." Exn_printer.exn_printer e;
raise e raise e
(* (*
Local Variables: Local Variables:
compile-command: "unset LANG; make -C ../.. src/coq-plugin/whytac.cmxs" compile-command: "unset LANG; make -C ../.. src/coq-plugin/why3tac.cmxs"
End: 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