diff options
Diffstat (limited to 'lego')
| -rw-r--r-- | lego/BUGS | 53 | ||||
| -rw-r--r-- | lego/README | 37 | ||||
| -rw-r--r-- | lego/example.l | 15 | ||||
| -rw-r--r-- | lego/example2.l | 1 | ||||
| -rw-r--r-- | lego/lego-syntax.el | 120 | ||||
| -rw-r--r-- | lego/lego.el | 444 | ||||
| -rw-r--r-- | lego/legotags | 91 | ||||
| -rw-r--r-- | lego/readonly/readonly.l | 1 | ||||
| -rw-r--r-- | lego/todo | 44 | ||||
| -rw-r--r-- | lego/x-symbol-lego.el | 83 |
10 files changed, 889 insertions, 0 deletions
diff --git a/lego/BUGS b/lego/BUGS new file mode 100644 index 00000000..bfe39752 --- /dev/null +++ b/lego/BUGS @@ -0,0 +1,53 @@ +-*- mode:outline -*- + +* LEGO Proof General Bugs + +See also ../BUGS for generic bugs. + + +** PBP doesn't work on FSF, reason mentioned in generic bugs. + +** [FSF specific] `proof-zap-commas-region' does not work for Emacs + + On lego/example.l . On *initially* fontifying the buffer, + commas are not zapped [unfontified]. However, when entering text, + commata are zapped correctly. Workaround: don't stare too much at commata + +** If LEGO attempts to write a (object) file in a non-writable directory + + It forgets the protocol mechanism on how to interact with + Proof General and gets stuck. Workaround: Directly enter "Configure + AnnotateOn" in the Proof Shell to recover. + +** After a `Discharge', retraction ought to only be possible back + + to the first declaration/definition which is discharged. However, + LEGO Proof General does not know that Discharge has such a non-local + effect. Workaround: retract back to the first declaration/definition + which is discharged. + +** A thorny issue is local definitions in a proof state. + + LEGO cannot undo them explicitly. Workaround: retract back to a + command before a definition. + +** Normalisation commands such as `Dnf', `Hnf' `Normal' cannot be undone + + in a proof state by Proof General. Workaround: retract back to the + start of the proof. + +** After LEGO has issued a `*** QED ***' you may undo steps in the proof + + as long as you don't issue a `Save' command or start a new proof. + LEGO Proof General assumes that all proofs are terminated with a + proper `Save' command. Workaround: Always issue a `Save' command after + completing a proof. If you forget one, you should retract to a point + before the offending proof development. + +** legotags doesn't find all declarations. + + It cannot handle lists e.g., with [x,y:nat]; it only tags x but not y. + [The same problem exists for coqtags] + Workaround: don't rely too much on the etags mechanism. + + diff --git a/lego/README b/lego/README new file mode 100644 index 00000000..273c3e90 --- /dev/null +++ b/lego/README @@ -0,0 +1,37 @@ +LEGO Proof General + +Written by Thomas Kleymann and Dilip Sequeira. +Later maintainance by David Aspinall and Paul Callaghan. + +Status: supported +Maintainer: Paul Callaghan / David Aspinall +LEGO version: 1.3.1 +LEGO homepage: http://www.lfcs.informatics.ed.ac.uk/lego + +======================================== + +LEGO Proof General has full support for multiple file scripting, and +experimental support for proof by pointing. + +There is support for X Symbol, but not using a proper token language. + +There is a tags program, legotags. + +======================================== + +Installation notes: + +Install legotags in a standard place or add <proofgeneral-home>/lego +to your PATH. +NB: You may need to change the path to perl at the top of the file. + +Generate a TAGS file for the Lego library by running + legotags `find . -name \*.l -print` +in the root directory of the library. + + + +======================================== + +$Id$ + diff --git a/lego/example.l b/lego/example.l new file mode 100644 index 00000000..535d5712 --- /dev/null +++ b/lego/example.l @@ -0,0 +1,15 @@ +(* + Example proof script for Lego Proof General. + + $Id$ +*) + +Module example Import lib_logic; + +Goal {A,B:Prop}(A /\ B) -> (B /\ A); +intros; +Refine H; +intros; +andI; +Immed; +Save and_comms; diff --git a/lego/example2.l b/lego/example2.l new file mode 100644 index 00000000..37d1e563 --- /dev/null +++ b/lego/example2.l @@ -0,0 +1 @@ +Module example2 Import "readonly/readonly";
\ No newline at end of file diff --git a/lego/lego-syntax.el b/lego/lego-syntax.el new file mode 100644 index 00000000..5cf7867a --- /dev/null +++ b/lego/lego-syntax.el @@ -0,0 +1,120 @@ +;; lego-syntax.el Syntax of LEGO +;; Copyright (C) 1994 - 1998 LFCS Edinburgh. +;; Author: Thomas Kleymann and Dilip Sequeira +;; License: GPL (GNU GENERAL PUBLIC LICENSE) +;; Maintainer: Paul Callaghan <P.C.Callaghan@durham.ac.uk> + +;; +;; $Id$ +;; + +(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 +(defconst lego-error-regexp "^\\(cannot assume\\|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 + 'proof-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 + 'proof-declaration-name-face) + + ;; Kinds + (cons (concat "\\<Prop\\>\\|\\<Type\\s *\\((" + lego-id ")\\)?") 'font-lock-type-face) + + ;; Special hacks!! + (cons "Discharge.." 'font-lock-keyword-face) + (cons "\\*\\*\\* QED \\*\\*\\*" 'font-lock-keyword-face)) + "*Font-lock table for LEGO terms (displayed in output buffers).") + +;; 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 "\\(" (proof-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 "\\(" (proof-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 (proof-ids-to-regexp lego-keywords) 'font-lock-keyword-face) + (cons (proof-ids-to-regexp lego-tacticals) 'proof-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) + ;; Remove spurious variable and function faces on commas. + '(proof-zap-commas)))) + +(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")) + +(provide 'lego-syntax) diff --git a/lego/lego.el b/lego/lego.el new file mode 100644 index 00000000..6a8b50d6 --- /dev/null +++ b/lego/lego.el @@ -0,0 +1,444 @@ +;; lego.el Major mode for LEGO proof assistants +;; Copyright (C) 1994 - 1998 LFCS Edinburgh. +;; Author: Thomas Kleymann and Dilip Sequeira +;; License: GPL (GNU GENERAL PUBLIC LICENSE) +;; Maintainer: Paul Callaghan <P.C.Callaghan@durham.ac.uk> + +;; +;; $Id$ +;; + +(require 'proof) +(require 'lego-syntax) + +;;;;;;;;;;;;;;;;;;;;;;;;;; +;;; User Configuration ;;; +;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; I believe this is standard for Linux under RedHat -tms +(defcustom lego-tags "/usr/lib/lego/lib_Type/" + "*The directory of the TAGS table for the LEGO library" + :type 'file + :group 'lego) + +(defcustom lego-test-all-name "test_all" + "*The name of the LEGO module which inherits all other modules of the + library." + :type 'string + :group 'lego) + +(defpgdefault help-menu-entries + '(["LEGO Reference Card" (browse-url lego-www-refcard) t] + ["LEGO library (WWW)" (browse-url lego-library-www-page) t])) + +(defpgdefault menu-entries + '(["intros" lego-intros t] + ["Intros" lego-Intros t] + ["Refine" lego-Refine t])) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;; Configuration of Generic Proof Package ;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Users should not need to change this. + +(defvar lego-shell-process-output + '((lambda (cmd string) (proof-string-match "^Module" cmd)) . + (lambda (cmd string) + (setq proof-shell-delayed-output + ;;FIXME: This should be displayed in the minibuffer only + (cons 'insert "\n\nImports done!")))) + "Acknowledge end of processing import declarations.") + +(defconst lego-process-config + ;; da: I think "Configure AnnotateOn;" is only included here for + ;; safety since there is a bug in LEGO which turns it off + ;; inadvertently sometimes. + "Init XCC; Configure PrettyOn; Configure AnnotateOn;" + "Command to initialise the LEGO process. + +Initialises empty context and prepares XCC theory. +Enables pretty printing. +Activates extended printing routines required for Proof General.") + +(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") + +;; ----- web documentation + +(defcustom lego-www-home-page "http://www.dcs.ed.ac.uk/home/lego/" + "Lego home page URL." + :type 'string + :group 'lego) + +(defcustom lego-www-latest-release + "http://www.dcs.ed.ac.uk/home/lego/html/release-1.3.1/" + "The WWW address for the latest LEGO release." + :type 'string + :group 'lego) + +(defcustom lego-www-refcard + (concat lego-www-latest-release "refcard.ps.gz") + "URL for the Lego reference card." + :type 'string + :group 'lego) + +(defcustom lego-library-www-page + (concat lego-www-latest-release "library/library.html") + "The HTML documentation of the LEGO library." + :type 'string + :group 'lego) + + +;; ----- lego-shell configuration options + +(defvar lego-prog-name "lego" + "*Name of program to run as lego.") + +(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\\|Forget forced KillRef" + "*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 "^" (proof-ids-to-regexp lego-keywords-save))) +(defvar lego-goal-command-regexp + (concat "^" (proof-ids-to-regexp lego-keywords-goal))) + +(defvar lego-kill-goal-command "KillRef;") +(defvar lego-forget-id-command "Forget %s;") + +(defvar lego-undoable-commands-regexp + (proof-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 "[[*]\\|" + (proof-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" + ;; With nil argument for docstring, Emacs makes up a nice one. + nil + (lego-shell-mode-config)) + +(define-derived-mode lego-mode proof-mode + "lego" nil + (lego-mode-config)) + +(eval-and-compile + (define-derived-mode lego-response-mode proof-response-mode + "LEGOResp" nil + (setq font-lock-keywords lego-font-lock-terms) + (lego-init-syntax-table) + (proof-response-config-done))) + +(define-derived-mode lego-goals-mode proof-goals-mode + "LEGOGoals" "LEGO Proof State" + (lego-goals-mode-config)) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Code that's lego specific ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; needs to handle Normal as well +;; it should ignore Normal TReg Normal VReg and (Normal ...) +(defun lego-count-undos (span) + "This is how to work out what the undo commands are. +Given is the first SPAN which needs to be undone." + (let ((ct 0) str i) + (while span + (setq str (span-property span 'cmd)) + (cond ((eq (span-property span 'type) 'vanilla) + (if (or (proof-string-match lego-undoable-commands-regexp str) + (and (proof-string-match "Equiv" str) + (not (proof-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))) + ;; FIXME: make this stuff generic. This should be undo-n-times-cmd + (concat "Undo " (int-to-string ct) ";"))) + +(defun lego-goal-command-p (str) + "Decide whether argument is a goal or not" + (proof-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) + (unless (eq (span-property span 'name) proof-unnamed-theorem-name) + (setq ans (format lego-forget-id-command (span-property span 'name))))) + ;; alternative definitions + ((proof-string-match lego-definiendum-alternative-regexp str) + (setq ans (format lego-forget-id-command (match-string 1 str)))) + ;; declarations + ((proof-string-match (concat "\\`\\$?" (lego-decl-defn-regexp "[:|=]")) str) + (let ((ids (match-string 1 str))) ; returns "a,b" + (proof-string-match proof-id ids) ; matches "a" + (setq ans (format lego-forget-id-command (match-string 1 ids))))) + + ((proof-string-match "\\`\\(Inductive\\|\\Record\\)\\s-*\\[\\s-*\\w+\\s-*:[^;]+\\`Parameters\\s-*\\[\\s-*\\(\\w+\\)\\s-*:" str) + (setq ans (format lego-forget-id-command (match-string 2 str)))) + + ((proof-string-match + "\\`\\(Inductive\\|Record\\)\\s-*\\[\\s-*\\(\\w+\\)\\s-*:" str) + (setq ans + (format lego-forget-id-command (match-string 2 str)))) + + ((proof-string-match "\\`\\s-*Module\\s-+\\(\\S-+\\)\\W" str) + (setq ans (format "ForgetMark %s;" (match-string 1 str))))) + ;; Carry on searching forward for something to forget + ;; (The first thing to be forget will forget everything following) + (setq span (next-span span 'type))) + (or ans proof-no-command))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Other stuff which is required to customise script management ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun lego-goal-hyp () + (cond + ((looking-at lego-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 (proof-string-match lego-undoable-commands-regexp cmd))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Commands specific to lego ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(proof-defshortcut lego-Intros "Intros " [(control I)]) +(proof-defshortcut lego-intros "intros " [(control i)]) +(proof-defshortcut lego-Refine "Refine " [(control r)]) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; 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 () + "Use LEGO's pretty printing facilities to adjust output line width. +Checks the width in the `proof-goals-buffer'" + (and (buffer-live-p proof-goals-buffer) + (proof-shell-live-buffer) + (save-excursion + (set-buffer proof-goals-buffer) + (let ((current-width + ;; Actually, one might sometimes + ;; want to get the width of the proof-response-buffer + ;; instead. Never mind. + (window-width (get-buffer-window proof-goals-buffer)))) + (if (equal current-width lego-shell-current-line-width) () + ; else + (setq lego-shell-current-line-width current-width) + (set-buffer proof-shell-buffer) + (insert (format lego-pretty-set-width (- current-width 1))) + ))))) + +(defun lego-pre-shell-start () + (setq proof-prog-name lego-prog-name + proof-mode-for-shell 'lego-shell-mode + proof-mode-for-response 'lego-response-mode + proof-mode-for-goals 'lego-goals-mode)) + + +(defun lego-mode-config () + + (setq proof-terminal-char ?\;) + (setq proof-script-comment-start "(*") + (setq proof-script-comment-end "*)") + + (setq proof-assistant-home-page lego-www-home-page) + + (setq proof-mode-for-script 'lego-mode) + + (setq proof-showproof-command "Prf;" + proof-goal-command "Goal %s;" + proof-save-command "Save %s;" + proof-context-command "Ctxt;" + proof-info-command "Help;") + + (setq proof-goal-command-p 'lego-goal-command-p + proof-completed-proof-behaviour 'closeany ; new in 3.0 + proof-count-undos-fn 'lego-count-undos + proof-find-and-forget-fn 'lego-find-and-forget + pg-topterm-goalhyp-fn 'lego-goal-hyp + proof-state-preserving-p 'lego-state-preserving-p) + + (setq proof-save-command-regexp lego-save-command-regexp + proof-goal-command-regexp lego-goal-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-indent-any-regexp + (proof-regexp-alt (proof-ids-to-regexp lego-commands) "\\s(" "\\s)")) + + (lego-init-syntax-table) + + ;; da: I've moved these out of proof-config-done in proof-script.el + (setq pbp-goal-command "Pbp %s;") + (setq pbp-hyp-command "PbpHyp %s;") + +;; font-lock + + (setq font-lock-keywords lego-font-lock-keywords-1) + + (proof-config-done) + +;; 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 blink-matching-paren-dont-ignore-comments t) + +;; hooks and callbacks + + (add-hook 'proof-pre-shell-start-hook 'lego-pre-shell-start nil t) + (add-hook 'proof-shell-insert-hook 'lego-shell-adjust-line-width)) + +(defun lego-equal-module-filename (module filename) + "Returns `t' if MODULE is equal to the FILENAME and `nil' otherwise. +The directory and extension is stripped of FILENAME before the test." + (equal module + (file-name-sans-extension (file-name-nondirectory filename)))) + +(defun lego-shell-compute-new-files-list (str) + "Function to update `proof-included-files list'. + +It needs to return an up to date list of all processed files. Its +output is stored in `proof-included-files-list'. Its input is the +string of which `lego-shell-retract-files-regexp' matched a +substring. + +We assume that module identifiers coincide with file names." + (let ((module (match-string 1 str))) + (cdr (member-if + (lambda (filename) (lego-equal-module-filename module filename)) + proof-included-files-list)))) + +(defun lego-shell-mode-config () + (setq proof-shell-prompt-pattern lego-shell-prompt-pattern + proof-shell-cd-cmd 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-assumption-regexp lego-id + pg-subterm-first-special-char ?\360 + proof-shell-wakeup-char ?\371 + pg-subterm-start-char ?\372 + pg-subterm-sep-char ?\373 + pg-subterm-end-char ?\374 + pg-topterm-char ?\375 + proof-shell-eager-annotation-start "\376" + proof-shell-eager-annotation-start-length 1 + 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-pre-sync-init-cmd "Configure AnnotateOn;" + proof-shell-init-cmd lego-process-config + proof-shell-restart-cmd lego-process-config + pg-subterm-anns-use-stack nil + proof-shell-process-output-system-specific lego-shell-process-output + lego-shell-current-line-width nil + + proof-shell-process-file + (cons "Creating mark \"\\(.*\\)\" \\[\\(.*\\)\\]" + (lambda (str) (let ((match (match-string 2 str))) + (if (equal match "") match + (concat (file-name-sans-extension match) ".l"))))) + + proof-shell-retract-files-regexp + "forgot back through Mark \"\\(.*\\)\"" + font-lock-keywords lego-font-lock-keywords-1 + + proof-shell-compute-new-files-list + 'lego-shell-compute-new-files-list) + + (lego-init-syntax-table) + + (proof-shell-config-done)) + +(defun lego-goals-mode-config () + (setq pg-goals-change-goal "Next %s;" + pg-goals-error-regexp lego-error-regexp) + (setq font-lock-keywords lego-font-lock-terms) + (lego-init-syntax-table) + (proof-goals-config-done)) + + +(provide 'lego) diff --git a/lego/legotags b/lego/legotags new file mode 100644 index 00000000..8243287a --- /dev/null +++ b/lego/legotags @@ -0,0 +1,91 @@ +#!/usr/bin/perl +# +# Or perhaps: /usr/local/bin/perl +# +# $Id$ +# +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; +} + diff --git a/lego/readonly/readonly.l b/lego/readonly/readonly.l new file mode 100644 index 00000000..11719f49 --- /dev/null +++ b/lego/readonly/readonly.l @@ -0,0 +1 @@ +Module readonly;
\ No newline at end of file diff --git a/lego/todo b/lego/todo new file mode 100644 index 00000000..dc0b1f28 --- /dev/null +++ b/lego/todo @@ -0,0 +1,44 @@ +-*- mode:outline -*- + +* Things to do for LEGO + +See also ../todo for generic things to do, priority codes. + +** C Improve X-Symbol support. + +** D Fix Pbp implementation in LEGO itself (10h) + +** D In LEGO, apart from Goal...Save pairs, we have + declaration...discharge pairs. See the section "Granularity of + Atomic Commands" for a proposal on how to generalise the current + implementation so that it can also deal with "Discharge". + [See also the Coq problem with Sections] (6h) + +** D Inoking an "Expand" command produces a new proof state. But this is + incorrectly displayed in the response buffer and not the goals + buffer because special annotations are missing. Presumably, one + ought to replace "Toplevel.Pr()" by "Toplevel.PR()" in the + definition of "Expand" (see file newtop.sml [Version 1.4]). (30min) + +** D Even with the more flexible region model, with + proof-nested-goals-behaviour=closequick, Proof General doesn't + do quite the right thing. Forget for a definition when inside + a proofstate kills off the whole proofstate. Effectively, + the definition is *global* rather than local to the proofstate, + and could perhaps be lifted to before the goal + (with the lift-global nonsense not so daft after all? Editing + behind the user's back is still objectionable though). + Another alternative fix would be to trigger some retraction action + on seeing the "Abort" regexp, rather than assuming it is the result of + some retraction action. More generally this could be used for error + handling. + +** D Improve legotags. It cannot handle lists e.g., with + [x,y:nat]; + it only tags x but not y. [The same problem exists for coqtags] + +** X Mechanism to save object file. Specifically, after having processed + a script (interactively), it would be nice if one could now save the + buffer in object format. At the moment, it only gets converted + (automatically) when it is read in indirectly at a later stage. + However, there is currently no LEGO command to do this. [4h] diff --git a/lego/x-symbol-lego.el b/lego/x-symbol-lego.el new file mode 100644 index 00000000..c434ac46 --- /dev/null +++ b/lego/x-symbol-lego.el @@ -0,0 +1,83 @@ +;; x-symbol-lego.el +;; +;; David Aspinall, adapted from file supplied by David von Obheimb +;; License: GPL (GNU GENERAL PUBLIC LICENSE) +;; +;; $Id$ +;; + +(defvar x-symbol-lego-symbol-table + '((longarrowright () "->" "\\<longrightarrow>") + (logicaland () "/\\" "\\<and>") + (logicalor () "\\/" "\\<or>") + ;; Some naughty ones, but probably what you'd like. + ;; FIXME: can we set context to prevent accidental use, + ;; e.g. sear<chi>ng ? + (Gamma () "Gamma" "\\<Gamma>") + (Delta () "Delta" "\\<Delta>") + (Theta () "Theta" "\\<Theta>") + (Lambda () "Lambda" "\\<Lambda>") + (Pi () "Pi" "\\<Pi>") + (Sigma () "Sigma" "\\<Sigma>") + (Phi () "Phi" "\\<Phi>") + (Psi () "Psi" "\\<Psi>") + (Omega () "Omega" "\\<Omega>") + (alpha () "alpha" "\\<alpha>") + (beta () "beta" "\\<beta>") + (gamma () "gamma" "\\<gamma>") + (delta () "delta" "\\<delta>") + (epsilon1 () "epsilon" "\\<epsilon>") + (zeta () "zeta" "\\<zeta>") + (eta () "eta" "\\<eta>") + (theta1 () "theta" "\\<theta>") + (kappa1 () "kappa" "\\<kappa>") + (lambda () "lambda" "\\<lambda>") + ; (mu () "mu" "\\<mu>") + ; (nu () "nu" "\\<nu>") + ; (xi () "xi" "\\<xi>") + ; (pi () "pi" "\\<pi>") + (rho () "rho" "\\<rho>") + (sigma () "sigma" "\\<sigma>") + (tau () "tau" "\\<tau>") + (phi1 () "phi" "\\<phi>") + ; (chi () "chi" "\\<chi>") + (psi () "psi" "\\<psi>") + (omega () "omega" "\\<omega>"))) + +;; All the stuff X-Symbol complains about +(defvar x-symbol-lego-master-directory 'ignore) +(defvar x-symbol-lego-image-searchpath '("./")) +(defvar x-symbol-lego-image-cached-dirs '("images/" "pictures/")) +(defvar x-symbol-lego-image-keywords nil) +(defvar x-symbol-lego-font-lock-keywords nil) +(defvar x-symbol-lego-header-groups-alist nil) +(defvar x-symbol-lego-class-alist + '((VALID "Lego Symbol" (x-symbol-info-face)) + (INVALID "no Lego Symbol" (red x-symbol-info-face)))) +(defvar x-symbol-lego-class-face-alist nil) +(defvar x-symbol-lego-electric-ignore nil) +(defvar x-symbol-lego-required-fonts nil) +(defvar x-symbol-lego-case-insensitive nil) +;; Setting token shape prevents "philosophy" example, but still +;; problems, e.g. delphi, false1. (Pierre) +(defvar x-symbol-lego-token-shape '(?_ "[A-Za-z]+" . "[A-Za-z_]")) +(defvar x-symbol-lego-table x-symbol-lego-symbol-table) +(defun x-symbol-lego-default-token-list (tokens) tokens) +(defvar x-symbol-lego-token-list 'x-symbol-lego-default-token-list) +(defvar x-symbol-lego-input-token-ignore nil) + +;; internal stuff +(defvar x-symbol-lego-exec-specs nil) +(defvar x-symbol-lego-menu-alist nil) +(defvar x-symbol-lego-grid-alist nil) +(defvar x-symbol-lego-decode-atree nil) +(defvar x-symbol-lego-decode-alist nil) +(defvar x-symbol-lego-encode-alist nil) +(defvar x-symbol-lego-nomule-decode-exec nil) +(defvar x-symbol-lego-nomule-encode-exec nil) + +(warn "LEGO support for X-Symbol is highly incomplete! Please help improve it! +Send improvements to x-symbol-lego.el to proofgen@dcs.ed.ac.uk") + + +(provide 'x-symbol-lego) |