		Search-engine friendly clone of the ACL2 documentation.

Unparameterization

Vl-plainarg-update-ifports

Signature
(vl-plainarg-update-ifports x1 port1 ss scopes) → (mv err new-port ifportalist-chunk)
Arguments: x1 — Guard (vl-plainarg-p x1).; port1 — Guard (vl-port-p port1).; ss — Guard (vl-scopestack-p ss).; scopes — Guard (vl-elabscopes-p scopes).
Returns: err — Type (iff (vl-msg-p err) err).; new-port — Type (vl-port-p new-port).; ifportalist-chunk — Type (vl-ifport-alist-p ifportalist-chunk).

Definitions and Theorems

Function: vl-plainarg-update-ifports

(defun vl-plainarg-update-ifports (x1 port1 ss scopes)
 (declare (xargs :guard (and (vl-plainarg-p x1)
                             (vl-port-p port1)
                             (vl-scopestack-p ss)
                             (vl-elabscopes-p scopes))))
 (let ((__function__ 'vl-plainarg-update-ifports))
  (declare (ignorable __function__))
  (b*
   ((port1 (vl-port-fix port1))
    ((vl-plainarg x1) (vl-plainarg-fix x1))
    ((when (eq (tag port1) :vl-regularport))
     (mv nil port1 nil))
    (name (and x1.expr
               (vl-expr-case x1.expr
                             :vl-index x1.expr.scope
                             :otherwise nil)))
    ((unless name)
     (mv (vmsg "Bad interface port connection: ~a0"
               (or x1.expr "(empty)"))
         port1 nil))
    ((vl-interfaceport port1) port1)
    ((mv err trace ?context tail)
     (vl-follow-scopeexpr name ss))
    ((when err)
     (mv (vmsg "Error resolving interface port argument ~a0: ~@1"
               x1.expr err)
         port1 nil))
    ((unless (vl-hidexpr-case tail :end))
     (mv
      (vmsg
       "Unexpected indexing on interface port argument ~a0: ~a1 (modports
                   should have been previously removed)"
       x1.expr
       (make-vl-index :scope (make-vl-scopeexpr-end :hid tail)))
      port1 nil))
    (name (vl-hidexpr-end->name tail))
    ((vl-hidstep step) (car trace))
    (item-scopes (vl-elabscopes-traverse (rev step.elabpath)
                                         scopes))
    (item (or (vl-elabscopes-item-info name item-scopes)
              step.item))
    ((unless (and item
                  (or (eq (tag item) :vl-interfaceport)
                      (eq (tag item) :vl-modinst))))
     (mv (vmsg "Bad interface port connection: ~a0"
               x1.expr)
         port1 nil))
    (ifname (if (eq (tag item) :vl-interfaceport)
                (vl-interfaceport->ifname item)
              (vl-modinst->modname item))))
   (if (equal ifname port1.ifname)
       (mv nil port1 nil)
     (mv nil
         (change-vl-interfaceport port1
                                  :ifname ifname)
         (list (cons port1.ifname ifname)))))))

Theorem: return-type-of-vl-plainarg-update-ifports.err

(defthm return-type-of-vl-plainarg-update-ifports.err
  (b* (((mv ?err ?new-port ?ifportalist-chunk)
        (vl-plainarg-update-ifports x1 port1 ss scopes)))
    (iff (vl-msg-p err) err))
  :rule-classes :rewrite)

Theorem: vl-port-p-of-vl-plainarg-update-ifports.new-port

(defthm vl-port-p-of-vl-plainarg-update-ifports.new-port
  (b* (((mv ?err ?new-port ?ifportalist-chunk)
        (vl-plainarg-update-ifports x1 port1 ss scopes)))
    (vl-port-p new-port))
  :rule-classes :rewrite)

Theorem: vl-ifport-alist-p-of-vl-plainarg-update-ifports.ifportalist-chunk

(defthm
  vl-ifport-alist-p-of-vl-plainarg-update-ifports.ifportalist-chunk
  (b* (((mv ?err ?new-port ?ifportalist-chunk)
        (vl-plainarg-update-ifports x1 port1 ss scopes)))
    (vl-ifport-alist-p ifportalist-chunk))
  :rule-classes :rewrite)

Theorem: vl-plainarg-update-ifports-preserves-port

(defthm vl-plainarg-update-ifports-preserves-port
  (b* (((mv ?err ?new-port ?ifportalist-chunk)
        (vl-plainarg-update-ifports x1 port1 ss scopes)))
    (implies (atom ifportalist-chunk)
             (equal new-port (vl-port-fix port1)))))

Theorem: vl-plainarg-update-ifports-of-vl-plainarg-fix-x1

(defthm vl-plainarg-update-ifports-of-vl-plainarg-fix-x1
  (equal (vl-plainarg-update-ifports (vl-plainarg-fix x1)
                                     port1 ss scopes)
         (vl-plainarg-update-ifports x1 port1 ss scopes)))

Theorem: vl-plainarg-update-ifports-vl-plainarg-equiv-congruence-on-x1

(defthm
      vl-plainarg-update-ifports-vl-plainarg-equiv-congruence-on-x1
 (implies
      (vl-plainarg-equiv x1 x1-equiv)
      (equal (vl-plainarg-update-ifports x1 port1 ss scopes)
             (vl-plainarg-update-ifports x1-equiv port1 ss scopes)))
 :rule-classes :congruence)

Theorem: vl-plainarg-update-ifports-of-vl-port-fix-port1

(defthm vl-plainarg-update-ifports-of-vl-port-fix-port1
  (equal (vl-plainarg-update-ifports x1 (vl-port-fix port1)
                                     ss scopes)
         (vl-plainarg-update-ifports x1 port1 ss scopes)))

Theorem: vl-plainarg-update-ifports-vl-port-equiv-congruence-on-port1

(defthm vl-plainarg-update-ifports-vl-port-equiv-congruence-on-port1
 (implies
      (vl-port-equiv port1 port1-equiv)
      (equal (vl-plainarg-update-ifports x1 port1 ss scopes)
             (vl-plainarg-update-ifports x1 port1-equiv ss scopes)))
 :rule-classes :congruence)

Theorem: vl-plainarg-update-ifports-of-vl-scopestack-fix-ss

(defthm vl-plainarg-update-ifports-of-vl-scopestack-fix-ss
  (equal (vl-plainarg-update-ifports x1 port1 (vl-scopestack-fix ss)
                                     scopes)
         (vl-plainarg-update-ifports x1 port1 ss scopes)))

Theorem: vl-plainarg-update-ifports-vl-scopestack-equiv-congruence-on-ss

(defthm
    vl-plainarg-update-ifports-vl-scopestack-equiv-congruence-on-ss
 (implies
      (vl-scopestack-equiv ss ss-equiv)
      (equal (vl-plainarg-update-ifports x1 port1 ss scopes)
             (vl-plainarg-update-ifports x1 port1 ss-equiv scopes)))
 :rule-classes :congruence)

Theorem: vl-plainarg-update-ifports-of-vl-elabscopes-fix-scopes

(defthm vl-plainarg-update-ifports-of-vl-elabscopes-fix-scopes
  (equal (vl-plainarg-update-ifports
              x1 port1 ss (vl-elabscopes-fix scopes))
         (vl-plainarg-update-ifports x1 port1 ss scopes)))

Theorem: vl-plainarg-update-ifports-vl-elabscopes-equiv-congruence-on-scopes

(defthm
 vl-plainarg-update-ifports-vl-elabscopes-equiv-congruence-on-scopes
 (implies
      (vl-elabscopes-equiv scopes scopes-equiv)
      (equal (vl-plainarg-update-ifports x1 port1 ss scopes)
             (vl-plainarg-update-ifports x1 port1 ss scopes-equiv)))
 :rule-classes :congruence)