Experimental hol-light version, not usable yet

3 files changed, 248 insertions, 0 deletions

diff --git a/hol-light/README b/hol-light/README
new file mode 100644
index 00000000..edcba896
--- /dev/null
+++ b/hol-light/README
@@ -0,0 +1,53 @@
+HOL Light in Proof General.
+
+Written by David Aspinall.
+
+Status:	           not officially supported yet
+Maintainer:       volunteer required
+HOL-Ligh version:
+HOL homepage:      http://hol.sourceforge.net
+
+========================================
+
+
+This is a "technology demonstration" of Proof General for HOL-Light.
+
+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 Unicode Tokens.
+
+I have written this in the hope that somebody from the HOL-Light
+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 might also be useful for other provers.
+
+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/hol-light/example.ml b/hol-light/example.ml
new file mode 100644
index 00000000..ccd59c23
--- /dev/null
+++ b/hol-light/example.ml
@@ -0,0 +1,32 @@
+(*
+    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);;
+
+goal `A && B ==> B && A`;
+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/hol-light/hol-light.el b/hol-light/hol-light.el
new file mode 100644
index 00000000..9b662038
--- /dev/null
+++ b/hol-light/hol-light.el
@@ -0,0 +1,163 @@
+;; hol-light.el   Basic Proof General instance for HOL Light
+;;
+;; Copyright (C) 2010 LFCS Edinburgh, David Aspinall.
+;;
+;; Author: David Aspinall <David.Aspinall@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
+
+(defvar hol-light-keywords nil)
+(defvar hol-light-rules nil)
+(defvar hol-light-tactics nil)
+(defvar hol-light-tacticals nil)
+
+(proof-easy-config  'hol-light "HOL Light"
+ proof-prog-name		 "ocaml"
+ proof-terminal-string           ";;"
+ 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   "let \\(\\([^ \t=]*\\)\\)[ \t]*=[ \t]*prove"
+ proof-save-with-hole-regexp   "let \\(\\([^ \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              "#cd \"%s\""
+ proof-shell-filename-escapes    '(("\\\\" . "\\\\") ("\""   . "\\\""))
+ 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 "Characters [0-9]+-[0-9]+:"
+ proof-shell-init-cmd 
+ '("#cd \"/Users/da/hol_light\"" 
+   "#use \"hol.ml\""
+   "let rec pg_repeat f n = match n with 0 -> () | _ -> (f(); pg_repeat f (n-1));;"
+   "let pg_top_thm_and_drop () = let t = top_thm() in (b(); t);;")
+
+ ;; 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);"
+
+ proof-forget-id-command	";" ;; vacuous: but empty string doesn't give
+				    ;; new prompt
+ ;; 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!
+ ;;
+ hol-light-keywords  '("g" "expand" "e" "let" "store_thm" "top_thm" "by"
+		   "Define" "xDefine" "Hol_defn"
+		   "Induct" "Cases" "Cases_on" "Induct_on"
+		   "std_ss" "arith_ss" "list_ss"
+		   "define_type")
+ hol-light-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")
+ hol-light-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")
+ hol-light-tacticals '("ORELSE" "FIRST" "CHANGED_TAC" "THEN"
+		   "THENL" "EVERY" "REPEAT"
+		   "MAP_EVERY")
+ proof-script-font-lock-keywords
+ (list
+  (cons (proof-ids-to-regexp hol-light-keywords) 'font-lock-keyword-face)
+  (cons (proof-ids-to-regexp hol-light-tactics) 'font-lock-keyword-face)
+  ; (cons (proof-ids-to-regexp hol-light-rules) 'font-lock-keyword-face)
+  (cons (proof-ids-to-regexp hol-light-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 Light Proof General is incomplete!  Please help improve it!
+Read the manual, make improvements, upload at http://proofgeneral.inf.ed.ac.uk/trac")
+
+(provide 'hol-light)