• Top

• Sv::vl-moddb.lisp

Vl-plainarglist-portinfo

Signature

(vl-plainarglist-portinfo x y argindex ss scopes inst-modname 
                          inst-ss inst-scopes arraysize) 
 
  → 
(mv vttree portinfo)

Arguments

x — Guard (vl-plainarglist-p x).

y — Guard (vl-portlist-p y).

argindex — Guard (natp argindex).

ss — Guard (vl-scopestack-p ss).

scopes — Guard (vl-elabscopes-p scopes).

inst-modname — Guard (stringp inst-modname).

inst-ss — Guard (vl-scopestack-p inst-ss).

inst-scopes — Guard (vl-elabscopes-p inst-scopes).

arraysize — Guard (maybe-posp arraysize).

Returns

vttree — Type (and (vttree-p vttree) (sv::svarlist-addr-p (sv::constraintlist-vars (vttree->constraints vttree)))) .

portinfo — Type (vl-portinfolist-p portinfo).

Definitions and Theorems

Function: vl-plainarglist-portinfo

(defun vl-plainarglist-portinfo (x y argindex ss scopes inst-modname
                                   inst-ss inst-scopes arraysize)
 (declare (xargs :guard (and (vl-plainarglist-p x)
                             (vl-portlist-p y)
                             (natp argindex)
                             (vl-scopestack-p ss)
                             (vl-elabscopes-p scopes)
                             (stringp inst-modname)
                             (vl-scopestack-p inst-ss)
                             (vl-elabscopes-p inst-scopes)
                             (maybe-posp arraysize))))
 (declare (xargs :guard (eql (len x) (len y))))
 (let ((__function__ 'vl-plainarglist-portinfo))
  (declare (ignorable __function__))
  (if (atom x)
      (mv nil nil)
    (b* ((vttree nil)
         ((vmv vttree portinfo1)
          (vl-plainarg-portinfo (car x)
                                (car y)
                                argindex ss scopes inst-modname
                                inst-ss inst-scopes arraysize))
         ((vmv vttree portinfo2)
          (vl-plainarglist-portinfo (cdr x)
                                    (cdr y)
                                    (1+ (lnfix argindex))
                                    ss scopes inst-modname
                                    inst-ss inst-scopes arraysize)))
      (mv vttree (cons portinfo1 portinfo2))))))

Theorem: return-type-of-vl-plainarglist-portinfo.vttree

(defthm return-type-of-vl-plainarglist-portinfo.vttree
 (b* (((mv ?vttree ?portinfo)
       (vl-plainarglist-portinfo x y argindex ss scopes inst-modname
                                 inst-ss inst-scopes arraysize)))
  (and
      (vttree-p vttree)
      (sv::svarlist-addr-p
           (sv::constraintlist-vars (vttree->constraints vttree)))))
 :rule-classes :rewrite)

Theorem: vl-portinfolist-p-of-vl-plainarglist-portinfo.portinfo

(defthm vl-portinfolist-p-of-vl-plainarglist-portinfo.portinfo
 (b* (((mv ?vttree ?portinfo)
       (vl-plainarglist-portinfo x y argindex ss scopes inst-modname
                                 inst-ss inst-scopes arraysize)))
   (vl-portinfolist-p portinfo))
 :rule-classes :rewrite)

Theorem: vars-of-vl-plainarglist-portinfo

(defthm vars-of-vl-plainarglist-portinfo
 (b* (((mv ?vttree ?portinfo)
       (vl-plainarglist-portinfo x y argindex ss scopes inst-modname
                                 inst-ss inst-scopes arraysize)))
   (and (sv::svarlist-addr-p (vl-portinfolist-vars portinfo)))))

Theorem: vl-plainarglist-portinfo-of-vl-plainarglist-fix-x

(defthm vl-plainarglist-portinfo-of-vl-plainarglist-fix-x
  (equal
       (vl-plainarglist-portinfo (vl-plainarglist-fix x)
                                 y argindex ss scopes inst-modname
                                 inst-ss inst-scopes arraysize)
       (vl-plainarglist-portinfo x y argindex ss scopes inst-modname
                                 inst-ss inst-scopes arraysize)))

Theorem: vl-plainarglist-portinfo-vl-plainarglist-equiv-congruence-on-x

(defthm
     vl-plainarglist-portinfo-vl-plainarglist-equiv-congruence-on-x
 (implies
  (vl-plainarglist-equiv x x-equiv)
  (equal
       (vl-plainarglist-portinfo x y argindex ss scopes inst-modname
                                 inst-ss inst-scopes arraysize)
       (vl-plainarglist-portinfo x-equiv
                                 y argindex ss scopes inst-modname
                                 inst-ss inst-scopes arraysize)))
 :rule-classes :congruence)

Theorem: vl-plainarglist-portinfo-of-vl-portlist-fix-y

(defthm vl-plainarglist-portinfo-of-vl-portlist-fix-y
  (equal
       (vl-plainarglist-portinfo x (vl-portlist-fix y)
                                 argindex ss scopes inst-modname
                                 inst-ss inst-scopes arraysize)
       (vl-plainarglist-portinfo x y argindex ss scopes inst-modname
                                 inst-ss inst-scopes arraysize)))

Theorem: vl-plainarglist-portinfo-vl-portlist-equiv-congruence-on-y

(defthm vl-plainarglist-portinfo-vl-portlist-equiv-congruence-on-y
 (implies
  (vl-portlist-equiv y y-equiv)
  (equal
   (vl-plainarglist-portinfo x y argindex ss scopes inst-modname
                             inst-ss inst-scopes arraysize)
   (vl-plainarglist-portinfo x
                             y-equiv argindex ss scopes inst-modname
                             inst-ss inst-scopes arraysize)))
 :rule-classes :congruence)

Theorem: vl-plainarglist-portinfo-of-nfix-argindex

(defthm vl-plainarglist-portinfo-of-nfix-argindex
  (equal
       (vl-plainarglist-portinfo x y (nfix argindex)
                                 ss scopes inst-modname
                                 inst-ss inst-scopes arraysize)
       (vl-plainarglist-portinfo x y argindex ss scopes inst-modname
                                 inst-ss inst-scopes arraysize)))

Theorem: vl-plainarglist-portinfo-nat-equiv-congruence-on-argindex

(defthm vl-plainarglist-portinfo-nat-equiv-congruence-on-argindex
 (implies
  (acl2::nat-equiv argindex argindex-equiv)
  (equal
   (vl-plainarglist-portinfo x y argindex ss scopes inst-modname
                             inst-ss inst-scopes arraysize)
   (vl-plainarglist-portinfo x
                             y argindex-equiv ss scopes inst-modname
                             inst-ss inst-scopes arraysize)))
 :rule-classes :congruence)

Theorem: vl-plainarglist-portinfo-of-vl-scopestack-fix-ss

(defthm vl-plainarglist-portinfo-of-vl-scopestack-fix-ss
  (equal
       (vl-plainarglist-portinfo x y argindex (vl-scopestack-fix ss)
                                 scopes inst-modname
                                 inst-ss inst-scopes arraysize)
       (vl-plainarglist-portinfo x y argindex ss scopes inst-modname
                                 inst-ss inst-scopes arraysize)))

Theorem: vl-plainarglist-portinfo-vl-scopestack-equiv-congruence-on-ss

(defthm
      vl-plainarglist-portinfo-vl-scopestack-equiv-congruence-on-ss
 (implies
  (vl-scopestack-equiv ss ss-equiv)
  (equal
   (vl-plainarglist-portinfo x y argindex ss scopes inst-modname
                             inst-ss inst-scopes arraysize)
   (vl-plainarglist-portinfo x
                             y argindex ss-equiv scopes inst-modname
                             inst-ss inst-scopes arraysize)))
 :rule-classes :congruence)

Theorem: vl-plainarglist-portinfo-of-vl-elabscopes-fix-scopes

(defthm vl-plainarglist-portinfo-of-vl-elabscopes-fix-scopes
 (equal
  (vl-plainarglist-portinfo x
                            y argindex ss (vl-elabscopes-fix scopes)
                            inst-modname
                            inst-ss inst-scopes arraysize)
  (vl-plainarglist-portinfo x y argindex ss scopes inst-modname
                            inst-ss inst-scopes arraysize)))

Theorem: vl-plainarglist-portinfo-vl-elabscopes-equiv-congruence-on-scopes

(defthm
  vl-plainarglist-portinfo-vl-elabscopes-equiv-congruence-on-scopes
 (implies
  (vl-elabscopes-equiv scopes scopes-equiv)
  (equal
   (vl-plainarglist-portinfo x y argindex ss scopes inst-modname
                             inst-ss inst-scopes arraysize)
   (vl-plainarglist-portinfo x
                             y argindex ss scopes-equiv inst-modname
                             inst-ss inst-scopes arraysize)))
 :rule-classes :congruence)

Theorem: vl-plainarglist-portinfo-of-str-fix-inst-modname

(defthm vl-plainarglist-portinfo-of-str-fix-inst-modname
  (equal
       (vl-plainarglist-portinfo x y argindex
                                 ss scopes (str-fix inst-modname)
                                 inst-ss inst-scopes arraysize)
       (vl-plainarglist-portinfo x y argindex ss scopes inst-modname
                                 inst-ss inst-scopes arraysize)))

Theorem: vl-plainarglist-portinfo-streqv-congruence-on-inst-modname

(defthm vl-plainarglist-portinfo-streqv-congruence-on-inst-modname
 (implies
  (streqv inst-modname inst-modname-equiv)
  (equal
   (vl-plainarglist-portinfo x y argindex ss scopes inst-modname
                             inst-ss inst-scopes arraysize)
   (vl-plainarglist-portinfo x
                             y argindex ss scopes inst-modname-equiv
                             inst-ss inst-scopes arraysize)))
 :rule-classes :congruence)

Theorem: vl-plainarglist-portinfo-of-vl-scopestack-fix-inst-ss

(defthm vl-plainarglist-portinfo-of-vl-scopestack-fix-inst-ss
 (equal
  (vl-plainarglist-portinfo x y argindex ss scopes
                            inst-modname (vl-scopestack-fix inst-ss)
                            inst-scopes arraysize)
  (vl-plainarglist-portinfo x y argindex ss scopes inst-modname
                            inst-ss inst-scopes arraysize)))

Theorem: vl-plainarglist-portinfo-vl-scopestack-equiv-congruence-on-inst-ss

(defthm
 vl-plainarglist-portinfo-vl-scopestack-equiv-congruence-on-inst-ss
 (implies
  (vl-scopestack-equiv inst-ss inst-ss-equiv)
  (equal
    (vl-plainarglist-portinfo x y argindex ss scopes inst-modname
                              inst-ss inst-scopes arraysize)
    (vl-plainarglist-portinfo x y argindex ss scopes inst-modname
                              inst-ss-equiv inst-scopes arraysize)))
 :rule-classes :congruence)

Theorem: vl-plainarglist-portinfo-of-vl-elabscopes-fix-inst-scopes

(defthm vl-plainarglist-portinfo-of-vl-elabscopes-fix-inst-scopes
 (equal
   (vl-plainarglist-portinfo x y argindex ss scopes inst-modname
                             inst-ss (vl-elabscopes-fix inst-scopes)
                             arraysize)
   (vl-plainarglist-portinfo x y argindex ss scopes inst-modname
                             inst-ss inst-scopes arraysize)))

Theorem: vl-plainarglist-portinfo-vl-elabscopes-equiv-congruence-on-inst-scopes

(defthm
 vl-plainarglist-portinfo-vl-elabscopes-equiv-congruence-on-inst-scopes
 (implies
  (vl-elabscopes-equiv inst-scopes inst-scopes-equiv)
  (equal
    (vl-plainarglist-portinfo x y argindex ss scopes inst-modname
                              inst-ss inst-scopes arraysize)
    (vl-plainarglist-portinfo x y argindex ss scopes inst-modname
                              inst-ss inst-scopes-equiv arraysize)))
 :rule-classes :congruence)

Theorem: vl-plainarglist-portinfo-of-maybe-posp-fix-arraysize

(defthm vl-plainarglist-portinfo-of-maybe-posp-fix-arraysize
 (equal
   (vl-plainarglist-portinfo x y argindex ss
                             scopes inst-modname inst-ss inst-scopes
                             (acl2::maybe-posp-fix arraysize))
   (vl-plainarglist-portinfo x y argindex ss scopes inst-modname
                             inst-ss inst-scopes arraysize)))

Theorem: vl-plainarglist-portinfo-maybe-pos-equiv-congruence-on-arraysize

(defthm
   vl-plainarglist-portinfo-maybe-pos-equiv-congruence-on-arraysize
 (implies
  (acl2::maybe-pos-equiv arraysize arraysize-equiv)
  (equal
    (vl-plainarglist-portinfo x y argindex ss scopes inst-modname
                              inst-ss inst-scopes arraysize)
    (vl-plainarglist-portinfo x y argindex ss scopes inst-modname
                              inst-ss inst-scopes arraysize-equiv)))
 :rule-classes :congruence)