Automatic "Proof using" insertion.

When "Suggest Proof Using" is set in coq, coq suggests "Proof using"
annotations. We insert these annotation (by default after asking the
user).

3 files changed, 103 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 2b686029..cbe2e76d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -45,6 +45,29 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac
     compilation does not stop at the first error but rather
     continues as far as possible.
 
+*** Automatic insertion of "Proof using" annotations.
+
+    When "Suggest Proof Using" is set in coq, coq suggests "Proof
+    using" annotations when it detects there is no such annotation (or
+    a wrong one) in you proof and there should be one (i.r. you are
+    inside a section). By default PG will ask the user before
+    inserting the suggested annotation. You can customize this
+    behaviour:
+
+    (setq coq-accept-proof-using-suggestion 'always)
+    or
+    (setq coq-accept-proof-using-suggestion 'never)
+    or (default)
+    (setq coq-accept-proof-using-suggestion 'ask)
+
+    This is also settable from Coq menu.
+
+    Limitations:
+    - do not support nested proofs.
+    - always use the first suggestion (coq can provide several solutions).
+    - the proof is not replayed, which is consistent with the fact
+      that pg do not deal with async proofs.
+
 *** Limited extensibility for indentation 
 
     Coq indentation mechanism is based on a fixed set of tokens and
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 391b1238..0eb707f7 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -113,6 +113,22 @@
       :selected (eq proof-three-window-mode-policy 'vertical)
       :help "One column mode"])
     ["Refresh Windows Layout" proof-layout-windows t]
+    ("Automatic Proof using annotations..."
+     ["ask"
+      (customize-set-variable 'coq-accept-proof-using-suggestion 'ask)
+      :style radio
+      :selected (eq coq-accept-proof-using-suggestion 'ask)
+      :help "ask user when a new proof using annotation is suggested"]
+     ["always"
+      (customize-set-variable 'coq-accept-proof-using-suggestion 'always)
+      :style radio
+      :selected (eq coq-accept-proof-using-suggestion 'always)
+      :help "Always update the proof using annotation when suggested"]
+     ["never"
+      (customize-set-variable 'coq-accept-proof-using-suggestion 'never)
+      :style radio
+      :selected (eq coq-accept-proof-using-suggestion 'never)
+      :help "never update the proof using"])
     ["Toggle tooltips" proof-output-tooltips-toggle
      :style toggle
      :selected proof-output-tooltips
diff --git a/coq/coq.el b/coq/coq.el
index 8acc1b72..14a3338c 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -2563,6 +2563,70 @@ Warning: this makes the error messages (and location) wrong.")
   "Return t if the last tactic of locked region contains an \"as\" close."
   (save-excursion (string-match "\\<as\\>" s)))
 
+;::::::::::::: inserting suggested Proof using XXX... ;;;;;;;;;;
+
+(defcustom accept-proof-using-suggestion 'ask
+  "Wether proofgeneral should automatically update proof using when
+recieving suggestions from coq at Qed time."
+  :type '(choice
+	  (const :tag "Ask user" ask)
+	  (const :tag "always accept" always)
+	  (const :tag "never accept" never)) 
+  :group 'coq)
+
+(defun coq-extract-proof-using-from-suggestion ()
+  (proof-with-current-buffer-if-exists proof-response-buffer
+     (when (string-match
+            "following commands:\n.*Proof using\\([^.]*\\)\\."
+            (buffer-string))
+         (let* ((s (match-string 1 (buffer-string)))
+                (prefix (if (equal (aref s 0) ? ) " using" " using ")))
+           (concat prefix s)))))
+
+(defun coq-proof-using-equal (s1 s2)
+  (let* ((l1 (split-string s1)) (l2 (split-string s2))
+         (diff (cl-set-exclusive-or l1 l2 :test 'string-equal)))
+    (not diff))) ;; nil if empty xor
+
+
+(defun coq-insert-proof-using-suggestion (suggested)
+  ;; Not compatible with nested lemmas.
+  (with-current-buffer proof-script-buffer
+    (save-excursion
+      (goto-char (proof-unprocessed-begin))
+      (let* ((pos-unproc (point))
+             (proof-pos (save-excursion
+                          (search-backward-regexp "\\<Proof\\>\\([^.]*\\)\\.")))
+             (previous-content (match-string 1))
+             (same (coq-proof-using-equal previous-content suggested)))
+        (when (and (not same) (or (equal coq-accept-proof-using-suggestion 'always)
+                                  (y-or-n-p (concat "Update proof using annotation ("
+                                                    suggested ")"))))
+          (goto-char (+ 5 proof-pos)) ; "Proof" has length 6
+                                        ;(if (stored proof-strict-read-only) )
+          (let ((spl proof-locked-span))
+            ;; temporarily make the locked span writable
+	    (span-read-write spl)
+            (delete-char (length previous-content))
+            (insert suggested)
+            ;; go back to `proof-strict-read-only' says
+            (proof-span-read-only spl)))))))
+
+;; This should be called after a Save or Qed command is called (but not a
+;; "Define").
+(defun coq-proof-using-suggest-hook ()
+  (unless (equal coq-accept-proof-using-suggestion 'never)
+    (let ((suggestion (coq-extract-proof-using-from-suggestion)))
+      (when suggestion
+        (coq-insert-proof-using-suggestion suggestion)))))
+
+
+(add-hook 'proof-shell-handle-delayed-output-hook
+	  #'coq-proof-using-suggest-hook t)
+
+
+;::::::::::::: inserting suggested Proof using XXX... ;;;;;;;;;;
+
 
 (defun coq-insert-as-in-next-command ()
   (interactive)