		Search-engine friendly clone of the ACL2 documentation.

Mod-internal-paths

Follow-esim-path

Walk down a list of instance names (or a path) and retrieve the ESIM module it points to.

(follow-esim-path instnames mod) returns an ESIM module on success, or nil for failure.

We are given instnames, which should be a list of instance names, and mod, which should be a good esim module. We try to follow these names down through the occurrences of mod and return the submodule they point to.

Note that instnames need not be a true-listp, so you can use this function to look up the module associated with an ESIM path without needing to list-fix the path or similar.

Definitions and Theorems

Function: follow-esim-path

(defun follow-esim-path (instnames mod)
  "Returns SUBMOD or NIL."
  (declare (xargs :guard t))
  (b* (((when (atom instnames)) mod)
       (name1 (car instnames))
       (occ (cdr (hons-get name1 (make-fast-alist (occmap mod))))))
    (and occ
         (follow-esim-path (cdr instnames)
                           (gpl :op occ)))))

Theorem: good-esim-modulep-of-follow-esim-path

(defthm good-esim-modulep-of-follow-esim-path
  (implies (good-esim-modulep mod)
           (good-esim-modulep (follow-esim-path instnames mod))))