		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 config loc) → (mv successp actuals remainder)
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).; config — Guard (vl-loadconfig-p config).; 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), given (force (vl-echarlist-p echars)).

Definitions and Theorems

Function: vl-parse-define-actuals

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

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

(defthm booleanp-of-vl-parse-define-actuals.successp
  (b* (((mv ?successp ?actuals ?remainder)
        (vl-parse-define-actuals name echars config loc)))
    (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)
        (vl-parse-define-actuals name echars config loc)))
    (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
  (implies (force (vl-echarlist-p echars))
           (b* (((mv ?successp ?actuals ?remainder)
                 (vl-parse-define-actuals name echars config loc)))
             (vl-echarlist-p remainder)))
  :rule-classes :rewrite)