diff options
Diffstat (limited to 'toplevel')
| -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 |
11 files changed, 509 insertions, 339 deletions
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 *) |