		Search-engine friendly clone of the ACL2 documentation.

Vl-expand-define

Vl-parse-define-actuals

Collect the arguments to a macro, like `max(a+b, c).

Signature
(vl-parse-define-actuals name echars loc ppst) → (mv successp actuals remainder ppst)
Arguments: name — Name of macro being expanded, e.g., max, for error messages.
Guard (stringp name).; echars — Text that follows the initial open paren, or that follows a comma.
Guard (vl-echarlist-p echars).; loc — Location information in case of error messages.
Guard (vl-location-p loc).
Returns: successp — Type (booleanp successp).; actuals — Type (string-listp actuals).; remainder — Remainder of the input stream after eating all the actuals and also the closing paren.
Type (vl-echarlist-p remainder).

Definitions and Theorems

Function: vl-parse-define-actuals

(defun vl-parse-define-actuals (name echars loc ppst)
  (declare (xargs :stobjs (ppst)))
  (declare (xargs :guard (and (stringp name)
                              (vl-echarlist-p echars)
                              (vl-location-p loc))))
  (let ((__function__ 'vl-parse-define-actuals))
    (declare (ignorable __function__))
    (b* (((mv successp morep actual1 echars ppst)
          (vl-parse-define-actual name echars loc nil nil ppst))
         ((unless successp)
          (mv nil nil echars ppst))
         ((unless morep)
          (mv t (list actual1) echars ppst))
         ((mv successp rest-actuals echars ppst)
          (vl-parse-define-actuals name echars loc ppst))
         ((unless successp)
          (mv nil nil echars ppst)))
      (mv t (cons actual1 rest-actuals)
          echars ppst))))

Theorem: booleanp-of-vl-parse-define-actuals.successp

(defthm booleanp-of-vl-parse-define-actuals.successp
  (b* (((mv ?successp ?actuals ?remainder ?ppst)
        (vl-parse-define-actuals name echars loc ppst)))
    (booleanp successp))
  :rule-classes :type-prescription)

Theorem: string-listp-of-vl-parse-define-actuals.actuals

(defthm string-listp-of-vl-parse-define-actuals.actuals
  (b* (((mv ?successp ?actuals ?remainder ?ppst)
        (vl-parse-define-actuals name echars loc ppst)))
    (string-listp actuals))
  :rule-classes :rewrite)

Theorem: vl-echarlist-p-of-vl-parse-define-actuals.remainder

(defthm vl-echarlist-p-of-vl-parse-define-actuals.remainder
  (b* (((mv ?successp ?actuals ?remainder ?ppst)
        (vl-parse-define-actuals name echars loc ppst)))
    (vl-echarlist-p remainder))
  :rule-classes :rewrite)