		Search-engine friendly clone of the ACL2 documentation.

Vl-portdecl

Make-vl-portdecl

Basic constructor macro for vl-portdecl structures.

Syntax

(make-vl-portdecl [:name <name>] 
                  [:loc <loc>] 
                  [:dir <dir>] 
                  [:type <type>] 
                  [:default <default>] 
                  [:nettype <nettype>] 
                  [:atts <atts>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-portdecl

(defmacro make-vl-portdecl (&rest args)
  (std::make-aggregate 'vl-portdecl
                       args
                       '((:name)
                         (:loc)
                         (:dir)
                         (:type)
                         (:default)
                         (:nettype)
                         (:atts))
                       'make-vl-portdecl
                       nil))

Function: vl-portdecl

(defun vl-portdecl (name loc dir type default nettype atts)
  (declare (xargs :guard (and (stringp name)
                              (vl-location-p loc)
                              (vl-direction-p dir)
                              (vl-datatype-p type)
                              (vl-maybe-expr-p default)
                              (vl-maybe-nettypename-p nettype)
                              (vl-atts-p atts))))
  (declare (xargs :guard t))
  (let ((__function__ 'vl-portdecl))
    (declare (ignorable __function__))
    (b* ((name (mbe :logic (str-fix name) :exec name))
         (loc (mbe :logic (vl-location-fix loc)
                   :exec loc))
         (dir (mbe :logic (vl-direction-fix dir)
                   :exec dir))
         (type (mbe :logic (vl-datatype-fix type)
                    :exec type))
         (default (mbe :logic (vl-maybe-expr-fix default)
                       :exec default))
         (nettype (mbe :logic (vl-maybe-nettypename-fix nettype)
                       :exec nettype))
         (atts (mbe :logic (vl-atts-fix atts)
                    :exec atts)))
      (cons :vl-portdecl
            (std::prod-cons
                 (std::prod-cons name (std::prod-cons loc dir))
                 (std::prod-cons (std::prod-cons type default)
                                 (std::prod-cons nettype atts)))))))