diff options
| -rw-r--r-- | CHANGES | 1 | ||||
| -rw-r--r-- | doc/refman/RefMan-pro.tex | 63 | ||||
| -rw-r--r-- | printing/printer.ml | 7 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 226 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 9 | ||||
| -rw-r--r-- | proofs/proofview.ml | 16 | ||||
| -rw-r--r-- | proofs/proofview.mli | 8 |
7 files changed, 184 insertions, 146 deletions
@@ -224,6 +224,7 @@ Tactics so that terms with holes can be constructed piecewise in Ltac. - New bullets --, ++, **, ---, +++, ***, ... made available. - More informative messages when wrong bullet is used. +- bullet suggestion when a subgoal is solved. - New tactic "enough", symmetric to "assert", but with subgoals swapped, as a more friendly replacement of "cut". - In destruct/induction, experimental modifier "!" prefixing the diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 25dc32e3d..eabb37639 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -307,14 +307,19 @@ only be unfocused when it has been fully solved (\emph{i.e.} when there is no focused goal left). Unfocusing is then handled by {\tt \}} (again, without a terminating period). See also example in next section. +Note that when a focused goal is proved a message is displayed +together with a suggestion about the right bullet or {\tt \}} to +unfocus it or focus the next one. + \begin{ErrMsgs} \item \errindex{Error: This proof is focused, but cannot be unfocused - this way} - You are trying to use a bullet that is already in use or a {\tt \}} but the current - subproof has not been fully solved. + this way} You are trying to use {\tt \}} but the current subproof + has not been fully solved. +\item see also error message about bullets below. \end{ErrMsgs} -\subsection[Bullets]{Bullets\comindex{+ (command)}\comindex{- (command)}\comindex{* (command)}\index{Bullets}} +\subsection[Bullets]{Bullets\comindex{+ (command)} + \comindex{- (command)}\comindex{* (command)}\index{Bullets}} Alternatively to {\tt \{} and {\tt \}}, proofs can be structured with bullets. The use of a bullet $b$ for the first time focuses on the first goal $g$, the same bullet cannot be used again until the proof @@ -329,6 +334,15 @@ Available bullets are {\tt -}, {\tt +}, {\tt *}, {\tt --}, {\tt ++}, {\tt **}, {\tt ---}, {\tt +++}, {\tt ***}, ... (without a terminating period). +Note again that when a focused goal is proved a message is displayed +together with a suggestion about the right bullet or {\tt \}} to +unfocus it or focus the next one. + +Remark: In {\ProofGeneral} (Emacs interface to {\Coq}), you must use +bullets with the priority ordering shown above to have a correct +indentation. For example {\tt -} must be the outer bullet and {\tt **} +the inner one in the example below. + The following example script illustrates all these features: \begin{coq_example*} Goal (((True/\True)/\True)/\True)/\True. @@ -336,46 +350,39 @@ Proof. split. - split. + split. - * { split. + ** { split. - trivial. - trivial. } - * trivial. + ** trivial. + trivial. - assert True. { trivial. } assumption. \end{coq_example*} -Remark: In {\ProofGeneral} (Emacs interface to {\Coq}), you must use bullets -with this priority ordering to have a correct indentation: {\tt -}, -{\tt +}, {\tt *}. That is {\tt -} must be the outer bullet and {\tt *} -the inner one, like in the example above. \begin{ErrMsgs} -\item \errindex{Error: Wrong bullet: The current bullet {\abullet} - seems not finished.} You are trying to use a bullet already in use - but the current bullet {\abullet} is not finished. +\item \errindex{Error: Wrong bullet {\abullet}1 : Current bullet + {\abullet}2 is not finished.} + + Before using bullet {\abullet}1 again, you should first finish + proving the current focused goal. Note that {\abullet}1 and + {\abullet}2 may be the same. -\item \errindex{Error: Wrong bullet: Finish bullet {\abullet}1 before - going back to {\abullet}2.} You need a bullet here but {\abullet}2, - despite already in use, is the wrong one. Use bullet {\abullet}1 - instead. +\item \errindex{Error: Wrong bullet {\abullet}1 : Bullet {\abullet}2 + is mandatory here.} You must put {\abullet}2 to focus next goal. + No other bullet is allowed here. -\item \errindex{Error: No focussed goal. To focus next goal, use - bullet {\abullet}.} You need a bullet here but you are trying to - introduce a fresh one. Use {\abullet} instead. -\item \errindex{Error: Wrong bullet: no more goals at this level. Try - {\abullet} instead.} You need a bullet here but the one you just - tried is exhausted. Use {\abullet} instead. +\item \errindex{Error: No such goal. Focus next goal with bullet + {\abullet}.} -\item \errindex{Error: No such goal} there is no proof under focus - (because it has just been solved), so the command you are trying - to use cannot be applied. You need to first focus the next proof - by using the bullet corresponding to the right level (using an - incorrect bullet can also generates this message in some cases). + You tried to applied a tactic but no goal where under focus. Using + {\abullet} is mandatory here. +\item \errindex{Error: No such goal. Try unfocusing with "{\tt \}}".} You + just finished a goal focused by {\tt \{}, you must unfocus it with "{\tt \}}". \end{ErrMsgs} diff --git a/printing/printer.ml b/printing/printer.ml index 38b5e0bfd..47cf2ac1f 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -626,9 +626,10 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] shelf | _ , _, _ -> - msg_info (str "This subproof is complete, but there are still unfocused goals."); - fnl () - ++ pr_subgoals ~pr_first:false None bsigma seeds shelf [] bgoals + msg_info (str "This subproof is complete, but there are still unfocused goals." ++ + (match Proof_global.Bullet.suggest p + with None -> str"" | Some s -> fnl () ++ str s)); + fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds shelf [] bgoals end | _ -> pr_subgoals None sigma seeds shelf stack goals end diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index d26a8c487..0c617fb25 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -392,23 +392,6 @@ module Bullet = struct type t = Vernacexpr.bullet - (* There are two reasons why a bullet may be wrong: *) - - (* 1) because the previous same bullet is not finished. - - t contains the unfinished bullet and optionally the deeper - unfinished one (better suggestion to the user). *) - exception FailedUnfocusBullet of t * t option - - (* 2) there is no more goal at this level of bullet. - - t is the wrong bullet, looking which one is correct is not - implemented yet. *) - exception FailedFocusUsedBullet of t - - exception ExhaustedBulletStack - exception FailedFocusUnusedBullet of t - let bullet_eq b1 b2 = match b1, b2 with | Vernacexpr.Dash n1, Vernacexpr.Dash n2 -> n1 = n2 | Vernacexpr.Star n1, Vernacexpr.Star n2 -> n1 = n2 @@ -421,37 +404,11 @@ module Bullet = struct | Vernacexpr.Star n -> str (String.make n '*') | Vernacexpr.Plus n -> str (String.make n '+') - let _ = - Errors.register_handler - (function - | FailedUnfocusBullet (b,optb') -> - (match optb' with - | Some b' -> - if b = b' then - Errors.errorlabstrm - "Focus" Pp.(str"Wrong bullet: The current bullet " - ++ pr_bullet b' ++ str" seems not finished.") - else Errors.errorlabstrm - "Focus" Pp.(str"Wrong bullet: Finish bullet " - ++ pr_bullet b' - ++ str" before going back to " ++ pr_bullet b - ++ str".") - | None -> assert false) - - | FailedFocusUsedBullet b -> - Errors.errorlabstrm - "Focus" Pp.(str"Wrong bullet: no more goals at this level. Try " - ++ pr_bullet b ++ str" instead.") - | FailedFocusUnusedBullet b -> - Errors.errorlabstrm - "Focus" Pp.(str"No focussed goal. To focus next goal, use bullet " - ++ pr_bullet b ++ str".") - | _ -> raise Errors.Unhandled) - type behavior = { name : string; - put : Proof.proof -> t -> Proof.proof + put : Proof.proof -> t -> Proof.proof; + suggest: Proof.proof -> string option } let behaviors = Hashtbl.create 4 @@ -460,11 +417,55 @@ module Bullet = struct (*** initial modes ***) let none = { name = "None"; - put = fun x _ -> x + put = (fun x _ -> x); + suggest = (fun _ -> None) } let _ = register_behavior none module Strict = struct + type suggestion = + | Suggest of t (* this bullet is mandatory here *) + | Unfinished of t (* no mandatory bullet here, but this bullet is unfinished *) + | NoBulletInUse (* No mandatory bullet (or brace) here, no bullet pending, + some focused goals exists. *) + | NeedClosingBrace (* Some unfocussed goal exists "{" needed to focus them *) + | ProofFinished (* No more goal anywhere *) + + (* give a message only if more informative than the standard coq message *) + let suggest_on_solved_goal sugg = + match sugg with + | NeedClosingBrace -> Some "Try unfocusing with \"}\"." + | NoBulletInUse -> None + | ProofFinished -> None + | Suggest b -> Some ("Focus next goal with bullet " + ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) + ^".") + | Unfinished b -> Some ("The current bullet " + ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) + ^ " is unfinished.") + + (* give always a message. *) + let suggest_on_error sugg = + match sugg with + | NeedClosingBrace -> "Try unfocusing with \"}\"." + | NoBulletInUse -> assert false (* This should never raise an error. *) + | ProofFinished -> "No more subgoals." + | Suggest b -> ("Bullet " ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) + ^ " is mandatory here.") + | Unfinished b -> ("Current bullet " ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) + ^ " is not finished.") + + exception FailedBullet of t * suggestion + + let _ = + Errors.register_handler + (function + | FailedBullet (b,sugg) -> + let prefix = "Wrong bullet " ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) ^ " : " in + Errors.errorlabstrm "Focus" (str prefix ++ str (suggest_on_error sugg)) + | _ -> raise Errors.Unhandled) + + (* spiwack: we need only one focus kind as we keep a stack of (distinct!) bullets *) let bullet_kind = (Proof.new_focus_kind () : t list Proof.focus_kind) let bullet_cond = Proof.done_cond ~loose_end:true bullet_kind @@ -486,80 +487,75 @@ module Bullet = struct in has_bullet (get_bullets pr) - (* pop a bullet from proof [pr]. If no more bullet in [pr] then - raise [Proof.CannotUnfocusThisWay]. Otherwise if pop impossible - (pending proofs on this level of bullet or higher) then raise - [FailedUnfocusBullet (b)] where [b] is the bullet that could - not be popped. Beware that [b] is not the good suggestion at - this point. *) + (* pop a bullet from proof [pr]. There should be at least one + bullet in use. If pop impossible (pending proofs on this level + of bullet or higher) then raise [Proof.CannotUnfocusThisWay]. *) let pop pr = match get_bullets pr with - | b::_ -> - (try Proof.unfocus bullet_kind pr () , b - with Proof.CannotUnfocusThisWay -> raise (FailedUnfocusBullet (b,None))) - | _ -> raise ExhaustedBulletStack + | b::_ -> Proof.unfocus bullet_kind pr () , b + | _ -> assert false let push (b:t) pr = Proof.focus bullet_cond (b::get_bullets pr) 1 pr - (* This function pops bullets one by one until [bul] or end - of stack. If [bul] is found and all pops were ok (no pending - subgoals in popped bullets) then return the new proof. - Otherwise raise an exception with a bullet suggestion *) - let rec pop_or_explain (untilbul:t option) (p:Proof.proof) (suggestbul:t option) = - try - let p, b = pop p in - (* pop went well, see if b is a good suggestion. *) - let newsuggestbul = - (* if push does not fail then b is a good suggestion. *) - try let _ = push b p in Some b (* push didn't fail so b is OK *) - with _ -> suggestbul in - (* Check if we found untilbul (if applicable) and recursive - call if not. *) - (match untilbul with - | None -> pop_or_explain untilbul p newsuggestbul - | Some bul' -> if bullet_eq bul' b - then p - else pop_or_explain untilbul p newsuggestbul) - with FailedUnfocusBullet (b,None) -> - (* the current bullet is [b] and it cannot be popped. If we - don't have a suggestion at this point, it means that the - current bullet is not finished, otherwise suggest. *) - (match suggestbul with - None -> raise (FailedUnfocusBullet (b,Some b)) - | Some b' -> raise (FailedUnfocusBullet (b, Some b'))) - - | ExhaustedBulletStack -> - (* bullet stack is exhausted, suggest [suggestbul]. *) - (match suggestbul with - None -> raise Proof.CannotUnfocusThisWay - | Some b' -> raise (FailedFocusUnusedBullet b')) - + (* Used only in the next function. + TODO: use a recursive function instead? *) + exception SuggestFound of t + + let suggest_bullet (prf:Proof.proof): suggestion = + if Proof.is_done prf then ProofFinished + else if not (Proof.no_focused_goal prf) + then (* No suggestion if a bullet is not mandatory, look for an unfinished bullet *) + match get_bullets prf with + | b::_ -> Unfinished b + | _ -> NoBulletInUse + else (* There is no goal under focus but some are unfocussed, + let us look at the bullet needed. If no *) + let pcobaye = ref prf in + try + while true do + let pcobaye', b = pop !pcobaye in + (* pop went well, this means that there are no more goals + *under this* bullet b, see if a new b can be pushed. *) + (try let _ = push b pcobaye' in (* push didn't fail so a new b can be pushed. *) + raise (SuggestFound b) + with SuggestFound _ as e -> raise e + | _ -> ()); (* b could not be pushed, so we must look for a outer bullet *) + pcobaye := pcobaye' + done; + assert false + with SuggestFound b -> Suggest b + | _ -> NeedClosingBrace (* No push was possible, but there are still + subgoals somewhere: there must be a "}" to use. *) + + + let rec pop_until (prf:Proof.proof) bul: Proof.proof = + let prf', b = pop prf in + if bullet_eq bul b then prf' + else pop_until prf' bul let put p bul = - if has_bullet bul p then - let p' = pop_or_explain (Some bul) p None in - try push bul p' - with Proof.NoSuchGoals(1,1) -> - (* raise (FailedFocusUsedBullet bul) *) - try let _ = pop_or_explain None p None in - raise Proof.CannotUnfocusThisWay - with FailedUnfocusBullet (b,Some bsugg) -> raise (FailedFocusUsedBullet bsugg) - else - try push bul p - with - | Proof.NoSuchGoals(1,1) -> - (* pop_until should raise an exception with a bullet suggestion, - but FailedUnfocusBullet should be transformed into - FailedFocusUnusedBullet. *) - (try let _ = pop_or_explain None p None in - raise (Proof.NoSuchGoals(1,1)) - with FailedUnfocusBullet (b,Some bsugg) -> - raise (FailedFocusUnusedBullet bsugg)) - + try + if not (has_bullet bul p) then + (* bullet is not in use, so pushing it is always ok unless + no goal under focus. *) + push bul p + else + match suggest_bullet p with + | Suggest suggested_bullet when bullet_eq bul suggested_bullet + -> (* suggested_bullet is mandatory and you gave the right one *) + let p' = pop_until p bul in + push bul p' + (* the bullet you gave is in use but not the right one *) + | sugg -> raise (FailedBullet (bul,sugg)) + with Proof.NoSuchGoals _ -> (* push went bad *) + raise (FailedBullet (bul,suggest_bullet p)) + let strict = { name = "Strict Subproofs"; - put = put + put = put; + suggest = (fun prf -> suggest_on_solved_goal (suggest_bullet prf)) + } let _ = register_behavior strict end @@ -583,9 +579,19 @@ module Bullet = struct let put p b = (!current_behavior).put p b + + let suggest p = + (!current_behavior).suggest p end +let _ = + let hook n = + let prf = give_me_the_proof () in + (Bullet.suggest prf) in + Proofview.set_nosuchgoals_hook hook + + (**********************************************************) (* *) (* Default goal selector *) diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index c9a812c4c..f9f67235b 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -151,11 +151,13 @@ module Bullet : sig type t = Vernacexpr.bullet (** A [behavior] is the data of a put function which - is called when a bullet prefixes a tactic, together - with a name to identify it. *) + is called when a bullet prefixes a tactic, a suggest function + suggesting the right bullet to use on a given proof, together + with a name to identify the behavior. *) type behavior = { name : string; - put : Proof.proof -> t -> Proof.proof + put : Proof.proof -> t -> Proof.proof; + suggest: Proof.proof -> string option } (** A registered behavior can then be accessed in Coq @@ -172,6 +174,7 @@ module Bullet : sig (** Handles focusing/defocusing with bullets: *) val put : Proof.proof -> t -> Proof.proof + val suggest : Proof.proof -> string option end diff --git a/proofs/proofview.ml b/proofs/proofview.ml index f1d10bbe5..44bf65212 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -343,8 +343,22 @@ let tclBREAK = Proof.break (** {7 Focusing tactics} *) exception NoSuchGoals of int + +(* This hook returns a string to be appended to the usual message. + Primarily used to add a suggestion about the right bullet to use to + focus the next goal, if applicable. *) +let nosuchgoals_hook:(int -> string option) ref = ref ((fun n -> None)) +let set_nosuchgoals_hook f = nosuchgoals_hook := f + + + +(* This uses the hook above *) let _ = Errors.register_handler begin function - | NoSuchGoals n -> Errors.error ("No such " ^ String.plural n "goal" ^".") + | NoSuchGoals n -> + let suffix:string option = (!nosuchgoals_hook) n in + Errors.errorlabstrm "" + (str "No such " ++ str (String.plural n "goal") ++ str "." + ++ pr_opt str suffix) | _ -> raise Errors.Unhandled end diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 25f4547a9..adcdeb819 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -229,8 +229,14 @@ val tclBREAK : (iexn -> iexn option) -> 'a tactic -> 'a tactic (** [tclFOCUS i j t] applies [t] after focusing on the goals number [i] to [j] (see {!focus}). The rest of the goals is restored after the tactic action. If the specified range doesn't correspond to - existing goals, fails with [NoSuchGoals] (a user error). *) + existing goals, fails with [NoSuchGoals] (a user error). this + exception is catched at toplevel with a default message + a hook + message that can be customized by [set_nosuchgoals_hook] below. + This hook is used to add a suggestion about bullets when + applicable. *) exception NoSuchGoals of int +val set_nosuchgoals_hook: (int -> string option) -> unit + val tclFOCUS : int -> int -> 'a tactic -> 'a tactic (** [tclFOCUSID x t] applies [t] on a (single) focused goal like |