		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Vl-read-define-default-text

Signature
(vl-read-define-default-text echars starting-loc ppst) → (mv successp prefix remainder ppst)
Arguments: echars — Text starting just after the equal sign.
Guard (vl-echarlist-p echars).; starting-loc — Context for error messages.
Guard (vl-location-p starting-loc).
Returns: successp — Type (booleanp successp).; prefix — Type (vl-echarlist-p prefix).; remainder — On success this should start with a comma or endparen.
Type (vl-echarlist-p remainder).

Definitions and Theorems

Function: vl-read-define-default-text

(defun vl-read-define-default-text (echars starting-loc ppst)
 (declare (xargs :stobjs (ppst)))
 (declare (xargs :guard (and (vl-echarlist-p echars)
                             (vl-location-p starting-loc))))
 (let ((__function__ 'vl-read-define-default-text))
  (declare (ignorable __function__))
  (b*
   ((echars (vl-echarlist-fix echars))
    ((when (atom echars))
     (let
      ((ppst
            (vl-ppst-fatal
                 :msg "~a0: EOF while reading `define default text."
                 :args (list starting-loc))))
      (mv nil nil echars ppst)))
    (char1 (vl-echar->char (car echars)))
    ((when (or (eql char1 #\,) (eql char1 #\))))
     (mv t nil echars ppst))
    ((when (eql char1 #\\))
     (b*
      (((mv name prefix1 remainder)
        (vl-read-escaped-identifier echars))
       ((unless name)
        (let
         ((ppst
           (vl-ppst-fatal
             :msg "~a0: stray backslash in define default argument?"
             :args (list (vl-echar->loc (car echars))))))
         (mv nil nil echars ppst)))
       ((mv okp prefix2 remainder ppst)
        (vl-read-define-default-text remainder starting-loc ppst))
       ((unless okp) (mv nil nil echars ppst)))
      (mv t (append prefix1 prefix2)
          remainder ppst)))
    ((when (eql char1 #\"))
     (b*
      (((mv string prefix1 remainder)
        (vl-read-string echars
                        (vl-lexstate-init (vl-ppst->config))))
       ((unless string)
        (let
         ((ppst
           (vl-ppst-fatal
            :msg
            "~a0: unterminated string literal in `define default argument?"
            :args (list (vl-echar->loc (car echars))))))
         (mv nil nil echars ppst)))
       ((mv okp prefix2 remainder ppst)
        (vl-read-define-default-text remainder starting-loc ppst))
       ((unless okp) (mv nil nil echars ppst)))
      (mv t (append prefix1 prefix2)
          remainder ppst)))
    ((mv okp rest remainder ppst)
     (vl-read-define-default-text (cdr echars)
                                  starting-loc ppst))
    ((unless okp) (mv nil nil echars ppst)))
   (mv t (cons (car echars) rest)
       remainder ppst))))

Theorem: booleanp-of-vl-read-define-default-text.successp

(defthm booleanp-of-vl-read-define-default-text.successp
  (b* (((mv ?successp ?prefix ?remainder ?ppst)
        (vl-read-define-default-text echars starting-loc ppst)))
    (booleanp successp))
  :rule-classes :type-prescription)

Theorem: vl-echarlist-p-of-vl-read-define-default-text.prefix

(defthm vl-echarlist-p-of-vl-read-define-default-text.prefix
  (b* (((mv ?successp ?prefix ?remainder ?ppst)
        (vl-read-define-default-text echars starting-loc ppst)))
    (vl-echarlist-p prefix))
  :rule-classes :rewrite)

Theorem: vl-echarlist-p-of-vl-read-define-default-text.remainder

(defthm vl-echarlist-p-of-vl-read-define-default-text.remainder
  (b* (((mv ?successp ?prefix ?remainder ?ppst)
        (vl-read-define-default-text echars starting-loc ppst)))
    (vl-echarlist-p remainder))
  :rule-classes :rewrite)

Theorem: true-listp-of-vl-read-define-default-text-prefix

(defthm true-listp-of-vl-read-define-default-text-prefix
 (true-listp
    (mv-nth 1
            (vl-read-define-default-text echars starting-loc ppst)))
 :rule-classes :type-prescription)

Theorem: true-listp-of-vl-read-define-default-text-remainder

(defthm true-listp-of-vl-read-define-default-text-remainder
 (true-listp
    (mv-nth 2
            (vl-read-define-default-text echars starting-loc ppst)))
 :rule-classes :type-prescription)

Theorem: acl2-count-of-vl-read-define-default-text-weak

(defthm acl2-count-of-vl-read-define-default-text-weak
 (<=
  (acl2-count
     (mv-nth
          2
          (vl-read-define-default-text echars config starting-loc)))
  (acl2-count (vl-echarlist-fix echars)))
 :rule-classes ((:rewrite) (:linear)))

Theorem: acl2-count-of-vl-read-define-default-text-strong

(defthm acl2-count-of-vl-read-define-default-text-strong
 (implies
  (mv-nth 1
          (vl-read-define-default-text echars config starting-loc))
  (<
   (acl2-count
     (mv-nth
          2
          (vl-read-define-default-text echars config starting-loc)))
   (acl2-count (vl-echarlist-fix echars))))
 :rule-classes ((:rewrite) (:linear)))