		Search-engine friendly clone of the ACL2 documentation.

Vl-split-define-text

Vl-parse-define-formal-arguments

Signature
(vl-parse-define-formal-arguments text config starting-loc) → (mv successp formals body)
Arguments: text — Text after the opening paren, or after some comma.
Guard (vl-echarlist-p text).; config — Guard (vl-loadconfig-p config).; starting-loc — Context for error messages.
Guard (vl-location-p starting-loc).
Returns: successp — Type (booleanp successp).; formals — Type (vl-define-formallist-p formals).; body — Remaining characters after the closing paren.
Type (vl-echarlist-p body), given (force (vl-echarlist-p text)).

Definitions and Theorems

Function: vl-parse-define-formal-arguments

(defun vl-parse-define-formal-arguments (text config starting-loc)
 (declare (xargs :guard (and (vl-echarlist-p text)
                             (vl-loadconfig-p config)
                             (vl-location-p starting-loc))))
 (let ((__function__ 'vl-parse-define-formal-arguments))
  (declare (ignorable __function__))
  (b*
   (((when (atom text))
     (mv
      (cw
       "Preprocessor error (~s0): `define arguments are not closed.~%"
       (vl-location-string starting-loc))
      nil nil))
    ((mv ?ws rest)
     (vl-read-while-whitespace text))
    ((mv id rest)
     (vl-read-simple-identifier rest))
    ((unless id)
     (mv
      (cw
         "Preprocessor error (~s0): invalid `define argument name~%"
         (vl-location-string (vl-echar->loc (car text))))
      nil nil))
    (name1 (vl-echarlist->string id))
    ((when (vl-keyword-lookup
                name1
                (vl-lexstate->kwdtable (vl-lexstate-init config))))
     (mv
      (cw
       "Preprocessor error (~s0): keyword ~s1 not permitted as `define argument~%"
       (vl-location-string (vl-echar->loc (car text)))
       name1)
      nil nil))
    ((mv ?ws rest)
     (vl-read-while-whitespace rest))
    (formal1 (make-vl-define-formal :name name1
                                    :default ""))
    ((when (and (consp rest)
                (eql (vl-echar->char (car rest)) #\))))
     (mv t (list formal1) (cdr rest)))
    ((unless (and (consp rest)
                  (eql (vl-echar->char (car rest)) #\,)))
     (mv
      (cw
       "Preprocessor error (~s0): expected next `define argument or end of arguments.~%"
       (vl-location-string (if (consp rest)
                               (vl-echar->loc (car rest))
                             (vl-echar->loc (car text)))))
      nil nil))
    (starting-loc (vl-echar->loc (car rest)))
    (rest (cdr rest))
    ((mv rest-okp rest-formals body)
     (vl-parse-define-formal-arguments rest config starting-loc))
    ((unless rest-okp) (mv nil nil nil))
    (formals (cons formal1 rest-formals)))
   (mv t formals body))))

Theorem: booleanp-of-vl-parse-define-formal-arguments.successp

(defthm booleanp-of-vl-parse-define-formal-arguments.successp
 (b* (((mv ?successp ?formals ?body)
       (vl-parse-define-formal-arguments text config starting-loc)))
   (booleanp successp))
 :rule-classes :type-prescription)

Theorem: vl-define-formallist-p-of-vl-parse-define-formal-arguments.formals

(defthm
 vl-define-formallist-p-of-vl-parse-define-formal-arguments.formals
 (b* (((mv ?successp ?formals ?body)
       (vl-parse-define-formal-arguments text config starting-loc)))
   (vl-define-formallist-p formals))
 :rule-classes :rewrite)

Theorem: vl-echarlist-p-of-vl-parse-define-formal-arguments.body

(defthm vl-echarlist-p-of-vl-parse-define-formal-arguments.body
 (implies
   (force (vl-echarlist-p text))
   (b*
     (((mv ?successp ?formals ?body)
       (vl-parse-define-formal-arguments text config starting-loc)))
     (vl-echarlist-p body)))
 :rule-classes :rewrite)