		Search-engine friendly clone of the ACL2 documentation.

Inline-mods

Vl-inline-mod-in-mod

Expand any instances of a submodule into its inlined body, throughout a module.

Signature
(vl-inline-mod-in-mod sub x) → new-mod
Arguments: sub — Guard (and (vl-module-p sub) (vl-ok-to-inline-p sub)).; x — Guard (vl-module-p x).
Returns: new-mod — Type (vl-module-p new-mod), given the guard.

Definitions and Theorems

Function: vl-inline-mod-in-mod

(defun vl-inline-mod-in-mod (sub x)
  (declare (xargs :guard (and (and (vl-module-p sub)
                                   (vl-ok-to-inline-p sub))
                              (vl-module-p x))))
  (let ((__function__ 'vl-inline-mod-in-mod))
    (declare (ignorable __function__))
    (b* (((vl-module x) x)
         (- (cw "; Inlining in ~x0.~%" x.name))
         ((when (vl-module->hands-offp x)) x)
         (nf (vl-starting-namefactory x))
         ((mv nf modinsts
              gateinsts assigns vardecls warnings)
          (vl-inline-mod-in-modinsts sub x.modinsts nf x.warnings)))
      (vl-free-namefactory nf)
      (change-vl-module x
                        :modinsts modinsts
                        :gateinsts (append gateinsts x.gateinsts)
                        :assigns (append assigns x.assigns)
                        :vardecls (append vardecls x.vardecls)
                        :warnings warnings))))

Theorem: vl-module-p-of-vl-inline-mod-in-mod

(defthm vl-module-p-of-vl-inline-mod-in-mod
  (implies (and (if (vl-module-p sub)
                    (vl-ok-to-inline-p sub)
                  'nil)
                (vl-module-p x))
           (b* ((new-mod (vl-inline-mod-in-mod sub x)))
             (vl-module-p new-mod)))
  :rule-classes :rewrite)