		Search-engine friendly clone of the ACL2 documentation.

Vl-delta

Make-vl-delta

Basic constructor macro for vl-delta structures.

Syntax

(make-vl-delta [:nf <nf>] 
               [:vardecls <vardecls>] 
               [:assigns <assigns>] 
               [:modinsts <modinsts>] 
               [:gateinsts <gateinsts>] 
               [:warnings <warnings>] 
               [:addmods <addmods>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-delta

(defmacro make-vl-delta (&rest args)
  (std::make-aggregate 'vl-delta
                       args
                       '((:nf)
                         (:vardecls)
                         (:assigns)
                         (:modinsts)
                         (:gateinsts)
                         (:warnings)
                         (:addmods))
                       'make-vl-delta
                       nil))

Function: vl-delta

(defun vl-delta (nf vardecls assigns
                    modinsts gateinsts warnings addmods)
  (declare (xargs :guard (and (vl-namefactory-p nf)
                              (vl-vardecllist-p vardecls)
                              (vl-assignlist-p assigns)
                              (vl-modinstlist-p modinsts)
                              (vl-gateinstlist-p gateinsts)
                              (vl-warninglist-p warnings)
                              (vl-modulelist-p addmods))))
  (declare (xargs :guard t))
  (let ((__function__ 'vl-delta))
    (declare (ignorable __function__))
    (b* ((nf (mbe :logic (vl-namefactory-fix nf)
                  :exec nf))
         (vardecls (mbe :logic (vl-vardecllist-fix vardecls)
                        :exec vardecls))
         (assigns (mbe :logic (vl-assignlist-fix assigns)
                       :exec assigns))
         (modinsts (mbe :logic (vl-modinstlist-fix modinsts)
                        :exec modinsts))
         (gateinsts (mbe :logic (vl-gateinstlist-fix gateinsts)
                         :exec gateinsts))
         (warnings (mbe :logic (vl-warninglist-fix warnings)
                        :exec warnings))
         (addmods (mbe :logic (vl-modulelist-fix addmods)
                       :exec addmods)))
      (std::prod-cons
           (std::prod-cons nf (std::prod-cons vardecls assigns))
           (std::prod-cons (std::prod-cons modinsts gateinsts)
                           (std::prod-cons warnings addmods))))))