		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Module-named->indexed

Signature
(module-named->indexed x modidx moddb) → (mv errmsg xx)
Arguments: x — Guard (module-p x).; modidx — Guard (natp modidx).; moddb — Guard (moddb-ok moddb).
Returns: xx — Type (module-p xx).

Definitions and Theorems

Function: module-named->indexed

(defun module-named->indexed (x modidx moddb)
 (declare (xargs :stobjs (moddb)))
 (declare (xargs :guard (and (module-p x)
                             (natp modidx)
                             (moddb-ok moddb))))
 (declare (xargs :guard (and (svarlist-addr-p (module-vars x))
                             (< modidx (moddb->nmods moddb)))))
 (let ((__function__ 'module-named->indexed))
   (declare (ignorable __function__))
   (b* (((module x) x)
        ((mv err1 assigns)
         (assigns-named->indexed x.assigns modidx moddb))
        ((mv err2 constraints)
         (constraintlist-named->indexed x.constraints modidx moddb))
        ((mv err3 fixups)
         (assigns-named->indexed x.fixups modidx moddb))
        ((mv err4 aliaspairs)
         (lhspairs-named->indexed x.aliaspairs modidx moddb)))
     (mv (or err1 err2 err3 err4)
         (change-module x
                        :assigns assigns
                        :constraints constraints
                        :fixups fixups
                        :aliaspairs aliaspairs)))))

Theorem: module-p-of-module-named->indexed.xx

(defthm module-p-of-module-named->indexed.xx
  (b* (((mv ?errmsg ?xx)
        (module-named->indexed x modidx moddb)))
    (module-p xx))
  :rule-classes :rewrite)

Theorem: module-named->indexed-of-module-fix-x

(defthm module-named->indexed-of-module-fix-x
  (equal (module-named->indexed (module-fix x)
                                modidx moddb)
         (module-named->indexed x modidx moddb)))

Theorem: module-named->indexed-module-equiv-congruence-on-x

(defthm module-named->indexed-module-equiv-congruence-on-x
  (implies (module-equiv x x-equiv)
           (equal (module-named->indexed x modidx moddb)
                  (module-named->indexed x-equiv modidx moddb)))
  :rule-classes :congruence)

Theorem: module-named->indexed-of-nfix-modidx

(defthm module-named->indexed-of-nfix-modidx
  (equal (module-named->indexed x (nfix modidx)
                                moddb)
         (module-named->indexed x modidx moddb)))

Theorem: module-named->indexed-nat-equiv-congruence-on-modidx

(defthm module-named->indexed-nat-equiv-congruence-on-modidx
  (implies (nat-equiv modidx modidx-equiv)
           (equal (module-named->indexed x modidx moddb)
                  (module-named->indexed x modidx-equiv moddb)))
  :rule-classes :congruence)

Theorem: module-named->indexed-of-moddb-fix-moddb

(defthm module-named->indexed-of-moddb-fix-moddb
  (equal (module-named->indexed x modidx (moddb-fix moddb))
         (module-named->indexed x modidx moddb)))

Theorem: module-named->indexed-moddb-equiv-congruence-on-moddb

(defthm module-named->indexed-moddb-equiv-congruence-on-moddb
  (implies (moddb-equiv moddb moddb-equiv)
           (equal (module-named->indexed x modidx moddb)
                  (module-named->indexed x modidx moddb-equiv)))
  :rule-classes :congruence)

Theorem: module-idxaddr-okp-of-module-named->indexed

(defthm module-idxaddr-okp-of-module-named->indexed
 (b* (((mv err mod)
       (module-named->indexed x modidx moddb)))
  (implies
       (and (moddb-ok moddb)
            (< (nfix modidx)
               (nfix (nth *moddb->nmods* moddb)))
            (not err))
       (svarlist-idxaddr-okp (module-vars mod)
                             (moddb-mod-totalwires modidx moddb)))))