		Search-engine friendly clone of the ACL2 documentation.

Loader

Vl-load

Wrapper for vl-load-main that also reports errors or (with some configuration) can print other information.

Signature
(vl-load config &key (state 'state)) → (mv result state)
Arguments: config — Guard (vl-loadconfig-p config).
Returns: result — Type (vl-loadresult-p result).; state — Type (state-p1 state), given (force (state-p1 state)).

This is very similar to vl-load-main, but calls vl-load-summary afterwards.

Definitions and Theorems

Function: vl-load-fn

(defun
     vl-load-fn (config state)
     (declare (xargs :stobjs (state)))
     (declare (xargs :guard (vl-loadconfig-p config)))
     (let ((__function__ 'vl-load))
          (declare (ignorable __function__))
          (b* (((vl-loadconfig config)
                (vl-loadconfig-clean config))
               ((mv result state)
                (time$ (vl-load-main config state)
                       :msg "; vl-load-main: ~st sec, ~sa bytes~%"
                       :mintime config.mintime)))
              (clear-memoize-table 'vl-actually-report-parse-error)
              (vl-gc)
              (vl-load-summary config result)
              (mv result state))))

Theorem: vl-loadresult-p-of-vl-load.result

(defthm vl-loadresult-p-of-vl-load.result
        (b* (((mv ?result acl2::?state)
              (vl-load-fn config state)))
            (vl-loadresult-p result))
        :rule-classes :rewrite)

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

(defthm state-p1-of-vl-load.state
        (implies (force (state-p1 state))
                 (b* (((mv ?result acl2::?state)
                       (vl-load-fn config state)))
                     (state-p1 state)))
        :rule-classes :rewrite)

Subtopics

Vl-filemap: Mapping of source files to their contents.