aboutsummaryrefslogtreecommitdiff
path: root/acl2
diff options
context:
space:
mode:
Diffstat (limited to 'acl2')
-rw-r--r--acl2/README22
-rw-r--r--acl2/acl2.el71
-rw-r--r--acl2/example.acl213
-rw-r--r--acl2/x-symbol-acl2.el85
4 files changed, 191 insertions, 0 deletions
diff --git a/acl2/README b/acl2/README
new file mode 100644
index 00000000..fbe93440
--- /dev/null
+++ b/acl2/README
@@ -0,0 +1,22 @@
+ACL2 Proof General, for ACL2.
+
+Written by David Aspinall.
+
+Status: alpha; unsupported
+Maintainer: volunteer required
+ACL2 version: Tested briefly with acl2.5
+ACL2 homepage: http://www.cs.utexas.edu/users/moore/acl2
+
+========================================
+
+This is the absolute bare beginnings of a PG instance for ACL2.
+At the moment, only basic script management is configured.
+
+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.
+
+
+
+$Id$
+
diff --git a/acl2/acl2.el b/acl2/acl2.el
new file mode 100644
index 00000000..90a4486b
--- /dev/null
+++ b/acl2/acl2.el
@@ -0,0 +1,71 @@
+;; 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-assistant-home-page "http://www.cs.utexas.edu/users/moore/acl2"
+ proof-prog-name "acl2"
+
+ proof-script-sexp-commands t
+ proof-comment-start ";"
+ proof-comment-start ";"
+
+ proof-shell-annotated-prompt-regexp "ACL2[ !]*>+"
+
+ proof-shell-error-regexp "^Error: "
+ proof-shell-interrupt-regexp "Correctable error: Console interrupt."
+ proof-shell-prompt-pattern "ACL2[ !]*>+"
+
+ proof-shell-quit-cmd ":q" ;; FIXME: followed by C-d.
+ proof-shell-restart-cmd "#." ;; FIXME: maybe not?
+ proof-info-command ":help"
+
+ ;;
+ ;; Syntax table entries for proof scripts (FIXME: incomplete)
+ ;;
+ proof-script-syntax-table-entries
+ '(?\[ "(] "
+ ?\] "([ "
+ ?\( "() "
+ ?\) ")( "
+ ?. "w"
+ ?_ "w"
+ ?\' "' "
+ ?` "' "
+ ?, "' "
+ ?\| "."
+ ?\; "< "
+ ?\n "> "
+ )
+
+ ;; End of easy config.
+ )
+
+;; Interrupts and errors enter another loop; break out of it
+(add-hook
+ 'proof-shell-handle-error-or-interrupt-hook
+ (lambda () (proof-shell-insert ":q" nil)))
+
+
+
+(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..a493ab1a
--- /dev/null
+++ b/acl2/example.acl2
@@ -0,0 +1,13 @@
+;; 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)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 21:25:33 +0000