aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--ide/coq_lex.mll2
-rw-r--r--library/lib.ml83
-rw-r--r--library/lib.mli42
-rw-r--r--plugins/funind/invfun.ml2
-rw-r--r--plugins/funind/recdef.ml7
-rw-r--r--plugins/subtac/subtac.ml227
-rw-r--r--proofs/pfedit.mli4
-rw-r--r--toplevel/backtrack.ml225
-rw-r--r--toplevel/backtrack.mli93
-rw-r--r--toplevel/coqtop.ml10
-rw-r--r--toplevel/ide_slave.ml308
-rw-r--r--toplevel/toplevel.ml3
-rw-r--r--toplevel/toplevel.mllib1
-rw-r--r--toplevel/vernac.ml44
-rw-r--r--toplevel/vernac.mli9
-rw-r--r--toplevel/vernacentries.ml116
-rw-r--r--toplevel/vernacentries.mli19
-rw-r--r--toplevel/vernacexpr.ml20
18 files changed, 780 insertions, 435 deletions
diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll
index f0f1afb74..314e15e3e 100644
--- a/ide/coq_lex.mll
+++ b/ide/coq_lex.mll
@@ -24,7 +24,7 @@
let one_word_commands =
[ "Add" ; "Check"; "Eval"; "Extraction" ;
"Load" ; "Undo"; "Goal";
- "Proof" ; "Print";"Save" ;
+ "Proof" ; "Print";"Save" ; "Restart";
"End" ; "Section"; "Chapter"; "Transparent"; "Opaque"; "Comments" ]
in
let one_word_declarations =
diff --git a/library/lib.ml b/library/lib.ml
index 54087ce1c..40a427e49 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -573,44 +573,16 @@ let reset_to_gen test =
let reset_to sp = reset_to_gen (fun x -> fst x = sp)
-let reset_name (loc,id) =
- let (sp,_) =
- try
- find_entry_p (fun (sp,_) -> let (_,spi) = repr_path (fst sp) in id = spi)
- with Not_found ->
- user_err_loc (loc,"reset_name",pr_id id ++ str ": no such entry")
- in
- reset_to sp
-
-let is_mod_node = function
- | OpenedModule _ | OpenedSection _
- | ClosedModule _ | ClosedSection _ -> true
- | Leaf o -> let t = object_tag o in t = "MODULE" || t = "MODULE TYPE"
- || t = "MODULE ALIAS"
- | _ -> false
-
-(* Reset on a module or section name in order to bypass constants with
- the same name *)
-
-let reset_mod (loc,id) =
- let (_,before) =
- try
- find_split_p (fun (sp,node) ->
- let (_,spi) = repr_path (fst sp) in id = spi
- && is_mod_node node)
- with Not_found ->
- user_err_loc (loc,"reset_mod",pr_id id ++ str ": no such entry")
- in
- set_lib_stk before
+let first_command_label = 1
-let mark_end_of_command, current_command_label, set_command_label =
- let n = ref 0 in
+let mark_end_of_command, current_command_label, reset_command_label =
+ let n = ref (first_command_label-1) in
(fun () ->
match !lib_stk with
(_,Leaf o)::_ when object_tag o = "DOT" -> ()
| _ -> incr n;add_anonymous_leaf (inLabel !n)),
(fun () -> !n),
- (fun x -> n:=x)
+ (fun x -> n:=x;add_anonymous_leaf (inLabel x))
let is_label_n n x =
match x with
@@ -623,21 +595,21 @@ let is_label_n n x =
let reset_label n =
if n >= current_command_label () then
error "Cannot backtrack to the current label or a future one";
- let res = reset_to_gen (is_label_n n) in
+ reset_to_gen (is_label_n n);
(* forget state numbers after n only if reset succeeded *)
- set_command_label (n-1);
- res
+ reset_command_label n
-let rec back_stk n stk =
- match stk with
- (sp,Leaf o)::tail when object_tag o = "DOT" ->
- if n=0 then sp else back_stk (n-1) tail
- | _::tail -> back_stk n tail
- | [] -> error "Reached begin of command history"
+(** Search the last label registered before defining [id] *)
-let back n =
- reset_to (back_stk n !lib_stk);
- set_command_label (current_command_label () - n - 1)
+let label_before_name (loc,id) =
+ let found = ref false in
+ let search = function
+ | (_,Leaf o) when !found && object_tag o = "DOT" -> true
+ | (sp,_) -> (if id = snd (repr_path (fst sp)) then found := true); false
+ in
+ match find_entry_p search with
+ | (_,Leaf o) -> outLabel o
+ | _ -> raise Not_found
(* State and initialization. *)
@@ -657,29 +629,6 @@ let init () =
path_prefix := initial_prefix;
init_summaries()
-(* Initial state. *)
-
-let initial_state = ref None
-
-let declare_initial_state () =
- let name = add_anonymous_entry (FrozenState (freeze_summaries())) in
- initial_state := Some name
-
-let reset_initial () =
- match !initial_state with
- | None ->
- error "Resetting to the initial state is possible only interactively"
- | Some sp ->
- begin match split_lib sp with
- | (_,[_,FrozenState fs as hd],before) ->
- lib_stk := hd::before;
- recalc_path_prefix ();
- set_command_label 0;
- unfreeze_summaries fs
- | _ -> assert false
- end
-
-
(* Misc *)
let mp_of_global ref =
diff --git a/library/lib.mli b/library/lib.mli
index df931f060..781ecfe32 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -62,17 +62,6 @@ val add_leaves : Names.identifier -> Libobject.obj list -> Libnames.object_name
val add_frozen_state : unit -> unit
-(** Adds a "dummy" entry in lib_stk with a unique new label number. *)
-val mark_end_of_command : unit -> unit
-
-(** Returns the current label number *)
-val current_command_label : unit -> int
-
-(** [reset_label n] resets [lib_stk] to the label n registered by
- [mark_end_of_command()]. It forgets the label and anything
- registered after it. The label should be strictly in the past. *)
-val reset_label : int -> unit
-
(** {6 ... } *)
(** The function [contents_after] returns the current library segment,
starting from a given section path. If not given, the entire segment
@@ -151,15 +140,28 @@ val remove_section_part : Libnames.global_reference -> Names.dir_path
val open_section : Names.identifier -> unit
val close_section : unit -> unit
-(** {6 Backtracking (undo). } *)
+(** {6 Backtracking } *)
-val reset_to : Libnames.object_name -> unit
-val reset_name : Names.identifier Pp.located -> unit
-val reset_mod : Names.identifier Pp.located -> unit
+(** NB: The next commands are low-level ones, do not use them directly
+ otherwise the command history stack in [Backtrack] will be out-of-sync.
+ Also note that [reset_initial] is now [reset_label first_command_label] *)
-(** [back n] resets to the place corresponding to the {% $ %}n{% $ %}-th call of
- [mark_end_of_command] (counting backwards) *)
-val back : int -> unit
+(** Adds a "dummy" entry in lib_stk with a unique new label number. *)
+val mark_end_of_command : unit -> unit
+
+(** Returns the current label number *)
+val current_command_label : unit -> int
+
+(** The first label number *)
+val first_command_label : int
+
+(** [reset_label n] resets [lib_stk] to the label n registered by
+ [mark_end_of_command()]. It forgets anything registered after
+ this label. The label should be strictly in the past. *)
+val reset_label : int -> unit
+
+(** search the label registered immediately before adding some definition *)
+val label_before_name : Names.identifier Pp.located -> int
(** {6 We can get and set the state of the operations (used in [States]). } *)
@@ -170,10 +172,6 @@ val unfreeze : frozen -> unit
val init : unit -> unit
-val declare_initial_state : unit -> unit
-val reset_initial : unit -> unit
-
-
(** XML output hooks *)
val set_xml_open_section : (Names.identifier -> unit) -> unit
val set_xml_close_section : (Names.identifier -> unit) -> unit
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
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index ceed54696..a271fb336 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -126,7 +126,9 @@ val current_proof_statement :
val get_current_proof_name : unit -> identifier
-(** [get_all_proof_names ()] returns the list of all pending proof names *)
+(** [get_all_proof_names ()] returns the list of all pending proof names.
+ The first name is the current proof, the other names may come in
+ any order. *)
val get_all_proof_names : unit -> identifier list
diff --git a/toplevel/backtrack.ml b/toplevel/backtrack.ml
new file mode 100644
index 000000000..a84550a5d
--- /dev/null
+++ b/toplevel/backtrack.ml
@@ -0,0 +1,225 @@
+(************************************************************************)
+(* 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 Names
+open Vernacexpr
+
+(** Command history stack
+
+ We maintain a stack of the past states of the system. Each
+ successfully interpreted command adds an [info] element
+ to this stack, storing what were the (label / current proof / ...)
+ just _after_ the interpretation of this command.
+
+ - A label is just an integer, starting from Lib.first_command_label
+ initially, and incremented at each new successful command.
+ - If some proofs are opened, we have their number in [nproofs],
+ the name of the current proof in [prfname], the current depth in
+ [prfdepth].
+ - Otherwise, [nproofs = 0], [prfname = None], [prfdepth = 0]
+ - The text of the command is stored (for Show Script currently).
+ - A command can be tagged later as non-"reachable" when the current proof
+ at the time of this command has been ended by Qed/Abort/Restart,
+ meaning we can't backtrack there.
+*)
+
+type info = {
+ label : int;
+ nproofs : int;
+ prfname : identifier option;
+ prfdepth : int;
+ cmd : vernac_expr;
+ mutable reachable : bool;
+}
+
+let history : info Stack.t = Stack.create ()
+
+(** For debug purpose, a dump of the history *)
+
+let dump_history () =
+ let l = ref [] in
+ Stack.iter (fun i -> l:=i::!l) history;
+ !l
+
+(** Basic manipulation of the command history stack *)
+
+exception Invalid
+
+let pop () = ignore (Stack.pop history)
+
+let npop n =
+ (* Since our history stack always contains an initial entry,
+ it's invalid to try to completely empty it *)
+ if n < 0 || n >= Stack.length history then raise Invalid
+ else for i = 1 to n do pop () done
+
+let top () =
+ try Stack.top history with Stack.Empty -> raise Invalid
+
+(** Search the history stack for a suitable location. We perform first
+ a non-destructive search: in case of search failure, the stack is
+ unchanged. *)
+
+exception Found of info
+
+let search test =
+ try
+ Stack.iter (fun i -> if test i then raise (Found i)) history;
+ raise Invalid
+ with Found i ->
+ while i != Stack.top history do pop () done
+
+(** Register the end of a command and store the current state *)
+
+let mark_command ast =
+ Lib.add_frozen_state();
+ Lib.mark_end_of_command();
+ Stack.push
+ { label = Lib.current_command_label ();
+ nproofs = List.length (Pfedit.get_all_proof_names ());
+ prfname = (try Some (Pfedit.get_current_proof_name ()) with _ -> None);
+ prfdepth = max 0 (Pfedit.current_proof_depth ());
+ reachable = true;
+ cmd = ast }
+ history
+
+(** Backtrack by aborting [naborts] proofs, then setting proof-depth back to
+ [pnum] and finally going to state number [snum]. *)
+
+let raw_backtrack snum pnum naborts =
+ for i = 1 to naborts do Pfedit.delete_current_proof () done;
+ Pfedit.undo_todepth pnum;
+ Lib.reset_label snum
+
+(** Re-sync the state of the system (label, proofs) with the top
+ of the history stack. We may end on some earlier state to avoid
+ re-opening proofs. This function will return the final label
+ and the number of extra backtracking steps performed. *)
+
+let sync nb_opened_proofs =
+ (* Backtrack by enough additional steps to avoid re-opening proofs.
+ Typically, when a Qed has been crossed, we backtrack to the proof start.
+ NB: We cannot reach the empty stack, since the first entry in the
+ stack has no opened proofs and is tagged as reachable.
+ *)
+ let extra = ref 0 in
+ while not (top()).reachable do incr extra; pop () done;
+ let target = top ()
+ in
+ (* Now the opened proofs at target is a subset of the opened proofs before
+ the backtrack, we simply abort the extra proofs (if any).
+ NB: It is critical here that proofs are nested in a regular way
+ (i.e. no more Resume or Suspend commands as earlier). This way, we can
+ simply count the extra proofs to abort instead of taking care of their
+ names.
+ *)
+ let naborts = nb_opened_proofs - target.nproofs in
+ (* We are now ready to do a low-level backtrack *)
+ raw_backtrack target.label target.prfdepth naborts;
+ (target.label, !extra)
+
+(** Backtracking by a certain number of (non-state-preserving) commands.
+ This is used by Coqide.
+ It may actually undo more commands than asked : for instance instead
+ of jumping back in the middle of a finished proof, we jump back before
+ this proof. The number of extra backtracked command is returned at
+ the end. *)
+
+let back count =
+ if count = 0 then 0
+ else
+ let nb_opened_proofs = List.length (Pfedit.get_all_proof_names ()) in
+ npop count;
+ snd (sync nb_opened_proofs)
+
+(** Backtracking to a certain state number, and reset proofs accordingly.
+ We may end on some earlier state if needed to avoid re-opening proofs.
+ Return the final state number. *)
+
+let backto snum =
+ if snum = Lib.current_command_label () then snum
+ else
+ let nb_opened_proofs = List.length (Pfedit.get_all_proof_names ()) in
+ search (fun i -> i.label = snum);
+ fst (sync nb_opened_proofs)
+
+(** Old [Backtrack] code with corresponding update of the history stack.
+ [Backtrack] is now deprecated (in favor of [BackTo]) but is kept for
+ compatibility with ProofGeneral. It's completely up to ProofGeneral
+ to decide where to go and how to adapt proofs. Note that the choices
+ of ProofGeneral are currently not always perfect (for instance when
+ backtracking an Undo). *)
+
+let backtrack snum pnum naborts =
+ raw_backtrack snum pnum naborts;
+ search (fun i -> i.label = snum)
+
+(** [reset_initial] resets the system and clears the command history
+ stack, only pushing back the initial entry. It should be equivalent
+ to [backto Lib.first_command_label], but sligthly more efficient. *)
+
+let reset_initial () =
+ let init_label = Lib.first_command_label in
+ if Lib.current_command_label () = init_label then ()
+ else begin
+ if Pfedit.refining() then Pfedit.delete_all_proofs ();
+ Lib.reset_label init_label;
+ Stack.clear history;
+ Stack.push
+ { label = init_label;
+ nproofs = 0;
+ prfname = None;
+ prfdepth = 0;
+ reachable = true;
+ cmd = VernacNop }
+ history
+ end
+
+(** Reset to the last known state just before defining [id] *)
+
+let reset_name id =
+ let lbl =
+ try Lib.label_before_name id with Not_found -> raise Invalid
+ in
+ ignore (backto lbl)
+
+(** When a proof is ended (via either Qed/Admitted/Restart/Abort),
+ old proof steps should be marked differently to avoid jumping back
+ to them:
+ - either this proof isn't there anymore in the proof engine
+ - either it's there but it's a more recent attempt after a Restart,
+ so we shouldn't mix the two.
+ We also mark as unreachable the proof steps cancelled via a Undo. *)
+
+let mark_unreachable ?(after=0) prf_lst =
+ let fix i = match i.prfname with
+ | None -> raise Not_found (* stop hacking the history outside of proofs *)
+ | Some p ->
+ if List.mem p prf_lst && i.prfdepth > after
+ then i.reachable <- false
+ in
+ try Stack.iter fix history with Not_found -> ()
+
+(** Parse the history stack for printing the script of a proof *)
+
+let get_script prf =
+ let script = ref [] in
+ let select i = match i.prfname with
+ | None -> raise Not_found
+ | Some p when p=prf && i.reachable -> script := i :: !script
+ | _ -> ()
+ in
+ (try Stack.iter select history with Not_found -> ());
+ (* Get rid of intermediate commands which don't grow the depth *)
+ let rec filter n = function
+ | [] -> []
+ | {prfdepth=d; cmd=c}::l when n < d -> c :: filter d l
+ | {prfdepth=d}::l -> filter d l
+ in
+ (* initial proof depth (after entering the lemma statement) is 1 *)
+ filter 1 !script
diff --git a/toplevel/backtrack.mli b/toplevel/backtrack.mli
new file mode 100644
index 000000000..f6c69d890
--- /dev/null
+++ b/toplevel/backtrack.mli
@@ -0,0 +1,93 @@
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+
+(** Command history stack
+
+ We maintain a stack of the past states of the system after each
+ (non-state-preserving) interpreted commands
+*)
+
+(** [mark_command ast] marks the end of a command:
+ - it stores a frozen state and a end of command in the Lib stack,
+ - it stores the current state information in the command history
+ stack *)
+
+val mark_command : Vernacexpr.vernac_expr -> unit
+
+(** The [Invalid] exception is raised when one of the following function
+ tries to empty the history stack, or reach an unknown states, etc.
+ The stack is preserved in these cases. *)
+
+exception Invalid
+
+(** Nota Bene: it is critical for the following functions that proofs
+ are nested in a regular way (i.e. no more Resume or Suspend commands
+ as earlier). *)
+
+(** Backtracking by a certain number of (non-state-preserving) commands.
+ This is used by Coqide.
+ It may actually undo more commands than asked : for instance instead
+ of jumping back in the middle of a finished proof, we jump back before
+ this proof. The number of extra backtracked command is returned at
+ the end. *)
+
+val back : int -> int
+
+(** Backtracking to a certain state number, and reset proofs accordingly.
+ We may end on some earlier state if needed to avoid re-opening proofs.
+ Return the state number on which we finally end. *)
+
+val backto : int -> int
+
+(** Old [Backtrack] code with corresponding update of the history stack.
+ [Backtrack] is now deprecated (in favor of [BackTo]) but is kept for
+ compatibility with ProofGeneral. It's completely up to ProofGeneral
+ to decide where to go and how to adapt proofs. Note that the choices
+ of ProofGeneral are currently not always perfect (for instance when
+ backtracking an Undo). *)
+
+val backtrack : int -> int -> int -> unit
+
+(** [reset_initial] resets the system and clears the command history
+ stack, only pushing back the initial entry. It should be equivalent
+ to [backto Lib.first_command_label], but sligthly more efficient. *)
+
+val reset_initial : unit -> unit
+
+(** Reset to the last known state just before defining [id] *)
+
+val reset_name : Names.identifier Pp.located -> unit
+
+(** When a proof is ended (via either Qed/Admitted/Restart/Abort),
+ old proof steps should be marked differently to avoid jumping back
+ to them:
+ - either this proof isn't there anymore in the proof engine
+ - either a proof with the same name is there, but it's a more recent
+ attempt after a Restart/Abort, we shouldn't mix the two.
+ We also mark as unreachable the proof steps cancelled via a Undo.
+*)
+
+val mark_unreachable : ?after:int -> Names.identifier list -> unit
+
+(** Parse the history stack for printing the script of a proof *)
+
+val get_script : Names.identifier -> Vernacexpr.vernac_expr list
+
+
+(** For debug purpose, a dump of the history *)
+
+type info = {
+ label : int;
+ nproofs : int;
+ prfname : Names.identifier option;
+ prfdepth : int;
+ cmd : Vernacexpr.vernac_expr;
+ mutable reachable : bool;
+}
+
+val dump_history : unit -> info list
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index d17d07300..bf5c84e64 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -248,10 +248,13 @@ let parse_args arglist =
| "-compat" :: [] -> usage ()
| "-vm" :: rem -> use_vm := true; parse rem
- | "-emacs" :: rem -> Flags.print_emacs := true; Pp.make_pp_emacs(); parse rem
+ | "-emacs" :: rem ->
+ Flags.print_emacs := true; Pp.make_pp_emacs();
+ Vernacentries.qed_display_script := false;
+ parse rem
| "-emacs-U" :: rem ->
warning "Obsolete option \"-emacs-U\", use -emacs instead.";
- Flags.print_emacs := true; Pp.make_pp_emacs(); parse rem
+ parse ("-emacs" :: rem)
| "-unicode" :: rem -> add_require "Utf8_core"; parse rem
@@ -351,7 +354,8 @@ let init arglist =
Pp.ppnl (with_option raw_print Prettyp.print_full_pure_context ());
Profile.print_profile ();
exit 0);
- Lib.declare_initial_state ()
+ (* We initialize the command history stack with a first entry *)
+ Backtrack.mark_command Vernacexpr.VernacNop
let init_toplevel = init
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index bc024e641..f8bf9fccb 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -21,12 +21,6 @@ open Namegen
the only one using this mode, but we try here to be as generic as
possible, so this may change in the future... *)
-
-(** Comment the next line for displaying some more debug messages *)
-
-let prerr_endline _ = ()
-
-
(** Signal handling: we postpone ^C during input and output phases,
but make it directly raise a Sys.Break during evaluation of the request. *)
@@ -74,282 +68,56 @@ let coqide_known_option table = List.mem table [
["Printing";"Existential";"Instances"];
["Printing";"Universes"]]
-type command_attribute =
- NavigationCommand | QueryCommand | DebugCommand | KnownOptionCommand
- | OtherStatePreservingCommand | GoalStartingCommand | SolveCommand
- | ProofEndingCommand
-
-let rec attribute_of_vernac_command = function
- (* Control *)
- | VernacTime com -> attribute_of_vernac_command com
- | VernacTimeout(_,com) -> attribute_of_vernac_command com
- | VernacFail com -> attribute_of_vernac_command com
- | VernacList _ -> [] (* unsupported *)
- | VernacLoad _ -> []
-
- (* Syntax *)
- | VernacTacticNotation _ -> []
- | VernacSyntaxExtension _ -> []
- | VernacDelimiters _ -> []
- | VernacBindScope _ -> []
- | VernacOpenCloseScope _ -> []
- | VernacArgumentsScope _ -> []
- | VernacInfix _ -> []
- | VernacNotation _ -> []
-
- (* Gallina *)
- | VernacDefinition (_,_,DefineBody _,_) -> []
- | VernacDefinition (_,_,ProveBody _,_) -> [GoalStartingCommand]
- | VernacStartTheoremProof _ -> [GoalStartingCommand]
- | VernacEndProof _ -> [ProofEndingCommand]
- | VernacExactProof _ -> [ProofEndingCommand]
-
- | VernacAssumption _ -> []
- | VernacInductive _ -> []
- | VernacFixpoint _ -> []
- | VernacCoFixpoint _ -> []
- | VernacScheme _ -> []
- | VernacCombinedScheme _ -> []
-
- (* Modules *)
- | VernacDeclareModule _ -> []
- | VernacDefineModule _ -> []
- | VernacDeclareModuleType _ -> []
- | VernacInclude _ -> []
-
- (* Gallina extensions *)
- | VernacBeginSection _ -> []
- | VernacEndSegment _ -> []
- | VernacRequire _ -> []
- | VernacImport _ -> []
- | VernacCanonical _ -> []
- | VernacCoercion _ -> []
- | VernacIdentityCoercion _ -> []
-
- (* Type classes *)
- | VernacInstance _ -> []
- | VernacContext _ -> []
- | VernacDeclareInstances _ -> []
- | VernacDeclareClass _ -> []
-
- (* Solving *)
- | VernacSolve _ -> [SolveCommand]
- | VernacSolveExistential _ -> [SolveCommand]
-
- (* Auxiliary file and library management *)
- | VernacRequireFrom _ -> []
- | VernacAddLoadPath _ -> []
- | VernacRemoveLoadPath _ -> []
- | VernacAddMLPath _ -> []
- | VernacDeclareMLModule _ -> []
- | VernacChdir o ->
- (* TODO: [Chdir d] is currently not undo-able (not stored in coq state).
- But if we register [Chdir] in the state, loading [initial.coq] will
- wrongly cd to the compile-time directory at each coqtop launch. *)
- if o = None then [QueryCommand] else []
-
- (* State management *)
- | VernacWriteState _ -> []
- | VernacRestoreState _ -> []
-
- (* Resetting *)
- | VernacResetName _ -> [NavigationCommand]
- | VernacResetInitial -> [NavigationCommand]
- | VernacBack _ -> [NavigationCommand]
- | VernacBackTo _ -> [NavigationCommand]
-
- (* Commands *)
- | VernacDeclareTacticDefinition _ -> []
- | VernacCreateHintDb _ -> []
- | VernacRemoveHints _ -> []
- | VernacHints _ -> []
- | VernacSyntacticDefinition _ -> []
- | VernacDeclareImplicits _ -> []
- | VernacArguments _ -> []
- | VernacDeclareReduction _ -> []
- | VernacReserve _ -> []
- | VernacGeneralizable _ -> []
- | VernacSetOpacity _ -> []
- | VernacSetOption (_,["Ltac";"Debug"], _) -> [DebugCommand]
- | VernacSetOption (_,o,BoolValue true) | VernacUnsetOption (_,o) ->
- if coqide_known_option o then [KnownOptionCommand] else []
- | VernacSetOption _ -> []
- | VernacRemoveOption _ -> []
- | VernacAddOption _ -> []
- | VernacMemOption _ -> [QueryCommand]
-
- | VernacPrintOption _ -> [QueryCommand]
- | VernacCheckMayEval _ -> [QueryCommand]
- | VernacGlobalCheck _ -> [QueryCommand]
- | VernacPrint _ -> [QueryCommand]
- | VernacSearch _ -> [QueryCommand]
- | VernacLocate _ -> [QueryCommand]
-
- | VernacComments _ -> [OtherStatePreservingCommand]
- | VernacNop -> [OtherStatePreservingCommand]
-
- (* Proof management *)
- | VernacGoal _ -> [GoalStartingCommand]
-
- | VernacAbort _ -> []
- | VernacAbortAll -> [NavigationCommand]
- | VernacRestart -> [NavigationCommand]
- | VernacUndo _ -> [NavigationCommand]
- | VernacUndoTo _ -> [NavigationCommand]
- | VernacBacktrack _ -> [NavigationCommand]
-
- | VernacFocus _ -> [SolveCommand]
- | VernacUnfocus -> [SolveCommand]
- | VernacShow _ -> [OtherStatePreservingCommand]
- | VernacCheckGuard -> [OtherStatePreservingCommand]
- | VernacProof (None, None) -> [OtherStatePreservingCommand]
- | VernacProof _ -> []
-
- | VernacProofMode _ -> []
- | VernacBullet _ -> [SolveCommand]
- | VernacSubproof _ -> [SolveCommand]
- | VernacEndSubproof -> [SolveCommand]
-
- (* Toplevel control *)
- | VernacToplevelControl _ -> []
-
- (* Extensions *)
- | VernacExtend ("Subtac_Obligations", _) -> [GoalStartingCommand]
- | VernacExtend _ -> []
-
-let is_vernac_navigation_command com =
- List.mem NavigationCommand (attribute_of_vernac_command com)
-
-let is_vernac_query_command com =
- List.mem QueryCommand (attribute_of_vernac_command com)
-
-let is_vernac_known_option_command com =
- List.mem KnownOptionCommand (attribute_of_vernac_command com)
-
-let is_vernac_debug_command com =
- List.mem DebugCommand (attribute_of_vernac_command com)
-
-let is_vernac_goal_printing_command com =
- let attribute = attribute_of_vernac_command com in
- List.mem GoalStartingCommand attribute or
- List.mem SolveCommand attribute
-
-let is_vernac_state_preserving_command com =
- let attribute = attribute_of_vernac_command com in
- List.mem OtherStatePreservingCommand attribute or
- List.mem QueryCommand attribute
-
-let is_vernac_tactic_command com =
- List.mem SolveCommand (attribute_of_vernac_command com)
-
-let is_vernac_proof_ending_command com =
- List.mem ProofEndingCommand (attribute_of_vernac_command com)
-
-
-(** Command history stack
-
- We maintain a stack of the past states of the system. Each
- successfully interpreted command adds a [reset_info] element
- to this stack, storing what were the (label / open proofs /
- current proof depth) just _before_ the interpretation of this
- command. A label is just an integer (cf. BackTo and Bactrack
- vernac commands).
-*)
-
-type reset_info = { label : int; proofs : identifier list; depth : int }
-
-let com_stk = Stack.create ()
-
-let compute_reset_info () =
- { label = Lib.current_command_label ();
- proofs = Pfedit.get_all_proof_names ();
- depth = max 0 (Pfedit.current_proof_depth ()) }
-
-
-(** Interpretation (cf. [Ide_intf.interp]) *)
+let is_known_option cmd = match cmd with
+ | VernacSetOption (_,o,BoolValue true)
+ | VernacUnsetOption (_,o) -> coqide_known_option o
+ | _ -> false
+
+let is_debug cmd = match cmd with
+ | VernacSetOption (_,["Ltac";"Debug"], _) -> true
+ | _ -> false
+
+let is_query cmd = match cmd with
+ | VernacChdir None
+ | VernacMemOption _
+ | VernacPrintOption _
+ | VernacCheckMayEval _
+ | VernacGlobalCheck _
+ | VernacPrint _
+ | VernacSearch _
+ | VernacLocate _ -> true
+ | _ -> false
+
+let is_undo cmd = match cmd with
+ | VernacUndo _ | VernacUndoTo _ -> true
+ | _ -> false
(** Check whether a command is forbidden by CoqIDE *)
let coqide_cmd_checks (loc,ast) =
- let user_error s =
- raise (Loc.Exc_located (loc, Errors.UserError ("CoqIde", str s)))
- in
- if is_vernac_debug_command ast then
+ let user_error s = Errors.user_err_loc (loc, "CoqIde", str s) in
+ if is_debug ast then
user_error "Debug mode not available within CoqIDE";
- if is_vernac_navigation_command ast then
- user_error "Use CoqIDE navigation instead";
- if is_vernac_known_option_command ast then
+ if is_known_option ast then
user_error "Use CoqIDE display menu instead";
- if is_vernac_query_command ast then
+ if is_navigation_vernac ast then
+ user_error "Use CoqIDE navigation instead";
+ if is_undo ast then
+ msgerrnl (str "Warning: rather use CoqIDE navigation instead");
+ if is_query ast then
msgerrnl (str "Warning: query commands should not be inserted in scripts")
-let raw_eval_expr = Vernac.eval_expr
-
-let eval_expr loc_ast =
- let rewind_info = compute_reset_info () in
- raw_eval_expr loc_ast;
- Stack.push rewind_info com_stk
+(** Interpretation (cf. [Ide_intf.interp]) *)
let interp (raw,verbosely,s) =
- if not raw then (prerr_endline "Starting interp..."; prerr_endline s);
let pa = Pcoq.Gram.parsable (Stream.of_string s) in
let loc_ast = Vernac.parse_sentence (pa,None) in
if not raw then coqide_cmd_checks loc_ast;
- (* We run tactics silently, since we will query the goal state later.
- Otherwise, we honor the IDE verbosity flag. *)
- Flags.make_silent
- (is_vernac_goal_printing_command (snd loc_ast) || not verbosely);
- if raw then raw_eval_expr loc_ast else eval_expr loc_ast;
+ Flags.make_silent (not verbosely);
+ Vernac.eval_expr ~preserving:raw loc_ast;
Flags.make_silent true;
- if not raw then prerr_endline ("...Done with interp of : "^s);
read_stdout ()
-
-(** Backtracking (cf. [Ide_intf.rewind]).
- We now rely on the [Backtrack] command just as ProofGeneral. *)
-
-let rewind count =
- if count = 0 then 0
- else
- let current_proofs = Pfedit.get_all_proof_names ()
- in
- (* 1) First, let's pop the history stack exactly [count] times.
- NB: Normally, the IDE will not rewind by more than the numbers
- of already interpreted commands, hence no risk of [Stack.Empty].
- *)
- let initial_target =
- for i = 1 to count - 1 do ignore (Stack.pop com_stk) done;
- Stack.pop com_stk
- in
- (* 2) Backtrack by enough additional steps to avoid re-opening proofs.
- Typically, when a Qed has been crossed, we backtrack to the proof start.
- NB: We cannot reach the empty stack, since the oldest [reset_info]
- in the history cannot have opened proofs.
- *)
- let already_opened p = List.mem p current_proofs in
- let rec extra_back n target =
- if List.for_all already_opened target.proofs then n,target
- else extra_back (n+1) (Stack.pop com_stk)
- in
- let extra_count, target = extra_back 0 initial_target
- in
- (* 3) Now that [target.proofs] is a subset of the opened proofs before
- the rewind, we simply abort the extra proofs (if any).
- NB: It is critical here that proofs are nested in a regular way.
- (i.e. no Resume or Suspend, as enforced above). This way, we can simply
- count the extra proofs to abort instead of taking care of their names.
- *)
- let naborts = List.length current_proofs - List.length target.proofs
- in
- (* 4) We are now ready to call [Backtrack] *)
- prerr_endline ("Rewind to state "^string_of_int target.label^
- ", proof depth "^string_of_int target.depth^
- ", num of aborts "^string_of_int naborts);
- Vernacentries.vernac_backtrack target.label target.depth naborts;
- Lib.mark_end_of_command (); (* We've short-circuited Vernac.eval_expr *)
- extra_count
-
-
(** Goal display *)
let hyp_next_tac sigma env (id,_,ast) =
@@ -514,7 +282,7 @@ let eval_call c =
in
let handler = {
Interface.interp = interruptible interp;
- Interface.rewind = interruptible rewind;
+ Interface.rewind = interruptible Backtrack.back;
Interface.goals = interruptible goals;
Interface.evars = interruptible evars;
Interface.hints = interruptible hints;
@@ -550,9 +318,9 @@ let loop () =
let () = Xml_parser.check_eof p false in
init_signal_handler ();
catch_break := false;
- (* ensure we have a command separator object (DOT) so that the first
- command can be reseted. *)
- Lib.mark_end_of_command();
+ (* We'll handle goal fetching and display in our own way *)
+ Vernacentries.enable_goal_printing := false;
+ Vernacentries.qed_display_script := false;
try
while true do
let xml_answer =
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 5187b3a28..6a06ba3dc 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -368,9 +368,6 @@ let do_vernac () =
let rec loop () =
Sys.catch_break true;
- (* ensure we have a command separator object (DOT) so that the first
- command can be reseted. *)
- Lib.mark_end_of_command();
try
reset_input_buffer stdin top_buffer;
while true do do_vernac() done
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index 2ca2f0739..599f8e9ff 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -14,6 +14,7 @@ Command
Classes
Record
Ppvernac
+Backtrack
Vernacinterp
Mltop
Vernacentries
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 60354f4cf..20b45a2b0 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -52,6 +52,8 @@ let real_error = function
| Error_in_file (_, _, e) -> e
| e -> e
+let user_error loc s = Errors.user_err_loc (loc,"_",str s)
+
(** Timeout handling *)
(** A global default timeout, controled by option "Set Default Timeout n".
@@ -167,7 +169,7 @@ let pr_new_syntax loc ocom =
States.unfreeze fs;
Format.set_formatter_out_channel stdout
-let rec vernac_com interpfun (loc,com) =
+let rec vernac_com interpfun checknav (loc,com) =
let rec interp = function
| VernacLoad (verbosely, fname) ->
let fname = expand_path_macros fname in
@@ -205,8 +207,10 @@ let rec vernac_com interpfun (loc,com) =
| VernacList l -> List.iter (fun (_,v) -> interp v) l
+ | v when !just_parsing -> ()
+
| VernacFail v ->
- if not !just_parsing then begin try
+ begin try
(* If the command actually works, ignore its effects on the state *)
States.with_state_protection
(fun v -> interp v; raise HasNotFailed) v
@@ -222,22 +226,17 @@ let rec vernac_com interpfun (loc,com) =
end
| VernacTime v ->
- if not !just_parsing then begin
let tstart = System.get_time() in
interp v;
let tend = System.get_time() in
msgnl (str"Finished transaction in " ++
System.fmt_time_difference tstart tend)
- end
| VernacTimeout(n,v) ->
- if not !just_parsing then begin
current_timeout := Some n;
interp v
- end
| v ->
- if not !just_parsing then
let psh = default_set_timeout () in
try
States.with_heavy_rollback interpfun
@@ -246,6 +245,7 @@ let rec vernac_com interpfun (loc,com) =
with e -> restore_timeout psh; raise e
in
try
+ checknav loc com;
current_timeout := !default_timeout;
if do_beautify () then pr_new_syntax loc (Some com);
interp com
@@ -259,13 +259,17 @@ and read_vernac_file verbosely s =
if verbosely then Vernacentries.interp
else Flags.silently Vernacentries.interp
in
+ let checknav loc cmd =
+ if is_navigation_vernac cmd then
+ user_error loc "Navigation commands forbidden in files"
+ in
let (in_chan, fname, input) =
open_file_twice_if verbosely s in
try
(* we go out of the following infinite loop when a End_of_input is
* raised, which means that we raised the end of the file being loaded *)
while true do
- vernac_com interpfun (parse_sentence input);
+ vernac_com interpfun checknav (parse_sentence input);
pp_flush ()
done
with e -> (* whatever the exception *)
@@ -276,15 +280,21 @@ and read_vernac_file verbosely s =
if do_beautify () then pr_new_syntax (make_loc (max_int,max_int)) None
| _ -> raise_with_file fname e
-
-(* eval_expr : Util.loc * Vernacexpr.vernac_expr -> unit
- * execute one vernacular command. Marks the end of the command in the lib_stk
- * with a new label to make vernac undoing easier. Also freeze state to speed up
- * backtracking. *)
-let eval_expr last =
- vernac_com Vernacentries.interp last;
- Lib.add_frozen_state();
- Lib.mark_end_of_command()
+(** [eval_expr : ?preserving:bool -> Pp.loc * Vernacexpr.vernac_expr -> unit]
+ It executes one vernacular command. By default the command is
+ considered as non-state-preserving, in which case we add it to the
+ Backtrack stack (triggering a save of a frozen state and the generation
+ of a new state label). An example of state-preserving command is one coming
+ from the query panel of Coqide. *)
+
+let checknav loc ast =
+ if is_deep_navigation_vernac ast then
+ user_error loc "Navigation commands forbidden in nested commands"
+
+let eval_expr ?(preserving=false) loc_ast =
+ vernac_com Vernacentries.interp checknav loc_ast;
+ if not preserving && not (is_navigation_vernac (snd loc_ast)) then
+ Backtrack.mark_command (snd loc_ast)
(* raw_do_vernac : Pcoq.Gram.parsable -> unit
* vernac_step . parse_sentence *)
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 1cfd94e05..9998fb19c 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -21,7 +21,14 @@ exception DuringCommandInterp of Pp.loc * exn
exception End_of_input
val just_parsing : bool ref
-val eval_expr : Pp.loc * Vernacexpr.vernac_expr -> unit
+
+(** [eval_expr] executes one vernacular command. By default the command is
+ considered as non-state-preserving, in which case we add it to the
+ Backtrack stack (triggering a save of a frozen state and the generation
+ of a new state label). An example of state-preserving command is one coming
+ from the query panel of Coqide. *)
+
+val eval_expr : ?preserving:bool -> Pp.loc * Vernacexpr.vernac_expr -> unit
val raw_do_vernac : Pcoq.Gram.parsable -> unit
(** Set XML hooks *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 6100fbd1d..1b89eaa68 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -74,8 +74,9 @@ let show_node () =
()
let show_script () =
- (* spiwack: show_script is currently not working *)
- ()
+ let prf = Pfedit.get_current_proof_name () in
+ let cmds = Backtrack.get_script prf in
+ msgnl (Pp.prlist_with_sep Pp.fnl Ppvernac.pr_vernac cmds)
let show_thesis () =
msgnl (anomaly "TODO" )
@@ -92,7 +93,16 @@ let show_prooftree () =
(* Spiwack: proof tree is currently not working *)
()
-let print_subgoals () = if_verbose (fun () -> msg (pr_open_subgoals ())) ()
+let enable_goal_printing = ref true
+
+let print_subgoals () =
+ if !enable_goal_printing && is_verbose ()
+ then msg (pr_open_subgoals ())
+
+let try_print_subgoals () =
+ Pp.flush_all();
+ try print_subgoals () with Proof_global.NoCurrentProof | UserError _ -> ()
+
(* Simulate the Intro(s) tactic *)
@@ -357,14 +367,21 @@ let vernac_start_proof kind l lettop hook =
(str "Let declarations can only be used in proof editing mode.");
start_proof_and_print (Global, Proof kind) l hook
+let qed_display_script = ref true
+
let vernac_end_proof = function
- | Admitted -> admit ()
+ | Admitted ->
+ Backtrack.mark_unreachable [Pfedit.get_current_proof_name ()];
+ admit ()
| Proved (is_opaque,idopt) ->
- if not !Flags.print_emacs then if_verbose show_script ();
- match idopt with
+ let prf = Pfedit.get_current_proof_name () in
+ if is_verbose () && !qed_display_script then (show_script (); msg (fnl()));
+ begin match idopt with
| None -> save_named is_opaque
| Some ((_,id),None) -> save_anonymous is_opaque id
| Some ((_,id),Some kind) -> save_anonymous_with_strength kind is_opaque id
+ end;
+ Backtrack.mark_unreachable [prf]
(* A stupid macro that should be replaced by ``Exact c. Save.'' all along
the theories [??] *)
@@ -732,19 +749,6 @@ let vernac_write_state file = abort_refine States.extern_state file
let vernac_restore_state file = abort_refine States.intern_state file
-
-(*************)
-(* Resetting *)
-
-let vernac_reset_name id = abort_refine Lib.reset_name id
-
-let vernac_reset_initial () = abort_refine Lib.reset_initial ()
-
-let vernac_back n = Lib.back n
-
-let vernac_backto n = Lib.reset_label n
-
-(* see also [vernac_backtrack] which combines undoing and resetting *)
(************)
(* Commands *)
@@ -1320,15 +1324,54 @@ let vernac_locate = function
| LocateTactic qid -> print_located_tactic qid
| LocateFile f -> locate_file f
+(****************)
+(* Backtracking *)
+
+(** NB: these commands are now forbidden in non-interactive use,
+ e.g. inside VernacLoad, VernacList, ... *)
+
+let vernac_backto lbl =
+ try
+ let lbl' = Backtrack.backto lbl in
+ if lbl <> lbl' then
+ Pp.msg_warning
+ (str "Actually back to state "++ Pp.int lbl' ++ str ".");
+ try_print_subgoals ()
+ with Backtrack.Invalid -> error "Invalid backtrack."
+
+let vernac_back n =
+ try
+ let extra = Backtrack.back n in
+ if extra <> 0 then
+ Pp.msg_warning
+ (str "Actually back by " ++ Pp.int (extra+n) ++ str " steps.");
+ try_print_subgoals ()
+ with Backtrack.Invalid -> error "Invalid backtrack."
+
+let vernac_reset_name id =
+ try Backtrack.reset_name id; try_print_subgoals ()
+ with Backtrack.Invalid -> error "Invalid Reset."
+
+let vernac_reset_initial () = Backtrack.reset_initial ()
+
+(* For compatibility with ProofGeneral: *)
+
+let vernac_backtrack snum pnum naborts =
+ Backtrack.backtrack snum pnum naborts;
+ try_print_subgoals ()
+
+
(********************)
(* Proof management *)
let vernac_abort = function
| None ->
+ Backtrack.mark_unreachable [Pfedit.get_current_proof_name ()];
delete_current_proof ();
if_verbose message "Current goal aborted";
if !pcoq <> None then (Option.get !pcoq).abort ""
| Some id ->
+ Backtrack.mark_unreachable [snd id];
delete_proof id;
let s = string_of_id (snd id) in
if_verbose message ("Goal "^s^" aborted");
@@ -1336,37 +1379,30 @@ let vernac_abort = function
let vernac_abort_all () =
if refining() then begin
+ Backtrack.mark_unreachable (Pfedit.get_all_proof_names ());
delete_all_proofs ();
message "Current goals aborted"
end else
error "No proof-editing in progress."
-let vernac_restart () = restart_proof(); print_subgoals ()
-
- (* Proof switching *)
+let vernac_restart () =
+ Backtrack.mark_unreachable [Pfedit.get_current_proof_name ()];
+ restart_proof(); print_subgoals ()
let vernac_undo n =
- undo n;
- print_subgoals ()
-
-(* backtrack with [naborts] abort, then undo_todepth to [pnum], then
- back-to state number [snum]. This allows to backtrack proofs and
- state with one command (easier for proofgeneral). *)
-let vernac_backtrack snum pnum naborts =
- for i = 1 to naborts do vernac_abort None done;
- undo_todepth pnum;
- vernac_backto snum;
- Pp.flush_all();
- (* there may be no proof in progress, even if no abort *)
- (try print_subgoals () with Proof_global.NoCurrentProof | UserError _ -> ())
+ let d = Pfedit.current_proof_depth () - n in
+ Backtrack.mark_unreachable ~after:d [Pfedit.get_current_proof_name ()];
+ Pfedit.undo n; print_subgoals ()
+let vernac_undoto n =
+ Backtrack.mark_unreachable ~after:n [Pfedit.get_current_proof_name ()];
+ Pfedit.undo_todepth n;
+ print_subgoals ()
let vernac_focus gln =
let p = Proof_global.give_me_the_proof () in
- match gln with
- | None -> Proof.focus focus_command_cond () 1 p; print_subgoals ()
- | Some n -> Proof.focus focus_command_cond () n p; print_subgoals ()
-
+ let n = match gln with None -> 1 | Some n -> n in
+ Proof.focus focus_command_cond () n p; print_subgoals ()
(* Unfocuses one step in the focus stack. *)
let vernac_unfocus () =
@@ -1548,7 +1584,7 @@ let interp c = match c with
| VernacAbortAll -> vernac_abort_all ()
| VernacRestart -> vernac_restart ()
| VernacUndo n -> vernac_undo n
- | VernacUndoTo n -> undo_todepth n
+ | VernacUndoTo n -> vernac_undoto n
| VernacBacktrack (snum,pnum,naborts) -> vernac_backtrack snum pnum naborts
| VernacFocus n -> vernac_focus n
| VernacUnfocus -> vernac_unfocus ()
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 2b6a881d4..66aa6c20a 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -51,14 +51,23 @@ val abort_refine : ('a -> unit) -> 'a -> unit;;
val interp : Vernacexpr.vernac_expr -> unit
-val vernac_reset_name : identifier Pp.located -> unit
+(** Print subgoals when the verbose flag is on.
+ Meant to be used inside vernac commands from plugins. *)
-val vernac_backtrack : int -> int -> int -> unit
-
-(* Print subgoals when the verbose flag is on. Meant to be used inside
- vernac commands from plugins. *)
val print_subgoals : unit -> unit
+(** The printing of goals via [print_subgoals] or during
+ [interp] can be controlled by the following flag.
+ Used for instance by coqide, since it has its own
+ goal-fetching mechanism. *)
+
+val enable_goal_printing : bool ref
+
+(** Should Qed try to display the proof script ?
+ True by default, but false in ProofGeneral and coqIDE *)
+
+val qed_display_script : bool ref
+
(** Prepare a "match" template for a given inductive type.
For each branch of the match, we list the constructor name
followed by enough pattern variables.
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index c017393c1..259329a10 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -367,6 +367,26 @@ type vernac_expr =
and located_vernac_expr = loc * vernac_expr
+
+(** Categories of [vernac_expr] *)
+
+let rec strip_vernac = function
+ | VernacTime c | VernacTimeout(_,c) | VernacFail c -> strip_vernac c
+ | c -> c (* TODO: what about VernacList ? *)
+
+let rec is_navigation_vernac = function
+ | VernacResetInitial
+ | VernacResetName _
+ | VernacBacktrack _
+ | VernacBackTo _
+ | VernacBack _ -> true
+ | c -> is_deep_navigation_vernac c
+
+and is_deep_navigation_vernac = function
+ | VernacTime c | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c
+ | VernacList l -> List.exists (fun (_,c) -> is_navigation_vernac c) l
+ | _ -> false
+
(* Locating errors raised just after the dot is parsed but before the
interpretation phase *)