		Search-engine friendly clone of the ACL2 documentation.

Primitive-functions

Eval-pkg-witness

Evaluation semantics of pkg-witness.

Signature
(eval-pkg-witness 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 definition 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-witness says that, when the string does not name a package known to ACL2 (i.e. not in the environment), evaluation yields an ACL2 hard error. Thus our modeling is consistent with this documentation.

If the package exists, we return the symbol with the package and the name of the ACL2 package witness, which is contained in the constant acl2::*pkg-witness-name*.

If the input is not a string, it is treated like the string "ACL2".

Definitions and Theorems

Function: eval-pkg-witness

(defun eval-pkg-witness (x packages)
  (declare (xargs :guard (and (valuep x)
                              (package-listp packages))))
  (let ((__function__ 'eval-pkg-witness))
    (declare (ignorable __function__))
    (b* ((x-string (if (value-case x :string)
                       (value-string->get x)
                     "ACL2"))
         (package? (package-lookup x-string packages))
         ((when (not package?)) nil))
      (value-symbol
           (make-symbol-value :package x-string
                              :name acl2::*pkg-witness-name*)))))

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

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

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

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

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

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

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

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

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

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