		Search-engine friendly clone of the ACL2 documentation.

Unparameterization

Vl-create-unparameterized-interface

Signature
(vl-create-unparameterized-interface x name final-paramdecls final-ports elabindex ledger &key (config 'config)) → (mv new-mod keylist new-elabindex ledger)
Arguments: x — Guard (vl-interface-p x).; name — New name including parameter disambiguation.
Guard (stringp name).; final-paramdecls — Guard (vl-paramdecllist-p final-paramdecls).; final-ports — Guard (vl-portlist-p final-ports).; elabindex — at global scope.; ledger — Guard (vl-unparam-ledger-p ledger).; config — Guard (vl-simpconfig-p config).
Returns: new-mod — Type (vl-interface-p new-mod).; keylist — signatures for this interface.
Type (vl-unparam-instkeylist-p keylist).; ledger — Type (vl-unparam-ledger-p ledger).

Definitions and Theorems

Function: vl-create-unparameterized-interface-fn

(defun vl-create-unparameterized-interface-fn
       (x name final-paramdecls
          final-ports elabindex ledger config)
  (declare (xargs :stobjs (elabindex)))
  (declare (xargs :guard (and (vl-interface-p x)
                              (stringp name)
                              (vl-paramdecllist-p final-paramdecls)
                              (vl-portlist-p final-ports)
                              (vl-unparam-ledger-p ledger)
                              (vl-simpconfig-p config))))
  (let ((__function__ 'vl-create-unparameterized-interface))
    (declare (ignorable __function__))
    (b* ((name (string-fix name))
         (x (change-vl-interface x
                                 :name name
                                 :paramdecls final-paramdecls
                                 :ports final-ports))
         ((vl-interface x))
         (warnings x.warnings)
         (blob (vl-interface->genblob x))
         ((wmv warnings
               keylist new-blob elabindex ledger
               :ctx name)
          (vl-genblob-resolve blob elabindex ledger nil))
         (mod (vl-genblob->interface new-blob x))
         (mod (change-vl-interface mod
                                   :warnings warnings)))
      (mv mod keylist elabindex ledger))))

Theorem: vl-interface-p-of-vl-create-unparameterized-interface.new-mod

(defthm
      vl-interface-p-of-vl-create-unparameterized-interface.new-mod
  (b* (((mv ?new-mod
            ?keylist ?new-elabindex ?ledger)
        (vl-create-unparameterized-interface-fn
             x name final-paramdecls
             final-ports elabindex ledger config)))
    (vl-interface-p new-mod))
  :rule-classes :rewrite)

Theorem: vl-unparam-instkeylist-p-of-vl-create-unparameterized-interface.keylist

(defthm
 vl-unparam-instkeylist-p-of-vl-create-unparameterized-interface.keylist
 (b* (((mv ?new-mod
           ?keylist ?new-elabindex ?ledger)
       (vl-create-unparameterized-interface-fn
            x name final-paramdecls
            final-ports elabindex ledger config)))
   (vl-unparam-instkeylist-p keylist))
 :rule-classes :rewrite)

Theorem: vl-unparam-ledger-p-of-vl-create-unparameterized-interface.ledger

(defthm
  vl-unparam-ledger-p-of-vl-create-unparameterized-interface.ledger
  (b* (((mv ?new-mod
            ?keylist ?new-elabindex ?ledger)
        (vl-create-unparameterized-interface-fn
             x name final-paramdecls
             final-ports elabindex ledger config)))
    (vl-unparam-ledger-p ledger))
  :rule-classes :rewrite)

Theorem: vl-create-unparameterized-interface-fn-of-vl-interface-fix-x

(defthm vl-create-unparameterized-interface-fn-of-vl-interface-fix-x
  (equal (vl-create-unparameterized-interface-fn
              (vl-interface-fix x)
              name final-paramdecls
              final-ports elabindex ledger config)
         (vl-create-unparameterized-interface-fn
              x name final-paramdecls
              final-ports elabindex ledger config)))

Theorem: vl-create-unparameterized-interface-fn-vl-interface-equiv-congruence-on-x

(defthm
 vl-create-unparameterized-interface-fn-vl-interface-equiv-congruence-on-x
 (implies (vl-interface-equiv x x-equiv)
          (equal (vl-create-unparameterized-interface-fn
                      x name final-paramdecls
                      final-ports elabindex ledger config)
                 (vl-create-unparameterized-interface-fn
                      x-equiv name final-paramdecls
                      final-ports elabindex ledger config)))
 :rule-classes :congruence)

Theorem: vl-create-unparameterized-interface-fn-of-str-fix-name

(defthm vl-create-unparameterized-interface-fn-of-str-fix-name
  (equal (vl-create-unparameterized-interface-fn
              x (str-fix name)
              final-paramdecls
              final-ports elabindex ledger config)
         (vl-create-unparameterized-interface-fn
              x name final-paramdecls
              final-ports elabindex ledger config)))

Theorem: vl-create-unparameterized-interface-fn-streqv-congruence-on-name

(defthm
   vl-create-unparameterized-interface-fn-streqv-congruence-on-name
  (implies (streqv name name-equiv)
           (equal (vl-create-unparameterized-interface-fn
                       x name final-paramdecls
                       final-ports elabindex ledger config)
                  (vl-create-unparameterized-interface-fn
                       x name-equiv final-paramdecls
                       final-ports elabindex ledger config)))
  :rule-classes :congruence)

Theorem: vl-create-unparameterized-interface-fn-of-vl-paramdecllist-fix-final-paramdecls

(defthm
 vl-create-unparameterized-interface-fn-of-vl-paramdecllist-fix-final-paramdecls
 (equal (vl-create-unparameterized-interface-fn
             x name
             (vl-paramdecllist-fix final-paramdecls)
             final-ports elabindex ledger config)
        (vl-create-unparameterized-interface-fn
             x name final-paramdecls
             final-ports elabindex ledger config)))

Theorem: vl-create-unparameterized-interface-fn-vl-paramdecllist-equiv-congruence-on-final-paramdecls

(defthm
 vl-create-unparameterized-interface-fn-vl-paramdecllist-equiv-congruence-on-final-paramdecls
 (implies
    (vl-paramdecllist-equiv final-paramdecls final-paramdecls-equiv)
    (equal (vl-create-unparameterized-interface-fn
                x name final-paramdecls
                final-ports elabindex ledger config)
           (vl-create-unparameterized-interface-fn
                x name final-paramdecls-equiv
                final-ports elabindex ledger config)))
 :rule-classes :congruence)

Theorem: vl-create-unparameterized-interface-fn-of-vl-portlist-fix-final-ports

(defthm
 vl-create-unparameterized-interface-fn-of-vl-portlist-fix-final-ports
 (equal (vl-create-unparameterized-interface-fn
             x name final-paramdecls
             (vl-portlist-fix final-ports)
             elabindex ledger config)
        (vl-create-unparameterized-interface-fn
             x name final-paramdecls
             final-ports elabindex ledger config)))

Theorem: vl-create-unparameterized-interface-fn-vl-portlist-equiv-congruence-on-final-ports

(defthm
 vl-create-unparameterized-interface-fn-vl-portlist-equiv-congruence-on-final-ports
 (implies (vl-portlist-equiv final-ports final-ports-equiv)
          (equal (vl-create-unparameterized-interface-fn
                      x name final-paramdecls
                      final-ports elabindex ledger config)
                 (vl-create-unparameterized-interface-fn
                      x
                      name final-paramdecls final-ports-equiv
                      elabindex ledger config)))
 :rule-classes :congruence)

Theorem: vl-create-unparameterized-interface-fn-of-vl-unparam-ledger-fix-ledger

(defthm
 vl-create-unparameterized-interface-fn-of-vl-unparam-ledger-fix-ledger
 (equal (vl-create-unparameterized-interface-fn
             x name final-paramdecls final-ports
             elabindex (vl-unparam-ledger-fix ledger)
             config)
        (vl-create-unparameterized-interface-fn
             x name final-paramdecls
             final-ports elabindex ledger config)))

Theorem: vl-create-unparameterized-interface-fn-vl-unparam-ledger-equiv-congruence-on-ledger

(defthm
 vl-create-unparameterized-interface-fn-vl-unparam-ledger-equiv-congruence-on-ledger
 (implies (vl-unparam-ledger-equiv ledger ledger-equiv)
          (equal (vl-create-unparameterized-interface-fn
                      x name final-paramdecls
                      final-ports elabindex ledger config)
                 (vl-create-unparameterized-interface-fn
                      x name final-paramdecls final-ports
                      elabindex ledger-equiv config)))
 :rule-classes :congruence)

Theorem: vl-create-unparameterized-interface-fn-of-vl-simpconfig-fix-config

(defthm
 vl-create-unparameterized-interface-fn-of-vl-simpconfig-fix-config
 (equal (vl-create-unparameterized-interface-fn
             x name
             final-paramdecls final-ports elabindex
             ledger (vl-simpconfig-fix config))
        (vl-create-unparameterized-interface-fn
             x name final-paramdecls
             final-ports elabindex ledger config)))

Theorem: vl-create-unparameterized-interface-fn-vl-simpconfig-equiv-congruence-on-config

(defthm
 vl-create-unparameterized-interface-fn-vl-simpconfig-equiv-congruence-on-config
 (implies (vl-simpconfig-equiv config config-equiv)
          (equal (vl-create-unparameterized-interface-fn
                      x name final-paramdecls
                      final-ports elabindex ledger config)
                 (vl-create-unparameterized-interface-fn
                      x name final-paramdecls final-ports
                      elabindex ledger config-equiv)))
 :rule-classes :congruence)