		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Moddb-add-modinst

Signature
(moddb-add-modinst instname modidx elab-mod moddb) → elab-mod1
Arguments: instname — Guard (name-p instname).; modidx — instantiated module.
Guard (natp modidx).; elab-mod — module to which the instance will be added.

Definitions and Theorems

Function: moddb-add-modinst

(defun moddb-add-modinst (instname modidx elab-mod moddb)
 (declare (xargs :stobjs (elab-mod moddb)))
 (declare (xargs :guard (and (name-p instname) (natp modidx))))
 (declare
  (xargs
     :guard (and (moddb-ok moddb)
                 (< modidx (moddb->nmods moddb))
                 (not (elab-mod-instname->idx instname elab-mod)))))
 (let ((__function__ 'moddb-add-modinst))
  (declare (ignorable __function__))
  (flet
   ((body
     (instname modidx elab-mod moddb)
     (b*
      ((elab-mod (elab-mod-fix elab-mod))
       (instname (mbe :logic (name-fix instname)
                      :exec instname))
       (modidx (lnfix modidx))
       ((unless
             (mbt (not (elab-mod-instname->idx instname elab-mod))))
        elab-mod)
       ((acl2::local-stobjs elab-modinst$c)
        (mv elab-mod elab-modinst$c))
       (elab-modinst$c
          (update-elab-modinst$c->instname instname elab-modinst$c))
       (elab-modinst$c
            (update-elab-modinst$c->modidx modidx elab-modinst$c))
       ((stobj-get subwires subinsts)
        ((elab-mod2 (moddb->modsi modidx moddb)))
        (mv (elab-mod->totalwires elab-mod2)
            (elab-mod->totalinsts elab-mod2)))
       ((mv subwires subinsts)
        (if (mbt (< (lnfix modidx) (moddb->nmods moddb)))
            (mv subwires subinsts)
          (mv 0 0)))
       (totalwires (elab-mod->totalwires elab-mod))
       (elab-modinst$c (update-elab-modinst$c->wire-offset
                            totalwires elab-modinst$c))
       (elab-mod
            (update-elab-mod->totalwires (+ totalwires subwires)
                                         elab-mod))
       (totalinsts (elab-mod->totalinsts elab-mod))
       (elab-modinst$c (update-elab-modinst$c->inst-offset
                            totalinsts elab-modinst$c))
       (elab-mod
            (update-elab-mod->totalinsts (+ 1 totalinsts subinsts)
                                         elab-mod))
       (elab-mod (elab-mod-add-inst elab-modinst$c elab-mod)))
      (mv elab-mod elab-modinst$c))))
   (mbe :logic (non-exec (let ((moddb (moddb-fix moddb)))
                           (body instname modidx elab-mod moddb)))
        :exec (body instname modidx elab-mod moddb)))))

Theorem: moddb-add-modinst-of-name-fix-instname

(defthm moddb-add-modinst-of-name-fix-instname
  (equal (moddb-add-modinst (name-fix instname)
                            modidx elab-mod moddb)
         (moddb-add-modinst instname modidx elab-mod moddb)))

Theorem: moddb-add-modinst-name-equiv-congruence-on-instname

(defthm moddb-add-modinst-name-equiv-congruence-on-instname
 (implies
   (name-equiv instname instname-equiv)
   (equal (moddb-add-modinst instname modidx elab-mod moddb)
          (moddb-add-modinst instname-equiv modidx elab-mod moddb)))
 :rule-classes :congruence)

Theorem: moddb-add-modinst-of-nfix-modidx

(defthm moddb-add-modinst-of-nfix-modidx
  (equal (moddb-add-modinst instname (nfix modidx)
                            elab-mod moddb)
         (moddb-add-modinst instname modidx elab-mod moddb)))

Theorem: moddb-add-modinst-nat-equiv-congruence-on-modidx

(defthm moddb-add-modinst-nat-equiv-congruence-on-modidx
 (implies
   (nat-equiv modidx modidx-equiv)
   (equal (moddb-add-modinst instname modidx elab-mod moddb)
          (moddb-add-modinst instname modidx-equiv elab-mod moddb)))
 :rule-classes :congruence)

Theorem: moddb-add-modinst-of-elab-mod$a-fix-elab-mod

(defthm moddb-add-modinst-of-elab-mod$a-fix-elab-mod
  (equal (moddb-add-modinst instname
                            modidx (elab-mod$a-fix elab-mod)
                            moddb)
         (moddb-add-modinst instname modidx elab-mod moddb)))

Theorem: moddb-add-modinst-elab-mod$a-equiv-congruence-on-elab-mod

(defthm moddb-add-modinst-elab-mod$a-equiv-congruence-on-elab-mod
 (implies
   (elab-mod$a-equiv elab-mod elab-mod-equiv)
   (equal (moddb-add-modinst instname modidx elab-mod moddb)
          (moddb-add-modinst instname modidx elab-mod-equiv moddb)))
 :rule-classes :congruence)

Theorem: moddb-add-modinst-of-moddb-fix-moddb

(defthm moddb-add-modinst-of-moddb-fix-moddb
  (equal (moddb-add-modinst instname
                            modidx elab-mod (moddb-fix moddb))
         (moddb-add-modinst instname modidx elab-mod moddb)))

Theorem: moddb-add-modinst-moddb-equiv-congruence-on-moddb

(defthm moddb-add-modinst-moddb-equiv-congruence-on-moddb
 (implies
   (moddb-equiv moddb moddb-equiv)
   (equal (moddb-add-modinst instname modidx elab-mod moddb)
          (moddb-add-modinst instname modidx elab-mod moddb-equiv)))
 :rule-classes :congruence)

Theorem: moddb-add-modinst-of-moddb-norm-moddb

(defthm moddb-add-modinst-of-moddb-norm-moddb
  (equal (moddb-add-modinst instname
                            modidx elab-mod (moddb-norm moddb))
         (moddb-add-modinst instname modidx elab-mod moddb)))

Theorem: moddb-add-modinst-moddb-norm-equiv-congruence-on-moddb

(defthm moddb-add-modinst-moddb-norm-equiv-congruence-on-moddb
 (implies
   (moddb-norm-equiv moddb moddb-equiv)
   (equal (moddb-add-modinst instname modidx elab-mod moddb)
          (moddb-add-modinst instname modidx elab-mod moddb-equiv)))
 :rule-classes :congruence)

Theorem: name-of-elab-mod$a-add-inst

(defthm name-of-elab-mod$a-add-inst
  (equal (g :name (elab-mod$a-add-inst inst mod))
         (modname-fix (g :name mod))))

Theorem: moddb-add-module1-of-moddb-add-modinst

(defthm moddb-add-module1-of-moddb-add-modinst
 (implies
  (not (moddb-modname-get-index (g :name elab-mod)
                                moddb))
  (moddb-norm-equiv
     (mv-nth 1
             (moddb-add-module1
                  (moddb-add-modinst instname modidx elab-mod moddb)
                  moddb))
     (moddb-add-modinst-to-last
          instname modidx
          (mv-nth 1
                  (moddb-add-module1 elab-mod moddb))))))