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