diff options
| -rw-r--r-- | INSTALL | 56 | ||||
| -rw-r--r-- | Makefile.devel | 20 | ||||
| -rw-r--r-- | coq-syntax.el | 275 | ||||
| -rw-r--r-- | coq.el | 535 | ||||
| -rw-r--r-- | coqtags | 56 | ||||
| -rw-r--r-- | isa-print-functions.ML | 172 | ||||
| -rw-r--r-- | isa-syntax.el | 112 | ||||
| -rw-r--r-- | isa.el | 434 | ||||
| -rw-r--r-- | lego-syntax.el | 100 | ||||
| -rw-r--r-- | lego.el | 469 | ||||
| -rw-r--r-- | legotags | 87 | ||||
| -rw-r--r-- | pbp.el | 2 | ||||
| -rw-r--r-- | proof-indent.el | 124 | ||||
| -rw-r--r-- | proof-syntax.el | 146 | ||||
| -rw-r--r-- | proof.el | 1818 | ||||
| -rw-r--r-- | script-management.texinfo | 440 | ||||
| -rw-r--r-- | span-extent.el | 79 | ||||
| -rw-r--r-- | span-overlay.el | 288 | ||||
| -rw-r--r-- | todo | 175 |
19 files changed, 5388 insertions, 0 deletions
diff --git a/INSTALL b/INSTALL new file mode 100644 index 00000000..d3ad3e70 --- /dev/null +++ b/INSTALL @@ -0,0 +1,56 @@ +This file describes what to do to be able to run our script management +mode for xemacs. Please let us know if you have any problems in +trying to install it. + +Check the values of coq-tags and coq-prog-name in coq.el to see that +they correspond to the paths for coqtop and the library on your system. + +To install, begin by making sure that your load-path has the current +directory in it by typing: + load-path C-j +in the *scratch* buffer. If it does not, type: + (setq load-path (cons "." load-path)) C-j +again in the *scratch* buffer (or add it to your .emacs file). + +Then put the .el files in an appropriate directory and compile them +using `byte-recompile-file' in xemacs: + M-0 M-x byte-recompile-directory + +Put the compiled emacs files and the file script-management.info in a +suitable directory for local emacs files, as suggested by your system +administrator. Otherwise, if you prefer to keep your own private +copy, alter the variable coq-info-dir in coq.el to that directory and +add the line: + (setq load-path (cons <directory> load-path)) +to your .emacs file, where <directory> is your local directory. + +If you want to use this mode for Coq, you need to make sure you have +an appropriate version, which is from later than 1 March 1998. + +Install coqtags or legotags in a standard place. + +If you are running Coq, generate a TAGS file for the library by running + coqtags `find . -name \*.v -print` +in the root directory of the library, $COQTOP/theories. If you are +running LEGO, do the same using legotags in the appropriate directory. + +Finally, you should add the following lines to your .emacs file. + +;;; LEGO and Coq +(setq auto-mode-alist + (cons '("\\.v" . coq-mode) + (cons '("\\.l$" . lego-mode) auto-mode-alist))) + +(autoload 'coq-mode "coq" + "Major mode for editing Coq vernacular." t) + +(autoload 'lego-mode "lego" + "Major mode for editing Lego proof scripts." t) + +; Tags is unusable with Coq library otherwise: +(setq tag-always-exact t) + +After this, simply load a LEGO or Coq file and the appropriate mode +will be run automatically. + +Healfdene GOGUEN diff --git a/Makefile.devel b/Makefile.devel new file mode 100644 index 00000000..4cda4a31 --- /dev/null +++ b/Makefile.devel @@ -0,0 +1,20 @@ +CVSROOT = /home/lego/src +EXPORTDIR = /home/lego/pub/emacs +RELEASENAME = emacs-2.0 +TRELEASENAME = $(RELEASENAME).tar + +release : + cd /tmp; \ + rm -fr lego;\ + mkdir lego;\ + cd lego;\ + cvs -d $(CVSROOT) export -D today elisp;\ + cd elisp; \ + tar cf $(TRELEASENAME) *;\ + compress -c $(TRELEASENAME) > $(TRELEASENAME).Z;\ + gzip -c $(TRELEASENAME) > $(TRELEASENAME).gz;\ + cp -p $(RELEASENAME).* $(EXPORTDIR);\ + cd ..; cvs release -d elisp + + + diff --git a/coq-syntax.el b/coq-syntax.el new file mode 100644 index 00000000..b81a93e8 --- /dev/null +++ b/coq-syntax.el @@ -0,0 +1,275 @@ +;; coq-syntax.el Font lock expressions for Coq +;; Copyright (C) 1997, 1998 LFCS Edinburgh. +;; Author: Thomas Kleymann and Healfdene Goguen +;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> + +;; $Log$ +;; Revision 2.0 1998/08/11 14:59:53 da +;; New branch +;; +;; Revision 1.2 1998/08/11 11:43:13 da +;; Renamed <file>-fontlock to <file>-syntax +;; +;; Revision 1.14 1998/06/11 12:20:14 hhg +;; Added "Scheme" as definition keyword. +;; +;; Revision 1.13 1998/06/10 11:38:04 hhg +;; Added "Mutual Inductive" as definition keyword. +;; Changed "\\s " into "\\s-" as whitespace pattern. +;; +;; Revision 1.12 1998/06/03 18:01:54 hhg +;; Changed Compute from command to tactic. +;; Added Fix, Destruct and Cofix as tactics. +;; Added Local as goal. +;; +;; Revision 1.11 1998/06/02 15:33:16 hhg +;; Minor modifications to comments +;; +;; Revision 1.10 1998/05/15 16:13:23 hhg +;; Added CoFixpoint and tactics. +;; Changed indentation. +;; +;; Revision 1.9 1998/05/05 14:19:39 hhg +;; Added CoInductive. +;; Made updates to reflect problem with "Definition", which couldn't be +;; used with proof scripts. +;; +;; Revision 1.8 1998/01/15 13:30:17 hhg +;; Added coq-shell-cd +;; Some new fontlocks +;; +;; Revision 1.7 1997/11/26 17:12:55 hhg +;; Incorporated tms's suggestion for simplifying coq-font-lock-keywords-1 +;; +;; Revision 1.6 1997/11/06 16:46:20 hhg +;; Updates to Coq fontlock tables +;; +;; Revision 1.5 1997/10/30 15:58:29 hhg +;; Updates for coq, including: +;; * pbp-goal-command and pbp-hyp-command use proof-terminal-string +;; * updates to keywords +;; * fix for goal regexp +;; +;; Revision 1.4 1997/10/24 14:51:07 hhg +;; Changed order of "Inversion_clear" and "Inversion" so that former is +;; fontified first. +;; Added "Print" to list of commands. +;; +;; Revision 1.3 1997/10/17 14:45:53 hhg +;; Added "Induction" as tactic +;; +;; Revision 1.2 1997/10/13 17:10:29 tms +;; *** empty log message *** +;; +;; Revision 1.1.2.2 1997/10/08 08:22:28 hhg +;; Updated undo, fixed bugs, more modularization +;; +;; Revision 1.1.2.1 1997/10/07 13:34:10 hhg +;; New structure to share as much as possible between LEGO and Coq. +;; +;; + +(require 'proof-syntax) + +;; ----- keywords for font-lock. + +(defvar coq-keywords-decl + '( +"Axiom" +"Hypothesis" +"Parameter" +"Variable" +)) + +(defvar coq-keywords-defn + '( +"CoFixpoint" +"CoInductive" +"Fixpoint" +"Inductive" +"Mutual\\s-+Inductive" +"Scheme" +)) + +(defvar coq-keywords-goal + '( +"Definition" +"Fact" +"Goal" +"Lemma" +"Local" +"Remark" +"Theorem" +)) + +(defvar coq-keywords-save + '( +"Defined" +"Save" +"Qed" +)) + +(defvar coq-keywords-kill-goal '( +"Abort" +)) + +(defvar coq-keywords-commands + '( +"AddPath" +"Cd" +"Check" +"Class" +"Coercion" +"DelPath" +"Eval" +"Extraction" +"Focus" +"Immediate" +"Hint" +"Infix" +"Opaque" +"Print" +"Proof" +"Pwd" +"Reset" +"Search" +"Show" +"Transparent" +)) + +(defvar coq-tactics + '( +"Absurd" +"Apply" +"Assumption" +"Auto" +"Case" +"Change" +"Clear" +"Cofix" +"Compute" +"Constructor" +"Contradiction" +"Cut" +"DHyp" +"DInd" +"Dependent" +"Destruct" +"Discriminate" +"Double" +"EApply" +"EAuto" +"Elim" +"End" +"Exact" +"Exists" +"Fix" +"Generalize" +"Grammar" +"Hnf" +"Induction" +"Injection" +"Intro" +"Intros" +"Intuition" +"Inversion_clear" +"Inversion" +"LApply" +"Left" +"Linear" +"Load" +"Pattern" +"Program_all" +"Program" +"Prolog" +"Realizer" +"Red" +"Reflexivity" +"Replace" +"Rewrite" +"Right" +"Section" +"Simplify_eq" +"Simpl" +"Specialize" +"Split" +"Symmetry" +"Syntax" +"Tauto" +"Transitivity" +"Trivial" +"Unfold" +)) + +(defvar coq-keywords + (append coq-keywords-goal coq-keywords-save coq-keywords-decl + coq-keywords-defn coq-keywords-commands coq-tactics) + "All keywords in a Coq script") + +(defvar coq-tacticals '( +"Do" +"Idtac" +"OrElse" +"Repeat" +"Try" +)) + +;; ----- regular expressions +(defvar coq-error-regexp "^\\(Error\\|Discarding\\|Syntax error\\|System Error\\)" + "A regular expression indicating that the Coq process has identified + an error.") + +(defvar coq-id proof-id) + +(defvar coq-ids (proof-ids coq-id)) + +(defun coq-abstr-regexp (paren char) + (concat paren "\\s-*\\(" coq-ids "\\)\\s-*" char)) + +(defvar coq-font-lock-terms + (list + + ;; lambda binders + (list (coq-abstr-regexp "\\[" ":") 1 'font-lock-declaration-name-face) + + ;; Pi binders + (list (coq-abstr-regexp "(" ":") 1 'font-lock-declaration-name-face) + + ;; Kinds + (cons (concat "\\<Prop\\>\\|\\<Set\\>\\|\\<Type\\s-*\\((" + coq-id ")\\)?") 'font-lock-type-face)) + "*Font-lock table for Coq terms.") + +;; According to Coq, "Definition" is both a declaration and a goal. +;; It is understood here as being a goal. This is important for +;; recognizing global identifiers, see coq-global-p. +(defconst coq-save-command-regexp + (concat "^" (ids-to-regexp coq-keywords-save))) +(defconst coq-save-with-hole-regexp + (concat "\\(" (ids-to-regexp coq-keywords-save) + "\\)\\s-+\\(" coq-id "\\)\\s-*\.")) +(defconst coq-goal-command-regexp + (concat "^" (ids-to-regexp coq-keywords-goal))) +(defconst coq-goal-with-hole-regexp + (concat "\\(" (ids-to-regexp coq-keywords-goal) + "\\)\\s-+\\(" coq-id "\\)\\s-*:")) +(defconst coq-decl-with-hole-regexp + (concat "\\(" (ids-to-regexp coq-keywords-decl) + "\\)\\s-+\\(" coq-ids "\\)\\s-*:")) +(defconst coq-defn-with-hole-regexp + (concat "\\(" (ids-to-regexp coq-keywords-defn) + "\\)\\s-+\\(" coq-id "\\)\\s-*[:[]")) + +(defvar coq-font-lock-keywords-1 + (append + coq-font-lock-terms + (list + (cons (ids-to-regexp coq-keywords) 'font-lock-keyword-face) + (cons (ids-to-regexp coq-tacticals) 'font-lock-tacticals-name-face) + + (list coq-goal-with-hole-regexp 2 'font-lock-function-name-face) + (list coq-decl-with-hole-regexp 2 'font-lock-declaration-name-face) + (list coq-defn-with-hole-regexp 2 'font-lock-function-name-face) + (list coq-save-with-hole-regexp 2 'font-lock-function-name-face)))) + +(provide 'coq-syntax) @@ -0,0 +1,535 @@ +;; coq.el Major mode for Coq proof assistant +;; Copyright (C) 1994, 1995, 1996, 1997 LFCS Edinburgh. +;; Author: Healfdene Goguen and Thomas Kleymann + +;; $Log$ +;; Revision 2.0 1998/08/11 11:39:20 da +;; Renamed <file>-fontlock to <file>-syntax +;; +;; Revision 1.29 1998/06/10 11:42:06 hhg +;; Added coq-init-syntax-table as function to initialize syntax entries +;; particular to coq. +;; Changed proof-ctxt-string to "Print All". +;; Call coq-init-syntax-table from coq-shell-mode-config. This was +;; necessary to get prompts with "'"s in them (coming from goals with +;; same) recognized. +;; +;; Revision 1.28 1998/06/03 18:02:54 hhg +;; Added '?'s before single characters in define-keys for emacs19, at +;; Pascal Brisset's suggestion. +;; +;; Revision 1.27 1998/06/03 13:57:10 hhg +;; Added definition of proof-commands-regexp for coq +;; +;; Revision 1.26 1998/06/02 15:34:43 hhg +;; Generalized proof-retract-target, now parameterized by +;; proof-count-undos and proof-find-and-forget. +;; Generalized proof-shell-analyse-structure, introduced variable +;; proof-analyse-using-stack. +;; Generalized proof menu plus ancillary functions. +;; Generalized proof-mode-version-string. +;; Moved various comments into documentation string. +;; +;; Revision 1.25 1998/05/23 12:50:40 tms +;; improved support for Info +;; o employed `Info-default-directory-list' rather than +;; `Info-directory-list' so that code also works for Emacs 19.34 +;; o setting of `Info-default-directory-list' now at proof level +;; +;; Revision 1.24 1998/05/22 11:31:33 hhg +;; Correct path for coq-prog-name and coq-tags. +;; +;; Revision 1.23 1998/05/15 16:16:55 hhg +;; Changed variable names [s]ext to span. +;; Fixed coq-find-and-forget pattern for declarations and definitions +;; following Pascal Brisset's suggestion. +;; +;; Revision 1.22 1998/05/14 11:52:32 hhg +;; Changes to indentation code: +;; Changed "case" to "Case". +;; Added "CoInductive". +;; +;; Revision 1.21 1998/05/12 14:51:27 hhg +;; Added hook `coq-shell-init-hook', for `proof-shell-insert-hook'. +;; This initializes undo limit and changes directory to that associated +;; with buffer. +;; This is because Coq has a command line option to run with emacs mode. +;; +;; Revision 1.20 1998/05/08 17:08:31 hhg +;; Made separated indentation more elegant. +;; Fixed bug with Inductive. +;; Added CoInductive. +;; +;; Revision 1.19 1998/05/08 15:42:42 hhg +;; Merged indentation code for LEGO and Coq into proof.el. +;; +;; Revision 1.18 1998/05/06 16:39:10 hhg +;; Removed default instantiation of undo limit to 100. +;; +;; Revision 1.17 1998/05/06 15:29:11 hhg +;; Added coq-info-dir so that script-management.info can be hard-coded. +;; +;; Revision 1.16 1998/05/05 14:21:48 hhg +;; Made updates to fix problem with Definition, which couldn't be +;; used with proof scripts. +;; Removed some useless declarations. +;; Removed Abort from menu. +;; Now Reset's if user undoes to beginning of proof. +;; Added command to increase undo limit for Coq, and set default to 100. +;; +;; Revision 1.15 1998/03/25 17:30:35 tms +;; added support for etags at generic proof level +;; +;; Revision 1.14 1998/01/15 13:30:18 hhg +;; Added coq-shell-cd +;; Some new fontlocks +;; +;; Revision 1.13 1997/11/26 17:23:51 hhg +;; Added C-c C-s to run "Search" in Coq. +;; Moved coq-goal-with-hole-regexp etc to coq-fontlock. +;; Removed various superfluous definitions for COQPATH etc. +;; +;; Revision 1.12 1997/11/24 19:15:08 djs +;; Added proof-execute-minibuffer-cmd and scripting minor mode. +;; +;; Revision 1.11 1997/11/20 13:03:08 hhg +;; Added coq-global-p for global declarations and definitions. These now +;; get lifted in the same way as lemmas. +;; Changed [meta (control i)] to [meta tab] in key definition. +;; Changed menu, and made help in menu refer to info mode. +;; +;; Revision 1.10 1997/11/17 17:11:15 djs +;; Added some magic commands: proof-frob-locked-end, proof-try-command, +;; proof-interrupt-process. Added moving nested lemmas above goal for coq. +;; Changed the key mapping for assert-until-point to C-c RET. +;; +;; Revision 1.9 1997/11/12 15:56:15 hhg +;; Changed pbp-change-goal so that it only "Show"s the goal pointed at. +;; +;; Revision 1.8 1997/11/06 16:55:49 hhg +;; Assign new variable proof-goal-hyp-fn to coq-goal-hyp, which advances +;; over coq-goal-regexp to pick up goal for pbp +;; +;; Revision 1.7 1997/10/30 15:58:31 hhg +;; Updates for coq, including: +;; * pbp-goal-command and pbp-hyp-command use proof-terminal-string +;; * updates to keywords +;; * fix for goal regexp +;; +;; Revision 1.6 1997/10/24 14:51:09 hhg +;; Fixed coq-count-undos for comments +;; +;; Revision 1.5 1997/10/17 14:51:48 hhg +;; Fixed coq-shell-prompt-pattern to reflect proof-id +;; Changed ";" to "." in coq-save-with-hole-regexp +;; New modifications to syntax table to reflect actual use of symbols in Coq +;; +;; Revision 1.4 1997/10/16 13:14:32 djs +;; Merged Coq changes with main branch. +;; +;; Revision 1.2 1997/10/13 17:12:48 tms +;; *** empty log message *** +;; +;; Revision 1.1.2.3 1997/10/10 19:19:58 djs +;; Added multiple file support, changed the way comments work, fixed a +;; few minor bugs, and merged in coq support by hhg. +;; +;; Revision 1.1.2.2 1997/10/08 08:22:30 hhg +;; Updated undo, fixed bugs, more modularization +;; +;; Revision 1.1.2.1 1997/10/07 13:34:16 hhg +;; New structure to share as much as possible between LEGO and Coq. +;; + +(require 'coq-syntax) +(require 'outline) +(require 'proof) +(require 'info) + +; Configuration + +(defvar coq-assistant "Coq" + "Name of proof assistant") + +(defvar coq-tags "/usr/local/lib/coq/theories/TAGS" + "the default TAGS table for the Coq library") + +(defconst coq-process-config nil + "Command to configure pretty printing of the Coq process for emacs.") + +(defconst coq-interrupt-regexp "Interrupted" + "Regexp corresponding to an interrupt") + +(defvar coq-save-query t + "*If non-nil, ask user for permission to save the current buffer before + processing a module.") + +(defvar coq-default-undo-limit 100 + "Maximum number of Undo's possible when doing a proof.") + +;; ----- web documentation + +(defvar coq-www-home-page "http://pauillac.inria.fr/coq/") + +;; ----- coq-shell configuration options + +(defvar coq-prog-name "coqtop -emacs" + "*Name of program to run as Coq.") + +(defvar coq-shell-working-dir "" + "The working directory of the coq shell") + +(defvar coq-shell-prompt-pattern (concat "^" proof-id " < ") + "*The prompt pattern for the inferior shell running coq.") + +(defvar coq-shell-cd nil ; "Cd \"%s\"." + "*Command of the inferior process to change the directory.") + +(defvar coq-shell-abort-goal-regexp "Current goal aborted" + "*Regular expression indicating that the proof of the current goal + has been abandoned.") + +(defvar coq-shell-proof-completed-regexp "Subtree proved!" + "*Regular expression indicating that the proof has been completed.") + +(defvar coq-goal-regexp + "\\(============================\\)\\|\\(subgoal [0-9]+ is:\\)\n") + +;; ----- outline + +(defvar coq-outline-regexp + (ids-to-regexp + '("Section" "Chapter" "Goal" "Lemma" "Theorem" "Fact" + "Remark" "Record" "Inductive" "Definition"))) + +(defvar coq-outline-heading-end-regexp "\.\\|\\*)") + +(defvar coq-shell-outline-regexp coq-goal-regexp) +(defvar coq-shell-outline-heading-end-regexp coq-goal-regexp) + +(defconst coq-kill-goal-command "Abort.") +(defconst coq-forget-id-command "Reset ") + +(defconst coq-undoable-commands-regexp (ids-to-regexp coq-tactics)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Derived modes - they're here 'cos they define keymaps 'n stuff ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(define-derived-mode coq-shell-mode proof-shell-mode + "coq-shell" "Inferior shell mode for coq shell" + (coq-shell-mode-config)) + +(define-derived-mode coq-mode proof-mode + "coq" "Coq Mode" + (coq-mode-config)) + +(define-derived-mode coq-pbp-mode pbp-mode + "pbp" "Proof-by-pointing support for Coq" + (coq-pbp-mode-config)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Code that's coq specific ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun coq-shell-init-hook () + (insert (format "Set Undo %s." coq-default-undo-limit)) + (insert (format "Cd \"%s\"." default-directory)) + (remove-hook 'proof-shell-insert-hook 'coq-shell-init-hook)) + +(defun coq-set-undo-limit (undos) + (proof-invisible-command (format "Set Undo %s." undos))) + +(defun coq-count-undos (span) + (let ((ct 0) str i) + (if (and span (prev-span span 'type) + (not (eq (span-property (prev-span span 'type) 'type) 'comment)) + (coq-goal-command-p + (span-property (prev-span span 'type) 'cmd))) + (concat "Restart" proof-terminal-string) + (while span + (setq str (span-property span 'cmd)) + (cond ((eq (span-property span 'type) 'vanilla) + (if (string-match coq-undoable-commands-regexp str) + (setq ct (+ 1 ct)))) + ((eq (span-property span 'type) 'pbp) + (cond ((string-match coq-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 "Undo " (int-to-string ct) proof-terminal-string)))) + +(defconst coq-keywords-decl-defn-regexp + (ids-to-regexp (append coq-keywords-decl coq-keywords-defn)) + "Declaration and definition regexp.") + +(defun coq-goal-command-p (str) + "Decide whether argument is a goal or not" + (and (string-match coq-goal-command-regexp str) + (not (string-match "Definition.*:=" str)))) + +(defun coq-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 coq-forget-id-command + (span-property span 'name) proof-terminal-string))) + + ((string-match (concat "\\`\\(" coq-keywords-decl-defn-regexp + "\\)\\s-*\\(" proof-id "\\)\\s-*[\\[,:]") str) + (setq ans (concat coq-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 (coq-goal-command-p str)) + (string-match + (concat "Definition\\s-+\\(" proof-id "\\)\\s-*:") str)) + (setq ans (concat coq-forget-id-command + (match-string 2 str) proof-terminal-string)))) + + (setq span (next-span span 'type))) + + (or ans "COMMENT"))) + +(defvar coq-current-goal 1 + "Last goal that emacs looked at.") + +(defun coq-goal-hyp () + (cond + ((looking-at "============================\n") + (goto-char (match-end 0)) + (cons 'goal (int-to-string coq-current-goal))) + ((looking-at "subgoal \\([0-9]+\\) is:\n") + (goto-char (match-end 0)) + (cons 'goal (match-string 1)) + (setq coq-current-goal (string-to-int (match-string 1)))) + ((looking-at proof-shell-assumption-regexp) + (cons 'hyp (match-string 1))) + (t nil))) + +(defun coq-state-preserving-p (cmd) + (not (string-match coq-undoable-commands-regexp cmd))) + +(defun coq-global-p (cmd) + (or (string-match coq-keywords-decl-defn-regexp cmd) + (and (string-match + (concat "Definition\\s-+\\(" coq-id "\\)\\s-*:") cmd) + (string-match ":=" cmd)))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Commands specific to coq ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun coq-Intros () + "List proof state." + (interactive) + (insert "Intros ")) + +(defun coq-Apply () + "List proof state." + (interactive) + (insert "Apply ")) + +(defun coq-Search () + "Search for type in goals." + (interactive) + (let (cmd) + (proof-check-process-available) + (setq cmd (read-string "Search Type: " nil 'proof-minibuffer-history)) + (proof-invisible-command (concat "Search " cmd proof-terminal-string)))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Indentation ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; "Case" is represented by 'c' on the stack, and +;; "CoInductive is represented by 'C'. +(defun coq-stack-to-indent (stack) + (cond + ((null stack) 0) + ((null (car (car stack))) + (nth 1 (car stack))) + (t (let ((col (save-excursion + (goto-char (nth 1 (car stack))) + (current-column)))) + (cond + ((eq (car (car stack)) ?c) + (save-excursion (move-to-column (current-indentation)) + (cond + ((eq (char-after (point)) ?|) (+ col 3)) + ((looking-at "end") col) + (t (+ col 5))))) + ((or (eq (car (car stack)) ?I) (eq (car (car stack)) ?C)) + (+ col (if (eq ?| (save-excursion + (move-to-column (current-indentation)) + (char-after (point)))) 2 4))) + (t (1+ col))))))) + +(defun coq-parse-indent (c stack) + (cond + ((eq c ?C) + (cond ((looking-at "Case") + (cons (list ?c (point)) stack)) + ((looking-at "CoInductive") + (forward-char (length "CoInductive")) + (cons (list c (- (point) (length "CoInductive"))) stack)) + (t stack))) + ((and (eq c ?e) (looking-at "end") (eq (car (car stack)) ?c)) + (cdr stack)) + + ((and (eq c ?I) (looking-at "Inductive")) + (forward-char (length "Inductive")) + (cons (list c (- (point) (length "Inductive"))) stack)) + + ((and (eq c ?.) (or (eq (car (car stack)) ?I) (eq (car (car stack)) ?C))) + (cdr stack)) + + (t stack))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Coq shell startup and exit hooks ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun coq-pre-shell-start () + (setq proof-prog-name coq-prog-name) + (setq proof-mode-for-shell 'coq-shell-mode) + (setq proof-mode-for-pbp 'coq-pbp-mode) +) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Configuring proof and pbp mode and setting up various utilities ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun coq-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 coq-mode-config () + + (setq proof-terminal-char ?\.) + (setq proof-comment-start "(*") + (setq proof-comment-end "*)") + + (setq proof-assistant coq-assistant + proof-www-home-page coq-www-home-page) + + (setq proof-prf-string "Show" + proof-ctxt-string "Print All" + proof-help-string "Help") + + (setq proof-goal-command-p 'coq-goal-command-p + proof-count-undos-fn 'coq-count-undos + proof-find-and-forget-fn 'coq-find-and-forget + proof-goal-hyp-fn 'coq-goal-hyp + proof-state-preserving-p 'coq-state-preserving-p + proof-global-p 'coq-global-p + proof-parse-indent 'coq-parse-indent + proof-stack-to-indent 'coq-stack-to-indent) + + (setq proof-save-command-regexp coq-save-command-regexp + proof-save-with-hole-regexp coq-save-with-hole-regexp + proof-goal-with-hole-regexp coq-goal-with-hole-regexp + proof-kill-goal-command coq-kill-goal-command + proof-commands-regexp (ids-to-regexp coq-keywords)) + + (coq-init-syntax-table) + +;; font-lock + + (setq font-lock-keywords coq-font-lock-keywords-1) + + (proof-config-done) + + (define-key (current-local-map) [(control c) ?I] 'coq-Intros) + (define-key (current-local-map) [(control c) ?a] 'coq-Apply) + (define-key (current-local-map) [(control c) (control s)] 'coq-Search) + +;; outline + + (make-local-variable 'outline-regexp) + (setq outline-regexp coq-outline-regexp) + + (make-local-variable 'outline-heading-end-regexp) + (setq outline-heading-end-regexp coq-outline-heading-end-regexp) + +;; tags + (and (boundp 'tag-table-alist) + (setq tag-table-alist + (append '(("\\.v$" . coq-tags) + ("coq" . coq-tags)) + tag-table-alist))) + + (setq blink-matching-paren-dont-ignore-comments t) + +;; hooks and callbacks + + (add-hook 'proof-shell-exit-hook 'coq-zap-line-width nil t) + (add-hook 'proof-pre-shell-start-hook 'coq-pre-shell-start nil t)) + +(defun coq-shell-mode-config () + (setq proof-shell-prompt-pattern coq-shell-prompt-pattern + proof-shell-cd coq-shell-cd + proof-shell-abort-goal-regexp coq-shell-abort-goal-regexp + proof-shell-proof-completed-regexp coq-shell-proof-completed-regexp + proof-shell-error-regexp coq-error-regexp + proof-shell-interrupt-regexp coq-interrupt-regexp + proof-shell-noise-regexp "" + proof-shell-assumption-regexp coq-id + proof-shell-goal-regexp coq-goal-regexp + proof-shell-first-special-char ?\360 + proof-shell-wakeup-char ?\371 ; done: prompt + ; The next three represent path annotation information + proof-shell-start-char ?\372 ; not done + proof-shell-end-char ?\373 ; not done + proof-shell-field-char ?\374 ; not done + proof-shell-goal-char ?\375 ; done + proof-shell-eager-annotation-start "\376" ; done + proof-shell-eager-annotation-end "\377" ; done + proof-shell-annotated-prompt-regexp + (concat proof-shell-prompt-pattern + (char-to-string proof-shell-wakeup-char)) ; done + proof-shell-result-start "\372 Pbp result \373" + proof-shell-result-end "\372 End Pbp result \373" + proof-shell-start-goals-regexp "[0-9]+ subgoals?" + proof-shell-end-goals-regexp proof-shell-annotated-prompt-regexp + proof-shell-init-cmd nil + proof-analyse-using-stack t) + + ;; The following hook is removed once it's called. + (add-hook 'proof-shell-insert-hook 'coq-shell-init-hook nil t) + + (coq-init-syntax-table) + + (proof-shell-config-done)) + +(defun coq-pbp-mode-config () + (setq pbp-change-goal "Show %s.") + (setq pbp-error-regexp coq-error-regexp)) + +(provide 'coq) diff --git a/coqtags b/coqtags new file mode 100644 index 00000000..b6c72c78 --- /dev/null +++ b/coqtags @@ -0,0 +1,56 @@ +#!/usr/local/bin/perl4 +$/=0777; + +if($#ARGV<$[) {die "No Files\n";} +open(tagfile,">TAGS") || die "Couldn't open TAGS: $!\n"; + +while(<>) +{ + print "Tagging $ARGV\n"; + $a=$_; + $cp=1; + $lp=1; + $tagstring=""; + + while(1) + { + +# ---- Get the next statement starting on a newline ---- + + if($a=~/^[ \t\n]*\(\*/) + { while($a=~/^\s*\(\*/) + { $d=1; $a=$'; $cp+=length $&; $lp+=($&=~tr/\n/\n/); + while($d>0 && $a=~/\(\*|\*\)/) + { $a=$'; $cp+=2+length $`; $lp+=($`=~tr/\n/\n/); + if($& eq "(*") {$d++} else {$d--}; + } + if($d!=0) {die "Unbalanced Comment?";} + } + } + + if($cp>1 && $a=~/.*\n/) {$a=$'; $cp+=length $&; $lp++;} + while($a=~/^\n/) {$cp++;$lp++;$a=$'} + + if($a=~/^[^\.]*\./) + { $stmt=$&; $newa=$'; $newcp=$cp+length $&; $newlp=$lp+($&=~tr/\n/\n/); } + else { last;} + +# ---- The above embarrasses itself if there are semicolons inside comments +# ---- inside commands. Could do better. + +# print "----- (",$lp,",",$cp,")\n", $stmt, "\n"; + + if($stmt=~/^([ \t]*((Fact)|(Goal)|(Lemma)|(Remark)|(Theorem))\s+([\w\']+))\s*:/) + { $tagstring.=$1."\177".$8."\001".$lp.",".$cp."\n"; } + + elsif($stmt=~/^([ \t]*((Axiom)|(Hypothesis)|(Parameter)|(Variable))\s+([\w\']+))\s*:/) + { $tagstring.=$1."\177".$7."\001".$lp.",".$cp."\n"; } + + elsif($stmt=~/^([ \t]*((Definition)|(Fixpoint)|(Inductive))\s+([\w\']+))\s*[:[]/) + { $tagstring.=$1."\177".$6."\001".$lp.",".$cp."\n"; } + + $cp=$newcp; $lp=$newlp; $a=$newa; + } + print tagfile "\f\n".$ARGV.",".(length $tagstring)."\n".$tagstring; +} +close tagfile; diff --git a/isa-print-functions.ML b/isa-print-functions.ML new file mode 100644 index 00000000..3af539a5 --- /dev/null +++ b/isa-print-functions.ML @@ -0,0 +1,172 @@ +(* + isa-print-functions.ML + + Customized version of Isabelle printing for script management + mode. + + $Id$ + +*) + + + +val proof_state_special_prefix="\248"; +val proof_state_special_suffix="\249"; +val goal_start_special="\253"; + + + +(* val orig_prs_fn = !prs_fn; *) +(* val orig_warning_fn = !warning_fn; *) +(* val orig_error_fn = !error_fn; *) + +(* copied from Pure/library.ML: *) +local + fun out s = + (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut); + + fun prefix_lines prfx txt = + txt |> split_lines |> map (fn s => prfx ^ s ^ "\n") |> implode; +in + +(*hooks for output channels: normal, warning, error*) + +(* da: NO CHANGES NEEDED YET *) +val () = + (prs_fn := (fn s => out s); + warning_fn := (fn s => out (prefix_lines "### " s)); + error_fn := (fn s => out (prefix_lines "*** " s))) + +end; + + + +local + + (* utils *) + + fun ins_entry (x, y) [] = [(x, [y])] + | ins_entry (x, y) ((pair as (x', ys')) :: pairs) = + if x = x' then (x', y ins ys') :: pairs + else pair :: ins_entry (x, y) pairs; + + fun add_consts (Const (c, T), env) = ins_entry (T, (c, T)) env + | add_consts (t $ u, env) = add_consts (u, add_consts (t, env)) + | add_consts (Abs (_, _, t), env) = add_consts (t, env) + | add_consts (_, env) = env; + + fun add_vars (Free (x, T), env) = ins_entry (T, (x, ~1)) env + | add_vars (Var (xi, T), env) = ins_entry (T, xi) env + | add_vars (Abs (_, _, t), env) = add_vars (t, env) + | add_vars (t $ u, env) = add_vars (u, add_vars (t, env)) + | add_vars (_, env) = env; + + fun add_varsT (Type (_, Ts), env) = foldr add_varsT (Ts, env) + | add_varsT (TFree (x, S), env) = ins_entry (S, (x, ~1)) env + | add_varsT (TVar (xi, S), env) = ins_entry (S, xi) env; + + fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs; + fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs; + + + (* prepare atoms *) + + fun consts_of t = sort_cnsts (add_consts (t, [])); + fun vars_of t = sort_idxs (add_vars (t, [])); + fun varsT_of t = rev (sort_idxs (it_term_types add_varsT (t, []))); + +in + + fun script_print_goals maxgoals state = + let + val {sign, ...} = rep_thm state; + + val prt_term = Sign.pretty_term sign; + val prt_typ = Sign.pretty_typ sign; + val prt_sort = Sign.pretty_sort sign; + + fun prt_atoms prt prtT (X, xs) = Pretty.block + [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::", + Pretty.brk 1, prtT X]; + + fun prt_var (x, ~1) = prt_term (Syntax.free x) + | prt_var xi = prt_term (Syntax.var xi); + + fun prt_varT (x, ~1) = prt_typ (TFree (x, [])) + | prt_varT xi = prt_typ (TVar (xi, [])); + + val prt_consts = prt_atoms (prt_term o Const) prt_typ; + val prt_vars = prt_atoms prt_var prt_typ; + val prt_varsT = prt_atoms prt_varT prt_sort; + + + fun print_list _ _ [] = () + | print_list name prt lst = (writeln ""; + Pretty.writeln (Pretty.big_list name (map prt lst))); + + fun print_subgoals (_, []) = () + | print_subgoals (n, A :: As) = (Pretty.writeln (Pretty.blk (0, + [Pretty.str (goal_start_special ^ + " " ^ string_of_int n ^ ". "), prt_term A])); + print_subgoals (n + 1, As)); + + val print_ffpairs = + print_list "Flex-flex pairs:" (prt_term o Logic.mk_flexpair); + + val print_consts = print_list "Constants:" prt_consts o consts_of; + val print_vars = print_list "Variables:" prt_vars o vars_of; + val print_varsT = print_list "Type variables:" prt_varsT o varsT_of; + + + val {prop, ...} = rep_thm state; + val (tpairs, As, B) = Logic.strip_horn prop; + val ngoals = length As; + + fun print_gs (types, sorts) = + (Pretty.writeln (prt_term B); + if ngoals = 0 then writeln "No subgoals!" + else if ngoals > maxgoals then + (print_subgoals (1, take (maxgoals, As)); + writeln ("A total of " ^ string_of_int ngoals ^ " subgoals...")) + else print_subgoals (1, As); + + print_ffpairs tpairs; + + if types andalso ! show_consts then print_consts prop else (); + if types then print_vars prop else (); + if sorts then print_varsT prop else ()); + in + setmp show_no_free_types true + (setmp show_types (! show_types orelse ! show_sorts) + (setmp show_sorts false print_gs)) + (! show_types orelse ! show_sorts, ! show_sorts) + end; + +end; + + + + +(* Pure/goals.ML declares print_current_goals_fn. *) + +val orig_print_current_goals_fn = !print_current_goals_fn; + +fun script_mode_print_current_goals_fn n max th = + (writeln ("Level " ^ string_of_int n); script_print_goals max th); + +local + fun out s = + (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut); + fun cgf i j t = + (out proof_state_special_prefix; + script_mode_print_current_goals_fn i j t; + out proof_state_special_suffix) +in + val () = (print_current_goals_fn := cgf) +end + + + + + +
\ No newline at end of file diff --git a/isa-syntax.el b/isa-syntax.el new file mode 100644 index 00000000..2cba6435 --- /dev/null +++ b/isa-syntax.el @@ -0,0 +1,112 @@ +;; isa-syntax.el Syntax expressions for Isabelle +;; + +(require 'proof-syntax) + +;; ----- keywords for font-lock. + +(defvar isa-keywords-decl + '( +)) + +(defvar isa-keywords-defn + '( +"bind_thm" +)) + +(defvar isa-keywords-goal + '( +"goal" +)) + +(defvar isa-keywords-save + '( +"qed" +)) + +(defvar isa-keywords-kill-goal '( +)) + +(defvar isa-keywords-commands + '( +"by" +"goal" +)) + +;; See isa-command-table in Isamode/isa-menus.el to get this list. +(defvar isa-tactics + '( +"resolve_tac" "assume_tac" +)) + +(defvar isa-keywords + (append isa-keywords-goal isa-keywords-save isa-keywords-decl + isa-keywords-defn isa-keywords-commands isa-tactics) + "All keywords in a Isa script") + +(defvar isa-tacticals '( +"REPEAT" "THEN" "ORELSE" "TRY" +)) + +;; ----- regular expressions + +;; this should come from isa-ml-compiler stuff. +(defvar isa-error-regexp + "^.*Error:" + "A regular expression indicating that the Isa process has identified + an error.") + +(defvar isa-id proof-id) + +(defvar isa-ids (proof-ids isa-id)) + +(defun isa-abstr-regexp (paren char) + (concat paren "\\s-*\\(" isa-ids "\\)\\s-*" char)) + +(defvar isa-font-lock-terms + (list + + ;; lambda binders + (list (isa-abstr-regexp "\\[" ":") 1 'font-lock-declaration-name-face) + + ;; Pi binders + (list (isa-abstr-regexp "(" ":") 1 'font-lock-declaration-name-face) + + ;; Kinds + (cons (concat "\\<Prop\\>\\|\\<Set\\>\\|\\<Type\\s-*\\((" + isa-id ")\\)?") 'font-lock-type-face)) + "*Font-lock table for Isa terms.") + +;; According to Isa, "Definition" is both a declaration and a goal. +;; It is understood here as being a goal. This is important for +;; recognizing global identifiers, see isa-global-p. +(defconst isa-save-command-regexp + (concat "^" (ids-to-regexp isa-keywords-save))) +(defconst isa-save-with-hole-regexp + (concat "\\(" (ids-to-regexp isa-keywords-save) + "\\)\\s-+\\(" isa-id "\\)\\s-*\.")) +(defconst isa-goal-command-regexp + (concat "^" (ids-to-regexp isa-keywords-goal))) +(defconst isa-goal-with-hole-regexp + (concat "\\(" (ids-to-regexp isa-keywords-goal) + "\\)\\s-+\\(" isa-id "\\)\\s-*:")) +(defconst isa-decl-with-hole-regexp + (concat "\\(" (ids-to-regexp isa-keywords-decl) + "\\)\\s-+\\(" isa-ids "\\)\\s-*:")) +(defconst isa-defn-with-hole-regexp + (concat "\\(" (ids-to-regexp isa-keywords-defn) + "\\)\\s-+\\(" isa-id "\\)\\s-*[:[]")) + +(defvar isa-font-lock-keywords-1 + (append + isa-font-lock-terms + (list + (cons (ids-to-regexp isa-keywords) 'font-lock-keyword-face) + (cons (ids-to-regexp isa-tacticals) 'font-lock-tacticals-name-face) + + (list isa-goal-with-hole-regexp 2 'font-lock-function-name-face) + (list isa-decl-with-hole-regexp 2 'font-lock-declaration-name-face) + (list isa-defn-with-hole-regexp 2 'font-lock-function-name-face) + (list isa-save-with-hole-regexp 2 'font-lock-function-name-face)))) + +(provide 'isa-syntax) @@ -0,0 +1,434 @@ +;; isa.el Major mode for Isabelle proof assistant +;; Copyright (C) 1994-1998 LFCS Edinburgh. +;; Author: David Aspinall + +;; $Log$ +;; Revision 2.1 1998/08/21 14:37:18 da +;; First attempt, proof state works. +;; +;; Revision 2.0 1998/08/11 14:59:57 da +;; New branch +;; +;; Revision 1.1 1998/08/11 14:43:34 da +;; Isabelle proof.el support. +;; + +;; STATUS: +;; - Basic proof state extraction works, using prompt regexp +;; - Undo needs attention + + +(require 'isa-syntax) +(require 'outline) +(require 'proof) + +; Configuration + +(defvar isa-assistant "Isabelle" + "Name of proof assistant") + +(defvar isa-tags nil ; "/usr/local/lib/isa/theories/TAGS" + "the default TAGS table for the Isa library") + +(defconst isa-process-config nil + "Command to configure pretty printing of the Isa process for emacs.") + +(defconst isa-interrupt-regexp "Interrupt" + "Regexp corresponding to an interrupt") + +(defvar isa-save-query t + "*If non-nil, ask user for permission to save the current buffer before + processing a module.") + +(defvar isa-default-undo-limit 100 + "Maximum number of Undo's possible when doing a proof.") + +;; ----- web documentation + +(defvar isa-www-home-page "http://www.cl.cam.ac.uk/Research/HVG/isabelle.html") + +;; ----- isa-shell configuration options + +;; FIXME: needs to have special characters for proof.el, also path +;; name shouldn't be here. +(defvar isa-prog-name "/usr/lib/Isabelle98/bin/isabelle" + "*Name of program to run as Isabelle.") + +(defvar isa-shell-working-dir "" + "The working directory of the isabelle shell") + +(defvar isa-shell-prompt-pattern + ;; borrowed from somewhere? + ;; "^2?[---=#>]>? *\\|^\\*\\* .*" + "^> " + "*The prompt pattern for the inferior shell running isabelle.") + +(defvar isa-shell-cd "cd \"%s\";" + "*Command of the inferior process to change the directory.") + +;; FIXME: check this? +; Don't define this, no correspondence. +;(defvar isa-shell-abort-goal-regexp nil +; "*Regular expression indicating that the proof of the current goal +; has been abandoned.") + +(defvar isa-shell-proof-completed-regexp "No subgoals!" + "*Regular expression indicating that the proof has been completed.") + +(defvar isa-goal-regexp + "^[ \t]*[0-9]+\\. " + "Regexp to match subgoal heading.") + +;; ----- outline + +;;; FIXME: BROKEN +(defvar isa-outline-regexp + (ids-to-regexp + '("Section" "Chapter" "Goal" "Lemma" "Theorem" "Fact" + "Remark" "Record" "Inductive" "Definition"))) + +(defvar isa-outline-heading-end-regexp "\.\\|\\*)") + +(defvar isa-shell-outline-regexp isa-goal-regexp) +(defvar isa-shell-outline-heading-end-regexp isa-goal-regexp) + +;;; ---- end-outline + +(defconst isa-kill-goal-command nil) ; "Abort." +(defconst isa-forget-id-command nil) ; "Reset " + +;;; FIXME!! +(defconst isa-undoable-commands-regexp (ids-to-regexp isa-tactics)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Derived modes - they're here 'cos they define keymaps 'n stuff ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(define-derived-mode isa-shell-mode proof-shell-mode + "isa-shell" "Inferior shell mode for isabelle shell" + (isa-shell-mode-config)) + +(define-derived-mode isa-mode proof-mode + "isa" "Isabelle Mode" + (isa-mode-config)) + +(define-derived-mode isa-pbp-mode pbp-mode + "pbp" "Proof-by-pointing support for Isabelle" + (isa-pbp-mode-config)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Code that's Isabelle specific ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;(defun isa-shell-init-hook () +; (remove-hook 'proof-shell-insert-hook 'isa-shell-init-hook)) + +;(defun isa-set-undo-limit (undos) +; (proof-invisible-command (format "Set Undo %s." undos))) + +(defun isa-count-undos (span) + (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) + (if (string-match isa-undoable-commands-regexp str) + (setq ct (+ 1 ct)))) + ((eq (span-property span 'type) 'pbp) + (cond ((string-match isa-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)))) + +(defconst isa-keywords-decl-defn-regexp + (ids-to-regexp (append isa-keywords-decl isa-keywords-defn)) + "Declaration and definition regexp.") + +(defun isa-goal-command-p (str) + "Decide whether argument is a goal or not" + (and (string-match isa-goal-command-regexp str) + (not (string-match "Definition.*:=" str)))) + +(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"))) + +(defvar isa-current-goal 1 + "Last goal that emacs looked at.") + +(defun isa-goal-hyp () + (cond + ((looking-at "============================\n") + (goto-char (match-end 0)) + (cons 'goal (int-to-string isa-current-goal))) + ((looking-at "subgoal \\([0-9]+\\) is:\n") + (goto-char (match-end 0)) + (cons 'goal (match-string 1)) + (setq isa-current-goal (string-to-int (match-string 1)))) + ((looking-at proof-shell-assumption-regexp) + (cons 'hyp (match-string 1))) + (t nil))) + +(defun isa-state-preserving-p (cmd) + (not (string-match isa-undoable-commands-regexp cmd))) + +(defun isa-global-p (cmd) + (or (string-match isa-keywords-decl-defn-regexp cmd) + (and (string-match + (concat "Definition\\s-+\\(" isa-id "\\)\\s-*:") cmd) + (string-match ":=" cmd)))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Commands specific to Isabelle ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun isa-Intros () + "List proof state." + (interactive) + (insert "printlev")) + +(defun isa-Apply () + "List proof state." + (interactive) + (insert "Apply ")) + +(defun isa-Search () + "Search for type in goals." + (interactive) + (let (cmd) + (proof-check-process-available) + (setq cmd (read-string "Search Type: " nil 'proof-minibuffer-history)) + (proof-invisible-command (concat "Search " cmd proof-terminal-string)))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Indentation ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; "Case" is represented by 'c' on the stack, and +;; "CoInductive is represented by 'C'. +(defun isa-stack-to-indent (stack) + (cond + ((null stack) 0) + ((null (car (car stack))) + (nth 1 (car stack))) + (t (let ((col (save-excursion + (goto-char (nth 1 (car stack))) + (current-column)))) + (cond + ((eq (car (car stack)) ?c) + (save-excursion (move-to-column (current-indentation)) + (cond + ((eq (char-after (point)) ?|) (+ col 3)) + ((looking-at "end") col) + (t (+ col 5))))) + ((or (eq (car (car stack)) ?I) (eq (car (car stack)) ?C)) + (+ col (if (eq ?| (save-excursion + (move-to-column (current-indentation)) + (char-after (point)))) 2 4))) + (t (1+ col))))))) + +(defun isa-parse-indent (c stack) + (cond + ((eq c ?C) + (cond ((looking-at "Case") + (cons (list ?c (point)) stack)) + ((looking-at "CoInductive") + (forward-char (length "CoInductive")) + (cons (list c (- (point) (length "CoInductive"))) stack)) + (t stack))) + ((and (eq c ?e) (looking-at "end") (eq (car (car stack)) ?c)) + (cdr stack)) + + ((and (eq c ?I) (looking-at "Inductive")) + (forward-char (length "Inductive")) + (cons (list c (- (point) (length "Inductive"))) stack)) + + ((and (eq c ?.) (or (eq (car (car stack)) ?I) (eq (car (car stack)) ?C))) + (cdr stack)) + + (t 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 () + + (setq proof-terminal-char ?\;) + (setq proof-comment-start "(*") + (setq proof-comment-end "*)") + + (setq proof-assistant isa-assistant + proof-www-home-page isa-www-home-page) + + (setq proof-prf-string "pr()" + proof-ctxt-string "print \"No context for Isabelle.\"" + proof-help-string "print \"No in-built help for Isabelle.\"") + + (setq proof-goal-command-p 'isa-goal-command-p + proof-count-undos-fn 'isa-count-undos + ;; this one won't be relevant. + 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 + proof-parse-indent 'isa-parse-indent + proof-stack-to-indent 'isa-stack-to-indent) + + (setq 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-kill-goal-command isa-kill-goal-command + proof-commands-regexp (ids-to-regexp isa-keywords)) + + (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 + + (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 '(("\\.v$" . isa-tags) + ("isa" . isa-tags)) + tag-table-alist))) + + (setq blink-matching-paren-dont-ignore-comments t) + +;; hooks and callbacks + + (add-hook 'proof-shell-exit-hook 'isa-zap-line-width nil t) + (add-hook 'proof-pre-shell-start-hook 'isa-pre-shell-start nil t)) + + + +(defun isa-shell-mode-config () + (setq proof-shell-prompt-pattern isa-shell-prompt-pattern + proof-shell-cd isa-shell-cd +; this one not set. +; proof-shell-abort-goal-regexp isa-shell-abort-goal-regexp + proof-shell-proof-completed-regexp isa-shell-proof-completed-regexp + proof-shell-error-regexp isa-error-regexp + proof-shell-interrupt-regexp isa-interrupt-regexp + proof-shell-noise-regexp "" + proof-shell-assumption-regexp isa-id + proof-shell-goal-regexp isa-goal-regexp + proof-shell-first-special-char ?\360 + ; The next three represent path annotation information + + proof-shell-eager-annotation-start "\376" + proof-shell-eager-annotation-end "\377" + proof-shell-annotated-prompt-regexp proof-shell-prompt-pattern + ;(concat proof-shell-prompt-pattern + ; (char-to-string proof-shell-wakeup-char)) + 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 ; not done + proof-shell-end-char ?\373 ; not done + proof-shell-field-char ?\374 ; not done + ;; da: settings below here WORK + ;; ============================ + proof-shell-goal-char ?\375 + ;; 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 directory for this: /home/da/devel/lego/elisp/ + proof-shell-init-cmd + "use \"isa-print-functions.ML\";") + + + ;; 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) + + (proof-shell-config-done)) + +(defun isa-pbp-mode-config () + (setq pbp-change-goal "Show %s.") + (setq pbp-error-regexp isa-error-regexp)) + +(provide 'isa) diff --git a/lego-syntax.el b/lego-syntax.el new file mode 100644 index 00000000..60ede04f --- /dev/null +++ b/lego-syntax.el @@ -0,0 +1,100 @@ +;; lego-fontlock.el Font lock expressions for LEGO +;; Copyright (C) 1994, 1995, 1996, 1997 LFCS Edinburgh. +;; Author: Healfdene Goguen, Thomas Kleymann and Dilip Sequeira +;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> + +(require 'proof-syntax) + +;; ----- keywords for font-lock. + +(defconst lego-keywords-goal '("$?Goal")) + +(defconst lego-keywords-save '("$?Save" "SaveFrozen" "SaveUnfrozen")) + +(defconst lego-commands + (append lego-keywords-goal lego-keywords-save + '("allE" "allI" "andE" "andI" "Assumption" "Claim" + "Cut" "Discharge" "DischargeKeep" + "echo" "exE" "exI" "Expand" "ExpAll" + "ExportState" "Equiv" "For" "Freeze" "Hnf" "Immed" + "impE" "impI" "Induction" "Inductive" + "Invert" "Init" "intros" "Intros" "Module" "Next" + "Normal" "notE" "notI" "orE" "orIL" "orIR" "qnify" "Qnify" + "Qrepl" "Record" "Refine" "Repeat" "Try" "Unfreeze")) + "Subset of LEGO keywords and tacticals which are terminated by a \?;") + +(defconst lego-keywords + (append lego-commands + '("Constructors" "Double" "ElimOver" "Fields" "Import" "Inversion" + "NoReductions" "Parameters" "Relation" "Theorems"))) + +(defconst lego-tacticals '("Then" "Else" "Try" "Repeat" "For")) + +;; ----- regular expressions for font-lock +(defvar lego-error-regexp "^\\(Error\\|Lego parser\\)" + "A regular expression indicating that the LEGO process has + identified an error.") + +(defvar lego-id proof-id) + +(defvar lego-ids (concat lego-id "\\(\\s *,\\s *" lego-id "\\)*") + "*For font-lock, we treat \",\" separated identifiers as one identifier + and refontify commata using \\{lego-fixup-change}.") + +(defconst lego-arg-list-regexp "\\s *\\(\\[[^]]+\\]\\s *\\)*" + "Regular expression maching a list of arguments.") + +(defun lego-decl-defn-regexp (char) + (concat "\\[\\s *\\(" lego-ids "\\)" lego-arg-list-regexp char)) +; Examples +; ^ ^^^^ ^^^^^^^^^^^^^^^^^^^^^^^ ^^^^ +; [ sort = +; [ sort [n:nat] = +; [ sort [abbrev=...][n:nat] = + +(defconst lego-definiendum-alternative-regexp + (concat "\\(" lego-id "\\)" lego-arg-list-regexp "\\s * ==") + "Regular expression where the first match identifies the definiendum.") + +(defvar lego-font-lock-terms + (list + + ; lambda binders + (list (lego-decl-defn-regexp "[:|]") 1 + 'font-lock-declaration-name-face) + + ; let binders + (list lego-definiendum-alternative-regexp 1 'font-lock-function-name-face) + (list (lego-decl-defn-regexp "=") 1 'font-lock-function-name-face) + + ; Pi and Sigma binders + (list (concat "[{<]\\s *\\(" lego-ids "\\)") 1 + 'font-lock-declaration-name-face) + + ;; Kinds + (cons (concat "\\<Prop\\>\\|\\<Type\\s *\\((" + lego-id ")\\)?") 'font-lock-type-face)) + "*Font-lock table for LEGO terms.") + +;; Instead of "[^:]+", it may be better to use "lego-id". Furthermore, +;; it might be safer to append "\\s-*:". +(defconst lego-goal-with-hole-regexp + (concat "\\(" (ids-to-regexp lego-keywords-goal) "\\)\\s-+\\([^:]+\\)") + "Regular expression which matches an entry in `lego-keywords-goal' + and the name of the goal.") + +(defconst lego-save-with-hole-regexp + (concat "\\(" (ids-to-regexp lego-keywords-save) "\\)\\s-+\\([^;]+\\)") + "Regular expression which matches an entry in + `lego-keywords-save' and the name of the goal.") + +(defvar lego-font-lock-keywords-1 + (append + lego-font-lock-terms + (list + (cons (ids-to-regexp lego-keywords) 'font-lock-keyword-face) + (cons (ids-to-regexp lego-tacticals) 'font-lock-tacticals-name-face) + (list lego-goal-with-hole-regexp 2 'font-lock-function-name-face) + (list lego-save-with-hole-regexp 2 'font-lock-function-name-face)))) + +(provide 'lego-syntax) diff --git a/lego.el b/lego.el new file mode 100644 index 00000000..b8a398e1 --- /dev/null +++ b/lego.el @@ -0,0 +1,469 @@ +;; lego.el Major mode for LEGO proof assistants +;; Copyright (C) 1994 - 1998 LFCS Edinburgh. +;; Author: Thomas Kleymann and Dilip Sequeira +;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> + +(require 'lego-syntax) +(require 'outline) +(require 'proof) + +;;;;;;;;;;;;;;;;;;;;;;;;;; +;;; User Configuration ;;; +;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; I believe this is standard for Linux under RedHat -tms +(defvar lego-tags "/usr/lib/lego/lib_Type/" + "*the default TAGS table for the LEGO library") + +(defvar lego-indent 2 "*Indentation") + +(defvar lego-test-all-name "test_all" + "*The name of the LEGO module which inherits all other modules of the + library.") + +(defvar lego-save-query t + "*If non-nil, ask user for permission to save the current buffer before + processing a module.") + +(defvar lego-help-menu-list + '(["The LEGO Reference Card" (w3-fetch lego-www-refcard) t] + ["The LEGO library (WWW)" (w3-fetch lego-library-www-page) t]) + "List of menu items, as defined in `easy-menu-define' for LEGO + specific help.") + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;; Configuration of Generic Proof Package ;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Users should not need to change this. + +(defvar lego-shell-process-output + '((lambda (cmd string) (string-match "^Module" cmd)) . + (lambda (cmd string) + (setq proof-shell-delayed-output + (cons 'insert "Imports done!")))) + "Acknowledge end of processing import declarations.") + +(defvar lego-assistant "LEGO" + "Name of proof assistant") + +(defconst lego-process-config "Configure PrettyOn; Configure AnnotateOn;" + "Command to enable pretty printing of the LEGO process.") + +(defconst lego-pretty-set-width "Configure PrettyWidth %s; " + "Command to adjust the linewidth for pretty printing of the LEGO + process.") + +(defconst lego-interrupt-regexp "Interrupt.." + "Regexp corresponding to an interrupt") + +(defvar lego-path-name "LEGOPATH" + "The name of the environmental variable to search for modules. This + is used by \\{legogrep} to find the files corresponding to a + search.") + +(defvar lego-path-separator ":" + "A character indicating how the items in the \\{lego-path-name} are + separated.") + + +;; ----- web documentation + +(defvar lego-www-home-page "http://www.dcs.ed.ac.uk/home/lego/") + +(defvar lego-www-latest-release + (concat (w3-remove-file-name lego-www-home-page) + "html/release-1.3/") + "The WWW address for the latest LEGO release.") + +(defvar lego-www-refcard (concat lego-www-latest-release + "refcard.ps.gz")) + +(defvar lego-library-www-page + (concat lego-www-latest-release "library/library.html") + "The HTML documentation of the LEGO library.") + +;; ----- legostat and legogrep, courtesy of Mark Ruys + +(defvar legogrep-command (concat "legogrep -n \"\" " lego-test-all-name) + "Last legogrep command used in \\{legogrep}; default for next legogrep.") + +(defvar legostat-command "legostat -t") + +(defvar legogrep-regexp-alist + '(("^\\([^:( \t\n]+\\)[:( \t]+\\([0-9]+\\)[:) \t]" 1 2 nil ("%s.l"))) + "Regexp used to match legogrep hits. See `compilation-error-regexp-alist'.") + +;; ----- lego-shell configuration options + +(defvar lego-prog-name "lego" + "*Name of program to run as lego.") + +(defvar lego-shell-working-dir "" + "The working directory of the lego shell") + +(defvar lego-shell-prompt-pattern "^\\(Lego>[ \201]*\\)+" + "*The prompt pattern for the inferior shell running lego.") + +(defvar lego-shell-cd "Cd \"%s\";" + "*Command of the inferior process to change the directory.") + +(defvar lego-shell-abort-goal-regexp "KillRef: ok, not in proof state" + "*Regular expression indicating that the proof of the current goal + has been abandoned.") + +(defvar lego-shell-proof-completed-regexp "\\*\\*\\* QED \\*\\*\\*" + "*Regular expression indicating that the proof has been completed.") + +(defvar lego-save-command-regexp + (concat "^" (ids-to-regexp lego-keywords-save))) +(defvar lego-goal-command-regexp + (concat "^" (ids-to-regexp lego-keywords-goal))) + +(defvar lego-kill-goal-command "KillRef;") +(defvar lego-forget-id-command "Forget ") + +(defvar lego-undoable-commands-regexp + (ids-to-regexp '("Dnf" "Refine" "Intros" "intros" "Next" "Normal" + "Qrepl" "Claim" "For" "Repeat" "Succeed" "Fail" "Try" "Assumption" + "UTac" "Qnify" "qnify" "andE" "andI" "exE" "exI" "orIL" "orIR" "orE" "ImpI" + "impE" "notI" "notE" "allI" "allE" "Expand" "Induction" "Immed" + "Invert")) "Undoable list") + +;; ----- outline + +(defvar lego-goal-regexp "\\?\\([0-9]+\\)") + +(defvar lego-outline-regexp + (concat "[[*]\\|" + (ids-to-regexp + '("Discharge" "DischargeKeep" "Freeze" "$?Goal" "Module" "Record" "Inductive" + "Unfreeze")))) + +(defvar lego-outline-heading-end-regexp ";\\|\\*)") + +(defvar lego-shell-outline-regexp lego-goal-regexp) +(defvar lego-shell-outline-heading-end-regexp lego-goal-regexp) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Derived modes - they're here 'cos they define keymaps 'n stuff ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(define-derived-mode lego-shell-mode proof-shell-mode + "lego-shell" "Inferior shell mode for lego shell" + (lego-shell-mode-config)) + +(define-derived-mode lego-mode proof-mode + "lego" "Lego Mode" + (lego-mode-config) + (easy-menu-change (list proof-mode-name) (car proof-help-menu) + (append (cdr proof-help-menu) lego-help-menu-list))) + +(define-derived-mode lego-pbp-mode pbp-mode + "pbp" "Proof-by-pointing support for LEGO" + (lego-pbp-mode-config)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Code that's lego specific ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; Martin Steffen <mnsteffe@informatik.uni-erlangen.de> has pointed +;; out that calling lego-get-path has to deal with a user who hasn't +;; set the environmental variable LEGOPATH. It is probably best if +;; lego is installed as a shell script which sets a sensible default +;; for LEGOPATH if the user hasn't done so before. See the +;; documentation of the library for further details. + +(defun lego-get-path () + (let ((path-name (getenv lego-path-name))) + (cond ((not path-name) + (message "Warning: LEGOPATH has not been set!") + (setq path-name "."))) + (proof-string-to-list path-name lego-path-separator))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; This is how to work out what the undo commands are, given the ;; +;; first span which needs to be undone ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; needs to handle Normal as well +;; it should ignore Normal TReg Normal VReg and (Normal ...) +(defun lego-count-undos (span) + (let ((ct 0) str i) + (while span + (setq str (span-property span 'cmd)) + (cond ((eq (span-property span 'type) 'vanilla) + (if (or (string-match lego-undoable-commands-regexp str) + (and (string-match "Equiv" str) + (not (string-match "Equiv\\s +[TV]Reg" str)))) + (setq ct (+ 1 ct)))) + ((eq (span-property span 'type) 'pbp) + (setq i 0) + (while (< i (length str)) + (if (= (aref str i) proof-terminal-char) (setq ct (+ 1 ct))) + (setq i (+ 1 i))))) + (setq span (next-span span 'type))) + (concat "Undo " (int-to-string ct) proof-terminal-string))) + +(defun lego-goal-command-p (str) + "Decide whether argument is a goal or not" + (string-match lego-goal-command-regexp str)) + +(defun lego-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 lego-forget-id-command + (span-property span 'name) proof-terminal-string))) + + ;; alternative definitions + ((string-match lego-definiendum-alternative-regexp str) + (setq ans (concat lego-forget-id-command (match-string 1 str) + proof-terminal-string))) + ;; declarations + ((string-match (concat "\\`\\$?" (lego-decl-defn-regexp "[:|=]")) str) + (let ((ids (match-string 1 str))) ; returns "a,b" + (string-match proof-id ids) ; matches "a" + (setq ans (concat lego-forget-id-command(match-string 1 ids) + proof-terminal-string)))) + + ((string-match "\\`\\(Inductive\\|\\Record\\)\\s-*\\[\\s-*\\w+\\s-*:[^;]+\\`Parameters\\s-*\\[\\s-*\\(\\w+\\)\\s-*:" str) + (setq ans (concat lego-forget-id-command + (match-string 2 str) proof-terminal-string))) + + ((string-match + "\\`\\(Inductive\\|Record\\)\\s-*\\[\\s-*\\(\\w+\\)\\s-*:" str) + (setq ans + (concat lego-forget-id-command (match-string 2 str) + proof-terminal-string))) + + ((string-match "\\`\\s-*Module\\s-+\\(\\S-+\\)\\W" str) + (setq ans (concat "ForgetMark " (match-string 1 str) + proof-terminal-string)))) + + (setq span (next-span span 'type))) + (or ans + "COMMENT"))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Other stuff which is required to customise script management ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun lego-goal-hyp () + (cond + ((looking-at proof-shell-goal-regexp) + (cons 'goal (match-string 1))) + ((looking-at proof-shell-assumption-regexp) + (cons 'hyp (match-string 1))) + (t nil))) + + +(defun lego-state-preserving-p (cmd) + (not (string-match lego-undoable-commands-regexp cmd))) + +(defun lego-global-p (cmd) + nil) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Commands specific to lego ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun lego-intros () + "intros." + (interactive) + (insert "intros ")) + +(defun lego-Intros () + "List proof state." + (interactive) + (insert "Intros ")) + +(defun lego-Refine () + "List proof state." + (interactive) + (insert "Refine ")) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Lego Indentation ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun lego-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))) + (+ lego-indent (current-column)))))) + +(defun lego-parse-indent (c stack) + (cond + ((eq c ?\{) (cons (list c (point)) stack)) + ((eq c ?\}) (cdr stack)) + (t stack))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Lego shell startup and exit hooks ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defvar lego-shell-current-line-width nil + "Current line width of the LEGO process's pretty printing module. + Its value will be updated whenever the corresponding screen gets + selected.") + +;; The line width needs to be adjusted if the LEGO process is +;; running and is out of sync with the screen width + +(defun lego-shell-adjust-line-width () + "Uses LEGO's pretty printing facilities to adjust the line width of + the output." + (save-excursion + (set-buffer proof-shell-buffer) + (and (proof-shell-live-buffer) + (let ((current-width + (window-width (get-buffer-window proof-shell-buffer)))) + (if (equal current-width lego-shell-current-line-width) () + ; else + (setq lego-shell-current-line-width current-width) + (insert (format lego-pretty-set-width (- current-width 1))) + ))))) + +(defun lego-pre-shell-start () + (setq proof-prog-name lego-prog-name) + (setq proof-mode-for-shell 'lego-shell-mode) + (setq proof-mode-for-pbp 'lego-pbp-mode)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Configuring proof and pbp mode and setting up various utilities ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun lego-init-syntax-table () + "Set appropriate values for syntax table in current buffer." + + (modify-syntax-entry ?_ "_") + (modify-syntax-entry ?\' "_") + (modify-syntax-entry ?\| ".") + (modify-syntax-entry ?\* ". 23") + (modify-syntax-entry ?\( "()1") + (modify-syntax-entry ?\) ")(4")) + +(defun lego-mode-config () + + (setq proof-terminal-char ?\;) + (setq proof-comment-start "(*") + (setq proof-comment-end "*)") + + (setq proof-assistant lego-assistant + proof-www-home-page lego-www-home-page) + + (setq proof-prf-string "Prf" + proof-ctxt-string "Ctxt" + proof-help-string "Help") + + (setq proof-goal-command-p 'lego-goal-command-p + proof-count-undos-fn 'lego-count-undos + proof-find-and-forget-fn 'lego-find-and-forget + proof-goal-hyp-fn 'lego-goal-hyp + proof-state-preserving-p 'lego-state-preserving-p + proof-global-p 'lego-global-p + proof-parse-indent 'lego-parse-indent + proof-stack-to-indent 'lego-stack-to-indent) + + (setq proof-save-command-regexp lego-save-command-regexp + proof-save-with-hole-regexp lego-save-with-hole-regexp + proof-goal-with-hole-regexp lego-goal-with-hole-regexp + proof-kill-goal-command lego-kill-goal-command + proof-commands-regexp (ids-to-regexp lego-commands)) + + (lego-init-syntax-table) + + (proof-config-done) + + (define-key (current-local-map) [(control c) ?i] 'lego-intros) + (define-key (current-local-map) [(control c) ?I] 'lego-Intros) + (define-key (current-local-map) [(control c) ?r] 'lego-Refine) + +;; outline + + (make-local-variable 'outline-regexp) + (setq outline-regexp lego-outline-regexp) + + (make-local-variable 'outline-heading-end-regexp) + (setq outline-heading-end-regexp lego-outline-heading-end-regexp) + +;; tags + (cond ((boundp 'tags-table-list) + (make-local-variable 'tags-table-list) + (setq tags-table-list (cons lego-tags tags-table-list)))) + + (and (boundp 'tag-table-alist) + (setq tag-table-alist + (append '(("\\.l$" . lego-tags) + ("lego" . lego-tags)) + tag-table-alist))) + + (setq font-lock-keywords lego-font-lock-keywords-1) + +;; where to find files + + (setq compilation-search-path (cons nil (lego-get-path))) + + (setq blink-matching-paren-dont-ignore-comments t) + +;; font-lock + +;; if we don't have the following in xemacs, zap-commas fails to work. + + (and (boundp 'font-lock-always-fontify-immediately) + (setq font-lock-always-fontify-immediately t)) + +;; hooks and callbacks + + (add-hook 'proof-shell-exit-hook 'lego-zap-line-width nil t) + (add-hook 'proof-pre-shell-start-hook 'lego-pre-shell-start nil t) + (add-hook 'proof-shell-insert-hook 'lego-shell-adjust-line-width)) + +;; insert standard header and footer in fresh buffers + +(defun lego-shell-mode-config () + (setq proof-shell-prompt-pattern lego-shell-prompt-pattern + proof-shell-cd lego-shell-cd + proof-shell-abort-goal-regexp lego-shell-abort-goal-regexp + proof-shell-proof-completed-regexp lego-shell-proof-completed-regexp + proof-shell-error-regexp lego-error-regexp + proof-shell-interrupt-regexp lego-interrupt-regexp + proof-shell-noise-regexp "Discharge\\.\\. " + proof-shell-assumption-regexp lego-id + proof-shell-goal-regexp lego-goal-regexp + proof-shell-first-special-char ?\360 + proof-shell-wakeup-char ?\371 + proof-shell-start-char ?\372 + proof-shell-end-char ?\373 + proof-shell-field-char ?\374 + proof-shell-goal-char ?\375 + proof-shell-eager-annotation-start "\376" + proof-shell-eager-annotation-end "\377" + proof-shell-annotated-prompt-regexp "Lego> \371" + proof-shell-result-start "\372 Pbp result \373" + proof-shell-result-end "\372 End Pbp result \373" + proof-shell-start-goals-regexp "\372 Start of Goals \373" + proof-shell-end-goals-regexp "\372 End of Goals \373" + proof-shell-init-cmd lego-process-config + proof-analyse-using-stack nil + proof-shell-process-output-system-specific lego-shell-process-output + lego-shell-current-line-width nil) + + (lego-init-syntax-table) + + (proof-shell-config-done)) + +(defun lego-pbp-mode-config () + (setq pbp-change-goal "Next %s;") + (setq pbp-error-regexp lego-error-regexp)) + +(provide 'lego) diff --git a/legotags b/legotags new file mode 100644 index 00000000..a3c13eab --- /dev/null +++ b/legotags @@ -0,0 +1,87 @@ +#!/usr/local/bin/perl + +undef $/; + +if($#ARGV<$[) {die "No Files\n";} +open(tagfile,">TAGS") || die "Couldn't open TAGS: $!\n"; + +while(<>) +{ + print "Tagging $ARGV\n"; + $a=$_; + $cp=1; + $lp=1; + $tagstring=""; + + while(1) + { + +# ---- Get the next statement starting on a newline ---- + + if($a=~/^[ \t\n]*\(\*/) + { while($a=~/^\s*\(\*/) + { $d=1; $a=$'; $cp+=length $&; $lp+=(($wombat=$&)=~tr/\n/\n/); + while($d>0 && $a=~/\(\*|\*\)/) + { $a=$'; $cp+=2+length $`; $lp+=(($wombat=$`)=~tr/\n/\n/); + if($& eq "(*") {$d++} else {$d--}; + } + if($d!=0) {die "Unbalanced Comment?";} + } + } + + if($cp>1 && $a=~/.*\n/) {$a=$'; $cp+=length $&; $lp++;} + while($a=~/^\n/) {$cp++;$lp++;$a=$'} + + if($a=~/^[^;]*;/) + { $stmt=$&; + $newa=$'; + $newcp=$cp+length $&; + $newlp=$lp+(($wombat=$&)=~tr/\n/\n/); } + else { last;} + +# ---- The above embarrasses itself if there are semicolons inside comments +# ---- inside commands. Could do better. + +# print "----- (",$lp,",",$cp,")\n", $stmt, "\n"; + + if($stmt=~/^([ \t]*\$?Goal\s*([\w\']+))\s*:/) + { $tagstring.=$1."\177".$2."\001".$lp.",".$cp."\n"; } + + elsif($stmt=~/^([ \t]*\$?\[\s*[\w\']+)/) + { do adddecs($stmt,$1) } + + elsif($stmt=~/^([ \t]*Inductive\s*\[\s*[\w\']+)/) + { do adddecs($stmt,$1) } + +# ---- we don't need to tag saves: all goals should be named! + +# elsif($stmt=~/([ \t]*\$?Save\s+([\w\']+))/) +# { $tagstring.=$1."\177".$2."\001".$lp.",".$cp."\n"; } +# +# elsif($stmt=~/^([ \t]*\$?SaveUnfrozen\s+([\w\']+))/) +# { $tagstring.=$1."\177".$2."\001".$lp.",".$cp."\n"; } + +# ---- Maybe do something smart with discharge as well? + + $cp=$newcp; $lp=$newlp; $a=$newa; + } + print tagfile "\f\n".$ARGV.",".(length $tagstring)."\n".$tagstring; +} +close tagfile; + + +sub adddecs { + $wk=$_[0]; + $tag=$_[1]; + while($wk=~/\[\s*([\w\']+)/) + { $tagstring.=$tag."\177".$1."\001".$lp.",".$cp."\n"; $wk=$'; + while($wk=~/^\s*,\s*([\w\']+)/) + { $tagstring.=$tag."\177".$1."\001".$lp.",".$cp."\n"; $wk=$'; } + $d=1; + while($d>0 && $wk=~/\[|\]/) + { $wk=$'; if($& eq "[") {$d++} else {$d--}; + } + } + 0; +} + @@ -0,0 +1,2 @@ + +(provide 'pbp) diff --git a/proof-indent.el b/proof-indent.el new file mode 100644 index 00000000..bb42f462 --- /dev/null +++ b/proof-indent.el @@ -0,0 +1,124 @@ +;; proof-indent.el Generic Indentation for Proof Assistants +;; Copyright (C) 1997, 1998 LFCS Edinburgh +;; Authors: Healfdene Goguen, Thomas Kleymann and Dilip Sequeira +;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> + +(require 'cl) +(require 'proof-syntax) + +(defvar proof-stack-to-indent nil + "Prover-specific code for indentation.") + +(defvar proof-parse-indent nil + "Proof-assistant specific function for parsing characters for + indentation which is invoked in `proof-parse-to-point.'. Must be a + function taking two arguments, a character (the current character) + and a stack reflecting indentation, and must return a stack. The + stack is a list of the form (c . p) where `c' is a character + representing the type of indentation and `p' records the column for + indentation. The generic `proof-parse-to-point.' function supports + parentheses and commands. It represents these with the characters + `?\(', `?\[' and `proof-terminal-char'. ") + +;; This is quite different from sml-mode, but borrows some bits of +;; code. It's quite a lot less general, but works with nested +;; comments. + +;; parse-to-point: If from is nil, parsing starts from either +;; proof-locked-end if we're in the proof-script-buffer or the +;; beginning of the buffer. Otherwise state must contain a valid +;; triple. + +(defun proof-parse-to-point (&optional from state) + (let ((comment-level 0) (stack (list (list nil 0))) + (end (point)) instring c) + (save-excursion + (if (null from) + (if (eq proof-script-buffer (current-buffer)) + (proof-goto-end-of-locked) + (goto-char 1)) + (goto-char from) + (setq instring (car state) + comment-level (nth 1 state) + stack (nth 2 state))) + (while (< (point) end) + (setq c (char-after (point))) + (cond + (instring + (if (eq c ?\") (setq instring nil))) + (t (cond + ((eq c ?\() + (cond + ((looking-at "(\\*") + (progn + (incf comment-level) + (forward-char))) + ((eq comment-level 0) + (setq stack (cons (list ?\( (point)) stack))))) + ((and (eq c ?\*) (looking-at "\\*)")) + (decf comment-level) + (forward-char)) + ((> comment-level 0)) + ((eq c ?\") (setq instring t)) + ((eq c ?\[) + (setq stack (cons (list ?\[ (point)) stack))) + ((or (eq c ?\)) (eq c ?\])) + (setq stack (cdr stack))) + ((looking-at proof-commands-regexp) + (setq stack (cons (list proof-terminal-char (point)) stack))) + ((and (eq c proof-terminal-char) + (eq (car (car stack)) proof-terminal-char)) (cdr stack)) + (proof-parse-indent + (setq stack (funcall proof-parse-indent c stack)))))) + (forward-char)) + (list instring comment-level stack)))) + +(defun proof-indent-line () + (interactive) + (if (and (eq proof-script-buffer (current-buffer)) + (< (point) (proof-locked-end))) + (if (< (current-column) (current-indentation)) + (skip-chars-forward "\t ")) + (save-excursion + (beginning-of-line) + (let* ((state (proof-parse-to-point)) + (beg (point)) + (indent (cond ((car state) 1) + ((> (nth 1 state) 0) 1) + (t (funcall proof-stack-to-indent (nth 2 state)))))) + (skip-chars-forward "\t ") + (if (not (eq (current-indentation) indent)) + (progn (delete-region beg (point)) + (indent-to indent))))) + (skip-chars-forward "\t "))) + +(defun proof-indent-region (start end) + (interactive "r") + (if (and (eq proof-script-buffer (current-buffer)) + (< (point) (proof-locked-end))) + (error "can't indent locked region!")) + (save-excursion + (goto-char start) + (beginning-of-line) + (let* ((beg (point)) + (state (proof-parse-to-point)) + indent) + ;; End of region changes with new indentation + (while (< (point) end) + (setq indent + (cond ((car state) 1) + ((> (nth 1 state) 0) 1) + (t (funcall proof-stack-to-indent (nth 2 state))))) + (skip-chars-forward "\t ") + (let ((diff (- (current-indentation) indent))) + (if (not (eq diff 0)) + (progn + (delete-region beg (point)) + (indent-to indent) + (setq end (- end diff))))) + (end-of-line) + (if (< (point) (point-max)) (forward-char)) + (setq state (proof-parse-to-point beg state) + beg (point)))))) + +(provide 'proof-indent)
\ No newline at end of file diff --git a/proof-syntax.el b/proof-syntax.el new file mode 100644 index 00000000..45c9015d --- /dev/null +++ b/proof-syntax.el @@ -0,0 +1,146 @@ +;; proof-syntax.el Generic font lock expressions +;; Copyright (C) 1997 LFCS Edinburgh. +;; Author: Healfdene Goguen, Thomas Kleymann and Dilip Sequiera +;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> + +;; $Log$ +;; Revision 2.0 1998/08/11 15:00:04 da +;; New branch +;; +;; Revision 1.2 1998/08/11 11:43:14 da +;; Renamed <file>-fontlock to <file>-syntax +;; +;; Revision 1.8 1998/06/10 11:45:12 hhg +;; Changed "\\s " to "\\s-" in proof-id as whitespace pattern. +;; +;; Revision 1.7 1998/05/29 09:49:53 tms +;; o outsourced indentation to proof-indent +;; o support indentation of commands +;; o replaced test of Emacs version with availability test of specific +;; features +;; o C-c C-c, C-c C-v and M-tab is now available in all buffers +;; +;; Revision 1.6 1998/05/06 15:56:14 hhg +;; Fixed problem introduced by working on emacs19 in +;; proof-zap-commas-region. +;; +;; Revision 1.5 1998/05/05 14:25:45 hhg +;; Simple white-space changes. +;; +;; Revision 1.4 1998/01/16 15:40:28 djs +;; Commented the code of proof.el and lego.el a bit. Made a minor change +;; to the way errors are handled, so that any delayed output is inserted +;; in the buffer before the error message is printed. +;; +;; Revision 1.3 1997/11/17 17:11:19 djs +;; Added some magic commands: proof-frob-locked-end, proof-try-command, +;; proof-interrupt-process. Added moving nested lemmas above goal for coq. +;; Changed the key mapping for assert-until-point to C-c RET. +;; +;; Revision 1.2 1997/10/13 17:13:50 tms +;; *** empty log message *** +;; +;; Revision 1.1.2.1 1997/10/07 13:34:27 hhg +;; New structure to share as much as possible between LEGO and Coq. +;; +;; + +(require 'font-lock) + +;;; FIXME: change this to proof- +(defun ids-to-regexp (l) + "transforms a non-empty list of identifiers `l' into a regular + expression matching any of its elements" + (mapconcat (lambda (s) (concat "\\<" s "\\>")) l "\\|")) + +;; Generic font-lock + +;; proof-commands-regexp is used for indentation +(defvar proof-commands-regexp "" + "Subset of keywords and tacticals which are terminated by the + `proof-terminal-char'") + + +(defvar proof-id "\\(\\w\\(\\w\\|\\s_\\)*\\)" + "A regular expression for parsing identifiers.") + +;; For font-lock, we treat ,-separated identifiers as one identifier +;; and refontify commata using \{proof-unfontify-separator}. + +(defun proof-ids (proof-id) + "Function to generate a regular expression for separated lists of + identifiers." + (concat proof-id "\\(\\s-*,\\s-*" proof-id "\\)*")) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; font lock faces: declarations, errors, tacticals ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun proof-have-color () + ()) + +(defvar font-lock-declaration-name-face +(progn + (cond + ((proof-have-color) + (copy-face 'bold 'font-lock-declaration-name-face) + + ;; Emacs 19.28 compiles this down to + ;; internal-set-face-1. This is not compatible with XEmacs + (set-face-foreground + 'font-lock-declaration-name-face "chocolate")) + (t (copy-face 'bold-italic 'font-lock-declaration-name-face))))) + +;; (if running-emacs19 +;; (setq font-lock-declaration-name-face +;; (face-name 'font-lock-declaration-name-face)) + +(defvar font-lock-tacticals-name-face +(if (proof-have-color) + (let ((face (make-face 'font-lock-tacticals-name-face))) + (dont-compile + (set-face-foreground face "MediumOrchid3")) + face) + (copy-face 'bold 'font-lock-tacticals-name-face))) + +(defvar font-lock-error-face +(if (proof-have-color) + (let ((face (make-face 'font-lock-error-face))) + (dont-compile + (set-face-foreground face "red")) + face) + (copy-face 'bold 'font-lock-error-face))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; A big hack to unfontify commas in declarations and definitions. ;; +;; All that can be said for it is that the previous way of doing ;; +;; this was even more bogus. ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; Refontify the whole line, 'cos that's what font-lock-after-change +;; does. + +(defun proof-zap-commas-region (start end length) + (save-excursion + (let + ((start (progn (goto-char start) (beginning-of-line) (point))) + (end (progn (goto-char end) (end-of-line) (point)))) + (goto-char start) + (while (search-forward "," end t) + (if (memq (get-char-property (- (point) 1) 'face) + '(font-lock-declaration-name-face + font-lock-function-name-face)) + (font-lock-remove-face (- (point) 1) (point)) + ))))) + +(defun proof-zap-commas-buffer () + (proof-zap-commas-region (point-min) (point-max) 0)) + +(defun proof-unfontify-separator () + (make-local-variable 'after-change-functions) + (setq after-change-functions + (append (delq 'proof-zap-commas-region after-change-functions) + '(proof-zap-commas-region)))) + + +(provide 'proof-syntax) diff --git a/proof.el b/proof.el new file mode 100644 index 00000000..9e6866e8 --- /dev/null +++ b/proof.el @@ -0,0 +1,1818 @@ +;; proof.el Major mode for proof assistants +;; Copyright (C) 1994 - 1998 LFCS Edinburgh. +;; Authors: David Aspinall, Yves Bertot, Healfdene Goguen, +;; Thomas Kleymann and Dilip Sequeira + +;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> +;; Thanks to Robert Boyer, Rod Burstall, +;; James McKinna, Mark Ruys, Martin Steffen, Perdita Stevens + + +(require 'cl) +(require 'compile) +(require 'comint) +(require 'etags) +(cond ((fboundp 'make-extent) (require 'span-extent)) + ((fboundp 'make-overlay) (require 'span-overlay)) + (t nil)) +(require 'proof-syntax) +(require 'proof-indent) +(require 'easymenu) +(require 'tl-list) + +(autoload 'w3-fetch "w3" nil t) + +(defmacro deflocal (var value docstring) + (list 'progn + (list 'defvar var 'nil docstring) + (list 'make-variable-buffer-local (list 'quote var)) + (list 'setq var value))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Configuration ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconst proof-mode-version-string + "PROOF-MODE. ALPHA Version 2 (August 1998) LEGO Team <lego@dcs.ed.ac.uk>") + +(defvar proof-assistant "" + "Name of the proof assistant") + +(defvar proof-www-home-page "" + "Web address for information on proof assistant") + +(defvar proof-shell-cd nil + "*Command of the inferior process to change the directory.") + +(defconst proof-info-dir "/usr/local/share/info" + "Directory to search for Info documents on Script Management.") + +(defvar proof-universal-keys + (list (cons '[(control c) (control c)] 'proof-interrupt-process) + (cons '[(control c) (control v)] + 'proof-execute-minibuffer-cmd) + (cons '[(meta tab)] 'tag-complete-symbol)) + "List of keybindings which are valid in both in the script and the + response buffer. Elements of the list are tuples (k . f) + where `k' is a keybinding (vector) and `f' the designated function.") + +(defvar proof-prog-name-ask-p nil + "*If t, you will be asked which program to run when the inferior + process starts up.") + +(defvar proof-shell-process-output-system-specific nil + "*Errors, start of proofs, abortions of proofs and completions of + proofs are recognised in the function `proof-shell-process-output'. + All other output from the proof engine is simply reported to the + user in the RESPONSE buffer. + + To catch further special cases, set this variable to a tuple of + functions '(condf . actf). Both are given (cmd string) as arguments. + `cmd' is a string containing the currently processed command. + `string' is the response from the proof system. To change the + behaviour of `proof-shell-process-output', (condf cmd string) must + return a non-nil value. Then (actf cmd string) is invoked. See the + documentation of `proof-shell-process-output' for the required + output format.") + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Other buffer-local variables used by proof mode ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; These should be set before proof-config-done is called + +(defvar proof-terminal-char nil "terminator character") + +(defvar proof-comment-start nil "Comment start") +(defvar proof-comment-end nil "Comment end") + +(defvar proof-save-command-regexp nil "Matches a save command") +(defvar proof-save-with-hole-regexp nil "Matches a named save command") +(defvar proof-goal-with-hole-regexp nil "Matches a saved goal command") + +(defvar proof-goal-command-p nil "Is this a goal") +(defvar proof-count-undos-fn nil "Compute number of undos in a target segment") +(defvar proof-find-and-forget-fn nil "Compute command to forget up to point") +(defvar proof-goal-hyp-fn nil "Is point at goal or hypothesis") +(defvar proof-kill-goal-command nil "How to kill a goal.") +(defvar proof-global-p nil "Is this a global declaration") + +(defvar proof-state-preserving-p nil + "whether a command preserves the proof state") + +(defvar pbp-change-goal nil + "*Command to change to the goal %s") + +;; these should be set in proof-pre-shell-start-hook + +(defvar proof-prog-name nil "program name for proof shell") +(defvar proof-mode-for-shell nil "mode for proof shell") +(defvar proof-mode-for-pbp nil "The actual mode for Proof-by-Pointing.") +(defvar proof-shell-insert-hook nil + "Function to config proof-system to interface") + +(defvar proof-pre-shell-start-hook) +(defvar proof-post-shell-exit-hook) + +(defvar proof-shell-prompt-pattern nil + "comint-prompt-pattern for proof shell") + +(defvar proof-shell-init-cmd nil + "The command for initially configuring the proof process") + +(defvar proof-shell-handle-delayed-output-hook + '(proof-pbp-focus-on-first-goal) + "*This hook is called after output from the PROOF process has been + displayed in the RESPONSE buffer.") + +(defvar proof-shell-handle-error-hook + '(proof-goto-end-of-locked-if-pos-not-visible-in-window) + "*This hook is called after an error has been reported in the + RESPONSE buffer.") + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Generic config for script management ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defvar proof-shell-wakeup-char nil + "A character terminating the prompt in annotation mode") + +(defvar proof-shell-annotated-prompt-regexp "" + "Annotated prompt pattern") + +(defvar proof-shell-abort-goal-regexp nil + "*Regular expression indicating that the proof of the current goal + has been abandoned.") + +(defvar proof-shell-error-regexp nil + "A regular expression indicating that the PROOF process has + identified an error.") + +(defvar proof-shell-interrupt-regexp nil + "A regular expression indicating that the PROOF process has + responded to an interrupt.") + +(defvar proof-shell-proof-completed-regexp nil + "*Regular expression indicating that the proof has been completed.") + +(defvar proof-shell-result-start "" + "String indicating the start of an output from the prover following + a `pbp-goal-command' or a `pbp-hyp-command'.") + +(defvar proof-shell-result-end "" + "String indicating the end of an output from the prover following a + `pbp-goal-command' or a `pbp-hyp-command'.") + +(defvar proof-shell-start-goals-regexp "" + "String indicating the start of the proof state.") + +(defvar proof-shell-end-goals-regexp "" + "String indicating the end of the proof state.") + +(defvar pbp-error-regexp nil + "A regular expression indicating that the PROOF process has + identified an error.") + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Internal variables used by scripting and pbp ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defvar proof-mode-name "Proof") + +(defvar proof-shell-echo-input t + "If nil, input to the proof shell will not be echoed") + +(defvar proof-terminal-string nil + "End-of-line string for proof process.") + +(defvar proof-re-end-of-cmd nil + "You are not authorised for this information.") + +(defvar proof-re-term-or-comment nil + "You are not authorised for this information.") + +(defvar proof-marker nil + "You are not authorised for this information.") + +(defvar proof-shell-buffer nil + "You are not authorised for this information.") + +(defvar proof-script-buffer nil + "You are not authorised for this information.") + +(defvar proof-pbp-buffer nil + "You are not authorised for this information.") + +(defvar proof-shell-busy nil + "You are not authorised for this information.") + +(deflocal proof-buffer-type nil + "You are not authorised for this information.") + +(defvar proof-action-list nil "action list") + +(defvar proof-included-files-list nil + "Files currently included in proof process") + +(deflocal proof-active-buffer-fake-minor-mode nil + "An indication in the modeline that this is the *active* buffer") + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; A couple of small utilities ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun proof-define-keys (map kbl) + "Adds keybindings `kbl' in `map'. The argument `kbl' is a list of + tuples (k . f) where `k' is a keybinding (vector) and `f' the + designated function." + (mapcar + (lambda (kbl) + (let ((k (car kbl)) (f (cdr kbl))) + (define-key map k f))) + kbl)) + +(defun proof-string-to-list (s separator) + "converts strings `s' separated by the character `separator' to a + list of words" + (let ((end-of-word-occurence (string-match (concat separator "+") s))) + (if (not end-of-word-occurence) + (if (string= s "") + nil + (list s)) + (cons (substring s 0 end-of-word-occurence) + (proof-string-to-list + (substring s + (string-match (concat "[^" separator "]") + s end-of-word-occurence)) separator))))) + +(defun w3-remove-file-name (address) + "remove the file name in a World Wide Web address" + (string-match "://[^/]+/" address) + (concat (substring address 0 (match-end 0)) + (file-name-directory (substring address (match-end 0))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Basic code for the locked region and the queue region ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defvar proof-locked-hwm nil + "Upper limit of the locked region") + +(defvar proof-queue-loose-end nil + "Limit of the queue region that is not equal to proof-locked-hwm.") + +(defvar proof-locked-span nil + "Upper limit of the locked region") + +(defvar proof-queue-span nil + "Upper limit of the locked region") + +(make-variable-buffer-local 'proof-locked-span) +(make-variable-buffer-local 'proof-queue-span) + +(defun proof-init-segmentation () + (setq proof-queue-loose-end nil) + (if (not proof-queue-span) + (setq proof-queue-span (make-span 1 1))) + (set-span-property proof-queue-span 'start-closed t) + (set-span-property proof-queue-span 'end-open t) + (span-read-only proof-queue-span) + + (make-face 'proof-queue-face) + ;; Whether display has color or not + (cond ((and (fboundp 'device-class) + (eq (device-class (frame-device)) 'color)) + (set-face-background 'proof-queue-face "mistyrose")) + ((and (fboundp 'x-display-color-p) (x-display-color-p)) + (set-face-background 'proof-queue-face "mistyrose")) + (t (progn + (set-face-background 'proof-queue-face "Black") + (set-face-foreground 'proof-queue-face "White")))) + (set-span-property proof-queue-span 'face 'proof-queue-face) + + (detach-span proof-queue-span) + + (setq proof-locked-hwm nil) + (if (not proof-locked-span) + (setq proof-locked-span (make-span 1 1))) + (set-span-property proof-locked-span 'start-closed t) + (set-span-property proof-locked-span 'end-open t) + (span-read-only proof-locked-span) + + (make-face 'proof-locked-face) + ;; Whether display has color or not + (cond ((and (fboundp 'device-class) + (eq (device-class (frame-device)) 'color)) + (set-face-background 'proof-locked-face "lavender")) + ((and (fboundp 'x-display-color-p) (x-display-color-p)) + (set-face-background 'proof-locked-face "lavender")) + (t (set-face-property 'proof-locked-face 'underline t))) + (set-span-property proof-locked-span 'face 'proof-locked-face) + + (detach-span proof-locked-span)) + +(defsubst proof-lock-unlocked () + (span-read-only proof-locked-span)) + +(defsubst proof-unlock-locked () + (span-read-write proof-locked-span)) + +(defsubst proof-set-queue-endpoints (start end) + (set-span-endpoints proof-queue-span start end)) + +(defsubst proof-set-locked-endpoints (start end) + (set-span-endpoints proof-locked-span start end)) + +(defsubst proof-detach-queue () + (and proof-queue-span (detach-span proof-queue-span))) + +(defsubst proof-detach-locked () + (and proof-locked-span (detach-span proof-locked-span))) + +(defsubst proof-set-queue-start (start) + (set-span-endpoints proof-queue-span start (span-end proof-queue-span))) + +(defsubst proof-set-queue-end (end) + (set-span-endpoints proof-queue-span (span-start proof-queue-span) end)) + +(defun proof-detach-segments () + (proof-detach-queue) + (proof-detach-locked)) + +(defsubst proof-set-locked-end (end) + (if (>= (point-min) end) + (proof-detach-locked) + (set-span-endpoints proof-locked-span (point-min) end))) + +(defun proof-unprocessed-begin () + "proof-unprocessed-begin returns end of locked region in script + buffer and point-min otherwise." + (or + (and (eq proof-script-buffer (current-buffer)) + proof-locked-span (span-end proof-locked-span)) + (point-min))) + +(defun proof-locked-end () + "proof-locked-end returns the end of the locked region. It should + only be called if we're in the scripting buffer." + (if (eq proof-script-buffer (current-buffer)) + (proof-unprocessed-begin) + (error "bug: proof-locked-end called from wrong buffer"))) + +(defsubst proof-end-of-queue () + (and proof-queue-span (span-end proof-queue-span))) + +(defun proof-dont-show-annotations () + "This sets the display values of the annotations used to + communicate with the proof assistant so that they don't show up on + the screen." + (let ((disp (make-display-table)) + (i 128)) + (while (< i 256) + (aset disp i []) + (incf i)) + (cond ((fboundp 'add-spec-to-specifier) + (add-spec-to-specifier current-display-table disp + (current-buffer))) + ((boundp 'buffer-display-table) + (setq buffer-display-table disp))))) + +;;; in case Emacs is not aware of read-shell-command-map + +(defvar read-shell-command-map + (let ((map (make-sparse-keymap))) + (if (not (fboundp 'set-keymap-parents)) + (setq map (append minibuffer-local-map map)) + (set-keymap-parents map minibuffer-local-map) + (set-keymap-name map 'read-shell-command-map)) + (define-key map "\t" 'comint-dynamic-complete) + (define-key map "\M-\t" 'comint-dynamic-complete) + (define-key map "\M-?" 'comint-dynamic-list-completions) + map) + "Minibuffer keymap used by shell-command and related commands.") + + +;;; in case Emacs is not aware of the function read-shell-command +(or (fboundp 'read-shell-command) + ;; from minibuf.el distributed with XEmacs 19.11 + (defun read-shell-command (prompt &optional initial-input history) + "Just like read-string, but uses read-shell-command-map: +\\{read-shell-command-map}" + (let ((minibuffer-completion-table nil)) + (read-from-minibuffer prompt initial-input read-shell-command-map + nil (or history + 'shell-command-history))))) + +;; The package fume-func provides a function with the same name and +;; specification. However, fume-func's version is incorrect. +(and (fboundp 'fume-match-find-next-function-name) +(defun fume-match-find-next-function-name (buffer) + "General next function name in BUFFER finder using match. + The regexp is assumed to be a two item list the car of which is the regexp + to use, and the cdr of which is the match position of the function name" + (set-buffer buffer) + (let ((r (car fume-function-name-regexp)) + (p (cdr fume-function-name-regexp))) + (and (re-search-forward r nil t) + (cons (buffer-substring (setq p (match-beginning p)) (point)) p))))) + +(defun proof-goto-end-of-locked-interactive () + "Jump to the end of the locked region." + (interactive) + (switch-to-buffer proof-script-buffer) + (goto-char (proof-locked-end))) + +(defun proof-goto-end-of-locked () + "Jump to the end of the locked region." + (goto-char (proof-locked-end))) + +(defun proof-goto-end-of-locked-if-pos-not-visible-in-window () + "If the end of the locked region is not visible, jump to the end of + the locked region." + (interactive) + (let ((pos (save-excursion + (set-buffer proof-script-buffer) + (proof-locked-end)))) + (or (pos-visible-in-window-p pos (get-buffer-window + proof-script-buffer t)) + (proof-goto-end-of-locked-interactive)))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Starting and stopping the proof-system shell ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun proof-shell-live-buffer () + (and proof-shell-buffer + (comint-check-proc proof-shell-buffer) + proof-shell-buffer)) + +(defun proof-start-shell () + (if (proof-shell-live-buffer) + () + (run-hooks 'proof-pre-shell-start-hook) + (setq proof-included-files-list nil) + (if proof-prog-name-ask-p + (save-excursion + (setq proof-prog-name (read-shell-command "Run process: " + proof-prog-name)))) + (let ((proc + (concat "Inferior " + (substring proof-prog-name + (string-match "[^/]*$" proof-prog-name))))) + (while (get-buffer (concat "*" proc "*")) + (if (string= (substring proc -1) ">") + (aset proc (- (length proc) 2) + (+ 1 (aref proc (- (length proc) 2)))) + (setq proc (concat proc "<2>")))) + + (message (format "Starting %s process..." proc)) + + ;; Starting the inferior process (asynchronous) + (let ((prog-name-list (proof-string-to-list proof-prog-name " "))) + (apply 'make-comint (append (list proc (car prog-name-list) nil) + (cdr prog-name-list)))) + ;; To send any initialisation commands to the inferior process, + ;; consult proof-shell-config-done... + + (setq proof-shell-buffer (get-buffer (concat "*" proc "*"))) + (setq proof-pbp-buffer (get-buffer-create (concat "*" proc "-goals*"))) + + (save-excursion + (set-buffer proof-shell-buffer) + (funcall proof-mode-for-shell) + (set-buffer proof-pbp-buffer) + (funcall proof-mode-for-pbp)) + + (setq proof-script-buffer (current-buffer)) + (proof-init-segmentation) + (setq proof-active-buffer-fake-minor-mode t) + + (if (fboundp 'redraw-modeline) + (redraw-modeline) + (force-mode-line-update)) + + (or (assq 'proof-active-buffer-fake-minor-mode minor-mode-alist) + (setq minor-mode-alist + (append minor-mode-alist + (list '(proof-active-buffer-fake-minor-mode + " Scripting"))))) + + (message + (format "Starting %s process... done." proc))))) + + +(defun proof-stop-shell () + "Exit the PROOF process + + Runs proof-shell-exit-hook if non nil" + + (interactive) + (save-excursion + (let ((buffer (proof-shell-live-buffer)) (proc)) + (if buffer + (progn + (save-excursion + (set-buffer buffer) + (setq proc (process-name (get-buffer-process))) + (comint-send-eof) + (save-excursion + (set-buffer proof-script-buffer) + (proof-detach-segments)) + (kill-buffer)) + (run-hooks 'proof-shell-exit-hook) + + ;;it is important that the hooks are + ;;run after the buffer has been killed. In the reverse + ;;order e.g., intall-shell-fonts causes problems and it + ;;is impossible to restart the PROOF shell + + (message (format "%s process terminated." proc))))))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Proof by pointing ;; +;; All very lego-specific at present ;; +;; To make sense of this code, you should read the ;; +;; relevant LFCS tech report by tms, yb, and djs ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defvar pbp-goal-command nil + "Command informing the prover that `pbp-button-action' has been + requested on a goal.") + +(defvar pbp-hyp-command nil + "Command informing the prover that `pbp-button-action' has been + requested on an assumption.") + +(defun pbp-button-action (event) + (interactive "e") + (mouse-set-point event) + (pbp-construct-command)) + +; Using the spans in a mouse behavior is quite simple: from the +; mouse position, find the relevant span, then get its annotation +; and produce a piece of text that will be inserted in the right +; buffer. + +(defun proof-expand-path (string) + (let ((a 0) (l (length string)) ls) + (while (< a l) + (setq ls (cons (int-to-string (aref string a)) + (cons " " ls))) + (incf a)) + (apply 'concat (nreverse ls)))) + +(defun proof-send-span (event) + (interactive "e") + (let* ((span (span-at (mouse-set-point event) 'type)) + (str (span-property span 'cmd))) + (cond ((and (eq proof-script-buffer (current-buffer)) (not (null span))) + (proof-goto-end-of-locked) + (cond ((eq (span-property span 'type) 'vanilla) + (insert str))))))) + +(defun pbp-construct-command () + (let* ((span (span-at (point) 'proof)) + (top-span (span-at (point) 'proof-top-element)) + top-info) + (if (null top-span) () + (setq top-info (span-property top-span 'proof-top-element)) + (pop-to-buffer proof-script-buffer) + (cond + (span + (proof-invisible-command + (format (if (eq 'hyp (car top-info)) pbp-hyp-command + pbp-goal-command) + (concat (cdr top-info) (proof-expand-path + (span-property span 'proof)))))) + ((eq (car top-info) 'hyp) + (proof-invisible-command (format pbp-hyp-command (cdr top-info)))) + (t + (proof-insert-pbp-command (format pbp-change-goal (cdr top-info)))))) + )) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Turning annotated output into pbp goal set ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defvar proof-shell-first-special-char nil "where the specials start") +(defvar proof-shell-goal-char nil "goal mark") +(defvar proof-shell-start-char nil "annotation start") +(defvar proof-shell-end-char nil "annotation end") +(defvar proof-shell-field-char nil "annotated field end") +(defvar proof-shell-eager-annotation-start nil "eager ann. field start") +(defvar proof-shell-eager-annotation-end nil "eager ann. field end") + +(defvar proof-shell-assumption-regexp nil + "A regular expression matching the name of assumptions.") + +;; FIXME: da: where is this variable used? +;; dropped in favour of goal-char? +(defvar proof-shell-goal-regexp nil + "A regular expressin matching the identifier of a goal.") + +(defvar proof-shell-noise-regexp nil + "Unwanted information output from the proof process within + `proof-start-goals-regexp' and `proof-end-goals-regexp'.") + +(defun pbp-make-top-span (start end) + (let (span name) + (goto-char start) + (setq name (funcall proof-goal-hyp-fn)) + (beginning-of-line) + (setq start (point)) + (goto-char end) + (beginning-of-line) + (backward-char) + (setq span (make-span start (point))) + (set-span-property span 'mouse-face 'highlight) + (set-span-property span 'proof-top-element name))) + + +;; Need this for processing error strings and so forth + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; The filter. First some functions that handle those few ;; +;; occasions when the glorious illusion that is script-management ;; +;; is temporarily suspended ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; Output from the proof process is handled lazily, so that only +;; the output from the last of multiple commands is actually +;; processed (assuming they're all successful) + +(defvar proof-shell-delayed-output nil + "The last interesting output the proof process output, and what to do + with it.") + +(defvar proof-analyse-using-stack nil + "Are annotations sent by proof assistant local or global") + +;; FIXME: da: what's magical value 128 below? should be in defconst? +(defun proof-shell-analyse-structure (string) + (save-excursion + (let* ((ip 0) (op 0) ap (l (length string)) + (ann (make-string (length string) ?x)) + (stack ()) (topl ()) + (out (make-string l ?x)) c span) + (while (< ip l) + (if (< (setq c (aref string ip)) 128) + (progn (aset out op c) + (incf op))) + (incf ip)) + (display-buffer (set-buffer proof-pbp-buffer)) + (erase-buffer) + (insert (substring out 0 op)) + + (setq ip 0 + op 1) + (while (< ip l) + (setq c (aref string ip)) + (cond + ((= c proof-shell-goal-char) + (setq topl (cons op topl)) + (setq ap 0)) + ((= c proof-shell-start-char) + (if proof-analyse-using-stack + (setq ap (- ap (- (aref string (incf ip)) 128))) + (setq ap (- (aref string (incf ip)) 128))) + (incf ip) + (while (not (= (setq c (aref string ip)) proof-shell-end-char)) + (aset ann ap (- c 128)) + (incf ap) + (incf ip)) + (setq stack (cons op (cons (substring ann 0 ap) stack)))) + ((= c proof-shell-field-char) + (setq span (make-span (car stack) op)) + (set-span-property span 'mouse-face 'highlight) + (set-span-property span 'proof (car (cdr stack))) + ;; Pop annotation off stack + (and proof-analyse-using-stack + (progn + (setq ap 0) + (while (< ap (length (cadr stack))) + (aset ann ap (aref (cadr stack) ap)) + (incf ap)))) + ;; Finish popping annotations + (setq stack (cdr (cdr stack)))) + (t (incf op))) + (incf ip)) + (setq topl (reverse (cons (point-max) topl))) + ;; If we want Coq pbp: (setq coq-current-goal 1) + (while (setq ip (car topl) + topl (cdr topl)) + (pbp-make-top-span ip (car topl)))))) + +(defun proof-shell-strip-annotations (string) + (let* ((ip 0) (op 0) (l (length string)) (out (make-string l ?x ))) + (while (< ip l) + (if (>= (aref string ip) proof-shell-first-special-char) + (if (char-equal (aref string ip) proof-shell-start-char) + (progn (incf ip) + (while (< (aref string ip) proof-shell-first-special-char) + (incf ip)))) + (aset out op (aref string ip)) + (incf op)) + (incf ip)) + (substring out 0 op))) + +(defun proof-shell-handle-delayed-output () + (let ((ins (car proof-shell-delayed-output)) + (str (cdr proof-shell-delayed-output))) + (display-buffer proof-pbp-buffer) + (save-excursion + (cond + ((eq ins 'insert) + (setq str (proof-shell-strip-annotations str)) + (set-buffer proof-pbp-buffer) + (erase-buffer) + (insert str)) + ((eq ins 'analyse) + (proof-shell-analyse-structure str)) + (t (set-buffer proof-pbp-buffer) + (insert "\n\nbug???"))))) + (run-hooks 'proof-shell-handle-delayed-output-hook) + (setq proof-shell-delayed-output (cons 'insert "done"))) + +(defun proof-shell-handle-error (cmd string) + (save-excursion + (display-buffer (set-buffer proof-pbp-buffer)) + (if (not (eq proof-shell-delayed-output (cons 'insert "done"))) + (progn + (set-buffer proof-pbp-buffer) + (erase-buffer) + (insert (proof-shell-strip-annotations + (cdr proof-shell-delayed-output))))) + (goto-char (point-max)) + (if (re-search-backward pbp-error-regexp nil t) + (delete-region (- (point) 2) (point-max))) + (newline 2) + (insert-string string) + (beep)) + (set-buffer proof-script-buffer) + (proof-detach-queue) + (delete-spans (proof-locked-end) (point-max) 'type) + (proof-release-lock) + (run-hooks 'proof-shell-handle-error-hook)) + +(defun proof-shell-handle-interrupt () + (save-excursion + (display-buffer (set-buffer proof-pbp-buffer)) + (goto-char (point-max)) + (newline 2) + (insert-string + "Interrupt: Script Management may be in an inconsistent state\n") + (beep)) + (set-buffer proof-script-buffer) + (if proof-shell-busy + (progn (proof-detach-queue) + (delete-spans (proof-locked-end) (point-max) 'type) + (proof-release-lock)))) + + +(defun proof-goals-pos (span maparg) + "Given a span, this function returns the start of it if corresponds + to a goal and nil otherwise." + (and (eq 'goal (car (span-property span 'proof-top-element))) + (span-start span))) + +(defun proof-pbp-focus-on-first-goal () + "If the `proof-pbp-buffer' contains goals, the first one is brought + into view." + (and (fboundp 'map-extents) + (let + ((pos (map-extents 'proof-goals-pos proof-pbp-buffer + nil nil nil nil 'proof-top-element))) + (and pos (set-window-point + (get-buffer-window proof-pbp-buffer t) pos))))) + + + +(defun proof-shell-process-output (cmd string) + "Deals with errors, start of proofs, abortions of proofs and + completions of proofs. All other output from the proof engine is + simply reported to the user in the RESPONSE buffer. To extend this + function, set `proof-shell-process-output-system-specific'. + + The basic output processing function - it can return one of 4 + things: 'error, 'interrupt, 'loopback, or nil. 'loopback means this + was output from pbp, and should be inserted into the script buffer + and sent back to the proof assistant." + (cond + ((string-match proof-shell-error-regexp string) + (cons 'error (proof-shell-strip-annotations + (substring string (match-beginning 0))))) + + ((string-match proof-shell-interrupt-regexp string) + 'interrupt) + + ((and proof-shell-abort-goal-regexp + (string-match proof-shell-abort-goal-regexp string)) + (setq proof-shell-delayed-output (cons 'insert "\n\nAborted")) + ()) + + ((string-match proof-shell-proof-completed-regexp string) + (setq proof-shell-delayed-output + (cons 'insert (concat "\n" (match-string 0 string))))) + + ((string-match proof-shell-start-goals-regexp string) + (let (start end) + (while (progn (setq start (match-end 0)) + (string-match proof-shell-start-goals-regexp + string start))) + (setq end (string-match proof-shell-end-goals-regexp string start)) + (setq proof-shell-delayed-output + (cons 'analyse (substring string start end))))) + + ((string-match proof-shell-result-start string) + (let (start end) + (setq start (+ 1 (match-end 0))) + (string-match proof-shell-result-end string) + (setq end (- (match-beginning 0) 1)) + (cons 'loopback (substring string start end)))) + + ;; hook to tailor proof-shell-process-output to a specific proof + ;; system + ((and proof-shell-process-output-system-specific + (funcall (car proof-shell-process-output-system-specific) + cmd string)) + (funcall (cdr proof-shell-process-output-system-specific) + cmd string)) + + (t (setq proof-shell-delayed-output (cons 'insert string))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Low-level commands for shell communication ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun proof-shell-insert (string) + (set-buffer proof-shell-buffer) + (goto-char (point-max)) + + (run-hooks 'proof-shell-insert-hook) + (insert string) + + ;; xemacs and emacs19 have different semantics for what happens when + ;; shell input is sent next to a marker + ;; the following code accommodates both definitions + (if (marker-position proof-marker) + (let ((inserted (point))) + (comint-send-input) + (set-marker proof-marker inserted)) + (comint-send-input))) + +(defun proof-send (string) + (let ((l (length string)) (i 0)) + (while (< i l) + (if (= (aref string i) ?\n) (aset string i ?\ )) + (incf i))) + (save-excursion (proof-shell-insert string))) + +;; Note that this is not really intended for anything complicated - +;; just to stop the user accidentally sending a command while the +;; queue is running. +(defun proof-check-process-available (&optional relaxed) + "Checks + (1) Is a proof process running? + (2) Is the proof process idle? + (3) Does the current buffer own the proof process? + (4) Is the current buffer a proof script? + and signals an error if at least one of the conditions is not + fulfilled. If relaxed is set, only (1) and (2) are tested." + (if (proof-shell-live-buffer) + (cond + (proof-shell-busy (error "Proof Process Busy!")) + (relaxed ()) ;exit cond + ((not (eq proof-script-buffer (current-buffer))) + (error "Don't own proof process")))) + (if (not (or relaxed (eq proof-buffer-type 'script))) + (error "Must be running in a script buffer"))) + +(defun proof-grab-lock (&optional relaxed) + (proof-start-shell) + (proof-check-process-available relaxed) + (setq proof-shell-busy t)) + +(defun proof-release-lock () + (if (proof-shell-live-buffer) + (progn + (if (not proof-shell-busy) + (error "Bug: Proof process not busy")) + (if (not (eq proof-script-buffer (current-buffer))) + (error "Bug: Don't own process")) + (setq proof-shell-busy nil)))) + +; Pass start and end as nil if the cmd isn't in the buffer. + +(defun proof-start-queue (start end alist &optional relaxed) + (if start + (proof-set-queue-endpoints start end)) + (let (item) + (while (and alist (string= + (nth 1 (setq item (car alist))) + "COMMENT")) + (funcall (nth 2 item) (car item)) + (setq alist (cdr alist))) + (if alist + (progn + (proof-grab-lock relaxed) + (setq proof-shell-delayed-output (cons 'insert "Done.")) + (setq proof-action-list alist) + (proof-send (nth 1 item)))))) + +; returns t if it's run out of input + +(defun proof-shell-exec-loop () + (save-excursion + (set-buffer proof-script-buffer) + (if (null proof-action-list) (error "Non Sequitur")) + (let ((item (car proof-action-list))) + (funcall (nth 2 item) (car item)) + (setq proof-action-list (cdr proof-action-list)) + (while (and proof-action-list + (string= + (nth 1 (setq item (car proof-action-list))) + "COMMENT")) + (funcall (nth 2 item) (car item)) + (setq proof-action-list (cdr proof-action-list))) + (if (null proof-action-list) + (progn (proof-release-lock) + (proof-detach-queue) + t) + (proof-send (nth 1 item)) + nil)))) + +(defun proof-shell-insert-loopback-cmd (cmd) + "Insert command sequence triggered by the proof process +at the end of locked region (after inserting a newline and indenting)." + (save-excursion + (set-buffer proof-script-buffer) + (let (span) + (proof-goto-end-of-locked) + (newline-and-indent) + (insert cmd) + (setq span (make-span (proof-locked-end) (point))) + (set-span-property span 'type 'pbp) + (set-span-property span 'cmd cmd) + (proof-set-queue-endpoints (proof-locked-end) (point)) + (setq proof-action-list + (cons (car proof-action-list) + (cons (list span cmd 'proof-done-advancing) + (cdr proof-action-list))))))) + +;; ******** NB ********** +;; While we're using pty communication, this code is OK, since all +;; eager annotations are one line long, and we get input a line at a +;; time. If we go over to piped communication, it will break. + +(defun proof-shell-popup-eager-annotation () + "Eager annotations are annotations which the proof system produces +while it's doing something (e.g. loading libraries) to say how much +progress it's made. Obviously we need to display these as soon as they +arrive." + (let (mrk str file module) + (save-excursion + (goto-char (point-max)) + (search-backward proof-shell-eager-annotation-start) + (setq mrk (+ 1 (point))) + (search-forward proof-shell-eager-annotation-end) + (setq str (buffer-substring mrk (- (point) 1))) + (display-buffer (set-buffer proof-pbp-buffer)) + (goto-char (point-max)) + (insert str "\n")) + (if (string-match "Creating mark \"\\(.*\\)\" \\[\\(.*\\)\\]" str) + (progn + (setq file (match-string 2 str) + module (match-string 1 str)) + (if (string= file "") + (setq file (buffer-file-name proof-script-buffer))) + (setq file (expand-file-name file)) + (if (string-match "\\(.*\\)\\.." file) + (setq file (match-string 1 file))) + (setq proof-included-files-list (cons (cons module file) + proof-included-files-list)))))) + +(defun proof-shell-filter (str) + "The filter for the shell-process. We sleep until we get a + wakeup-char in the input, then run proof-shell-process-output, and + set proof-marker to keep track of how far we've got." + (if (string-match proof-shell-eager-annotation-end str) + (proof-shell-popup-eager-annotation)) + (if (or + ;; Some proof systems can be hacked to have annotated prompts; + ;; for these we set proof-shell-wakeup-char to the annotation special. + (and proof-shell-wakeup-char + (string-match (char-to-string proof-shell-wakeup-char) str)) + ;; Others rely on a standard top-level (e.g. SML) whose prompt can't + ;; be hacked. For those we use the prompt regexp. + (string-match proof-shell-annotated-prompt-regexp str)) + (if (null (marker-position proof-marker)) + ;; Set marker to first prompt in output buffer, and sleep again. + (progn + (goto-char (point-min)) + (re-search-forward proof-shell-annotated-prompt-regexp) + ;; FIXME: da: why is this next line here? to delete the + ;; possibly several character prompt? why? + ;; TMS: Its purpose is to remove the wakeup + ;; character associated with the prompt. This + ;; should not be necessary anymore, because the wakeup + ;; character isn't displayed anyway; see + ;; `proof-dont-show-annotations'. Watch this space! + (backward-delete-char 1) + (set-marker proof-marker (point))) + ;; We've matched against a second prompt in str now. Search + ;; the output buffer for the second prompt after the one previously + ;; marked. + (let (string res cmd) + (goto-char (marker-position proof-marker)) + (re-search-forward proof-shell-annotated-prompt-regexp nil t) + (backward-char (- (match-end 0) (match-beginning 0))) + (setq string (buffer-substring (marker-position proof-marker) + (point))) + (goto-char (point-max)) ; da: assumed to be after a prompt? + (backward-delete-char 1) ; da: WHY? nasty assumption. + (setq cmd (nth 1 (car proof-action-list))) + (save-excursion + (setq res (proof-shell-process-output cmd string)) + (cond + ((and (consp res) (eq (car res) 'error)) + (proof-shell-handle-error cmd (cdr res))) + ((eq res 'interrupt) + (proof-shell-handle-interrupt)) + ((and (consp res) (eq (car res) 'loopback)) + (proof-shell-insert-loopback-cmd (cdr res)) + (proof-shell-exec-loop)) + (t (if (proof-shell-exec-loop) + (proof-shell-handle-delayed-output))))))))) + +(defun proof-last-goal-or-goalsave () + (save-excursion + (let ((span (span-at-before (proof-locked-end) 'type))) + (while (and span + (not (eq (span-property span 'type) 'goalsave)) + (or (eq (span-property span 'type) 'comment) + (not (funcall proof-goal-command-p + (span-property span 'cmd))))) + (setq span (prev-span span 'type))) + span))) + +;; This needs some work to make it generic, since most of the code +;; doesn't apply to Coq at all. +(defun proof-steal-process () + "This allows us to steal the process if we want to change the buffer + in which script management is running." + (proof-start-shell) + (if proof-shell-busy (error "Proof Process Busy!")) + (if (not (eq proof-buffer-type 'script)) + (error "Must be running in a script buffer")) + (cond + ((eq proof-script-buffer (current-buffer)) + nil) + (t + (let ((flist proof-included-files-list) + (file (expand-file-name (buffer-file-name))) span (cmd "")) + (if (string-match "\\(.*\\)\\.." file) (setq file (match-string 1 file))) + (while (and flist (not (string= file (cdr (car flist))))) + (setq flist (cdr flist))) + (if (null flist) + (if (not (y-or-n-p "Steal script management? " )) (error "Aborted")) + (if (not (y-or-n-p "Reprocess this file? " )) (error "Aborted"))) + (if (not (buffer-name proof-script-buffer)) + (message "Warning: Proof script buffer deleted: proof state may be inconsistent") + (save-excursion + (set-buffer proof-script-buffer) + (setq proof-active-buffer-fake-minor-mode nil) + (setq span (proof-last-goal-or-goalsave)) + ;; This won't work for Coq if we have recursive goals in progress + (if (and span (not (eq (span-property span 'type) 'goalsave))) + (setq cmd proof-kill-goal-command)) + (proof-detach-segments) + (delete-spans (point-min) (point-max) 'type))) + + (setq proof-script-buffer (current-buffer)) + (proof-init-segmentation) + (setq proof-active-buffer-fake-minor-mode t) + + (cond + (flist + (list nil (concat cmd "ForgetMark " (car (car flist)) ";") + `(lambda (span) (setq proof-included-files-list + (quote ,(cdr flist)))))) + ((not (string= cmd "")) + (list nil cmd 'proof-done-invisible)) + (t nil)))))) + +(defun proof-done-invisible (span) ()) + +(defun proof-invisible-command (cmd &optional relaxed) + "Send cmd to the proof process without responding to the user." + (proof-check-process-available relaxed) + (if (not (string-match proof-re-end-of-cmd cmd)) + (setq cmd (concat cmd proof-terminal-string))) + (proof-start-queue nil nil (list (list nil cmd + 'proof-done-invisible)) relaxed)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; User Commands ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +; Script management uses two major segments: Locked, which marks text +; which has been sent to the proof assistant and cannot be altered +; without being retracted, and Queue, which contains stuff being +; queued for processing. proof-action-list contains a list of +; (span,command,action) triples. The loop looks like: Execute the +; command, and if it's successful, do action on span. If the +; command's not successful, we bounce the rest of the queue and do +; some error processing. +; +; when a span has been processed, we classify it as follows: +; 'goalsave - denoting a 'goalsave pair in the locked region +; a 'goalsave region has a 'name property which is the name of the goal +; 'comment - denoting a comment +; 'pbp - denoting a span created by pbp +; 'vanilla - denoting any other span. +; 'pbp & 'vanilla spans have a property 'cmd, which says what +; command they contain. + +; We don't allow commands while the queue has anything in it. So we +; do configuration by concatenating the config command on the front in +; proof-send + +;; proof-assert-until-point, and various gunk for its ;; +;; setup and callback ;; + +;; This code is for nested goals in Coq, and shouldn't affect things +;; in LEGO. It lifts "local" lemmas from inside goals out to top +;; level. + +(defun proof-lift-global (glob-span) + (let (start (next (span-at 1 'type)) str (goal-p nil)) + (while (and next (and (not (eq next glob-span)) (not goal-p))) + (if (and (eq (span-property next 'type) 'vanilla) + (funcall proof-goal-command-p (span-property next 'cmd))) + (setq goal-p t) + (setq next (next-span next 'type)))) + + (if (and next (not (eq next glob-span))) + (progn + (proof-unlock-locked) + (setq str (buffer-substring (span-start glob-span) + (span-end glob-span))) + (delete-region (span-start glob-span) (span-end glob-span)) + (goto-char (span-start next)) + (setq start (point)) + (insert str "\n") + (set-span-endpoints glob-span start (point)) + (set-span-start next (point)) + (proof-lock-unlocked))))) + +;; This is the actual callback for assert-until-point. + +(defun proof-done-advancing (span) + (let ((end (span-end span)) nam gspan next cmd) + (proof-set-locked-end end) + (proof-set-queue-start end) + (setq cmd (span-property span 'cmd)) + (cond + ((eq (span-property span 'type) 'comment) + (set-span-property span 'mouse-face 'highlight)) + ((string-match proof-save-command-regexp cmd) + ;; In coq, we have the invariant that if we've done a save and + ;; there's a top-level declaration then it must be the + ;; associated goal. (Notice that because it's a callback it + ;; must have been approved by the theorem prover.) + (if (string-match proof-save-with-hole-regexp cmd) + (setq nam (match-string 2 cmd))) + (setq gspan span) + (while (or (eq (span-property gspan 'type) 'comment) + (not (funcall proof-goal-command-p + (setq cmd (span-property gspan 'cmd))))) + (setq next (prev-span gspan 'type)) + (delete-span gspan) + (setq gspan next)) + + (if (null nam) + (if (string-match proof-goal-with-hole-regexp + (span-property gspan 'cmd)) + (setq nam (match-string 2 (span-property gspan 'cmd))) + ;; This only works for Coq, but LEGO raises an error if + ;; there's no name. + (setq nam "Unnamed_thm"))) + + (set-span-end gspan end) + (set-span-property gspan 'mouse-face 'highlight) + (set-span-property gspan 'type 'goalsave) + (set-span-property gspan 'name nam) + + (proof-lift-global gspan)) + (t + (set-span-property span 'mouse-face 'highlight) + (if (funcall proof-global-p cmd) + (proof-lift-global span)))))) + +; depth marks number of nested comments. quote-parity is false if +; we're inside ""'s. Only one of (depth > 0) and (not quote-parity) +; should be true at once. -- hhg + +(defun proof-segment-up-to (pos) + "Create a list of (type,int,string) pairs from the end of the locked +region to pos, denoting the command and the position of its +terminator. type is one of comment, or cmd. 'unclosed-comment may be +consed onto the start if the segment finishes with an unclosed +comment." + (save-excursion + (let ((str (make-string (- (buffer-size) (proof-locked-end) -10) ?x)) + (i 0) (depth 0) (quote-parity t) done alist c) + (proof-goto-end-of-locked) + (while (not done) + (cond + ((and (= (point) pos) (> depth 0)) + (setq done t alist (cons 'unclosed-comment alist))) + ((= (point) (point-max)) + (if (not quote-parity) + (message "Warning: unclosed quote")) + (setq done t)) + ((and (looking-at "\\*)") quote-parity) + (if (= depth 0) + (progn (message "Warning: extraneous comment end") (setq done t)) + (setq depth (- depth 1)) (forward-char 2) + (if (eq i 0) + (setq alist (cons (list 'comment "" (point)) alist)) + (aset str i ?\ ) (incf i)))) + ((and (looking-at "(\\*") quote-parity) + (setq depth (+ depth 1)) (forward-char 2)) + ((> depth 0) (forward-char)) + (t + (setq c (char-after (point))) + (if (or (> i 0) (not (= (char-syntax c) ?\ ))) + (progn (aset str i c) (incf i))) + (if (looking-at "\"") + (setq quote-parity (not quote-parity))) + (forward-char) + (if (and (= c proof-terminal-char) quote-parity) + (progn + (setq alist + (cons (list 'cmd (substring str 0 i) (point)) alist)) + (if (>= (point) pos) (setq done t) (setq i 0))))))) + alist))) + +(defun proof-semis-to-vanillas (semis &optional callback-fn) + "Convert a sequence of semicolon positions (returned by the above +function) to a set of vanilla extents." + (let ((ct (proof-locked-end)) span alist semi) + (while (not (null semis)) + (setq semi (car semis) + span (make-span ct (nth 2 semi)) + ct (nth 2 semi)) + (if (eq (car (car semis)) 'cmd) + (progn + (set-span-property span 'type 'vanilla) + (set-span-property span 'cmd (nth 1 semi)) + (setq alist (cons (list span (nth 1 semi) + (or callback-fn 'proof-done-advancing)) + alist))) + (set-span-property span 'type 'comment) + (setq alist (cons (list span "COMMENT" 'proof-done-advancing) alist))) + (setq semis (cdr semis))) + (nreverse alist))) + +; Assert until point - We actually use this to implement the +; assert-until-point, active terminator keypress, and find-next-terminator. +; In different cases we want different things, but usually the information +; (i.e. are we inside a comment) isn't available until we've actually run +; proof-segment-up-to (point), hence all the different options when we've +; done so. + +(defun proof-assert-until-point + (&optional unclosed-comment-fun ignore-proof-process-p) + "Process the region from the end of the locked-region until point. + Default action if inside a comment is just to go until the start of + the comment. If you want something different, put it inside + unclosed-comment-fun. If ignore-proof-process-p is set, no commands + will be added to the queue." + (interactive) + (let ((pt (point)) + (crowbar (or ignore-proof-process-p (proof-steal-process))) + semis) + (save-excursion + (if (not (re-search-backward "\\S-" (proof-locked-end) t)) + (progn (goto-char pt) + (error "Nothing to do!"))) + (setq semis (proof-segment-up-to (point)))) + (if (and unclosed-comment-fun (eq 'unclosed-comment (car semis))) + (funcall unclosed-comment-fun) + (if (eq 'unclosed-comment (car semis)) (setq semis (cdr semis))) + (if (and (not ignore-proof-process-p) (not crowbar) (null semis)) + (error "Nothing to do!")) + (goto-char (nth 2 (car semis))) + (and (not ignore-proof-process-p) + (let ((vanillas (proof-semis-to-vanillas (nreverse semis)))) + (if crowbar (setq vanillas (cons crowbar vanillas))) + (proof-start-queue (proof-locked-end) (point) vanillas)))))) + +;; insert-pbp-command - an advancing command, for use when ;; +;; PbpHyp or Pbp has executed in LEGO, and returned a ;; +;; command for us to run ;; + +(defun proof-insert-pbp-command (cmd) + (proof-check-process-available) + (let (span) + (proof-goto-end-of-locked) + (insert cmd) + (setq span (make-span (proof-locked-end) (point))) + (set-span-property span 'type 'pbp) + (set-span-property span 'cmd cmd) + (proof-start-queue (proof-locked-end) (point) + (list (list span cmd 'proof-done-advancing))))) + + +;; proof-retract-until-point and associated gunk ;; +;; most of the hard work (i.e computing the commands to do ;; +;; the retraction) is implemented in the customisation ;; +;; module (lego.el or coq.el) which is why this looks so ;; +;; straightforward ;; + + +(defun proof-done-retracting (span) + "Updates display after proof process has reset its state. See also +the documentation for `proof-retract-until-point'. It optionally +deletes the region corresponding to the proof sequence." + (let ((start (span-start span)) + (end (span-end span)) + (kill (span-property span 'delete-me))) + (proof-set-locked-end start) + (proof-set-queue-end start) + (delete-spans start end 'type) + (delete-span span) + (if kill (delete-region start end)))) + +(defun proof-setup-retract-action (start end proof-command delete-region) + (let ((span (make-span start end))) + (set-span-property span 'delete-me delete-region) + (list (list span proof-command 'proof-done-retracting)))) + +(defun proof-retract-target (target delete-region) + (let ((end (proof-locked-end)) + (start (span-start target)) + (span (proof-last-goal-or-goalsave)) + actions) + + (if (and span (not (eq (span-property span 'type) 'goalsave))) + (if (< (span-end span) (span-end target)) + (progn + (setq span target) + (while (and span (eq (span-property span 'type) 'comment)) + (setq span (next-span span 'type))) + (setq actions (proof-setup-retract-action + start end + (if (null span) "COMMENT" + (funcall proof-count-undos-fn span)) + delete-region) + end start)) + + (setq actions (proof-setup-retract-action (span-start span) end + proof-kill-goal-command + delete-region) + end (span-start span)))) + + (if (> end start) + (setq actions + (nconc actions (proof-setup-retract-action + start end + (funcall proof-find-and-forget-fn target) + delete-region)))) + + (proof-start-queue (min start end) (proof-locked-end) actions))) + +(defun proof-retract-until-point (&optional delete-region) + "Sets up the proof process for retracting until point. In + particular, it sets a flag for the filter process to call + `proof-done-retracting' after the proof process has actually + successfully reset its state. It optionally deletes the region in + the proof script corresponding to the proof command sequence. If + this function is invoked outside a locked region, the last + successfully processed command is undone." + (interactive) + (proof-check-process-available) + (let ((span (span-at (point) 'type))) + (if (null (proof-locked-end)) (error "No locked region")) + (and (null span) + (progn (proof-goto-end-of-locked) (backward-char) + (setq span (span-at (point) 'type)))) + (proof-retract-target span delete-region))) + +;; proof-try-command ;; +;; this isn't really in the spirit of script management, ;; +;; but sometimes the user wants to just try an expression ;; +;; without having to undo it in order to try something ;; +;; different. Of course you can easily lose sync by doing ;; +;; something here which changes the proof state ;; + +(defun proof-done-trying (span) + (delete-span span) + (proof-detach-queue)) + +(defun proof-try-command + (&optional unclosed-comment-fun) + + "Process the command at point, + but don't add it to the locked region. This will only happen if + the command satisfies proof-state-preserving-p. + + Default action if inside a comment is just to go until the start of + the comment. If you want something different, put it inside + unclosed-comment-fun." + (interactive) + (let ((pt (point)) semis crowbar test) + (setq crowbar (proof-steal-process)) + (save-excursion + (if (not (re-search-backward "\\S-" (proof-locked-end) t)) + (progn (goto-char pt) + (error "Nothing to do!"))) + (setq semis (proof-segment-up-to (point)))) + (if (and unclosed-comment-fun (eq 'unclosed-comment (car semis))) + (funcall unclosed-comment-fun) + (if (eq 'unclosed-comment (car semis)) (setq semis (cdr semis))) + (if (and (not crowbar) (null semis)) (error "Nothing to do!")) + (setq test (car semis)) + (if (not (funcall proof-state-preserving-p (nth 1 test))) + (error "Command is not state preserving")) + (goto-char (nth 2 test)) + (let ((vanillas (proof-semis-to-vanillas (list test) + 'proof-done-trying))) + (if crowbar (setq vanillas (cons crowbar vanillas))) + (proof-start-queue (proof-locked-end) (point) vanillas))))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; misc other user functions ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defun proof-undo-last-successful-command () + "Undo last successful command, both in the buffer recording the + proof script and in the proof process. In particular, it deletes + the corresponding part of the proof script." + (interactive) + (goto-char (span-start (span-at-before (proof-locked-end) 'type))) + (proof-retract-until-point t)) + +(defun proof-interrupt-process () + (interactive) + (if (not (proof-shell-live-buffer)) + (error "Proof Process Not Started!")) + (if (not (eq proof-script-buffer (current-buffer))) + (error "Don't own process!")) + (if (not proof-shell-busy) + (error "Proof Process Not Active!")) + (save-excursion + (set-buffer proof-shell-buffer) + (comint-interrupt-subjob))) + + +(defun proof-find-next-terminator () + "Set point after next `proof-terminal-char'." + (interactive) + (let ((cmd (span-at (point) 'type))) + (if cmd (goto-char (span-end cmd)) + (and (re-search-forward "\\S-" nil t) + (proof-assert-until-point nil 'ignore-proof-process))))) + +(defun proof-process-buffer () + "Process the current buffer and set point at the end of the buffer." + (interactive) + (end-of-buffer) + (proof-assert-until-point)) + +;; For when things go horribly wrong + +(defun proof-restart-script () + (interactive) + (save-excursion + (if (buffer-live-p proof-script-buffer) + (progn + (set-buffer proof-script-buffer) + (setq proof-active-buffer-fake-minor-mode nil) + (delete-spans (point-min) (point-max) 'type) + (proof-detach-segments))) + (setq proof-shell-busy nil + proof-script-buffer nil) + (if (buffer-live-p proof-shell-buffer) + (kill-buffer proof-shell-buffer)) + (if (buffer-live-p proof-pbp-buffer) + (kill-buffer proof-pbp-buffer)))) + +;; A command for making things go horribly wrong - it moves the +;; end-of-locked-region marker backwards, so user had better move it +;; correctly to sync with the proof state, or things will go all +;; pear-shaped. + +(defun proof-frob-locked-end () + (interactive) + "Move the end of the locked region backwards. + Only for use by consenting adults." + (cond + ((not (eq proof-script-buffer (current-buffer))) + (error "Not in proof buffer")) + ((> (point) (proof-locked-end)) + (error "Can only move backwards")) + (t (proof-set-locked-end (point)) + (delete-spans (proof-locked-end) (point-max) 'type)))) + +(defvar proof-minibuffer-history nil + "The last command read from the minibuffer") + +(defun proof-execute-minibuffer-cmd () + (interactive) + (let (cmd) + (proof-check-process-available 'relaxed) + (setq cmd (read-string "Command: " nil 'proof-minibuffer-history)) + (proof-invisible-command cmd 'relaxed))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;; Popup and Pulldown Menu ;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;;; Menu commands for the underlying proof assistant +(defvar proof-ctxt-string "" + "Command to display context in proof assistant") + +(defvar proof-help-string "" + "Command to ask for help in proof assistant") + +(defvar proof-prf-string "" + "Command to display proof state in proof assistant") + +(defun proof-ctxt () + "List context." + (interactive) + (proof-invisible-command (concat proof-ctxt-string proof-terminal-string))) + +(defun proof-help () + "Print help message giving syntax." + (interactive) + (proof-invisible-command (concat proof-help-string proof-terminal-string))) + +(defun proof-prf () + "List proof state." + (interactive) + (proof-invisible-command (concat proof-prf-string proof-terminal-string))) + +;;; To be called from menu +(defun proof-info-mode () + "Info mode on proof mode." + (interactive) + (info "script-management")) + +(defun proof-exit () + "Exit Proof-assistant." + (interactive) + (proof-restart-script)) + +(defvar proof-help-menu + '("Help" + ["Proof assistant web page" + (w3-fetch proof-www-home-page) t] + ["Help on Emacs proof-mode" proof-info-mode t] + ) + "The Help Menu in Script Management.") + +(defvar proof-shared-menu + (append-element '( + ["Display context" proof-ctxt + :active (proof-shell-live-buffer)] + ["Display proof state" proof-prf + :active (proof-shell-live-buffer)] + ["Exit proof assistant" proof-exit + :active (proof-shell-live-buffer)] + "----" + ["Find definition/declaration" find-tag-other-window t] + ) + proof-help-menu)) + +(defvar proof-menu + (append '("Commands" + ["Toggle active terminator" proof-active-terminator-minor-mode + :active t + :style toggle + :selected proof-active-terminator-minor-mode] + "----") + (list (if (string-match "XEmacs 19.1[2-9]" emacs-version) + "--:doubleLine" "----")) + proof-shared-menu + ) + "*The menu for the proof assistant.") + +(defvar proof-shell-menu proof-shared-menu + "The menu for the Proof-assistant shell") + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Active terminator minor mode ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(deflocal proof-active-terminator-minor-mode nil + "active terminator minor mode flag") + +(defun proof-active-terminator-minor-mode (&optional arg) + "Toggle PROOF's Active Terminator minor mode. +With arg, turn on the Active Terminator minor mode if and only if arg +is positive. + +If Active terminator mode is enabled, a terminator will process the +current command." + + (interactive "P") + +;; has this minor mode been registered as such? + (or (assq 'proof-active-terminator-minor-mode minor-mode-alist) + (setq minor-mode-alist + (append minor-mode-alist + (list '(proof-active-terminator-minor-mode + (concat " " proof-terminal-string)))))) + + (setq proof-active-terminator-minor-mode + (if (null arg) (not proof-active-terminator-minor-mode) + (> (prefix-numeric-value arg) 0))) + (if (fboundp 'redraw-modeline) + (redraw-modeline) + (force-mode-line-update))) + +(defun proof-process-active-terminator () + "Insert the terminator in an intelligent way and assert until the + new terminator. Fire up proof process if necessary." + (let ((mrk (point)) ins) + (if (looking-at "\\s-\\|\\'\\|\\w") + (if (not (re-search-backward "\\S-" (proof-unprocessed-begin) t)) + (error "Nothing to do!"))) + (if (not (= (char-after (point)) proof-terminal-char)) + (progn (forward-char) (insert proof-terminal-string) (setq ins t))) + (proof-assert-until-point + (function (lambda () + (if ins (backward-delete-char 1)) + (goto-char mrk) (insert proof-terminal-string)))))) + +(defun proof-active-terminator () + (interactive) + (if proof-active-terminator-minor-mode + (proof-process-active-terminator) + (self-insert-command 1))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Proof mode configuration ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(define-derived-mode proof-mode fundamental-mode + proof-mode-name "Proof mode - not standalone" + ;; define-derived-mode proof-mode initialises proof-mode-map + (setq proof-buffer-type 'script)) + +;; This has to come after proof-mode is defined + +(define-derived-mode proof-shell-mode comint-mode + "proof-shell" "Proof shell mode - not standalone" + (setq proof-buffer-type 'shell) + (setq proof-shell-busy nil) + (setq proof-shell-delayed-output (cons 'insert "done")) + (setq comint-prompt-regexp proof-shell-prompt-pattern) + (add-hook 'comint-output-filter-functions 'proof-shell-filter nil t) + (setq comint-get-old-input (function (lambda () ""))) + (proof-dont-show-annotations) + (setq proof-marker (make-marker))) + +(easy-menu-define proof-shell-menu + proof-shell-mode-map + "Menu used in the proof assistant shell." + (cons proof-mode-name (cdr proof-shell-menu))) + +(easy-menu-define proof-mode-menu + proof-mode-map + "Menu used in proof mode." + (cons proof-mode-name (cdr proof-menu))) + +;; the following callback is an irritating hack - there should be some +;; elegant mechanism for computing constants after the child has +;; configured. + +(defun proof-config-done () + +;; calculate some strings and regexps for searching + + (setq proof-terminal-string (char-to-string proof-terminal-char)) + + (setq pbp-goal-command (concat "Pbp %s" proof-terminal-string)) + (setq pbp-hyp-command (concat "PbpHyp %s" proof-terminal-string)) + + (make-local-variable 'comment-start) + (setq comment-start (concat proof-comment-start " ")) + (make-local-variable 'comment-end) + (setq comment-end (concat " " proof-comment-end)) + (make-local-variable 'comment-start-skip) + (setq comment-start-skip + (concat (regexp-quote proof-comment-start) "+\\s_?")) + + (setq proof-re-end-of-cmd (concat "\\s_*" proof-terminal-string "\\s_*\\\'")) + (setq proof-re-term-or-comment + (concat proof-terminal-string "\\|" (regexp-quote proof-comment-start) + "\\|" (regexp-quote proof-comment-end))) + +;; func-menu --- Jump to a goal within a buffer + (and (boundp 'fume-function-name-regexp-alist) + (defvar fume-function-name-regexp-proof + (cons proof-goal-with-hole-regexp 2)) + (push (cons major-mode 'fume-function-name-regexp-proof) + fume-function-name-regexp-alist)) + (and (boundp 'fume-find-function-name-method-alist) + (push (cons major-mode 'fume-match-find-next-function-name) + fume-find-function-name-method-alist)) + +;; Info + (or (memq proof-info-dir Info-default-directory-list) + (setq Info-default-directory-list + (cons proof-info-dir Info-default-directory-list))) + +;; keymaps and menus + (easy-menu-add proof-mode-menu proof-mode-map) + + (proof-define-keys proof-mode-map proof-universal-keys) + + (define-key proof-mode-map + (vconcat [(control c)] (vector proof-terminal-char)) + 'proof-active-terminator-minor-mode) + + (define-key proof-mode-map [(control c) (control e)] + 'proof-find-next-terminator) + + (define-key proof-mode-map (vector proof-terminal-char) + 'proof-active-terminator) + (define-key proof-mode-map [(control c) (return)] 'proof-assert-until-point) + (define-key proof-mode-map [(control c) (control t)] 'proof-try-command) + (define-key proof-mode-map [(control c) ?u] 'proof-retract-until-point) + (define-key proof-mode-map [(control c) (control u)] + 'proof-undo-last-successful-command) + + (define-key proof-mode-map [(control c) ?\'] + 'proof-goto-end-of-locked-interactive) + (define-key proof-mode-map [(control button1)] 'proof-send-span) + (define-key proof-mode-map [(control c) (control b)] 'proof-process-buffer) + (define-key proof-mode-map [(control c) (control z)] 'proof-frob-locked-end) + + (define-key proof-mode-map [tab] 'proof-indent-line) + (setq indent-line-function 'proof-indent-line) + + (define-key (current-local-map) [(control c) (control p)] 'proof-prf) + (define-key (current-local-map) [(control c) ?c] 'proof-ctxt) + (define-key (current-local-map) [(control c) ?h] 'proof-help) + +;; For fontlock + (remove-hook 'font-lock-after-fontify-buffer-hook 'proof-zap-commas-buffer t) + (add-hook 'font-lock-after-fontify-buffer-hook 'proof-zap-commas-buffer nil t) + (remove-hook 'font-lock-mode-hook 'proof-unfontify-separator t) + (add-hook 'font-lock-mode-hook 'proof-unfontify-separator nil t) + +;; if we don't have the following, zap-commas fails to work. + + (and (boundp 'font-lock-always-fontify-immediately) + (setq font-lock-always-fontify-immediately t)) + + (run-hooks 'proof-mode-hook)) + +(defun proof-shell-config-done () + (accept-process-output (get-buffer-process (current-buffer))) + + ;; If the proof process in invoked on a different machine e.g., + ;; for proof-prog-name="rsh fastmachine proofprocess", one needs + ;; to adjust the directory: + (and proof-shell-cd + (proof-shell-insert (format proof-shell-cd + ;; under Emacs 19.34 default-directory contains "~" which causes + ;; problems with LEGO's internal Cd command + (expand-file-name default-directory)))) + + (if proof-shell-init-cmd + (proof-shell-insert proof-shell-init-cmd)) + +;; Note that proof-marker actually gets set in proof-shell-filter. +;; This is manifestly a hack, but finding somewhere more convenient +;; to do the setup is tricky. + + (while (null (marker-position proof-marker)) + (if (accept-process-output (get-buffer-process (current-buffer)) 15) + () + (error "Failed to initialise proof process")))) + +(define-derived-mode pbp-mode fundamental-mode + proof-mode-name "Proof by Pointing" + ;; defined-derived-mode pbp-mode initialises pbp-mode-map + (setq proof-buffer-type 'pbp) + (suppress-keymap pbp-mode-map 'all) +; (define-key pbp-mode-map [(button2)] 'pbp-button-action) + (proof-define-keys pbp-mode-map proof-universal-keys) + (erase-buffer)) + + +(provide 'proof) diff --git a/script-management.texinfo b/script-management.texinfo new file mode 100644 index 00000000..a7232b3c --- /dev/null +++ b/script-management.texinfo @@ -0,0 +1,440 @@ +\input texinfo @c -*-texinfo-*- +@c %**start of header +@setfilename script-management.info +@settitle Script Management +@paragraphindent 0 +@c %**end of header + +@setchapternewpage odd + +@titlepage +@sp 10 +@comment The title is printed in a large font. +@center @titlefont{Script Management Mode} + +@c The following two commands start the copyright page. +@page +@vskip 0pt plus 1filll +Copyright @copyright{} 1997, 1998 LEGO Team, LFCS Edinburgh +@end titlepage + +@node Top, Credits, (dir), (dir) +@comment node-name, next, previous, up + +A @emph{proof script} is a sequence of commands to a proof assistant. +Proof mode is a mode designed to be customised for a particular proof +assistant, to manage communication with a proof process and thereby +support building and secure editing of proof scripts. Currently custom +modes exist for LEGO and Coq. + +@menu +* Credits:: The people Involved +* Introduction:: Introduction to Script Management +* Commands:: Proof mode Commands +* Multiple Files:: Proof developments spanning several files +* Proof by Pointing:: Proof using the Mouse +* An Active Terminator:: Active Terminator minor mode +* Walkthrough:: An example of using proof mode +* LEGO mode:: Extra Bindings for LEGO +* Coq mode:: Extra Bindings for Coq +* Internals:: The Seedy Underside of Proof mode +* Known Problems:: Caveat Emptor +@end menu + +@node Credits, Introduction, Top, Top +@comment node-name, next, previous, up +@unnumberedsec Credits + +Inspired by Yves Bertot's Centaur-based proof environment CtCoq, Healf +Goguen, Thomas Kleymann and Dilip Sequeira have implented a generic +proof mode for Emacs. The original proof-by-pointing algorithm has been +implemented by Yves Bertot. This manual was originally written by Dilip +Sequeira. + +@node Introduction, Commands, Credits, Top +@comment node-name, next, previous, up +@unnumberedsec Introduction + +Each script resides in an Emacs buffer, called a @emph{script buffer}, +which is divided into three regions: + +@itemize @bullet +@item The @emph{Locked} region appears in blue (underlined on monochrome +displays) and contains commands which have been sent to the proof process +and verified. The commands in the locked region cannot be edited. + +@item The @emph{Queue} region appears in pink (inverse video) and contains +commands waiting to be sent to the proof process. Like those in the +locked region, these commands can't be edited. + +@item The @emph{Editing} region contains the commands the user is working +on, and can be edited as normal Emacs text. +@end itemize + +These three regions appear in the buffer in the order above; that is, +the locked region is always at the start of the buffer, and the editing +region always at the end. The queue region only exists if there is input +waiting to be sent to the proof process. + +Proof mode has two operations which transfer commands between these +regions: assertion and retraction. These cause commands to be sent to +the proof process, and Emacs will summarise the results in the +@emph{Response Buffer}. + +@strong{Assertion} causes commands from the editing region to be +transferred to the queue region and sent one by one to the proof +process. If the command is accepted, it is transferred to the locked +region, but if an error occurs it is signalled to the user, and the +offending command is transferred back to the editing region together +with any remaining commands in the queue. @strong{Retraction} causes +commands to be transferred from the locked region to the editing region +(again via the queue region) and the appropriate 'undo' commands to be +sent to the proof process. + +As commands are transferred to the locked region, they are aggregated +into segments which constitute the smallest units which can be +undone. Typically a segment consists of a declaration or definition, or +all the text from a `goal' command to the corresponding `save' command, +or the individual commands in the proof of an unfinished goal. As the +mouse moves over the the region, the segment containing the pointer will +be highlighted. + +Commands in the editing region can be freely edited while +commands in the queue are transferred to the proof process. However, +assertion and retraction commands can only be issued when the queue is +empty. + +@node Commands, Multiple Files, Introduction, Top +@unnumberedsec Proof Mode Commands + +@table @kbd + +@item C-c C-b +assert the commands in the buffer. + +@item C-c return +assert the commands in the editing region up to and +including the one containing the point. + +@item C-c u +retract the segments in the locked region back to and +including the one containing the point. If point is outside the *Locked* +region, the last segment is undone. + +@item C-c C-u +retract the last segment in the locked region, and kill the text in it. +@footnote{Be careful with this, as it may delete more than you anticipate. +However, you can always recover the killed text using Emacs Undo.} + +@item C-c ' +move the point to the end of the locked region. If you are in a script +buffer other than the active scripting buffer, this will also transfer +you to the active one. + +@item C-c C-e +move the point to the next terminator + +@item C-c C-p +display the proof state in the response buffer + +@item C-c c +display the context in the response buffer + +@item C-c h +print proof-system specific help text in the response buffer + +@item C-c C-c +interrupt the process process. This may leave script management or the +proof process (or both) in an inconsistent state. + +@item C-c C-z +move the end of the locked region backwards to the end of the segment +containing the point. @footnote{Don't try this one at home, kids.} + +@item C-c C-t +Send the command at the point to the subprocess, not +recording it in the locked region. @footnote{This is supplied in order +to enable the user to test the types and values of expressions. There's +some checking that the command won't change the proof state, but it +isn't foolproof.} + +@item C-c C-v +Request a command from the minibuffer and send it to +the subprocess. Currently no checking whatsoever is done on the command. +@end table + +The command @code{proof-restart-script} can be used to completely +restart script management. + + +@node Multiple Files, An Active Terminator, Commands, Top +@unnumberedsec Multiple Files + +Proof mode has a rudimentary facility for operating with multiple files +in a proof development. This is currently only supported for LEGO. If +the user invokes script management in a different buffer from the one in +which it is running, one of two prompts will appear: + +@itemize @bullet +@item ``Steal script management?'' +if Emacs doesn't think the file is already part of the proof development +@item ``Reprocess this file?'' +if Emacs thinks the file is already included in the proof process. If +the user confirms, Emacs will cause the proof process to forget the +contents of the file, so that it is processed afresh. +@end itemize + +Currently this facility requires each script buffer to have a +corresponding file. + +When working with script management in multiple buffers, it is easy +to lose track of which buffer is the current script buffer. As a mnemonic +aid, the word @samp{Scripting} appears in the minor mode list of the +active scripting buffer. + +Caveats: +@itemize @minus +@item Note that if processing a buffer causes other files to be loaded +into the LEGO process, those files will be imported from disk rather +than from any Emacs buffer in which it is being edited, i.e.@: if your +file is going to be included indirectly, save it. + +@item However much you move around the file system in Emacs, the +LEGOPATH will be the LEGOPATH you started with. No concept of +"current directory" is currently supported. +@end itemize + +@node An Active Terminator, Proof by Pointing, Multiple Files, Top +@unnumberedsec An Active Terminator + +Proof mode has a minor mode which causes the terminator to become +active. When this mode is active, pressing the terminator key (@kbd{;} +for LEGO, @kbd{.} for Coq) outside a comment or quote will cause the +character to be entered into the buffer, and all the commands in the +editing region up to the point to be asserted. + +This mode can be toggled with the command +`proof-active-terminator-minor-mode' (@kbd{C-c ;} or @kbd{C-c .}) + +@node Proof by Pointing, Walkthrough, An Active Terminator, Top +@unnumberedsec Proof by Pointing + +@emph{This mode is currently very unreliable, and we do not guarantee +that it will work as discussed in this document.} + +Proof by pointing is a facility whereby proof commands can be generated +by using the mouse to select terms. When proving a goal, a summary of +the current proof state will appear in the response buffer. By moving +the mouse over the buffer, the structure of the goal and hypothesis +terms will be shown by highlighting. + +If a selection is made using the second (usually the middle) mouse +button, Emacs will generate the appropriate commands, insert them in the +script buffer, and send them to the proof process. These commands are +aggregated in the locked region as a single segment, so that a +mouse-generated command sequence can be retracted with a single +retraction command. + +Further Information about proof by pointing may be found in the paper +@cite{User Interfaces for Theorem Provers} by Yves Bertot and Laurent +Thery, to appear in @cite{Information and Computation}, from which +the following example is taken. + +@menu +* Proof by Pointing Example:: An example using proof by pointing +@end menu + +@node Proof by Pointing Example, ,Proof by Pointing,Proof by Pointing + +Suppose we wish to prove the lego term: + +@example +(((p a) \/ (q b)) /\ @{x:Prop@}(p x) -> (q x)) -> (Ex ([x:Prop] q(x))); +@end example + +Asserting this goal will result in the proof state + +@example +?0 : ((p a \/ q b) /\ @{x:Prop@}(p x)->q x)->Ex ([x:Prop]q x) +@end example + +appearing in the response buffer. Suppose our strategy is to use a +case analysis on the disjunction, starting with the @samp{p(a)} subterm. +Clicking on this term will cause script management to insert the following +command sequence in the script buffer, and execute it. + +@example +Intros H; Refine H; Intros H0 H1; +Refine or_elim H0 Then Intros H2; Try Refine H2; +@end example + + +The response buffer will then read + +@example + H : (p a \/ q b) /\ @{x:Prop@}(p x)->q x + H0 : p a \/ q b + H1 : @{x:Prop@}(p x)->q x + H2 : p a + ?10 : Ex ([x:Prop]q x) +@end example + +Clicking on the subterm @samp{(p x)} in the hypothesis H1 will instruct +script management to prove an instance of @samp{(p x)} and deduce the +corresponding @samp{(q x)}. The commands + +@example +allE H1; intros +1 H3; Refine impl_elim H3; Try Assumption; +@end example + +are inserted and executed, leaving the proof state as + +@example + H : (p a \/ q b) /\ @{x:Prop@}(p x)->q x + H0 : p a \/ q b + H1 : @{x:Prop@}(p x)->q x + H2 : p a + H3 : (p a)->q a + ?20 : (q a)->Ex ([x:Prop]q x) +@end example + +Now clicking on the @samp{q x)} subterm in ?20 will prove the subgoal. We are +left with the other half of the original case analysis: + +@example + H : (p a \/ q b) /\ @{x:Prop@}(p x)->q x + H0 : p a \/ q b + H1 : @{x:Prop@}(p x)->q x + H2 : q b + ?26 : Ex ([x:Prop]q x) +@end example + +Clicking on @samp{q x} proves the goal. + + + + +@node Walkthrough, LEGO mode, Proof by Pointing, Top +@unnumberedsec A Walkthrough + +Here's a LEGO example of how script management is used. + +First, we turn on active terminator minor mode by typing @kbd{C-c ;} +Then we enter + +`Module Walkthrough Import lib_logic;' + +The command should be lit in pink (or inverse video if you don't have a +colour display). As LEGO imports each module, a line will appear in the +response buffer showing the creation of context marks. Eventually the +command should turn blue, indicating that LEGO has successfully +processed it. Then type (on a separate line if you like) + +@samp{Goal bland_commutes: @{A,B:Prop@} (and A B) -> (and B A);} + +The goal should be echoed in the response buffer. + +@samp{Intros;} + +Whoops! @kbd{C-c C-u} to pretend that didn't happen. + +@samp{intros; andI;} + +A proof summary will appear in the response buffer. We could solve the +goal by pointing now, but we'll stay with the keyboard. + +@samp{Refine H; intros; Immed; Refine H; intros; Immed;} + +finishes the Goal. + +@samp{Save bland_commutes;} + +Moving the mouse pointer over the locked region now reveals that the +entire proof has been aggregated into a single segment. Suppose we +decide to call the goal something more sensible. Moving the cursor up +into the locked region, somewhere between `Goal' and `Save', we enter +@kbd{C-c u}. The segment is transferred back into the editing +region. Now we correct the goal name, move the cursor to the end of the +buffer, and type @kbd{C-c return}. Proof mode queues the commands for +processing and executes them. + +@node LEGO mode, Coq mode, Walkthrough, Top +@unnumberedsec LEGO mode + +LEGO mode is a mode derived from proof mode for editing LEGO scripts. +There are some abbreviations for common commands, which +add text to the buffer: + +@table @kbd +@item C-c i +intros +@item C-c I +Intros +@item C-c R +Refine +@end table + + +@node Coq mode, Known Problems, LEGO mode, Top +@unnumberedsec Coq mode + +Coq mode is a mode derived from proof mode for editing Coq scripts. +As well as custom popup menus, it has the following commands: + +@table @kbd + +@item C-c C-s +search for items in the library of a given type. This runs the +@kbd{Search} command of Coq. + +@end table + +In addition, there are some abbreviations for common commands, which +add text to the buffer: + +@table @kbd +@item C-c I +Intros +@item C-c a +Apply +@end table + +@node Known Problems, Internals, Coq mode, Top +@unnumberedsec Known Problems + +Since Emacs is pretty flexible, there are a whole bunch of things you +can do to confuse script management. When it gets confused, it may +become distressed, and may eventually sulk. In such instances +@code{proof-restart-script-management} may be of use. + +A few things to avoid: + +@itemize @minus +@item If you're using script management with multiple files, don't start +changing the file names. + +@item Script Management doesn't understand how to undo @code{Discharge} +commands in LEGO, and any attempts it makes to do so may leave it in an +inconsistent state. If you're undoing the effects of a @code{Discharge} +command, retract back to the declaration of whatever gets discharged. + +@item Proof by Pointing doesn't work very well, and is inefficiently +implemented. + +@item The locked and queue regions are not quite read-only: in particular +Emacs Undo can insert text into them. + +@item When a LEGO import command fails, the created "Mark" is not +forgotten, and the proof process thinks the file has been included. So +if you assert the command again, it will probably be accepted by LEGO, +because the relevant mark is in the namespace. +@end itemize + +Fixes for some of these may be provided in a future release. + +@node Internals, , Known Problems, Top +@unnumberedsec Internals + +I may one day document the script management internals here. Until then, +UtSL. +@bye diff --git a/span-extent.el b/span-extent.el new file mode 100644 index 00000000..b49670b7 --- /dev/null +++ b/span-extent.el @@ -0,0 +1,79 @@ +;;; This file implements spans in terms of extents, for xemacs. +;;; Copyright (C) 1998 LFCS Edinburgh +;;; Author: Healfdene Goguen + +;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> + +;; $Log$ +;; Revision 2.0 1998/08/11 15:00:13 da +;; New branch +;; +;; Revision 1.4 1998/06/10 14:01:48 hhg +;; Wrote generic span functions for making spans read-only or read-write. +;; +;; Revision 1.3 1998/06/02 15:36:44 hhg +;; Corrected comment about this being for xemacs. +;; +;; Revision 1.2 1998/05/19 15:30:27 hhg +;; Added header and log message. +;; + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Bridging the emacs19/xemacs gulf ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; Now define "spans" in terms of extents. + +(defsubst make-span (start end) + (make-extent start end)) + +(defsubst detach-span (span) + (detach-extent span)) + +(defsubst set-span-endpoints (span start end) + (set-extent-endpoints span start end)) + +(defsubst set-span-start (span value) + (set-extent-endpoints span value (extent-end-position span))) + +(defsubst set-span-end (span value) + (set-extent-endpoints span (extent-start-position span) value)) + +(defsubst span-read-only (span) + (set-span-property span 'read-only t)) + +(defsubst span-read-write (span) + (set-span-property span 'read-only nil)) + +(defsubst span-property (span name) + (extent-property span name)) + +(defsubst set-span-property (span name value) + (set-extent-property span name value)) + +(defsubst delete-span (span) + (delete-extent span)) + +(defsubst delete-spans (start end prop) + (mapcar-extents 'delete-extent nil (current-buffer) start end nil prop)) + +(defsubst span-at (pt prop) + (extent-at pt nil prop)) + +(defsubst span-at-before (pt prop) + (extent-at pt nil prop nil 'before)) + +(defsubst span-start (span) + (extent-start-position span)) + +(defsubst span-end (span) + (extent-end-position span)) + +(defsubst prev-span (span prop) + (extent-at (extent-start-position span) nil prop nil 'before)) + +(defsubst next-span (span prop) + (extent-at (extent-end-position span) nil prop nil 'after)) + + +(provide 'span-extent) diff --git a/span-overlay.el b/span-overlay.el new file mode 100644 index 00000000..f74350ed --- /dev/null +++ b/span-overlay.el @@ -0,0 +1,288 @@ +;;; This file implements spans in terms of overlays, for emacs19. +;;; Copyright (C) 1998 LFCS Edinburgh +;;; Author: Healfdene Goguen + +;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> + +;; $Log$ +;; Revision 2.0 1998/08/11 15:00:13 da +;; New branch +;; +;; Revision 1.9 1998/06/10 14:02:39 hhg +;; Wrote generic span functions for making spans read-only or read-write. +;; Fixed bug in add-span and remove-span concerning return value of +;; span-traverse. +;; +;; Revision 1.8 1998/06/10 12:41:47 hhg +;; Compare span-end first rather than span-start in span-lt, because +;; proof-lock-span is often changed and has starting point 1. +;; Factored out common code of add-span and remove-span into +;; span-traverse. +;; +;; Revision 1.7 1998/06/03 17:40:07 hhg +;; Changed last-span to before-list. +;; Added definitions of foldr and foldl if they aren't already loaded. +;; Changed definitions of add-span, remove-span and find-span-aux to be +;; non-recursive. +;; Removed detach-extent since this file isn't used by xemacs. +;; Added function append-unique to avoid repetitions in list generated by +;; spans-at-region. +;; Changed next-span so it uses member-if. +;; +;; Revision 1.6 1998/06/02 15:36:51 hhg +;; Corrected comment about this being for emacs19. +;; +;; Revision 1.5 1998/05/29 09:50:10 tms +;; o outsourced indentation to proof-indent +;; o support indentation of commands +;; o replaced test of Emacs version with availability test of specific +;; features +;; o C-c C-c, C-c C-v and M-tab is now available in all buffers +;; +;; Revision 1.4 1998/05/21 17:27:41 hhg +;; Removed uninitialized os variable in spans-at-region. +;; +;; Revision 1.3 1998/05/21 08:28:52 hhg +;; Initialize 'before pointer in add-span-aux when last-span is nil. +;; Removed span-at-type. +;; Fixed bug in span-at-before, where (span-start span) may be nil. +;; Added spans-at-(point|region)[-prop], which fixes bug of C-c u at end +;; of buffer. +;; +;; Revision 1.2 1998/05/19 15:31:37 hhg +;; Added header and log message. +;; Fixed set-span-endpoints so it preserves invariant. +;; Changed add-span and remove-span so that they update last-span +;; correctly themselves, and don't take last-span as an argument. +;; + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Bridging the emacs19/xemacs gulf ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; before-list represents a linked list of spans for each buffer. +;; It has the invariants of: +;; * being ordered wrt the starting point of the spans in the list, +;; with detached spans at the end. +;; * not having overlapping overlays of the same type. + +(defvar before-list nil + "Start of backwards-linked list of spans") + +(make-variable-buffer-local 'before-list) + + +(or (fboundp 'foldr) +(defun foldr (func a seq) + "Return (func (func (func (... (func a Sn) ...) S2) S1) S0) +when func's argument is 2 and seq is a sequence whose +elements = S0 S1 S2 ... Sn. [tl-seq.el]" + (let ((i (length seq))) + (while (> i 0) + (setq i (1- i)) + (setq a (funcall func a (elt seq i))) + ) + a))) + +(or (fboundp 'foldl) +(defun foldl (func a seq) + "Return (... (func (func (func a S0) S1) S2) ...) +when func's argument is 2 and seq is a sequence whose +elements = S0 S1 S2 .... [tl-seq.el]" + (let ((len (length seq)) + (i 0)) + (while (< i len) + (setq a (funcall func a (elt seq i))) + (setq i (1+ i)) + ) + a))) + +(defsubst span-start (span) + (overlay-start span)) + +(defsubst span-end (span) + (overlay-end span)) + +(defun set-span-property (span name value) + (overlay-put span name value)) + +(defsubst span-property (span name) + (overlay-get span name)) + +(defun span-read-only-hook (overlay after start end &optional len) + (error "Region is read-only")) + +(defun span-read-only (span) + (set-span-property span 'modification-hooks '(span-read-only-hook)) + (set-span-property span 'insert-in-front-hooks '(span-read-only-hook))) + +(defun span-read-write (span) + (set-span-property span 'modification-hooks nil) + (set-span-property span 'insert-in-front-hooks nil)) + +(defun int-nil-lt (m n) + (cond + ((eq m n) nil) + ((not n) t) + ((not m) nil) + (t (< m n)))) + +;; We use end first because proof-locked-queue is often changed, and +;; its starting point is always 1 +(defun span-lt (s u) + (or (int-nil-lt (span-end s) (span-end u)) + (and (eq (span-end s) (span-end u)) + (int-nil-lt (span-start s) (span-start u))))) + +(defun span-traverse (span prop) + (cond + ((not before-list) + ;; before-list empty + 'empty) + ((funcall prop before-list span) + ;; property holds for before-list and span + 'hd) + (t + ;; traverse before-list for property + (let ((l before-list) (before (span-property before-list 'before))) + (while (and before (not (funcall prop before span))) + (setq l before) + (setq before (span-property before 'before))) + l)))) + +(defun add-span (span) + (let ((ans (span-traverse span 'span-lt))) + (cond + ((eq ans 'empty) + (set-span-property span 'before nil) + (setq before-list span)) + ((eq ans 'hd) + (set-span-property span 'before before-list) + (setq before-list span)) + (t + (set-span-property span 'before + (span-property ans 'before)) + (set-span-property ans 'before span))))) + +(defun make-span (start end) + (add-span (make-overlay start end))) + +(defun remove-span (span) + (let ((ans (span-traverse span 'eq))) + (cond + ((eq ans 'empty) + (error "Bug: empty span list")) + ((eq ans 'hd) + (setq before-list (span-property before-list 'before))) + (ans + (set-span-property ans 'before (span-property span 'before))) + (t (error "Bug: span does not occur in span list"))))) + +;; extent-at gives "smallest" extent at pos +;; we're assuming right now that spans don't overlap +(defun spans-at-point (pt) + (let ((overlays nil) (os nil)) + (setq os (overlays-at pt)) + (while os + (if (not (memq (car os) overlays)) + (setq overlays (cons (car os) overlays))) + (setq os (cdr os))) + overlays)) + +;; assumes that there are no repetitions in l or m +(defun append-unique (l m) + (foldl (lambda (n a) (if (memq a m) n (cons a n))) m l)) + +(defun spans-at-region (start end) + (let ((overlays nil) (pos start)) + (while (< pos end) + (setq overlays (append-unique (spans-at-point pos) overlays)) + (setq pos (next-overlay-change pos))) + overlays)) + +(defun spans-at-point-prop (pt prop) + (let ((f (cond + (prop (lambda (spans span) + (if (span-property span prop) (cons span spans) + spans))) + (t (lambda (spans span) (cons span spans)))))) + (foldl f nil (spans-at-point pt)))) + +(defun spans-at-region-prop (start end prop) + (let ((f (cond + (prop (lambda (spans span) + (if (span-property span prop) (cons span spans) + spans))) + (t (lambda (spans span) (cons span spans)))))) + (foldl f nil (spans-at-region start end)))) + +(defun span-at (pt prop) + (car (spans-at-point-prop pt prop))) + +(defsubst detach-span (span) + (remove-span span) + (delete-overlay span) + (add-span span)) + +(defsubst delete-span (span) + (remove-span span) + (delete-overlay span)) + +;; The next two change ordering of list of spans: +(defsubst set-span-endpoints (span start end) + (remove-span span) + (move-overlay span start end) + (add-span span)) + +(defsubst set-span-start (span value) + (set-span-endpoints span value (span-end span))) + +;; This doesn't affect invariant: +(defsubst set-span-end (span value) + (set-span-endpoints span (span-start span) value)) + +(defsubst delete-spans (start end prop) + (mapcar 'delete-span (spans-at-region-prop start end prop))) + +(defun map-spans-aux (f l) + (cond (l (cons (funcall f l) (map-spans-aux f (span-property l 'before)))) + (t ()))) + +(defsubst map-spans (f) + (map-spans-aux f before-list)) + +(defun find-span-aux (prop-p l) + (while (and l (not (funcall prop-p l))) + (setq l (span-property l 'before))) + l) + +(defun find-span (prop-p) + (find-span-aux prop-p before-list)) + +(defun span-at-before (pt prop) + (let ((prop-pt-p + (cond (prop (lambda (span) + (let ((start (span-start span))) + (and start (> pt start) + (span-property span prop))))) + (t (lambda (span) + (let ((start (span-start span))) + (and start (> pt start)))))))) + (find-span prop-pt-p))) + +(defun prev-span (span prop) + (let ((prev-prop-p + (cond (prop (lambda (span) (span-property span prop))) + (t (lambda (span) t))))) + (find-span-aux prev-prop-p (span-property span 'before)))) + +;; overlays are [start, end) +;; If there are two spans overlapping then this won't work. +(defun next-span (span prop) + (let ((l (member-if (lambda (span) (span-property span prop)) + (overlays-at + (next-overlay-change (overlay-start span)))))) + (if l (car l) nil))) + + +(provide 'span-overlay) @@ -0,0 +1,175 @@ +-*- mode:outline -*- + +* Priorities +============ +A (High) to be fixed before release (Version 2.0) +B (Medium) desirable to fix at some point +C (Low) probably not worth wasting time on + +* This is a list of things which need doing in the generic interface +==================================================================== + +B Outsource script management features from proof.el to + proof-script.el (1h) + +A Write function proof-retract-file. (30min) + Currently, the command ForgetMark (for LEGO) is hardwired in + proof-steal-process. + +B Improve documentation in proof.el to help porting/understanding + Also add notes into script-management.texinfo + (ongoing, da). + +A Update source documentation and manual, in particular document bugs + and workarounds + (4h hhg & tms) + +A Implement more generic mechanism for large undos (2h) + + COQ: C-c u inside a Section should reset the whole section, then + redo defns + + LEGO: consider Discharge; perhaps unrol to the beginning of the + module? + +A Multiple files are sometimes handled incorrectly, because the + function `proof-steal-process' cannot figure out that some files have + already been processed. This is most likely caused by the ad-hoc + equality test on file names. Instead, one could employ + the built-in `file-truename' to trigger *canonical* file names. + (1h tms) + +B Implement proof-find-previous-terminator and bind it to C-c C-a + (45min tms) + +B Technical documentation to record expertise and allow users of other + proof systems to adopt generic package (40h hhg & tms) + +B Support for x-symbols package + +C XEmacs sessions seem to grow excessively in terms of memory + allocation. Perhaps some of the spans aren't removed properly? + Setting a limit on the size of the process buffer doesn't seem to + help. + +A file handling could be more robust; perhaps one should always cd to + the directory corresponding to the script buffer (currently only + done for the buffer which starts up the proof system) (30min tms) + +A replace (current-buffer) by proof-shell-buffer/proof-script-buffer + where ever possible (30 min tms) + +A Replace "You are not authorised for this information." by a proper + documentation (2h) + +A Reengineer *-count-undos and *-find-and-forget at generic level + (3h) + +B Allow bib-cite style clicking on Load/Import commands to go to file. + +C LEGO and Coq modes overwrite each other. + +C We need to go over to piped communication rather than ptys to fix + the (Solaris) ^G bug. In this circumstance there's a bug in the + eager annotation code + +C Outline-mode does not work due to read-only restrictions of + protected region + +B Remove LEGO-specific code in proof.el: for example, + proof-shell-eager-annotation-end, proof-included-files-list. + (added by hhg) + +B support font-lock in response buffer + +B Response buffer: after an error message has been displayed; ensure + that the error message is visible + +B Introduce keybinding to save the proof e.g., in LEGO, this should + insert "Save id" or "$Save id" depending on the name of the theorem. + +B use proof buffer instead of response buffer and leave non-proof + state output in the process buffer (1h) + +B Remove duplication of variables e.g., proof-prog-name and + lego-prog-name . (1h) + + +* Proof-by-Pointing +=================== + +A Fixing up errors caused by pbp-generated commands; currently, script + management unwisely assumes that pbp commands cannot fail (2h tms) + +A Rename pbp-mode to response-mode (which doesn't support any actual + proof-by-pointing) (30min) + +A Outsource actual pbp functionality (30min) + (separate pbp annotations from other annotations) + +C pbp code doesn't quite accord with the tech report; in particular it + decodes annotations eagerly. Lazily would be faster, and it's what + the tech report claims + --- djs: probably not much faster, actually. + +* Here are things to be done to Lego mode +========================================= + +A fix Pbp implementation (10h; tms) + +A Sometimes e.g., ~tms/lego/imperative/recursion/Prepare_vc.l, + annotations are recorded in the object file. This needs to be + changed in the SML code. (initially 2h tms) + +C Mechanism to save object file + +B Equiv, Next,... aren't handled properly, because LEGO does not + refresh the proof state. Perhaps it would be easiest to get LEGO to + output more information in proof script mode (2h tms) + +A Error messages need to be revised e.g., if an import fails, LEGO + outputs + + Error in file: search: undefined or out of context: should + (* closing file ./blah.l; time= 0.010000 gc= 0.0 sys= 0.0 *) + Error: Unwinding to top-level + + but script management only prints the last line. (5h tms) + +* Here are things to be done to Coq mode +======================================== + +B set proof-commands-regexp to support indentation for commands + (10min hhg) + +B Add Patrick Loiseleur's commands to search for vernac or ml files. + +C Sections and files are handled incorrectly. + +A Lifted nested lemmas respond incorrectly to C-c u: Coq gets sent the + correct command if I undo up to the lower lemma, but the buffer + undoes to the upper lemma. I.e., if I start Lemma x, then prove + Lemma y, then finish x, and undo lemma x, then lemma y gets undone + in the buffer as well. (45min hhg) + [ This seems to have corrected itself... hhg ] + +B Proof-by-Pointing (10h hhg) + +A Add coq-add-tactic with a tactic name, which adds that tactic to the + undoable tactics and to the font-lock. (2h hhg) + +* Emacs19 +========= + +B The proof-locked-span isn't set to read-only, because overlays don't + have that capability. This needs to be done with text-regions. + (2hr hhg) + +* Release +========= + +A remove CVS history in all files + +A extend Copyright to 1998 + +A Release Number 2.0
\ No newline at end of file |