		Search-engine friendly clone of the ACL2 documentation.

Vl-fundecl

Make-vl-fundecl

Basic constructor macro for vl-fundecl structures.

Syntax

(make-vl-fundecl [:name <name>] 
                 [:rettype <rettype>] 
                 [:body <body>] 
                 [:loc <loc>] 
                 [:portdecls <portdecls>] 
                 [:function-map <function-map>] 
                 [:lifetime <lifetime>] 
                 [:vardecls <vardecls>] 
                 [:paramdecls <paramdecls>] 
                 [:typedefs <typedefs>] 
                 [:imports <imports>] 
                 [:atts <atts>] 
                 [:loaditems <loaditems>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-fundecl

(defmacro make-vl-fundecl (&rest args)
  (std::make-aggregate 'vl-fundecl
                       args
                       '((:name)
                         (:rettype)
                         (:body)
                         (:loc)
                         (:portdecls)
                         (:function-map)
                         (:lifetime)
                         (:vardecls)
                         (:paramdecls)
                         (:typedefs)
                         (:imports)
                         (:atts)
                         (:loaditems))
                       'make-vl-fundecl
                       nil))

Function: vl-fundecl

(defun vl-fundecl (name rettype body loc portdecls function-map
                        lifetime vardecls paramdecls
                        typedefs imports atts loaditems)
 (declare
  (xargs :guard (and (stringp name)
                     (vl-datatype-p rettype)
                     (vl-stmt-p body)
                     (vl-location-p loc)
                     (vl-portdecllist-p portdecls)
                     (vl-function-specialization-map-p function-map)
                     (vl-lifetime-p lifetime)
                     (vl-vardecllist-p vardecls)
                     (vl-paramdecllist-p paramdecls)
                     (vl-typedeflist-p typedefs)
                     (vl-importlist-p imports)
                     (vl-atts-p atts)
                     (vl-portdecl-or-blockitem-list-p loaditems))))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-fundecl))
  (declare (ignorable __function__))
  (b*
   ((name (mbe :logic (str-fix name) :exec name))
    (rettype (mbe :logic (vl-datatype-fix rettype)
                  :exec rettype))
    (body (mbe :logic (vl-stmt-fix body)
               :exec body))
    (loc (mbe :logic (vl-location-fix loc)
              :exec loc))
    (portdecls (mbe :logic (vl-portdecllist-fix portdecls)
                    :exec portdecls))
    (function-map
       (mbe :logic (vl-function-specialization-map-fix function-map)
            :exec function-map))
    (lifetime (mbe :logic (vl-lifetime-fix lifetime)
                   :exec lifetime))
    (vardecls (mbe :logic (vl-vardecllist-fix vardecls)
                   :exec vardecls))
    (paramdecls (mbe :logic (vl-paramdecllist-fix paramdecls)
                     :exec paramdecls))
    (typedefs (mbe :logic (vl-typedeflist-fix typedefs)
                   :exec typedefs))
    (imports (mbe :logic (vl-importlist-fix imports)
                  :exec imports))
    (atts (mbe :logic (vl-atts-fix atts)
               :exec atts))
    (loaditems
         (mbe :logic (vl-portdecl-or-blockitem-list-fix loaditems)
              :exec loaditems)))
   (cons
    :vl-fundecl
    (std::prod-cons
      (std::prod-cons
           (std::prod-cons name (std::prod-cons rettype body))
           (std::prod-cons loc
                           (std::prod-cons portdecls function-map)))
      (std::prod-cons
           (std::prod-cons lifetime
                           (std::prod-cons vardecls paramdecls))
           (std::prod-cons (std::prod-cons typedefs imports)
                           (std::prod-cons atts loaditems))))))))