Skip to content

Commit

Permalink
omit-proofs: split command processing into two phases
Browse files Browse the repository at this point in the history 
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.
  • Loading branch information
@hendriktews
hendriktews committed Mar 25, 2024
1 parent 5d6cbdf commit ad39c0c
Show file tree
Hide file tree
Showing 2 changed files with 207 additions and 75 deletions.
22 changes: 20 additions & 2 deletions ci/simple-tests/coq-test-omit-proofs.el
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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 ()
Expand Down
260 changes: 187 additions & 73 deletions generic/proof-script.el
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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
Expand All @@ -2045,69 +2099,32 @@ 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))
;; End of opaque proof recognized and we didn't
;; 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
Expand All @@ -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))

Expand All @@ -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)
Expand All @@ -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"))))))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
Expand Down

0 comments on commit ad39c0c

Please sign in to comment.