		Search-engine friendly clone of the ACL2 documentation.

Vl-design

Make-vl-design

Basic constructor macro for vl-design structures.

Syntax

(make-vl-design [:version <version>] 
                [:mods <mods>] 
                [:udps <udps>] 
                [:interfaces <interfaces>] 
                [:programs <programs>] 
                [:packages <packages>] 
                [:configs <configs>] 
                [:vardecls <vardecls>] 
                [:taskdecls <taskdecls>] 
                [:fundecls <fundecls>] 
                [:paramdecls <paramdecls>] 
                [:imports <imports>] 
                [:fwdtypes <fwdtypes>] 
                [:typedefs <typedefs>] 
                [:warnings <warnings>] 
                [:comments <comments>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-design

(defmacro make-vl-design (&rest args)
  (std::make-aggregate 'vl-design
                       args
                       '((:version . *vl-current-syntax-version*)
                         (:mods)
                         (:udps)
                         (:interfaces)
                         (:programs)
                         (:packages)
                         (:configs)
                         (:vardecls)
                         (:taskdecls)
                         (:fundecls)
                         (:paramdecls)
                         (:imports)
                         (:fwdtypes)
                         (:typedefs)
                         (:warnings)
                         (:comments))
                       'make-vl-design
                       nil))

Function: vl-design

(defun vl-design (version mods udps interfaces
                          programs packages configs vardecls
                          taskdecls fundecls paramdecls imports
                          fwdtypes typedefs warnings comments)
 (declare (xargs :guard (and (vl-syntaxversion-p version)
                             (vl-modulelist-p mods)
                             (vl-udplist-p udps)
                             (vl-interfacelist-p interfaces)
                             (vl-programlist-p programs)
                             (vl-packagelist-p packages)
                             (vl-configlist-p configs)
                             (vl-vardecllist-p vardecls)
                             (vl-taskdecllist-p taskdecls)
                             (vl-fundecllist-p fundecls)
                             (vl-paramdecllist-p paramdecls)
                             (vl-importlist-p imports)
                             (vl-fwdtypedeflist-p fwdtypes)
                             (vl-typedeflist-p typedefs)
                             (vl-warninglist-p warnings)
                             (vl-commentmap-p comments))))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-design))
  (declare (ignorable __function__))
  (b* ((version (mbe :logic (vl-syntaxversion-fix version)
                     :exec version))
       (mods (mbe :logic (vl-modulelist-fix mods)
                  :exec mods))
       (udps (mbe :logic (vl-udplist-fix udps)
                  :exec udps))
       (interfaces (mbe :logic (vl-interfacelist-fix interfaces)
                        :exec interfaces))
       (programs (mbe :logic (vl-programlist-fix programs)
                      :exec programs))
       (packages (mbe :logic (vl-packagelist-fix packages)
                      :exec packages))
       (configs (mbe :logic (vl-configlist-fix configs)
                     :exec configs))
       (vardecls (mbe :logic (vl-vardecllist-fix vardecls)
                      :exec vardecls))
       (taskdecls (mbe :logic (vl-taskdecllist-fix taskdecls)
                       :exec taskdecls))
       (fundecls (mbe :logic (vl-fundecllist-fix fundecls)
                      :exec fundecls))
       (paramdecls (mbe :logic (vl-paramdecllist-fix paramdecls)
                        :exec paramdecls))
       (imports (mbe :logic (vl-importlist-fix imports)
                     :exec imports))
       (fwdtypes (mbe :logic (vl-fwdtypedeflist-fix fwdtypes)
                      :exec fwdtypes))
       (typedefs (mbe :logic (vl-typedeflist-fix typedefs)
                      :exec typedefs))
       (warnings (mbe :logic (vl-warninglist-fix warnings)
                      :exec warnings))
       (comments (mbe :logic (vl-commentmap-fix comments)
                      :exec comments)))
   (cons
    :vl-design
    (std::prod-cons
      (std::prod-cons
           (std::prod-cons (std::prod-cons version mods)
                           (std::prod-cons udps interfaces))
           (std::prod-cons (std::prod-cons programs packages)
                           (std::prod-cons configs vardecls)))
      (std::prod-cons
           (std::prod-cons (std::prod-cons taskdecls fundecls)
                           (std::prod-cons paramdecls imports))
           (std::prod-cons (std::prod-cons fwdtypes typedefs)
                           (std::prod-cons warnings comments))))))))