		Search-engine friendly clone of the ACL2 documentation.

Vl-union

Make-vl-union

Basic constructor macro for vl-union structures.

Syntax

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

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-union

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

Function: vl-union

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