		Search-engine friendly clone of the ACL2 documentation.

Parse-paramdecls

Vl-parse-0+-param-assignments

Signature
(vl-parse-0+-param-assignments leading-comma-required &key (tokstream 'tokstream) (config 'config)) → (mv errmsg? value new-tokstream)
Arguments: config — Guard (vl-loadconfig-p config).

Definitions and Theorems

Function: vl-parse-0+-param-assignments-fn

(defun vl-parse-0+-param-assignments-fn
       (leading-comma-required tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-0+-param-assignments))
  (declare (ignorable __function__))
  (b*
   ((backup (vl-tokstream-save))
    ((mv err assigns tokstream)
     (seq
      tokstream
      (when leading-comma-required
            (:= (vl-match-token :vl-comma)))
      (first := (vl-parse-param-assignment
                     nil nil
                     *vl-parse-0+-param-assignments-implicit-type*))
      (unless (vl-is-some-token? '(:vl-comma :vl-rparen))
              (return-raw (mv t nil tokstream)))
      (rest := (vl-parse-0+-param-assignments t))
      (return (cons first rest))))
    ((unless err)
     (mv err assigns tokstream))
    (tokstream (vl-tokstream-restore backup)))
   (mv nil nil tokstream))))

Theorem: vl-parse-0+-param-assignments-never-fails

(defthm vl-parse-0+-param-assignments-never-fails
 (not
   (mv-nth 0
           (vl-parse-0+-param-assignments leading-comma-required))))

Theorem: vl-parse-0+-param-assignments-result

(defthm vl-parse-0+-param-assignments-result
 (implies
  (and
   (not
    (mv-nth 0
            (vl-parse-0+-param-assignments leading-comma-required)))
   (and t))
  (vl-paramdecllist-p
     (mv-nth
          1
          (vl-parse-0+-param-assignments leading-comma-required)))))

Theorem: vl-parse-0+-param-assignments-true-listp

(defthm vl-parse-0+-param-assignments-true-listp
 (true-listp
    (mv-nth 1
            (vl-parse-0+-param-assignments leading-comma-required)))
 :rule-classes :type-prescription)

Theorem: vl-parse-0+-param-assignments-count-strong-on-value

(defthm vl-parse-0+-param-assignments-count-strong-on-value
 (and
  (<=
   (vl-tokstream-measure
    :tokstream
    (mv-nth 2
            (vl-parse-0+-param-assignments leading-comma-required)))
   (vl-tokstream-measure))
  (implies
   (mv-nth 1
           (vl-parse-0+-param-assignments leading-comma-required))
   (<
    (vl-tokstream-measure
       :tokstream
       (mv-nth
            2
            (vl-parse-0+-param-assignments leading-comma-required)))
    (vl-tokstream-measure))))
 :rule-classes ((:rewrite) (:linear)))