		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Svar-named->indexed

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

Definitions and Theorems

Function: svar-named->indexed

(defun svar-named->indexed (x modidx moddb)
 (declare (xargs :stobjs (moddb)))
 (declare (xargs :guard (and (svar-p x)
                             (natp modidx)
                             (moddb-ok moddb))))
 (declare (xargs :guard (and (< modidx (moddb->nmods moddb))
                             (svar-addr-p x))))
 (let ((__function__ 'svar-named->indexed))
  (declare (ignorable __function__))
  (b* ((x (svar-addr-fix x))
       (addr (svar->address x))
       ((address addr))
       ((unless (eql 0 addr.scope))
        (mv nil
            (change-svar x
                         :name (change-address addr :index nil))))
       (idx (moddb-path->wireidx addr.path modidx moddb))
       ((unless idx)
        (mv (msg "Did not find wire: ~x0 in module ~s1~%"
                 addr.path
                 (stobj-let ((elab-mod (moddb->modsi modidx moddb)))
                            (name)
                            (elab-mod->name elab-mod)
                            name))
            (change-svar x
                         :name (change-address addr :index nil)))))
    (mv nil
        (change-svar x
                     :name (change-address addr :index idx))))))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: svar-named->indexed-idxaddr-ok

(defthm svar-named->indexed-idxaddr-ok
 (b* (((mv ?err newx)
       (svar-named->indexed x modidx moddb)))
  (implies (and (moddb-ok moddb)
                (< (nfix modidx)
                   (nfix (nth *moddb->nmods* moddb))))
           (svar-idxaddr-okp newx
                             (moddb-mod-totalwires modidx moddb)))))