Experiments with real-time extraction

mindless-extraction.el

(require 'dash)

(defun company-coq--plug-subproof-holes (partial-proof)
  "Plug evars in PARTIAL-PROOF, producing a closed term.
Note that type inference may fail on that term."
  (replace-regexp-in-string (concat "[?]\\(" coq-id "\\(@{[^}]+}\\)?\\)")
                            "(_UNFINISHED_GOAL_ _)"
                            partial-proof t))

(defun company-coq-backto (state)
  "Reqing Coq to STATE, if non-nil."
  (when state
    (company-coq-ask-prover (format "BackTo %d." state))))

(defun company-coq-ask-prover-throw-errors (command)
  "Run COMMAND, and fail if it returns an error.
If UNDO-STATE is non-nil, go back to that Coq state before throwing."
  (let ((result (company-coq-ask-prover command)))
    (when (company-coq-error-message-p result)
      (error "Running %S failed with message %S" command result))
    result))

(defvar company-coq--partial-prog-name "_UNFINISHED_PROGRAM_"
  "Name of the program to partially extract.")

(defvar company-coq--extraction-busy nil
  "Whether the extraction view is currently busy.")

(defun company-coq--extract-partial ()
  "Extract the current proof, plugging holes with _UNFINISHED_GOAL."
  (interactive)
  (unless (or proof-shell-busy company-coq--extraction-busy)
    (-when-let* ((statenum (car (coq-last-prompt-info-safe))))
      (setq company-coq--extraction-busy t)
      (unwind-protect
          (let* ((proof-shell-eager-annotation-start nil) ;; Disable capture of urgent messages
                 (_ (company-coq-ask-prover-throw-errors "Axiom _UNFINISHED_GOAL_ : forall (T : Type), T."))
                 (partial-proof (company-coq-ask-prover-throw-errors "Show Proof."))
                 (complete-proof (company-coq--plug-subproof-holes partial-proof))
                 (def-command (format "Definition %s := %s." company-coq--partial-prog-name complete-proof))
                 (definition-result (company-coq-ask-prover-throw-errors def-command))
                 (extraction-command (format "Extraction %s." company-coq--partial-prog-name))
                 (extraction-result (company-coq-ask-prover-throw-errors extraction-command)))
            (company-coq--display-extraction extraction-result))
        (company-coq-backto statenum)
        (setq company-coq--extraction-busy nil)))))

(defvar company-coq--extraction-buffer-name "*extraction*")

(defun company-coq--display-extraction (extraction)
  "Display EXTRACTION in its own window."
  (with-current-buffer (get-buffer-create company-coq--extraction-buffer-name)
    (erase-buffer)
    (insert extraction)
    (let ((tuareg-mode-hook nil))
      (tuareg-mode))
    (company-coq-fontify-buffer)
    (unless (get-buffer-window (current-buffer))
      (-when-let* ((script-buf proof-script-buffer)
                   (script-win (get-buffer-window script-buf)))
        (set-window-buffer (split-window-vertically) (current-buffer))))))

(defun company-coq--extract-partial-in-bg ()
  "Update extraction buffer, ignoring errors if any."
  (condition-case err
      (company-coq--extract-partial)
    (error (-when-let* ((buf (get-buffer company-coq--extraction-buffer-name))
                        (win (get-buffer-window buf)))
             (delete-window win)))))

(defun company-coq--extraction-hook-fn ()
  "Hook function to update extraction display."
  (run-with-timer 0 nil #'company-coq--extract-partial-in-bg))

(define-key coq-mode-map (kbd "<f5>") #'company-coq--extract-partial)

(add-hook 'proof-shell-handle-delayed-output-hook #'company-coq--extraction-hook-fn)

test.v

Definition ExampleFunction : nat -> nat.
Proof.
  intros.
  refine (S _).
  refine (_ - 1).

  refine (3 * _).
  destruct H.
  + refine (1 + _).
    apply 0.
  + refine (2 + _).
    destruct H.
    * refine (3 + _).
      apply 0.
    * refine (4 + _).
Admitted.