First bash at HOL support, working but barely

3 files changed, 172 insertions, 0 deletions

diff --git a/hol98/example.sml b/hol98/example.sml
new file mode 100644
index 00000000..04b3b062
--- /dev/null
+++ b/hol98/example.sml
@@ -0,0 +1,22 @@
+(*
+    Example proof script for HOL Proof General.
+
+    $Id$
+*)    
+
+g `A /\ B ==> B /\ A`;
+e DISCH_TAC;
+e CONJ_TAC;
+
+
+(* Ooops, I'm stuck now.  Can somebody help?? 
+   Just want a simple low-level proof here. *)
+
+
+
+
+
+
+
+
+
diff --git a/hol98/hol98.el b/hol98/hol98.el
new file mode 100644
index 00000000..a6c5ca71
--- /dev/null
+++ b/hol98/hol98.el
@@ -0,0 +1,69 @@
+;; hol98.el   Basic Proof General instance for HOL 98
+;;
+;; Copyright (C) 2000 LFCS Edinburgh. 
+;;
+;; Author: David Aspinall <da@dcs.ed.ac.uk>
+;;
+;; $Id$
+;;
+;; Needs improvement!
+;;
+;; See the README file in this directory for information.
+
+
+;; keywords:
+;; val prove store_thm prove by
+;; tacticals: THEN THENL 
+;; by seems to be "e";
+
+
+(require 'proof-easy-config)            ; easy configure mechanism
+(require 'proof-syntax)
+
+(proof-easy-config  'hol98 "HOL" 
+ proof-prog-name		 "hol.unquote"
+ proof-terminal-char             ?\;
+ proof-comment-start             "(*"
+ proof-comment-end               "*)"
+ proof-goal-command-regexp       "^g[ `]"
+ proof-save-command-regexp       "^qed"
+ proof-goal-with-hole-regexp     "qed_goal \"\\(\\(.*\\)\\)\""
+ proof-save-with-hole-regexp     "qed \"\\(\\(.*\\)\\)\""
+ proof-non-undoables-regexp      "b()"
+ proof-goal-command              "g `%s`;"
+ proof-save-command              "val %s = top_thm(); drop();"
+ proof-kill-goal-command         "drop();"
+ proof-showproof-command         "p()"
+ proof-undo-n-times-cmd          "(pg_repeat backup %s; p());"
+ proof-auto-multiple-files       t
+; proof-shell-cd-cmd              "cd \"%s\""
+ proof-shell-prompt-pattern      "^[->] "
+ proof-shell-interrupt-regexp    "Interrupted"
+; proof-shell-start-goals-regexp  "Proof manager status\\|OK.."
+ proof-shell-start-goals-regexp  
+ (proof-regexp-alt "Proof manager status" "OK.." "val it =\n")
+ proof-shell-end-goals-regexp    
+ (proof-regexp-alt "^[ \t]*: GoalstackPure.goalstack"
+		   "^[ \t]*: GoalstackPure.proofs")
+ proof-shell-quit-cmd            "quit();"
+ proof-assistant-home-page    
+ "http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html"
+ proof-shell-annotated-prompt-regexp 
+ "^\\(> val it = () : unit\n\\)?- "
+ proof-shell-error-regexp        "^! "
+ proof-shell-init-cmd		  
+ "Help.displayLines:=3000;
+  fun pg_repeat f 0 = () | pg_repeat f n = (f(); pg_repeat f (n-1));"
+ ;; FIXME: add optional help topic parameter to help command. 
+ ;; Have patch ready for PG 3.2, but PG 3.1 is strictly bug fix.
+ proof-info-command "help \"hol\""
+ proof-shell-proof-completed-regexp   
+ "\\(\\(.\\|\n\\)*No subgoals!\n\\)"
+; proof-shell-eager-annotation-start
+ proof-find-theorems-command	"DB.match [] (%s);"
+ ;; We must set this to use ptys since mosml doesn't flush its output
+ ;; (on Linux, presumably on Solaris to).
+ proof-shell-process-connection-type t
+ )
+
+(provide 'demoisa)
\ No newline at end of file
diff --git a/hol98/x-symbol-hol98.el b/hol98/x-symbol-hol98.el
new file mode 100644
index 00000000..cf4614ec
--- /dev/null
+++ b/hol98/x-symbol-hol98.el
@@ -0,0 +1,81 @@
+;; x-symbol-hol98.el
+;;
+;; David Aspinall, adapted from file supplied by David von Obheimb
+;;
+;; $Id$
+;;
+
+(defvar x-symbol-hol98-symbol-table 
+  '((longarrowright () "->"  "\\<longrightarrow>")
+    (logicaland     () "/\\" "\\<and>")
+    (logicalor      () "\\/" "\\<or>")
+    (equivalence    () "<->" "\\<equiv>")
+    (existential1   () "EX"  "\\<exists>")
+    ;; some naughty ones, but probably what you'd like
+    ;; (a mess in words like "searching" "philosophy" etc!!)
+    (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-hol98-master-directory 'ignore)
+(defvar x-symbol-hol98-image-searchpath '("./"))
+(defvar x-symbol-hol98-image-cached-dirs '("images/" "pictures/"))
+(defvar x-symbol-hol98-image-keywords nil)
+(defvar x-symbol-hol98-font-lock-keywords nil)
+(defvar x-symbol-hol98-header-groups-alist nil)
+(defvar x-symbol-hol98-class-alist 
+  '((VALID "Hol98 Symbol" (x-symbol-info-face))
+    (INVALID "no Hol98 Symbol" (red x-symbol-info-face))))
+(defvar x-symbol-hol98-class-face-alist nil)
+(defvar x-symbol-hol98-electric-ignore nil)
+(defvar x-symbol-hol98-required-fonts nil)
+(defvar x-symbol-hol98-case-insensitive nil)
+(defvar x-symbol-hol98-token-shape nil)
+(defvar x-symbol-hol98-table x-symbol-hol98-symbol-table)
+(defun x-symbol-hol98-default-token-list (tokens) tokens)
+(defvar x-symbol-hol98-token-list 'x-symbol-hol98-default-token-list)
+(defvar x-symbol-hol98-input-token-ignore nil)
+
+;; internal stuff 
+(defvar x-symbol-hol98-exec-specs nil)
+(defvar x-symbol-hol98-menu-alist nil)
+(defvar x-symbol-hol98-grid-alist nil)
+(defvar x-symbol-hol98-decode-atree nil)
+(defvar x-symbol-hol98-decode-alist nil)
+(defvar x-symbol-hol98-encode-alist nil)
+(defvar x-symbol-hol98-nomule-decode-exec nil)
+(defvar x-symbol-hol98-nomule-encode-exec nil)
+
+(warn "Hol98 support for X-Symbol is highly incomplete!  Please help improve it!
+Send improvements to x-symbol-hol98.el to proofgen@dcs.ed.ac.uk")
+
+
+(provide 'x-symbol-hol98)