From ad39c0cc412c56247f7a4abe371b426297b7e4b4 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Mon, 25 Mar 2024 13:57:45 +0100 Subject: [PATCH] omit-proofs: split command processing into two phases The first phase only classifies proofs to be omitted and stuff not to be omitted. The second phase does the actual replacement and adjusts the overlays/spans. Feature wise this commit does not change anything but it enables reusing the first phase for new features. Additionally, slightly extend the omit proofs test. --- ci/simple-tests/coq-test-omit-proofs.el | 22 +- generic/proof-script.el | 260 +++++++++++++++++------- 2 files changed, 207 insertions(+), 75 deletions(-) diff --git a/ci/simple-tests/coq-test-omit-proofs.el b/ci/simple-tests/coq-test-omit-proofs.el index d676ab34b..1779f372a 100644 --- a/ci/simple-tests/coq-test-omit-proofs.el +++ b/ci/simple-tests/coq-test-omit-proofs.el @@ -92,10 +92,11 @@ configured there may be taken from faces with less priority." "Test the omit proofs feature. In particular, test that with proof-omit-proofs-option configured: - the proof _is_ processed when using a prefix argument -- in this case the proof as normal locked color +- in this case the proof has normal locked color - without prefix arg, the proof is omitted - the proof has omitted color then -- stuff before the proof still has normal color " +- stuff before the proof still has normal color +- trailing incomplete proofs are not omitted" (setq proof-omit-proofs-option t proof-three-window-enable nil) (reset-coq) @@ -175,6 +176,23 @@ In particular, test that with proof-omit-proofs-option configured: (should (search-backward "automatic test marker 1" nil t)) (should (eq (first-overlay-face) 'proof-locked-face)) (should (search-forward "automatic test marker 2" nil t)) + (should (eq (first-overlay-face) 'proof-locked-face)) + + ;; Check 6: check that a partial proof at the end is not omitted + (message "6: check that a partial proof at the end is not omitted") + (goto-char (point-min)) + (proof-goto-point) + (wait-for-coq) + (should (search-forward "automatic test marker 3" nil t)) + (forward-line 2) + (proof-goto-point) + (wait-for-coq) + ;; there are 2 goals + (with-current-buffer "*goals*" + (goto-char (point-min)) + (should (looking-at "2 \\(?:sub\\)?goals"))) + ;; the line before should be locked + (forward-line -1) (should (eq (first-overlay-face) 'proof-locked-face))) (ert-deftest omit-proofs-never-omit-hints () diff --git a/generic/proof-script.el b/generic/proof-script.el index 854bd6bf8..264270efe 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1985,6 +1985,15 @@ Assumes that point is at the end of a command." ;; buffer content has been converted to vanilla spans, ;; `proof-script-omit-proofs' searches for complete opaque proofs in ;; there and replaces them with `proof-script-proof-admit-command'. +;; +;; The replacement works in two phases. First, +;; `proof-script-omit-filter' transfers the list of vanilla spans into +;; a list of lists of these spans, where each sublist is tagged with +;; either `'proof' or `'no-proof'. Second, `proof-script-omit-proofs' +;; replaces the proof parts with admit commands. Partitioning into two +;; phases makes it possible to reuse the first phase for different +;; features. See the documentation of `proof-script-omit-filter' for a +;; specification of the list of lists result type. (defun proof-move-over-whitespace-to-next-line (pos) "Return position of next line if one needs only to jump over white space. @@ -1999,33 +2008,78 @@ line, otherwise POS." (if (eolp) (1+ (point)) pos))) - -(defun proof-script-omit-proofs (vanillas) - "Return a copy of VANILLAS with complete opaque proofs omitted. + +(defun proof-script-omit-filter (vanillas) + "Classify VANILLAS into those which are inside and those outside of proofs. +Classify the list of vanilla spans VANILLAS into those belonging +to a proof script that can be omitted by the omit proofs feature +and those which can not be omitted (either outside proofs or +inside proofs that cannot be omitted). + See `proof-omit-proofs-configured' for the description of the omit proofs feature. This function uses `proof-script-proof-start-regexp', `proof-script-proof-end-regexp' and `proof-script-definition-end-regexp' to search for complete -opaque proofs in the action list VANILLAS. Complete opaque proofs -are replaced by `proof-script-proof-admit-command'. The span of -the admit command contains an 'omitted-proof-region property with -the region of the omitted proof. This is used in -`proof-done-advancing-save' to colour the omitted proof with -`proof-omitted-proof-face'. - -Report an error to the (probably surprised) user if another proof -start is found inside a proof." +opaque proofs in the action list VANILLAS. Additionally, it uses +`proof-script-cmd-prevents-proof-omission' and +`proof-script-cmd-force-next-proof-kept' to detect proofs that +cannot be omitted. + +The result is a list of chunks, where each chunk is a list that +contains a type tag as first element. The chunk list is returned +in reversed order, i.e., the first vanilla span in VANILLAS is +inside the last chunk. + +There are three types of chunks: 'proof for commands inside a +proof that can be omitted, 'no-proof for commands that are +outside a proof or cannot be omitted, and 'nested for commands +that contain a nested proof. Note that there may be several +adjacent 'no-proof chunks, for instance for commands outside a +proof followed by a proof that cannot be omitted. + +The 'proof chunk has 4 elements: + +('proof span-start-first-proof-cmd span-end-first-proof-cmd proof-cmds-reversed) + +The last, proof-cmds-reversed, contains the vanilla spans from +VANILLAS corresponding to commands belonging to a proof, +excluding the first that matched +`proof-script-proof-start-regexp' and including the last that +matched `proof-script-proof-end-regexp' in reversed order. The +second element span-start-first-proof-cmd is the position of the +start of the command that matched +`proof-script-proof-start-regexp' and span-end-first-proof-cmd is +the position of the end of that command. + +The 'no-proof chunk has 2 elements. + +('no-proof cmds-reversed) + +cmds-reversed contains the vanilla spans of VANILLAS in reversed +order. + +The 'nested-proof chunk has 3 elements. + +('nested-proof line-number-nested-proof cmds-reversed) + +line-number-nested-proof is the line number where the nested +proof was detected. cmds-reversed is the tail of VANILLAS, +containing the start of the nested proof, in reversed order. If +there is a 'nested-proof chunk in the result, it is the first +chunk." (cl-assert (and proof-omit-proofs-configured proof-script-proof-start-regexp proof-script-proof-end-regexp proof-script-definition-end-regexp proof-script-proof-admit-command) nil "proof-script omit proof feature not properly configured") - (let (;; result vanillas with omitted proofs in reverse order - result - ;; commands of current proof before deciding opaqueness in reverse order + (let (;; result in reversed order + result-chunks + ;; accumulated commands in reversed order before they are put + ;; into a result chunk maybe-result + ;; flag: is the processing loop currently inside a proof or not? inside-proof proof-start-span-start proof-start-span-end ;; t if the proof contains state changing commands and must be kept @@ -2045,25 +2099,18 @@ start is found inside a proof." (progn (if (string-match proof-script-proof-start-regexp cmd) ;; Found another proof start inside a proof. - ;; Stop omitting and pass the remainder unmodified. - ;; The result in `result' is aggregated in reverse - ;; order, need to reverse vanillas. + ;; Stop classifying and return the remainder as + ;; 'no-proof chunk. The commands in `result-chunks' + ;; are in reverse order, need to reverse the remaining + ;; vanillas. (progn - (setq result (nconc (nreverse vanillas) maybe-result result)) + (push (list 'nested-proof + (line-number-at-pos (span-end (car item))) + (nconc (nreverse vanillas) maybe-result)) + result-chunks) (setq maybe-result nil) ;; terminate the while loop - (setq vanillas nil) - ;; for Coq nobody will notice the warning, because - ;; the error about nested proofs will pop up shortly - ;; afterwards - (display-warning - '(proof-script) - ;; use the end of the span, because the start is - ;; usually on the preceding line - (format (concat "found second proof start at line %d" - " - are there nested proofs?") - (line-number-at-pos (span-end (car item)))))) - + (setq vanillas nil)) ;; else - no nested proof, but still inside-proof (if (and (string-match proof-script-proof-end-regexp cmd) (not proof-must-be-kept)) @@ -2071,43 +2118,13 @@ start is found inside a proof." ;; recognize a state changing command inside the ;; proof that would prohibit throwing the proof ;; away. - (let - ;; Reuse the Qed span for the whole proof, - ;; including the faked Admitted command. - ;; `proof-done-advancing' expects such a span. - ((cmd-span (car item))) - (span-set-property cmd-span 'type 'omitted-proof) - (span-set-property cmd-span - 'cmd proof-script-proof-admit-command) - (span-set-endpoints cmd-span proof-start-span-end - (span-end (car item))) - ;; Throw away all commands between start of proof - ;; and the current point, in particular, delete - ;; all the spans. - (mapc - (lambda (item) (span-detach (car item))) - maybe-result) + (progn + (push (list 'proof + proof-start-span-start + proof-start-span-end + (cons item maybe-result)) + result-chunks) (setq maybe-result nil) - ;; Record start and end point for the fancy - ;; colored span that marks the skipped proof. The - ;; span will be created in - ;; `proof-done-advancing-save' when - ;; `proof-script-proof-admit-command' is retired. - (span-set-property - cmd-span 'omitted-proof-region - ;; for the start take proper line start if possible - (list (proof-move-over-whitespace-to-next-line - proof-start-span-start) - ;; For the end, don't extend to the end of - ;; the line, because then the fancy color - ;; span is behind the end of the proof span - ;; and will get deleted when undoing just - ;; behind that proof. - (span-end (car item)))) - (push (list cmd-span - (list proof-script-proof-admit-command) - 'proof-done-advancing nil) - result) (setq inside-proof nil)) ;; else - no nested proof, no opaque proof, but still inside @@ -2119,7 +2136,9 @@ start is found inside a proof." ;; such that the proof-must-be-kept. ;; Need to keep all commands from the start of the proof. (progn - (setq result (cons item (nconc maybe-result result))) + (push (list 'no-proof + (cons item maybe-result)) + result-chunks) (setq maybe-result nil) (setq inside-proof nil)) @@ -2139,9 +2158,12 @@ start is found inside a proof." ;; else - outside proof (if (string-match proof-script-proof-start-regexp cmd) (progn + (push (list 'no-proof + ;; Keep the Proof using command in the + ;; 'no-proof chunk. + (cons item maybe-result)) + result-chunks) (setq maybe-result nil) - ;; Keep the Proof using command in any case. - (push item result) (setq proof-start-span-start (span-start (car item))) (setq proof-start-span-end (span-end (car item))) (setq inside-proof t) @@ -2157,12 +2179,104 @@ start is found inside a proof." (setq next-proof-must-be-kept nil))) ;; keep current item unmodified - (push item result))) + (push item maybe-result))) (setq vanillas (cdr vanillas))) - ;; end of loop - return filtered vanillas - (nreverse (nconc maybe-result result)))) + ;; end of loop - keep remaining items + (when maybe-result + (push (list 'no-proof maybe-result) result-chunks)) + result-chunks)) +(defun proof-script-omit-proofs (vanillas) + "Return a copy of VANILLAS with complete opaque proofs omitted. +See `proof-omit-proofs-configured' for the description of the +omit proofs feature. This function uses +`proof-script-proof-start-regexp', +`proof-script-proof-end-regexp' and +`proof-script-definition-end-regexp' to search for complete +opaque proofs in the action list VANILLAS. Additionally, it uses +`proof-script-cmd-prevents-proof-omission' and +`proof-script-cmd-force-next-proof-kept' to detect proofs that +cannot be omitted. Complete opaque proofs are replaced by +`proof-script-proof-admit-command'. The span of the admit command +contains an 'omitted-proof-region property with the region of the +omitted proof. This is used in `proof-done-advancing-save' to +colour the omitted proof with `proof-omitted-proof-face'. + +Display a warning if another proof start is found inside a +proof." + (let ((chunks (proof-script-omit-filter vanillas)) + result) + (dolist (chunk chunks result) + (cond + ((eq (car chunk) 'nested-proof) + ;; chunk: ('nested-proof line-number-nested-proof cmds-reversed) + ;; + ;; A nested-proof chunk can only appear at the head when + ;; result is still empty. + (cl-assert (null result) nil + "proof-script-omit internal error: nested-proof not at head") + ;; Display a warning and keep the commands unmodified. + ;; + ;; For Coq nobody will notice the warning, because the error + ;; about nested proofs will pop up shortly afterwards. + (display-warning + '(proof-script) + ;; use the end of the span, because the start is + ;; usually on the preceding line + (format (concat "found second proof start at line %d" + " - are there nested proofs?") + (nth 1 chunk))) + (setq result (nreverse (nth 2 chunk)))) + + ((eq (car chunk) 'no-proof) + ;; chunk: ('no-proof cmds-reversed) + ;; + ;; keep all commands unmodified + (setq result (nconc (nreverse (nth 1 chunk)) result))) + + ((eq (car chunk) 'proof) + ;; chunk: ('proof span-start-first-proof-cmd + ;; span-end-first-proof-cmd + ;; proof-cmds-reversed) + (let* ((proof-start-span-start (nth 1 chunk)) + (proof-start-span-end (nth 2 chunk)) + (cmds-rev (nth 3 chunk)) + (last-cmd-span (caar cmds-rev))) + ;; Reuse the span of the last proof command (Qed) for the + ;; whole proof, including the faked Admitted. + (span-set-property last-cmd-span 'type 'omitted-proof) + (span-set-property last-cmd-span 'cmd proof-script-proof-admit-command) + (span-set-endpoints last-cmd-span + proof-start-span-end + (span-end last-cmd-span)) + ;; Commands inside the proof are thrown away. Thererfore + ;; delete all their spans, except the span of the last proof + ;; command, which is reused here. + (mapc + (lambda (item) (span-detach (car item))) + (cdr cmds-rev)) + ;; Record start and end point for the fancy colored span + ;; that marks the skipped proof. The span will be created in + ;; `proof-done-advancing-save' when + ;; `proof-script-proof-admit-command' is retired. + (span-set-property + last-cmd-span 'omitted-proof-region + (list + ;; for the start take proper line start if possible + (proof-move-over-whitespace-to-next-line proof-start-span-start) + ;; For the end, don't extend to the end of the line, + ;; because then the fancy color span is behind the end of + ;; the proof span and will get deleted when undoing just + ;; behind that proof. + (span-end last-cmd-span))) + ;; replace proof commands by admit + (push (list last-cmd-span (list proof-script-proof-admit-command) + 'proof-done-advancing nil) + result))) + (t + (cl-assert nil nil + "proof-script-omit internal error: unknown chunk type")))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;