Evaluation semantics of intern-in-package-of-symbol.
(eval-intern-in-package-of-symbol x y packages) → 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 of the second symbol argument.
If the package does not exist, it is an error,
which we formalize by returning
If a package is found, we check whether its import list includes a symbol whose name is the first string argument. If it does, that symbol is the result. Otherwise, we return a symbol consisting of the package name and the first string argument name.
Function:
(defun eval-intern-in-package-of-symbol (x y packages) (declare (xargs :guard (and (valuep x) (valuep y) (package-listp packages)))) (let ((__function__ 'eval-intern-in-package-of-symbol)) (declare (ignorable __function__)) (if (and (value-case x :string) (value-case y :symbol)) (b* ((x-string (value-string->get x)) (y-symbol (value-symbol->get y)) (y-package (symbol-value->package y-symbol)) (package? (package-lookup y-package packages)) ((when (not package?)) nil) (imports (package->imports package?)) (symbol? (import-lookup x-string imports)) ((when symbol?) (value-symbol symbol?))) (value-symbol (make-symbol-value :package y-package :name x-string))) (value-nil))))
Theorem:
(defthm value-optionp-of-eval-intern-in-package-of-symbol (b* ((result (eval-intern-in-package-of-symbol x y packages))) (value-optionp result)) :rule-classes :rewrite)
Theorem:
(defthm eval-intern-in-package-of-symbol-of-value-fix-x (equal (eval-intern-in-package-of-symbol (value-fix x) y packages) (eval-intern-in-package-of-symbol x y packages)))
Theorem:
(defthm eval-intern-in-package-of-symbol-value-equiv-congruence-on-x (implies (value-equiv x x-equiv) (equal (eval-intern-in-package-of-symbol x y packages) (eval-intern-in-package-of-symbol x-equiv y packages))) :rule-classes :congruence)
Theorem:
(defthm eval-intern-in-package-of-symbol-of-value-fix-y (equal (eval-intern-in-package-of-symbol x (value-fix y) packages) (eval-intern-in-package-of-symbol x y packages)))
Theorem:
(defthm eval-intern-in-package-of-symbol-value-equiv-congruence-on-y (implies (value-equiv y y-equiv) (equal (eval-intern-in-package-of-symbol x y packages) (eval-intern-in-package-of-symbol x y-equiv packages))) :rule-classes :congruence)
Theorem:
(defthm eval-intern-in-package-of-symbol-of-package-list-fix-packages (equal (eval-intern-in-package-of-symbol x y (package-list-fix packages)) (eval-intern-in-package-of-symbol x y packages)))
Theorem:
(defthm eval-intern-in-package-of-symbol-package-list-equiv-congruence-on-packages (implies (package-list-equiv packages packages-equiv) (equal (eval-intern-in-package-of-symbol x y packages) (eval-intern-in-package-of-symbol x y packages-equiv))) :rule-classes :congruence)