		Search-engine friendly clone of the ACL2 documentation.

Vl-port-direction

Vl-port-direction-aux

Signature
(vl-port-direction-aux names scope warnings port) → (mv successp warnings directions)
Arguments: names — Guard (string-listp names).; scope — Guard (vl-scope-p scope).; warnings — Guard (vl-warninglist-p warnings).; port — Guard (vl-port-p port).
Returns: successp — Type (booleanp successp).; warnings — Type (vl-warninglist-p warnings).; directions — Type (vl-directionlist-p directions).

Definitions and Theorems

Function: vl-port-direction-aux

(defun vl-port-direction-aux (names scope warnings port)
 (declare (xargs :guard (and (string-listp names)
                             (vl-scope-p scope)
                             (vl-warninglist-p warnings)
                             (vl-port-p port))))
 (let ((__function__ 'vl-port-direction-aux))
  (declare (ignorable __function__))
  (b* (((when (atom names)) (mv t (ok) nil))
       (name1 (string-fix (car names)))
       (decl (vl-scope-find-portdecl-fast name1 scope))
       ((mv successp warnings directions)
        (vl-port-direction-aux (cdr names)
                               scope warnings port))
       ((when decl)
        (mv successp warnings
            (cons (vl-portdecl->dir decl)
                  directions))))
   (mv
    nil
    (warn
     :type :vl-bad-port
     :msg
     "~a0 refers to ~w1, but there is no port declaration for ~
                      ~w1."
     :args (list (vl-port-fix port) name1))
    directions))))

Theorem: booleanp-of-vl-port-direction-aux.successp

(defthm booleanp-of-vl-port-direction-aux.successp
  (b* (((mv ?successp ?warnings ?directions)
        (vl-port-direction-aux names scope warnings port)))
    (booleanp successp))
  :rule-classes :type-prescription)

Theorem: vl-warninglist-p-of-vl-port-direction-aux.warnings

(defthm vl-warninglist-p-of-vl-port-direction-aux.warnings
  (b* (((mv ?successp ?warnings ?directions)
        (vl-port-direction-aux names scope warnings port)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-directionlist-p-of-vl-port-direction-aux.directions

(defthm vl-directionlist-p-of-vl-port-direction-aux.directions
  (b* (((mv ?successp ?warnings ?directions)
        (vl-port-direction-aux names scope warnings port)))
    (vl-directionlist-p directions))
  :rule-classes :rewrite)

Theorem: vl-port-direction-aux-mvtypes-2

(defthm vl-port-direction-aux-mvtypes-2
  (true-listp
       (mv-nth 2
               (vl-port-direction-aux names scope warnings port)))
  :rule-classes :type-prescription)

Theorem: vl-port-direction-aux-of-string-list-fix-names

(defthm vl-port-direction-aux-of-string-list-fix-names
  (equal (vl-port-direction-aux (string-list-fix names)
                                scope warnings port)
         (vl-port-direction-aux names scope warnings port)))

Theorem: vl-port-direction-aux-string-list-equiv-congruence-on-names

(defthm vl-port-direction-aux-string-list-equiv-congruence-on-names
 (implies
    (str::string-list-equiv names names-equiv)
    (equal (vl-port-direction-aux names scope warnings port)
           (vl-port-direction-aux names-equiv scope warnings port)))
 :rule-classes :congruence)

Theorem: vl-port-direction-aux-of-vl-scope-fix-scope

(defthm vl-port-direction-aux-of-vl-scope-fix-scope
  (equal (vl-port-direction-aux names (vl-scope-fix scope)
                                warnings port)
         (vl-port-direction-aux names scope warnings port)))

Theorem: vl-port-direction-aux-vl-scope-equiv-congruence-on-scope

(defthm vl-port-direction-aux-vl-scope-equiv-congruence-on-scope
 (implies
    (vl-scope-equiv scope scope-equiv)
    (equal (vl-port-direction-aux names scope warnings port)
           (vl-port-direction-aux names scope-equiv warnings port)))
 :rule-classes :congruence)

Theorem: vl-port-direction-aux-of-vl-warninglist-fix-warnings

(defthm vl-port-direction-aux-of-vl-warninglist-fix-warnings
  (equal (vl-port-direction-aux names
                                scope (vl-warninglist-fix warnings)
                                port)
         (vl-port-direction-aux names scope warnings port)))

Theorem: vl-port-direction-aux-vl-warninglist-equiv-congruence-on-warnings

(defthm
  vl-port-direction-aux-vl-warninglist-equiv-congruence-on-warnings
 (implies
    (vl-warninglist-equiv warnings warnings-equiv)
    (equal (vl-port-direction-aux names scope warnings port)
           (vl-port-direction-aux names scope warnings-equiv port)))
 :rule-classes :congruence)

Theorem: vl-port-direction-aux-of-vl-port-fix-port

(defthm vl-port-direction-aux-of-vl-port-fix-port
 (equal
     (vl-port-direction-aux names scope warnings (vl-port-fix port))
     (vl-port-direction-aux names scope warnings port)))

Theorem: vl-port-direction-aux-vl-port-equiv-congruence-on-port

(defthm vl-port-direction-aux-vl-port-equiv-congruence-on-port
 (implies
    (vl-port-equiv port port-equiv)
    (equal (vl-port-direction-aux names scope warnings port)
           (vl-port-direction-aux names scope warnings port-equiv)))
 :rule-classes :congruence)