		Search-engine friendly clone of the ACL2 documentation.

Packages

Import-lookup

Find a symbol with a given name in a package import list.

Signature
(import-lookup name imports) → symbol?
Arguments: name — Guard (stringp name).; imports — Guard (symbol-value-listp imports).
Returns: symbol? — Type (symbol-value-optionp symbol?).

When denoting a symbol via a package name P and a (symbol) name N, the denoted symbol does not always have that package name (in the sense of the one returned by symbol-package-name). The reason is that if P imports, from another package Q, a symbol with name N, that is the denoted symbol, i.e. its symbol-package-name is Q and not P. For instance acl2::cons denotes common-lisp::cons, whose symbol-package-name is "COMMON-LISP".

This function looks up a symbol, by name, in a list of symbols that is meant to be a package import list. We return the first symbol found, if any. If none is found, we return nil.

An import list in a package definition of an ACL2 environment will have symbols with unique names; will have unique package names; this will be formalized elsewhere. Under this condition, returning the first symbol found is as good as returning any symbol with that name in the list, since there can be at most one.

Definitions and Theorems

Function: import-lookup

(defun import-lookup (name imports)
  (declare (xargs :guard (and (stringp name)
                              (symbol-value-listp imports))))
  (let ((__function__ 'import-lookup))
    (declare (ignorable __function__))
    (b* (((when (endp imports)) nil)
         (import (car imports))
         ((when (equal name (symbol-value->name import)))
          (symbol-value-fix import)))
      (import-lookup name (cdr imports)))))

Theorem: symbol-value-optionp-of-import-lookup

(defthm symbol-value-optionp-of-import-lookup
  (b* ((symbol? (import-lookup name imports)))
    (symbol-value-optionp symbol?))
  :rule-classes :rewrite)

Theorem: import-lookup-of-symbol-value-list-fix-imports

(defthm import-lookup-of-symbol-value-list-fix-imports
  (equal (import-lookup name (symbol-value-list-fix imports))
         (import-lookup name imports)))

Theorem: import-lookup-symbol-value-list-equiv-congruence-on-imports

(defthm import-lookup-symbol-value-list-equiv-congruence-on-imports
  (implies (symbol-value-list-equiv imports imports-equiv)
           (equal (import-lookup name imports)
                  (import-lookup name imports-equiv)))
  :rule-classes :congruence)