Filtering...

raw

books/hacking/raw

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))))