		Search-engine friendly clone of the ACL2 documentation.

Sv-ansi-port-interpretation

Vl-process-subsequent-ansi-port

Signature
(vl-process-subsequent-ansi-port x prev-ifacep warnings ports-acc portdecls-acc vardecls-acc) → (mv ifacep warnings ports-acc portdecls-acc vardecls-acc)
Arguments: x — Next parsed port to process.
Guard (vl-parsed-ansi-port-p x).; prev-ifacep — Was the previous port an interface port?.
Guard (booleanp prev-ifacep).; warnings — Guard (vl-warninglist-p warnings).; ports-acc — Guard (vl-portlist-p ports-acc).; portdecls-acc — Guard (vl-portdecllist-p portdecls-acc).; vardecls-acc — Guard (vl-vardecllist-p vardecls-acc).
Returns: ifacep — Was this port an interface port?.
Type (booleanp ifacep).; warnings — Type (vl-warninglist-p warnings).; ports-acc — Type (and (vl-portlist-p ports-acc) (consp ports-acc) (equal (vl-interfaceport-p (car ports-acc)) ifacep) (equal (vl-regularport-p (car ports-acc)) (not ifacep))) .; portdecls-acc — Type (and (vl-portdecllist-p portdecls-acc) (implies (not ifacep) (consp portdecls-acc))) .; vardecls-acc — Type (and (vl-vardecllist-p vardecls-acc) (implies (not ifacep) (consp vardecls-acc))) .

Definitions and Theorems

Function: vl-process-subsequent-ansi-port

(defun vl-process-subsequent-ansi-port
       (x prev-ifacep warnings
          ports-acc portdecls-acc vardecls-acc)
 (declare (xargs :guard (and (vl-parsed-ansi-port-p x)
                             (booleanp prev-ifacep)
                             (vl-warninglist-p warnings)
                             (vl-portlist-p ports-acc)
                             (vl-portdecllist-p portdecls-acc)
                             (vl-vardecllist-p vardecls-acc))))
 (declare
      (xargs :guard (and (consp ports-acc)
                         (equal (vl-interfaceport-p (car ports-acc))
                                prev-ifacep)
                         (equal (vl-regularport-p (car ports-acc))
                                (not prev-ifacep))
                         (implies (not prev-ifacep)
                                  (and (consp portdecls-acc)
                                       (consp vardecls-acc))))))
 (let ((__function__ 'vl-process-subsequent-ansi-port))
  (declare (ignorable __function__))
  (b* ((warnings (vl-warninglist-fix warnings))
       (ports-acc (vl-portlist-fix ports-acc))
       (portdecls-acc (vl-portdecllist-fix portdecls-acc))
       (vardecls-acc (vl-vardecllist-fix vardecls-acc))
       ((vl-parsed-ansi-port x) x)
       ((vl-parsed-port-identifier x.id) x.id)
       (name (vl-idtoken->name x.id.name))
       (loc (vl-token->loc x.id.name)))
   (case
    (tag x.head)
    (:vl-parsed-interface-head
     (mv
      t warnings
      (cons (make-vl-interfaceport
                 :name name
                 :ifname (vl-parsed-interface-head->ifname x.head)
                 :modport (vl-parsed-interface-head->modport x.head)
                 :udims x.id.udims
                 :loc loc)
            ports-acc)
      portdecls-acc vardecls-acc))
    (:vl-parsed-portdecl-head
     (b*
      (((vl-parsed-portdecl-head x.head))
       ((when (and (not x.dir)
                   (not x.head.nettype)
                   (not x.head.var-p)
                   (not x.head.explicit-p)
                   (not x.head.implicit-p)))
        (if prev-ifacep
            (mv t warnings
                (cons (change-vl-interfaceport (car ports-acc)
                                               :name name
                                               :loc loc)
                      ports-acc)
                portdecls-acc vardecls-acc)
         (mv
          nil warnings
          (cons
               (change-vl-regularport (car ports-acc)
                                      :name name
                                      :expr (vl-idexpr name nil nil)
                                      :loc loc)
               ports-acc)
          (cons (change-vl-portdecl (car portdecls-acc)
                                    :name name
                                    :loc loc)
                portdecls-acc)
          (cons (change-vl-vardecl (car vardecls-acc)
                                   :name name
                                   :loc loc)
                vardecls-acc))))
       (ports-acc
           (cons (make-vl-regularport :name name
                                      :expr (vl-idexpr name nil nil)
                                      :loc loc)
                 ports-acc))
       (complete-p t)
       ((mv dir warnings)
        (cond
         (x.dir (mv x.dir (ok)))
         (prev-ifacep
          (mv
           :vl-inout
           (fatal
            :type :vl-bad-ports
            :msg
            "~a0: can't infer direction for port ~a1 ~
                                     since it follows an interface port.  ~
                                     Please explicitly specify a direction ~
                                     (input, output, ...)"
            :args (list loc name))))
         (t (mv (vl-portdecl->dir (car portdecls-acc))
                (ok)))))
       (nettype (vl-nettype-for-parsed-ansi-port dir x.head))
       (type x.head.type)
       ((cons new-portdecls new-vardecls)
        (vl-make-ports-and-maybe-nets (list x.id)
                                      :dir dir
                                      :nettype nettype
                                      :type type
                                      :complete-p complete-p
                                      :atts x.atts))
       (portdecls-acc (append new-portdecls portdecls-acc))
       (vardecls-acc (append new-vardecls vardecls-acc)))
      (mv nil warnings
          ports-acc portdecls-acc vardecls-acc)))
    (otherwise
         (progn$ (impossible)
                 (mv t warnings
                     (cons (make-vl-interfaceport :name "bogus"
                                                  :ifname "bogus")
                           ports-acc)
                     portdecls-acc vardecls-acc)))))))

Theorem: booleanp-of-vl-process-subsequent-ansi-port.ifacep

(defthm booleanp-of-vl-process-subsequent-ansi-port.ifacep
  (b* (((mv ?ifacep ?warnings
            ?ports-acc ?portdecls-acc ?vardecls-acc)
        (vl-process-subsequent-ansi-port
             x prev-ifacep warnings
             ports-acc portdecls-acc vardecls-acc)))
    (booleanp ifacep))
  :rule-classes :type-prescription)

Theorem: vl-warninglist-p-of-vl-process-subsequent-ansi-port.warnings

(defthm vl-warninglist-p-of-vl-process-subsequent-ansi-port.warnings
  (b* (((mv ?ifacep ?warnings
            ?ports-acc ?portdecls-acc ?vardecls-acc)
        (vl-process-subsequent-ansi-port
             x prev-ifacep warnings
             ports-acc portdecls-acc vardecls-acc)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-process-subsequent-ansi-port.ports-acc

(defthm return-type-of-vl-process-subsequent-ansi-port.ports-acc
  (b* (((mv ?ifacep ?warnings
            ?ports-acc ?portdecls-acc ?vardecls-acc)
        (vl-process-subsequent-ansi-port
             x prev-ifacep warnings
             ports-acc portdecls-acc vardecls-acc)))
    (and (vl-portlist-p ports-acc)
         (consp ports-acc)
         (equal (vl-interfaceport-p (car ports-acc))
                ifacep)
         (equal (vl-regularport-p (car ports-acc))
                (not ifacep))))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-process-subsequent-ansi-port.portdecls-acc

(defthm return-type-of-vl-process-subsequent-ansi-port.portdecls-acc
  (b* (((mv ?ifacep ?warnings
            ?ports-acc ?portdecls-acc ?vardecls-acc)
        (vl-process-subsequent-ansi-port
             x prev-ifacep warnings
             ports-acc portdecls-acc vardecls-acc)))
    (and (vl-portdecllist-p portdecls-acc)
         (implies (not ifacep)
                  (consp portdecls-acc))))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-process-subsequent-ansi-port.vardecls-acc

(defthm return-type-of-vl-process-subsequent-ansi-port.vardecls-acc
  (b* (((mv ?ifacep ?warnings
            ?ports-acc ?portdecls-acc ?vardecls-acc)
        (vl-process-subsequent-ansi-port
             x prev-ifacep warnings
             ports-acc portdecls-acc vardecls-acc)))
    (and (vl-vardecllist-p vardecls-acc)
         (implies (not ifacep)
                  (consp vardecls-acc))))
  :rule-classes :rewrite)