		Search-engine friendly clone of the ACL2 documentation.

Parse-asserts

Vl-parse-0+-assertion-variable-declarations

Parse { assertion_variable_declaration } .

Signature
(vl-parse-0+-assertion-variable-declarations &key (tokstream 'tokstream) (config 'config)) → (mv errmsg? value new-tokstream)
Arguments: config — Guard (vl-loadconfig-p config).

In sequence_declaration and property_declaration we need to match however many assertion_variable_declarations there are, followed by a sequence expression or property expression. It's not very easy to tell if we're looking at a user-defined type or the start of a sequence/property expression, so we use backtracking.

assertion_variable_declaration ::= var_data_type list_of_variable_decl_assignments ';'

var_data_type ::= data_type
                | 'var' data_type_or_implicit

Definitions and Theorems

Function: vl-parse-0+-assertion-variable-declarations-fn

(defun vl-parse-0+-assertion-variable-declarations-fn
       (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-0+-assertion-variable-declarations))
  (declare (ignorable __function__))
  (b*
   ((loc (if (consp (vl-tokstream->tokens))
             (vl-token->loc (car (vl-tokstream->tokens)))
           *vl-fakeloc*))
    ((when (vl-is-token? :vl-kwd-var))
     (seq
      tokstream (:= (vl-match))
      (type := (vl-parse-datatype-or-implicit))
      (vars
        :=
        (vl-parse-1+-variable-decl-assignments-separated-by-commas))
      (:= (vl-match-token :vl-semi))
      (rest := (vl-parse-0+-assertion-variable-declarations))
      (return (append (vl-make-assertion-vardecls type vars loc)
                      rest))))
    (backup (vl-tokstream-save))
    ((mv err type tokstream)
     (vl-parse-datatype))
    ((when (and (not err)
                (vl-is-token? :vl-idtoken)))
     (seq
      tokstream
      (vars
        :=
        (vl-parse-1+-variable-decl-assignments-separated-by-commas))
      (:= (vl-match-token :vl-semi))
      (return (vl-make-assertion-vardecls type vars loc))))
    (tokstream (vl-tokstream-restore backup)))
   (mv nil nil tokstream))))

Theorem: vl-parse-0+-assertion-variable-declarations-fails-gracefully

(defthm vl-parse-0+-assertion-variable-declarations-fails-gracefully
 (implies
      (mv-nth 0
              (vl-parse-0+-assertion-variable-declarations))
      (not (mv-nth 1
                   (vl-parse-0+-assertion-variable-declarations)))))

Theorem: vl-warning-p-of-vl-parse-0+-assertion-variable-declarations

(defthm vl-warning-p-of-vl-parse-0+-assertion-variable-declarations
  (iff (vl-warning-p
            (mv-nth 0
                    (vl-parse-0+-assertion-variable-declarations)))
       (mv-nth 0
               (vl-parse-0+-assertion-variable-declarations))))

Theorem: vl-parse-0+-assertion-variable-declarations-result

(defthm vl-parse-0+-assertion-variable-declarations-result
 (implies
      (and t)
      (vl-vardecllist-p
           (mv-nth 1
                   (vl-parse-0+-assertion-variable-declarations)))))

Theorem: vl-parse-0+-assertion-variable-declarations-true-listp

(defthm vl-parse-0+-assertion-variable-declarations-true-listp
 (true-listp (mv-nth 1
                     (vl-parse-0+-assertion-variable-declarations)))
 :rule-classes :type-prescription)

Theorem: vl-parse-0+-assertion-variable-declarations-count-weak

(defthm vl-parse-0+-assertion-variable-declarations-count-weak
  (<= (vl-tokstream-measure
           :tokstream
           (mv-nth 2
                   (vl-parse-0+-assertion-variable-declarations)))
      (vl-tokstream-measure))
  :rule-classes ((:rewrite) (:linear)))