		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Vl-preprocess

Top-level interface to the preprocessor.

Signature
(vl-preprocess echars &key defines filemap config iskips bytes idcache ifdefmap defmap warnings (state 'state)) → (mv successp defines filemap iskips ifdefmap defmap bytes warnings new-echars state)
Arguments: echars — Characters to preprocess, in order.
Guard (vl-echarlist-p echars).; defines — Initial definitions to use.
Guard (vl-defines-p defines).; filemap — Initial file map to extend (for `includes).
Guard (vl-filemap-p filemap).; config — Controls the Verilog edition, include paths, etc.
Guard (vl-loadconfig-p config).; iskips — Multi-include optimization.
Guard (vl-includeskips-p iskips).; bytes — Bytes read so far.
Guard (natp bytes).; idcache — Include-directory cache.
Guard (vl-dirlist-cache-p idcache).; ifdefmap — Ifdef use map to extend.
Guard (vl-ifdef-use-map-p ifdefmap).; defmap — Define use map to extend.
Guard (vl-def-use-map-p defmap).; warnings — Warnings accumulator to extend.
Guard (vl-warninglist-p warnings).; state — ACL2's state, for file i/o.
Returns: successp — Was preprocessing successful?.
Type (booleanp successp).; defines — Updated defines after preprocessing the files.
Type (vl-defines-p defines).; filemap — Possibly extended filemap.
Type (vl-filemap-p filemap).; iskips — Possibly updated iskips.
Type (vl-includeskips-p iskips).; ifdefmap — Possibly extended ifdef use map.
Type (vl-ifdef-use-map-p ifdefmap).; defmap — Possibly extended define use map.
Type (vl-def-use-map-p defmap).; bytes — Updated total bytes.
Type (natp bytes).; warnings — Possibly updated warnings.
Type (vl-warninglist-p warnings).; new-echars — Updated extended characters, after preprocessing.
Type (vl-echarlist-p new-echars).; state — Type (state-p1 state), given (force (state-p1 state)).

Definitions and Theorems

Function: vl-preprocess-fn

(defun vl-preprocess-fn
       (echars defines filemap config iskips bytes
               idcache ifdefmap defmap warnings state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (vl-echarlist-p echars)
                             (vl-defines-p defines)
                             (vl-filemap-p filemap)
                             (vl-loadconfig-p config)
                             (vl-includeskips-p iskips)
                             (natp bytes)
                             (vl-dirlist-cache-p idcache)
                             (vl-ifdef-use-map-p ifdefmap)
                             (vl-def-use-map-p defmap)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-preprocess))
  (declare (ignorable __function__))
  (b* (((local-stobjs ppst)
        (mv successp
            defines filemap iskips ifdefmap defmap
            bytes warnings new-echars ppst state))
       (ppst (vl-ppst-update-defines defines))
       (ppst (vl-ppst-update-filemap filemap))
       (ppst (vl-ppst-update-config config))
       (ppst (vl-ppst-update-activep t))
       (ppst (vl-ppst-update-iskips iskips))
       (ppst (vl-ppst-update-warnings warnings))
       (ppst (vl-ppst-update-idcache idcache))
       (ppst (vl-ppst-update-ifdefmap ifdefmap))
       (ppst (vl-ppst-update-defmap defmap))
       (- (or (equal (vl-loadconfig->include-dirs config)
                     (alist-keys (vl-ppst->idcache)))
              (raise "idcache is screwed up: ~x0 versus ~x1"
                     (vl-loadconfig->include-dirs config)
                     (alist-keys (vl-ppst->idcache)))))
       (ppst (vl-ppst-update-bytes bytes))
       ((mv successp remainder ppst state)
        (vl-preprocess-loop echars
                            *vl-preprocess-clock* ppst state))
       (defines (vl-ppst->defines))
       (filemap (vl-ppst->filemap))
       (iskips (vl-ppst->iskips))
       (ifdefmap (vl-ppst->ifdefmap))
       (defmap (vl-ppst->defmap))
       (bytes (vl-ppst->bytes))
       (warnings (vl-ppst->warnings))
       ((when successp)
        (let ((ppst (vl-ppst-unsound-nreverse-acc ppst)))
          (mv successp defines filemap iskips ifdefmap
              defmap bytes warnings (vl-ppst->acc)
              ppst state))))
   (mv
    (cw
       "[[ Previous  ]]: ~s0~%~
             [[ Remaining ]]: ~s1~%"
       (vl-echarlist->string (vl-safe-previous-n 50 (vl-ppst->acc)))
       (vl-echarlist->string (vl-safe-next-n 50 remainder)))
    defines filemap iskips ifdefmap
    defmap bytes warnings nil ppst state))))

Theorem: booleanp-of-vl-preprocess.successp

(defthm booleanp-of-vl-preprocess.successp
  (b* (((mv ?successp acl2::?defines ?filemap
            ?iskips ?ifdefmap ?defmap ?bytes
            ?warnings ?new-echars acl2::?state)
        (vl-preprocess-fn echars defines
                          filemap config iskips bytes idcache
                          ifdefmap defmap warnings state)))
    (booleanp successp))
  :rule-classes :type-prescription)

Theorem: vl-defines-p-of-vl-preprocess.defines

(defthm vl-defines-p-of-vl-preprocess.defines
  (b* (((mv ?successp acl2::?defines ?filemap
            ?iskips ?ifdefmap ?defmap ?bytes
            ?warnings ?new-echars acl2::?state)
        (vl-preprocess-fn echars defines
                          filemap config iskips bytes idcache
                          ifdefmap defmap warnings state)))
    (vl-defines-p defines))
  :rule-classes :rewrite)

Theorem: vl-filemap-p-of-vl-preprocess.filemap

(defthm vl-filemap-p-of-vl-preprocess.filemap
  (b* (((mv ?successp acl2::?defines ?filemap
            ?iskips ?ifdefmap ?defmap ?bytes
            ?warnings ?new-echars acl2::?state)
        (vl-preprocess-fn echars defines
                          filemap config iskips bytes idcache
                          ifdefmap defmap warnings state)))
    (vl-filemap-p filemap))
  :rule-classes :rewrite)

Theorem: vl-includeskips-p-of-vl-preprocess.iskips

(defthm vl-includeskips-p-of-vl-preprocess.iskips
  (b* (((mv ?successp acl2::?defines ?filemap
            ?iskips ?ifdefmap ?defmap ?bytes
            ?warnings ?new-echars acl2::?state)
        (vl-preprocess-fn echars defines
                          filemap config iskips bytes idcache
                          ifdefmap defmap warnings state)))
    (vl-includeskips-p iskips))
  :rule-classes :rewrite)

Theorem: vl-ifdef-use-map-p-of-vl-preprocess.ifdefmap

(defthm vl-ifdef-use-map-p-of-vl-preprocess.ifdefmap
  (b* (((mv ?successp acl2::?defines ?filemap
            ?iskips ?ifdefmap ?defmap ?bytes
            ?warnings ?new-echars acl2::?state)
        (vl-preprocess-fn echars defines
                          filemap config iskips bytes idcache
                          ifdefmap defmap warnings state)))
    (vl-ifdef-use-map-p ifdefmap))
  :rule-classes :rewrite)

Theorem: vl-def-use-map-p-of-vl-preprocess.defmap

(defthm vl-def-use-map-p-of-vl-preprocess.defmap
  (b* (((mv ?successp acl2::?defines ?filemap
            ?iskips ?ifdefmap ?defmap ?bytes
            ?warnings ?new-echars acl2::?state)
        (vl-preprocess-fn echars defines
                          filemap config iskips bytes idcache
                          ifdefmap defmap warnings state)))
    (vl-def-use-map-p defmap))
  :rule-classes :rewrite)

Theorem: natp-of-vl-preprocess.bytes

(defthm natp-of-vl-preprocess.bytes
  (b* (((mv ?successp acl2::?defines ?filemap
            ?iskips ?ifdefmap ?defmap ?bytes
            ?warnings ?new-echars acl2::?state)
        (vl-preprocess-fn echars defines
                          filemap config iskips bytes idcache
                          ifdefmap defmap warnings state)))
    (natp bytes))
  :rule-classes :type-prescription)

Theorem: vl-warninglist-p-of-vl-preprocess.warnings

(defthm vl-warninglist-p-of-vl-preprocess.warnings
  (b* (((mv ?successp acl2::?defines ?filemap
            ?iskips ?ifdefmap ?defmap ?bytes
            ?warnings ?new-echars acl2::?state)
        (vl-preprocess-fn echars defines
                          filemap config iskips bytes idcache
                          ifdefmap defmap warnings state)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-echarlist-p-of-vl-preprocess.new-echars

(defthm vl-echarlist-p-of-vl-preprocess.new-echars
  (b* (((mv ?successp acl2::?defines ?filemap
            ?iskips ?ifdefmap ?defmap ?bytes
            ?warnings ?new-echars acl2::?state)
        (vl-preprocess-fn echars defines
                          filemap config iskips bytes idcache
                          ifdefmap defmap warnings state)))
    (vl-echarlist-p new-echars))
  :rule-classes :rewrite)

Theorem: state-p1-of-vl-preprocess.state

(defthm state-p1-of-vl-preprocess.state
  (implies
       (force (state-p1 state))
       (b* (((mv ?successp acl2::?defines ?filemap
                 ?iskips ?ifdefmap ?defmap ?bytes
                 ?warnings ?new-echars acl2::?state)
             (vl-preprocess-fn echars defines
                               filemap config iskips bytes idcache
                               ifdefmap defmap warnings state)))
         (state-p1 state)))
  :rule-classes :rewrite)