		Search-engine friendly clone of the ACL2 documentation.

Parse-port-types

Vl-parse-port-declaration-head-2012

Matches net_port_type or variable_port_type. Assumes that an identifier (i.e., a port name) must follow.

Signature
(vl-parse-port-declaration-head-2012 &key (tokstream 'tokstream) (config 'config)) → (mv errmsg? value new-tokstream)
Arguments: config — Guard (vl-loadconfig-p config).

Here is the grammar we are implementing:

net_port_type ::= [net_type] data_type
                | [net_type] [signing] {packed_dimension}
                | identifier                                           (*)
                | 'interconnect' [signing] {packed_dimension}          (**)

variable_port_type ::= data_type
                     | 'var' data_type
                     | 'var' [signing] {packed_dimension}

We assume that we have already ruled out interface ports.

(*) Since VL doesn't support user-defined net types, we don't implement the second net_port_type case.

(**) We do not yet implement interconnect ports.

Definitions and Theorems

Function: vl-parse-port-declaration-head-2012-fn

(defun vl-parse-port-declaration-head-2012-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-port-declaration-head-2012))
  (declare (ignorable __function__))
  (seq
   tokstream
   (when
        (vl-is-token? :vl-kwd-interconnect)
        (return-raw
             (vl-parse-error "BOZO implement interconnect ports!")))
   (when
    (vl-is-token? :vl-kwd-var)
    (:= (vl-match))
    (when (vl-is-some-token? '(:vl-kwd-signed :vl-kwd-unsigned))
          (signing := (vl-match)))
    (when (vl-is-token? :vl-lbrack)
          (ranges := (vl-parse-0+-ranges)))
    (when
     (or signing ranges)
     (return
      (make-vl-parsed-portdecl-head
        :nettype nil
        :var-p t
        :explicit-p nil
        :implicit-p t
        :type
        (make-vl-coretype :name :vl-logic
                          :signedp (and signing
                                        (eq (vl-token->type signing)
                                            :vl-kwd-signed))
                          :pdims ranges))))
    (when
      (and (vl-is-token? :vl-idtoken)
           (not (vl-parsestate-is-user-defined-type-p
                     (vl-idtoken->name (car (vl-tokstream->tokens)))
                     (vl-tokstream->pstate))))
      (return (make-vl-parsed-portdecl-head
                   :nettype nil
                   :var-p t
                   :explicit-p nil
                   :implicit-p nil
                   :type (make-vl-coretype :name :vl-logic
                                           :signedp nil
                                           :pdims nil))))
    (type := (vl-parse-datatype))
    (return (make-vl-parsed-portdecl-head :nettype nil
                                          :var-p t
                                          :explicit-p t
                                          :implicit-p nil
                                          :type type)))
   (nettype := (vl-parse-optional-nettype))
   (when (vl-is-some-token? '(:vl-kwd-signed :vl-kwd-unsigned))
         (signing := (vl-match)))
   (when (vl-is-token? :vl-lbrack)
         (ranges := (vl-parse-0+-ranges)))
   (when
    (or signing ranges)
    (return
     (make-vl-parsed-portdecl-head
        :nettype nettype
        :var-p nil
        :explicit-p nil
        :implicit-p t
        :type
        (make-vl-coretype :name :vl-logic
                          :signedp (and signing
                                        (eq (vl-token->type signing)
                                            :vl-kwd-signed))
                          :pdims ranges))))
   (when
      (and (vl-is-token? :vl-idtoken)
           (not (vl-parsestate-is-user-defined-type-p
                     (vl-idtoken->name (car (vl-tokstream->tokens)))
                     (vl-tokstream->pstate))))
      (return (make-vl-parsed-portdecl-head
                   :nettype nettype
                   :var-p nil
                   :explicit-p nil
                   :implicit-p nil
                   :type (make-vl-coretype :name :vl-logic
                                           :signedp nil
                                           :pdims nil))))
   (type := (vl-parse-datatype))
   (return (make-vl-parsed-portdecl-head :nettype nettype
                                         :var-p nil
                                         :explicit-p t
                                         :implicit-p nil
                                         :type type)))))

Theorem: vl-parse-port-declaration-head-2012-fails-gracefully

(defthm vl-parse-port-declaration-head-2012-fails-gracefully
  (implies (mv-nth 0 (vl-parse-port-declaration-head-2012))
           (not (mv-nth 1
                        (vl-parse-port-declaration-head-2012)))))

Theorem: vl-warning-p-of-vl-parse-port-declaration-head-2012

(defthm vl-warning-p-of-vl-parse-port-declaration-head-2012
  (iff (vl-warning-p (mv-nth 0
                             (vl-parse-port-declaration-head-2012)))
       (mv-nth 0
               (vl-parse-port-declaration-head-2012))))

Theorem: vl-parse-port-declaration-head-2012-result

(defthm vl-parse-port-declaration-head-2012-result
 (implies
      (and t)
      (equal (vl-parsed-portdecl-head-p
                  (mv-nth 1
                          (vl-parse-port-declaration-head-2012)))
             (not (mv-nth 0
                          (vl-parse-port-declaration-head-2012))))))

Theorem: vl-parse-port-declaration-head-2012-count-weak

(defthm vl-parse-port-declaration-head-2012-count-weak
 (<= (vl-tokstream-measure
          :tokstream (mv-nth 2
                             (vl-parse-port-declaration-head-2012)))
     (vl-tokstream-measure))
 :rule-classes ((:rewrite) (:linear)))