		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Elab-mod$c-add-wire

Signature
(elab-mod$c-add-wire wire elab-mod$c) → elab-mod$c
Arguments: wire — Guard (wire-p wire).

Definitions and Theorems

Function: elab-mod$c-add-wire

(defun elab-mod$c-add-wire (wire elab-mod$c)
 (declare (xargs :stobjs (elab-mod$c)))
 (declare (xargs :guard (wire-p wire)))
 (declare (xargs :guard (elab-mod$c-wires-ok elab-mod$c)))
 (let ((__function__ 'elab-mod$c-add-wire))
  (declare (ignorable __function__))
  (b*
   ((idx (lnfix (elab-mod$c->nwires elab-mod$c)))
    (wire (wire-fix wire))
    (name (wire->name wire))
    ((when (elab-mod$c->wirename-idxes-boundp name elab-mod$c))
     (cw "In ~x2: Wire already exists in ~s0: ~x1~%"
         (elab-mod$c->name elab-mod$c)
         name __function__)
     elab-mod$c)
    (elab-mod$c (if (<= (elab-mod$c->wiretable-length elab-mod$c)
                        idx)
                    (resize-elab-mod$c->wiretable (max 16 (* 2 idx))
                                                  elab-mod$c)
                  elab-mod$c))
    (elab-mod$c (update-elab-mod$c->nwires (1+ idx)
                                           elab-mod$c))
    (elab-mod$c
         (update-elab-mod$c->wiretablei idx wire elab-mod$c)))
   (elab-mod$c->wirename-idxes-put name idx elab-mod$c))))

Theorem: elab-mod$c-wires-ok-of-elab-mod$c-add-wire

(defthm elab-mod$c-wires-ok-of-elab-mod$c-add-wire
  (implies
       (elab-mod$c-wires-ok elab-mod$c)
       (elab-mod$c-wires-ok (elab-mod$c-add-wire wire elab-mod$c))))

Theorem: wirelist-fix-of-update-nth

(defthm wirelist-fix-of-update-nth
  (implies (<= (nfix n) (len x))
           (equal (wirelist-fix (update-nth n v x))
                  (update-nth n (wire-fix v)
                              (wirelist-fix x)))))

Theorem: wirelist-fix-of-take

(defthm wirelist-fix-of-take
  (implies (<= (nfix n) (len x))
           (equal (wirelist-fix (take n x))
                  (take n (wirelist-fix x)))))

Theorem: elab-mod$c-add-wire-update

(defthm elab-mod$c-add-wire-update
 (implies
   (elab-mod$c-wires-ok elab-mod$c)
   (equal
        (elab-mod$c-wire-abstraction
             (elab-mod$c-add-wire wire elab-mod$c))
        (let ((orig-wires (elab-mod$c-wire-abstraction elab-mod$c)))
          (if (member (wire->name wire)
                      (wirelist->names orig-wires))
              orig-wires
            (append orig-wires (list (wire-fix wire))))))))

Theorem: elab-mod$cp-of-add-wire

(defthm elab-mod$cp-of-add-wire
  (implies (elab-mod$cp elab-mod$c)
           (elab-mod$cp (elab-mod$c-add-wire name elab-mod$c))))

Theorem: elab-mod$cp-add-wire-frame

(defthm elab-mod$cp-add-wire-frame
  (implies (and (not (equal n *elab-mod$c->nwires*))
                (not (equal n *elab-mod$c->wiretablei*))
                (not (equal n *elab-mod$c->wirename-idxes-get*)))
           (equal (nth n (elab-mod$c-add-wire wire elab-mod$c))
                  (nth n elab-mod$c))))

Theorem: elab-mod$cp-add-wire-irrel

(defthm elab-mod$cp-add-wire-irrel
  (implies
       (and (not (equal n *elab-mod$c->nwires*))
            (not (equal n *elab-mod$c->wiretablei*))
            (not (equal n *elab-mod$c->wirename-idxes-get*)))
       (equal (elab-mod$c-add-wire wire (update-nth n v elab-mod$c))
              (update-nth n v
                          (elab-mod$c-add-wire wire elab-mod$c)))))

Theorem: elab-mod$c-add-wire-of-wire-fix-wire

(defthm elab-mod$c-add-wire-of-wire-fix-wire
  (equal (elab-mod$c-add-wire (wire-fix wire)
                              elab-mod$c)
         (elab-mod$c-add-wire wire elab-mod$c)))

Theorem: elab-mod$c-add-wire-wire-equiv-congruence-on-wire

(defthm elab-mod$c-add-wire-wire-equiv-congruence-on-wire
  (implies (wire-equiv wire wire-equiv)
           (equal (elab-mod$c-add-wire wire elab-mod$c)
                  (elab-mod$c-add-wire wire-equiv elab-mod$c)))
  :rule-classes :congruence)