		Search-engine friendly clone of the ACL2 documentation.

Parse-expressions

Vl-parse-0+-scope-prefixes

Match { id '::' } and return an expression list with all of the ids that have been matched.

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

See also vl-parse-indexed-id-2012 and abstract-hids. We use this in the tricky case of parsing:

{ id '::' } hierarchical_identifier select

But per our desired abstract HID representation, we want to keep all of the scoping stuff bundled up together, so we prefer to match it first, if it exists.

Definitions and Theorems

Function: vl-parse-0+-scope-prefixes-fn

(defun vl-parse-0+-scope-prefixes-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-0+-scope-prefixes))
  (declare (ignorable __function__))
  (seq
   tokstream
   (unless (and (vl-is-token? :vl-idtoken)
                (vl-lookahead-is-token?
                     :vl-scope (cdr (vl-tokstream->tokens))))
           (return nil))
   (first := (vl-match))
   (:= (vl-match))
   (rest := (vl-parse-0+-scope-prefixes))
   (return
    (cons
       (make-vl-atom
            :guts (make-vl-hidpiece :name (vl-idtoken->name first)))
       rest)))))

Theorem: vl-parse-0+-scope-prefixes-never-fails

(defthm vl-parse-0+-scope-prefixes-never-fails
  (not (mv-nth 0 (vl-parse-0+-scope-prefixes))))

Theorem: vl-parse-0+-scope-prefixes-result

(defthm vl-parse-0+-scope-prefixes-result
  (implies (and (not (mv-nth 0 (vl-parse-0+-scope-prefixes)))
                (and t))
           (vl-exprlist-p (mv-nth 1 (vl-parse-0+-scope-prefixes)))))

Theorem: vl-parse-0+-scope-prefixes-true-listp

(defthm vl-parse-0+-scope-prefixes-true-listp
  (true-listp (mv-nth 1 (vl-parse-0+-scope-prefixes)))
  :rule-classes :type-prescription)

Theorem: vl-parse-0+-scope-prefixes-count-strong-on-value

(defthm vl-parse-0+-scope-prefixes-count-strong-on-value
 (and
    (<= (vl-tokstream-measure
             :tokstream (mv-nth 2 (vl-parse-0+-scope-prefixes)))
        (vl-tokstream-measure))
    (implies
         (mv-nth 1 (vl-parse-0+-scope-prefixes))
         (< (vl-tokstream-measure
                 :tokstream (mv-nth 2 (vl-parse-0+-scope-prefixes)))
            (vl-tokstream-measure))))
 :rule-classes ((:rewrite) (:linear)))

Theorem: vl-parse-0+-scope-prefixes-on-eof

(defthm vl-parse-0+-scope-prefixes-on-eof
 (implies
  (not (consp (vl-tokstream->tokens)))
  (b* (((mv & val new-tokstream)
        (vl-parse-0+-scope-prefixes)))
   (and
    (not val)
    (not
        (consp (vl-tokstream->tokens :tokstream new-tokstream)))))))