		Search-engine friendly clone of the ACL2 documentation.

Primitive-functions

Eval-intern-in-package-of-symbol

Evaluation semantics of intern-in-package-of-symbol.

Signature
(eval-intern-in-package-of-symbol x y packages) → result
Arguments: x — Guard (valuep x).; y — Guard (valuep y).; 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 of the second symbol argument. If the package does not exist, it is an error, which we formalize by returning nil instead of a value. Under suitable well-formedness conditions on ACL2 programs and evaluation states, the package should always exist, because only symbols from existing packages can be manipulated during evaluation. This will be proved formally eventually, but here we define a defensive evaluation semantics, which is common practice in programming language formalizations.

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.

Definitions and Theorems

Function: eval-intern-in-package-of-symbol

(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: value-optionp-of-eval-intern-in-package-of-symbol

(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: eval-intern-in-package-of-symbol-of-value-fix-x

(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: eval-intern-in-package-of-symbol-value-equiv-congruence-on-x

(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: eval-intern-in-package-of-symbol-of-value-fix-y

(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: eval-intern-in-package-of-symbol-value-equiv-congruence-on-y

(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: eval-intern-in-package-of-symbol-of-package-list-fix-packages

(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: eval-intern-in-package-of-symbol-package-list-equiv-congruence-on-packages

(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)