A unified backtrack mechanism, with a basic "Show Script" as side-effect

 Migrate the backtracking code from ide_slave.ml into a new backtrack.ml.
 In particular the history stack of commands that used to be there is now
 non-coqide-specific.

 ** Adapted commands **

 - "Show Script": a basic functional version is restored (and the printing
 of scripts at Qed in coqtop). No indentation, one Coq command per line,
 based on the vernac_expr asts recorded in the history stack, printed via
 Ppvernac.

 - "Back n" : now mimics the backtrack of coqide: it goes n steps back
 (both commands and proofs), and maybe more if needed to avoid re-entering
 a proof (it outputs a warning in this case).

 - "BackTo n" : still try to go back to state n, but it also handles the
 proof state, and it may end on some state n' <= n if needed to avoid
 re-entering a proof. Ideally, it could someday be used by ProofGeneral
 instead of the complex Backtrack command.

 ** Compatible commands **

 - "Backtrack" is left intact from compatibility with current ProofGeneral.
 We simply re-synchronize the command history stack after each Backtrack.

 - "Undo" is kept as a standard command, not a backtracking one, a bit like
 "Focus". Same for "Restart" and "Abort". All of these are now accepted
 in coqide (Undo simply triggers a warning).

 - Undocumented command "Undo To n" (counting from start of proof instead of
 from end) also keep its semantics, it is simply made compatible with
 the new stack mechanism.

 ** New restrictions **

 We now forbid backtracking commands (Reset* / Back*) inside files
 when Load'ing or compiling, or inside VernacList/VernacTime/VernacFail.
 Too much work dealing with these situation that nobody uses.

 ** Internal details **

 Internally, the command stack differs a bit from what was in Ide_slave
 earlier (which was inspired by lisp code in ProofGeneral). We now tag
 commands that are unreachable by a backtrack, due to some proof being
 finished, aborted, restarted, or partly Undo'ed. This induce a bit of
 bookkeeping during Qed/Abort/Restart/Undo, but then the backtracking code
 is straightforward: we simply search backward the first reachable state
 starting from the desired place. We don't depend anymore on the proof
 names (apart in the last proof block), It's more robust this way
 (think of re-entering a M.foo from an outside proof foo).

 Many internal clarifications in Lib, Vernac, etc. For instance
 "Reset Initial" is now just a BackTo 1, while "Reset foo" now calls
 (Lib.label_before_name "foo"), and performs a BackTo to the corresponding
 label.

 Concerning Coqide, we directly suppress the regular printing of goals
 via a flag in Vernacentries. This avoid relying on a classification
 of commands in Ide_slave as earlier.

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

3 files changed, 231 insertions, 5 deletions

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index a9b162819..e4695792b 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1143,7 +1143,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 
       mk_correct_id f_id
     in
-     ignore(try Vernacentries.vernac_reset_name (Pp.dummy_loc,first_lemma_id) with _ -> ());
+    (try Backtrack.reset_name (Pp.dummy_loc,first_lemma_id) with _ -> ());
     raise e
 
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 872d3be4a..7613c6765 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1471,6 +1471,7 @@ let (com_eqn : int -> identifier ->
 
 let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq
     generate_induction_principle using_lemmas : unit =
+  let previous_label = Lib.current_command_label () in
   let function_type = interp_constr Evd.empty (Global.env()) type_of_f in
   let env = push_named (function_name,None,function_type) (Global.env()) in
   (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type);  *)
@@ -1522,7 +1523,6 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
 	  then pperrnl (str "Cannot create equation Lemma " ++ Errors.print e)
 	  else anomaly "Cannot create equation Lemma"
 	  ;
-(* 	  ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ()); *)
 	  true
 	end
     in
@@ -1554,9 +1554,8 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
       hook 
   with e ->
     begin
-      ignore(try Vernacentries.vernac_reset_name (Pp.dummy_loc,functional_id) with _ -> ());
-(*       anomaly "Cannot create termination Lemma" *)
+      (try ignore (Backtrack.backto previous_label) with _ -> ());
+      (*       anomaly "Cannot create termination Lemma" *)
       raise e
     end
 
-
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
new file mode 100644
index 000000000..a8d69bdcf
--- /dev/null
+++ b/plugins/subtac/subtac.ml
@@ -0,0 +1,227 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Compat
+open Global
+open Pp
+open Errors
+open Util
+open Names
+open Sign
+open Evd
+open Term
+open Termops
+open Namegen
+open Reductionops
+open Environ
+open Type_errors
+open Typeops
+open Libnames
+open Classops
+open List
+open Recordops
+open Evarutil
+open Pretype_errors
+open Glob_term
+open Evarconv
+open Pattern
+open Vernacexpr
+
+open Subtac_coercion
+open Subtac_utils
+open Coqlib
+open Printer
+open Subtac_errors
+open Eterm
+
+let require_library dirpath =
+  let qualid = (dummy_loc, qualid_of_dirpath (dirpath_of_string dirpath)) in
+    Library.require_library [qualid] None
+
+open Pp
+open Ppconstr
+open Decl_kinds
+open Tacinterp
+open Tacexpr
+
+let solve_tccs_in_type env id isevars evm c typ =
+  if not (Evd.is_empty evm) then
+    let stmt_id = Nameops.add_suffix id "_stmt" in
+    let obls, _, c', t' = eterm_obligations env stmt_id !isevars evm 0 ~status:Expand c typ in
+      match Subtac_obligations.add_definition stmt_id ~term:c' typ obls with
+      | Subtac_obligations.Defined cst -> constant_value (Global.env())
+	  (match cst with ConstRef kn -> kn | _ -> assert false)
+      | _ ->
+	  errorlabstrm "start_proof"
+	    (str "The statement obligations could not be resolved automatically, " ++ spc () ++
+		str "write a statement definition first.")
+  else
+    let _ = Typeops.infer_type env c in c
+
+
+let start_proof_com env isevars sopt kind (bl,t) hook =
+  let id = match sopt with
+    | Some (loc,id) ->
+        (* We check existence here: it's a bit late at Qed time *)
+        if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then
+          user_err_loc (loc,"start_proof",pr_id id ++ str " already exists");
+        id
+    | None ->
+	next_global_ident_away (id_of_string "Unnamed_thm")
+	  (Pfedit.get_all_proof_names ())
+  in
+  let evm, c, typ, imps =
+    Subtac_pretyping.subtac_process ~is_type:true env isevars id [] (Topconstr.prod_constr_expr t bl) None
+  in
+  let c = solve_tccs_in_type env id isevars evm c typ in
+    Lemmas.start_proof id kind c (fun loc gr ->
+      Impargs.declare_manual_implicits (loc = Local) gr ~enriching:true [imps];
+      hook loc gr)
+
+let start_proof_and_print env isevars idopt k t hook =
+  start_proof_com env isevars idopt k t hook;
+  Vernacentries.print_subgoals ()
+
+let _ = Detyping.set_detype_anonymous (fun loc n -> GVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n)))
+
+let assumption_message id =
+  Flags.if_verbose message ((string_of_id id) ^ " is assumed")
+
+let declare_assumptions env isevars idl is_coe k bl c nl =
+  if not (Pfedit.refining ()) then
+    let id = snd (List.hd idl) in
+    let evm, c, typ, imps =
+      Subtac_pretyping.subtac_process env isevars id [] (Topconstr.prod_constr_expr c bl) None
+    in
+    let c = solve_tccs_in_type env id isevars evm c typ in
+      List.iter (Command.declare_assumption is_coe k c imps false nl) idl
+  else
+    errorlabstrm "Command.Assumption"
+	(str "Cannot declare an assumption while in proof editing mode.")
+
+let dump_constraint ty ((loc, n), _, _) =
+  match n with
+    | Name id -> Dumpglob.dump_definition (loc, id) false ty
+    | Anonymous -> ()
+
+let dump_variable lid = ()
+
+let vernac_assumption env isevars kind l nl =
+  let global = fst kind = Global in
+    List.iter (fun (is_coe,(idl,c)) ->
+      if Dumpglob.dump () then
+	List.iter (fun lid ->
+	  if global then Dumpglob.dump_definition lid (not global) "ax"
+	  else dump_variable lid) idl;
+      declare_assumptions env isevars idl is_coe kind [] c nl) l
+
+let check_fresh (loc,id) =
+  if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then
+    user_err_loc (loc,"",pr_id id ++ str " already exists")
+
+let subtac (loc, command) =
+  check_required_library ["Coq";"Init";"Datatypes"];
+  check_required_library ["Coq";"Init";"Specif"];
+  let env = Global.env () in
+  let isevars = ref (create_evar_defs Evd.empty) in
+  try
+  match command with
+  | VernacDefinition (defkind, (_, id as lid), expr, hook) ->
+      check_fresh lid;
+      Dumpglob.dump_definition lid false "def";
+      (match expr with
+      | ProveBody (bl, t) ->
+	  start_proof_and_print env isevars (Some lid) (Global, DefinitionBody Definition) (bl,t)
+	    (fun _ _ -> ())
+      | DefineBody (bl, _, c, tycon) ->
+	  ignore(Subtac_pretyping.subtac_proof defkind hook env isevars id bl c tycon))
+  | VernacFixpoint l ->
+      List.iter (fun ((lid, _, _, _, _), _) ->
+	check_fresh lid;
+	Dumpglob.dump_definition lid false "fix") l;
+      let _ = trace (str "Building fixpoint") in
+	ignore(Subtac_command.build_recursive l)
+
+  | VernacStartTheoremProof (thkind, [Some id, (bl,t,guard)], lettop, hook) ->
+      if guard <> None then
+        error "Do not support building theorems as a fixpoint.";
+      Dumpglob.dump_definition id false "prf";
+      if not(Pfedit.refining ()) then
+	if lettop then
+	  errorlabstrm "Subtac_command.StartProof"
+	    (str "Let declarations can only be used in proof editing mode");
+      if Lib.is_modtype () then
+	errorlabstrm "Subtac_command.StartProof"
+	  (str "Proof editing mode not supported in module types");
+      check_fresh id;
+      start_proof_and_print env isevars (Some id) (Global, Proof thkind) (bl,t) hook
+
+  | VernacAssumption (stre,nl,l) ->
+      vernac_assumption env isevars stre l nl
+
+  | VernacInstance (abst, glob, sup, is, props, pri) ->
+      dump_constraint "inst" is;
+      if abst then
+	error "Declare Instance not supported here.";
+      ignore(Subtac_classes.new_instance ~global:glob sup is props pri)
+
+  | VernacCoFixpoint l ->
+      if Dumpglob.dump () then
+	List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "cofix") l;
+      ignore(Subtac_command.build_corecursive l)
+
+  (*| VernacEndProof e ->
+    subtac_end_proof e*)
+
+  | _ -> user_err_loc (loc,"", str ("Invalid Program command"))
+  with
+  | Typing_error e ->
+      msg_warning (str "Type error in Program tactic:");
+      let cmds =
+	(match e with
+	| NonFunctionalApp (loc, x, mux, e) ->
+	    str "non functional application of term " ++
+	      e ++ str " to function " ++ x ++ str " of (mu) type " ++ mux
+	| NonSigma (loc, t) ->
+	    str "Term is not of Sigma type: " ++ t
+	| NonConvertible (loc, x, y) ->
+	    str "Unconvertible terms:" ++ spc () ++
+	      x ++ spc () ++ str "and" ++ spc () ++ y
+	| IllSorted (loc, t) ->
+	    str "Term is ill-sorted:" ++ spc () ++ t
+	)
+      in msg_warning cmds
+
+  | Subtyping_error e ->
+      msg_warning (str "(Program tactic) Subtyping error:");
+      let cmds =
+	match e with
+	| UncoercibleInferType (loc, x, y) ->
+	    str "Uncoercible terms:" ++ spc ()
+	    ++ x ++ spc () ++ str "and" ++ spc () ++ y
+	| UncoercibleInferTerm (loc, x, y, tx, ty) ->
+	    str "Uncoercible terms:" ++ spc ()
+	    ++ tx ++ spc () ++ str "of" ++ spc () ++ str "type" ++ spc () ++ x
+	    ++ str "and" ++ spc() ++ ty ++ spc () ++ str "of" ++ spc () ++ str "type" ++ spc () ++ y
+	| UncoercibleRewrite (x, y) ->
+	    str "Uncoercible terms:" ++ spc ()
+	    ++ x ++ spc () ++ str "and" ++ spc () ++ y
+      in msg_warning cmds
+
+  | Cases.PatternMatchingError (env, exn) as e -> raise e
+
+  | Type_errors.TypeError (env, exn) as e -> raise e
+
+  | Pretype_errors.PretypeError (env, _, exn) as e -> raise e
+
+  | (Loc.Exc_located (loc, Proof_type.LtacLocated (_,e')) |
+     Loc.Exc_located (loc, e') as e) -> raise e
+
+  | e ->
+      (*       msg_warning (str "Uncaught exception: " ++ Errors.print e); *)
+      raise e