		Search-engine friendly clone of the ACL2 documentation.

Vl-scopeinfo

Make-vl-scopeinfo

Basic constructor macro for vl-scopeinfo structures.

Syntax

(make-vl-scopeinfo [:locals <locals>] 
                   [:imports <imports>] 
                   [:star-packages <star-packages>] 
                   [:id <id>] 
                   [:scopetype <scopetype>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-scopeinfo

(defmacro make-vl-scopeinfo (&rest args)
  (std::make-aggregate 'vl-scopeinfo
                       args
                       '((:locals)
                         (:imports)
                         (:star-packages)
                         (:id)
                         (:scopetype quote :vl-anonymous-scope))
                       'make-vl-scopeinfo
                       nil))

Function: vl-scopeinfo

(defun vl-scopeinfo (locals imports star-packages id scopetype)
  (declare (xargs :guard (and (vl-scopeitem-alist-p locals)
                              (vl-importresult-alist-p imports)
                              (string-listp star-packages)
                              (vl-maybe-scopeid-p id)
                              (vl-scopetype-p scopetype))))
  (declare (xargs :guard t))
  (let ((__function__ 'vl-scopeinfo))
    (declare (ignorable __function__))
    (b* ((locals (mbe :logic (vl-scopeitem-alist-fix locals)
                      :exec locals))
         (imports (mbe :logic (vl-importresult-alist-fix imports)
                       :exec imports))
         (star-packages (mbe :logic (string-list-fix star-packages)
                             :exec star-packages))
         (id (mbe :logic (vl-maybe-scopeid-fix id)
                  :exec id))
         (scopetype (mbe :logic (vl-scopetype-fix scopetype)
                         :exec scopetype)))
      (cons :vl-scopeinfo
            (std::prod-cons
                 (std::prod-cons locals imports)
                 (std::prod-cons star-packages
                                 (std::prod-cons id scopetype)))))))