		Search-engine friendly clone of the ACL2 documentation.

Vl-enum

Make-vl-enum

Basic constructor macro for vl-enum structures.

Syntax

(make-vl-enum [:basetype <basetype>] 
              [:items <items>] 
              [:values <values>] 
              [:pdims <pdims>] 
              [:udims <udims>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-enum

(defmacro make-vl-enum (&rest args)
  (std::make-aggregate 'vl-enum
                       args
                       '((:basetype)
                         (:items)
                         (:values)
                         (:pdims)
                         (:udims))
                       'make-vl-enum
                       nil))

Function: vl-enum

(defun vl-enum (basetype items values pdims udims)
 (declare (xargs :guard (and (vl-datatype-p basetype)
                             (vl-enumitemlist-p items)
                             (vl-exprlist-p values)
                             (vl-dimensionlist-p pdims)
                             (vl-dimensionlist-p udims))))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-enum))
  (declare (ignorable __function__))
  (b* ((basetype (mbe :logic (vl-datatype-fix basetype)
                      :exec basetype))
       (items (mbe :logic (vl-enumitemlist-fix items)
                   :exec items))
       (values (mbe :logic (vl-exprlist-fix values)
                    :exec values))
       (pdims (mbe :logic (vl-dimensionlist-fix pdims)
                   :exec pdims))
       (udims (mbe :logic (vl-dimensionlist-fix udims)
                   :exec udims)))
   (cons
    :vl-enum (std::prod-cons
                  (std::prod-cons basetype items)
                  (std::prod-cons values
                                  (std::prod-cons pdims udims)))))))