;;; inferior-coq.el --- Run an inferior Coq process.
;;;
;;; Copyright (C) Marco Maggesi <maggesi@math.unifi.it>
;;; Time-stamp: "2002-07-03 12:53:43 maggesi"


;; Emacs Lisp Archive Entry
;; Filename: inferior-coq.el
;; Version: 1.0
;; Keywords: process coq
;; Author: Marco Maggesi <maggesi@math.unifi.it>
;; Maintainer: Marco Maggesi <maggesi@math.unifi.it>
;; Description: Run an inferior Coq process.
;; URL: http://www.math.unifi.it/~maggesi/
;; Compatibility: Emacs20, Emacs21, XEmacs21

;; This is free software; you can redistribute it and/or modify it under
;; the terms of the GNU General Public License as published by the Free
;; Software Foundation; either version 2, or (at your option) any later
;; version.
;;
;; This is distributed in the hope that it will be useful, but WITHOUT
;; ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
;; FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
;; for more details.
;;
;; You should have received a copy of the GNU General Public License
;; along with GNU Emacs; see the file COPYING.  If not, write to the
;; Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
;; MA 02111-1307, USA.

;;; Commentary:

;; Coq is a proof assistant (http://coq.inria.fr/).  This code run an
;; inferior Coq process and defines functions to send bits of code
;; from other buffers to the inferior process.  This is a
;; customisation of comint-mode (see comint.el).  For a more complex
;; and full featured Coq interface under Emacs look at Proof General
;; (http://zermelo.dcs.ed.ac.uk/~proofgen/).
;;
;; Written by Marco Maggesi <maggesi@math.unifi.it> with code heavly
;; borrowed from emacs cmuscheme.el
;;
;; Please send me bug reports, bug fixes, and extensions, so that I can
;; merge them into the master source.

;;; Installation:

;; You need to have coq.el already installed (it comes with the
;; standard Coq distribution) in order to use this code.  Put this
;; file somewhere in you load-path and add the following lines in your
;; "~/.emacs":
;;
;;   (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist))
;;   (autoload 'coq-mode "coq" "Major mode for editing Coq vernacular." t)
;;   (autoload 'run-coq "inferior-coq" "Run an inferior Coq process." t)
;;   (autoload 'run-coq-other-window "inferior-coq"
;;     "Run an inferior Coq process in a new window." t)
;;   (autoload 'run-coq-other-frame "inferior-coq"
;;     "Run an inferior Coq process in a new frame." t)

;;; Usage:

;; Call `M-x "run-coq'.
;;
;; Functions and key bindings (Learn more keys with `C-c C-h' or `C-h m'):
;;
;; C-return (`coq-add-line')     send the current line and insert ret.
;; M-return (`coq-send-line')    send the current line.
;; C-down   (`coq-send-line')    send the current line.
;; C-up     (`coq-send-undo')    send the command "Undo".
;; C-right  (`coq-come-here')    restart and send until current point.
;; C-left   (`coq-send-abort')   send the command "Abort".
;; C-c C-r  (`coq-send-region')  send the current region.
;; C-c C-a  (`coq-send-abort')   send the command "Abort".
;; C-c C-t  (`coq-send-restart') send the command "Restart".
;; C-c C-s  (`coq-send-show')    send the command "Show".
;; C-c C-u  (`coq-send-undo')    send the command "Undo".
;; C-c C-v  (`coq-check-region') run command "Check" on region.
;; C-c C-v  (`coq-check-print')  run command "Print" on region.
;; C-c .    (`coq-come-here')    restart and send until current point.

;;; Change Log:

;; From -0.0 to 1.0 brought into existence.


(require 'coq)
(require 'comint)
(require 'easymenu)

(setq coq-program-name "coqtop")
(setq coq-byte-program-name "coqtop -byte")

(defgroup inferior-coq nil
  "Run a coq process in a buffer."
  :group 'coq)

(defcustom inferior-coq-mode-hook nil
  "*Hook for customising `inferior-coq-mode'."
  :type 'hook
  :group 'coq)

(defvar inferior-coq-mode-map
  (let ((m (make-sparse-keymap)))
    (define-key m "\C-c\C-r" 'coq-send-region)
    (define-key m "\C-c\C-a" 'coq-send-abort)
    (define-key m "\C-c\C-t" 'coq-send-restart)
    (define-key m "\C-c\C-s" 'coq-send-show)
    (define-key m "\C-c\C-u" 'coq-send-undo)
    (define-key m "\C-c\C-v" 'coq-check-region)
    (define-key m "\C-c\C-p" 'coq-print-region)
    (define-key m [(control up)] 'coq-send-undo)
    (define-key m [(control left)] 'coq-send-abort)
    m))

;; Install the process communication commands in the coq-mode keymap.
(define-key coq-mode-map [(control return)] 'coq-add-line)
(define-key coq-mode-map [(meta return)] 'coq-send-line)
(define-key coq-mode-map [(control down)] 'coq-send-line)
(define-key coq-mode-map [(control up)] 'coq-send-undo)
(define-key coq-mode-map [(control right)] 'coq-come-here)
(define-key coq-mode-map [(control left)] 'coq-send-abort)
(define-key coq-mode-map [f8] 'coq-send-vernac)
(define-key coq-mode-map [f7] 'coq-send-replay)

(define-key coq-mode-map "\C-c\C-r" 'coq-send-region)
(define-key coq-mode-map "\C-c\C-a" 'coq-send-abort)
(define-key coq-mode-map "\C-c\C-t" 'coq-send-restart)
(define-key coq-mode-map "\C-c\C-s" 'coq-send-show)
(define-key coq-mode-map "\C-c\C-u" 'coq-send-undo)
(define-key coq-mode-map "\C-c\C-v" 'coq-check-region)
(define-key coq-mode-map "\C-c\C-p" 'coq-print-region)
(define-key coq-mode-map "\C-c." 'coq-come-here)

'(easy-menu-define coq-menu inferior-coq-mode-map "Menu for `inferior-coq'"
  '("Coq"
    ["One entry" coq-send-region t]
    '("Sub Menu"
      ["My subentry" my-obscure-function t])
    ))

(easy-menu-define inferior-coq-menu inferior-coq-mode-map
  "Menu for `inferior-coq-mode'."
  '("Inf-Coq"
    ["Abort" coq-send-abort t]
    ["Restart" coq-send-restart t]
    ["Show" coq-send-show t]
    ["Undo" coq-send-undo t]
    ["Check region" coq-check-region t]
    ["Print region" coq-print-region t]
    ))

(easy-menu-define coq-menu coq-mode-map
  "Menu for `coq-mode'."
  '("Inf-Coq"
    ["Run Coq" run-coq-other-frame t]
    ["Run Coq Byte" run-coq-byte-other-frame t]
    ["Send line" coq-send-line t]
    ["Send Region" coq-send-region t]
    ["Come here" coq-come-here t]
    ["Abort" coq-send-abort t]
    ["Restart" coq-send-restart t]
    ["Show" coq-send-show t]
    ["Undo" coq-send-undo t]
    ["Check region" coq-check-region t]
    ["Print region" coq-print-region t]
    ))

(defvar coq-buffer)

(define-derived-mode inferior-coq-mode comint-mode "Inferior Coq"
  "\
Major mode for interacting with an inferior Coq process.

The following commands are available:
\\{inferior-coq-mode-map}

A Coq process can be fired up with M-x run-coq.

Customisation: Entry to this mode runs the hooks on comint-mode-hook
and inferior-coq-mode-hook (in that order).

You can send text to the inferior Coq process from other buffers
containing Coq source.

Functions and key bindings (Learn more keys with `C-c C-h'):
  C-return ('M-x coq-send-line)     send the current line.
  C-c C-r  (`M-x coq-send-region')  send the current region.
  C-c C-a  (`M-x coq-send-abort')   send the command \"Abort\".
  C-c C-t  (`M-x coq-send-restart') send the command \"Restart\".
  C-c C-s  (`M-x coq-send-show')    send the command \"Show\".
  C-c C-u  (`M-x coq-send-undo')    send the command \"Undo\".
  C-c C-v  (`M-x coq-check-region') run command \"Check\" on region.
  C-c C-p  (`M-x coq-print-region') run command \"Print\" on region.
  C-c .    (`M-x coq-come-here')    Restart and send until current point.
"
  ;; Customise in inferior-coq-mode-hook
  (setq comint-prompt-regexp "^[^<]* < *")
  (coq-mode-variables)
  (setq mode-line-process '(":%s"))
  (setq comint-input-filter (function coq-input-filter))
  (setq comint-get-old-input (function coq-get-old-input))
  ;; (easy-menu-add (inferior-coq-menu "inferior-coq-mode"))
  ;; (easy-menu-add (coq-menu "coq-mode"))
  )

(defcustom inferior-coq-filter-regexp "\\`\\s *\\S ?\\S ?\\s *\\'"
  "*Input matching this regexp are not saved on the history list.
Defaults to a regexp ignoring all inputs of 0, 1, or 2 letters."
  :type 'regexp
  :group 'inferior-coq)

(defun coq-input-filter (str)
  "Don't save anything matching `inferior-coq-filter-regexp'."
  (not (string-match inferior-coq-filter-regexp str)))

(defun coq-get-old-input ()
  "Snarf the sexp ending at point."
  (save-excursion
    (let ((end (point)))
      (backward-sexp)
      (buffer-substring (point) end))))

(defun coq-args-to-list (string)
  (let ((where (string-match "[ \t]" string)))
    (cond ((null where) (list string))
	  ((not (= where 0))
	   (cons (substring string 0 where)
		 (coq-args-to-list (substring string (+ 1 where)
						 (length string)))))
	  (t (let ((pos (string-match "[^ \t]" string)))
	       (if (null pos)
		   nil
		 (coq-args-to-list (substring string pos
						 (length string)))))))))

;;;###autoload
(defun run-coq (cmd)
  "Run an inferior Coq process, input and output via buffer *coq*.
If there is a process already running in `*coq*', switch to that buffer.
With argument, allows you to edit the command line (default is value
of `coq-program-name').  Runs the hooks `inferior-coq-mode-hook'
\(after the `comint-mode-hook' is run).
\(Type \\[describe-mode] in the process buffer for a list of commands.)"

  (interactive (list (if current-prefix-arg
			 (read-string "Run Coq: " coq-program-name)
			 coq-program-name)))
  (if (not (comint-check-proc "*coq*"))
      (let ((cmdlist (coq-args-to-list cmd)))
	(set-buffer (apply 'make-comint "coq" (car cmdlist)
			   nil (cdr cmdlist)))
	(inferior-coq-mode)))
  (setq coq-program-name cmd)
  (setq coq-buffer "*coq*")
  (switch-to-buffer "*coq*"))
;;;###autoload (add-hook 'same-window-buffer-names "*coq*")

;;;###autoload
(defun run-coq-other-window (cmd)
  "Run an inferior Coq process, input and output via buffer *coq*.
If there is a process already running in `*coq*', switch to that buffer.
With argument, allows you to edit the command line (default is value
of `coq-program-name').  Runs the hooks `inferior-coq-mode-hook'
\(after the `comint-mode-hook' is run).
\(Type \\[describe-mode] in the process buffer for a list of commands.)"

  (interactive (list (if current-prefix-arg
			 (read-string "Run Coq: " coq-program-name)
			 coq-program-name)))
  (if (not (comint-check-proc "*coq*"))
      (let ((cmdlist (coq-args-to-list cmd)))
	(set-buffer (apply 'make-comint "coq" (car cmdlist)
			   nil (cdr cmdlist)))
	(inferior-coq-mode)))
  (setq coq-program-name cmd)
  (setq coq-buffer "*coq*")
  ;;(pop-to-buffer "*coq*")
  (display-buffer "*coq*"))
;;;###autoload (add-hook 'same-window-buffer-names "*coq*")

(defun run-coq-other-frame (cmd)
  "Run an inferior Coq process, input and output via buffer *coq*.
If there is a process already running in `*coq*', switch to that buffer.
With argument, allows you to edit the command line (default is value
of `coq-program-name').  Runs the hooks `inferior-coq-mode-hook'
\(after the `comint-mode-hook' is run).
\(Type \\[describe-mode] in the process buffer for a list of commands.)"

  (interactive (list (if current-prefix-arg
			 (read-string "Run Coq: " coq-program-name)
			 coq-program-name)))
  (if (not (comint-check-proc "*coq*"))
      (let ((cmdlist (coq-args-to-list cmd)))
	(set-buffer (apply 'make-comint "coq" (car cmdlist)
			   nil (cdr cmdlist)))
	(inferior-coq-mode)))
  (setq coq-program-name cmd)
  (setq coq-buffer "*coq*")
  (switch-to-buffer-other-frame "*coq*"))

(defun run-coq-byte-other-frame (cmd)
  "Run an inferior Coq process, input and output via buffer *coq*.
If there is a process already running in `*coq*', switch to that buffer.
With argument, allows you to edit the command line (default is value
of `coq-program-name').  Runs the hooks `inferior-coq-mode-hook'
\(after the `comint-mode-hook' is run).
\(Type \\[describe-mode] in the process buffer for a list of commands.)"

  (interactive (list (if current-prefix-arg
			 (read-string "Run Coq: " coq-byte-program-name)
			 coq-byte-program-name)))
  (if (not (comint-check-proc "*coq*"))
      (let ((cmdlist (coq-args-to-list cmd)))
	(set-buffer (apply 'make-comint "coq" (car cmdlist)
			   nil (cdr cmdlist)))
	(inferior-coq-mode)))
  (setq coq-program-name cmd)
  (setq coq-buffer "*coq*")
  (switch-to-buffer-other-frame "*coq*"))

(defun switch-to-coq (eob-p)
  "Switch to the coq process buffer.
With argument, position cursor at end of buffer."
  (interactive "P")
  (if (get-buffer coq-buffer)
      (pop-to-buffer coq-buffer)
      (error "No current process buffer.  See variable `coq-buffer'"))
  (cond (eob-p
	 (push-mark)
	 (goto-char (point-max)))))

(defun coq-send-region (start end)
  "Send the current region to the inferior Coq process."
  (interactive "r")
  (comint-send-region (coq-proc) start end)
  (comint-send-string (coq-proc) "\n"))

(defun coq-send-line ()
  "Send the current line to the Coq process."
  (interactive)
  (save-excursion
    (end-of-line)
    (let ((end (point)))
      (beginning-of-line)
      (coq-send-region (point) end)))
  (next-line 1))

(defun coq-add-line ()
  "Send the current line to the Coq process then insert return."
  (interactive)
  (save-excursion
    (end-of-line)
    (let ((end (point)))
      (beginning-of-line)
      (coq-send-region (point) end)))
  (end-of-line)
  (newline))

(defun coq-send-vernac ()
  "Send vernacular phrase at point."
  (interactive)
  (coq-backward-vernac)
  (while (forward-comment 1))
  (let ((beg (point))) 
    (coq-forward-vernac)
    (coq-send-region beg (point))
    (coq-forward-vernac)))

(defun coq-send-abort ()
  "Send the command \"Abort.\" to the inferior Coq process."
  (interactive)
  (comint-send-string (coq-proc) "Abort.\n"))

(defun coq-send-restart ()
  "Send the command \"Restart.\" to the inferior Coq process."
  (interactive)
  (comint-send-string (coq-proc) "Restart.\n"))

(defun coq-send-replay ()
  "Send the command \"Restart\" and move point at the beginning of the
current proof."
  (interactive)
  (coq-send-restart)
  (let ((pos (coq-search-theorem-backward)))
    (if pos (goto-char pos))
    (coq-forward-vernac)
    (coq-forward-vernac)))

(defun coq-send-undo ()
  "Reset coq to the initial state and send the region between the
beginning of file and the point."
  (interactive)
  (comint-send-string (coq-proc) "Undo.\n"))

(defun coq-check-region (start end)
  "Run the commmand \"Check\" on the current region."
  (interactive "r")
  (comint-send-string (coq-proc) "Check ")
  (comint-send-region (coq-proc) start end)
  (comint-send-string (coq-proc) ".\n"))

(defun coq-print-region (start end)
  "Run the commmand \"Check\" on the current region."
  (interactive "r")
  (comint-send-string (coq-proc) "Print ")
  (comint-send-region (coq-proc) start end)
  (comint-send-string (coq-proc) ".\n"))

(defun coq-send-show ()
  "Send the command \"Show.\" to the inferior Coq process."
  (interactive)
  (comint-send-string (coq-proc) "Show.\n"))

(defun coq-come-here ()
  "Reset coq to the initial state and send the region between the
   beginning of file and the point."
  (interactive)
  (comint-send-string (coq-proc) "Reset Initial.\n")
  (coq-send-region 1 (point)))

(defvar coq-buffer nil "*The current coq process buffer.")

(defun coq-proc ()
  "Return the current coq process.  See variable `coq-buffer'."
  (let ((proc (get-buffer-process (if (eq major-mode 'inferior-coq-mode)
				      (current-buffer)
				      coq-buffer))))
    (or proc
	(error "No current process.  See variable `coq-buffer'"))))

(defcustom inferior-coq-load-hook nil
  "This hook is run when inferior-coq is loaded in.
This is a good place to put keybindings."
  :type 'hook
  :group 'inferior-coq)
	
(run-hooks 'inferior-coq-load-hook)

(provide 'inferior-coq)