diff options
-rw-r--r-- | ide/coq_lex.mll | 2 | ||||
-rw-r--r-- | library/lib.ml | 83 | ||||
-rw-r--r-- | library/lib.mli | 42 | ||||
-rw-r--r-- | plugins/funind/invfun.ml | 2 | ||||
-rw-r--r-- | plugins/funind/recdef.ml | 7 | ||||
-rw-r--r-- | plugins/subtac/subtac.ml | 227 | ||||
-rw-r--r-- | proofs/pfedit.mli | 4 | ||||
-rw-r--r-- | toplevel/backtrack.ml | 225 | ||||
-rw-r--r-- | toplevel/backtrack.mli | 93 | ||||
-rw-r--r-- | toplevel/coqtop.ml | 10 | ||||
-rw-r--r-- | toplevel/ide_slave.ml | 308 | ||||
-rw-r--r-- | toplevel/toplevel.ml | 3 | ||||
-rw-r--r-- | toplevel/toplevel.mllib | 1 | ||||
-rw-r--r-- | toplevel/vernac.ml | 44 | ||||
-rw-r--r-- | toplevel/vernac.mli | 9 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 116 | ||||
-rw-r--r-- | toplevel/vernacentries.mli | 19 | ||||
-rw-r--r-- | toplevel/vernacexpr.ml | 20 |
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 *) |