path: root/isa/isa.el

;; isa.el Major mode for Isabelle proof assistant
;; Copyright (C) 1994-1998 LFCS Edinburgh. 
;;
;; Author:      David Aspinall <da@dcs.ed.ac.uk>
;; Maintainer:  Proof General maintainer <proofgen@dcs.ed.ac.uk>
;;
;; $Id$
;;


(require 'isa-syntax)
(require 'outline)
(require 'proof)


;;;
;;; ======== User settings for Isabelle ========
;;;

(defgroup isabelle-settings nil
  "Customization of Isabelle specifics for Proof General."
  :group 'proof-general)
  
(defcustom isa-prog-name "/usr/lib/Isabelle98/bin/isabelle"
  "*Name of program to run Isabelle."
  :type 'file
  :group 'isabelle-settings)

(defcustom isa-indent 2
  "*Indentation degree in proof scripts.
Somewhat irrelevant for Isabelle because normal proof scripts have
no regular or easily discernable structure."
  :type 'number
  :group 'isabelle-settings)

(defcustom isa-www-home-page
  ;; "http://www.cl.cam.ac.uk/Research/HVG/isabelle.html"
  "http://www.dcs.ed.ac.uk/home/isabelle"
  "URL of web page for Isabelle."
  :type 'string
  :group 'isabelle-settings)
  
  
  

;;;
;;; ======== Configuration of generic modes ========
;;;

;;; NB!  Disadvantage of *not* shadowing variables is that user
;;; cannot override them.  It might be nice to override some
;;; variables, which ones?

(defun isa-mode-config-set-variables
  "Configure generic proof scripting mode variables for Isabelle."
  (setq
   proof-assistant		"Isabelle"
   proof-www-home-page		isa-www-home-page
   ;; proof script syntax
   proof-terminal-char		?\;	; ends a proof
   proof-comment-start		"(*"	; comment in a proof
   proof-comment-end		"*)"	; 
   ;; proof engine output syntax
   proof-save-command-regexp    isa-save-command-regexp
   proof-save-with-hole-regexp  isa-save-with-hole-regexp
   proof-goal-with-hole-regexp  isa-goal-with-hole-regexp
   proof-commands-regexp	(ids-to-regexp isa-keywords)
   ;; proof engine commands (first three for menus, last for undo)
   proof-prf-string		"pr();"
   proof-goal-command		"Goal \"%s\";"
   proof-save-command		"qed \"%s\";"
   proof-ctxt-string		"ProofGeneral.show_context();"
   proof-help-string		"ProofGeneral.help();"
   proof-kill-goal-command	"ProofGeneral.kill_goal();"
   ;; command hooks
   proof-goal-command-p		'isa-goal-command-p
   proof-count-undos-fn		'isa-count-undos
   proof-find-and-forget-fn	'isa-find-and-forget
   proof-goal-hyp-fn		'isa-goal-hyp
   proof-state-preserving-p	'isa-state-preserving-p
   proof-global-p		'isa-global-p    ; FIXME: proof.el should allow nil
   proof-parse-indent		'isa-parse-indent
   proof-stack-to-indent	'isa-stack-to-indent))


(defun isa-shell-mode-config-set-variables
  "Configure generic proof shell mode variables for Isabelle."
  (setq
   proof-shell-prompt-pattern
   "^\\(val it = () : unit\n\\)?2?[-=#>]>? *"
   ;"^[-=#>]>? *"
   ;; This pattern matches a variety of prompts from ML.
   ;; It doesn't match the tracing output prompt.
   ;; Probably it isn't general enough for all MLs, please send me
   ;; problem reports / patches.
   ;; Alternative version to match vacuous assignments:
     
   ;; this doesn't work as intended, probably because the
   ;; process mungling searches backwards and forwards for
   ;; regexps.
   proof-shell-cd			"cd \"%s\";"
   ;; this one not set: proof-shell-abort-goal-regexp 
   proof-shell-proof-completed-regexp   "No subgoals!"
   proof-shell-error-regexp		isa-error-regexp
   proof-shell-interrupt-regexp         "Interrupt"     ; FIXME: only good for NJ/SML
   proof-shell-noise-regexp	        ""
   proof-shell-assumption-regexp	isa-id		   ; matches name of assumptions
   proof-shell-goal-regexp		isa-goal-regexp    ; matches subgoal heading
   ;; We can't hack the SML prompt, so set wakeup-char to nil.
   proof-shell-wakeup-char		nil
   proof-shell-start-goals-regexp	"\370"
   proof-shell-end-goals-regexp		"\371"
   ;; initial command configures Isabelle by hacking print functions.
   ;; may need to set directory somewhere for this:
   ;; /home/da/devel/lego/elisp/   or  $PROOFGENERIC_HOME ?
   proof-shell-init-cmd			(concat
					 "use \"" proof-home
					  "isa/ProofGeneral.ML\";")
   proof-shell-eager-annotation-start   "^\\[opening "
  ;;   proof-shell-eager-annotation-end "$"
   proof-shell-eager-annotation-end     "$"
   ;; === ANNOTATIONS  === ones below here are broken
   proof-shell-goal-char	        ?\375
   proof-shell-first-special-char	?\360
   proof-shell-annotated-prompt-regexp  proof-shell-prompt-pattern
   proof-shell-result-start	        "\372 Pbp result \373"
   proof-shell-result-end		"\372 End Pbp result \373"
   proof-analyse-using-stack		t
   proof-shell-start-char		?\372
   proof-shell-end-char			?\373
   proof-shell-field-char		?\374))


;; ===== outline mode

;;; FIXME: test and add more things here
(defvar isa-outline-regexp
  (ids-to-regexp '("goal" "Goal" "prove_goal"))
  "Outline regexp for Isabelle ML files")

;;; End of a command needs parsing to find, so this is approximate.
(defvar isa-outline-heading-end-regexp ";[ \t\n]*")

(defconst isa-goal-regexp "^[ \t]*[0-9]+\\. "
  "Regexp to match subgoal headings.
Used by proof mode to parse proofstate output, and also
to set outline heading regexp.")
  
;; 
(defvar isa-shell-outline-regexp isa-goal-regexp)
(defvar isa-shell-outline-heading-end-regexp isa-goal-regexp)

;;; ---- end-outline


;;
;;   Define the derived modes 
;;
(define-derived-mode isa-shell-mode proof-shell-mode
   "Isabelle shell" nil
   (isa-shell-mode-config))

(define-derived-mode isa-pbp-mode pbp-mode
  "Isabelle proofstate" nil
  (isa-pbp-mode-config))

(define-derived-mode isa-proofscript-mode proof-mode
   "Isabelle script" nil
   (isa-mode-config))

;; Automatically selecting theory mode or Proof General script mode.

(defun isa-mode ()
  "Mode for Isabelle buffers: either isa-proofscript-mode or isa-thy-mode.
Files with extension .thy will be in isa-thy-mode, otherwise we choose
isa-proofscript-mode."
  (interactive)
  (cond
   ((string-match ".thy" (buffer-file-name))
    (isa-thy-mode))
   (t 
    (isa-proofscript-mode))))

;; Next portion taken from isa-load.el
;; isa-load.el,v 3.8 1998/09/01 

(defcustom isa-use-sml-mode
   (if (fboundp 'sml-mode) 'sml-mode)
  "*If non-nil, attempt to use sml-mode in ML section of theory files."
  :type 'boolean
  :group 'isabelle-settings)

(defgroup isa-thy-mode nil
  "Customization of Isamode's theory editing mode"
  ;; :link '(info-link "(Isamode)Theory Files")
  :load 'isa-thy-mode
  :group 'isabelle-settings)

(autoload 'isa-thy-mode "isa-thy-mode" 
	  "Major mode for Isabelle theory files" t nil)


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;   Code that's Isabelle specific                                  ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


;; FIXME: think about the next variable.  I've changed sense from
;;  LEGO and Coq's treatment.
(defconst isa-not-undoable-commands-regexp
  (ids-to-regexp '("undo" "back"))
  "Regular expression matching commands which are *not* undoable.")

;; This next function is the important one for undo operations.
(defun isa-count-undos (span)
  "Count number of undos in a span, return the command needed to undo that far."
  (let ((ct 0) str i)
    (if (and span (prev-span span 'type)
	     (not (eq (span-property (prev-span span 'type) 'type) 'comment))
	     (isa-goal-command-p
	      (span-property (prev-span span 'type) 'cmd)))
	(concat "choplev 0" proof-terminal-string)
      (while span
	(setq str (span-property span 'cmd))
	(cond ((eq (span-property span 'type) 'vanilla)
	       (or (string-match isa-not-undoable-commands-regexp str)
		   (setq ct (+ 1 ct))))
	      ((eq (span-property span 'type) 'pbp)
	       ;; this case probably redundant for Isabelle, unless
	       ;; we think of some nice ways of matching non-undoable
	       ;; commands.
	       (cond ((not (string-match isa-not-undoable-commands-regexp str))
		      (setq i 0)
		      (while (< i (length str))
			(if (= (aref str i) proof-terminal-char)
			    (setq ct (+ 1 ct)))
			(setq i (+ 1 i))))
		     (t nil))))
	(setq span (next-span span 'type)))
      (concat "choplev " (int-to-string ct) proof-terminal-string))))

(defun isa-goal-command-p (str)
  "Decide whether argument is a goal or not"
  (string-match isa-goal-command-regexp str)) ; this regexp defined in isa-syntax.el

;; Isabelle has no concept of a Linear context, so forgetting back
;; to the declaration of a particular something makes no real
;; sense.  Perhaps in the future there will be functions to remove
;; theorems from theories, but even then all we could do is
;; forget particular theorems one by one.  So we ought to search
;; backwards in isa-find-and-forget, rather than forwards as
;; the old code below does.

(defun isa-find-and-forget (span)
  ;; Special return value to indicate nothing needs to be done.
  proof-no-command)
  
  
;; BEGIN Old code  (taken from Coq.el)
;(defconst isa-keywords-decl-defn-regexp
;  (ids-to-regexp (append isa-keywords-decl isa-keywords-defn))
;  "Declaration and definition regexp.")
;(defun isa-find-and-forget (span)
;  (let (str ans)
;    (while (and span (not ans))
;      (setq str (span-property span 'cmd))
;      (cond
;       ((eq (span-property span 'type) 'comment))       

;       ((eq (span-property span 'type) 'goalsave)
;	(setq ans (concat isa-forget-id-command
;			  (span-property span 'name) proof-terminal-string)))

;       ((string-match (concat "\\`\\(" isa-keywords-decl-defn-regexp
;                              "\\)\\s-*\\(" proof-id "\\)\\s-*[\\[,:]") str)
;	(setq ans (concat isa-forget-id-command
;			  (match-string 2 str) proof-terminal-string)))
;       ;; If it's not a goal but it contains "Definition" then it's a
;       ;; declaration
;       ((and (not (isa-goal-command-p str))
;	     (string-match
;	      (concat "Definition\\s-+\\(" proof-id "\\)\\s-*:") str))
;	(setq ans (concat isa-forget-id-command
;			  (match-string 2 str) proof-terminal-string))))
;      (setq span (next-span span 'type)))
;      (or ans "COMMENT")))
; END old code 

(defvar isa-current-goal 1
  "Last goal that emacs looked at.")

;; Parse proofstate output.  Isabelle does not display
;; named hypotheses in the proofstate output:  they
;; appear as a list in each subgoal.  Ignore
;; that aspect for now and just return the
;; subgoal number.
(defun isa-goal-hyp ()
  (if (looking-at proof-shell-goal-regexp)
      (cons 'goal (match-string 1))))

(defun isa-state-preserving-p (cmd)
  "Non-nil if command preserves the proofstate."
  (string-match isa-not-undoable-commands-regexp cmd))

;; FIXME: I don't really know what this means, but lego sets
;; it to always return nil.  Probably should be able to
;; leave it unset.
(defun isa-global-p (cmd)
  nil)


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;   Indentation                                                    ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;
;; Sadly this is pretty pointless for Isabelle.
;; Proof scripts in Isabelle don't really have an easily-observed
;; block structure  -- a case split can be done by any obscure tactic,
;; and then solved in a number of steps that bears no relation to the
;; number of cases!  And the end is certainly not marked in anyway.
;; 
(defun isa-stack-to-indent (stack)
    (cond
   ((null stack) 0)
   ((null (car (car stack)))
    (nth 1 (car stack)))
   (t (save-excursion
	(goto-char (nth 1 (car stack)))
	(+ isa-indent (current-column))))))

(defun isa-parse-indent (c stack)
  "Indentation function for Isabelle.  Does nothing."
  stack)


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;   Isa shell startup and exit hooks                               ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defun isa-pre-shell-start ()
  (setq proof-prog-name		isa-prog-name)
  (setq proof-mode-for-shell    'isa-shell-mode)
  (setq proof-mode-for-pbp	'isa-pbp-mode))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;   Configuring proof and pbp mode and setting up various utilities  ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defun isa-init-syntax-table ()
  "Set appropriate values for syntax table in current buffer."
  (modify-syntax-entry ?\$ ".")
  (modify-syntax-entry ?\/ ".")
  (modify-syntax-entry ?\\ ".")
  (modify-syntax-entry ?+  ".")
  (modify-syntax-entry ?-  ".")
  (modify-syntax-entry ?=  ".")
  (modify-syntax-entry ?%  ".")
  (modify-syntax-entry ?<  ".")
  (modify-syntax-entry ?>  ".")
  (modify-syntax-entry ?\& ".")
  (modify-syntax-entry ?_  "_")
  (modify-syntax-entry ?\' "_")
  (modify-syntax-entry ?\| ".")
  (modify-syntax-entry ?\* ". 23")
  (modify-syntax-entry ?\( "()1")
  (modify-syntax-entry ?\) ")(4"))

(defun isa-mode-config ()
  (isa-mode-config-set-variables)
  (isa-init-syntax-table)
  ;; font-lock
  (setq font-lock-keywords isa-font-lock-keywords-1)
  (proof-config-done)
  (define-key (current-local-map) [(control c) ?I] 'isa-Intros)
  (define-key (current-local-map) [(control c) ?a] 'isa-Apply)
  (define-key (current-local-map) [(control c) (control s)] 'isa-Search)
  ;; outline
  ;; FIXME: do we need to call make-local-variable here?
  (make-local-variable 'outline-regexp)
  (setq outline-regexp isa-outline-regexp)
  (make-local-variable 'outline-heading-end-regexp)
  (setq outline-heading-end-regexp isa-outline-heading-end-regexp)
  ;; tags
  ;  (and (boundp 'tag-table-alist)
  ;       (setq tag-table-alist
  ;	     (append '(("\\.ML$"  . isa-ML-file-tags-table)
  ;		       ("\\.thy$" . isa-thy-file-tags-table))
  ;		     tag-table-alist)))
  (setq blink-matching-paren-dont-ignore-comments t)
  ;; hooks and callbacks
  (add-hook 'proof-pre-shell-start-hook 'isa-pre-shell-start nil t))


(defun isa-shell-mode-config ()
  ;; The following hook is removed once it's called.
  ;; FIXME: maybe add this back later.
  ;;(add-hook 'proof-shell-insert-hook 'isa-shell-init-hook nil t)
  (isa-init-syntax-table)
  (isa-shell-mode-config-set-variables)
  (proof-shell-config-done))

;; FIXME: broken, of course, as is all PBP everywhere.
(defun isa-pbp-mode-config ()
  (setq pbp-change-goal "Show %s.")
  (setq pbp-error-regexp isa-error-regexp))

(provide 'isa)