coq-plugin: configuration and compilation

Makefile.in

@@ -52,10 +52,10 @@ OCAMLYACC = @OCAMLYACC@
 OCAMLDOC  = @OCAMLDOC@
 OCAMLLIB  = @OCAMLLIB@
 OCAMLBEST = @OCAMLBEST@
-#CAMLP4   = @CAMLP4O@
-
 OCAMLVERSION = @OCAMLVERSION@
 
+CAMLP5O   = @CAMLP5O@
+
 #PSVIEWER  = @PSVIEWER@
 #PDFVIEWER = @PDFVIEWER@
 
@@ -338,25 +338,54 @@ clean::
 # Coq plugin
 ##############
 
+COQGENERATED = src/coq-plugin/g_whytac.ml
+
+COQ_FILES = whytac g_whytac
+
+COQMODULES = $(addprefix src/coq-plugin/, $(COQ_FILES))
+
+COQML  = $(addsuffix .ml,  $(COQMODULES))
+COQCMO = $(addsuffix .cmo, $(COQMODULES))
+COQCMX = $(addsuffix .cmx, $(COQMODULES))
+
+COQTREES = kernel lib interp parsing proofs pretyping tactics library toplevel
+COQINCLUDES = -I src/coq-plugin $(addprefix -I @COQLIB@/, $(COQTREES))
+
+$(COQCMO) $(COQCMX): INCLUDES = $(COQINCLUDES)
+
 ifeq (@enable_coq_support@,yes)
 byte: src/coq-plugin/whytac.cma
 opt:  src/coq-plugin/whytac.cmxs
 endif
 
-COQTREES = kernel lib interp parsing proofs pretyping tactics library toplevel
-
-src/coq-plugin/whytac.cma:  INCLUDES = $(addprefix -I @COQLIB@/, $(COQTREES))
-src/coq-plugin/whytac.cmxs: INCLUDES = $(addprefix -I @COQLIB@/, $(COQTREES))
-
 src/coq-plugin/whytac.cma:  BFLAGS+=-rectypes -I +camlp5
 src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes -I +camlp5
 
-src/coq-plugin/whytac.cmxs: src/why.cmxa src/coq-plugin/whytac.ml
+src/coq-plugin/whytac.cmxs: src/why.cmxa $(COQCMX)
 	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^
 
-src/coq-plugin/whytac.cma: src/why.cma src/coq-plugin/whytac.ml
+src/coq-plugin/whytac.cma: src/why.cma $(COQCMO)
 	$(OCAMLC) -a $(BFLAGS) -o $@ $^
 
+src/coq-plugin/g_whytac.ml: src/coq-plugin/g_whytac.ml4
+	$(CAMLP5O) pr_o.cmo @COQLIB@/parsing/grammar.cma -impl $^ -o $@
+
+# depend and clean targets
+
+include .depend.coq
+
+.depend.coq: $(COQGENERATED)
+	$(OCAMLDEP) -slash -I src -I src/coq-plugin $(COQML) > $@
+
+depend: .depend.coq
+
+clean::
+	rm -f src/coq-plugin/*.cm[iox] src/coq-plugin/*.o
+	rm -f src/coq-plugin/*.cma src/coq-plugin/*.cmxs
+	rm -f src/coq-plugin/*.annot src/coq-plugin/*~
+	rm -f $(COQGENERATED)
+	rm -f .depend.coq
+
 #######
 # tools
 #######

configure.in

@@ -211,6 +211,8 @@ else
     fi
 fi
 
+AC_CHECK_PROG(CAMLP5O,camlp5o,camlp5o,no)
+
 # checking for sqlite3
 if test "$enable_proof_manager" = yes ; then
 AC_CHECK_FILE($OCAMLLIB/sqlite3/sqlite3.cma,,enable_proof_manager=no)
@@ -253,8 +255,8 @@ fi
 if test "$enable_coq_support" = yes; then
    AC_CHECK_FILE($COQLIB/kernel/term.cmi,,enable_coq_support=no)
 fi
-if test "$enable_coq_support" = yes; then
-   AC_CHECK_FILE($OCAMLLIB/camlp5/gramext.cmi,,enable_coq_support=no)
+if test "$CAMLP5O" = no; then
+   enable_coq_support=no
 fi
 
 #Viewer for ps and pdf
@@ -289,6 +291,8 @@ dnl AC_SUBST(FORPACK)
 dnl AC_SUBST(OCAMLGRAPHLIB)
 dnl AC_SUBST(OCAMLWEB)
 
+AC_SUBST(CAMLP5O)
+
 AC_SUBST(enable_ide)
 AC_SUBST(enable_plugins)
 AC_SUBST(DYNLINK)

src/coq-plugin/g_whytac.ml4

+
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+open Whytac
+
+TACTIC EXTEND Why
+  [ "why" string(s) ] -> [ whytac s ]
+END

src/coq-plugin/test.v

@@ -4,6 +4,8 @@ Open Scope Z_scope.
 Require Export List.
 
 Ltac ae := why "alt-ergo".
+Ltac z3 := why "z3".
+Ltac spass := why "spass".
 
 (* type definitions *)
 
@@ -22,7 +24,7 @@ Qed.
 Definition p (x:nat) := x=O.
 
 Goal p O.
-ae.
+spass.
 Qed.
 
 Definition eq (A:Set) (x y : A) := x=y.
@@ -53,7 +55,7 @@ Qed.
 Definition id A (x:A) := x.
 
 Goal id nat O = O.
-ae.
+spass.
 Qed.
 
 (* inductive types *)
@@ -63,7 +65,7 @@ Parameter P : (nat -> nat) -> Prop.
 Goal forall (a:Set), forall x:nat, x=S O -> P S -> 
   let y := (S (S O)) in S x=y.
 intros.
-ae.
+spass.
 Qed.
 
 Goal  forall (a:Set), forall x:Z, x=1 -> P S -> let y := 2 in x+1=y.
@@ -73,7 +75,7 @@ Qed.
 
 Goal  forall x: list nat, x=x.
 intros.
-ae.
+spass.
 Qed.
 
 (* Mutually inductive types *)
@@ -87,7 +89,7 @@ with forest : Set :=
   | Cons : tree -> forest -> forest.
 
 Goal forall x : tree, x=x.
-ae.
+spass.
 Qed.
 
 (* Polymorphic, Mutually inductive types *)
@@ -101,7 +103,7 @@ with pforest (a:Set) : Set :=
   | PCons : ptree a -> pforest a -> pforest a.
 
 Goal forall x : ptree Z, x=x.
-ae.
+spass.
 Qed.
 
 (* the same, without parameters *)
@@ -115,6 +117,6 @@ with pforest' : Type -> Type :=
   | PCons' : forall (a:Type), ptree' a -> pforest' a -> pforest' a.
 
 Goal forall x : ptree' Z, x=x.
-ae.
+spass.
 Qed.