Here comes the commit, announced long ago, of the new tactic engine.

This is a fairly large commit (around 140 files and 7000 lines of code
impacted), it will cause some troubles for sure (I've listed the know
regressions below, there is bound to be more).
At this state of developpement it brings few features to the user, as
the old tactics were
ported with no change. Changes are on the side of the developer mostly.

Here comes a list of the major changes. I will stay brief, but the code
is hopefully well documented so that it is reasonably easy to infer the
details from it.

Feature developer-side:
* Primitives for a "real" refine tactic (generating a goal for each
evar).
* Abstract type of tactics, goals and proofs
* Tactics can act on several goals (formally all the focused goals). An
interesting consequence of this is that the tactical (. ; [ . | ... ])
can be separated in two
tacticals (. ; .) and ( [ . | ... ] ) (although there is a conflict for
this particular syntax). We can also imagine a tactic to reorder the
goals.
* Possibility for a tactic to pass a value to following tactics (a
typical example is
an intro function which tells the following tactics which name it
introduced).
* backtracking primitives for tactics (it is now possible to implement a
tactical '+'
  with (a+b);c equivalent to (a;c+b;c) (itself equivalent to
(a;c||b;c)). This is a valuable
  tool to implement tactics like "auto" without nowing of the
implementation of tactics.
* A notion of proof modes, which allows to dynamically change the parser
for tactics. It is controlled at user level with the keywords Set
Default Proof Mode (this is the proof mode which is loaded at the start
of each proof) and Proof Mode (switches the proof mode of the current
proof) to control them.
* A new primitive Evd.fold_undefined which operates like an Evd.fold,
except it only goes through the evars whose body is Evar_empty. This is
a common operation throughout the code,
some of the fold-and-test-if-empty occurences have been replaced by
fold_undefined. For now,
it is only implemented as a fold-and-test, but we expect to have some
optimisations coming some day, as there can be a lot of evars in an
evar_map with this new implementation (I've observed a couple of
thousands), whereas there are rarely more than a dozen undefined ones.
Folding being a linear operation, this might result in a significant
speed-up.
* The declarative mode has been moved into the plugins. This is made
possible by the proof mode feature. I tried to document it so that it
can serve as a tutorial for a tactic mode plugin.

Features user-side:
* Unfocus does not go back to the root of the proof if several Focus-s
have been performed.
  It only goes back to the point where it was last focused.
* experimental (non-documented) support of keywords
BeginSubproof/EndSubproof:
  BeginSubproof focuses on first goal, one can unfocus only with
EndSubproof, and only
  if the proof is completed for that goal.
* experimental (non-documented) support for bullets ('+', '-' and '*')
  they act as hierarchical BeginSubproof/EndSubproof:
  First time one uses '+' (for instance) it focuses on first goal, when
the subproof is
  completed, one can use '+' again which unfocuses and focuses on next
first goal.
  Meanwhile, one cas use '*' (for instance) to focus more deeply.

Known regressions:
* The xml plugin had some functions related to proof trees. As the
structure of proof changed significantly, they do not work anymore.
* I do not know how to implement info or show script in this new engine.
Actually I don't even know what they were suppose to actually mean in
earlier versions either. I wager they would require some calm thinking
before going back to work.
* Declarative mode not entirely working (in particular proofs by
induction need to be restored).
* A bug in the inversion tactic (observed in some contributions)
* A bug in Program (observed in some contributions)
* Minor change in the 'old' type of tactics causing some contributions
to fail.
* Compilation time takes about 10-15% longer for unknown reasons (I
suspect it might be linked to the fact that I don't perform any
reduction at QED-s, and also to some linear operations on evar_map-s
(see Evd.fold_undefined above)).


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12961 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 190 insertions, 0 deletions

diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml
new file mode 100644
index 0000000000..40c712cdff
--- /dev/null
+++ b/plugins/decl_mode/ppdecl_proof.ml
@@ -0,0 +1,190 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+open Util
+open Pp
+open Decl_expr
+open Names
+open Nameops
+
+let pr_constr = Printer.pr_constr_env
+let pr_tac = Pptactic.pr_glob_tactic
+let pr_pat mpat = Ppconstr.pr_cases_pattern_expr mpat.pat_expr
+
+let pr_label = function
+    Anonymous -> mt ()
+  | Name id -> pr_id id ++ spc () ++ str ":" ++ spc ()
+
+let pr_justification_items env = function
+    Some [] -> mt ()
+  | Some (_::_ as l) ->
+      spc () ++ str "by" ++ spc () ++
+	prlist_with_sep (fun () -> str ",") (pr_constr env) l
+  | None -> spc () ++ str "by *"
+
+let pr_justification_method env = function
+    None -> mt ()
+  | Some tac ->
+      spc () ++ str "using" ++ spc () ++ pr_tac env tac
+
+let pr_statement pr_it env st =
+  pr_label st.st_label ++ pr_it env st.st_it
+
+let pr_or_thesis pr_this env = function
+    Thesis Plain -> str "thesis"
+  | Thesis (For id) ->
+      str "thesis" ++ spc() ++ str "for" ++ spc () ++ pr_id id
+  | This c -> pr_this env c
+
+let pr_cut pr_it env c =
+  hov 1 (pr_it env c.cut_stat) ++
+    pr_justification_items env c.cut_by ++
+    pr_justification_method env c.cut_using
+
+let type_or_thesis = function
+    Thesis _ -> Term.mkProp
+  | This c -> c
+
+let _I x = x
+
+let rec print_hyps pconstr gtyp env sep _be _have hyps =
+  let pr_sep = if sep then str "and" ++ spc () else mt () in
+    match hyps with
+	(Hvar _ ::_) as rest ->
+	  spc () ++ pr_sep ++ str _have ++
+	    print_vars pconstr gtyp env false _be _have rest
+      | Hprop st :: rest ->
+	  begin
+	    let nenv =
+	      match st.st_label with
+		  Anonymous -> env
+		| Name id -> Environ.push_named (id,None,gtyp st.st_it) env in
+	      spc() ++ pr_sep ++ pr_statement pconstr env st ++
+		print_hyps pconstr gtyp nenv true _be _have rest
+	  end
+      | [] -> mt ()
+
+and print_vars pconstr gtyp env sep _be _have vars =
+  match vars with
+    Hvar st :: rest ->
+      begin
+	let nenv =
+	  match st.st_label with
+	      Anonymous -> anomaly "anonymous variable"
+	    | Name id -> Environ.push_named (id,None,st.st_it) env in
+	let pr_sep = if sep then pr_coma () else mt () in
+		spc() ++ pr_sep ++
+		   pr_statement pr_constr env st ++
+		  print_vars pconstr gtyp nenv true _be _have rest
+      end
+   | (Hprop _ :: _) as rest ->
+      let _st =  if _be then
+	str "be such that"
+      else
+	str "such that" in
+	spc() ++ _st ++  print_hyps pconstr gtyp env false _be _have rest
+  | [] -> mt ()
+
+let pr_suffices_clause env (hyps,c) =
+    print_hyps pr_constr _I env false false "to have" hyps ++ spc () ++
+       str "to show" ++ spc () ++ pr_or_thesis pr_constr env c
+
+let pr_elim_type = function
+    ET_Case_analysis -> str "cases"
+  | ET_Induction -> str "induction"
+
+let pr_casee env =function
+    Real c -> str "on" ++ spc () ++ pr_constr env c
+  | Virtual cut -> str "of" ++ spc () ++ pr_cut (pr_statement pr_constr) env cut
+
+let pr_side = function
+    Lhs -> str "=~"
+  | Rhs -> str "~="
+
+let rec pr_bare_proof_instr _then _thus env = function
+  | Pescape -> str "escape"
+  | Pthen i -> pr_bare_proof_instr true _thus env i
+  | Pthus i -> pr_bare_proof_instr _then true env i
+  | Phence i -> pr_bare_proof_instr true true env i
+  | Pcut c ->
+      begin
+	match _then,_thus with
+	    false,false -> str "have" ++ spc () ++
+	      pr_cut (pr_statement (pr_or_thesis pr_constr)) env c
+	  | false,true  -> str "thus" ++ spc () ++
+	      pr_cut (pr_statement (pr_or_thesis pr_constr)) env c
+	  | true,false  -> str "then" ++ spc () ++
+	      pr_cut (pr_statement (pr_or_thesis pr_constr)) env c
+	  | true,true   -> str "hence" ++ spc () ++
+	      pr_cut (pr_statement (pr_or_thesis pr_constr)) env c
+      end
+  | Psuffices c ->
+      str "suffices" ++  pr_cut pr_suffices_clause env c
+  | Prew (sid,c) ->
+      (if _thus then str "thus" else str "    ") ++ spc () ++
+	pr_side sid ++ spc () ++ pr_cut (pr_statement pr_constr) env c
+  | Passume hyps ->
+      str "assume" ++ print_hyps pr_constr _I env false false "we have" hyps
+  | Plet hyps ->
+      str "let" ++ print_vars pr_constr _I env false true "let" hyps
+  | Pclaim st ->
+      str "claim" ++ spc () ++ pr_statement pr_constr env st
+  | Pfocus st ->
+      str "focus on" ++ spc () ++ pr_statement pr_constr env st
+  | Pconsider (id,hyps) ->
+      str "consider" ++ print_vars pr_constr _I env false false "consider" hyps
+      ++ spc () ++ str "from " ++ pr_constr env id
+  | Pgiven hyps ->
+      str "given" ++ print_vars pr_constr _I env false false "given" hyps
+  | Ptake witl ->
+      str "take" ++ spc () ++
+	prlist_with_sep pr_coma (pr_constr env) witl
+  | Pdefine (id,args,body) ->
+      str "define" ++ spc () ++ pr_id id ++ spc () ++
+	prlist_with_sep spc
+	(fun st -> str "(" ++
+	   pr_statement pr_constr env st ++ str ")") args ++ spc () ++
+	str "as" ++ (pr_constr env body)
+  | Pcast (id,typ) ->
+      str "reconsider" ++ spc () ++
+	pr_or_thesis (fun _ -> pr_id) env id ++ spc () ++
+	str "as" ++ spc () ++ (pr_constr env typ)
+  | Psuppose hyps ->
+      str "suppose" ++
+	print_hyps pr_constr _I env false false "we have" hyps
+  | Pcase (params,pat,hyps) ->
+      str "suppose it is" ++ spc () ++ pr_pat pat ++
+	(if params = [] then mt () else
+	   (spc () ++ str "with" ++ spc () ++
+	      prlist_with_sep spc
+	      (fun st -> str "(" ++
+		 pr_statement pr_constr env st ++ str ")") params ++ spc ()))
+      ++
+	(if hyps = [] then mt () else
+	   (spc () ++ str "and" ++
+	      print_hyps (pr_or_thesis pr_constr) type_or_thesis
+	      env false false "we have" hyps))
+  | Pper (et,c) ->
+      str "per" ++ spc () ++ pr_elim_type et ++ spc () ++
+      pr_casee env c
+  | Pend (B_elim et) -> str "end" ++ spc () ++ pr_elim_type et
+  | _ -> anomaly "unprintable instruction"
+
+let pr_emph = function
+    0 -> str "    "
+  | 1 -> str "*   "
+  | 2 -> str "**  "
+  | 3 -> str "*** "
+  | _ -> anomaly "unknown emphasis"
+
+let pr_proof_instr env instr =
+  pr_emph instr.emph ++ spc () ++
+    pr_bare_proof_instr false false env instr.instr
+