		Search-engine friendly clone of the ACL2 documentation.

Parse-paramdecls

Vl-parse-list-of-param-assignments

Signature
(vl-parse-list-of-param-assignments atts localp type &key (tokstream 'tokstream) (config 'config)) → (mv errmsg? value new-tokstream)
Arguments: config — Guard (vl-loadconfig-p config).

Definitions and Theorems

Function: vl-parse-list-of-param-assignments-fn

(defun vl-parse-list-of-param-assignments-fn
       (atts localp type tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (declare
  (xargs
   :guard
   (and (vl-atts-p atts)
        (booleanp localp)
        (vl-paramtype-p type)
        (member (vl-paramtype-kind type)
                '(:vl-implicitvalueparam :vl-explicitvalueparam)))))
 (let ((__function__ 'vl-parse-list-of-param-assignments))
  (declare (ignorable __function__))
  (seq
   tokstream
   (first := (vl-parse-param-assignment atts localp type))
   (when (or (atom (vl-tokstream->tokens))
             (vl-is-token? :vl-rparen)
             (vl-is-token? :vl-semi))
         (return (list first)))
   (when
    (vl-is-token? :vl-comma)
    (when
     (vl-lookahead-is-token?
          :vl-idtoken (cdr (vl-tokstream->tokens)))
     (return-raw
      (b*
       ((backup (vl-tokstream-save))
        ((mv err decls tokstream)
         (seq
          tokstream (:= (vl-match))
          (decls
           := (vl-parse-list-of-param-assignments atts localp type))
          (return decls)))
        ((unless err)
         (mv nil (cons first decls) tokstream))
        (tokstream (vl-tokstream-restore backup)))
       (mv nil (list first) tokstream))))
    (return (list first)))
   (return-raw
    (vl-parse-error
     "Expected a comma or right paren to follow a list of param assignments")))))

Theorem: vl-parse-list-of-param-assignments-fails-gracefully

(defthm vl-parse-list-of-param-assignments-fails-gracefully
 (implies
  (mv-nth 0
          (vl-parse-list-of-param-assignments atts localp type))
  (not
   (mv-nth 1
           (vl-parse-list-of-param-assignments atts localp type)))))

Theorem: vl-warning-p-of-vl-parse-list-of-param-assignments

(defthm vl-warning-p-of-vl-parse-list-of-param-assignments
 (iff
  (vl-warning-p
     (mv-nth 0
             (vl-parse-list-of-param-assignments atts localp type)))
  (mv-nth 0
          (vl-parse-list-of-param-assignments atts localp type))))

Theorem: vl-parse-list-of-param-assignments-result

(defthm vl-parse-list-of-param-assignments-result
 (implies
  (and
   (and
    (force (vl-atts-p atts))
    (force (booleanp localp))
    (force (vl-paramtype-p type))
    (force
        (member (vl-paramtype-kind type)
                '(:vl-implicitvalueparam :vl-explicitvalueparam)))))
  (vl-paramdecllist-p
   (mv-nth 1
           (vl-parse-list-of-param-assignments atts localp type)))))

Theorem: vl-parse-list-of-param-assignments-true-listp

(defthm vl-parse-list-of-param-assignments-true-listp
 (true-listp
     (mv-nth 1
             (vl-parse-list-of-param-assignments atts localp type)))
 :rule-classes :type-prescription)

Theorem: vl-parse-list-of-param-assignments-count-strong

(defthm vl-parse-list-of-param-assignments-count-strong
 (and
  (<=
   (vl-tokstream-measure
     :tokstream
     (mv-nth 2
             (vl-parse-list-of-param-assignments atts localp type)))
   (vl-tokstream-measure))
  (implies
   (not
     (mv-nth 0
             (vl-parse-list-of-param-assignments atts localp type)))
   (<
    (vl-tokstream-measure
     :tokstream
     (mv-nth 2
             (vl-parse-list-of-param-assignments atts localp type)))
    (vl-tokstream-measure))))
 :rule-classes ((:rewrite) (:linear)))