diff options
| -rw-r--r-- | coq/coq.el | 7 | ||||
| -rw-r--r-- | doc/PG-adapting.texi | 43 | ||||
| -rw-r--r-- | generic/proof-tree.el | 37 |
3 files changed, 78 insertions, 9 deletions
@@ -202,6 +202,12 @@ See also `coq-hide-additional-subgoals'." :type 'regexp :group 'coq-proof-tree) +(defcustom coq-proof-tree-new-layer-command-regexp + "^\\(\\(Proof\\)\\|\\(Grab Existential Variables\\)\\)" + "Regexp for `proof-tree-new-layer-command-regexp'." + :type 'regexp + :group 'coq-proof-tree) + (defcustom coq-proof-tree-current-goal-regexp (concat "^[0-9]+ \\(?:focused \\)?subgoal\\(?:s\\)?" "\\(?: (unfocused: [-0-9]+)\\)?\\(?:\\s-*, subgoal 1\\)? " @@ -1191,6 +1197,7 @@ flag Printing All set." proof-tree-ignored-commands-regexp coq-proof-tree-ignored-commands-regexp proof-tree-navigation-command-regexp coq-navigation-command-regexp proof-tree-cheating-regexp coq-proof-tree-cheating-regexp + proof-tree-new-layer-command-regexp coq-proof-tree-new-layer-command-regexp proof-tree-current-goal-regexp coq-proof-tree-current-goal-regexp proof-tree-update-goal-regexp coq-proof-tree-update-goal-regexp proof-tree-existential-regexp coq-proof-tree-existential-regexp diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index 1684e882..a23a91e7 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -2515,12 +2515,45 @@ in @code{generic/proof-tree.el} as well as in the Prooftree program. @menu +* A layered set of proof trees:: * Prerequisites:: * Proof-Tree Display Internals:: * Configuring Prooftree for a New Proof Assistant:: @end menu +@node A layered set of proof trees +@section A layered set of proof trees + +Prooftree can actually display more than one proof tree per +proof. This is necessary to support the +@code{Grab Existential Variables} command in Coq. When the main +goal has been proved, this command turns all open existential +variables into new proof obligations. All these new proof +obligations become root nodes for their own proof trees. When +they all have been proved one can again grab the open existential +variables... + +For each proof, Prooftree can therefore display several layers, +where each layer can contain several (graphically) independent +proof trees. The first layer contains one tree for the original +proof goal. The second layer contains proof trees for goals that +have been added to the proof after the first proof tree was +completed. And so on. + +To organize the layers, Prooftree must identify those proof +commands that add new goals to a proof. + +@c TEXI DOCSTRING MAGIC: proof-tree-new-layer-command-regexp +@defvar proof-tree-new-layer-command-regexp +Regexp to match proof commands that add new goals to a proof.@* +This regexp must match the command that turns the proof assistant +into prover mode, which adds the initial goal to the proof. It +must further match commands that add additional goals after all +previous goals have been proved. +@end defvar + + @node Prerequisites @section Prerequisites @@ -2823,13 +2856,19 @@ assistant is already busy with the next item from @code{proof-action-list}. @c TEXI DOCSTRING MAGIC: proof-tree-handle-delayed-output -@defun proof-tree-handle-delayed-output cmd flags span +@defun proof-tree-handle-delayed-output old-proof-marker cmd flags span Process delayed output for prooftree.@* This function is the main entry point of the Proof General prooftree support. It examines the delayed output in order to take appropriate actions and maintains the internal state. -All arguments are (former) fields of the @samp{@code{proof-action-list}} +The delayed output to handle is in the region +[@code{proof-shell-delayed-output-start}, @code{proof-shell-delayed-output-end}]. +Urgent messages might be before that, following @var{old-proof-marker}, +which contains the position of @samp{@code{proof-marker}}, before the next +command was sent to the proof assistant. + +All other arguments are (former) fields of the @samp{@code{proof-action-list}} entry that is now finally retired. @var{cmd} is the command, @var{flags} are the flags and @var{span} is the span. @end defun diff --git a/generic/proof-tree.el b/generic/proof-tree.el index 969dce05..bca6baf8 100644 --- a/generic/proof-tree.el +++ b/generic/proof-tree.el @@ -32,7 +32,7 @@ ;; the middle of a proof. Therefore, if the user wants to start the ;; proof-tree display in the middle of the proof, it is necessary to ;; retract to the start of the proof and then to reassert to the -;; previous end of the locked region. To achieve this one has to call +;; previous end of the locked region. To achieve this, one has to call ;; `accept-process-output' at suitable points to let Proof General ;; process the `proof-action-list'. ;; @@ -73,7 +73,16 @@ ;; the next real proof command runs. For Coq this needs to be done for ;; newly generated subgoals and for goals that contain an existential ;; variable that got instantiated in the last proof step. - +;; +;; Actually, for every proof, Prooftree can display a set of disjunct +;; proof trees, which are organized into layers. More than one proof +;; tree in more than one layer is needed to support the Grap +;; Existential Variables command in Coq. There is one proof tree in +;; the first layer for the original goal. The second layer contains +;; all the goals that the first Grab Existential Variables command +;; created from uninstantiated existential variabes in the main proof. +;; The third layer contains the goals that the second Grap Existential +;; Variables created. ;;; Code: @@ -144,6 +153,15 @@ Coq. Leave at nil if there are no cheating commands." :type '(choice regexp (const nil)) :group 'proof-tree-internals) +(defcustom proof-tree-new-layer-command-regexp nil + "Regexp to match proof commands that add new goals to a proof. +This regexp must match the command that turns the proof assistant +into prover mode, which adds the initial goal to the proof. It +must further match commands that add additional goals after all +previous goals have been proved." + :type 'regexp + :group 'proof-tree-internals) + (defcustom proof-tree-current-goal-regexp nil "Regexp to match the current goal and its ID. The regexp is matched against the output of the proof assistant @@ -505,21 +523,23 @@ DATA as data sections to Prooftree." ())) (defun proof-tree-send-goal-state (state proof-name command-string cheated-flag - current-sequent-id current-sequent-text - additional-sequent-ids existential-info) + layer-flag current-sequent-id + current-sequent-text additional-sequent-ids + existential-info) "Send the current goal state to prooftree." ;; (message "PTSGS id %s sequent %s ex-info %s" ;; current-sequent-id current-sequent-text existential-info) (let* ((add-id-string (mapconcat 'identity additional-sequent-ids " ")) (second-line (format - (concat "current-goals state %d current-sequent %s %s " + (concat "current-goals state %d current-sequent %s %s %s " "proof-name-bytes %d " "command-bytes %d sequent-text-bytes %d " "additional-id-bytes %d existential-bytes %d") state current-sequent-id (if cheated-flag "cheated" "not-cheated") + (if layer-flag "new-layer" "current-layer") (1+ (string-bytes proof-name)) (1+ (string-bytes command-string)) (1+ (string-bytes current-sequent-text)) @@ -876,11 +896,14 @@ command was sent to the proof assistant." (let ((current-sequent-id (car current-goals)) (current-sequent-text (nth 1 current-goals)) ;; nth 2 current-goals contains the additional ID's - ) + (layer-flag + (and proof-tree-new-layer-command-regexp + (proof-string-match proof-tree-new-layer-command-regexp + cmd-string)))) ;; send all to prooftree (proof-tree-send-goal-state proof-state proof-name cmd-string - cheated-flag + cheated-flag layer-flag current-sequent-id current-sequent-text (nth 2 current-goals) |