		Search-engine friendly clone of the ACL2 documentation.

Vl-split-define-text

Vl-parse-define-formal-arguments

Signature
(vl-parse-define-formal-arguments text starting-loc ppst) → (mv successp formals body ppst)
Arguments: text — Text after the opening paren, or after some comma.
Guard (vl-echarlist-p text).; 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).

Definitions and Theorems

Function: vl-parse-define-formal-arguments

(defun vl-parse-define-formal-arguments (text starting-loc ppst)
 (declare (xargs :stobjs (ppst)))
 (declare (xargs :guard (and (vl-echarlist-p text)
                             (vl-location-p starting-loc))))
 (let ((__function__ 'vl-parse-define-formal-arguments))
  (declare (ignorable __function__))
  (b*
   ((text (vl-echarlist-fix text))
    ((when (atom text))
     (let
      ((ppst
        (vl-ppst-fatal :msg "~a0: `define arguments are not closed."
                       :args (list starting-loc))))
      (mv nil nil nil ppst)))
    ((mv ?ws rest)
     (vl-read-while-whitespace text))
    ((mv id rest)
     (vl-read-simple-identifier rest))
    ((unless id)
     (let
      ((ppst
           (vl-ppst-fatal :msg "~a0: invalid `define argument name."
                          :args (list (vl-echar->loc (car text))))))
      (mv nil nil nil ppst)))
    (name1 (vl-echarlist->string id))
    ((mv ?ws rest)
     (vl-read-while-whitespace rest))
    ((mv okp default rest ppst)
     (b* (((unless (and (consp rest)
                        (eql (vl-echar->char (car rest)) #\=)))
           (mv t nil rest ppst))
          (rest (cdr rest))
          ((mv okp prefix rest ppst)
           (vl-read-define-default-text rest starting-loc ppst)))
       (mv okp (vl-echarlist->string prefix)
           rest ppst)))
    ((unless okp) (mv nil nil nil ppst))
    ((mv ?ws rest)
     (vl-read-while-whitespace rest))
    (formal1 (make-vl-define-formal :name name1
                                    :default default))
    ((when (and (consp rest)
                (eql (vl-echar->char (car rest)) #\))))
     (mv t (list formal1) (cdr rest) ppst))
    ((unless (and (consp rest)
                  (eql (vl-echar->char (car rest)) #\,)))
     (let
      ((ppst
        (vl-ppst-fatal
          :msg
          "~a0: expected next `define argument or end of arguments."
          :args (list (if (consp rest)
                          (vl-echar->loc (car rest))
                        (vl-echar->loc (car text)))))))
      (mv nil nil nil ppst)))
    (starting-loc (vl-echar->loc (car rest)))
    (rest (cdr rest))
    ((mv rest-okp rest-formals body ppst)
     (vl-parse-define-formal-arguments rest starting-loc ppst))
    ((unless rest-okp)
     (mv nil nil nil ppst))
    (formals (cons formal1 rest-formals)))
   (mv t formals body ppst))))

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

(defthm booleanp-of-vl-parse-define-formal-arguments.successp
  (b* (((mv ?successp ?formals ?body ?ppst)
        (vl-parse-define-formal-arguments text starting-loc ppst)))
    (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 ?ppst)
       (vl-parse-define-formal-arguments text starting-loc ppst)))
   (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
  (b* (((mv ?successp ?formals ?body ?ppst)
        (vl-parse-define-formal-arguments text starting-loc ppst)))
    (vl-echarlist-p body))
  :rule-classes :rewrite)