		Search-engine friendly clone of the ACL2 documentation.

Unparameterization

Vl-recover-modules-lost-from-elaboration

Signature
(vl-recover-modules-lost-from-elaboration &key pre post) → new-x
Arguments: pre — Guard (vl-design-p pre).; post — Guard (vl-design-p post).
Returns: new-x — Type (vl-design-p new-x).

Definitions and Theorems

Function: vl-recover-modules-lost-from-elaboration-fn

(defun vl-recover-modules-lost-from-elaboration-fn (pre post)
 (declare (xargs :guard (and (vl-design-p pre)
                             (vl-design-p post))))
 (let ((__function__ 'vl-recover-modules-lost-from-elaboration))
  (declare (ignorable __function__))
  (b*
   (((vl-design pre))
    ((vl-design post))
    (lost-mods
     (b* ((old-modnames (mergesort (vl-modulelist->names pre.mods)))
          (new-modnames
               (mergesort (vl-modulelist->orignames post.mods)))
          (lost-modnames (difference old-modnames new-modnames))
          (lost-mods (vl-keep-modules lost-modnames pre.mods)))
       (vl-add-lost-module-warnings lost-mods)))
    (lost-ifs
     (b*
      ((old-ifnames
            (mergesort (vl-interfacelist->names pre.interfaces)))
       (new-ifnames
          (mergesort (vl-interfacelist->orignames post.interfaces)))
       (lost-ifnames (difference old-ifnames new-ifnames))
       (lost-interfaces
            (vl-keep-interfaces lost-ifnames pre.interfaces)))
      (vl-add-lost-interface-warnings lost-interfaces))))
   (change-vl-design
        post
        :mods (append lost-mods post.mods)
        :interfaces (append lost-ifs post.interfaces)))))

Theorem: vl-design-p-of-vl-recover-modules-lost-from-elaboration

(defthm vl-design-p-of-vl-recover-modules-lost-from-elaboration
  (b*
    ((new-x (vl-recover-modules-lost-from-elaboration-fn pre post)))
    (vl-design-p new-x))
  :rule-classes :rewrite)

Theorem: vl-recover-modules-lost-from-elaboration-fn-of-vl-design-fix-pre

(defthm
   vl-recover-modules-lost-from-elaboration-fn-of-vl-design-fix-pre
 (equal
    (vl-recover-modules-lost-from-elaboration-fn (vl-design-fix pre)
                                                 post)
    (vl-recover-modules-lost-from-elaboration-fn pre post)))

Theorem: vl-recover-modules-lost-from-elaboration-fn-vl-design-equiv-congruence-on-pre

(defthm
 vl-recover-modules-lost-from-elaboration-fn-vl-design-equiv-congruence-on-pre
 (implies
  (vl-design-equiv pre pre-equiv)
  (equal
      (vl-recover-modules-lost-from-elaboration-fn pre post)
      (vl-recover-modules-lost-from-elaboration-fn pre-equiv post)))
 :rule-classes :congruence)

Theorem: vl-recover-modules-lost-from-elaboration-fn-of-vl-design-fix-post

(defthm
  vl-recover-modules-lost-from-elaboration-fn-of-vl-design-fix-post
  (equal (vl-recover-modules-lost-from-elaboration-fn
              pre (vl-design-fix post))
         (vl-recover-modules-lost-from-elaboration-fn pre post)))

Theorem: vl-recover-modules-lost-from-elaboration-fn-vl-design-equiv-congruence-on-post

(defthm
 vl-recover-modules-lost-from-elaboration-fn-vl-design-equiv-congruence-on-post
 (implies
  (vl-design-equiv post post-equiv)
  (equal
      (vl-recover-modules-lost-from-elaboration-fn pre post)
      (vl-recover-modules-lost-from-elaboration-fn pre post-equiv)))
 :rule-classes :congruence)