		Search-engine friendly clone of the ACL2 documentation.

Vl-struct

Make-vl-struct

Basic constructor macro for vl-struct structures.

Syntax

(make-vl-struct [:packedp <packedp>] 
                [:signedp <signedp>] 
                [:members <members>] 
                [:pdims <pdims>] 
                [:udims <udims>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-struct

(defmacro make-vl-struct (&rest args)
  (std::make-aggregate 'vl-struct
                       args
                       '((:packedp)
                         (:signedp)
                         (:members)
                         (:pdims)
                         (:udims))
                       'make-vl-struct
                       nil))

Function: vl-struct

(defun vl-struct (packedp signedp members pdims udims)
  (declare (xargs :guard (and (booleanp packedp)
                              (booleanp signedp)
                              (vl-structmemberlist-p members)
                              (vl-packeddimensionlist-p pdims)
                              (vl-packeddimensionlist-p udims))))
  (declare (xargs :guard t))
  (let ((__function__ 'vl-struct))
    (declare (ignorable __function__))
    (b* ((packedp (mbe :logic (acl2::bool-fix packedp)
                       :exec packedp))
         (signedp (mbe :logic (acl2::bool-fix signedp)
                       :exec signedp))
         (members (mbe :logic (vl-structmemberlist-fix members)
                       :exec members))
         (pdims (mbe :logic (vl-packeddimensionlist-fix pdims)
                     :exec pdims))
         (udims (mbe :logic (vl-packeddimensionlist-fix udims)
                     :exec udims)))
      (cons :vl-struct
            (std::prod-cons
                 (std::prod-cons packedp signedp)
                 (std::prod-cons members
                                 (std::prod-cons pdims udims)))))))