		Search-engine friendly clone of the ACL2 documentation.

Blankargs

Vl-module-blankargs

Fill in blank arguments throughout a vl-module-p.

Signature
(vl-module-blankargs x ss) → new-x
Arguments: x — Guard (vl-module-p x).; ss — Guard (vl-scopestack-p ss).
Returns: new-x — Type (vl-module-p new-x).

We rewrite all module instances with vl-modinst-blankargs and all gate instances with vl-gateinst-blankargs.

Definitions and Theorems

Function: vl-module-blankargs

(defun vl-module-blankargs (x ss)
  (declare (xargs :guard (and (vl-module-p x)
                              (vl-scopestack-p ss))))
  (let ((__function__ 'vl-module-blankargs))
    (declare (ignorable __function__))
    (b* ((x (vl-module-fix x))
         ((when (vl-module->hands-offp x)) x)
         ((vl-module x) x)
         (ss (vl-scopestack-push x ss))
         (warnings (vl-module->warnings x))
         (nf (vl-starting-namefactory x))
         ((mv warnings modinsts vardecls1 nf)
          (vl-modinstlist-blankargs x.modinsts ss nf warnings))
         ((mv warnings gateinsts vardecls2 nf)
          (vl-gateinstlist-blankargs x.gateinsts nf warnings))
         (- (vl-free-namefactory nf))
         (all-vardecls (append vardecls1 vardecls2 x.vardecls)))
      (change-vl-module x
                        :modinsts modinsts
                        :gateinsts gateinsts
                        :vardecls all-vardecls
                        :warnings warnings))))

Theorem: vl-module-p-of-vl-module-blankargs

(defthm vl-module-p-of-vl-module-blankargs
  (b* ((new-x (vl-module-blankargs x ss)))
    (vl-module-p new-x))
  :rule-classes :rewrite)

Theorem: vl-module-blankargs-of-vl-module-fix-x

(defthm vl-module-blankargs-of-vl-module-fix-x
  (equal (vl-module-blankargs (vl-module-fix x)
                              ss)
         (vl-module-blankargs x ss)))

Theorem: vl-module-blankargs-vl-module-equiv-congruence-on-x

(defthm vl-module-blankargs-vl-module-equiv-congruence-on-x
  (implies (vl-module-equiv x x-equiv)
           (equal (vl-module-blankargs x ss)
                  (vl-module-blankargs x-equiv ss)))
  :rule-classes :congruence)

Theorem: vl-module-blankargs-of-vl-scopestack-fix-ss

(defthm vl-module-blankargs-of-vl-scopestack-fix-ss
  (equal (vl-module-blankargs x (vl-scopestack-fix ss))
         (vl-module-blankargs x ss)))

Theorem: vl-module-blankargs-vl-scopestack-equiv-congruence-on-ss

(defthm vl-module-blankargs-vl-scopestack-equiv-congruence-on-ss
  (implies (vl-scopestack-equiv ss ss-equiv)
           (equal (vl-module-blankargs x ss)
                  (vl-module-blankargs x ss-equiv)))
  :rule-classes :congruence)