From a1f38c7d643246761804359354c11c6c183a9d20 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 9 Mar 2000 11:03:17 +0000 Subject: First bash at HOL support, working but barely --- hol98/example.sml | 22 ++++++++++++++ hol98/hol98.el | 69 +++++++++++++++++++++++++++++++++++++++++ hol98/x-symbol-hol98.el | 81 +++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 172 insertions(+) create mode 100644 hol98/example.sml create mode 100644 hol98/hol98.el create mode 100644 hol98/x-symbol-hol98.el (limited to 'hol98') 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 +;; +;; $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 () "->" "\\") + (logicaland () "/\\" "\\") + (logicalor () "\\/" "\\") + (equivalence () "<->" "\\") + (existential1 () "EX" "\\") + ;; some naughty ones, but probably what you'd like + ;; (a mess in words like "searching" "philosophy" etc!!) + (Gamma () "Gamma" "\\") + (Delta () "Delta" "\\") + (Theta () "Theta" "\\") + (Lambda () "Lambda" "\\") + (Pi () "Pi" "\\") + (Sigma () "Sigma" "\\") + (Phi () "Phi" "\\") + (Psi () "Psi" "\\") + (Omega () "Omega" "\\") + (alpha () "alpha" "\\") + (beta () "beta" "\\") + (gamma () "gamma" "\\") + (delta () "delta" "\\") + (epsilon1 () "epsilon" "\\") + (zeta () "zeta" "\\") + (eta () "eta" "\\") + (theta1 () "theta" "\\") + (kappa1 () "kappa" "\\") + (lambda () "lambda" "\\") +; (mu () "mu" "\\") +; (nu () "nu" "\\") +; (xi () "xi" "\\") +; (pi () "pi" "\\") + (rho () "rho" "\\") + (sigma () "sigma" "\\") + (tau () "tau" "\\") + (phi1 () "phi" "\\") +; (chi () "chi" "\\") + (psi () "psi" "\\") + (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) -- cgit v1.2.3