diff options
Diffstat (limited to 'hol98')
| -rw-r--r-- | hol98/README | 53 | ||||
| -rw-r--r-- | hol98/example.sml | 30 | ||||
| -rw-r--r-- | hol98/hol98.el | 157 | ||||
| -rw-r--r-- | hol98/todo | 25 | ||||
| -rw-r--r-- | hol98/x-symbol-hol98.el | 85 |
5 files changed, 350 insertions, 0 deletions
diff --git a/hol98/README b/hol98/README new file mode 100644 index 00000000..e6c3b4b3 --- /dev/null +++ b/hol98/README @@ -0,0 +1,53 @@ +HOL Proof General, for HOL98. + +Written by David Aspinall. + +Status: not officially supported yet +Maintainer: volunteer required +HOL version: HOL98, tested with Taupo 2 +HOL homepage: http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html + +======================================== + + +This is a "technology demonstration" of Proof General for HOL 98. + +It may work with other versions of HOL, but is untested (please let me +know if you try). Probably just a few settings need changing +to configure for different output formats. + +It has basic script management support, with a little bit of +decoration of scripts and output. + +There is support for X Symbol, but not using a proper token language. + +I have written this in the hope that somebody from the HOL community +will adopt it, maintain and improve it, and thus turn it into a proper +instantiation of Proof General. + + +------------ + +Notes: + +There are some problems at the moment. HOL proof scripts often use +batch-oriented single step tactic proofs, but Proof General does not +offer an easy way to edit these kind of proofs. The "Boomburg-HOL" +Emacs interface by Koichi Takahashi and Masima Hagiya addressed this, +and to some extent so perhaps does the Emacs interface supplied with +HOL. Perhaps one of these could be embedded/reimplemented inside +Proof General. Implemented in a generic way, managing batch vs +interactive proofs would also be useful for Isabelle. + +Another problem is that HOL scripts sometimes use SML structures, +which can cause confusion because Proof General does not really parse +SML, it just looks for semicolons. This could be improved by taking a +better parser (e.g. from sml mode). + +These improvements would be worthwhile contributions to Proof General +and also provide the HOL community with a nice front end. +Please have a go! + + +$Id$ + diff --git a/hol98/example.sml b/hol98/example.sml new file mode 100644 index 00000000..7e008eb8 --- /dev/null +++ b/hol98/example.sml @@ -0,0 +1,30 @@ +(* + Example proof script for HOL Proof General. + + $Id$ +*) + +g `A /\ B ==> B /\ A`; +e DISCH_TAC; +e CONJ_TAC; +e (IMP_RES_TAC AND_INTRO_THM); +e (IMP_RES_TAC AND_INTRO_THM); +val and_comms = pg_top_thm_and_drop(); + +(* Hints about HOL Proof General: + + Proof General needs to work with top-level declarations throughout, + and with "interactive" rather than "batch" versions of proofs. + + For best results, theorems should be saved in the way that they are + saved above, with pg_top_thm_and_drop. The function isn't + mysterious, it is defined as: + + fun pg_top_thm_and_drop () = let val t = top_thm(); in (drop(); t) end; +*) + +(* this simple proof is not quite like proofs in the other systems, + can anyone tell me a more similar proof in HOL? I want to split + the IMP_RES_TAC into two steps. +*) + diff --git a/hol98/hol98.el b/hol98/hol98.el new file mode 100644 index 00000000..d45c321c --- /dev/null +++ b/hol98/hol98.el @@ -0,0 +1,157 @@ +;; 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. + + +(require 'proof-easy-config) ; easy configure mechanism +(require 'proof-syntax) ; functions for making regexps + +(proof-easy-config 'hol98 "HOL" + proof-prog-name "hol.unquote" + proof-terminal-char ?\; + proof-script-comment-start "(*" + proof-script-comment-end "*)" + ;; These are all approximations, of course. + proof-goal-command-regexp "^g[ `]" + proof-save-command-regexp "pg_top_thm_and_drop" + proof-goal-with-hole-regexp "val \\(\\([^ \t=]*\\)\\)[ \t]*=[ \t]*prove" + proof-save-with-hole-regexp "val \\(\\([^ \t=]*\\)\\)[ \t]*=[ \t]*top_thm()" + proof-non-undoables-regexp "b()" ; and others.. + proof-goal-command "g `%s`;" + proof-save-command "val %s = pg_top_thm_and_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 "FileSys.chDir \"%s\"" + proof-shell-filename-escapes '(("\\\\" . "\\\\") ("\"" . "\\\"")) + proof-shell-prompt-pattern "^[->] " + proof-shell-interrupt-regexp "Interrupted" + 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 + "^- " + ;; This one is nice but less reliable, I think. + ;; "\\(> 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)); + fun pg_top_thm_and_drop () = let val t = top_thm(); in (drop(); t) end;" + ;; FIXME: add optional help topic parameter to help command. + proof-info-command "help \"hol\"" + proof-shell-proof-completed-regexp "Initial goal proved" + ;; FIXME: next one needs setting so that "urgent" messages are displayed + ;; eagerly from HOL. + ;; proof-shell-eager-annotation-start + proof-find-theorems-command "DB.match [] (%s);" + + ;; We must force this to use ptys since mosml doesn't flush its output + ;; (on Linux, presumably on Solaris too). + proof-shell-process-connection-type t + + ;; + ;; Syntax table entries for proof scripts + ;; + proof-script-syntax-table-entries + '(?\` "\"" + ?\$ "." + ?\/ "." + ?\\ "." + ?+ "." + ?- "." + ?= "." + ?% "." + ?< "." + ?> "." + ?\& "." + ?. "w" + ?_ "w" + ?\' "w" + ?\| "." + ?\* ". 23" + ?\( "()1" + ?\) ")(4") + + ;; + ;; A few of the vast variety of keywords, tactics, tacticals, + ;; for decorating proof scripts. + ;; + ;; In the future, PG will use a mechanism for passing identifier + ;; lists like this from the proof assistant, we don't really + ;; want to duplicate the information here! + ;; + hol98-keywords '("g" "expand" "e" "val" "store_thm" "top_thm" "by" + "pg_top_thm_and_drop" + "Define" "xDefine" "Hol_defn" + "Induct" "Cases" "Cases_on" "Induct_on" + "std_ss" "arith_ss" "list_ss" + "define_type") + hol98-rules '("ASSUME" "REFL" "BETA_CONV" "SUBST" + "ABS" "INST_TYPE" "DISCH" "MP" + "T_DEF" "FORALL_DEF" "AND_DEF" "OR_DEF" "F_DEF" + "NOT_DEF" "EXISTS_UNIQUE_DEF" "BOOL_CASES_AX" + "IMP_ANTISYM_AX" "ETA_AX" "SELECT_AX" "ONE_ONE_DEF" + "ONTO_DEF" "INFINITY_AX" "LET_DEF" "COND_DEF" "ARB_DEF") + hol98-tactics '("ACCEPT_TAC" "ASSUME_TAC" "GEN_TAC" + "CONJ_TAC" "DISCH_TAC" "STRIP_TAC" + "SUBST_TAC" "ASM_CASES_TAC" "DISJ_CASES_TAC" + "REWRITE_TAC" "IMP_RES_TAC" "ALL_TAC" "NO_TAC" + "EQ_TAC" "EXISTS_TAC" "INDUCT_TAC" + "POP_ASM" "SUBST1_TAC" "ASSUM_LIST" + "PROVE" "PROVE_TAC" "DECIDE" "DECIDE_TAC" "RW_TAC" + "STP_TAC" "ZAP_TAC" + "EXISTS_TAC") + hol98-tacticals '("ORELSE" "FIRST" "CHANGED_TAC" "THEN" + "THENL" "EVERY" "REPEAT" + "MAP_EVERY") + proof-script-font-lock-keywords + (list + (cons (proof-ids-to-regexp hol98-keywords) 'font-lock-keyword-face) + (cons (proof-ids-to-regexp hol98-tactics) 'font-lock-keyword-face) + ; (cons (proof-ids-to-regexp hol98-rules) 'font-lock-keyword-face) + (cons (proof-ids-to-regexp hol98-tacticals) 'proof-tacticals-name-face)) + + ;; + ;; Some decoration of the goals output + ;; + proof-goals-font-lock-keywords + (list + (cons (proof-ids-to-regexp '("Proof manager status" + "proof" "Incomplete" + "Initial goal proved" + "Initial goal" + "There are currently no proofs" + "OK")) + 'font-lock-keyword-face) + (cons (regexp-quote "------------------------------------") + 'font-lock-comment-face) + (cons ": GoalstackPure.goalstack" 'proof-boring-face) + (cons ": GoalstackPure.proofs" 'proof-boring-face) + (cons ": Thm.thm" 'proof-boring-face) + (cons "val it =" 'proof-boring-face)) + + ;; End of easy config. + ) + + +(warn "Hol Proof General is incomplete! Please help improve it! +Read the manual, make improvements and send them to proofgen@dcs.ed.ac.uk") + +(provide 'hol98) diff --git a/hol98/todo b/hol98/todo new file mode 100644 index 00000000..d65df204 --- /dev/null +++ b/hol98/todo @@ -0,0 +1,25 @@ +-*- mode:outline -*- + +* Things to do for HOL + +See also ../todo for generic things to do, priority codes. + +** A Problem with process filtering. + + Process (sometimes?) doesn't recover after interrupt, and no output + is seen. Why? + + Also problem with some input texts: try interactive version of + clScript.sml, inductive defn of CL terms breaks things. + +** B Improve display to strip ugly val it and spurious >'s. + +** B Add special markup to improve robustness + +** B Add support for multiple files + +** B Add support for proof by pointing. + +** B Output highlighting doesn't seem to work properly. + + diff --git a/hol98/x-symbol-hol98.el b/hol98/x-symbol-hol98.el new file mode 100644 index 00000000..920af03d --- /dev/null +++ b/hol98/x-symbol-hol98.el @@ -0,0 +1,85 @@ +;; x-symbol-hol98.el +;; +;; David Aspinall, adapted from file supplied by David von Obheimb +;; +;; $Id$ +;; + +(defvar x-symbol-hol98-symbol-table + '((longarrowright () "->" "\\<longrightarrow>") + (longarrowdblright () "==>" "\\<Longrightarrow>") + (logicaland () "/\\" "\\<and>") + (logicalor () "\\/" "\\<or>") + (equivalence () "<->" "\\<equiv>") + (existential1 () "EX" "\\<exists>") + (universal1 () "ALL" "\\<forall>") + ;; 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) +;; Setting token shape prevents "philosophy" example, but still +;; problems, e.g. delphi, false1. (Pierre) +(defvar x-symbol-hol98-token-shape '(?_ "[A-Za-z]+" . "[A-Za-z_]")) +(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) |