		Search-engine friendly clone of the ACL2 documentation.

Primitive-functions

Eval-pkg-imports

Evaluation semantics of pkg-imports.

Signature
(eval-pkg-imports x packages) → result
Arguments: x — Guard (valuep x).; packages — Guard (package-listp packages).
Returns: result — Type (value-optionp result).

The evaluation semantics of this function depends on the package definitions in the ACL2 environment. Thus, this meta-level function takes a list of packages as argument (meant to capture the package definitions in the ACL2 environment).

We find the package with the given name. If the package does not exist, it is an error, which we model by returning nil here. The documentation of pkg-imports says that, when the string does not name a package known to ACL2 (i.e. not in the environment), the result is (logically) undefined and evaluation fails to yield a value. Thus our modeling is consistent with this documentation. In practice, calling pkg-imports on a non-package string causes an ACL2 error.

Definitions and Theorems

Function: eval-pkg-imports

(defun eval-pkg-imports (x packages)
  (declare (xargs :guard (and (valuep x)
                              (package-listp packages))))
  (let ((__function__ 'eval-pkg-imports))
    (declare (ignorable __function__))
    (if (value-case x :string)
        (b* ((x-string (value-string->get x))
             (package? (package-lookup x-string packages))
             ((when (not package?)) nil)
             (imports (package->imports package?)))
          (value-list-of (value-symbol-list imports)))
      (value-nil))))

Theorem: value-optionp-of-eval-pkg-imports

(defthm value-optionp-of-eval-pkg-imports
  (b* ((result (eval-pkg-imports x packages)))
    (value-optionp result))
  :rule-classes :rewrite)

Theorem: eval-pkg-imports-of-value-fix-x

(defthm eval-pkg-imports-of-value-fix-x
  (equal (eval-pkg-imports (value-fix x)
                           packages)
         (eval-pkg-imports x packages)))

Theorem: eval-pkg-imports-value-equiv-congruence-on-x

(defthm eval-pkg-imports-value-equiv-congruence-on-x
  (implies (value-equiv x x-equiv)
           (equal (eval-pkg-imports x packages)
                  (eval-pkg-imports x-equiv packages)))
  :rule-classes :congruence)

Theorem: eval-pkg-imports-of-package-list-fix-packages

(defthm eval-pkg-imports-of-package-list-fix-packages
  (equal (eval-pkg-imports x (package-list-fix packages))
         (eval-pkg-imports x packages)))

Theorem: eval-pkg-imports-package-list-equiv-congruence-on-packages

(defthm eval-pkg-imports-package-list-equiv-congruence-on-packages
  (implies (package-list-equiv packages packages-equiv)
           (equal (eval-pkg-imports x packages)
                  (eval-pkg-imports x packages-equiv)))
  :rule-classes :congruence)