Filtering...

defaggrify-defrec

books/std/util/defaggrify-defrec
other
(in-package "STD")
other
(include-book "da-base")
other
(program)
other
(defxdoc defaggrify-defrec
  :parents (defaggregate)
  :short "Add @(see defaggregate)-style emulation for @('defrec') records."
  :long "<p>The @('defrec') macro is an undocumented utility which is used
within the ACL2 theorem prover to introduce structures.  Although many of the
details are different, it is in many ways like @(see defaggregate).</p>

<p>@(call defaggrify-defrec) is a macro that automatically adds
@('defaggregate')-style accessors and @(see b*) binders that work on
@('defrec') structures.</p>

<p>Typical usage is, e.g.,:</p>

@({
     (in-package "ACL2")
     (std::defaggrify-defrec rewrite-rule)
     (std::defaggrify-defrec def-body)
     ...
})

<p>We may eventually extend this to include additional @('defaggregate')-style
features such as @('make-') and @('change-') macros.</p>")
flatten-defrec-fieldsfunction
(defun flatten-defrec-fields
  (x)
  (if (atom x)
    (and x (list x))
    (append (flatten-defrec-fields (car x))
      (flatten-defrec-fields (cdr x)))))
look-up-defrec-fieldsfunction
(defun look-up-defrec-fields
  (rec world)
  (b* ((maker (record-maker-function-name rec)) (body (getprop maker
          'macro-body
          nil
          'current-acl2-world
          world))
      ((unless body) (er hard?
          'look-up-defrec-field-layout
          "Can't find macro-body for maker ~x0 of defrec ~x1.  is ~x1 even ~
             a defrec?"
          maker
          rec))
      (quoted-layout (third body))
      ((unless (quotep quoted-layout)) (er hard?
          'look-up-defrec-field-layout
          "Sanity check failed, field layout of ~x0 is not a quotep?"
          rec)))
    (flatten-defrec-fields (unquote quoted-layout))))
da-accessor-for-defrec-fieldfunction
(defun da-accessor-for-defrec-field
  (rec field)
  (let ((weak-rec-p (intern$ (concatenate 'string "WEAK-" (symbol-name rec) "-P")
         "ACL2")))
    `(defun-inline ,(STD::DA-ACCESSOR-NAME STD::REC STD::FIELD)
      (x)
      (declare (xargs :guard (,STD::WEAK-REC-P x)))
      (access ,STD::REC
        x
        ,(STD::INTERN$ (SYMBOL-NAME STD::FIELD) "KEYWORD")))))
da-accessors-for-defrec-fieldsfunction
(defun da-accessors-for-defrec-fields
  (rec fields)
  (if (atom fields)
    nil
    (cons (da-accessor-for-defrec-field rec
        (car fields))
      (da-accessors-for-defrec-fields rec
        (cdr fields)))))
da-defrec-emulation-fnfunction
(defun da-defrec-emulation-fn
  (rec world)
  (let ((fields (look-up-defrec-fields rec world)))
    `(encapsulate nil
      (logic)
      ,@(STD::DA-ACCESSORS-FOR-DEFREC-FIELDS STD::REC STD::FIELDS)
      ,(STD::DA-MAKE-BINDER STD::REC STD::FIELDS))))
defaggrify-defrecmacro
(defmacro defaggrify-defrec
  (rec)
  `(make-event (b* ((world (w state)))
      (value (da-defrec-emulation-fn ',STD::REC world)))))