		Search-engine friendly clone of the ACL2 documentation.

Vl-loadstate

Make-vl-loadstate

Basic constructor macro for vl-loadstate structures.

Syntax

(make-vl-loadstate [:config <config>] 
                   [:descs <descs>] 
                   [:descalist <descalist>] 
                   [:defines <defines>] 
                   [:iskips <iskips>] 
                   [:ifdefmap <ifdefmap>] 
                   [:defmap <defmap>] 
                   [:idcache <idcache>] 
                   [:spcache <spcache>] 
                   [:reportcard <reportcard>] 
                   [:pstate <pstate>] 
                   [:filemap <filemap>] 
                   [:bytes <bytes>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-loadstate

(defmacro make-vl-loadstate (&rest args)
  (std::make-aggregate 'vl-loadstate
                       args
                       '((:config)
                         (:descs)
                         (:descalist)
                         (:defines)
                         (:iskips)
                         (:ifdefmap)
                         (:defmap)
                         (:idcache)
                         (:spcache)
                         (:reportcard)
                         (:pstate)
                         (:filemap)
                         (:bytes))
                       'make-vl-loadstate
                       nil))

Function: vl-loadstate

(defun vl-loadstate (config descs descalist
                            defines iskips ifdefmap defmap idcache
                            spcache reportcard pstate filemap bytes)
 (declare (xargs :guard (and (vl-loadconfig-p config)
                             (vl-descriptionlist-p descs)
                             (vl-defines-p defines)
                             (vl-includeskips-p iskips)
                             (vl-ifdef-use-map-p ifdefmap)
                             (vl-def-use-map-p defmap)
                             (vl-dirlist-cache-p idcache)
                             (vl-dirxlist-cache-p spcache)
                             (vl-reportcard-p reportcard)
                             (vl-parsestate-p pstate)
                             (vl-filemap-p filemap)
                             (natp bytes))))
 (declare
      (xargs :guard (equal descalist (vl-make-descalist descs))))
 (let ((__function__ 'vl-loadstate))
  (declare (ignorable __function__))
  (b* ((config (mbe :logic (vl-loadconfig-fix config)
                    :exec config))
       (descs (mbe :logic (vl-descriptionlist-fix descs)
                   :exec descs))
       (defines (mbe :logic (vl-defines-fix defines)
                     :exec defines)
)
       (iskips (mbe :logic (vl-includeskips-fix iskips)
                    :exec iskips))
       (ifdefmap (mbe :logic (vl-ifdef-use-map-fix ifdefmap)
                      :exec ifdefmap))
       (defmap (mbe :logic (vl-def-use-map-fix defmap)
                    :exec defmap))
       (idcache (mbe :logic (vl-dirlist-cache-fix idcache)
                     :exec idcache))
       (spcache (mbe :logic (vl-dirxlist-cache-fix spcache)
                     :exec spcache))
       (reportcard (mbe :logic (vl-reportcard-fix reportcard)
                        :exec reportcard))
       (pstate (mbe :logic (vl-parsestate-fix pstate)
                    :exec pstate))
       (filemap (mbe :logic (vl-filemap-fix filemap)
                     :exec filemap))
       (bytes (mbe :logic (nfix bytes) :exec bytes)))
   (let ((descalist (mbe :logic (vl-make-descalist descs)
                         :exec descalist)))
    (cons
     :vl-loadstate
     (std::prod-cons
       (std::prod-cons
            (std::prod-cons config (std::prod-cons descs descalist))
            (std::prod-cons defines
                            (std::prod-cons iskips ifdefmap)))
       (std::prod-cons
            (std::prod-cons defmap (std::prod-cons idcache spcache))
            (std::prod-cons (std::prod-cons reportcard pstate)
                            (std::prod-cons filemap bytes)))))))))