diff options
Diffstat (limited to 'acl2')
| -rw-r--r-- | acl2/README | 22 | ||||
| -rw-r--r-- | acl2/acl2.el | 99 | ||||
| -rw-r--r-- | acl2/example.acl2 | 9 | ||||
| -rw-r--r-- | acl2/x-symbol-acl2.el | 85 |
4 files changed, 215 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..a7bf823d --- /dev/null +++ b/acl2/acl2.el @@ -0,0 +1,99 @@ +;; acl2.el Basic Proof General instance for ACL2 +;; +;; Copyright (C) 2000 LFCS Edinburgh. +;; License: GPL (GNU GENERAL PUBLIC LICENSE) +;; 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-script-comment-start ";" + proof-script-comment-start ";" + + proof-shell-annotated-prompt-regexp "ACL2[ !]*>+" + + proof-save-command-regexp "(def\\w+\\s " + proof-goal-command-regexp "(def\\w+\\s " + proof-save-with-hole-regexp "(def\\w+[ \t\n]+\\(\\w+\\)" + proof-save-with-hole-result 1 + proof-shell-error-regexp + "^Error: \\|Error in TOP-LEVEL: \\|\\*\\*\\*\\* FAILED \\*\\*\\*" + 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 ":q\n:q\n:q\n(lp)\n" ;; FIXME: maybe not? + proof-info-command ":help" + proof-undo-n-times-cmd ":ubt %s" ;; shouldn't give errors + proof-forget-id-command ":ubt %s" ;; so use ubt not ubt! + proof-context-command ":pbt :max" + ;; proof-showproof-cmd ":pbt :here" + + proof-shell-truncate-before-error nil + + ;; + ;; Syntax table entries for proof scripts (FIXME: incomplete) + ;; + proof-script-syntax-table-entries + '(?\[ "(] " + ?\] "([ " + ?\( "() " + ?\) ")( " + ?. "w " + ?_ "w " + ?- "w " + ?> "w " ;; things treated as names can have > in them + ?# "' " + ?\' "' " + ?` "' " + ?, "' " + ?\| "." + ?\; "< " + ?\n "> " + ) + + ;; A tiny bit of syntax highlighting + ;; + proof-script-font-lock-keywords + (append + (list + (proof-ids-to-regexp '("defthm" "defabbrev" "defaxiom" "defchoose" + "defcong" "defconst" "defdoc" "defequiv" + "defevaluator" "defpackage" "deflabel" "deftheory" + "implies" "equal" "and"))) + (if (boundp 'lisp-font-lock-keywords) ;; wins if font-lock is loaded + lisp-font-lock-keywords)) + + + ;; End of easy config. + ) + +;; Interrupts and errors enter another loop; break out of it +(add-hook + 'proof-shell-handle-error-or-interrupt-hook + (lambda () (if (eq proof-shell-error-or-interrupt-seen 'interrupt) + (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..a3a0f211 --- /dev/null +++ b/acl2/example.acl2 @@ -0,0 +1,9 @@ +;; Example proof script for ACL2 Proof General. +;; +;; $Id$ +;; + +(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) |