First (non-working) versions, committed so that doc builds.

4 files changed, 291 insertions, 0 deletions

diff --git a/acl2/README b/acl2/README
new file mode 100644
index 00000000..961e287a
--- /dev/null
+++ b/acl2/README
@@ -0,0 +1,30 @@
+ACL2 Proof General, for ACL2.
+
+Written by David Aspinall.
+
+$Id$
+
+Status:	       not officially supported yet
+Maintainer:    volunteer required
+ACL2 version:  Tested briefly with
+ACL2 homepage: 
+
+========================================
+
+
+This is a "technology demonstration" of Proof General for ACL2.
+
+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 ACL2 community
+will adopt it, maintain and improve it, and thus turn it into a proper
+instantiation of Proof General.
+
+
+------------
+
+Notes:
+
diff --git a/acl2/acl2.el b/acl2/acl2.el
new file mode 100644
index 00000000..6e6d3af4
--- /dev/null
+++ b/acl2/acl2.el
@@ -0,0 +1,162 @@
+;; acl2.el   Basic Proof General instance for ACL2
+;;
+;; 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
+
+(setq auto-mode-alist                   ; ACL2 uses two file extensions
+      (cons				; Only grab .lisp extension after 
+       (cons "\\.lisp$" 'acl2-mode)	; an acl2 file has been loaded
+       auto-mode-alist))	
+
+(proof-easy-config  'acl2 "ACL2" 
+ proof-prog-name		 "bash"
+ proof-script-sexp-commands	 t
+ proof-comment-start             ";"
+ ;; FIXME:
+ 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. 
+ ;; Have patch ready for PG 3.3
+ 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!
+ ;;
+ acl2-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")
+ acl2-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")
+ acl2-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")
+ acl2-tacticals '("ORELSE" "FIRST" "CHANGED_TAC" "THEN"
+		   "THENL" "EVERY" "REPEAT"
+		   "MAP_EVERY")
+ proof-script-font-lock-keywords	
+ (list
+  (cons (proof-ids-to-regexp acl2-keywords) 'font-lock-keyword-face)
+  (cons (proof-ids-to-regexp acl2-tactics) 'font-lock-keyword-face)
+  ; (cons (proof-ids-to-regexp acl2-rules) 'font-lock-keyword-face)
+  (cons (proof-ids-to-regexp acl2-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 "ACL2 Proof General is incomplete!  Please help improve it!
+Read the manual, make improvements and send them to feedback@proofgeneral.org")
+
+(provide 'acl2)
diff --git a/acl2/example.acl2 b/acl2/example.acl2
new file mode 100644
index 00000000..e597cd29
--- /dev/null
+++ b/acl2/example.acl2
@@ -0,0 +1,14 @@
+(*
+    Example proof script for ACL2 Proof General.
+
+    $Id$
+*)    
+
+(defthm assoc->assoc-equal
+  (equal (assoc x a)
+	 (assoc-equal x a)))
+
+(defthm assoc->assoc-equal
+  (equal (assoc x a)
+	 (assoc-equal x a)))
+
diff --git a/acl2/x-symbol-acl2.el b/acl2/x-symbol-acl2.el
new file mode 100644
index 00000000..b532d708
--- /dev/null
+++ b/acl2/x-symbol-acl2.el
@@ -0,0 +1,85 @@
+;; x-symbol-acl2.el
+;;
+;; David Aspinall, adapted from file supplied by David von Obheimb
+;;
+;; $Id$
+;;
+
+(defvar x-symbol-acl2-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-acl2-master-directory 'ignore)
+(defvar x-symbol-acl2-image-searchpath '("./"))
+(defvar x-symbol-acl2-image-cached-dirs '("images/" "pictures/"))
+(defvar x-symbol-acl2-image-keywords nil)
+(defvar x-symbol-acl2-font-lock-keywords nil)
+(defvar x-symbol-acl2-header-groups-alist nil)
+(defvar x-symbol-acl2-class-alist 
+  '((VALID "Acl2 Symbol" (x-symbol-info-face))
+    (INVALID "no Acl2 Symbol" (red x-symbol-info-face))))
+(defvar x-symbol-acl2-class-face-alist nil)
+(defvar x-symbol-acl2-electric-ignore nil)
+(defvar x-symbol-acl2-required-fonts nil)
+(defvar x-symbol-acl2-case-insensitive nil)
+;; Setting token shape prevents "philosophy" example, but still
+;; problems, e.g. delphi, false1.  (Pierre)
+(defvar x-symbol-acl2-token-shape '(?_ "[A-Za-z]+" . "[A-Za-z_]"))
+(defvar x-symbol-acl2-table x-symbol-acl2-symbol-table)
+(defun x-symbol-acl2-default-token-list (tokens) tokens)
+(defvar x-symbol-acl2-token-list 'x-symbol-acl2-default-token-list)
+(defvar x-symbol-acl2-input-token-ignore nil)
+
+;; internal stuff 
+(defvar x-symbol-acl2-exec-specs nil)
+(defvar x-symbol-acl2-menu-alist nil)
+(defvar x-symbol-acl2-grid-alist nil)
+(defvar x-symbol-acl2-decode-atree nil)
+(defvar x-symbol-acl2-decode-alist nil)
+(defvar x-symbol-acl2-encode-alist nil)
+(defvar x-symbol-acl2-nomule-decode-exec nil)
+(defvar x-symbol-acl2-nomule-encode-exec nil)
+
+(warn "Acl2 support for X-Symbol is highly incomplete!  Please help improve it!
+Send improvements to x-symbol-acl2.el to proofgen@proofeneral.org")
+
+
+(provide 'x-symbol-acl2)