From 41ffd7a69ab0c181d6ad3c8866e24b4feebcde70 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 28 Sep 2000 09:03:56 +0000 Subject: Fixes to twelf support, begins to work now. --- twelf/example.elf | 5 ++ twelf/twelf-font.el | 124 ++++++++++++++++++++++++++++ twelf/twelf.el | 213 ++++++++++++++++++++++++++---------------------- twelf/x-symbol-twelf.el | 4 +- 4 files changed, 248 insertions(+), 98 deletions(-) (limited to 'twelf') diff --git a/twelf/example.elf b/twelf/example.elf index e52d5a06..b4281734 100644 --- a/twelf/example.elf +++ b/twelf/example.elf @@ -4,6 +4,11 @@ %%% $Id$ %%% +%%% Rather than a proof this file is just a signature, +%%% bunch of declarations. Would be nice to have something +%%% closer to other systems for pedagogical purposes... +%%% (i.e. proving commutativity of conjunction in ND fragment +%%% of this logic) %%% Intuitionistic propositional calculus %%% Positive fragment with implies, and, true. diff --git a/twelf/twelf-font.el b/twelf/twelf-font.el index 9ec58371..cc6a9910 100644 --- a/twelf/twelf-font.el +++ b/twelf/twelf-font.el @@ -8,6 +8,8 @@ ;; ;; +(require 'font-lock) + ;; FIXME da: integrate with PG's face mechanism? ;; (but maybe keep twelf faces to help users) ;; Also should add immediate fontification. @@ -312,6 +314,128 @@ For these purposes, an existential variable is a bound, upper-case identifier." ;(define-key twelf-mode-map "\C-cl" 'twelf-font-fontify-buffer) +;;; +;;; +;;; This comes from twelf-old.el but is needed for fontification, +;;; +;;; Perhaps some of these parsing functions will need reusing +;;; for sending input to server properly? +;;; + +;;; FIXME: some of names need fixing for safe conventions. + +(defun twelf-current-decl () + "Returns list (START END COMPLETE) for current Twelf declaration. +This should be the declaration or query under or just before +point within the nearest enclosing blank lines. +If declaration ends in `.' then COMPLETE is t, otherwise nil." + (let (par-start par-end complete) + (save-excursion + ;; Skip backwards if between declarations + (if (or (eobp) (looking-at (concat "[" *whitespace* "]"))) + (skip-chars-backward (concat *whitespace* "."))) + (setq par-end (point)) + ;; Move forward from beginning of decl until last + ;; declaration before par-end is found. + (if (not (bobp)) (backward-paragraph 1)) + (setq par-start (point)) + (while (and (twelf-end-of-par par-end) + (< (point) par-end)) + (setq par-start (point))) + ;; Now par-start is at end of preceding declaration or query. + (goto-char par-start) + (skip-twelf-comments-and-whitespace) + (setq par-start (point)) + ;; Skip to period or consective blank lines + (setq complete (twelf-end-of-par)) + (setq par-end (point))) + (list par-start par-end complete))) + +(defun twelf-next-decl (filename error-buffer) + "Set point after the identifier of the next declaration. +Return the declared identifier or `nil' if none was found. +FILENAME and ERROR-BUFFER are used if something appears wrong." + (let ((id nil) + end-of-id + beg-of-id) + (skip-twelf-comments-and-whitespace) + (while (and (not id) (not (eobp))) + (setq beg-of-id (point)) + (if (zerop (skip-chars-forward *twelf-id-chars*)) + ;; Not looking at id: skip ahead + (skip-ahead filename (current-line-absolute) "No identifier" + error-buffer) + (setq end-of-id (point)) + (skip-twelf-comments-and-whitespace) + (if (not (looking-at ":")) + ;; Not looking at valid decl: skip ahead + (skip-ahead filename (current-line-absolute end-of-id) "No colon" + error-buffer) + (goto-char end-of-id) + (setq id (buffer-substring beg-of-id end-of-id)))) + (skip-twelf-comments-and-whitespace)) + id)) + +(defconst *whitespace* " \t\n\f" + "Whitespace characters to be skipped by various operations.") + +(defconst *twelf-comment-start* (concat "%[%{" *whitespace* "]") + "Regular expression to match the start of a Twelf comment.") + +(defconst *twelf-id-chars* "a-z!&$^+/<=>?@~|#*`;,\\-\\\\A-Z_0-9'" + "Characters that constitute Twelf identifiers.") + +(defun skip-twelf-comments-and-whitespace () + "Skip Twelf comments (single-line or balanced delimited) and white space." + (skip-chars-forward *whitespace*) + (while (looking-at *twelf-comment-start*) + (cond ((looking-at "%{") ; delimited comment + (condition-case nil (forward-sexp 1) + (error (goto-char (point-max)))) + (or (eobp) (forward-char 1))) + (t ; single-line comment + (end-of-line 1))) + (skip-chars-forward *whitespace*))) + +(defun twelf-end-of-par (&optional limit) + "Skip to presumed end of current Twelf declaration. +Moves to next period or blank line (whichever comes first) +and returns t if period is found, nil otherwise. +Skips over comments (single-line or balanced delimited). +Optional argument LIMIT specifies limit of search for period." + (if (not limit) + (save-excursion + (forward-paragraph 1) + (setq limit (point)))) + (while (and (not (looking-at "\\.")) + (< (point) limit)) + (skip-chars-forward "^.%" limit) + (cond ((looking-at *twelf-comment-start*) + (skip-twelf-comments-and-whitespace)) + ((looking-at "%") + (forward-char 1)))) + (cond ((looking-at "\\.") + (forward-char 1) + t) + (t ;; stopped at limit + nil))) + +(defun skip-ahead (filename line message error-buffer) + "Skip ahead when syntactic error was found. +A parsable error message constited from FILENAME, LINE, and MESSAGE is +deposited in ERROR-BUFFER." + (if error-buffer + (save-excursion + (set-buffer error-buffer) + (goto-char (point-max)) + (insert filename ":" (int-to-string line) " Warning: " message "\n") + (setq *twelf-error-pos* (point)))) + (twelf-end-of-par)) + +(defun current-line-absolute (&optional char-pos) + "Return line number of CHAR-POS (default: point) in current buffer. +Ignores any possible buffer restrictions." + (1+ (count-lines 1 (or char-pos (point))))) (provide 'twelf-font) diff --git a/twelf/twelf.el b/twelf/twelf.el index 77730b00..f7be550f 100644 --- a/twelf/twelf.el +++ b/twelf/twelf.el @@ -7,65 +7,100 @@ ;; $Id$ ;; ;; +;; TODO before 3.2: +;; Info doc menu entry +;; X-Symbol upgrade/test? Mule XE better? +;; -;; FIXME: PG needs a bit of tuning to get this to work -;; properly, because of mixed syntax for comments. - -;; We should introduce a proof-parse-to-next-command -;; configurable setting, perhaps, which should skip -;; comments automatically. (require 'proof-easy-config) ; easy configure mechanism (require 'twelf-font) ; font lock configuration -;; (require 'twelf-old) ; port of parts of old code +;; (require 'twelf-old) ;; FIXME: put parts of old code into twelf-syntax or similar -(proof-easy-config - 'twelf "Twelf" +;; +;; User configuration settings for Twelf PG +;; +(defcustom twelf-root-dir + "/usr/local/twelf/" + "*Root of twelf installation. Default /usr/local/twelf suits RPM package." + :type 'file + :group 'twelf) + +(defcustom twelf-info-dir + (concat twelf-root-dir "doc/info/") + "*Directory of Twelf Infor files." + :type 'file + :group 'twelf) + +;; +;; Instantiation of Proof General +;; +(proof-easy-config 'twelf "Twelf" proof-prog-name "twelf-server" proof-assistant-home-page "http://www.cs.cmu.edu/~twelf/" - proof-terminal-char ?\. - proof-shell-auto-terminate-commands nil ; server commands don't end with . - ;; FIXME: must also cope with single line comments beginning with % - proof-comment-start "%{\\|^%" - proof-comment-end "}%\\|^%.*\n" - proof-comment-start-regexp "%[%{\t\n\f]" - proof-comment-end "" - - ;; FIXME: these don't apply? - proof-goal-command-regexp "^%theorem" - proof-save-command-regexp "" ;; FIXME: empty? - proof-goal-with-hole-regexp "^%theorem\w-+\\(.*\\)\w-+:" - proof-save-with-hole-regexp "" ;; FIXME - ;; proof-non-undoables-regexp "undo\\|back" - proof-goal-command "%theorem %s." - proof-save-command "%prove " - ;; proof-kill-goal-command "Goal \"PROP no_goal_set\";" + proof-script-use-new-parsing t ;; FIXME: remove for PG 3.3 + proof-terminal-char ?\. + proof-comment-start "%" ;; for inserting comments + proof-comment-end "" + proof-comment-start-regexp "%[%{ \t\n\f]" ;; recognizing + proof-comment-end-regexp "%}\\|\n" ;; comments -;; proof-showproof-command "pr()" -;; proof-undo-n-times-cmd "pg_repeat undo %s;" + proof-shell-auto-terminate-commands nil ; server commands don't end with . + proof-shell-strip-crs-from-input nil ; server needs CRs with readDecl proof-auto-multiple-files t proof-shell-cd-cmd "OS.chDir %s" proof-shell-prompt-pattern "%% OK %%\n" proof-shell-interrupt-regexp "interrupt" -;; proof-shell-start-goals-regexp "Level [0-9]" -;; proof-shell-end-goals-regexp "val it" proof-shell-annotated-prompt-regexp "%% [OA][KB]O?R?T? %%\n" proof-shell-error-regexp "Server error:" proof-shell-quit-cmd "quit" proof-shell-restart-cmd "reset" - ;; unset - ;; proof-shell-init-cmd - ;; "fun pg_repeat f 0 = () | pg_repeat f n = (f(); pg_repeat f (n-1));" - ;; proof-shell-proof-completed-regexp "^No subgoals!" - ;; proof-shell-eager-annotation-start - ;;"^\\[opening \\|^###\\|^Reading") - ) + ;; "Eager annotations" mark messages Proof General should display + ;; or recognize while the prover is pontificating + proof-shell-eager-annotation-start + "^\\[Opening \\|\\[Closing " + proof-shell-eager-annotation-end "\n") + + +;; unset: all of the interactive proof commands +;; These don't really apply, I don't think, because Twelf +;; only has fully automatic prover at the moment. +;; Also, there is no concept of "undo" to remove declarations +;; (can simply repeat them, tho.) +;; proof-goal-command-regexp "^%theorem" +;; proof-save-command-regexp "" ;; FIXME: empty? +;; proof-goal-with-hole-regexp "^%theorem\w-+\\(.*\\)\w-+:" +;; proof-save-with-hole-regexp "" ;; FIXME +;; proof-non-undoables-regexp +;; proof-goal-command "%theorem %s." +;; proof-save-command "%prove " +;; remaining strings are left over from Isabelle example +;; proof-kill-goal-command "Goal \"PROP no_goal_set\";" +;; proof-showproof-command "pr()" +;; proof-undo-n-times-cmd "pg_repeat undo %s;" +;; proof-shell-start-goals-regexp "Level [0-9]" +;; proof-shell-end-goals-regexp "val it" +;; proof-shell-init-cmd +;; proof-shell-proof-completed-regexp "^No subgoals!" + + +;; +;; Twelf server doesn't take declarations directly: +;; we need to pre-process script input slightly +;; + +(defun twelf-add-read-declaration () + "A hook value for `proof-shell-insert-hook'." + (if (eq action 'proof-done-advancing) + (setq string (concat "readDecl\n" string)))) + +(add-hook 'proof-shell-insert-hook 'twelf-add-read-declaration) ;; @@ -92,7 +127,10 @@ ;; Delimited comments are %{ }%, see 1234 below. (twelf-set-syntax ?\ " ") ; whitespace (twelf-set-syntax ?\t " ") ; whitespace -(twelf-set-syntax ?% "< 14") ; comment begin +; da: this old entry is wrong: it says % always starts a comment +;(twelf-set-syntax ?% "< 14") ; comment begin +; This next one is much better, +(twelf-set-syntax ?% ". 14") ; comment begin (twelf-set-syntax ?\n "> ") ; comment end (twelf-set-syntax ?: ". ") ; punctuation (twelf-set-syntax ?. ". ") ; punctuation @@ -100,8 +138,8 @@ (twelf-set-syntax ?\) ")( ") ; close delimiter (twelf-set-syntax ?\[ "(] ") ; open delimiter (twelf-set-syntax ?\] ")[ ") ; close delimiter -(twelf-set-syntax ?\{ "(}2 ") ; open delimiter -(twelf-set-syntax ?\} "){ 3") ; close delimiter +;(twelf-set-syntax ?\{ "(}2 ") ; open delimiter +;(twelf-set-syntax ?\} "){ 3") ; close delimiter ;; Actually, strings are illegal but we include: (twelf-set-syntax ?\" "\" ") ; string quote ;; \ is not an escape, but a word constituent (see above) @@ -110,65 +148,21 @@ ;; -;; Syntax highlighting (from twelf-old.el, needs work) +;; Syntax highlighting (from twelf-old.el, NEEDS WORK) ;; +;; Highlighting is maybe a nuisance for twelf because of its funny syntax. +;; But font lock could perhaps be got to work with recent versions. +;; That would be better than the present mechanism, which doesn't lock, +;; doesn't work well with X Symbol (which really needs locking), and +;; even breaks the background colouring for some reason (presumably +;; the Twelf faces) -;; Automatically highlight Twelf sources using font-lock -;; (FIXME: this is not so good, should work with font-lock properly!) (require 'twelf-font) -(add-hook 'twelf-mode-hook 'twelf-font-fontify-buffer) - -(defun twelf-current-decl () - "Returns list (START END COMPLETE) for current Twelf declaration. -This should be the declaration or query under or just before -point within the nearest enclosing blank lines. -If declaration ends in `.' then COMPLETE is t, otherwise nil." - (let (par-start par-end complete) - (save-excursion - ;; Skip backwards if between declarations - (if (or (eobp) (looking-at (concat "[" *whitespace* "]"))) - (skip-chars-backward (concat *whitespace* "."))) - (setq par-end (point)) - ;; Move forward from beginning of decl until last - ;; declaration before par-end is found. - (if (not (bobp)) (backward-paragraph 1)) - (setq par-start (point)) - (while (and (twelf-end-of-par par-end) - (< (point) par-end)) - (setq par-start (point))) - ;; Now par-start is at end of preceding declaration or query. - (goto-char par-start) - (skip-twelf-comments-and-whitespace) - (setq par-start (point)) - ;; Skip to period or consective blank lines - (setq complete (twelf-end-of-par)) - (setq par-end (point))) - (list par-start par-end complete))) - -(defun twelf-next-decl (filename error-buffer) - "Set point after the identifier of the next declaration. -Return the declared identifier or `nil' if none was found. -FILENAME and ERROR-BUFFER are used if something appears wrong." - (let ((id nil) - end-of-id - beg-of-id) - (skip-twelf-comments-and-whitespace) - (while (and (not id) (not (eobp))) - (setq beg-of-id (point)) - (if (zerop (skip-chars-forward *twelf-id-chars*)) - ;; Not looking at id: skip ahead - (skip-ahead filename (current-line-absolute) "No identifier" - error-buffer) - (setq end-of-id (point)) - (skip-twelf-comments-and-whitespace) - (if (not (looking-at ":")) - ;; Not looking at valid decl: skip ahead - (skip-ahead filename (current-line-absolute end-of-id) "No colon" - error-buffer) - (goto-char end-of-id) - (setq id (buffer-substring beg-of-id end-of-id)))) - (skip-twelf-comments-and-whitespace)) - id)) +(add-hook 'twelf-mode-hook 'twelf-mode-extra-config) + +(defun twelf-mode-extra-config () + (make-local-hook 'font-lock-after-fontify-buffer-hook) + (add-hook 'font-lock-after-fontify-buffer-hook 'twelf-font-fontify-buffer nil 'local)) (defconst twelf-syntax-menu '("Syntax Highlighting" @@ -179,9 +173,34 @@ FILENAME and ERROR-BUFFER are used if something appears wrong." ) "Menu for syntax highlighting in Twelf mode.") + +;; +;; Setting Twelf options via Proof General +;; + +(defpacustom chatter 1 + "Value for chatter." + :type 'integer + :setting "set chatter %i") + +(defpacustom double-check nil + "Double-check declarations after type reconstruction." + :type 'boolean + :setting "set doubleCheck %b") +(defpacustom print-implicit nil + "Show implicit arguments." + :type 'boolean + :setting "set Print.implict %b") + +;; etc + + +;; +;; Twelf menu +;; + (defpgdefault menu-entries (cdr twelf-syntax-menu)) - (provide 'twelf) \ No newline at end of file diff --git a/twelf/x-symbol-twelf.el b/twelf/x-symbol-twelf.el index 0b3f9f36..58f3fa08 100644 --- a/twelf/x-symbol-twelf.el +++ b/twelf/x-symbol-twelf.el @@ -6,13 +6,15 @@ ;; (defvar x-symbol-twelf-symbol-table - '((longarrowright () "->" "\\") + '((arrowright () "->" "\\") + (longarrowright () "0->" "\\") (longarrowdblright () "==>" "\\") (logicaland () "/\\" "\\") (logicalor () "\\/" "\\") (equivalence () "<->" "\\") (existential1 () "EX" "\\") (universal1 () "ALL" "\\") + (bardash () "|-" "\\") ;; some naughty ones, but probably what you'd like ;; (a mess in words like "searching" "philosophy" etc!!) (Gamma () "Gamma" "\\") -- cgit v1.2.3