coq-plugin: requires camlp5 (detected at configuration time

Makefile.in

@@ -343,13 +343,13 @@ byte: src/coq-plugin/whytac.cma
 opt:  src/coq-plugin/whytac.cmxs
 endif
 
-COQTREES = kernel lib interp parsing proofs pretyping tactics library
+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
-src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes
+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
 	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^

configure.in

@@ -253,6 +253,9 @@ 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)
+fi
 
 #Viewer for ps and pdf
 dnl AC_CHECK_PROGS(PSVIEWER,gv evince)

src/coq-plugin/test.v

@@ -3,6 +3,8 @@ Require Export ZArith.
 Open Scope Z_scope.
 Require Export List.
 
+Ltac ae := why "alt-ergo".
+
 (* type definitions *)
 
 Definition t := list.
@@ -10,28 +12,27 @@ Definition t := list.
 Inductive foo : Set :=
   C : t nat -> foo.
 
-(*
 Goal forall x:foo, x=x.
 intros.
-why.
+ae.
 Qed.
-*)
 
 (* predicate definition *)
 
 Definition p (x:nat) := x=O.
 
-(*
 Goal p O.
-why.
+ae.
 Qed.
-*)
 
 Definition eq (A:Set) (x y : A) := x=y.
 
 Goal eq nat O O.
-why. (* BUG transformations ? *)
+(*
+why "z3".  (* BUG transformation ici ? *)
 Qed.
+*)
+Admitted.
 
 Parameter mem : forall (A:Set), A -> list A -> Prop.
 
@@ -46,13 +47,13 @@ Admitted.
 Definition f (x:Z) (y:Z) := x+y.
 
 Goal f 1 2 = 3.
-why.
+ae.
 Qed.
 
 Definition id A (x:A) := x.
 
 Goal id nat O = O.
-why.
+ae.
 Qed.
 
 (* inductive types *)
@@ -62,17 +63,17 @@ 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.
-why.
+ae.
 Qed.
 
 Goal  forall (a:Set), forall x:Z, x=1 -> P S -> let y := 2 in x+1=y.
 intros.
-why.
+ae.
 Qed.
 
 Goal  forall x: list nat, x=x.
 intros.
-why.
+ae.
 Qed.
 
 (* Mutually inductive types *)
@@ -86,7 +87,7 @@ with forest : Set :=
   | Cons : tree -> forest -> forest.
 
 Goal forall x : tree, x=x.
-why.
+ae.
 Qed.
 
 (* Polymorphic, Mutually inductive types *)
@@ -100,7 +101,7 @@ with pforest (a:Set) : Set :=
   | PCons : ptree a -> pforest a -> pforest a.
 
 Goal forall x : ptree Z, x=x.
-why.
+ae.
 Qed.
 
 (* the same, without parameters *)
@@ -114,6 +115,6 @@ with pforest' : Type -> Type :=
   | PCons' : forall (a:Type), ptree' a -> pforest' a -> pforest' a.
 
 Goal forall x : ptree' Z, x=x.
-why.
+ae.
 Qed.
 

src/coq-plugin/whytac.ml

@@ -24,18 +24,23 @@ let debug =
 
 let config = Whyconf.read_config None
 
-let env = Env.create_env (Typing.retrieve config.loadpath)
-    
-let config_prover = 
-  try Util.Mstr.find "alt-ergo" config.provers 
-  with Not_found -> assert false
-
-let drv = Driver.load_driver env config_prover.driver
-let command = config_prover.command
 let timelimit = match config.timelimit with
   | None -> 3
   | Some t -> t
 
+let env = Env.create_env (Typing.retrieve config.loadpath)
+    
+let provers = Hashtbl.create 17
+
+let get_prover s = 
+  try 
+    Hashtbl.find provers s 
+  with Not_found -> 
+    let cp = Util.Mstr.find s config.provers in
+    let drv = Driver.load_driver env cp.driver in
+    Hashtbl.add provers s (cp, drv);
+    cp, drv
+
 (* Coq constants *)
 let logic_dir = ["Coq";"Logic";"Decidable"]
 
@@ -705,12 +710,14 @@ let tr_goal gl =
   task := Task.add_prop_decl !task Decl.Pgoal pr f
 
 
-let whytac gl =
+let whytac s gl =
   let concl_type = pf_type_of gl (pf_concl gl) in
   if not (is_Prop concl_type) then error "Conclusion is not a Prop";
   task := Task.use_export None Theory.builtin_theory;
   try
     tr_goal gl;
+    let cp, drv = get_prover s in
+    let command = cp.command in
     if debug then Format.printf "@[%a@]@\n---@." Pretty.print_task !task;
     if debug then Format.printf "@[%a@]@\n---@." (Prover.print_task drv) !task;
     let res = Prover.prove_task ~debug ~command ~timelimit drv !task () in
@@ -725,11 +732,43 @@ let whytac gl =
   with NotFO ->
     error "Not a first order goal"
 
-
+(***
 let _ =
-  Tacinterp.overwriting_add_tactic "Why" (fun _ -> whytac);
+  Tacinterp.overwriting_add_tactic "Why" (fun s -> whytac s);
   Egrammar.extend_tactic_grammar "Why" [[Egrammar.TacTerm "why"]]
+***)
 
+open Pcoq
+let h_Why s =
+  Refiner.abstract_extended_tactic "Why"
+    [Genarg.in_gen Genarg.wit_string s] (whytac s)
+let _ =
+  try
+    let _ =
+      Tacinterp.add_tactic "Why"
+        (function
+           [s] when Genarg.genarg_tag s = Genarg.StringArgType && true ->
+             let s = Genarg.out_gen Genarg.wit_string s in whytac s
+         | _ -> failwith "Tactic extension: cannot occur")
+    in
+    List.iter
+      (fun s ->
+         Tacinterp.add_primitive_tactic s
+           (Tacexpr.TacAtom
+              (dummy_loc, Tacexpr.TacExtend (dummy_loc, s, []))))
+      []
+  with e -> pp (Cerrors.explain_exn e)
+let _ =
+  Egrammar.extend_tactic_grammar "Why"
+    [[Egrammar.TacTerm "why";
+      Egrammar.TacNonTerm
+        (dummy_loc,
+         (Gramext.Snterm (Pcoq.Gram.Entry.obj Prim.string),
+          Genarg.StringArgType),
+         Some "s")]]
+let _ =
+  List.iter Pptactic.declare_extra_tactic_pprule
+    ["Why", [Genarg.StringArgType], (0, [Some "why"; None])]
 
 (*
 Local Variables: