		Search-engine friendly clone of the ACL2 documentation.

Unparameterization

Vl-finish-unparameterized-module

Signature
(vl-finish-unparameterized-module x elabindex &key (config 'config)) → (mv new-mod new-elabindex)
Arguments: x — Guard (vl-module-p x).; elabindex — at global level.; config — Guard (vl-simpconfig-p config).
Returns: new-mod — Type (vl-module-p new-mod).

Definitions and Theorems

Function: vl-finish-unparameterized-module-fn

(defun vl-finish-unparameterized-module-fn (x elabindex config)
  (declare (xargs :stobjs (elabindex)))
  (declare (xargs :guard (and (vl-module-p x)
                              (vl-simpconfig-p config))))
  (let ((__function__ 'vl-finish-unparameterized-module))
    (declare (ignorable __function__))
    (b* (((vl-module x))
         (warnings x.warnings)
         (blob (vl-module->genblob x))
         ((wmv warnings elabindex new-blob
               :ctx x.name)
          (vl-genblob-finish-unparam blob elabindex nil config))
         (mod (vl-genblob->module new-blob x))
         (mod (change-vl-module mod
                                :warnings warnings)))
      (mv mod elabindex))))

Theorem: vl-module-p-of-vl-finish-unparameterized-module.new-mod

(defthm vl-module-p-of-vl-finish-unparameterized-module.new-mod
  (b* (((mv ?new-mod ?new-elabindex)
        (vl-finish-unparameterized-module-fn x elabindex config)))
    (vl-module-p new-mod))
  :rule-classes :rewrite)

Theorem: vl-finish-unparameterized-module-fn-of-vl-module-fix-x

(defthm vl-finish-unparameterized-module-fn-of-vl-module-fix-x
  (equal (vl-finish-unparameterized-module-fn (vl-module-fix x)
                                              elabindex config)
         (vl-finish-unparameterized-module-fn x elabindex config)))

Theorem: vl-finish-unparameterized-module-fn-vl-module-equiv-congruence-on-x

(defthm
 vl-finish-unparameterized-module-fn-vl-module-equiv-congruence-on-x
 (implies
  (vl-module-equiv x x-equiv)
  (equal
    (vl-finish-unparameterized-module-fn x elabindex config)
    (vl-finish-unparameterized-module-fn x-equiv elabindex config)))
 :rule-classes :congruence)

Theorem: vl-finish-unparameterized-module-fn-of-vl-simpconfig-fix-config

(defthm
    vl-finish-unparameterized-module-fn-of-vl-simpconfig-fix-config
  (equal (vl-finish-unparameterized-module-fn
              x elabindex (vl-simpconfig-fix config))
         (vl-finish-unparameterized-module-fn x elabindex config)))

Theorem: vl-finish-unparameterized-module-fn-vl-simpconfig-equiv-congruence-on-config

(defthm
 vl-finish-unparameterized-module-fn-vl-simpconfig-equiv-congruence-on-config
 (implies
  (vl-simpconfig-equiv config config-equiv)
  (equal
    (vl-finish-unparameterized-module-fn x elabindex config)
    (vl-finish-unparameterized-module-fn x elabindex config-equiv)))
 :rule-classes :congruence)