		Search-engine friendly clone of the ACL2 documentation.

Port-resolve

Vl-loaditems-remove-interfaceport-decls

Signature
(vl-loaditems-remove-interfaceport-decls x ss) → (mv warnings new-loaditems ifport-alist)
Arguments: x — Guard (vl-genelementlist-p x).; ss — Guard (vl-scopestack-p ss).
Returns: warnings — Type (vl-warninglist-p warnings).; new-loaditems — Type (vl-genelementlist-p new-loaditems).; ifport-alist — Type (vl-interfaceport-alist-p ifport-alist).

Definitions and Theorems

Function: vl-loaditems-remove-interfaceport-decls

(defun vl-loaditems-remove-interfaceport-decls (x ss)
  (declare (xargs :guard (and (vl-genelementlist-p x)
                              (vl-scopestack-p ss))))
  (let ((__function__ 'vl-loaditems-remove-interfaceport-decls))
    (declare (ignorable __function__))
    (b* (((when (atom x)) (mv nil nil nil))
         (warnings nil)
         ((wmv warnings rest rest-ifports)
          (vl-loaditems-remove-interfaceport-decls (cdr x)
                                                   ss))
         (x1 (vl-genelement-fix (car x))))
      (vl-genelement-case
           x1 :vl-genbase
           (b* (((unless (eq (tag x1.item) :vl-vardecl))
                 (mv warnings (cons x1 rest)
                     rest-ifports))
                ((wmv warnings ifport)
                 (vl-vardecl-is-really-interfaceport x1.item ss))
                ((unless ifport)
                 (mv warnings (cons x1 rest)
                     rest-ifports)))
             (mv warnings rest
                 (cons (cons (vl-vardecl->name x1.item) ifport)
                       rest-ifports)))
           :otherwise (mv warnings (cons x1 rest)
                          rest-ifports)))))

Theorem: vl-warninglist-p-of-vl-loaditems-remove-interfaceport-decls.warnings

(defthm
 vl-warninglist-p-of-vl-loaditems-remove-interfaceport-decls.warnings
 (b* (((mv ?warnings ?new-loaditems ?ifport-alist)
       (vl-loaditems-remove-interfaceport-decls x ss)))
   (vl-warninglist-p warnings))
 :rule-classes :rewrite)

Theorem: vl-genelementlist-p-of-vl-loaditems-remove-interfaceport-decls.new-loaditems

(defthm
 vl-genelementlist-p-of-vl-loaditems-remove-interfaceport-decls.new-loaditems
 (b* (((mv ?warnings ?new-loaditems ?ifport-alist)
       (vl-loaditems-remove-interfaceport-decls x ss)))
   (vl-genelementlist-p new-loaditems))
 :rule-classes :rewrite)

Theorem: vl-interfaceport-alist-p-of-vl-loaditems-remove-interfaceport-decls.ifport-alist

(defthm
 vl-interfaceport-alist-p-of-vl-loaditems-remove-interfaceport-decls.ifport-alist
 (b* (((mv ?warnings ?new-loaditems ?ifport-alist)
       (vl-loaditems-remove-interfaceport-decls x ss)))
   (vl-interfaceport-alist-p ifport-alist))
 :rule-classes :rewrite)

Theorem: vl-loaditems-remove-interfaceport-decls-of-vl-genelementlist-fix-x

(defthm
 vl-loaditems-remove-interfaceport-decls-of-vl-genelementlist-fix-x
 (equal
  (vl-loaditems-remove-interfaceport-decls (vl-genelementlist-fix x)
                                           ss)
  (vl-loaditems-remove-interfaceport-decls x ss)))

Theorem: vl-loaditems-remove-interfaceport-decls-vl-genelementlist-equiv-congruence-on-x

(defthm
 vl-loaditems-remove-interfaceport-decls-vl-genelementlist-equiv-congruence-on-x
 (implies
      (vl-genelementlist-equiv x x-equiv)
      (equal (vl-loaditems-remove-interfaceport-decls x ss)
             (vl-loaditems-remove-interfaceport-decls x-equiv ss)))
 :rule-classes :congruence)

Theorem: vl-loaditems-remove-interfaceport-decls-of-vl-scopestack-fix-ss

(defthm
    vl-loaditems-remove-interfaceport-decls-of-vl-scopestack-fix-ss
 (equal
  (vl-loaditems-remove-interfaceport-decls x (vl-scopestack-fix ss))
  (vl-loaditems-remove-interfaceport-decls x ss)))

Theorem: vl-loaditems-remove-interfaceport-decls-vl-scopestack-equiv-congruence-on-ss

(defthm
 vl-loaditems-remove-interfaceport-decls-vl-scopestack-equiv-congruence-on-ss
 (implies
      (vl-scopestack-equiv ss ss-equiv)
      (equal (vl-loaditems-remove-interfaceport-decls x ss)
             (vl-loaditems-remove-interfaceport-decls x ss-equiv)))
 :rule-classes :congruence)