		Search-engine friendly clone of the ACL2 documentation.

Defstruct-info

Make-defstruct-info

Basic constructor macro for defstruct-info structures.

Syntax

(make-defstruct-info [:tag <tag>] 
                     [:members <members>] 
                     [:flexiblep <flexiblep>] 
                     [:fixtype <fixtype>] 
                     [:recognizer <recognizer>] 
                     [:fixer <fixer>] 
                     [:fixer-recognizer-thm <fixer-recognizer-thm>] 
                     [:not-error-thm <not-error-thm>] 
                     [:valuep-thm <valuep-thm>] 
                     [:value-kind-thm <value-kind-thm>] 
                     [:type-of-value-thm <type-of-value-thm>] 
                     [:flexiblep-thm <flexiblep-thm>] 
                     [:type-to-quoted-thm <type-to-quoted-thm>] 
                     [:pointer-type-to-quoted-thm <pointer-type-to-quoted-thm>] 
                     [:call <call>])

This is the usual way to construct defstruct-info structures. It simply conses together a structure with the specified fields.

This macro generates a new defstruct-info structure from scratch. See also change-defstruct-info, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-defstruct-info

(defmacro make-defstruct-info (&rest args)
  (std::make-aggregate 'defstruct-info
                       args
                       '((:tag)
                         (:members)
                         (:flexiblep)
                         (:fixtype)
                         (:recognizer)
                         (:fixer)
                         (:fixer-recognizer-thm)
                         (:not-error-thm)
                         (:valuep-thm)
                         (:value-kind-thm)
                         (:type-of-value-thm)
                         (:flexiblep-thm)
                         (:type-to-quoted-thm)
                         (:pointer-type-to-quoted-thm)
                         (:call))
                       'make-defstruct-info
                       nil))

Function: defstruct-info

(defun defstruct-info (tag members flexiblep fixtype
                           recognizer fixer fixer-recognizer-thm
                           not-error-thm valuep-thm
                           value-kind-thm type-of-value-thm
                           flexiblep-thm type-to-quoted-thm
                           pointer-type-to-quoted-thm call)
 (declare (xargs :guard (and (identp tag)
                             (defstruct-member-info-listp members)
                             (booleanp flexiblep)
                             (symbolp fixtype)
                             (symbolp recognizer)
                             (symbolp fixer)
                             (symbolp fixer-recognizer-thm)
                             (symbolp not-error-thm)
                             (symbolp valuep-thm)
                             (symbolp value-kind-thm)
                             (symbolp type-of-value-thm)
                             (symbolp flexiblep-thm)
                             (symbolp type-to-quoted-thm)
                             (symbolp pointer-type-to-quoted-thm)
                             (pseudo-event-formp call))))
 (declare (xargs :guard t))
 (let ((__function__ 'defstruct-info))
   (declare (ignorable __function__))
   (b*
    ((tag (mbe :logic (ident-fix tag) :exec tag))
     (members (mbe :logic (defstruct-member-info-list-fix members)
                   :exec members))
     (flexiblep (mbe :logic (acl2::bool-fix flexiblep)
                     :exec flexiblep))
     (fixtype (mbe :logic (symbol-fix fixtype)
                   :exec fixtype))
     (recognizer (mbe :logic (symbol-fix recognizer)
                      :exec recognizer))
     (fixer (mbe :logic (symbol-fix fixer)
                 :exec fixer))
     (fixer-recognizer-thm
          (mbe :logic (symbol-fix fixer-recognizer-thm)
               :exec fixer-recognizer-thm))
     (not-error-thm (mbe :logic (symbol-fix not-error-thm)
                         :exec not-error-thm))
     (valuep-thm (mbe :logic (symbol-fix valuep-thm)
                      :exec valuep-thm))
     (value-kind-thm (mbe :logic (symbol-fix value-kind-thm)
                          :exec value-kind-thm))
     (type-of-value-thm (mbe :logic (symbol-fix type-of-value-thm)
                             :exec type-of-value-thm))
     (flexiblep-thm (mbe :logic (symbol-fix flexiblep-thm)
                         :exec flexiblep-thm))
     (type-to-quoted-thm (mbe :logic (symbol-fix type-to-quoted-thm)
                              :exec type-to-quoted-thm))
     (pointer-type-to-quoted-thm
          (mbe :logic (symbol-fix pointer-type-to-quoted-thm)
               :exec pointer-type-to-quoted-thm))
     (call (mbe :logic (acl2::pseudo-event-form-fix call)
                :exec call)))
    (list (cons 'tag tag)
          (cons 'members members)
          (cons 'flexiblep flexiblep)
          (cons 'fixtype fixtype)
          (cons 'recognizer recognizer)
          (cons 'fixer fixer)
          (cons 'fixer-recognizer-thm
                fixer-recognizer-thm)
          (cons 'not-error-thm not-error-thm)
          (cons 'valuep-thm valuep-thm)
          (cons 'value-kind-thm value-kind-thm)
          (cons 'type-of-value-thm
                type-of-value-thm)
          (cons 'flexiblep-thm flexiblep-thm)
          (cons 'type-to-quoted-thm
                type-to-quoted-thm)
          (cons 'pointer-type-to-quoted-thm
                pointer-type-to-quoted-thm)
          (cons 'call call)))))