add feature to omit complete opaque proofs

This commit adds a feature to recognize complete opaque proofs in
the asserted region and to replace them with an admitted proof.
This can drastically improve the processing time for the asserted
region at the cost of not checking the omitted proofs. Omitted
proofs are displayed slightly darker compared to other parts of
the locked region.

With this commit, the feature is supported for Coq for files in
which proofs are started with some form of Proof and ended with
either Qed, Defined, Admitted or Abort.

To enable, configure proof-omit-proofs-option or click
Proof General -> Quick Options -> Processing -> Omit Proofs.

7 files changed, 288 insertions, 3 deletions

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index a517df71..8806774f 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -1107,6 +1107,31 @@ It is used:
              (not (string-match "\\`Proof\\s-*\\(\\.\\|\\_<with\\_>\\|\\_<using\\_>\\)" str))))))
 
 
+;; ----- regular expressions for the proof omit feature
+;; see `proof-omit-proofs-configured' in generic/proof-config
+
+(defcustom coq-proof-start-regexp "^Proof\\(\\.\\| \\)"
+  "Value for `proof-script-proof-start-regexp'."
+  :type 'regexp
+  :group 'coq)
+
+(defcustom coq-proof-end-regexp "^\\(Qed\\|Admitted\\)\\."
+  "Value for `proof-script-proof-end-regexp'.
+This is similar to `coq-save-command-regexp-strict' but slightly
+different."
+  :type 'regexp
+  :group 'coq)
+
+(defcustom coq-definition-end-regexp "^\\(Defined\\|Abort\\)\\(\\.\\| \\)"
+  "Value for `proof-script-definition-end-regexp'."
+  :type 'regexp
+  :group 'coq)
+  
+(defcustom coq-omit-proof-admit-command "Admitted."
+  "Value for `proof-script-proof-admit-command'."
+  :type 'string
+  :group 'coq)
+
 ;; ----- keywords for font-lock.
 
 (defvar coq-keywords-kill-goal
diff --git a/coq/coq.el b/coq/coq.el
index c1f52d38..4add2642 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1979,6 +1979,14 @@ at `proof-assistant-settings-cmds' evaluation time.")
    proof-tree-find-begin-of-unfinished-proof
      'coq-find-begin-of-unfinished-proof)
 
+  ;; proof-omit-proofs config
+  (setq
+   proof-omit-proofs-configured t
+   proof-script-proof-start-regexp coq-proof-start-regexp
+   proof-script-proof-end-regexp coq-proof-end-regexp
+   proof-script-definition-end-regexp coq-definition-end-regexp
+   proof-script-proof-admit-command coq-omit-proof-admit-command)
+
   (setq proof-cannot-reopen-processed-files nil)
 
   (proof-config-done)
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 9632a268..011a6625 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -696,6 +696,67 @@ needed for Coq."
   :type 'boolean
   :group 'proof-script)
 
+(defcustom proof-omit-proofs-configured nil
+  "t if the omit proofs feature has been configured by the proof assitant.
+See also `proof-omit-proofs-option' or the Proof General manual
+for a description of the feature. This option can only be set, if
+all of `proof-script-proof-start-regexp',
+`proof-script-proof-end-regexp',
+`proof-script-definition-end-regexp' and
+`proof-script-proof-admit-command' have been configured.
+
+The omit proofs feature skips over opaque proofs in the source
+code, admitting the theorems, to speed up processing.
+
+If `proof-omit-proofs-option' is set by the user, all proof
+commands in the source following a match of
+`proof-script-proof-start-regexp' up to and including the next
+match of `proof-script-proof-end-regexp', are omitted (not send
+to the proof assistant) and replaced by
+`proof-script-proof-admit-command'. If a match for
+`proof-script-definition-end-regexp' is found while searching
+forward for the proof end, the current proof (up to and including
+the match of `proof-script-definition-end-regexp') is considered
+to be not opaque and not omitted, thus all these proof commands
+_are_ sent to the proof assistant.
+
+If a match for `proof-script-proof-start-regexp' is found before
+the next match for `proof-script-proof-end-regexp' or
+`proof-script-definition-end-regexp', an error is signaled to the
+user.
+
+All the regular expressions for this feature are matched against
+the commands inside proof action items, that is as strings,
+without surrounding space."
+  :type 'boolean
+  :group 'proof-script)
+
+;; proof-omit-proofs-option is in proof-useropts as user option
+
+(defcustom proof-script-proof-start-regexp nil
+  "Regular expression for the start of a proof for the omit proofs feature.
+See `proof-omit-proofs-configured'."
+  :type 'regexp
+  :group 'proof-script)
+
+(defcustom proof-script-proof-end-regexp nil
+  "Regular expression for the end of an opaque proof for the omit proofs feature.
+See `proof-omit-proofs-configured'."
+  :type 'regexp
+  :group 'proof-script)
+
+(defcustom proof-script-definition-end-regexp nil
+  "Regexp for the end of a non-opaque proof for the omit proofs feature.
+See `proof-omit-proofs-configured'."
+  :type 'regexp
+  :group 'proof-script)
+  
+(defcustom proof-script-proof-admit-command nil
+  "Proof command to be inserted instead of omitted proofs."
+  :type 'string
+  :group 'proof-script)
+
+
 ;;
 ;; Proof script indentation
 ;;
diff --git a/generic/proof-faces.el b/generic/proof-faces.el
index 115d8667..b06a64fd 100644
--- a/generic/proof-faces.el
+++ b/generic/proof-faces.el
@@ -218,6 +218,13 @@ Warning messages can come from proof assistant or from Proof General itself."
   "Proof General face for highlighting an error in the proof script. "
   :group 'proof-faces)
 
+(defface proof-omitted-proof-face
+  (proof-face-specs
+   (:background "#EAEFFF" :extend t)
+   (:background "#9C4A90" :extend t)
+   (:foreground "white" :background "black" :extend t))
+  "*Face for background of omitted proofs"
+  :group 'proof-faces)
 
 
 ;;; Compatibility: these are required for use in GNU Emacs/font-lock-keywords
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index 3846229e..e15ce4d5 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -334,6 +334,7 @@ without adjusting window layout."
 (proof-deftoggle proof-fast-process-buffer)
 (proof-deftoggle proof-imenu-enable proof-imenu-toggle)
 (proof-deftoggle proof-keep-response-history)
+(proof-deftoggle proof-omit-proofs-option)
 
 (proof-eval-when-ready-for-assistant
  ;; togglers for settings separately configurable per-prover
@@ -361,6 +362,11 @@ without adjusting window layout."
 ;;;       :selected proof-keep-response-history]
 
      ("Processing"
+      ["Omit Proofs" proof-omit-proofs-option-toggle
+       :style toggle
+       :selected proof-omit-proofs-option
+       :active proof-omit-proofs-configured
+       :help "Skip over proofs, admitting theorems, when asserting larger chunks"]
       ["Fast Process Buffer" proof-fast-process-buffer-toggle
        :style toggle
        :selected proof-fast-process-buffer
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 87a9975b..e9adc199 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1373,7 +1373,17 @@ With ARG, turn on scripting iff ARG is positive."
 
 (defun proof-done-advancing (span)
   "The callback function for `assert-until-point'.
-Argument SPAN has just been processed."
+Argument SPAN has just been processed.
+
+This is the callback for all the normal commands. Besides stuff
+that is not yet documented here, this function
+- extends the locked region
+- creates additional spans (without 'type property) for help,
+  tooltips, color and menus
+- merges spans with 'type as needed to achieve atomic undo for
+  proofs and sections
+- enters some commands and their spans in some database (with for
+  me unknown purpose)"
   (let ((end     (span-end span))
 	(cmd     (span-property span 'cmd)))
 
@@ -1406,6 +1416,8 @@ Argument SPAN has just been processed."
      ;; CASE 3: Proof completed one step or more ago, non-save
      ;; command seen, no nested goals allowed.
      ;;
+     ;; AFAICT case 3 is never taken for Coq.
+     ;; 
      ;; We make a fake goal-save from any previous
      ;; goal to the command before the present one.
      ;;
@@ -1463,11 +1475,23 @@ Argument SPAN has just been processed."
 
 
 (defun proof-done-advancing-save (span)
-  "A subroutine of `proof-done-advancing'.  Add info for save span SPAN."
+  "Retire commands that close a proof or some other region.
+This is a subroutine of `proof-done-advancing'.
+Besides stuff that is not yet documented here, this function
+- creates additional spans (without 'type property) for help,
+  tooltips, color and menus
+- in particular, adds the background color for omitted proofs
+- merges spans with 'type as needed to achieve atomic undo for
+  proofs and sections; for Coq this is done at least for proofs
+  and sections.
+- enters some commands and their spans in some database (with for
+  me unknown purpose)"
   (unless (or (eq proof-shell-proof-completed 1)
 	      (eq proof-assistant-symbol 'isar))
     ;; We expect saves to succeed only for recently completed top-level proofs.
     ;; NB: not true in Isar, because save commands can perform proof.
+    ;; Note: not true in Coq either, if there is a command (eg. a Check)
+    ;; between the tactic that finished the proof and the Qed.
     (proof-debug
      (format
       "PG: save command with proof-shell-proof-completed=%s, proof-nesting-depth=%s"
@@ -1480,6 +1504,13 @@ Argument SPAN has just been processed."
 	(savestart (span-start span))
 	(saveend   (span-end span))
 	(cmd       (span-property span 'cmd))
+        ;; With the omit proofs feature (see
+        ;; `proof-omit-proofs-configured'), the span of the Admitted
+        ;; command that replaces the proof contains an
+        ;; 'omitted-proof-region property, that holds the start and
+        ;; end of the omitted proof for colouring. The property is
+        ;; only inserted for omitted proofs in the replacing Admitted.
+        (omitted-proof-region (span-property span 'omitted-proof-region))
 	lev nestedundos nam next)
 
     (and proof-save-with-hole-regexp
@@ -1546,6 +1577,20 @@ Argument SPAN has just been processed."
       (proof-make-goalsave gspan (span-end gspan)
 			   savestart saveend nam nestedundos)
 
+      ;; In case SPAN (which is retired now) belongs to an admit
+      ;; command that closes an omitted proof: create an additional
+      ;; span for the different background color of the omitted span.
+      ;; Start and end point of this span has been computed before in
+      ;; `proof-script-omit-proofs'. This background color span is
+      ;; registered in the span of the goal command for the only
+      ;; reason to not leave it dangling around.
+      (when omitted-proof-region
+        (let ((omit-span (span-make (car omitted-proof-region)
+                                    (cadr omitted-proof-region))))
+          (span-set-property omit-span 'face 'proof-omitted-proof-face)
+          (span-set-property omit-span 'omitted-proof-span t)
+          (span-set-property gspan 'omit-color-span omit-span)))
+
       ;; *** Theorem dependencies ***
       (if proof-last-theorem-dependencies
 	  (proof-depends-process-dependencies nam gspan)))))
@@ -1933,6 +1978,124 @@ Assumes that point is at the end of a command."
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
+;; Omit proofs feature.
+;;
+;; See `proof-omit-proofs-configured' for the feature. When the parsed
+;; 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'.
+
+(defun proof-move-over-whitespace-to-next-line (pos)
+  "Return position of next line if one needs only to jump over white space.
+Utility function. In the current buffer, check if beginning of
+next line can be reached from POS by moving over white
+space (spaces, tabs) only. If yes return the beginning of next
+line, otherwise POS."
+  (save-excursion
+    (goto-char pos)
+    (skip-chars-forward " \t")
+    (setq pos (point))
+    (if (eolp)
+        (1+ (point))
+      pos)))
+  
+(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. 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."
+  (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 maybe-result inside-proof
+        proof-start-span-start proof-start-span-end)
+    (dolist (item vanillas (nreverse (nconc maybe-result result)))
+      (let ((cmd (mapconcat 'identity (nth 1 item) " ")))
+        (if inside-proof
+            (progn
+              (when (string-match proof-script-proof-start-regexp cmd)
+                ;; found another proof start inside a proof
+                (error "found another proof start inside a proof"))
+              (if (string-match proof-script-proof-end-regexp cmd)
+                  (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)
+                    (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))
+                (if (string-match proof-script-definition-end-regexp cmd)
+                    ;; A proof ending in Defined or something similar.
+                    ;; Need to keep all commands from the start of the proof.
+                    (progn
+                      (setq result (cons item (nconc maybe-result result)))
+                      (setq maybe-result nil)
+                      (setq inside-proof nil))
+                  ;; normal proof command - maybe it belongs to a
+                  ;; Defined, keep it separate, until we know.
+                  (push item maybe-result))))
+          ;; outside proof
+          (if (string-match proof-script-proof-start-regexp cmd)
+              (progn
+                (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))
+            ;; outside, no proof start - keep it unmodified
+            (push item result)))))
+    ;; return (nreverse (nconc maybe-result result)), see dolist above
+    ))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
 ;; Assert-until-point.
 ;;
 ;; This function parses some region of the script buffer into
@@ -2005,12 +2168,16 @@ SEMIS must be a non-empty list, in reverse order (last position first).
 We assume that the list is contiguous and begins at (proof-queue-or-locked-end).
 We also delete help spans which appear in the same region (in the expectation
 that these may be overwritten).
-This function expects the buffer to be activated for advancing."
+This function expects the buffer to be activated for advancing.
+If the omit proofs feature is active, complete opaque proofs will
+be omitted from the vanilla action list obtained from SEMIS."
   (cl-assert semis nil "proof-assert-semis: argument must be a list")
   (let ((startpos  (proof-queue-or-locked-end))
 	(lastpos   (nth 2 (car semis)))
 	(vanillas  (proof-semis-to-vanillas semis displayflags)))
     (proof-script-delete-secondary-spans startpos lastpos)
+    (when (and proof-omit-proofs-option proof-omit-proofs-configured)
+      (setq vanillas (proof-script-omit-proofs vanillas)))
     (proof-extend-queue lastpos vanillas)))
 
 (defun proof-retract-before-change (beg end)
diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el
index 4ce51c99..d5df0404 100644
--- a/generic/proof-useropts.el
+++ b/generic/proof-useropts.el
@@ -99,6 +99,17 @@ be inserted as the user types commands to the prover."
   :set 'proof-set-value
   :group 'proof-user-options)
 
+(defcustom proof-omit-proofs-option nil
+  "Set to t to omit complete opaque proofs for speed reasons.
+When t, complete opaque proofs in the asserted region are not
+sent to the proof assistant (and thus not checked). For files
+with big proofs this can drastically reduce the processing time
+for the asserted region at the cost of not checking the proofs.
+For partial and non-opaque proofs in the asserted region all
+proof commands are sent to the proof assistant."
+  :type 'boolean
+  :group 'proof-user-options)
+
 (defcustom pg-show-hints t
   "*Whether to display keyboard hints in the minibuffer."
   :type 'boolean