		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Vl-split-define-text

Split up the rest of a define line into macro arguments and macro text.

Signature
(vl-split-define-text text ppst) → (mv successp formals body ppst)
Arguments: text — The text that occurs after `define foo, perhaps including any macro arguments such as (a,b) in the case of macros such as `define max(a,b) ....
Guard (vl-echarlist-p text).
Returns: successp — Type (booleanp successp).; formals — Type (vl-define-formallist-p formals).; body — Remaining characters after any macro arguments.
Type (vl-echarlist-p body).

Definitions and Theorems

Function: vl-split-define-text

(defun vl-split-define-text (text ppst)
  (declare (xargs :stobjs (ppst)))
  (declare (xargs :guard (vl-echarlist-p text)))
  (let ((__function__ 'vl-split-define-text))
    (declare (ignorable __function__))
    (b* ((text (vl-echarlist-fix text))
         ((unless (and (consp text)
                       (eql (vl-echar->char (car text)) #\()))
          (mv t nil (vl-echarlist-fix text)
              ppst)))
      (vl-parse-define-formal-arguments (cdr text)
                                        (vl-echar->loc (car text))
                                        ppst))))

Theorem: booleanp-of-vl-split-define-text.successp

(defthm booleanp-of-vl-split-define-text.successp
  (b* (((mv ?successp ?formals ?body ?ppst)
        (vl-split-define-text text ppst)))
    (booleanp successp))
  :rule-classes :type-prescription)

Theorem: vl-define-formallist-p-of-vl-split-define-text.formals

(defthm vl-define-formallist-p-of-vl-split-define-text.formals
  (b* (((mv ?successp ?formals ?body ?ppst)
        (vl-split-define-text text ppst)))
    (vl-define-formallist-p formals))
  :rule-classes :rewrite)

Theorem: vl-echarlist-p-of-vl-split-define-text.body

(defthm vl-echarlist-p-of-vl-split-define-text.body
  (b* (((mv ?successp ?formals ?body ?ppst)
        (vl-split-define-text text ppst)))
    (vl-echarlist-p body))
  :rule-classes :rewrite)

Subtopics

Vl-parse-define-formal-arguments