aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <Pierre.Courtieu@cnam.fr>2015-01-08 16:59:47 +0100
committerGravatar Pierre Courtieu <Pierre.Courtieu@cnam.fr>2015-01-08 16:59:57 +0100
commitb92fff621cce1576c93fab9276fb41ea85e10982 (patch)
treed6e0c1964b274c9b00339452d77468f48ebe2794
parent448bf4529c5766e98367345076d00e64e25db7bf (diff)
Fixed and extend bullet related info/error messages. + doc.
Had to put some hook in the handler of Proofview.NoSuchgoals. Documentation updated. CHANGE updated.
-rw-r--r--CHANGES1
-rw-r--r--doc/refman/RefMan-pro.tex63
-rw-r--r--printing/printer.ml7
-rw-r--r--proofs/proof_global.ml226
-rw-r--r--proofs/proof_global.mli9
-rw-r--r--proofs/proofview.ml16
-rw-r--r--proofs/proofview.mli8
7 files changed, 184 insertions, 146 deletions
diff --git a/CHANGES b/CHANGES
index f5991416b..431817394 100644
--- a/CHANGES
+++ b/CHANGES
@@ -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