Import acl2_7.4dfsg.orig.tar.gz

[dgit import orig acl2_7.4dfsg.orig.tar.gz]

34 files changed, 4047 insertions, 0 deletions

diff --git a/books/hacking/Readme.lsp b/books/hacking/Readme.lsp
new file mode 100644
index 0000000..4a50528
--- /dev/null
+++ b/books/hacking/Readme.lsp
@@ -0,0 +1,118 @@
+((:FILES "
+.:
+all.acl2
+all.lisp
+bridge.acl2
+bridge.lisp
+copyright
+defcode.acl2
+defcode.lisp
+defstruct-parsing.acl2
+defstruct-parsing.lisp
+dynamic-make-event.acl2
+dynamic-make-event.lisp
+dynamic-make-event-test.acl2
+dynamic-make-event-test.lisp
+hacker.acl2
+hacker.lisp
+hacker-pkg.lsp
+Makefile
+progn-bang-enh.acl2
+progn-bang-enh.lisp
+raw.acl2
+raw.lisp
+Readme.lsp
+redefun.acl2
+redefun.lisp
+rewrite-code.acl2
+rewrite-code.lisp
+rewrite-code-pkg.lsp
+subsumption.acl2
+subsumption.lisp
+table-guard.acl2
+table-guard.lisp
+"
+)
+ (:TITLE    "Hacking & Extending ACL2")
+ (:AUTHOR/S "Peter C. Dillinger") ; With guidance & advice from Matt Kaufmann and Panagiotis Manolios
+ (:KEYWORDS ; non-empty list of keywords, case-insensitive
+   "book contributions" "contributed books"
+   "hacking" "system" "defcode" "redefun" "trust tags" "ttags"
+   "extensions" "raw mode" "raw lisp"
+   )
+ (:ABSTRACT
+"This support code is intended as a library to those who wish to use
+trust tags to modify or extend core ACL2 behavior.  We add some other
+constructs to the set of low-level tools enabled by trust tags that make
+system modifications easier to specify and keep track of.  We also offer
+some high-level tools that offer significant benefits (in both ease &
+soundness) over more direct methods of overriding behavior.  See the
+comments in Readme.lsp and individual files for more info.
+")
+ (:PERMISSION ; author/s permission for distribution and copying:
+"Copyright (C) 2008 Peter C. Dillinger, the Georgia Tech Research Corporation,
+                    and Northeastern University
+
+This program is free software; you can redistribute it and/or
+modify it under the terms of the GNU General Public License
+as published by the Free Software Foundation; either version 2
+of the License, or (at your option) any later version.
+
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+GNU General Public License for more details.
+
+You should have received a copy of the GNU General Public License
+along with this program; if not, write to the Free Software
+Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
+02110-1301, USA."))
+
+#|
+This was developed as part of ACL2s: "The ACL2 Sedan."
+
+hacker-pkg.lsp
+    Package & documentation topic/section used in preambles
+
+
+all.lisp
+    Book that includes all of the below
+
+bridge.lisp
+    Book for bridging the gap between ACL2 and raw Lisp
+
+defcode.lisp
+    Book for the DEFCODE construct (ttag required)
+
+defstruct-parsing.lisp
+    Book for parsing defstruct calls
+
+dynamic-make-event.lisp
+    Support for modified events to return a make-event expansion.
+
+dynamic-make-event-test.lisp
+    A regression test for dynamic-make-event.
+
+hacker.lisp
+    Basic book with hacking constructs
+
+progn-bang-enh.lisp
+    Used by defcode.lisp.  Subject to change. :)
+
+raw.lisp
+    Book for making raw definitions in a nice way
+
+redefun.lisp
+    Book for overriding and rewriting existing definitions
+
+rewrite-code.lisp
+    Book with tools for rewriting and copying existing code
+    (used by redefun.lisp)
+
+subsumption.lisp
+    Book with constructs to do ttag subsumption
+
+table-guard.lisp
+    An example application of this stuff to allow extension of table
+    guards, including the acl2-defaults-table.
+|#
diff --git a/books/hacking/all.acl2 b/books/hacking/all.acl2
new file mode 100644
index 0000000..d24e20d
--- /dev/null
+++ b/books/hacking/all.acl2
@@ -0,0 +1,5 @@
+(in-package "ACL2")
+(ld "hacker-pkg.lsp")
+(ld "rewrite-code-pkg.lsp")
+; cert-flags: ? t :ttags ((defcode) (table-guard))
+(certify-book "all" ? t :ttags ((defcode) (table-guard)))
diff --git a/books/hacking/all.lisp b/books/hacking/all.lisp
new file mode 100644
index 0000000..fbfbb31
--- /dev/null
+++ b/books/hacking/all.lisp
@@ -0,0 +1,22 @@
+(in-package "ACL2")
+
+; Modification by Matt K. after v4-3: Removed :load-compiled-file :comp, which
+; was part of all include-book forms just below, in support of provisional
+; certification.  Presumably the indicate books have already been compiled by
+; now, anyhow.
+
+(include-book "hacker")
+
+(include-book "defstruct-parsing")
+(include-book "rewrite-code")
+
+(include-book "defcode"
+              :ttags ((defcode)))
+(include-book "raw")
+(include-book "redefun")
+(include-book "bridge")
+(include-book "subsumption")
+(include-book "table-guard"
+              :ttags ((defcode) (table-guard)))
+
+(include-book "hacking-xdoc")
diff --git a/books/hacking/bridge.acl2 b/books/hacking/bridge.acl2
new file mode 100644
index 0000000..df68a7b
--- /dev/null
+++ b/books/hacking/bridge.acl2
@@ -0,0 +1,3 @@
+(in-package "ACL2")
+(ld "hacker-pkg.lsp")
+(certify-book "bridge" ? t)
diff --git a/books/hacking/bridge.lisp b/books/hacking/bridge.lisp
new file mode 100644
index 0000000..bf6b2b7
--- /dev/null
+++ b/books/hacking/bridge.lisp
@@ -0,0 +1,203 @@
+(in-package "ACL2")
+(include-book "doc-section")
+
+;Needed to use, but not needed for certification:
+;(include-book "defcode" :load-compiled-file :comp :ttags ((defcode)))
+
+(program)
+(set-state-ok t)
+
+
+; return world with last cltl-command global-value replaced with given value
+(defun replace-last-cltl-command-wrld (cltl-command wrld)
+  (declare (xargs :mode :program))
+  (cond ((endp wrld)
+         nil)
+        ((and (consp (car wrld))
+              (eq (caar wrld) 'cltl-command)
+              (consp (cdar wrld))
+              (eq (cadar wrld) 'global-value))
+         (cons
+          (list* 'cltl-command 'global-value cltl-command)
+          (cdr wrld)))
+        (t
+         (cons
+          (car wrld)
+          (replace-last-cltl-command-wrld cltl-command (cdr wrld))))))
+
+(defmacro replace-last-cltl-command (cltl-command)
+  `(progn!=touchable
+    :fns set-w!
+    :loop-only
+     (pprogn
+      (set-w! (replace-last-cltl-command-wrld
+               ,(if (and (consp cltl-command)
+                         (symbolp (car cltl-command))
+                         (member-eq (car cltl-command)
+                                    '(defuns defstobj defpkg defconst defmacro
+                                       memoize unmemoize)))
+                  `',cltl-command ; needs quoting
+                  cltl-command    ; might need evaluation
+                  )
+               (w state))
+              state)
+      (value :invisible))))
+
+
+; return world with last cltl-command global-value removed
+(defun remove-last-cltl-command-wrld (wrld)
+  (declare (xargs :mode :program))
+  (cond ((endp wrld)
+         nil)
+        ((and (consp (car wrld))
+              (eq (caar wrld) 'cltl-command)
+              (consp (cdar wrld))
+              (eq (cadar wrld) 'global-value))
+         (cdr wrld))
+        (t
+         (cons
+          (car wrld)
+          (remove-last-cltl-command-wrld (cdr wrld))))))
+
+(defmacro remove-last-cltl-command ()
+  '(progn!=touchable
+    :fns set-w!
+    :loop-only
+     (pprogn
+      (set-w! (remove-last-cltl-command-wrld (w state)) state)
+      (value :invisible))))
+
+
+; convert (declare (...)) or ((...)) or (...) into (declare (...))
+(defun reconstruct-declare-lst (spec)
+  (cond ((atom spec) nil)
+        ((eq 'declare (car spec))
+         (list spec))
+        ((consp (car spec))
+         (list (cons 'declare spec)))
+        (t
+         (list (list 'declare spec)))))
+
+; for public use
+(defmacro defun-bridge (name
+                        ll
+                        .(&key (logic '() logic-p)
+                               (logic-declare '())
+                               (program '() program-p)
+                               (program-declare '())
+                               (raw '() raw-p)
+                               (raw-declare '())
+                               (doc '())))
+
+;;; This legacy doc string was replaced Nov. 2014 by a corresponding
+;;; auto-generated defxdoc form in file hacking-xdoc.lisp.
+
+; ":Doc-Section hacker
+;
+; define a function with a different low-level definition.~/
+
+; ~bv[]
+; General Form:
+; (defun-bridge ~i[name] (~i[formals])
+;   [:doc ~i[doc-string]]
+;   [:loop-declare ~i[loop-decls]]
+;   :loop ~i[loop-body]
+;   [:raw-declare ~i[raw-decls]]
+;   :raw ~i[raw-body])
+; ~ev[] ~/
+;
+; This is much like executing
+; ~bv[]
+; (defun ~i[name] (~i[formals])
+;   ~i[doc-string]
+;   (declare (xargs :mode :program))
+;   ~i[loop-decls]
+;   ~i[loop-body])
+; ~ev[]
+; in ACL2 and then
+; ~bv[]
+; (defun ~i[name] (~i[formals])
+;   ~i[raw-decls]
+;   ~i[raw-body])
+; ~ev[]
+; in raw Lisp, except that extra checks and bookkeeping make it safer
+; than that.
+;
+; An active ttag is required to use this form (~l[defttag]), because
+; it can easily corrupt ACL2 or render it unsound.
+; ~/"
+  (declare (xargs :guard (and (or (and logic-p program-p (not raw-p))
+                                  (and logic-p (not program-p) raw-p)
+                                  (and (not logic-p) program-p raw-p))
+                              (implies doc
+                                       (stringp doc))))
+           (ignorable program-p))
+  (let*
+    ((ignorable-decl-lst
+      (and ll `((declare (ignorable . ,ll)))))
+     (raw-def-tuple
+      `(,name ,ll
+        ,@ ignorable-decl-lst
+        . ,(if raw-p
+             (append (reconstruct-declare-lst raw-declare)
+                     (list raw))
+             (append (reconstruct-declare-lst program-declare)
+                     (list program)))))
+     (loop-def
+      `(defun ,name
+         ,ll
+         ,@ (and doc (list doc))
+         . ,(if logic-p
+              (append
+               (list '(declare (xargs :mode :logic)))
+               ignorable-decl-lst
+               (reconstruct-declare-lst logic-declare)
+               (list logic))
+              (append
+               (list '(declare (xargs :mode :program)))
+               ignorable-decl-lst
+               (reconstruct-declare-lst program-declare)
+               (list program)))))
+     (code
+      (list loop-def
+            (if raw-p
+              '(remove-last-cltl-command)
+              `(replace-last-cltl-command
+                (defuns ,(if logic-p :logic :program) nil
+                  ,raw-def-tuple))))))
+    `(progn
+      (assert-unbound ,name)
+      ,@ (if logic-p
+           nil
+           `((ensure-program-only-flag ,name)))
+      (ensure-special-raw-definition-flag ,name)
+      (defcode
+        :loop ,code
+        ,@ (and raw-p
+                `(:extend (in-raw-mode (maybe-push-undo-stack 'defun ',name)
+                                       (defun . ,raw-def-tuple)
+                                       (defun-*1* ,name ,ll (,name . ,ll)))
+                  :retract (in-raw-mode (maybe-pop-undo-stack ',name))))
+        :compile ((defun . ,raw-def-tuple)
+                  . ,(and raw-p `((defun-*1* ,name ,ll (,name . ,ll)))))))))
+
+
+
+; tests and stuff:
+
+#|
+(include-book
+ "defcode" :ttags ((defcode)))
+(defttag t)
+(defun-bridge foo (x)
+  :program x
+  :raw (progn (format t "~a~%" x)
+              x))
+
+(foo 42)
+(set-guard-checking :none)
+(foo 42)
+(defmacro bar ()
+  (foo nil))
+(bar)
+|#
diff --git a/books/hacking/copyright b/books/hacking/copyright
new file mode 100644
index 0000000..bec73b2
--- /dev/null
+++ b/books/hacking/copyright
@@ -0,0 +1,20 @@
+This ACL2 hacking code is part of ACL2s: "The ACL2 Sedan"
+By Peter C. Dillinger, Panagiotis Manolios, and Daron Vroon
+
+Copyright 2008 (c)
+Georgia Tech Research Corporation and Northeastern University
+
+The code in this directory is free software; you can redistribute it and/or
+modify it under the terms of the GNU General Public License as published by
+the Free Software Foundation; either version 2 of the License, or (at your
+option) any later version.
+
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+GNU General Public License for more details.
+
+You should have received a copy of the GNU General Public License along
+with this program; if not, write to the Free Software Foundation, Inc.,
+51 Franklin Street, Fifth Floor, Boston, MA 02110-1301, USA.
+
diff --git a/books/hacking/defcode.acl2 b/books/hacking/defcode.acl2
new file mode 100644
index 0000000..1dc4126
--- /dev/null
+++ b/books/hacking/defcode.acl2
@@ -0,0 +1,3 @@
+(ld "hacker-pkg.lsp")
+; cert-flags: ? t :ttags ((defcode))
+(certify-book "defcode" ? t :ttags ((defcode)))
diff --git a/books/hacking/defcode.lisp b/books/hacking/defcode.lisp
new file mode 100644
index 0000000..5195aef
--- /dev/null
+++ b/books/hacking/defcode.lisp
@@ -0,0 +1,240 @@
+(in-package "ACL2")
+
+; Modification by Matt K. after v4-3: Removed :load-compiled-file :comp, which
+; was part of both include-book forms in this file, in support of provisional
+; certification.  Presumably the indicate books have already been compiled by
+; now, anyhow.
+
+(include-book "hacker") ;was in portcullis
+
+(program)
+(set-state-ok t)
+
+
+; auxiliary stuff:
+
+; check if something is a list of function applications
+(defun acl2-hacker::defcode-code-listp (l)
+  (or (null l)
+      (and (consp l)
+           (consp (car l))
+           (not (eq 'lambda (caar l))))))
+
+; coerce something to be a LIST of function applications
+(defun acl2-hacker::defcode-ensure-code-list (c)
+  (if (acl2-hacker::defcode-code-listp c)
+    c
+    (list c)))
+
+
+; ***********************************
+; beginning of actual dangerous stuff
+(defttag defcode)
+
+(include-book "progn-bang-enh" :ttags ((defcode)))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; defcode-fn
+;
+; this is the event code for defcode, that executes any :loop code and
+; puts any :extend or :retract code into the world.
+;
+
+(progn+touchable :fns install-event
+  (defun defcode-fn (loop extend retract state event-form)
+    (let* ((loop-lst (acl2-hacker::defcode-ensure-code-list loop))
+           (extend-lst (acl2-hacker::defcode-ensure-code-list extend))
+           (retract-lst (acl2-hacker::defcode-ensure-code-list retract)))
+      (er-progn
+       (if loop-lst
+         (progn!-fn loop-lst nil state)
+         (value nil))
+       (if (or extend-lst retract-lst)
+         (let* ((event-form (or event-form
+                                `(defcode :loop ,loop-lst
+                                          :extend ,extend-lst
+                                          :retract ,retract-lst)))
+                (wrld (w state))
+                (wrld (if extend-lst
+                        (putprop 'extend-progn! 'global-value extend-lst wrld)
+                        wrld))
+                (wrld (if retract-lst
+                        (putprop 'retract-progn! 'global-value retract-lst wrld)
+                        wrld)))
+           (install-event ':invisible
+                          event-form
+                          'defcode
+                          0
+                          nil
+                          nil
+                          nil
+                          'defcode
+                          wrld
+                          state))
+         (value nil))))))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; executing code on world changes
+;
+; these are made as permanent changes so that the rest of defcode can be
+; resurrected if an old world is reinstalled.
+;
+
+; execute code in (extend-progn! global-value #) triples on world extension
+(modify-raw-defun-permanent
+ add-trip pre-defcode-add-trip
+ (world-name world-key trip)
+ (progn
+  (pre-defcode-add-trip world-name world-key trip)
+  (when (and (eq (car trip) 'extend-progn!)
+             (eq (cadr trip) 'global-value))
+        (mv-let (erp val state)
+                (state-global-let*
+                 ((inhibit-output-lst
+                   (union-eq (@ inhibit-output-lst)
+                             (remove 'error *valid-output-names*))))
+                 (progn!-fn (cddr trip) nil *the-live-state*))
+                (declare (ignore val state))
+                (when erp
+                      (hard-error 'defcode
+                                  "Error returned."
+                                  nil))))))
+
+; execute code in (retract-progn! global-value #) triples on world retraction
+(modify-raw-defun-permanent
+ undo-trip pre-defcode-undo-trip
+ (world-name world-key trip)
+ (progn
+  (pre-defcode-undo-trip world-name world-key trip)
+  (when (and (eq (car trip) 'retract-progn!)
+             (eq (cadr trip) 'global-value))
+        (mv-let (erp val state)
+                (state-global-let*
+                 ((inhibit-output-lst
+                   (union-eq (@ inhibit-output-lst)
+                             (remove 'error *valid-output-names*))))
+                 (progn!-fn (cddr trip) nil *the-live-state*))
+                (declare (ignore val state))
+                (when erp
+                      (hard-error 'defcode
+                                  "Error returned."
+                                  nil))))))
+
+; for detecting reentry into set-w
+(in-raw-mode
+ (defvar *set-w-reentry-protect* nil))
+
+; enforce non-reentry of set-w
+(modify-raw-defun-permanent
+ set-w pre-defcode-set-w (flag wrld state)
+ (declare (special *set-w-reentry-protect*))
+ (if *set-w-reentry-protect*
+   (hard-error 'defcode
+               "Attempt to change world within DEFCODE code."
+               nil)
+   (let ((*set-w-reentry-protect* t))
+     (pre-defcode-set-w flag wrld state))))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; defcode macro
+
+(defmacro defcode (&whole event-form &key loop extend retract compile)
+  (let ((loop-code-lst
+         `((defcode-fn
+             ',loop
+             ',extend
+             ',retract
+             state
+             ',event-form)))
+        (compile-code-lst
+         (cond ((atom compile)
+                nil)
+               ((and (consp compile)
+                     (consp (car compile))
+                     (not (eq 'lambda (caar compile))))
+                compile)
+               (t
+                (list compile)))))
+    (if compile-code-lst
+      `(progn!
+        (progn! :loop-only .,loop-code-lst)
+        (progn! :compile-only .,compile-code-lst))
+      `(progn! :loop-only .,loop-code-lst))))
+
+; this copy helpful in case of world resurrection
+(defcode
+ :extend
+ (in-raw-mode
+  (defmacro progn! (&rest r)
+    (let ((sym (gensym)))
+      `(let ((state *the-live-state*)
+             (,sym (f-get-global 'acl2-raw-mode-p *the-live-state*)))
+         (declare (ignorable state))
+         ,@(cond ((not (consp r))
+                  (list nil))
+                 ((eq (car r) :loop-only)
+                  (list nil))
+                 ((eq (car r) :compile-only)
+                  (cdr r))
+                 ((eq (car r) :state-global-bindings)
+                  (cddr r))
+                 (t r))
+         (f-put-global 'acl2-raw-mode-p ,sym state)
+         (value nil))))))
+
+; **********************
+; end of dangerous stuff
+(defttag nil)
+
+; end of required defcode stuff
+
+
+; tests & stuff:
+
+#|
+(defttag defcode)
+
+;(defcode :extend (defun foo (x) (1+ x))) ; should fail
+
+(defcode :extend (cw "==> Hi!~%")
+         :retract (cw "==> Bye!~%")
+         :compile (format t "==> Yo!~%"))
+(u)
+
+(defttag nil)
+(progn (defttag t)
+       (defcode :extend  (in-raw-mode (format t "==> Hi!~%"))
+                :retract (in-raw-mode (format t "==> Bye!~%")))
+       (defttag nil))
+(u)
+
+;(defcode :extend  (in-raw-mode (format t "==> Hi!~%")))
+; should fail without a trust tag
+
+(mini-proveall)
+;|#
+
+
+; misc:
+
+; this was just a convenient place to put this, considering it depends
+; on defcode.
+
+; assert that a name is not bound in ACL2, nor as a raw lisp function, macro
+; or variable.
+(defmacro assert-unbound (&rest names)
+  `(defcode
+    :loop
+    (in-raw-mode
+     (dolist (name ',names)
+             (when (and (not (f-get-global 'ld-redefinition-action *the-live-state*))
+                        (or (getprop name 'absolute-event-number nil
+                                     'current-acl2-world (w *the-live-state*))
+                            (boundp name)
+                            (fboundp name)
+                            (macro-function name)))
+                   (hard-error 'assert-unbound
+                               "Already has an ACL2 or raw Lisp definition: ~x0~%"
+                               (list (cons #\0 name))))))))
diff --git a/books/hacking/defstruct-parsing.acl2 b/books/hacking/defstruct-parsing.acl2
new file mode 100644
index 0000000..3b7a199
--- /dev/null
+++ b/books/hacking/defstruct-parsing.acl2
@@ -0,0 +1,3 @@
+(in-package "ACL2")
+(ld "hacker-pkg.lsp")
+(certify-book "defstruct-parsing" ? t)
diff --git a/books/hacking/defstruct-parsing.lisp b/books/hacking/defstruct-parsing.lisp
new file mode 100644
index 0000000..e6d05d4
--- /dev/null
+++ b/books/hacking/defstruct-parsing.lisp
@@ -0,0 +1,188 @@
+(in-package "ACL2-HACKER")
+
+(program)
+(set-state-ok t)
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; defstruct parsing
+;
+
+(defun defstruct-conc-name (name options)
+  (cond ((endp options)
+         (string-append (symbol-name name) "-"))
+        ((eq ':conc-name (car options))
+         "")
+        ((and (consp (car options))
+              (eq ':conc-name (caar options)))
+         (let ((arglst (cdar options)))
+           (if (and (consp arglst)
+                    (symbolp (car arglst))
+                    (car arglst))
+             (symbol-name (car arglst))
+             "")))
+        (t
+         (defstruct-conc-name name (cdr options)))))
+
+
+(defun defstruct-constructor-name-lst1 (name options sofar nilseen)
+  (cond ((endp options)
+         (cond (sofar
+                sofar)
+               (nilseen
+                nil)
+               (t
+                (list (intern-in-package-of-symbol
+                       (string-append "MAKE-" (symbol-name name))
+                       name)))))
+        ((and (consp (car options))
+              (eq ':constructor (caar options))
+              (consp (cdar options)))
+         (cond ((null (cadar options))
+                (defstruct-constructor-name-lst1 name
+                                                 (cdr options)
+                                                 sofar
+                                                 t))
+               ((symbolp (cadar options))
+                (defstruct-constructor-name-lst1 name
+                                                 (cdr options)
+                                                 (cons (cadar options) sofar)
+                                                 nilseen))
+               (t ; bad
+                (defstruct-constructor-name-lst1 name
+                                                 (cdr options)
+                                                 sofar
+                                                 nilseen))))
+        (t
+         (defstruct-constructor-name-lst1 name (cdr options) sofar nilseen))))
+
+(defun defstruct-constructor-name-lst (name options)
+  (defstruct-constructor-name-lst1 name options nil nil))
+
+
+(defun defstruct-copier-name-lst1 (name options sofar nilseen)
+  (cond ((endp options)
+         (cond (sofar
+                sofar)
+               (nilseen
+                nil)
+               (t
+                (list (intern-in-package-of-symbol
+                       (string-append "COPY-" (symbol-name name))
+                       name)))))
+        ((and (consp (car options))
+              (eq ':copier (caar options))
+              (consp (cdar options)))
+         (cond ((null (cadar options))
+                (defstruct-copier-name-lst1 name
+                                               (cdr options)
+                                               sofar
+                                               t))
+               ((symbolp (cadar options))
+                (defstruct-copier-name-lst1 name
+                                               (cdr options)
+                                               (cons (cadar options) sofar)
+                                               nilseen))
+               (t ; bad
+                (defstruct-copier-name-lst1 name
+                                               (cdr options)
+                                               sofar
+                                               nilseen))))
+        (t
+         (defstruct-copier-name-lst1 name (cdr options) sofar nilseen))))
+
+(defun defstruct-copier-name-lst (name options)
+  (defstruct-copier-name-lst1 name options nil nil))
+
+
+; :include ignored!
+; :initial-offset unimportant
+; :named unimportant
+
+
+(defun defstruct-predicate-name-lst1 (name options sofar nilseen)
+  (cond ((endp options)
+         (cond (sofar
+                sofar)
+               (nilseen
+                nil)
+               (t
+                (list (intern-in-package-of-symbol
+                       (string-append (symbol-name name) "-P")
+                       name)))))
+        ((and (consp (car options))
+              (eq ':predicate (caar options))
+              (consp (cdar options)))
+         (cond ((null (cadar options))
+                (defstruct-predicate-name-lst1 name
+                                               (cdr options)
+                                               sofar
+                                               t))
+               ((symbolp (cadar options))
+                (defstruct-predicate-name-lst1 name
+                                               (cdr options)
+                                               (cons (cadar options) sofar)
+                                               nilseen))
+               (t ; bad
+                (defstruct-predicate-name-lst1 name
+                                               (cdr options)
+                                               sofar
+                                               nilseen))))
+        (t
+         (defstruct-predicate-name-lst1 name (cdr options) sofar nilseen))))
+
+(defun defstruct-predicate-name-lst (name options)
+  (defstruct-predicate-name-lst1 name options nil nil))
+
+
+; :print-function, :print-object unimportant
+; :type assumed unimportant
+
+
+(defun defstruct-accessors (conc-name descs package-of-symbol)
+  (if (endp descs)
+    nil
+    (let* ((desc (car descs))
+           (name (if (consp desc) (car desc) desc)))
+      (if (symbolp name)
+        (cons (if (equal conc-name "")
+                name
+                (intern-in-package-of-symbol
+                 (string-append conc-name (symbol-name name))
+                 package-of-symbol))
+              (defstruct-accessors conc-name (cdr descs) package-of-symbol))
+        ;; bad:
+        (defstruct-accessors conc-name (cdr descs) package-of-symbol)))))
+
+
+(defun defstruct-name-and-fns (form)
+  (if (not (and (consp form)
+                (eq (car form) 'defstruct)
+                (consp (cdr form))
+                (or (symbolp (cadr form))
+                    (and (consp (cadr form))
+                         (symbolp (caadr form))))))
+    nil
+    (let* ((name-and-options (cadr form))
+           (name (if (consp name-and-options)
+                   (car name-and-options)
+                   name-and-options))
+           (options (if (consp name-and-options)
+                      (cdr name-and-options)
+                      nil))
+           (slot-descs (if (and (consp (cddr form))
+                                (stringp (caddr form)))
+                         (cdddr form)
+                         (cddr form)))
+           (conc-name (defstruct-conc-name name options))
+           (top-fns (append (defstruct-constructor-name-lst name options)
+                            (defstruct-copier-name-lst name options)
+                            (defstruct-predicate-name-lst name options)))
+           (accessors (defstruct-accessors conc-name slot-descs name)))
+      (cons name (append top-fns accessors)))))
+
+
+;
+; end of defstruct parsing
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
diff --git a/books/hacking/doc-section.lisp b/books/hacking/doc-section.lisp
new file mode 100644
index 0000000..8915672
--- /dev/null
+++ b/books/hacking/doc-section.lisp
@@ -0,0 +1,14 @@
+(in-package "ACL2")
+
+;;; This legacy doc string was replaced Nov. 2014 by a corresponding
+;;; auto-generated defxdoc form in file hacking-xdoc.lisp.
+;(defdoc hacker
+; ":Doc-Section hacker
+
+; functions for extending ACL2 in ways that are potentially unsound.~/
+
+; The ~c[books/hacking] library.
+
+; These functions typically require an active ttag (~l[defttag]) to work.~/
+; ~/"
+;  )
diff --git a/books/hacking/dynamic-make-event-test.acl2 b/books/hacking/dynamic-make-event-test.acl2
new file mode 100644
index 0000000..b9c2780
--- /dev/null
+++ b/books/hacking/dynamic-make-event-test.acl2
@@ -0,0 +1,10 @@
+(in-package "ACL2")
+(ld "hacker-pkg.lsp")
+
+; We need the following for provisional certification, so that ACL2 can read
+; symbols rewrite-code::SYM in dynamic-make-event.acl2x at the start of the
+; Pcertify step.
+(include-book "rewrite-code")
+
+; cert-flags: ? t :ttags ((defcode) (dynamic-make-event-test))
+(certify-book "dynamic-make-event-test" ? t :ttags ((defcode) (dynamic-make-event-test)))
diff --git a/books/hacking/dynamic-make-event-test.lisp b/books/hacking/dynamic-make-event-test.lisp
new file mode 100644
index 0000000..11b7b04
--- /dev/null
+++ b/books/hacking/dynamic-make-event-test.lisp
@@ -0,0 +1,53 @@
+(in-package "ACL2")
+
+; Modification by Matt K. after v4-3: Removed :load-compiled-file :comp, which
+; was part of all four include-book forms just below, in support of provisional
+; certification.  Presumably the indicate books have already been compiled by
+; now, anyhow.
+
+(include-book "defcode" :ttags ((defcode)))
+(include-book "rewrite-code")
+(include-book "redefun")
+(include-book "dynamic-make-event")
+
+#|
+
+dynamic-make-event-test.lisp
+----------------------------
+
+By Peter Dillinger, ca. 2009
+
+This is a regression test for the dynamic-make-event book.
+
+|#
+
+(program)
+(set-state-ok t)
+
+
+(defttag dynamic-make-event-test) ; need to do some evil stuff
+
+; Tweak defun so that if we try to defun THE-MAGIC-NAME, then it
+; will instead expand to a definition of SOME-OTHER-NAME
+(progn+touchable
+ :all
+ (redefun+rewrite
+  defuns-fn
+  (:carpat %body%
+   :repl (if (eq (caar def-lst) 'the-magic-name)
+           (dynamic-make-event-fn '(defun some-other-name (x) (1+ x))
+				  event-form
+				  state)
+	   %body%)
+   :vars (%body%))))
+
+(defttag nil) ; end of evil stuff
+
+; Now try it out ...
+
+(defun the-magic-name (x) (1- x))
+; should become (defun some-other-name (x) (1+ x))
+
+; now we use some-other-name, to be sure it's now defined
+(defun testing-function (x) (some-other-name x))
+
diff --git a/books/hacking/dynamic-make-event.acl2 b/books/hacking/dynamic-make-event.acl2
new file mode 100644
index 0000000..4b73be6
--- /dev/null
+++ b/books/hacking/dynamic-make-event.acl2
@@ -0,0 +1,9 @@
+(in-package "ACL2")
+(ld "hacker-pkg.lsp")
+
+; We need the following for provisional certification, so that ACL2 can read
+; symbols rewrite-code::SYM in dynamic-make-event.acl2x at the start of the
+; Pcertify step.
+(include-book "rewrite-code")
+
+(certify-book "dynamic-make-event" ? t)
diff --git a/books/hacking/dynamic-make-event.lisp b/books/hacking/dynamic-make-event.lisp
new file mode 100644
index 0000000..4927693
--- /dev/null
+++ b/books/hacking/dynamic-make-event.lisp
@@ -0,0 +1,55 @@
+(in-package "ACL2")
+
+#|
+
+dynamic-make-event.lisp
+-----------------------
+
+By Peter Dillinger, ca. 2006-2009
+
+If you modify the code for an event (such as defun) to call
+DYNAMIC-MAKE-EVENT-FN, then that event can have a make-event expansion,
+just as a MAKE-EVENT would, meaning that at include-book time, the
+expansion is the only part that is seen.
+
+This functionality used to require a hack, but in latest ACL2 versions,
+it does not.
+
+The code here is trivial, but we want this functionality to remain in
+ACL2, so it should be in the regression suite.  See
+dynamic-make-event-test.lisp
+
+|#
+
+(program)
+(set-state-ok t)
+
+
+
+; body is the new form to replace this one
+; event-form is the original (if available?)
+(defun dynamic-make-event-fn (body event-form state)
+  (make-event-fn `',body
+                 nil
+                 nil
+                 nil
+                 event-form
+                 state))
+
+
+#| used to be needed for events other than MAKE-EVENT to have expansion:
+(progn+touchable
+ :all
+ (redefun+rewrite
+  make-event-fn
+  (:pat (mv-let (wrappers base)
+                %1%
+                (cond ((member-eq (car base) %2%)  %stuff%)
+                      . %3%))
+   :repl (mv-let (wrappers base)
+                 %1%
+                 (declare (ignorable base))
+                 %stuff%)
+   :vars (%1% %2% %3% %stuff%)
+   :mult 1)))
+|#
diff --git a/books/hacking/evalable-ld-printing.acl2 b/books/hacking/evalable-ld-printing.acl2
new file mode 100644
index 0000000..e83b61a
--- /dev/null
+++ b/books/hacking/evalable-ld-printing.acl2
@@ -0,0 +1,3 @@
+(in-package "ACL2")
+; cert-flags: ? t :ttags (:evalable-ld-printing)
+(certify-book "evalable-ld-printing" ? t :ttags (:evalable-ld-printing))
diff --git a/books/hacking/evalable-ld-printing.lisp b/books/hacking/evalable-ld-printing.lisp
new file mode 100644
index 0000000..6eabd43
--- /dev/null
+++ b/books/hacking/evalable-ld-printing.lisp
@@ -0,0 +1,78 @@
+; evalable-ld-printing.lisp - Print LD results in "evalable" way, as provided
+; by "evalable-printing" book.
+;
+; To activate, include this book and assign a non-nil value to the state
+; global EVALABLE-LD-PRINTINGP, as in
+;   (assign evalable-ld-printingp t)
+;
+; If ld-post-eval-print is :command-conventions, we do not make error
+; triple output evalable.  To make error triple output looks especially
+; unique, I recommend making it look like a comment:
+;   (assign triple-print-prefix "; ")
+;
+; Requires a trust tag :evalable-ld-printing
+;
+; Peter C. Dillinger, Northeastern University, 2008
+
+(in-package "ACL2")
+
+(program)
+(set-state-ok t)
+
+(defun evalable-ld-printingp (state)
+  (and (f-boundp-global 'evalable-ld-printingp state)
+       (f-get-global 'evalable-ld-printingp state)))
+
+(include-book "misc/evalable-printing" :dir :system)
+
+
+(defttag :evalable-ld-printing)
+
+(include-book "hacker")
+(progn+all-ttags-allowed
+ (include-book "defcode" :ttags ((defcode)))
+ (include-book "subsumption")
+ (include-book "raw")
+ )
+(subsume-ttags-since-defttag)
+
+(modify-raw-defun acl2::ld-print-results original-ld-print-results (trans-ans state)
+  (if (or (not (acl2::live-state-p state))
+          (acl2::output-in-infixp state)
+          (not (evalable-ld-printingp state)))
+    (original-ld-print-results trans-ans state)
+    (let* ((output-channel (standard-co state))
+           (flg (ld-post-eval-print state))
+           (stobjs-out (car trans-ans))
+           (valx (cdr trans-ans)))
+      #-(or gcl cmu sbcl lispworks)
+      (when (acl2::raw-mode-p state)
+            (acl2::format (acl2::get-output-stream-from-channel output-channel) "~&"))
+      (cond
+       ((null flg) state)
+       ((and (eq flg :command-conventions)
+             (equal (length stobjs-out) 3)
+             (eq (car stobjs-out) nil)
+             (eq (caddr stobjs-out) 'state))
+        (cond
+         ((eq (cadr valx) :invisible)
+          state)
+         (t
+          (pprogn
+           (acl2::princ$ (if (stringp (f-get-global 'acl2::triple-print-prefix state))
+                     (f-get-global 'acl2::triple-print-prefix state)
+                     "")
+                   output-channel state)
+           (let ((col (if (stringp (f-get-global 'acl2::triple-print-prefix state))
+                        (length (f-get-global 'acl2::triple-print-prefix state))
+                        0)))
+             (acl2::ppr (cadr valx) col output-channel state nil))
+           (acl2::newline output-channel state)))))
+     ((equal (length stobjs-out) 1)
+      (pprogn
+       (acl2::ppr (car (make-evalable-with-stobjs (list valx) stobjs-out)) 0 output-channel state nil)
+       (acl2::newline output-channel state)))
+     (t
+      (pprogn
+       (acl2::ppr (cons 'mv (make-evalable-with-stobjs valx stobjs-out)) 0 output-channel state nil)
+       (acl2::newline output-channel state)))))))
diff --git a/books/hacking/hacker-pkg.lsp b/books/hacking/hacker-pkg.lsp
new file mode 100644
index 0000000..9efd35e
--- /dev/null
+++ b/books/hacking/hacker-pkg.lsp
@@ -0,0 +1,57 @@
+(defpkg "ACL2-HACKER"
+ (append
+  '(; things we want from ACL2 package that aren't in *acl2-exports*:
+    value set-w! assert-event msg
+    ld-evisc-tuple connected-book-directory guard-checking-on
+    inhibit-output-lst print-clause-ids acl2-raw-mode-p 
+    raw-mode-restore-lst saved-output-token-lst tainted-okp
+    in-package-fn defpkg-fn pe! trans! pso pso! value-triple
+    default-evisc-tuple ttag hard soft
+
+    progn! untouchable-fns untouchable-vars ld-redefinition-action
+    set-ld-skip-proofsp set-ld-redefinition-action set-ld-prompt
+    set-ld-keyword-aliases set-ld-pre-eval-filter set-ld-error-triples
+    set-ld-error-action set-ld-query-control-alist set-cbd-fn
+    set-raw-mode set-raw-mode-fn set-tainted-okp
+    push-untouchable-fn remove-untouchable-fn
+    set-raw-mode-on set-raw-mode-off temp-touchable-vars temp-touchable-fns
+    set-temp-touchable-vars set-temp-touchable-fns
+    built-in-program-mode-fns program-fns-with-raw-code
+    
+    global-value current-acl2-world ld-level *wormholep* raw-mode-p
+    max-absolute-event-number getprop er-let* *valid-output-names*
+    state-global-let* extension absolute-to-relative-command-number
+    access-command-tuple-number global-set-lst command-number-baseline
+    event-number-baseline next-absolute-command-number add-command-landmark
+    next-absolute-event-number add-event-landmark scan-to-command
+    certify-book-fn f-get-global f-put-global f-boundp-global
+    checkpoint-processors global-val acl2-version earlier-acl2-versionp)
+    
+  '(; defined here and "exported" to ACL2 package:
+    progn!-with-bindings
+    hacker ; documentation topic
+    progn+touchable
+    progn=touchable
+    progn!+touchable
+    progn!=touchable
+    with-touchable ; alias
+    progn+redef
+    with-redef-allowed ; alias
+    in-raw-mode
+    with-raw-mode ; alias
+    assert-program-mode
+    ensure-program-only-flag
+    ensure-program-only
+    has-special-raw-definition ; state global
+    ensure-special-raw-definition-flag
+    assert-no-special-raw-definition
+    reconstruct-declare-lst
+    modify-raw-defun-permanent
+    progn+all-ttags-allowed
+    deflabels
+    ttag-skip-proofs
+    progn+ttag-skip-proofs
+    )
+   (union-eq *acl2-exports*
+             *common-lisp-symbols-from-main-lisp-package*)))
+
diff --git a/books/hacking/hacker.acl2 b/books/hacking/hacker.acl2
new file mode 100644
index 0000000..297075e
--- /dev/null
+++ b/books/hacking/hacker.acl2
@@ -0,0 +1,3 @@
+(in-package "ACL2")
+(ld "hacker-pkg.lsp")
+(certify-book "hacker" ? t)
diff --git a/books/hacking/hacker.lisp b/books/hacking/hacker.lisp
new file mode 100644
index 0000000..f7d92fc
--- /dev/null
+++ b/books/hacking/hacker.lisp
@@ -0,0 +1,1116 @@
+(in-package "ACL2-HACKER")
+(include-book "doc-section")
+;; hacker.lisp
+;;
+;; Functions for extending ACL2 in ways that are potentially unsound
+;;
+;; By Peter C. Dillinger with contributions by Matt Kaufmann
+
+
+(program)
+(set-state-ok t)
+
+;=========== some auxiliary definitions ===========
+
+; the special progn! support for doing state-global bindings was changed between
+; 3.2 and 3.2.1.  We define progn!-with-bindings to use the right one.
+(make-event
+ (if (earlier-acl2-versionp "ACL2 Version 3.2" (@ acl2-version)) ; >= 3.2.1
+   (value
+    '(defmacro progn!-with-bindings (acl2::bindings &rest acl2::rst)
+       `(progn! :state-global-bindings ,acl2::bindings . ,acl2::rst)))
+   (value
+    '(defmacro progn!-with-bindings (acl2::bindings &rest acl2::rst)
+       `(progn! (state-global-let* ,acl2::bindings (progn! . ,acl2::rst)))))))
+
+; read a state global or return a default value (defaulting to nil) if unbound
+(defmacro @opt (var &optional deflt)
+  `(if (boundp-global ',var state)
+     (f-get-global ',var state)
+     ,deflt))
+
+; like common lisp WHEN, but uses ACL2 error triples
+(defmacro er-when (test form &rest more-forms)
+  `(if ,test
+     (er-progn ,form . ,more-forms)
+     (value :invisible)))
+
+#|
+; to enable definition of macros that use keyword arguments at the beginning
+(defun transpose-keyword-args1 (args-rest kargs-sofar)
+  (if (and (consp args-rest)
+           (keywordp (car args-rest))
+           (consp (cdr args-rest)))
+    (transpose-keyword-args1 (cddr args-rest)
+                            (list* (car args-rest)
+                                   (cadr args-rest)
+                                   kargs-sofar))
+    (cons args-rest kargs-sofar)))
+
+(defun transpose-keyword-args (args)
+  (transpose-keyword-args1 args nil))
+|#
+
+
+
+;=========== begin touchable stuff ===========
+
+; union in the specification language of temp-untouchable-{vars,fns}
+(defun union-eq-with-top (a b)
+  (if (or (eq a t) (eq b t))
+    t
+    (union-eq a b)))
+
+; used for temp-touchable specifications
+(defun add-temp-touchable-aliases (spec sofar fn-p)
+  (declare (xargs :guard (booleanp fn-p)))
+  (if (null spec)
+    sofar
+    (let ((sym (if (consp spec) (car spec) spec))
+          (rest (if (consp spec) (cdr spec) nil)))
+      (add-temp-touchable-aliases
+       rest
+       (union-eq-with-top
+        (cond ((eq sym :all)
+               t)
+              ((eq sym :initial)
+               (if fn-p
+                 acl2::*initial-untouchable-fns*
+                 acl2::*initial-untouchable-vars*))
+              (t
+               (list sym)))
+        sofar)
+       fn-p))))
+
+#|; flawed in terms of undoing
+
+; defines a stack of saved untouchables
+(defun push-temp-touchables (state)
+  (f-put-global 'saved-temp-touchables
+                (cons (cons (@ temp-touchable-vars)
+                            (@ temp-touchable-fns))
+                      (@opt saved-temp-touchables))
+                state))
+
+(defun pop-temp-touchables (state)
+  (if (and (boundp-global 'saved-temp-touchables state)
+           (consp (@ saved-temp-touchables)))
+    (let ((result (car (@ saved-temp-touchables))))
+      (pprogn (f-put-global 'saved-temp-touchables
+                            (cdr (@ saved-temp-touchables))
+                            state)
+              (value result)))
+    (er soft 'pop-temp-touchables
+        "Stack of temp-touchables is empty.")))
+
+(push-untouchable saved-temp-touchables nil)
+
+;for export
+(defmacro push+touchable (&key vars fns)
+
+;;; This legacy doc string was replaced Nov. 2014 by a corresponding
+;;; auto-generated defxdoc form in file hacking-xdoc.lisp.
+
+; ":Doc-Section hacker
+;
+; add some fns/vars to those temporarily touchable, remembering previous setting.~/
+
+; ~bv[]
+; Examples:
+; (push+touchable :fns :all :vars :all)  ; like push-all-touchable
+; (push+touchable :fns set-w :vars :initial)
+; (push+touchable :vars (foo :initial bar))
+; ~ev[] ~/
+;
+; This event first pushes the previous temporary touchable settings
+; (functions and variables) onto a stack (stored in a global variable)
+; and then adds all those that meet the specification passed in.
+;
+; ~ilc[pop-touchable] reinstates the previous setting.
+;
+; An active ttag is required to use this form (~l[defttag]) because it
+; can render ACL2 unsound (~l[remove-untouchable]).
+; ~/"
+  `(progn! (push-temp-touchables state)
+           (set-temp-touchable-vars
+            (add-temp-touchable-aliases ',vars (@ temp-touchable-vars) nil)
+            state)
+           (set-temp-touchable-fns
+            (add-temp-touchable-aliases ',fns (@ temp-touchable-fns) t)
+            state)))
+
+;for export
+(defmacro push=touchable (&key vars fns)
+
+;;; This legacy doc string was replaced Nov. 2014 by a corresponding
+;;; auto-generated defxdoc form in file hacking-xdoc.lisp.
+
+; ":Doc-Section hacker
+;
+; set which fns/vars are temporarily touchable, remembering previous setting.~/
+
+; ~bv[]
+; Examples:
+; (push=touchable :fns :all :vars :all)  ; like push-all-touchable
+; (push=touchable :fns set-w :vars :initial)
+; (push=touchable :vars (foo :initial bar)) ;``:fns ()'' default
+; ~ev[] ~/
+;
+; This event first pushes the previous temporary touchable settings
+; (functions and variables) onto a stack (stored in a global variable)
+; and then sets them to the specification passed in.
+;
+; ~ilc[pop-touchable] reinstates the previous setting.
+;
+; An active ttag is required to use this form (~l[defttag]) because it
+; can render ACL2 unsound (~l[remove-untouchable]).
+; ~/"
+  `(progn! (push-temp-touchables state)
+           (set-temp-touchable-vars
+            (add-temp-touchable-aliases ',vars nil nil)
+            state)
+           (set-temp-touchable-fns
+            (add-temp-touchable-aliases ',fns nil t)
+            state)))
+
+;for export
+(defmacro push-all-touchable ()
+
+;;; This legacy doc string was replaced Nov. 2014 by a corresponding
+;;; auto-generated defxdoc form in file hacking-xdoc.lisp.
+
+; ":Doc-Section hacker
+;
+; make all fns/vars temporarily touchable, remembering previous setting.~/
+
+; ~bv[]
+; Usage:
+; (push-all-touchable)
+; ~ev[] ~/
+;
+; This event first pushes the previous temporary touchable settings
+; (functions and variables) onto a stack (stored in a global variable)
+; and then sets them to make everything temporarily touchable.
+;
+; ~ilc[pop-touchable] reinstates the previous setting.  ~ilc[push+touchable]
+; and ~ilc[push=touchable] allow more more specification of what should be
+; permitted.
+;
+; An active ttag is required to use this form (~l[defttag]) because it
+; can render ACL2 unsound (~l[remove-untouchable]).
+; ~/"
+  `(progn! (push-temp-touchables state)
+           (set-temp-touchable-vars t state)
+           (set-temp-touchable-fns t state)))
+
+;for export
+(defmacro pop-touchable ()
+
+;;; This legacy doc string was replaced Nov. 2014 by a corresponding
+;;; auto-generated defxdoc form in file hacking-xdoc.lisp.
+
+; ":Doc-Section hacker
+;
+; revert the effect of a push+touchable, push=touchable, or push-all-touchable.~/
+
+; ~bv[]
+; Usage:
+; (pop-touchable)
+; ~ev[] ~/
+;
+; This event pops of the stack of saved temporary touchable settings,
+; reverting the effect of a ~ilc[push+touchable], ~ilc[push=touchable], or
+; ~ilc[push-all-touchable].
+;
+; An active ttag is required to use this form (~l[defttag]) because it
+; can render ACL2 unsound (~l[remove-untouchable]).
+; ~/"
+  `(progn! (er-let*
+        ((to-restore (pop-temp-touchables state)))
+        (pprogn (set-temp-touchable-vars (car to-restore) state)
+            (set-temp-touchable-fns  (cdr to-restore) state)
+            (value ':invisible)))))
+;|#
+
+
+
+;helper for progn+touchable and progn=touchable
+(defun compute-progn-touchable-keyword1 (bangp addp vars fns form-lst)
+  (cond
+   ((and (not vars)
+         (consp form-lst)
+         (eq :vars (car form-lst))
+         (consp (cdr form-lst)))
+    (compute-progn-touchable-keyword1 bangp addp (cadr form-lst) fns (cddr form-lst)))
+   ((and (not fns)
+         (consp form-lst)
+         (eq :fns (car form-lst))
+         (consp (cdr form-lst)))
+    (compute-progn-touchable-keyword1 bangp addp vars (cadr form-lst) (cddr form-lst)))
+   (t
+    `(progn!-with-bindings
+      ((temp-touchable-vars
+        (add-temp-touchable-aliases ',vars
+                                    ,(if addp
+                                       '(@ temp-touchable-vars)
+                                       'nil)
+                                    nil)
+        set-temp-touchable-vars)
+       (temp-touchable-fns
+        (add-temp-touchable-aliases ',fns
+                                    ,(if addp
+                                       '(@ temp-touchable-fns)
+                                       'nil)
+                                    't)
+        set-temp-touchable-fns))
+      ,(if bangp
+         `(progn! . ,form-lst)
+         `(progn . ,form-lst))))))
+
+(defun compute-progn-touchable-keyword (bangp addp form-lst)
+  (compute-progn-touchable-keyword1 bangp addp nil nil form-lst))
+
+
+;for export
+(defmacro progn+touchable (&rest args)
+
+;;; This legacy doc string was replaced Nov. 2014 by a corresponding
+;;; auto-generated defxdoc form in file hacking-xdoc.lisp.
+
+; ":Doc-Section hacker
+;
+; execute some events with some additional fns and/or vars made temporarily touchable.~/
+
+; ~bv[]
+; Examples:
+; (progn+touchable :all ; same as :fns :all :vars :all
+;   (defun foo ...)
+;   (defun bar ...))
+; (progn+touchable :vars (current-package ld-skip-proofsp)
+;   ...)
+; (progn+touchable :fns :all
+;   ...)
+; (progn+touchable :fns set-w :vars :all
+;   ...)
+; ~ev[] ~/
+
+; This is like ~ilc[progn] except that it surrounds the events with code to
+; add certain fns and/or vars to those that are temporarily touchable.
+;
+; Related to ~ilc[progn=touchable].
+;
+; An active ttag is required to use this form (~l[defttag]) because it
+; can render ACL2 unsound (~l[remove-untouchable]).
+;
+; Note that the syntax for this macro is not quite like traditional
+; keyword arguments, which would come at the end of the argument list.
+; ~/"
+  (declare (xargs :guard (and (consp args)
+                              (keywordp (car args)))))
+  (if (not (member-eq (car args) '(:vars :fns)))
+    (compute-progn-touchable-keyword1 nil t (car args) (car args) (cdr args))
+    (compute-progn-touchable-keyword  nil t args)))
+
+(defmacro progn=touchable (&rest args)
+
+;;; This legacy doc string was replaced Nov. 2014 by a corresponding
+;;; auto-generated defxdoc form in file hacking-xdoc.lisp.
+
+; ":Doc-Section hacker
+;
+; execute some events with only the specified fns and/or vars temporarily touchable.~/
+
+; ~bv[]
+; Examples:
+; (progn=touchable :all ; same as :fns :all :vars :all
+;   (defun foo ...)
+;   (defun bar ...))
+; (progn=touchable :vars (current-package ld-skip-proofsp) ; :fns ()  implied
+;   ...)
+; (progn=touchable :fns :all    ; :vars ()  implied
+;   ...)
+; (progn=touchable :fns set-w :vars :all
+;   ...)
+; ~ev[] ~/
+
+; This is like ~ilc[progn] except that it surrounds the events with code to
+; set only certain fns and/or vars as temporarily touchable.
+;
+; Related to ~ilc[progn+touchable].
+;
+; An active ttag is required to use this form (~l[defttag]) because it
+; can render ACL2 unsound (~l[remove-untouchable]).
+;
+; Note that the syntax for this macro is not quite like traditional
+; keyword arguments, which would come at the end of the argument list.
+; ~/"
+  (declare (xargs :guard (and (consp args)
+                              (keywordp (car args)))))
+  (if (not (member-eq (car args) '(:vars :fns)))
+    (compute-progn-touchable-keyword1 nil nil (car args) (car args) (cdr args))
+    (compute-progn-touchable-keyword  nil nil args)))
+
+; for export
+(defmacro progn!+touchable (&rest args)
+  (declare (xargs :guard (and (consp args)
+                              (keywordp (car args)))))
+  (if (not (member-eq (car args) '(:vars :fns)))
+    (compute-progn-touchable-keyword1 t t (car args) (car args) (cdr args))
+    (compute-progn-touchable-keyword  t t args)))
+
+; for export
+(defmacro progn!=touchable (&rest args)
+  (declare (xargs :guard (and (consp args)
+                              (keywordp (car args)))))
+  (if (not (member-eq (car args) '(:vars :fns)))
+    (compute-progn-touchable-keyword1 t nil (car args) (car args) (cdr args))
+    (compute-progn-touchable-keyword  t nil args)))
+
+; for export
+(defmacro with-touchable (&rest args)
+
+;;; This legacy doc string was replaced Nov. 2014 by a corresponding
+;;; auto-generated defxdoc form in file hacking-xdoc.lisp.
+
+; ":Doc-Section hacker
+;
+; execute some events but with certain untouchables removed.
+; ~/~/
+; Same as ~c[progn+touchable]. ~l[progn+touchable]."
+  `(progn+touchable . ,args))
+
+
+
+;=========== begin redef stuff ===========
+
+(defun put-ld-redefinition-action (v state)
+  (mv-let (erp v state)
+      (set-ld-redefinition-action v state)
+      (declare (ignore v))
+      (prog2$
+       (and erp
+        (hard-error 'put-ld-redefinition-action
+                "~x0 returned an error."
+                '((#\0 . set-ld-redefinition-action))))
+       state)))
+
+(defun expand-redef-action-aliases (spec)
+  (cond ((equal spec t)
+         '(:doit! . :overwrite))
+        (t
+         spec)))
+
+(defmacro progn+redef-action (spec &rest form-lst)
+  (declare (xargs :guard form-lst))
+  `(progn!-with-bindings
+    ((ld-redefinition-action
+      ,(if (eq spec :unspecified)
+         '(@ ld-redefinition-action)
+         `(expand-redef-action-aliases ',spec))
+      put-ld-redefinition-action))
+    (progn . ,form-lst)))
+
+; for export
+(defmacro progn+redef (&rest args)
+
+;;; This legacy doc string was replaced Nov. 2014 by a corresponding
+;;; auto-generated defxdoc form in file hacking-xdoc.lisp.
+
+; ":Doc-Section hacker
+;
+; execute some events but with redefinition enabled.~/
+
+; ~bv[]
+; Examples (all equivalent):
+; (progn+redef
+;   (defun foo ...)
+;   (defun bar ...))
+; (progn+redef :action t
+;   ...)
+; (progn+redef :action (:doit! . :overwrite)
+;   ...)
+; ~ev[] ~/
+;
+; This is like ~ilc[progn] except that it sets the
+; ~ilc[ld-redefinition-action] as (optionally) specified for the
+; given events.  An ~c[:action] of ~c[t] is a shortcut for
+; ~c[(:doit! . :overwrite)].  ~ilc[make-event] is used to save and restore
+; the old value of ~ilc[ld-redefinition-action].
+;
+; An active ttag is required to use this form (~l[defttag]).
+;
+; Note that the syntax for this macro is not quite like traditional
+; keyword arguments, which would come at the end of the argument list.
+; ~/"
+  (declare (xargs :guard (consp args)))
+  (if (and (equal (car args) :action)
+           (consp (cdr args)))
+    `(progn+redef-action ,(cadr args) . ,(cddr args))
+    `(progn+redef-action t . ,args)))
+
+; for export
+(defmacro with-redef-allowed (&rest args)
+
+;;; This legacy doc string was replaced Nov. 2014 by a corresponding
+;;; auto-generated defxdoc form in file hacking-xdoc.lisp.
+
+; ":Doc-Section hacker
+;
+; execute some events but with redefinition enabled.
+; ~/~/
+; Same as ~c[progn+redef]. ~l[progn+redef]."
+  `(progn+redef . ,args))
+
+; for export
+; this is a wart from an older version of hacker.lisp
+(defmacro acl2::temporary-redef (&rest forms)
+  (declare (ignore forms))
+  (hard-error 'acl2::temporary-redef "Old implementation of ~x0 was flawed.  Adapt solution to use ~x1 (See :DOC ~x1)."
+              '((#\0 . acl2::temporary-redef)
+                (#\1 . progn+redef))))
+
+
+
+;=========== begin raw mode stuff ===========
+
+; for export
+(defmacro in-raw-mode (&rest form-lst)
+
+;;; This legacy doc string was replaced Nov. 2014 by a corresponding
+;;; auto-generated defxdoc form in file hacking-xdoc.lisp.
+
+; ":Doc-Section hacker
+;
+; embed some raw lisp code as an event.~/
+
+; ~bv[]
+; Example Form:
+; (in-raw-mode
+;   (format t \"Preparing to load file...~~%\")
+;   (load \"my-file.lisp\"))~/
+
+; General Form:
+; (in-raw-mode form1 form2 ... formk)
+; ~ev[]
+; where each ~c[formi] is processed as though all the forms are preceded by
+; ~c[:]~ilc[set-raw-mode]~c[ t].  Thus, the forms need not be ~il[events]; they
+; need not even be legal ACL2 forms.  ~l[set-raw-mode] for a discussion of the
+; so-called ``raw mode'' under which the forms are evaluated ~-[] unless raw
+; mode is disabled by one of the forms, for example, ~c[(set-raw-mode nil)], in
+; which case evaluation resumes in non-raw mode.
+
+; WARNING: Thus, an ~c[in-raw-mode] form is potentially very dangerous!  For
+; example, you can use it to call the Common Lisp ~c[load] function to load
+; arbitrary Common Lisp code, perhaps even overwriting definitions of ACL2
+; system functions!  Thus, as with ~ilc[set-raw-mode], ~ilc[in-raw-mode] may
+; not be evaluated unless there is an active trust tag in effect.  ~l[defttag].
+
+; Note that the normal undoing mechanism (~pl[ubt]) is not supported when raw
+; mode is used.
+; ~/"
+  `(progn! (with-output :off observation (set-raw-mode-on state))
+           (progn
+             ,@form-lst
+             nil)
+           ;;acl2-raw-mode-p is restored by progn!-fn
+           ))
+
+; for export
+(defmacro with-raw-mode (&rest args)
+
+;;; This legacy doc string was replaced Nov. 2014 by a corresponding
+;;; auto-generated defxdoc form in file hacking-xdoc.lisp.
+
+; ":Doc-Section hacker
+;
+; embed some raw lisp code as an event.
+; ~/~/
+; Same as ~c[in-raw-mode]. ~l[in-raw-mode]."
+  `(in-raw-mode . ,args))
+
+
+;=========== begin program-only stuff ===========
+
+; figure out which var is the program-only state global
+(make-event
+ (if (member-eq 'program-fns-with-raw-code (global-val 'untouchable-vars (w state)))
+   (value
+    '(defconst *program-only-state-global* 'program-fns-with-raw-code))
+   (value
+    '(defconst *program-only-state-global* 'built-in-program-mode-fns))))
+
+
+; for export
+(defmacro ensure-program-only-flag (&rest fn-lst)
+
+;;; This legacy doc string was replaced Nov. 2014 by a corresponding
+;;; auto-generated defxdoc form in file hacking-xdoc.lisp.
+
+; ":Doc-Section hacker
+;
+; ensure that given function names remain in :PROGRAM mode.~/
+
+; ~bv[]
+; Example Form:
+; (ensure-program-only-flag my-fn your-fn)~/
+
+; General Form:
+; (ensure-program-only-flag fn1 fn2 ... fnk)
+; ~ev[]
+; where each ~c[fni] is a literal symbol which should have a ~ilc[program] mode
+; definition. Each ~c[fni] not already flagged as \"program only\" is flagged
+; as such.  This prevents it from being migrated to ~ilc[logic] mode or being
+; used in a macro.
+;
+; This is a pseudo-event, meaning it can be used in an event context but does
+; not (ever) change the world.
+;
+; Note that the normal undoing mechanism (~pl[ubt]) does not undo the effects
+; of this pseudo-event.
+; ~/"
+  (declare (xargs :guard (and fn-lst
+                              (symbol-listp fn-lst))))
+  `(progn!=touchable :vars ,*program-only-state-global*
+     (assign ,*program-only-state-global*
+       (union-eq (@ ,*program-only-state-global*) ',fn-lst))))
+
+; test whether a function is in :PROGRAM mode
+(defun program-mode-p (fn wrld)
+  (eq ':program
+      (getprop fn 'symbol-class nil 'current-acl2-world wrld)))
+
+; test whether all functions in a list are in :PROGRAM mode
+(defun program-mode-p-lst (fn-lst wrld)
+  (or (endp fn-lst)
+      (and (program-mode-p     (car fn-lst) wrld)
+           (program-mode-p-lst (cdr fn-lst) wrld))))
+
+; for export
+(defmacro assert-program-mode (&rest fn-lst)
+
+;;; This legacy doc string was replaced Nov. 2014 by a corresponding
+;;; auto-generated defxdoc form in file hacking-xdoc.lisp.
+
+; ":Doc-Section hacker
+;
+; assert that given symbols name :PROGRAM mode functions.~/
+
+; ~bv[]
+; Example Form:
+; (assert-program-mode my-fn your-fn)~/
+
+; General Form:
+; (assert-program-mode fn1 fn2 ... fnk)
+; ~ev[]
+; where each ~c[fni] is a literal symbol which should have a ~ilc[program] mode
+; definition. An error is raised if any ~c[fni] is not a program mode function.
+;
+; This is a pseudo-event, meaning it can be used in an event context but does
+; not (ever) change the world.
+; ~/"
+  (declare (xargs :guard (and fn-lst
+                              (symbol-listp fn-lst))))
+  `(assert-event
+    (program-mode-p-lst ',fn-lst (w state))
+    :msg (msg "Assertion failed.  At least one not :program mode:~%~x0"
+              ',fn-lst)
+    :on-skip-proofs t))
+
+; for export
+(defmacro ensure-program-only (&rest fn-lst)
+
+;;; This legacy doc string was replaced Nov. 2014 by a corresponding
+;;; auto-generated defxdoc form in file hacking-xdoc.lisp.
+
+; ":Doc-Section hacker
+;
+; ensure that named functions are and remain in :PROGRAM mode.~/
+
+; ~bv[]
+; Example Form:
+; (ensure-program-only my-fn your-fn)~/
+
+; General Form:
+; (ensure-program-only fn1 fn2 ... fnk)
+; ~ev[]
+; where each ~c[fni] is a literal symbol which should have a ~ilc[program] mode
+; definition. An error is raised if any ~c[fni] is not a program mode function.
+; Also, each ~c[fni] not already flagged as \"program only\" is flagged
+; as such.  This prevents it from being migrated to ~ilc[logic] mode or being
+; used in a macro.
+;
+; This is actually a combination of ~ilc[assert-program-mode] and
+; ~ilc[ensure-program-only-flag].
+;
+; This is a pseudo-event, meaning it can be used in an event context but does
+; not (ever) change the world.
+;
+; Note that the normal undoing mechanism (~pl[ubt]) does not undo the effects
+; of this pseudo-event.
+; ~/"
+  (declare (xargs :guard (and fn-lst
+                              (symbol-listp fn-lst))))
+  `(progn (assert-program-mode . ,fn-lst)
+          (ensure-program-only-flag . ,fn-lst)))
+
+
+
+;=========== begin special-raw-definition stuff ===========
+
+; Here we introduce the notion of a "special raw definition",
+; which is somewhat related to the notion of "program only" but
+; importantly different.  The intended difference is this:
+; - A function should be "program only" if bad things could happen as
+;   a result of it migrating to logic mode (with verify-termination)
+;   or by use in macro expansion.
+; - A function should be considered to have a "special raw definition"
+;   if bad things could happen as a result of replacing its raw
+;   definition with the raw counterpart of its "loop" definition.
+;TODO: more
+
+(defconst *bootstrap-special-raw-definitions*
+  '(
+    ;;-- from axioms.lisp --
+    ;;len         #|not special, just fast|#
+    ;;strip-cars  #|not special, just fast|#
+    ;;strip-cdrs  #|not special, just fast|#
+    acl2::complex-rationalp
+    acl2::must-be-equal
+    acl2::zp
+    acl2::zip
+    acl2::prog2$
+    acl2::time$
+    acl2::hard-error
+    acl2::intern-in-package-of-symbol
+    acl2::pkg-witness
+    acl2::with-output
+    acl2::value-triple-fn
+    acl2::value-triple
+    acl2::pprogn
+    acl2::acl2-unwind-protect
+    acl2::defund
+    acl2::plist-worldp
+    acl2::getprop-default
+    acl2::fgetprop
+    acl2::sgetprop
+    acl2::getprops
+    acl2::has-propsp
+    acl2::extend-world
+    acl2::retract-world
+    acl2::array-1p
+    acl2::array-2pz
+    acl2::header
+    acl2::aref1
+    acl2::compress1
+    acl2::aset1
+    acl2::aref2
+    acl2::compress2
+    acl2::aset2
+    acl2::flush-compress
+    acl2::state-p1
+    acl2::global-table-cars1
+    acl2::boundp-global1
+    acl2::fboundp-global
+    acl2::makunbound-global
+    acl2::get-global
+    acl2::f-get-global
+    acl2::put-global
+    acl2::f-put-global
+    acl2::zpf
+    acl2::open-input-channel-p1
+    acl2::open-output-channel-p1
+    acl2::princ$
+    acl2::write-byte$
+    acl2::print-object$-ser ; Matt K. change shortly after v4-3
+    acl2::open-input-channel
+    acl2::close-input-channel
+    acl2::open-output-channel
+    acl2::close-output-channel
+    acl2::read-char$
+    acl2::peek-char$
+    acl2::read-byte$
+    acl2::read-object
+    acl2::prin1-with-slashes
+    acl2::may-need-slashes
+    acl2::t-stack-length1
+    acl2::extend-t-stack
+    acl2::shrink-t-stack
+    acl2::aref-t-stack
+    acl2::aset-t-stack
+    acl2::32-bit-integer-stack-length1
+    acl2::extend-32-bit-integer-stack
+    acl2::shrink-32-bit-integer-stack
+    acl2::aref-32-bit-integer-stack
+    acl2::aset-32-bit-integer-stack
+    acl2::f-big-clock-negative-p
+    acl2::f-decrement-big-clock
+    acl2::big-clock-negative-p
+    acl2::decrement-big-clock
+    acl2::list-all-package-names
+    acl2::user-stobj-alist
+    acl2::update-user-stobj-alist
+    acl2::read-idate
+    acl2::read-run-time
+    acl2::read-acl2-oracle
+    acl2::getenv$
+    acl2::setenv$
+    acl2::prin1$
+    acl2::the-mv
+    acl2::set-enforce-redundancy
+    acl2::set-verify-guards-eagerness
+    acl2::set-compile-fns
+    acl2::set-measure-function
+    acl2::set-well-founded-relation
+    acl2::logic
+    acl2::program
+    acl2::set-bogus-mutual-recursion-ok
+    acl2::set-irrelevant-formals-ok
+    acl2::set-ignore-ok
+    acl2::set-inhibit-warnings
+    acl2::set-inhibit-output-lst
+    acl2::set-state-ok
+    acl2::set-let*-abstractionp
+    acl2::set-backchain-limit
+    acl2::set-default-backchain-limit
+    acl2::set-rewrite-stack-limit
+    acl2::set-case-split-limitations
+    acl2::set-match-free-default
+    acl2::add-match-free-override
+    acl2::add-include-book-dir
+    acl2::delete-include-book-dir
+    acl2::set-non-linearp
+    acl2::defttag
+    acl2::set-default-hints!
+    acl2::add-default-hints!
+    acl2::remove-default-hints!
+    acl2::with-prover-time-limit
+    acl2::catch-time-limit4
+    acl2::time-limit4-reached-p
+    acl2::wormhole1
+    acl2::wormhole-p
+    acl2::abort!
+    acl2::er
+    acl2::mfc-clause
+    acl2::mfc-rdepth
+    acl2::mfc-type-alist
+    acl2::mfc-ancestors
+    acl2::bad-atom<=
+    acl2::alphorder
+
+    ;;-- from translate.lisp --
+    acl2::latch-stobjs1
+    acl2::big-n
+    acl2::decrement-big-n
+    acl2::zp-big-n
+    acl2::w-of-any-state
+    acl2::ev-fncall-rec
+    acl2::ev-rec
+    acl2::ev-rec-acl2-unwind-protect
+    acl2::ev-fncall
+    acl2::ev
+    acl2::ev-lst
+    acl2::ev-fncall-w
+    acl2::untranslate
+    acl2::untranslate-lst
+    acl2::ev-w
+    acl2::ev-w-lst
+    acl2::user-stobj-alist-safe
+
+    ;;-- from history-management.lisp --
+    acl2::start-proof-tree
+    acl2::initialize-summary-accumulators
+    acl2::print-summary
+    acl2::set-w
+    acl2::longest-common-tail-length-rec
+    acl2::chk-virgin
+
+    ;;-- from other-events.lisp --
+    in-package
+    defpkg
+    defchoose
+    defun
+    defuns
+    verify-termination
+    verify-guards
+    defmacro
+    defconst
+    defstobj
+    defthm
+    defaxiom
+    deflabel
+    defdoc
+    deftheory
+    in-theory
+    in-arithmetic-theory
+    push-untouchable
+    reset-prehistory
+    set-body
+    table
+    progn
+    encapsulate
+    include-book
+    local
+
+    acl2::chk-package-reincarnation-import-restrictions
+    acl2::theory-invariant
+    acl2::acl2-raw-eval
+    acl2::protected-eval-with-proofs
+    acl2::include-book-fn
+    acl2::write-expansion-file
+    acl2::certify-book-fn
+    acl2::defstobj-field-fns-raw-defs
+    acl2::open-trace-file-fn
+    acl2::close-trace-file-fn
+    acl2::with-error-trace-fn
+    acl2::trace$-fn-general
+    acl2::trace$-fn-simple
+    acl2::untrace$-fn
+    acl2::break-on-error-fn
+
+    ;;-- from ld.lisp --
+    acl2::ld-print-results
+    acl2::print-newline-for-time$
+    acl2::good-bye-fn
+    acl2::ld-loop
+    acl2::ld-fn-body
+    acl2::ld-fn
+    acl2::compile-function
+    acl2::comp-fn
+    acl2::comp
+    acl2::break$
+    acl2::set-debugger-enable-fn
+    acl2::mfc-ts
+    acl2::mfc-rw
+    acl2::mfc-rw+
+    acl2::mfc-relieve-hyp
+    acl2::mfc-ap
+    acl2::save-exec
+
+    ))
+
+#|| Removed by Matt K. after ACL2 Version 3.6.1 in favor of the defmacro just
+    below,  because make-event expansion does not take place during (early)
+    loading of compiled files.
+(make-event ; used here like progn! without a ttag
+ (er-progn
+  (if (member-eq 'has-special-raw-definition
+                 (global-val 'untouchable-vars (w state)))
+    (value nil) ; assume we're already good
+    (assign has-special-raw-definition
+      (union-eq (@opt has-special-raw-definition)
+                *bootstrap-special-raw-definitions*)))
+  (value '(value-triple 'has-special-raw-definition)))
+ :check-expansion t)
+||#
+
+(defmacro update-has-special-raw-definition (fn-lst)
+  `(pprogn (if (boundp-global 'has-special-raw-definition state)
+               state
+             (f-put-global 'has-special-raw-definition
+                           *bootstrap-special-raw-definitions*
+                           state))
+           (assign has-special-raw-definition
+                   (union-eq (@ has-special-raw-definition)
+                             ,fn-lst))))
+
+(push-untouchable has-special-raw-definition nil)
+
+; for export
+(defmacro ensure-special-raw-definition-flag (&rest fn-lst)
+
+;;; This legacy doc string was replaced Nov. 2014 by a corresponding
+;;; auto-generated defxdoc form in file hacking-xdoc.lisp.
+
+; ":Doc-Section hacker
+;
+; ensure that named functions are flagged as having special raw definitions.~/
+
+; ~bv[]
+; Example Form:
+; (ensure-special-raw-definition-flag my-fn your-fn)~/
+
+; General Form:
+; (ensure-special-raw-definition-flag fn1 fn2 ... fnk)
+; ~ev[]
+; where each ~c[fni] is a literal symbol which should have a function
+; definition. Each ~c[fni] not already flagged as having a special raw
+; definition is flagged as such.  This idicates to interested parties that
+; the \"loop\" definition of the function doesn't fully characterize the
+; effects it has in raw lisp.
+;
+; This is a pseudo-event, meaning it can be used in an event context but does
+; not (ever) change the world.
+;
+; Note that the normal undoing mechanism (~pl[ubt]) does not undo the effects
+; of this pseudo-event.
+; ~/"
+  (declare (xargs :guard (and fn-lst
+                              (symbol-listp fn-lst))))
+  `(progn!=touchable :vars has-special-raw-definition
+     (update-has-special-raw-definition ',fn-lst)))
+
+; for export
+(defmacro assert-no-special-raw-definition (&rest fn-lst)
+
+;;; This legacy doc string was replaced Nov. 2014 by a corresponding
+;;; auto-generated defxdoc form in file hacking-xdoc.lisp.
+
+; ":Doc-Section hacker
+;
+; assert that given symbols do not have a special raw function definition.~/
+
+; ~bv[]
+; Example Form:
+; (assert-no-special-raw-definition my-fn your-fn)~/
+
+; General Form:
+; (assert-no-special-raw-definition fn1 fn2 ... fnk)
+; ~ev[]
+; where each ~c[fni] is a literal symbol.  An error is raised if any ~c[fni]
+; is is flagged as having a special raw definition.
+; ~l[ensure-special-raw-definition-flag].
+;
+; This is a pseudo-event, meaning it can be used in an event context but does
+; not (ever) change the world.
+; ~/"
+  (declare (xargs :guard (and fn-lst
+                              (symbol-listp fn-lst))))
+  `(assert-event
+    (not (intersectp-eq (@opt has-special-raw-definition)
+                        ',fn-lst))
+    :msg (msg "Assertion failed.  Flagged as having special raw definition:~%~x0"
+              (intersection-eq (@opt has-special-raw-definition)
+                               ',fn-lst))
+    :on-skip-proofs t))
+
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; modify-raw-defun-permanent
+;
+; for permanently installing some changes (supporting defcode)
+;
+
+; for export
+(defmacro modify-raw-defun-permanent
+  (name name-for-old ll &rest decls-and-body)
+  (declare (xargs :guard (and (symbolp name)
+                              (symbolp name-for-old)
+                              (symbol-listp ll)
+                              (consp decls-and-body))))
+  `(progn
+    (in-raw-mode
+     (unless (fboundp ',name-for-old)
+             ; if the name-for-old already has a definition, we don't override
+             ; it. this provides idempotency for modify-raw-defun-permanent
+             ; but means this code doesn't know the first time whether
+             ; name-for-old is fresh/unused.
+             (setf (symbol-function ',name-for-old)
+                   (symbol-function ',name)))
+     (defun ,name ,ll
+       ,@ (and ll `((declare (ignorable . ,ll))))
+       . ,decls-and-body))
+    (ensure-special-raw-definition-flag ,name)))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; deflabels
+;
+; for stubbing out ACL2 names
+;
+
+(defun build-deflabels (names)
+  (if (endp names)
+    nil
+    (cons (list 'deflabel (car names))
+          (build-deflabels (cdr names)))))
+
+; for export
+(defmacro deflabels (&rest names)
+  `(progn
+     (with-output :off summary
+                  (progn . ,(build-deflabels names)))
+     (value-triple ',names)))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; allow other ttags
+;
+; this should only be used in subsuming hacker stuff, like so:
+;
+#|
+(include-book
+ "hacker/hacker")
+(progn+all-ttags-allowed
+ (include-book
+  "hacker/all" :ttags ((defcode) (table-guard))))
+(subsume-ttags-since-defttag) ; see subsumption.lisp
+|#
+;
+; this is a work-around for subsuming before progn+subsume-ttags is available.
+;
+
+; for export
+(defmacro progn+all-ttags-allowed (&rest form-lst)
+  `(progn!-with-bindings
+    ((temp-touchable-vars (if (eq (@ temp-touchable-vars) t)
+                            t
+                            (cons 'acl2::ttags-allowed (@ temp-touchable-vars)))
+                          set-temp-touchable-vars))
+    (progn!-with-bindings
+     ((acl2::ttags-allowed :all))
+     (progn!-with-bindings
+      ((temp-touchable-vars (if (eq (@ temp-touchable-vars) t)
+                              t
+                              (cdr (@ temp-touchable-vars)))
+                            set-temp-touchable-vars))
+      (progn . ,form-lst)))))
+
+
+#|; some tests
+(defttag test1)
+(progn+allow-ttags
+ :all
+ (defttag test2)
+ (progn+touchable :all
+                  (defun foo (x) (1+ x)))
+ (progn! (cw "Hi!~%")))
+(progn+allow-ttags
+ nil
+ (defttag test3)
+ (progn+touchable :all
+                  (defun foo (x) (1+ x)))
+ (progn! (cw "Hi!~%")))
+;|#
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; ttag-skip-proofs
+;
+; uses a ttag to skip proofs without the ordinary record that
+; proofs were skipped.
+;
+
+(defun put-ld-skip-proofsp (v state)
+  (mv-let (erp v state)
+      (set-ld-skip-proofsp v state)
+      (declare (ignore v))
+      (prog2$
+       (and erp
+        (hard-error 'set-ld-skip-proofsp
+                "~x0 returned an error."
+                '((#\0 . set-ld-skip-proofsp))))
+       state)))
+
+; for export
+(defmacro ttag-skip-proofs (x)
+  `(progn!-with-bindings
+    ((ld-skip-proofsp 'include-book put-ld-skip-proofsp))
+    (progn ,x)))
+
+; for export
+(defmacro progn+ttag-skip-proofs (&rest args)
+  `(progn!-with-bindings
+    ((ld-skip-proofsp 'include-book put-ld-skip-proofsp))
+    (progn . ,args)))
+
diff --git a/books/hacking/hacking-xdoc.lisp b/books/hacking/hacking-xdoc.lisp
new file mode 100644
index 0000000..5d04737
--- /dev/null
+++ b/books/hacking/hacking-xdoc.lisp
@@ -0,0 +1,309 @@
+; This file was initially generated automatically from legacy documentation
+; strings.  See source files in this directory for copyright and license
+; information.
+
+(in-package "ACL2")
+
+(include-book "xdoc/top" :dir :system)
+
+(defxdoc assert-no-special-raw-definition
+  :parents (hacker)
+  :short "Assert that given symbols do not have a special raw function definition."
+  :long "@({
+  Example Form:
+  (assert-no-special-raw-definition my-fn your-fn)
+
+  General Form:
+  (assert-no-special-raw-definition fn1 fn2 ... fnk)
+ })
+
+ <p>where each @('fni') is a literal symbol.  An error is raised if any
+ @('fni') is is flagged as having a special raw definition.  See @(see
+ ensure-special-raw-definition-flag).
+
+ This is a pseudo-event, meaning it can be used in an event context but does
+ not (ever) change the world.</p>")
+
+(defxdoc assert-program-mode
+  :parents (hacker)
+  :short "Assert that given symbols name :PROGRAM mode functions."
+  :long "@({
+  Example Form:
+  (assert-program-mode my-fn your-fn)
+
+  General Form:
+  (assert-program-mode fn1 fn2 ... fnk)
+ })
+
+ <p>where each @('fni') is a literal symbol which should have a @(tsee program)
+ mode definition. An error is raised if any @('fni') is not a program mode
+ function.
+
+ This is a pseudo-event, meaning it can be used in an event context but does
+ not (ever) change the world.</p>")
+
+(defxdoc defun-bridge
+  :parents (hacker)
+  :short "Define a function with a different low-level definition."
+  :long "<code>
+ General Form:
+ (defun-bridge <i>name</i> (<i>formals</i>)
+   [:doc <i>doc-string</i>]
+   [:loop-declare <i>loop-decls</i>]
+   :loop <i>loop-body</i>
+   [:raw-declare <i>raw-decls</i>]
+   :raw <i>raw-body</i>)
+ </code>
+
+ <p>This is much like executing</p>
+
+ <code>
+ (defun <i>name</i> (<i>formals</i>)
+   <i>doc-string</i>
+   (declare (xargs :mode :program))
+   <i>loop-decls</i>
+   <i>loop-body</i>)
+ </code>
+
+ <p>in ACL2 and then</p>
+
+ <code>
+ (defun <i>name</i> (<i>formals</i>)
+   <i>raw-decls</i>
+   <i>raw-body</i>)
+ </code>
+
+ <p>in raw Lisp, except that extra checks and bookkeeping make it safer than
+ that.
+
+ An active ttag is required to use this form (See @(see defttag)), because
+ it can easily corrupt ACL2 or render it unsound.</p>")
+
+(defxdoc ensure-program-only
+  :parents (hacker)
+  :short "Ensure that named functions are and remain in :PROGRAM mode."
+  :long "@({
+  Example Form:
+  (ensure-program-only my-fn your-fn)
+
+  General Form:
+  (ensure-program-only fn1 fn2 ... fnk)
+ })
+
+ <p>where each @('fni') is a literal symbol which should have a @(tsee program)
+ mode definition. An error is raised if any @('fni') is not a program mode
+ function.  Also, each @('fni') not already flagged as \"program only\" is
+ flagged as such.  This prevents it from being migrated to @(tsee logic) mode
+ or being used in a macro.
+
+ This is actually a combination of @(tsee assert-program-mode) and
+ @(tsee ensure-program-only-flag).
+
+ This is a pseudo-event, meaning it can be used in an event context but does
+ not (ever) change the world.
+
+ Note that the normal undoing mechanism (see @(see ubt)) does not undo the effects
+ of this pseudo-event.</p>")
+
+(defxdoc ensure-program-only-flag
+  :parents (hacker)
+  :short "Ensure that given function names remain in :PROGRAM mode."
+  :long "@({
+  Example Form:
+  (ensure-program-only-flag my-fn your-fn)
+
+  General Form:
+  (ensure-program-only-flag fn1 fn2 ... fnk)
+ })
+
+ <p>where each @('fni') is a literal symbol which should have a @(tsee program)
+ mode definition. Each @('fni') not already flagged as \"program only\" is
+ flagged as such.  This prevents it from being migrated to @(tsee logic) mode
+ or being used in a macro.
+
+ This is a pseudo-event, meaning it can be used in an event context but does
+ not (ever) change the world.
+
+ Note that the normal undoing mechanism (see @(see ubt)) does not undo the effects
+ of this pseudo-event.</p>")
+
+(defxdoc ensure-special-raw-definition-flag
+  :parents (hacker)
+  :short "Ensure that named functions are flagged as having special raw definitions."
+  :long "@({
+  Example Form:
+  (ensure-special-raw-definition-flag my-fn your-fn)
+
+  General Form:
+  (ensure-special-raw-definition-flag fn1 fn2 ... fnk)
+ })
+
+ <p>where each @('fni') is a literal symbol which should have a function
+ definition. Each @('fni') not already flagged as having a special raw
+ definition is flagged as such.  This idicates to interested parties that the
+ \"loop\" definition of the function doesn't fully characterize the effects it
+ has in raw lisp.
+
+ This is a pseudo-event, meaning it can be used in an event context but does
+ not (ever) change the world.
+
+ Note that the normal undoing mechanism (see @(see ubt)) does not undo the effects
+ of this pseudo-event.</p>")
+
+(defxdoc hacker
+  :parents (interfacing-tools)
+  :short "Functions for extending ACL2 in ways that are potentially unsound."
+  :long "<p>The @('books/hacking') library.</p>
+
+ <p>These functions typically require an active ttag (See @(see defttag)) to
+ work.</p>
+
+ ")
+
+(defxdoc in-raw-mode
+  :parents (hacker)
+  :short "Embed some raw lisp code as an event."
+  :long "@({
+  Example Form:
+  (in-raw-mode
+    (format t \"Preparing to load file...~%\")
+    (load \"my-file.lisp\"))
+
+  General Form:
+  (in-raw-mode form1 form2 ... formk)
+ })
+
+ <p>where each @('formi') is processed as though all the forms are preceded by
+ @(':')@(tsee set-raw-mode)@(' t').  Thus, the forms need not be @(see events);
+ they need not even be legal ACL2 forms.  See @(see set-raw-mode) for a
+ discussion of the so-called ``raw mode'' under which the forms are evaluated
+ &mdash; unless raw mode is disabled by one of the forms, for example,
+ @('(set-raw-mode nil)'), in which case evaluation resumes in non-raw mode.</p>
+
+ <p>WARNING: Thus, an @('in-raw-mode') form is potentially very dangerous!  For
+ example, you can use it to call the Common Lisp @('load') function to load
+ arbitrary Common Lisp code, perhaps even overwriting definitions of ACL2
+ system functions!  Thus, as with @(tsee set-raw-mode), @(tsee in-raw-mode) may
+ not be evaluated unless there is an active trust tag in effect.  See @(see
+ defttag).</p>
+
+ <p>Note that the normal undoing mechanism (see @(see ubt)) is not supported
+ when raw mode is used.</p>")
+
+(defxdoc progn+redef
+  :parents (hacker)
+  :short "Execute some events but with redefinition enabled."
+  :long "@({
+  Examples (all equivalent):
+  (progn+redef
+    (defun foo ...)
+    (defun bar ...))
+  (progn+redef :action t
+    ...)
+  (progn+redef :action (:doit! . :overwrite)
+    ...)
+ })
+
+ <p>This is like @(tsee progn) except that it sets the @(tsee
+ ld-redefinition-action) as (optionally) specified for the given events.  An
+ @(':action') of @('t') is a shortcut for @('(:doit! . :overwrite)').  @(tsee
+ make-event) is used to save and restore the old value of @(tsee
+ ld-redefinition-action).
+
+ An active ttag is required to use this form (See @(see defttag)).
+
+ Note that the syntax for this macro is not quite like traditional
+ keyword arguments, which would come at the end of the argument list.</p>")
+
+(defxdoc progn+subsume-ttags
+  :parents (hacker)
+  :short "Execute some events, subsuming the specified ttags with the current ttag."
+  :long "@({
+  Example:
+  (progn+subsume-ttags
+    ((:foo) (:bar))
+    (include-book
+     \"foo\" :ttags ((:foo)))
+    (include-book
+     \"bar\" :ttags ((:bar))))
+ })
+
+ <p>This is like @(tsee progn) except that the first argument is a ttag-spec
+ (See @(see defttag)) to be authorized within the constituent events and then
+ subsumed.  That is, an active ttag is required to use this form and that ttag
+ is (first) used to allow the use of other ttags that may not already be
+ authorized and (second) used to wipe the record that any extra ttags were
+ used.  This is what is meant by subsumption.  If my book requires a ttag, I
+ can then use this to include other books/forms requiring other ttags without
+ those others needing specific prior authorization.
+
+ An active ttag is required to use this form (See @(see defttag)).</p>")
+
+(defxdoc progn+touchable
+  :parents (hacker)
+  :short "Execute some events with some additional fns and/or vars made temporarily touchable."
+  :long "@({
+  Examples:
+  (progn+touchable :all ; same as :fns :all :vars :all
+    (defun foo ...)
+    (defun bar ...))
+  (progn+touchable :vars (current-package ld-skip-proofsp)
+    ...)
+  (progn+touchable :fns :all
+    ...)
+  (progn+touchable :fns set-w :vars :all
+    ...)
+ })
+
+ <p>This is like @(tsee progn) except that it surrounds the events with code to
+ add certain fns and/or vars to those that are temporarily touchable.
+
+ Related to @(tsee progn=touchable).
+
+ An active ttag is required to use this form (See @(see defttag)) because it
+ can render ACL2 unsound (See @(see remove-untouchable)).
+
+ Note that the syntax for this macro is not quite like traditional
+ keyword arguments, which would come at the end of the argument list.</p>")
+
+(defxdoc progn=touchable
+  :parents (hacker)
+  :short "Execute some events with only the specified fns and/or vars temporarily touchable."
+  :long "@({
+  Examples:
+  (progn=touchable :all ; same as :fns :all :vars :all
+    (defun foo ...)
+    (defun bar ...))
+  (progn=touchable :vars (current-package ld-skip-proofsp) ; :fns ()  implied
+    ...)
+  (progn=touchable :fns :all    ; :vars ()  implied
+    ...)
+  (progn=touchable :fns set-w :vars :all
+    ...)
+ })
+
+ <p>This is like @(tsee progn) except that it surrounds the events with code to
+ set only certain fns and/or vars as temporarily touchable.
+
+ Related to @(tsee progn+touchable).
+
+ An active ttag is required to use this form (See @(see defttag)) because it
+ can render ACL2 unsound (See @(see remove-untouchable)).
+
+ Note that the syntax for this macro is not quite like traditional
+ keyword arguments, which would come at the end of the argument list.</p>")
+
+(defxdoc with-raw-mode
+  :parents (hacker)
+  :short "Embed some raw lisp code as an event."
+  :long "<p>Same as @('in-raw-mode'). See @(see in-raw-mode).</p>")
+
+(defxdoc with-redef-allowed
+  :parents (hacker)
+  :short "Execute some events but with redefinition enabled."
+  :long "<p>Same as @('progn+redef'). See @(see progn+redef).</p>")
+
+(defxdoc with-touchable
+  :parents (hacker)
+  :short "Execute some events but with certain untouchables removed."
+  :long "<p>Same as @('progn+touchable'). See @(see progn+touchable).</p>")
diff --git a/books/hacking/progn-bang-enh.acl2 b/books/hacking/progn-bang-enh.acl2
new file mode 100644
index 0000000..bd1a252
--- /dev/null
+++ b/books/hacking/progn-bang-enh.acl2
@@ -0,0 +1,3 @@
+(in-package "ACL2")
+; cert-flags: ? t :ttags ((defcode))
+(certify-book "progn-bang-enh" ? t :ttags ((defcode)))
diff --git a/books/hacking/progn-bang-enh.lisp b/books/hacking/progn-bang-enh.lisp
new file mode 100644
index 0000000..e84f9a9
--- /dev/null
+++ b/books/hacking/progn-bang-enh.lisp
@@ -0,0 +1,63 @@
+(in-package "ACL2")
+
+#|
+
+This is a hack to add some special features to PROGN!:
+
+(progn! :compile-only ...)  expands to the given forms ONLY for the raw
+lisp compiler and not the ACL2 loop.
+
+(progn! :loop-only ...) expands to the given forms ONLY for the ACL2 loop
+and not the raw lisp compiler.
+
+This is currently the basis for implementing DEFCODE, and may not be
+in the future.
+
+|#
+
+(defttag defcode)
+
+(progn!
+ (set-ld-redefinition-action '(:doit! . :overwrite) state)
+ (defmacro progn! (&rest r)
+   (declare (xargs :guard (or (not (symbolp (car r)))
+                              (member-eq (car r)
+                                         '(:state-global-bindings
+                                           :compile-only
+                                           :loop-only)))))
+   (cond
+    ((not (consp r))
+     '(progn!-fn nil nil state))
+    ((eq (car r) :compile-only)
+     `(progn!-fn nil nil state))
+    ((eq (car r) :state-global-bindings)
+     `(state-global-let* ,(cadr r)
+                         (progn!-fn ',(cddr r) ',(cadr r) state)))
+    ((eq (car r) :loop-only)
+     `(progn!-fn ',(cdr r) nil state))
+    (t
+     `(progn!-fn ',r nil state))))
+ (set-ld-redefinition-action nil state)
+ (set-raw-mode t)
+ (progn
+  (defmacro progn! (&rest r)
+    (let ((sym (gensym)))
+      `(let ((state *the-live-state*)
+             (,sym (f-get-global 'acl2-raw-mode-p *the-live-state*)))
+         (declare (ignorable state))
+         ,@(cond ((not (consp r))
+                  (list nil))
+                 ((eq (car r) :loop-only)
+                  (list nil))
+                 ((eq (car r) :compile-only)
+                  (cdr r))
+                 ((eq (car r) :state-global-bindings)
+                  (cddr r))
+                 (t r))
+         (f-put-global 'acl2-raw-mode-p ,sym state)
+         (value nil))))
+  nil)
+ (set-raw-mode nil))
+
+;(reset-prehistory t)
+
diff --git a/books/hacking/raw.acl2 b/books/hacking/raw.acl2
new file mode 100644
index 0000000..0f9c1e6
--- /dev/null
+++ b/books/hacking/raw.acl2
@@ -0,0 +1,3 @@
+(in-package "ACL2")
+(ld "hacker-pkg.lsp")
+(certify-book "raw" ? t)
diff --git a/books/hacking/raw.lisp b/books/hacking/raw.lisp
new file mode 100644
index 0000000..7662024
--- /dev/null
+++ b/books/hacking/raw.lisp
@@ -0,0 +1,256 @@
+(in-package "ACL2")
+
+; Modification by Matt K. after v4-3: Removed :load-compiled-file :comp, which
+; was part of the include-book forms just below, in support of provisional
+; certification.  Presumably the indicated books have already been compiled by
+; now, anyhow.
+(include-book "defstruct-parsing"); was in portcullis
+
+;Needed to use, but not needed for certification:
+;(include-book "defcode" :load-compiled-file :comp :ttags ((defcode)))
+
+(program)
+(set-state-ok t)
+
+
+; a helper macro for building other stuff
+(defmacro make-raw-definitions (code &key compile fresh
+                                save-fns save-macros save-vars)
+  (declare (xargs :guard (and (true-listp code)
+                              (or (booleanp compile)
+                                  (true-listp compile))
+                              (or (booleanp fresh)
+                                  (symbol-listp fresh))
+                              (symbol-listp save-fns)
+                              (symbol-listp save-macros)
+                              (symbol-listp save-vars))))
+  (let* ((all-saves (append save-fns save-macros save-vars))
+         (fresh-lst (if (eq fresh 't) all-saves fresh)))
+    `(with-output
+      :off summary
+      (progn
+       ,@ (and fresh-lst
+               `((assert-unbound . ,fresh-lst)
+                 (deflabels . ,fresh-lst)))
+       ,@ (and save-fns
+               `((ensure-special-raw-definition-flag . ,save-fns)))
+       (defcode
+         :extend
+         (in-raw-mode ,@ (and save-fns
+                              `((dolist (f ',save-fns)
+                                        (maybe-push-undo-stack 'defun f))))
+                      ,@ (and save-macros
+                              `((dolist (m ',save-macros)
+                                        (maybe-push-undo-stack 'defmacro m))))
+                      ,@ (and save-vars
+                              `((dolist (v ',save-vars)
+                                        (maybe-push-undo-stack 'defconst v))))
+                      ,@ code)
+         :retract
+         ,(and all-saves
+               `(in-raw-mode (dolist (s ',all-saves)
+                                     (maybe-pop-undo-stack s))))
+         :compile
+         (progn . ,(if (eq compile 't) code compile)))))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; some low-level pieces for building high-level abstractions
+;
+;
+
+(defmacro defun-raw (name ll &rest rst)
+  `(make-raw-definitions
+    ((defun ,name ,ll . ,rst))
+    :compile t
+    :fresh t
+    :save-fns (,name)))
+
+
+(defmacro defmacro-raw (name ll &rest rst)
+  `(make-raw-definitions
+    ((defmacro ,name ,ll . ,rst))
+    :compile t
+    :fresh t
+    :save-macros (,name)))
+
+
+(defmacro copy-raw-defun (src dst)
+  `(make-raw-definitions
+    ((setf (symbol-function ',dst)
+           (symbol-function ',src)))
+    :compile nil
+    :fresh t
+    :save-fns (,dst)))
+
+
+(defmacro copy-raw-defmacro (src dst)
+  `(make-raw-definitions
+    ((setf (macro-function ',dst)
+           (macro-function ',src)))
+    :compile nil
+    :fresh t
+    :save-macros (,dst)))
+
+
+(defmacro defvar-raw (&whole form name &optional initial-val doc)
+  (declare (ignore initial-val doc)
+           (xargs :guard (symbolp name)))
+  `(make-raw-definitions
+    ((defvar . ,(cdr form)))
+    :compile nil
+    :fresh t
+    :save-vars (,name)))
+
+
+(defmacro defparameter-raw (&whole form name initial-val &optional doc)
+  (declare (ignore initial-val doc)
+           (xargs :guard (symbolp name)))
+  `(make-raw-definitions
+    ((defparameter . ,(cdr form)))
+    :compile nil
+    :fresh t
+    :save-vars (,name)))
+
+
+(defmacro defconstant-raw (&whole form name initial-val &optional doc)
+  (declare (ignore initial-val doc)
+           (xargs :guard (symbolp name)))
+  `(make-raw-definitions
+    ((defconstant . ,(cdr form)))
+    :compile nil
+    :fresh t
+    :save-vars (,name)))
+
+
+
+(defmacro defstruct-raw (&rest args)
+  (declare (xargs :guard args))
+  (let* ((form (cons 'defstruct args))
+         (name-and-fns (acl2-hacker::defstruct-name-and-fns form)))
+    (if (consp name-and-fns)
+      `(make-raw-definitions
+        (,form)
+        :compile nil
+        :fresh ,name-and-fns
+        :save-fns ,(cdr name-and-fns))
+      `(er hard 'defstruct-raw
+           "Unrecognized defstruct definition form:~%~x0~%"
+           ',form))))
+
+#| ; killed because of OpenMCL issues
+(defun raw-only-definitions1 (revremforms all-forms compile fresh
+                              save-fns save-macros save-vars)
+  (if (endp revremforms)
+    (let* ((fresh-no-dups (remove-duplicates-eql fresh))
+           (main `(make-raw-definitions
+                   ,all-forms
+                   :compile ,compile
+                   :fresh ,fresh-no-dups
+                   :save-fns ,save-fns
+                   :save-macros ,save-macros
+                   :save-vars ,save-vars)))
+      (if (equal fresh-no-dups fresh)
+        main
+        (let ((dups (duplicates fresh)))
+          `(progn (value-triple (cw "Warning: Some names are being defined more than once in raw lisp:~%~x0~%" ',dups))
+                  ,main))))
+    (let ((form (car revremforms))
+          (rst (cdr revremforms)))
+      (cond ((and (consp form)
+                  (eq 'defun (car form))
+                  (>= (len form) 4)
+                  (symbolp (cadr form)))
+             (raw-only-definitions1
+              rst
+              all-forms
+              (cons form compile)
+              (cons (cadr form) fresh)
+              (cons (cadr form) save-fns)
+              save-macros
+              save-vars))
+            ((and (consp form)
+                  (eq 'defmacro (car form))
+                  (>= (len form) 4)
+                  (symbolp (cadr form)))
+             (raw-only-definitions1
+              rst
+              all-forms
+              (cons form compile)
+              (cons (cadr form) fresh)
+              save-fns
+              (cons (cadr form) save-macros)
+              save-vars))
+            ((and (consp form)
+                  (or (eq 'defvar (car form))
+                      (eq 'defparameter (car form)))
+                  (>= (len form) 2)
+                  (symbolp (cadr form)))
+             (raw-only-definitions1
+              rst
+              all-forms
+              compile ; don't compile
+              (cons (cadr form) fresh)
+              save-fns
+              save-macros
+              (cons (cadr form) save-vars)))
+            ((and (consp form)
+                  (eq 'defstruct (car form))
+                  (>= (len form) 2))
+             (let ((name-and-fns (acl2-hacker::defstruct-name-and-fns form)))
+               (if (consp name-and-fns)
+                 (raw-only-definitions1
+                  rst
+                  all-forms
+                  compile ; don't compile
+                  (append name-and-fns fresh)
+                  (append (cdr name-and-fns) save-fns)
+                  save-macros
+                  save-vars)
+                 `(progn! (er soft
+                          'raw-only-definitions
+                          "Unrecognized defstruct definition form:~%~x0~%"
+                          ',form)))))
+            (t
+             `(progn! (er soft
+                          'raw-only-definitions
+                          "Unrecognized raw definition form:~%~x0~%"
+                          ',form)))))))
+
+(defmacro raw-only-definitions (&rest forms)
+  (raw-only-definitions1 (reverse forms) forms nil nil nil nil nil))
+|#
+
+
+(defmacro modify-raw-defun
+  (name name-for-old ll &rest decls-and-body)
+  (declare (xargs :guard (and (symbolp name)
+                              (symbolp name-for-old)
+                              (symbol-listp ll)
+                              (consp decls-and-body))))
+  `(progn (copy-raw-defun ,name ,name-for-old)
+          (make-raw-definitions
+           ((defun ,name ,ll
+              ,@ (and ll `((declare (ignorable . ,ll))))
+              . ,decls-and-body))
+           :compile t
+           :fresh nil
+           :save-fns (,name))))
+
+; tests & stuff:
+#|
+(include-book
+ "defcode" :ttags :all)
+
+(defttag t)
+
+(defstruct-raw foo bar)
+
+(modify-raw-defun foo-bar old-foo-bar (s)
+                  (progn (format t "Foobar!~%")
+                         (old-foo-bar s)))
+
+(set-raw-mode t)
+
+(foo-bar (make-foo :bar 42))
+
+|#
diff --git a/books/hacking/redefun.acl2 b/books/hacking/redefun.acl2
new file mode 100644
index 0000000..73720dd
--- /dev/null
+++ b/books/hacking/redefun.acl2
@@ -0,0 +1,3 @@
+(in-package "ACL2")
+(ld "hacker-pkg.lsp")
+(certify-book "redefun" ? t)
diff --git a/books/hacking/redefun.lisp b/books/hacking/redefun.lisp
new file mode 100644
index 0000000..025c060
--- /dev/null
+++ b/books/hacking/redefun.lisp
@@ -0,0 +1,126 @@
+(in-package "ACL2")
+
+;Needed to use, but not needed for certification:
+;(include-book "defcode" :load-compiled-file :comp :ttags ((defcode)))
+
+(program)
+(set-state-ok t)
+
+; cert_param: (non-acl2r)
+
+
+(defun chk-acceptable-redefun (def ctx wrld state)
+  (er-let*
+   ((tuple (chk-acceptable-defuns (list def) ctx wrld state)))
+   (assert$
+    (equal (length tuple) 23)
+    (let* ((name (car def))
+           (new-wrld (nth 18 tuple))
+           (old-symbol-class
+            (getprop name 'symbol-class 0 'current-acl2-world wrld))
+           (new-symbol-class (nth 15 tuple))
+           (old-formals
+            (getprop name 'formals 0 'current-acl2-world wrld))
+           (new-formals
+            (getprop name 'formals 0 'current-acl2-world new-wrld))
+           (old-stobjs-in
+            (getprop name 'stobjs-in 0 'current-acl2-world wrld))
+           (new-stobjs-in
+            (getprop name 'stobjs-in 0 'current-acl2-world new-wrld))
+           (old-stobjs-out
+            (getprop name 'stobjs-out 0 'current-acl2-world wrld))
+           (new-stobjs-out
+            (getprop name 'stobjs-out 0 'current-acl2-world new-wrld)))
+      (cond ((eql old-symbol-class 0)
+             (er soft ctx "No existing definition: ~x0" name))
+            ((nth 19 tuple) ; non-executablep
+             (er soft ctx
+                 "Please do not redefun a non-executable function.  The ~
+                  offending definition is: ~x0."
+                 def))
+            ((not (eq ':program old-symbol-class))
+             (er soft ctx
+                 "Old definition should have defun-mode :program.  Sorry."))
+            ((not (eq ':program new-symbol-class))
+             (er soft ctx
+                 "New definition should have defun-mode :program.  Sorry."))
+            ((not (equal new-formals old-formals))
+             (er soft ctx
+                 "Please use the same formal parameter list when redefining. ~
+                  Previous formals: ~x0"
+                 old-formals))
+            ((not (equal new-stobjs-in old-stobjs-in))
+             (er soft ctx
+                 "New definition should have the same stobjs-in.Previously, ~
+                  ~x0.  Specified, ~x1."
+                 old-stobjs-in new-stobjs-in))
+            ((not (equal new-stobjs-out old-stobjs-out))
+             (er soft ctx
+                 "New definition should have the same stobjs-out.Previously, ~
+                  ~x0.  Specified, ~x1."
+                 old-stobjs-out new-stobjs-out))
+            (t ; okay
+             (value :invisible)))))))
+
+
+; this is a safer version of doing defun with redefinition allowed.
+;
+; only :program mode functions may be used here, because the intent is to
+; maintain sound reasoning.
+;
+; lots of checks are performed and actions are taken to prevent the logic from
+; being tainted by the redefinition.
+;
+(defmacro redefun (name ll &rest decls-and-body)
+  (declare (xargs :guard (and (symbolp name)
+                              (symbol-listp ll)
+                              (consp decls-and-body))))
+  (let ((def (list* name ll decls-and-body)))
+    `(progn+redef
+      (assert-include-defun-matches-certify-defun ,name)
+      (defcode
+       :loop (er-progn
+              (assert-no-special-raw-definition ,name)
+              (chk-acceptable-redefun ',def
+                                      'redefun
+                                      (w state)
+                                      state)
+              (ensure-program-only-flag ,name)
+              (defun . ,def))
+       :extend
+       (in-raw-mode
+        (defun-*1* ,name ,ll
+                   (if (f-get-global 'safe-mode *the-live-state*)
+                     (throw-raw-ev-fncall (list 'program-only-er ',name
+                                                (list . ,ll) 't '(nil) t))
+                     (,name . ,ll))))
+       :compile
+       (defun . ,def)))))
+
+
+; this uses redefun and our code rewrite stuff (see rewrite-code.lisp,
+; especially compute-copy-defun+rewrite) to redefine a :program mode
+; function in terms of its existing definition.
+;
+(defmacro redefun+rewrite (name &rest rewrite-spec)
+  (declare (xargs :guard (symbolp name)))
+  `(make-event
+    (compute-copy-defun+rewrite
+     ',name ',name ',rewrite-spec 'redefun state)))
+
+
+; tests and stuff
+#|
+(include-book
+ "defcode" :ttags ((defcode)))
+
+(defttag t)
+
+(redefun deflabel-fn (name state doc event-form)
+         (declare (ignore doc event-form))
+         (value name))
+
+(set-guard-checking :none)
+(deflabel moo)
+(deflabel moo)
+|#
diff --git a/books/hacking/rewrite-code-pkg.lsp b/books/hacking/rewrite-code-pkg.lsp
new file mode 100644
index 0000000..be2dc1b
--- /dev/null
+++ b/books/hacking/rewrite-code-pkg.lsp
@@ -0,0 +1,14 @@
+(defpkg "REWRITE-CODE"
+        (append
+         ; "imports":
+         '(value er-let* er-decode-logical-name getprop current-acl2-world
+           stobjs-in cltl-command global-value soft)
+         ; "exports":
+         '(er-rewrite-form
+           get-defun
+           compute-copy-defun+rewrite
+           assert-include-defun-matches-certify-defun
+           copy-defun+rewrite
+           copy-defun)
+         (union-eq *acl2-exports*
+                   *common-lisp-symbols-from-main-lisp-package*)))
\ No newline at end of file
diff --git a/books/hacking/rewrite-code.acl2 b/books/hacking/rewrite-code.acl2
new file mode 100644
index 0000000..fad19c7
--- /dev/null
+++ b/books/hacking/rewrite-code.acl2
@@ -0,0 +1,3 @@
+(in-package "ACL2")
+(ld "rewrite-code-pkg.lsp")
+(certify-book "rewrite-code" ? t)
diff --git a/books/hacking/rewrite-code.lisp b/books/hacking/rewrite-code.lisp
new file mode 100644
index 0000000..2b52c09
--- /dev/null
+++ b/books/hacking/rewrite-code.lisp
@@ -0,0 +1,751 @@
+(in-package "REWRITE-CODE")
+
+(program)
+(set-state-ok t)
+
+; recognizer for ``augmented naturals'', which include 'inf as infinity
+(defun aug-natp (x)
+  (or (natp x)
+      (equal x 'inf)))
+
+; < relation for ``augmented naturals''
+(defun aug-nat-< (x y)
+  (and (not (eq x 'inf))
+       (or (eq y 'inf)
+           (< x y))))
+
+; decrement function for ``augmented naturals''
+(defun aug-nat-dec (x)
+  (cond ((eq x 'inf) 'inf)
+        ((zp x) 0)
+        (t (1- x))))
+
+; recognizer for intervals over ``augmented naturals''
+(defun multiplicity-rangep (x)
+  (or (null x) ; empty range
+      (and (consp x)
+           (aug-natp (car x))
+           (aug-natp (cdr x))
+           (not (aug-nat-< (cdr x) (car x))))))
+
+; decrement function for intervals over ``augmented naturals''
+(defun multiplicity-range-dec (x)
+  (if (or (endp x) (equal (cdr x) 0))
+    nil ; empty range
+    (cons (aug-nat-dec (car x))
+          (aug-nat-dec (cdr x)))))
+
+
+; prepend the reverse of one list onto another
+(defun rev-prepend (torev onto)
+  ; (declare (xargs :guard (and (true-listp torev) (true-listp onto))))
+  (if (endp torev)
+    onto
+    (rev-prepend (cdr torev) (cons (car torev) onto))))
+
+
+; n times, pops an element from ,from and pushes it on ,to
+(defun pop-push-n (n from to)
+  (if (or (zp n)
+          (endp from))
+    (mv from to)
+    (pop-push-n (1- n) (cdr from) (cons (car from) to))))
+
+
+; update an entry in an alist, or add it to the end
+(defun update-alist (key val lst)
+  (cond ((endp lst)
+         (list (cons key val)))
+        ((and (consp (car lst))
+              (equal (caar lst) key))
+         (cons (cons key val)
+               (cdr lst)))
+        (t
+         (cons (car lst)
+               (update-alist key val (cdr lst))))))
+
+
+; replaces occurances in ,expr of the symbols that are keys in ,assn-alist
+; with their bindings in ,assn-alist.
+;
+(defun replace-assns (expr assn-alist)
+  ;(declare (xargs :guard (symbol-alistp assn-alist)))
+  (if (consp expr)
+    (cons (replace-assns (car expr) assn-alist)
+          (replace-assns (cdr expr) assn-alist))
+    (if (symbolp expr)
+      (let ((assn (assoc-eq expr assn-alist)))
+        (if (consp assn)
+          (cdr assn)
+          expr))
+      expr)))
+
+
+; ,a1 and ,a2 are each assumed an alist with no keys duplicated.  if the keys
+; don't overlap between ,a1 and ,a2 or they agree on all the bindings, the
+; "union" is returned.  if they disagree on any bindings, ,t is returned.
+;
+(defun merge-matches (a1 a2)
+  (cond ((endp a1)
+         a2)
+        ((endp a2)
+         a1)
+        (t
+         (let* ((sym (caar a1))
+                (binding2 (assoc-eq sym a2)))
+           (if (consp binding2)
+             (let ((val1 (cdar a1))
+                   (val2 (cdr binding2)))
+               (if (equal val1 val2)
+                 (merge-matches (cdr a1) a2)
+                 t))
+             (merge-matches (cdr a1) (cons (car a1) a2)))))))
+
+
+; returns (smallest) assn-alist satisfying
+;   (equal (replace-assns pat assn-alist) expr)
+; if one exists.  otherwise, returns t (indicating, roughly, that
+; no assignments to ,vars in ,pat generate ,expr)
+;
+(defun match-pattern (expr pat vars)
+  ;(declare (xargs :guard (symbol-listp vars)))
+  (cond ((member-eq pat vars)
+         (list (cons pat expr)))
+        ((and (consp pat)
+              (consp expr))
+         (let ((car-result (match-pattern (car expr) (car pat) vars))
+               (cdr-result (match-pattern (cdr expr) (cdr pat) vars)))
+           (if (or (equal car-result t) (equal cdr-result t))
+             t ; bad match
+             (merge-matches car-result cdr-result))))
+        ((equal pat expr)
+         ())
+        (t
+         t) ; bad match
+        ))
+
+; predicates for the parsed pieces of a rewrite-spec, a rewrite-def and its
+; constituent pieces
+(mutual-recursion
+ (defun rewrite-defp (v) ; a list (sequenced) of lists (simultaneous)
+   (declare (xargs :measure (acl2-count v)
+                   :hints (("Goal"
+                            :in-theory (disable
+                                        (:definition multiplicity-rangep))))))
+   (or (null v)
+       (and (consp v)
+            (rewrite-simul-defp (car v))
+            (rewrite-defp (cdr v)))))
+ (defun rewrite-simul-defp (v) ; a list (simultaneous) of entries
+   (declare (xargs :measure (acl2-count v)))
+   (or (null v)
+       (and (consp v)
+            (rewrite-entryp (car v))
+            (rewrite-simul-defp (cdr v)))))
+ (defun rewrite-entryp (v)
+   (declare (xargs :measure (acl2-count v)))
+   (and (consp v)
+        (multiplicity-rangep (car v)) ; global
+        (consp (cdr v))
+        (rewrite-var-entry-lstp (cadr v)) ; no binding -> recursive
+        (consp (cddr v))
+        (symbol-listp (caddr v)) ; vars
+        (consp (cdddr v))
+        ; (cadddr v) is pat
+        ; (cddddr v) is repl
+        ))
+ (defun rewrite-var-entry-lstp (v) ; var -> rewrite-def alist
+   (declare (xargs :measure (acl2-count v)))
+   (or (null v)
+       (and (consp v)
+            (rewrite-var-entryp (car v))
+            (rewrite-var-entry-lstp (cdr v)))))
+ (defun rewrite-var-entryp (v) ; ( var . rewrite-def )
+   (declare (xargs :measure (acl2-count v)))
+   (and (consp v)
+        (symbolp (car v))
+        (rewrite-defp (cdr v)))))
+
+; some accessors
+(defmacro entry-multrng (v) `(car ,v))
+(defmacro entry-alist   (v) `(cadr ,v))
+(defmacro entry-vars    (v) `(caddr ,v))
+(defmacro entry-pat     (v) `(cadddr ,v))
+(defmacro entry-repl    (v) `(cddddr ,v))
+
+; some modifiers
+(defun    dec-entry     (v)
+  (cons (multiplicity-range-dec (car v))
+        (cdr v)))
+(defun update-entry-alist (v alist)
+  (cons (car v)
+        (cons alist
+              (cddr v))))
+(defun update-entry-alist-entry (v var def)
+  (update-entry-alist v (update-alist var def (entry-alist v))))
+
+; the guts of code rewriting
+(mutual-recursion
+ (defun rewrite-seq (form seq-from seq-to)
+   (declare (xargs :guard (and (rewrite-defp seq-from)
+                               (rewrite-defp seq-to))))
+   (if (consp seq-from)
+     (mv-let (form updated)
+             (rewrite-simul form (car seq-from) nil)
+             (rewrite-seq form (cdr seq-from) (cons updated seq-to)))
+     (mv form (reverse seq-to))))
+ (defun rewrite-simul (form simul-from simul-to)
+   (declare (xargs :guard (and (rewrite-simul-defp simul-from)
+                               (rewrite-simul-defp simul-to))))
+   (if (consp simul-from)
+     (let* ((entry (car simul-from))
+            (assns-opt (match-pattern form
+                                      (entry-pat entry)
+                                      (entry-vars entry))))
+       (if (eq 't assns-opt)
+         ; no match
+         (rewrite-simul form
+                        (cdr simul-from)
+                        (cons entry simul-to))
+         ; match!
+         (let* ((entry (dec-entry entry))
+                (simul-from (cons entry (cdr simul-from)))
+                (idx (len simul-to)))
+           (rewrite-assns (entry-repl entry)
+                          assns-opt
+                          idx
+                          (rev-prepend simul-to simul-from)))))
+     ;; no more rules to try
+     (let ((simul-all (reverse simul-to)))
+       (if (consp form)
+         ;; descend
+         (mv-let (car-form simul-all)
+                 (rewrite-simul (car form) simul-all nil)
+                 (mv-let (cdr-form simul-all)
+                         (rewrite-simul (cdr form) simul-all nil)
+                         (mv (cons car-form cdr-form) simul-all)))
+         (mv form simul-all)))))
+ (defun rewrite-assns (repl assns entry-idx simul-all)
+   (declare (xargs :guard (and (rewrite-simul-defp simul-all)
+                               (natp entry-idx)
+                               (< entry-idx (len simul-all))
+                               (symbol-alistp assns))))
+   (cond ((consp repl)
+          (mv-let (car-form simul-all)
+                  (rewrite-assns (car repl) assns entry-idx simul-all)
+                  (mv-let (cdr-form simul-all)
+                          (rewrite-assns (cdr repl) assns entry-idx simul-all)
+                          (mv (cons car-form cdr-form) simul-all))))
+         ((symbolp repl)
+          (let ((assn-opt (assoc-eq repl assns)))
+            (if (consp assn-opt)
+              (let* ((form (cdr assn-opt))
+                     (entry (nth entry-idx simul-all))
+                     (non-rec-defs (entry-alist entry))
+                     (non-rec-def-opt (assoc-eq repl non-rec-defs)))
+                (if (consp non-rec-def-opt)
+                  ; some non-recursive specification
+                  (mv-let (form updated-def)
+                          (rewrite-seq form (cdr non-rec-def-opt) nil)
+                          (mv form (update-nth entry-idx
+                                               (update-entry-alist-entry entry
+                                                                         repl
+                                                                         updated-def)
+                                               simul-all)))
+                  ; no non-rec-def => recursively apply simul-all
+                  (if (and (symbolp (entry-pat entry))
+                           (member-eq (entry-pat entry) (entry-vars entry)))
+                    ; illegal recursive rewrite that matches everything.
+                    ; for now, we'll just break the recursion.
+                    (mv form simul-all)
+                    ; text to match against getting smaller =>
+                    ;   recursively apply simul-all
+                    (rewrite-simul form simul-all nil))))
+              (mv repl simul-all))))
+         (t
+          (mv repl simul-all)))))
+
+; code for checking that the multiplicities allow zero.  used after they have
+; been decremented as many times as they have been used.
+(mutual-recursion
+ (defun assert-zero-allowed-def (v state)
+   (if (endp v)
+     state
+     (pprogn
+      (assert-zero-allowed-simul-def (car v) state)
+      (assert-zero-allowed-def (cdr v) state))))
+ (defun assert-zero-allowed-simul-def (v state)
+   (if (endp v)
+     state
+     (pprogn
+      (assert-zero-allowed-entry (car v) state)
+      (assert-zero-allowed-simul-def (cdr v) state))))
+ (defun assert-zero-allowed-entry (v state)
+   (if (or (endp v) (endp (cdr v)))
+     state
+     (let ((rng (car v))
+           (var-entries (cadr v)))
+       (pprogn
+        (if (or (endp rng) (not (equal (car rng) 0)))
+          ; zero not allowed
+          (pprogn
+           (acl2::f-put-global 'erp t state)
+           (fms (if (endp rng)
+                "Code rewrite entry used too many times:~%  ~xp -> ~xr~%"
+                "Code rewrite entry used too few times (at least ~xn applications remaining):~%  ~xp -> ~xr~%")
+              `((#\p . ,(entry-pat  v))
+                (#\r . ,(entry-repl v))
+                (#\n . ,(and (consp rng) (car rng))))
+              (standard-co state)
+              state
+              (acl2::abbrev-evisc-tuple state)))
+          ; ok
+          state)
+        (assert-zero-allowed-entry-lst var-entries state)))))
+ (defun assert-zero-allowed-entry-lst (v state)
+   (if (endp v)
+     state
+     (pprogn
+      (assert-zero-allowed-var-entry (car v) state)
+      (assert-zero-allowed-entry-lst (cdr v) state))))
+ (defun assert-zero-allowed-var-entry (v state)
+   (if (endp v)
+     state
+     (assert-zero-allowed-def (cdr v) state))))
+
+(defun er-if-zero-not-allowed-def (def state)
+  (acl2::state-global-let*
+   ((erp nil))
+   (pprogn
+    (assert-zero-allowed-def def state)
+    (mv (@ erp) :invisible state))))
+
+(defun rewrite-fn (form def state)
+  (if (not (rewrite-defp def))
+    (er acl2::soft 'rewrite "Code rewrite definition illegal:~%~x0" def)
+    (mv-let (result new-def)
+            (rewrite-seq form def nil)
+            (er-progn
+             (er-if-zero-not-allowed-def new-def state)
+             (acl2::value result)))))
+
+#|
+(rewrite-fn '(a b (c (c d)) (x c v))
+            '((((0 . 2) ((%)) (%) (c . %) . (f . %))))
+            state)
+|#
+
+; now i build up a more convenient specification language
+
+; first, instead of always (n . m) as range, we also allow
+; + == (1 . inf)
+; * == (0 . inf)
+; n == (n . n)
+
+; predicate for new multiplicity specs
+(defun multiplicity-specp (x)
+  (declare (xargs :guard t))
+  (or (and (multiplicity-rangep x)
+           (not (equal (car x) 'inf)))
+      (equal x '*)
+      (equal x '+)
+      (natp x)))
+
+(defun multiplicity-spec-to-noninf-range (x)
+  (declare (xargs :guard (multiplicity-specp x)))
+  (cond ((and (multiplicity-rangep x)
+              (not (equal (car x) 'inf)))
+         x)
+        ((equal x '*) '(0 . inf))
+        ((equal x '+) '(1 . inf))
+        ((natp x) (cons x x))
+        (t nil) ; invalid / unrecognized
+        ))
+
+
+; now we build up some macros that build rewrite-defs from a more natural,
+; flexible specification language.
+
+; roughly speaking, entries/rules consist of some pieces:
+;   :pat  = "pattern" to match   or  :carpat = pattern that must be in a car
+;   :repl = "replacement" to put in place of pattern (defaults to the pattern)
+;   :vars = "variables" = a list of symbols that should not be taken
+;           literally in the pattern, but can stand for any substructure
+;   :recvars = "recursive variables" = like :vars but the current rules also
+;           get applied to what these variables match
+;   :mult = "multiplicity" = an assertion on how many applications of this
+;           rule are to be made.  (violation results in post facto error)
+;
+; entries can be combined using "simultaneous" combination:
+;   (:simul e1 e2 e3)
+; to indicate that at each step in our pre-order search we attempt to match
+; e1, then e2, then e3.  if no matches, we go deeper.
+;
+; entries and/or :simul combinations can be combined with "sequences":
+;   (:seq s1 s2 s3)
+; to indicate that we apply s1 to our form, apply that result to s1, and
+; apply that result to s3.
+
+; syntax more precisely:
+; above relevant functions, i have kind-of a BNF for the language.  the
+; parentheses and dots are required cons structure.  symbols are also
+; matched literally, unless they are surrounded with _ _.  items in [] are
+; optional, with a default value given after an =.  ... is a postfix shorthand
+; for 0 or more of something.
+
+; to the right is an indication of what is shorthand for what.  if something
+; is canonical, "(canonical)" appears, meaning it should be pretty obvious
+; how this maps to the lower level structure, if you understand it.  ;)
+
+; _def_ ::= ()                          => (:seq)
+;         | (_def_)                     => _def_
+;         | (:seq _simul-def_...)       (canonical)
+;         | _simul-def_                 => (:seq _simul-def_)
+
+(defmacro quote-rewrite-def (&rest v)
+  (cond
+   ((endp v)
+    ''nil)
+   ((and (consp (car v))
+         (null (cdr v)))
+    `(quote-rewrite-def . ,(car v)))
+   ((eq ':seq (car v))
+    `(quote-rewrite-def-rest . ,(cdr v)))
+   (t
+    `(list (quote-rewrite-simul-def . ,v)))))
+
+(defmacro quote-rewrite-def-rest (&rest v)
+  (if (endp v)
+    ''nil
+    `(cons
+      (quote-rewrite-simul-def . ,(car v))
+      (quote-rewrite-def-rest . ,(cdr v)))))
+
+; _simul-def_ ::= ()                       => (:simul)
+;               | (:simul _entry_...)      (canonical)
+;               | _entry_                  => (:simul _entry_)
+
+(defmacro quote-rewrite-simul-def (&rest v)
+  (cond
+   ((endp v)
+    ''nil)
+   ((eq ':simul (car v))
+    `(quote-rewrite-simul-def-rest . ,(cdr v)))
+   (t
+    `(list (quote-rewrite-entry . ,v)))))
+
+(defmacro quote-rewrite-simul-def-rest (&rest v)
+  (if (endp v)
+    ''nil
+    `(cons
+      (quote-rewrite-entry . ,(car v))
+      (quote-rewrite-simul-def-rest . ,(cdr v)))))
+
+; some stuff for entries
+(defun namep (v)
+  (and (symbolp v)
+       (not (null v))
+       (not (keywordp v))))
+
+; _var-spec_ ::= ()                                (canonical)
+;              | _name_                            => ((_name_))
+;              | (_name_ . _var-spec_)             => ((_name_) . _var-spec_)
+;              | ((_name_ . _def_) . _var-spec_)   (canonical)
+
+(defun var-specp (v)
+  (or (null v)
+      (namep v)
+      (and (consp v)
+           (or (namep (car v))
+               (and (consp (car v))
+                    (namep (caar v))))
+           (var-specp (cdr v)))))
+
+; _recvar-spec_ ::= ()                             (canonical)
+;                 | _name_                         => (_name_)
+;                 | (_name_ . _var-spec_)          (canonical)
+
+(defun recvar-specp (v)
+  (or (null v)
+      (namep v)
+      (and (consp v)
+           (namep (car v))
+           (recvar-specp (cdr v)))))
+
+(defun get-var-names (var-spec)
+  (if (consp var-spec)
+    (cons (if (consp (car var-spec))
+            (caar var-spec)
+            (car var-spec))
+          (get-var-names (cdr var-spec)))
+    (if (null var-spec)
+      nil
+      (list var-spec))))
+
+(defun canonicalize-var-bindings (var-spec)
+  (if (consp var-spec)
+    (cons (if (consp (car var-spec))
+            (car var-spec)
+            (list (car var-spec)))
+          (canonicalize-var-bindings (cdr var-spec)))
+    (if (null var-spec)
+      nil
+      (list (list var-spec)))))
+
+; _entry_ ::= (:pat _pat_                     (canonical)
+;              [:repl _repl_=_pat_]
+;              [:mult _mult_=*]
+;              [:vars _var-spec_=()]
+;              [:recvars _recvar-spec_=()])
+;           | (:carpat _pat_                  => (:pat  (_pat_  . %cdr%)
+;              [:repl _repl_=_pat_]               :repl (_repl_ . %cdr%)
+;              [:mult _mult_=*]                :recvars (%cdr% . _recvar-spec_)
+;              [:vars _var-spec_=()]           :vars _var-spec_ :mult _mult_)
+;              [:recvars _recvar-spec_=()])
+
+(defmacro quote-rewrite-entry (&key (pat '() patp)
+                                    (carpat '() carpatp)
+                                    (repl '() replp)
+                                    (mult '*)
+                                    (vars '())
+                                    (recvars '()))
+  (declare (xargs :guard (and (multiplicity-specp mult)
+                              (var-specp vars)
+                              (recvar-specp recvars)
+                              (not (and patp carpatp))
+                              (or (and patp
+                                       (not (member pat (get-var-names recvars))))
+                                  (and carpatp
+                                       (not (member carpat (get-var-names recvars)))))
+                              (not (intersectp-eq (get-var-names vars)
+                                                  (get-var-names recvars))))))
+  (let* ((cdrvar '%cdr-reserved%)
+         (nrcvar-names (get-var-names vars))
+         (recvar-names (append (if carpatp (list cdrvar) '())
+                               (get-var-names recvars)))
+         (var-names (append nrcvar-names recvar-names))
+         (pat (if patp
+                pat
+                (cons carpat cdrvar)))
+         (repl (if replp
+                 (if carpatp
+                   (cons repl cdrvar)
+                   repl)
+                 pat)))
+    `(list* ',(multiplicity-spec-to-noninf-range mult)
+            (quote-rewrite-var-entry-lst . ,(canonicalize-var-bindings vars))
+            ',var-names
+            ',pat
+            ',repl)))
+
+; see _var-spec_ above
+
+(defmacro quote-rewrite-var-entry-lst (&rest bindings)
+  (if (endp bindings)
+    ''nil
+    `(cons (quote-rewrite-var-entry ,(car bindings))
+           (quote-rewrite-var-entry-lst . ,(cdr bindings)))))
+
+(defmacro quote-rewrite-var-entry (v)
+  (declare (xargs :guard (and (consp v)
+                              (namep (car v)))))
+  `(cons ',(car v)
+         (quote-rewrite-def . ,(cdr v))))
+
+
+
+; and now to put the more convenient language on top of the code rewriting:
+
+; for "export"
+(defmacro er-rewrite-form (form &rest def)
+  `(rewrite-fn
+    ,form
+    (quote-rewrite-def . ,def)
+    state))
+
+
+
+; EXAMPLES, for understanding the semantics more precisely:
+#|
+ACL2 !>(er-rewrite-form 'a)
+ A
+ACL2 !>(er-rewrite-form 'a (:pat a :repl b))
+ B
+ACL2 !>(er-rewrite-form 'a (:seq (:pat a :repl b) (:pat b :repl c)))
+ C
+ACL2 !>(er-rewrite-form '(a . b) (:seq (:pat a :repl b) (:pat b :repl c)))
+ (C . C)
+ACL2 !>(er-rewrite-form '(a . b) (:simul (:pat a :repl b) (:pat b :repl c)))
+ (B . C)
+ACL2 !>(er-rewrite-form '(b . a) (:simul (:pat a :repl b) (:pat b :repl c)))
+ (C . B)
+ACL2 !>(er-rewrite-form '(+ (fn1 42) (fn1 53))
+                        (:pat (fn1 %) :repl (fn2 %) :vars (%)))
+ (+ (FN2 42) (FN2 53))
+ACL2 !>(er-rewrite-form '(+ (fn1 42) (fn1 53))
+                        (:pat (fn1 %) :repl (fn2 %) :vars %))
+ (+ (FN2 42) (FN2 53))
+ACL2 !>(er-rewrite-form '(+ (fn1 (fn1 42)) (fn1 53))
+                        (:pat (fn1 %) :repl (fn2 %) :vars %))
+ (+ (FN2 (FN1 42)) (FN2 53))
+ACL2 !>(er-rewrite-form '(+ (fn1 (fn1 42)) (fn1 53))
+                        (:pat (fn1 %) :repl (fn2 %) :recvars %))
+ (+ (FN2 (FN2 42)) (FN2 53))
+ACL2 !>(er-rewrite-form '(+ (stuff fn1 42) (fn1 42))
+                        (:pat (fn1 %) :repl (fn2 %) :vars %))
+ (+ (STUFF FN2 42) (FN2 42))
+ACL2 !>(er-rewrite-form '(+ (stuff fn1 42) (fn1 42))
+                (:pat ((fn1 %1) . %2) :repl ((fn2 %1) . %2) :vars (%1 %2)))
+ (+ (STUFF FN1 42) (FN2 42))
+ACL2 !>(er-rewrite-form '(+ (stuff fn1 42) (fn1 42) (fn1 53))
+                (:pat ((fn1 %1) . %2) :repl ((fn2 %1) . %2) :vars (%1 %2)))
+ (+ (STUFF FN1 42) (FN2 42) (FN1 53))
+ACL2 !>(er-rewrite-form '(+ (stuff fn1 42) (fn1 42) (fn1 53))
+                (:pat ((fn1 %1) . %2) :repl ((fn2 %1) . %2) :recvars (%1 %2)))
+ (+ (STUFF FN1 42) (FN2 42) (FN2 53))
+
+|#
+; this demonstrates that in order to rewrite a function call in a more
+; robust way, we should do
+;   (:pat  ((old-fn . %params%) . %cdr%)
+;    :repl ((new-fn . %params%) . %cdr%)
+;    :vars %params%  :recvars %cdr%)
+; rather than
+;   (:pat  (old-fn . %params%)
+;    :repl (new-fn . %params%)
+;    :vars %params%)
+; but if we do it this way, will we match a function called in the
+; top level of a function?  consider (defun x (v) (y v)).  rather than
+; rewriting (y v) at the top level, we shall rewrite ((y v)), which is the
+; last cons of the defun.  we will use this below in
+; compute-copy-defun+rewrite.
+;
+; however, we offer :carpat as a shortcut for such specifications.  the
+; following are equivalent:
+#|
+ACL2 !>(er-rewrite-form '(+ (stuff fn1 42) (fn1 42) (fn1 53))
+                (:pat ((fn1 %1) . %2) :repl ((fn2 %1) . %2) :recvars (%1 %2)))
+ (+ (STUFF FN1 42) (FN2 42) (FN2 53))
+ACL2 !>(er-rewrite-form '(+ (stuff fn1 42) (fn1 42) (fn1 53))
+                (:carpat (fn1 %1) :repl (fn2 %1) :recvars %1))
+ (+ (STUFF FN1 42) (FN2 42) (FN2 53))
+|#
+
+; also, note that I, by convention, wrap my variables in %% to make them
+; stand out.  but any non-keyword, non-nil symbol can be a variable.
+
+
+; and now we want to support rewriting function definitions:
+
+; for "export"
+;
+; looks up a function definition, returning it in an error triple
+(defun get-defun (name state)
+  (let*
+   ((ev-wrld (acl2::decode-logical-name name (w state)))
+    (cltl-command
+     (and ev-wrld
+          (let ((cltl-cmd (getprop 'cltl-command 'global-value
+                                   nil 'current-acl2-world ev-wrld)))
+            (and (consp cltl-cmd)
+                 (equal (car cltl-cmd) 'defuns)
+                 (= (len cltl-cmd) 4)
+                 cltl-cmd)))))
+   (and cltl-command
+        (let* ((mode (second cltl-command))
+               (defuns-body (fourth cltl-command))
+               (ll (cadr defuns-body))
+               (tail (cddr defuns-body))
+               (stobjs (remove nil (getprop name 'stobjs-in
+                                            nil 'current-acl2-world ev-wrld)))
+               (dec `(declare (xargs :mode ,mode
+                                     :stobjs ,stobjs))))
+           `(defun ,name ,ll ,dec . ,tail)))))
+
+
+; for "export"
+;
+; compute the ,defun-like event to execute if we want to define ,dst to be
+; like ,src except for rewriting the code according to ,rwdef.
+;
+; ,src and ,dst may certainly be the same
+;
+; as mentioned above, ,rwdef is applied to the body in a singleton list;
+; e.g. (defun x (v) (y v)) applies rwdef to ((y v)), so if we want to, for
+; example, put a let around the body, we would use either
+;  (:pat (%body%)
+;   :repl ((let (...) %body%))
+;   :vars %body%)
+; or
+;  (:pat %bodycons%
+;   :repl ((let (...) . %bodycons%))  ; notice the dot!
+;   :vars %bodycons%)
+; or
+;  (:carpat %body%
+;   :repl (let (...) %body%)
+;   :vars %body%)
+(defun compute-copy-defun+rewrite (src dst rwdef defun-like state)
+  (if (and (null rwdef) (eq src dst))
+    (value '(value-triple :nothing-to-do))
+    (let*
+     ((src-defun (get-defun src state)))
+     (if src-defun
+       (value
+        (let* ((tuple (cddr src-defun)) ; remove 'defun and name
+               (bodycons (last tuple))
+               (tuple-no-body (butlast tuple 1)))
+          (if (null rwdef)
+            (list* defun-like dst tuple)
+            `(make-event
+              (er-let* ((b2 (er-rewrite-form ',bodycons . ,rwdef)))
+                (value `(,',defun-like ,',dst ,@',tuple-no-body . ,b2)))))))
+       (er soft 'compute-copy-defun+rewrite
+           "Illegal or missing defun for ~x0." src)))))
+
+
+; for "export"
+;
+; asserts that the definition of a function at certify-book time
+; time matches that at include-book time.  this is an extra check that
+; can be useful in the presence of redefinitions.
+(defmacro assert-include-defun-matches-certify-defun (name)
+  (declare (xargs :guard (symbolp name)))
+  `(make-event
+    `(acl2::assert-event
+      (let ((certify-time-defun ',(get-defun ',name state))
+            (include-time-defun (get-defun ',',name state)))
+        (or (equal certify-time-defun include-time-defun)
+            (cw "Certify time def: ~x0~%Include time def: ~x1~%"
+                certify-time-defun include-time-defun)))
+      :on-skip-proofs t)))
+
+
+
+; for "export"
+;
+; defun ,dst to be like ,src except for rewriting the code according to
+; ,rewrite-spec
+;
+; ,src and ,dst may be the same (if redefinition allowed)
+;
+; see compute-copy-defun+rewrite for more info
+;
+(defmacro copy-defun+rewrite (src dst &rest rewrite-spec)
+  (declare (xargs :guard (and (symbolp src)
+                              (symbolp dst))))
+  `(progn
+    (assert-include-defun-matches-certify-defun ,src)
+    (make-event (compute-copy-defun+rewrite
+                 ',src ',dst ',rewrite-spec 'defun state))))
+
+
+; for "export"
+;
+; defun ,dst to be like ,src
+;
+; ,src and ,dst may be the same (if redefinition allowed)
+;
+; see compute-copy-defun+rewrite for more info
+;
+(defmacro copy-defun (src dst)
+  `(copy-defun+rewrite ,src ,dst))
diff --git a/books/hacking/subsumption.acl2 b/books/hacking/subsumption.acl2
new file mode 100644
index 0000000..5c7e7b2
--- /dev/null
+++ b/books/hacking/subsumption.acl2
@@ -0,0 +1,3 @@
+(in-package "ACL2")
+(ld "hacker-pkg.lsp")
+(certify-book "subsumption" ? t)
diff --git a/books/hacking/subsumption.lisp b/books/hacking/subsumption.lisp
new file mode 100644
index 0000000..38cda92
--- /dev/null
+++ b/books/hacking/subsumption.lisp
@@ -0,0 +1,189 @@
+(in-package "ACL2")
+(include-book "doc-section")
+
+;Needed to use, but not needed for certification:
+;(include-book "defcode" :load-compiled-file :comp :ttags ((defcode)))
+
+(program)
+(set-state-ok t)
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; subsumption of ttags based on what's been done
+;
+; this should only be used in subsuming hacker stuff, like so:
+;
+#|
+(include-book
+ "hacker/hacker")
+(progn+all-ttags-allowed ; see hacker.lisp
+ (include-book
+  "hacker/all" :ttags ((defcode) (table-guard))))
+(subsume-ttags-since-defttag)
+|#
+;
+
+(defun acl2-hacker::ttags-seen-at-defttag (name path wrld last)
+  (if (endp wrld)
+    (er hard 'subsume-ttags-since-defttag
+        "Error retrieving old ttags-seen.")
+    (if (and (consp (car wrld))
+             (eq 'ttags-seen (caar wrld))
+             (consp (cdar wrld))
+             (eq 'global-value (cadar wrld)))
+      (let ((c (assoc-eq name (cddar wrld))))
+        (if (and (consp c)
+                 (member-equal path (cdr c)))
+          (acl2-hacker::ttags-seen-at-defttag name  path
+                                              (cdr wrld) (cddar wrld))
+          last))
+      (acl2-hacker::ttags-seen-at-defttag name path (cdr wrld) last))))
+
+(defun acl2-hacker::ttags-seen-at-current-defttag (state)
+  (let ((wrld (w state)))
+    (acl2-hacker::ttags-seen-at-defttag (ttag wrld)
+                                        (active-book-name wrld state)
+                                        wrld
+                                        (global-val 'ttags-seen wrld))))
+
+
+(defmacro subsume-ttags-since-defttag ()
+  '(defcode
+     :loop
+     (progn!=touchable
+      :fns install-event
+      (let ((original-ttags-seen
+             (acl2-hacker::ttags-seen-at-current-defttag state))
+            (current-ttags-seen
+             (global-val 'ttags-seen (w state))))
+        (if (equal original-ttags-seen
+                   current-ttags-seen)
+          (value :redundant)
+          (install-event ':invisible
+                         '(subsume-ttags-since-defttag)
+                         'subsume-ttags-since-defttag
+                         0
+                         nil
+                         nil
+                         nil
+                         'subsume-ttags-since-defttag
+                         (putprop 'ttags-seen
+                                  'global-value
+                                  original-ttags-seen
+                                  (w state))
+                         state))))))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; progn-based subsumption of ttags
+;
+
+(push-untouchable saved-ttags-seen nil)
+(push-untouchable saved-ttag nil)
+
+(defmacro restore-ttags-seen ()
+  '(progn!-with-bindings
+    ((temp-touchable-fns
+      '(install-event)
+      set-temp-touchable-fns))
+    (if (implies (boundp-global 'saved-ttags-seen state)
+                 (equal (@ saved-ttags-seen)
+                        (global-val 'ttags-seen (w state))))
+      (stop-redundant-event '(restore-ttags-seen) state)
+      (install-event ':invisible
+                     '(restore-ttags-seen)
+                     'restore-ttags-seen
+                     0
+                     nil
+                     nil
+                     nil
+                     'restore-ttags-seen
+                     (putprop 'ttags-seen
+                              'global-value
+                              (@ saved-ttags-seen)
+                              (w state))
+                     state))))
+
+(defmacro progn!+subsume-ttags (ttag-spec &rest form-lst)
+  `(progn!-with-bindings
+    ((progn!+subsume-ttags_saved-ttv (@ temp-touchable-vars))
+     (temp-touchable-vars '(ttags-allowed
+                            saved-ttag
+                            saved-ttags-seen)
+                          set-temp-touchable-vars))
+    (progn!-with-bindings
+     ((ttags-allowed (@ ttags-allowed))
+      (saved-ttags-seen (global-val 'acl2::ttags-seen (w state)))
+      (saved-ttag (ttag (w state))))
+     (progn!
+      (defcode
+        :loop
+        ((er-let*
+           ((ttags (chk-well-formed-ttags ',ttag-spec
+                                          (cbd)
+                                          'progn!+subsume-ttags
+                                          state)))
+           (assign ttags-allowed ttags))
+         (set-temp-touchable-vars (@ progn!+subsume-ttags_saved-ttv) state)))
+      ,@ form-lst
+      (defcode
+        :loop
+        ((if (eq (@ saved-ttag) (ttag (w state)))
+           (value :invisible)
+           (er soft 'progn!+subsume-ttags
+               "Please do not change the currently active ttag within the ~
+                body of ~x0." 'progn!+subsume-ttags))
+         (restore-ttags-seen)))))))
+
+; for export
+(defmacro progn+subsume-ttags (ttag-spec &rest form-lst)
+
+;;; This legacy doc string was replaced Nov. 2014 by a corresponding
+;;; auto-generated defxdoc form in file hacking-xdoc.lisp.
+
+; ":Doc-Section hacker
+;
+; execute some events, subsuming the specified ttags with the current ttag.~/
+
+; ~bv[]
+; Example:
+; (progn+subsume-ttags
+;   ((:foo) (:bar))
+;   (include-book
+;    \"foo\" :ttags ((:foo)))
+;   (include-book
+;    \"bar\" :ttags ((:bar))))
+; ~ev[] ~/
+;
+; This is like ~ilc[progn] except that the first argument is a
+; ttag-spec (~l[defttag]) to be authorized within the constituent
+; events and then subsumed.  That is, an active ttag is required
+; to use this form and that ttag is (first) used to allow the use of other
+; ttags that may not already be authorized and (second) used to wipe
+; the record that any extra ttags were used.  This is what is meant by
+; subsumption.  If my book requires a ttag, I can then use this to
+; include other books/forms requiring other ttags without those others
+; needing specific prior authorization.
+;
+; An active ttag is required to use this form (~l[defttag]).
+; ~/"
+  `(progn!+subsume-ttags ,ttag-spec
+                         (progn . ,form-lst)))
+
+
+#|; some tests
+(include-book
+ "defcode" :ttags ((defcode)))
+(defttag test1)
+(acl2::ttags-seen)
+(progn+subsume-ttags
+ :all
+ (defttag test2)
+ (progn+touchable :all
+                  (defun foo (x) (1+ x)))
+ (progn! (cw "Hi!~%"))
+ (defttag test1))
+(ttag (w state))
+(acl2::ttags-seen)
+;|#
+
diff --git a/books/hacking/table-guard.acl2 b/books/hacking/table-guard.acl2
new file mode 100644
index 0000000..2188cea
--- /dev/null
+++ b/books/hacking/table-guard.acl2
@@ -0,0 +1,10 @@
+(in-package "ACL2")
+(ld "hacker-pkg.lsp")
+
+; We need the following for provisional certification, so that ACL2 can read
+; symbols rewrite-code::SYM in dynamic-make-event.acl2x at the start of the
+; Pcertify step.
+(include-book "rewrite-code")
+
+; cert-flags: ? t :ttags ((defcode) (table-guard))
+(certify-book "table-guard" ? t :ttags ((defcode) (table-guard)))
diff --git a/books/hacking/table-guard.lisp b/books/hacking/table-guard.lisp
new file mode 100644
index 0000000..1d83f16
--- /dev/null
+++ b/books/hacking/table-guard.lisp
@@ -0,0 +1,111 @@
+(in-package "ACL2")
+
+; Modification by Matt K. after v4-3: Removed :load-compiled-file :comp, which
+; was part of all three include-book forms just below, in support of
+; provisional certification.  Presumably the indicate books have already been
+; compiled by now, anyhow.
+
+; were in portcullis:
+(include-book "defcode" :ttags ((defcode)))
+(include-book "rewrite-code")
+(include-book "redefun")
+
+#|
+
+table-guard.lisp
+----------------
+
+By Peter Dillinger, ca. 2006
+
+This is an example application of the hacking books which modifies ACL2 to
+allow extending table guards.
+
+|#
+
+(program)
+(set-state-ok t)
+
+
+(defttag table-guard) ; need to do some evil stuff
+
+; rewrite the table code to allow guard changes if a ttag is active
+(progn+touchable
+ :all
+ (redefun+rewrite
+  table-fn1
+  (:carpat (cond
+            ((equal old-guard tterm)
+             %redundant%)
+            (old-guard
+             %er1%)
+            ((getpropc name 'table-alist nil %wrld%)
+             %er2%)
+            (t
+             %rest%))
+   :repl   (cond
+            ((equal old-guard tterm)
+             %redundant%)
+            ((and old-guard (not (ttag %wrld%)))
+             %er1%)
+            ((and (getpropc name 'table-alist nil %wrld%)
+                  (not (ttag %wrld%)))
+             %er2%)
+            (t
+             %rest%))
+   :vars (%redundant%
+          %er1%
+          %er2%
+          %wrld%
+          %rest%)
+   :mult 1)))
+
+(defttag nil) ; end of evil stuff
+
+
+; name: name of table whose guard to rewrite
+; rewrite-spec: like in redefun+rewrite (see rewrite-code.lisp)
+; hints: for proving that old-guard implies new-guard
+; skip-proof: t if you want to skip proving old-guard implies new-guard
+;
+; proof is used as a sanity check mostly.
+(defmacro rewrite-table-guard (name rewrite-spec &key hints skip-proof)
+  (declare (xargs :guard (symbolp name)))
+  `(make-event
+    (er-let* ((old-guard (table ,name nil nil :guard))
+              (new-guard-cons (er-rewrite-form (list old-guard)
+                                               .,rewrite-spec)))
+      (er-progn
+       (if ',skip-proof
+         (value nil)
+         (thm-fn `(implies ,old-guard ,(car new-guard-cons))
+                 state ',hints nil))
+       (value `(table ,',name nil nil :guard ,(car new-guard-cons)))))))
+
+; adds specified key to acl2-defaults-table with guard for its value.
+; also defines a setter macro.
+(defmacro add-acl2-defaults-table-key (name val-guard)
+  (declare (xargs :guard (keywordp name)))
+  (let* ((name-str (symbol-name name))
+         (set-sym (intern (string-append "SET-" name-str) "ACL2")))
+    `(progn
+      (rewrite-table-guard
+       acl2-defaults-table
+       (:carpat %body%
+        :vars %body%
+        :repl (if (eq key ',name)
+                ,val-guard
+                %body%)))
+      (defmacro ,set-sym (v)
+        `(with-output :off summary
+          (progn (table acl2-defaults-table ,',name ',v)
+                 (table acl2-defaults-table ,',name)))))))
+
+
+#| test case:
+(defttag t)
+
+(add-acl2-defaults-table-key :termination-method
+                             (member-eq val '(:foo :bar :baz)))
+
+(set-termination-method :foo)
+|#