Fixes to twelf support, begins to work now.

4 files changed, 248 insertions, 98 deletions

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 () "->"  "\\<longrightarrow>")
+  '((arrowright () "->"  "\\<rightarrow>")
+    (longarrowright () "0->"  "\\<longrightarrow>")
     (longarrowdblright () "==>" "\\<Longrightarrow>")
     (logicaland     () "/\\" "\\<and>")
     (logicalor      () "\\/" "\\<or>")
     (equivalence    () "<->" "\\<equiv>")
     (existential1   () "EX"  "\\<exists>")
     (universal1     () "ALL"  "\\<forall>")
+    (bardash	    () "|-" "\\<turnstile>")
     ;; some naughty ones, but probably what you'd like
     ;; (a mess in words like "searching" "philosophy" etc!!)
     (Gamma  () "Gamma" "\\<Gamma>")