Fully working Isabelle PG in 30 setqs

1 files changed, 37 insertions, 156 deletions

diff --git a/demoisa/demoisa.el b/demoisa/demoisa.el
index d5098019..1d9dbf53 100644
--- a/demoisa/demoisa.el
+++ b/demoisa/demoisa.el
@@ -6,18 +6,25 @@
 ;;
 ;; $Id$
 ;;
-;;
 ;; =================================================================
 ;;
-;; This is a much-whittled down version of Isabelle Proof General,
-;; supplied as an (almost) minimal demonstration of how to instantiate
-;; Proof General to a particular proof assistant.  It uses the plain
-;; xterm interface of Isabelle, to demonstrate that hacking the proof
-;; assistant is not necessary to get basic features working.
+;;		Isabelle Proof General in 30 setqs
+;;
+;; This is a whittled down version of Isabelle Proof General, supplied
+;; as an (almost) minimal demonstration of how to instantiate Proof
+;; General to a particular proof assistant.  You can use this as a
+;; template to get support for a new assistant going.
+;;
+;; This mode uses the unadulterated terminal interface of Isabelle, to
+;; demonstrate that hacking the proof assistant is not necessary to
+;; get basic features working.
 ;;
-;; This mode really works!  You you get a toolbar, menus, short-cut
-;; keys, script management, a function menu, ability to run proof
-;; assistant remotely, etc, etc.
+;; And it really works!  You you get a toolbar, menus, short-cut keys,
+;; script management for multiple files, a function menu, ability to
+;; run proof assistant remotely, etc, etc.
+;;
+;; To try it out, set in the shell PROOFGENERAL_ASSISTANTS=demoisa
+;; before invoking Emacs.  (Of course, you need Isabelle installed).
 ;;
 ;; What's missing? 
 ;;
@@ -62,9 +69,9 @@
 ;; ======== User settings for Isabelle ========
 ;;
 ;; Defining variables using customize is pretty easy.
-;; You should do it at least for your user options.
+;; You should do it at least for your prover-specific user options.
 ;;
-;; proof-site provides use with two customization groups
+;; proof-site provides us with two customization groups
 ;; automatically:  (based on the name of the assistant)
 ;;
 ;; 'isabelledemo        -  User options for Isabelle Demo Proof General
@@ -75,6 +82,7 @@
 ;;   ProofGeneral -> Customize -> Isabelledemo 
 ;; The second group appears in the menu:
 ;;   ProofGeneral -> Internals -> Isabelledemo config
+;;
 
 (defcustom isabelledemo-prog-name "isabelle"
   "*Name of program to run Isabelle."
@@ -87,11 +95,6 @@
   :type 'string
   :group 'isabelledemo-config)
 
-(defcustom isabelledemo-not-undoable-commands-regexp
-  "undo\\|back"
-  "Regular expression matching commands which are *not* undoable."
-  :type 'regexp
-  :group 'isabelledemo-config)
 
 ;;
 ;; ======== Configuration of generic modes ========
@@ -100,76 +103,39 @@
 (defun demoisa-config ()
   "Configure Proof General scripting for Isabelle."
   (setq
-   ;; proof script syntax
    proof-terminal-char		?\;	; ends every command
    proof-comment-start		"(*"
    proof-comment-end		"*)"
-
-   ;; Next four used for function-menu and recognizing goal..save
-   ;; regions in script buffer.
-   ;; Isabelle has many (unbounded!) possible forms, we
-   ;; only match one form here.  
    proof-goal-command-regexp    "^Goal"
    proof-save-command-regexp    "^qed"
-   proof-goal-with-hole-regexp  "^Goal \"%s\""
-   proof-save-with-hole-regexp  "^qed \"%s\""
-
-   ;; proof engine commands
+   proof-goal-with-hole-regexp  "^Goal \\(\\(\"%s\"\\)\\)"
+   proof-save-with-hole-regexp  "^qed \\(\\(\"%s\"\\)\\)"
+   proof-non-undoables-regexp   "undo\\|back"
+   proof-undo-n-times-cmd	"pg_repeat undo %s;"
    proof-showproof-command	"pr()"
    proof-goal-command		"Goal \"%s\";"
    proof-save-command		"qed \"%s\";"
    proof-kill-goal-command	"Goal \"PROP no_goal_set\";"
-
-   ;; command hooks
-   proof-goal-command-p		'demoisa-goal-command-p
-   proof-count-undos-fn		'demoisa-count-undos
-   proof-find-and-forget-fn	'demoisa-find-and-forget
-   proof-goal-hyp-fn		'demoisa-goal-hyp
-   proof-state-preserving-p	'demoisa-state-preserving-p
-
-   ;; For the help menu
    proof-assistant-home-page	isabelledemo-web-page
-
-   ;; Self-referential variable that's used to find
-   ;; buffers in the scripting mode.
-   proof-mode-for-script	'demoisa-proofscript-mode))
+   proof-auto-multiple-files    t))
 
 
 (defun demoisa-shell-config ()
   "Configure Proof General shell for Isabelle."
   (setq
-   proof-shell-first-special-char	?\350
-
-   ;; 
    proof-shell-annotated-prompt-regexp   "^\\(val it = () : unit\n\\)?ML>? "
-
-   ;; cd command makes proof assistant follow directory of
-   ;; current proof script (in case of included files).
    proof-shell-cd-cmd			"cd \"%s\""
-
-   ;; This pattern is just for interaction in comint (shell buffer).
-   ;; You don't need to set it.
    proof-shell-prompt-pattern		"[ML-=#>]+>? "
-
    proof-shell-interrupt-regexp         "Interrupt"
    proof-shell-error-regexp		"\\*\\*\\*\\|^.*Error:\\|^uncaught exception \\|^Exception- "
-   
-   proof-shell-start-goals-regexp	"\n"
-   proof-shell-end-goals-regexp		""
-
-   proof-shell-proof-completed-regexp
-   (concat proof-shell-start-goals-regexp
-	   "\\(\\(.\\|\n\\)*\nNo subgoals!\n\\)"
-	   proof-shell-end-goals-regexp)
-
-   ;; init-command sent on startup
-   proof-shell-init-cmd                 "version;"
-   proof-shell-quit-cmd			"quit();"
-
-   ;; "urgent" messages displayed by Isabelle are highlighted in the
-   ;; respoonse buffer, by matching with these regexps.
-   proof-shell-eager-annotation-start   "^\\[opening \\|^###\\|^Reading\\|"
-   proof-shell-eager-annotation-end     "]$\\|)$"))
+   proof-shell-start-goals-regexp	"Level [0-9]"
+   proof-shell-end-goals-regexp		"val it"
+   proof-shell-proof-completed-regexp   "\\(\\(.\\|\n\\)*No subgoals!\n\\)"
+   proof-shell-eager-annotation-start   "^\\[opening \\|^###\\|^Reading"
+   proof-shell-init-cmd  ; define a utility function, in a lib somewhere?
+   "fun pg_repeat f 0 = () 
+      | pg_repeat f n = (f(); pg_repeat f (n-1));"
+   proof-shell-quit-cmd			"quit();"))
 
 
 
@@ -182,7 +148,6 @@
 ;;
 ;; The derived modes set the variables, then call the
 ;; <mode>-config-done function to complete configuration.
-;;
 
 (define-derived-mode demoisa-mode proof-mode
     "Isabelle Demo script" nil
@@ -205,16 +170,15 @@
 ;; The response buffer and goals buffer modes defined above are
 ;; trivial.  In fact, we don't need to define them at all -- they
 ;; would simply default to "proof-response-mode" and "pbp-mode".
-;;
+
 ;; A more sophisticated instantiation might set font-lock-keywords to
 ;; add highlighting, or some of the proof by pointing markup
 ;; configuration for the goals buffer.
 
-
-;; The final piece of magic here is a hook which configures
-;; the bare minimum to get the proof shell running.  
-;; Proof General needs to know the name of the program to
-;; run, and the modes for the shell, response, and goals buffers.
+;; The final piece of magic here is a hook which configures settings
+;; to get the proof shell running.  Proof General needs to know the
+;; name of the program to run, and the modes for the shell, response,
+;; and goals buffers.
 
 (add-hook 'proof-pre-shell-start-hook 'demoisa-pre-shell-start)
 
@@ -224,87 +188,4 @@
   (setq proof-mode-for-response 'demoisa-response-mode)
   (setq proof-mode-for-pbp	'demoisa-goals-mode))
 
-
-
-;;
-;; ======== Hook functions used above ========
-;;
-;;
-;; Code here has to be written specifically for each prover.
-;;
-;; There are four hook functions: count-undos, find-and-forget,
-;;
-
-;;
-;; 1. count-undos
-;;
-;; This calculates undo operations within a proof. 
-;;
-(defun demoisa-count-undos (span)
-  "Count number of undos in a span, return the command needed to undo that far."
-  (let 
-      ((case-fold-search nil)
-       (ct 0) str i)
-    (if (and span (prev-span span 'type)
-	     (not (eq (span-property (prev-span span 'type) 'type) 'comment))
-	     (demoisa-goal-command-p
-	      (span-property (prev-span span 'type) 'cmd)))
-	(concat "choplev 0" proof-terminal-string)
-      (while span
-	(setq str (span-property span 'cmd))
-	(cond ((eq (span-property span 'type) 'vanilla)
-	       (or (proof-string-match isabelledemo-not-undoable-commands-regexp str)
-		   (setq ct (+ 1 ct))))
-	      ((eq (span-property span 'type) 'pbp)
-	       ;; this case probably redundant for Isabelle, unless
-	       ;; we think of some nice ways of matching non-undoable
-	       ;; commands.
-	       (cond ((not (proof-string-match isabelledemo-not-undoable-commands-regexp str))
-		      (setq i 0)
-		      (while (< i (length str))
-			(if (= (aref str i) proof-terminal-char)
-			    (setq ct (+ 1 ct)))
-			(setq i (+ 1 i))))
-		     (t nil))))
-	(setq span (next-span span 'type)))
-      (concat "ProofGeneral.repeat_undo " (int-to-string ct) proof-terminal-string))))
-
-(defun demoisa-goal-command-p (str)
-  "Decide whether argument is a goal or not"
-  (proof-string-match demoisa-goal-command-regexp str)) ; this regexp defined in demoisa-syntax.el
-
-;;
-;; 2. find-and-forget
-;;
-;; This calculates undo operations outwith a proof.  If we retract
-;; before a "Goal" command, proof-kill-goal-command is sent, followed
-;; by whatever is calculated by this function.
-;;
-;; Isabelle has no concept of a linear context, and you can happily
-;; redeclare values in ML.  So forgetting back to the declaration of a
-;; particular something makes no real sense.  
-;; The function is given a trivial implementation in this case.
-;;
-;; Find LEGO or Coq's implementation of this function to see how to
-;; write it for proof assistants that can do this.
-
-(defun demoisa-find-and-forget (span)
-  proof-no-command)
-
-
-;; Parse proofstate output.  Isabelle does not display
-;; named hypotheses in the proofstate output:  they
-;; appear as a list in each subgoal.  Ignore
-;; that aspect for now and just return the
-;; subgoal number.
-(defun demoisa-goal-hyp ()
-  (if (looking-at proof-shell-goal-regexp)
-      (cons 'goal (match-string 1))))
-
-(defun demoisa-state-preserving-p (cmd)
-  "Non-nil if command preserves the proofstate."
-  (not (proof-string-match isabelledemo-not-undoable-commands-regexp cmd)))
-
-
-
 (provide 'demoisa)