Included Books
other
(in-package "ACL2")
include-book
(include-book "defstruct-parsing")
other
(program)
other
(set-state-ok t)
make-raw-definitionsmacro
(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)))))))
defun-rawmacro
(defmacro defun-raw (name ll &rest rst) `(make-raw-definitions ((defun ,NAME ,LL . ,RST)) :compile t :fresh t :save-fns (,NAME)))
defmacro-rawmacro
(defmacro defmacro-raw (name ll &rest rst) `(make-raw-definitions ((defmacro ,NAME ,LL . ,RST)) :compile t :fresh t :save-macros (,NAME)))
copy-raw-defunmacro
(defmacro copy-raw-defun (src dst) `(make-raw-definitions ((setf (symbol-function ',DST) (symbol-function ',SRC))) :compile nil :fresh t :save-fns (,DST)))
copy-raw-defmacromacro
(defmacro copy-raw-defmacro (src dst) `(make-raw-definitions ((setf (macro-function ',DST) (macro-function ',SRC))) :compile nil :fresh t :save-macros (,DST)))
defvar-rawmacro
(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)))
defparameter-rawmacro
(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)))
defconstant-rawmacro
(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)))
defstruct-rawmacro
(defmacro defstruct-raw (&rest args) (declare (xargs :guard args)) (let* ((form (cons 'defstruct args)) (name-and-fns (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))))
modify-raw-defunmacro
(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))))