		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.