		Search-engine friendly clone of the ACL2 documentation.

Vl-saved-ppst

Make-vl-saved-ppst

Basic constructor macro for vl-saved-ppst structures.

Syntax

(make-vl-saved-ppst [:acc <acc>] 
                    [:istack <istack>] 
                    [:activep <activep>] 
                    [:defines <defines>] 
                    [:filemap <filemap>] 
                    [:config <config>] 
                    [:iskips <iskips>] 
                    [:warnings <warnings>] 
                    [:includes <includes>] 
                    [:bytes <bytes>] 
                    [:idcache <idcache>] 
                    [:ifdefmap <ifdefmap>] 
                    [:defmap <defmap>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-saved-ppst

(defmacro make-vl-saved-ppst (&rest args)
  (std::make-aggregate 'vl-saved-ppst
                       args
                       '((:acc)
                         (:istack)
                         (:activep)
                         (:defines)
                         (:filemap)
                         (:config)
                         (:iskips)
                         (:warnings)
                         (:includes)
                         (:bytes)
                         (:idcache)
                         (:ifdefmap)
                         (:defmap))
                       'make-vl-saved-ppst
                       nil))

Function: vl-saved-ppst

(defun vl-saved-ppst (acc istack activep
                          defines filemap config iskips warnings
                          includes bytes idcache ifdefmap defmap)
 (declare (xargs :guard (and (vl-echarlist-p acc)
                             (vl-istack-p istack)
                             (booleanp activep)
                             (vl-defines-p defines)
                             (vl-filemap-p filemap)
                             (vl-loadconfig-p config)
                             (vl-includeskips-p iskips)
                             (vl-warninglist-p warnings)
                             (string-listp includes)
                             (natp bytes)
                             (vl-dirlist-cache-p idcache)
                             (vl-ifdef-use-map-p ifdefmap)
                             (vl-def-use-map-p defmap))))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-saved-ppst))
  (declare (ignorable __function__))
  (b* ((acc (mbe :logic (vl-echarlist-fix acc)
                 :exec acc))
       (istack (mbe :logic (vl-istack-fix istack)
                    :exec istack))
       (activep (mbe :logic (acl2::bool-fix activep)
                     :exec activep))
       (defines (mbe :logic (vl-defines-fix defines)
                     :exec defines)
)
       (filemap (mbe :logic (vl-filemap-fix filemap)
                     :exec filemap))
       (config (mbe :logic (vl-loadconfig-fix config)
                    :exec config))
       (iskips (mbe :logic (vl-includeskips-fix iskips)
                    :exec iskips))
       (warnings (mbe :logic (vl-warninglist-fix warnings)
                      :exec warnings))
       (includes (mbe :logic (string-list-fix includes)
                      :exec includes))
       (bytes (mbe :logic (nfix bytes) :exec bytes))
       (idcache (mbe :logic (vl-dirlist-cache-fix idcache)
                     :exec idcache))
       (ifdefmap (mbe :logic (vl-ifdef-use-map-fix ifdefmap)
                      :exec ifdefmap))
       (defmap (mbe :logic (vl-def-use-map-fix defmap)
                    :exec defmap)))
   (cons
    :vl-saved-ppst
    (std::prod-cons
        (std::prod-cons
             (std::prod-cons acc (std::prod-cons istack activep))
             (std::prod-cons defines
                             (std::prod-cons filemap config)))
        (std::prod-cons
             (std::prod-cons iskips
                             (std::prod-cons warnings includes))
             (std::prod-cons (std::prod-cons bytes idcache)
                             (std::prod-cons ifdefmap defmap))))))))