		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 (state 'state)) → (mv successp defines filemap 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).; 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), given the guard.; filemap — Possibly extended filemap.
Type (vl-filemap-p filemap), given the guard.; new-echars — Updated extended characters, after preprocessing.
Type (vl-echarlist-p new-echars), given the guard.; 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 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))))
 (let ((__function__ 'vl-preprocess))
  (declare (ignorable __function__))
  (b* (((mv successp
            defines filemap acc remainder state)
        (vl-preprocess-loop echars defines filemap nil t
                            nil *vl-preprocess-clock* config state))
       ((when successp)
        (mv successp defines filemap (rev acc)
            state)))
   (mv
    (cw
       "[[ Previous  ]]: ~s0~%~
             [[ Remaining ]]: ~s1~%"
       (vl-echarlist->string (vl-safe-previous-n 50 acc))
       (vl-echarlist->string (vl-safe-next-n 50 remainder)))
    defines filemap nil state))))

Theorem: booleanp-of-vl-preprocess.successp

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

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

(defthm vl-defines-p-of-vl-preprocess.defines
 (implies
      (and (force (state-p state))
           (force (vl-echarlist-p echars))
           (force (vl-defines-p defines))
           (force (vl-filemap-p filemap))
           (force (vl-loadconfig-p config)))
      (b* (((mv ?successp acl2::?defines
                ?filemap ?new-echars acl2::?state)
            (vl-preprocess-fn echars defines filemap config state)))
        (vl-defines-p defines)))
 :rule-classes :rewrite)

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

(defthm vl-filemap-p-of-vl-preprocess.filemap
 (implies
      (and (force (state-p state))
           (force (vl-echarlist-p echars))
           (force (vl-defines-p defines))
           (force (vl-filemap-p filemap))
           (force (vl-loadconfig-p config)))
      (b* (((mv ?successp acl2::?defines
                ?filemap ?new-echars acl2::?state)
            (vl-preprocess-fn echars defines filemap config state)))
        (vl-filemap-p filemap)))
 :rule-classes :rewrite)

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

(defthm vl-echarlist-p-of-vl-preprocess.new-echars
 (implies
      (and (force (state-p state))
           (force (vl-echarlist-p echars))
           (force (vl-defines-p defines))
           (force (vl-filemap-p filemap))
           (force (vl-loadconfig-p config)))
      (b* (((mv ?successp acl2::?defines
                ?filemap ?new-echars acl2::?state)
            (vl-preprocess-fn echars defines filemap config 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 ?new-echars acl2::?state)
            (vl-preprocess-fn echars defines filemap config state)))
        (state-p1 state)))
 :rule-classes :rewrite)