Evaluation semantics of pkg-witness.
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
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
If the input is not a string,
it is treated like the string
(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*)))))
(defthm maybe-valuep-of-eval-pkg-witness (b* ((result (eval-pkg-witness x packages))) (maybe-valuep result)) :rule-classes :rewrite)
(defthm eval-pkg-witness-of-value-fix-x (equal (eval-pkg-witness (value-fix x) packages) (eval-pkg-witness x packages)))
(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)
(defthm eval-pkg-witness-of-package-list-fix-packages (equal (eval-pkg-witness x (package-list-fix packages)) (eval-pkg-witness x 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)