		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Vl-substitute-into-macro-text

Signature
(vl-substitute-into-macro-text body subst name loc config acc) → (mv successp acc)
Arguments: body — Characters in the macro's body, which we recur through.
Guard (vl-echarlist-p body).; subst — The substitution being made, an alist binding formals to actuals.
Guard (and (alistp subst) (string-listp (alist-keys subst)) (string-listp (alist-vals subst))) .; name — Name of the text macro being expanded, for error messages.
Guard (stringp name).; loc — Location of the text macro being expanded, for error messages and also becomes the new location for each character being created.
Guard (vl-location-p loc).; config — Guard (vl-loadconfig-p config).; acc — Accumulated extended characters to be inserted into the file.
Guard (vl-echarlist-p acc).
Returns: successp — Type (booleanp successp).; acc — Accumulated characters, still in reverse order.
Type (vl-echarlist-p acc), given (and (force (vl-echarlist-p body)) (force (vl-echarlist-p acc))).

This is very underspecified. We need to minimally skip over things like string literals. We can at least assume that the body was accepted by vl-read-until-end-of-define. We try to do something reasonably sensible.

Definitions and Theorems

Function: vl-substitute-into-macro-text

(defun
 vl-substitute-into-macro-text
 (body subst name loc config acc)
 (declare (xargs :guard (and (vl-echarlist-p body)
                             (and (alistp subst)
                                  (string-listp (alist-keys subst))
                                  (string-listp (alist-vals subst)))
                             (stringp name)
                             (vl-location-p loc)
                             (vl-loadconfig-p config)
                             (vl-echarlist-p acc))))
 (let
  ((__function__ 'vl-substitute-into-macro-text))
  (declare (ignorable __function__))
  (b*
   (((when (atom body)) (mv t acc))
    (char1 (vl-echar->char (first body)))
    ((when (eql char1 #\`))
     (b*
      (((mv name prefix remainder)
        (vl-read-identifier (cdr body)))
       ((unless name)
        (mv
         (cw
          "Preprocessor error (~s0): bad grave character in macro ~
                       text for ~s1.~%"
          (vl-location-string loc)
          name)
         acc))
       (acc (revappend prefix (cons (car body) acc))))
      (vl-substitute-into-macro-text
           remainder subst name loc config acc)))
    ((when (eql char1 #\"))
     (b*
      (((mv string prefix remainder)
        (vl-read-string body (vl-lexstate-init config)))
       ((unless string)
        (mv
         (cw
          "Preprocessor error (~s0): bad string literal in macro ~
                       text for ~s1.~%"
          (vl-location-string loc)
          name)
         acc))
       (acc (revappend prefix acc)))
      (vl-substitute-into-macro-text
           remainder subst name loc config acc)))
    ((when (eql char1 #\\))
     (b*
      (((mv name prefix remainder)
        (vl-read-escaped-identifier body))
       ((unless name)
        (mv
         (cw
          "Preprocessor error (~s0): stray backslash in macro ~
                       text for ~s1.~%"
          (vl-location-string loc)
          name)
         acc))
       (acc (revappend prefix acc)))
      (vl-substitute-into-macro-text
           remainder subst name loc config acc)))
    ((when (eql char1 #\/))
     (b*
      (((when (vl-matches-string-p "//" body))
        (mv
         (cw
          "Preprocessor error (~s0): //-style comment in macro ~
                       text for ~s1? Jared thinks this shouldn't happen.~%"
          (vl-location-string loc)
          name)
         acc))
       ((when (vl-matches-string-p "/*" body))
        (b*
         (((mv successp prefix remainder)
           (vl-read-through-literal "*/" (cddr body)))
          ((unless successp)
           (mv
            (cw
             "Preprocessor error (~s0): unterminated /* ... */ ~
                             style comment in macro text for ~s1?  Jared ~
                             thinks this shouldn't happen."
             (vl-location-string loc)
             name)
            acc))
          (acc (revappend (list* (first body)
                                 (second body)
                                 prefix)
                          acc)))
         (vl-substitute-into-macro-text
              remainder subst name loc config acc))))
      (vl-substitute-into-macro-text
           (cdr body)
           subst
           name loc config (cons (car body) acc))))
    ((unless (vl-simple-id-head-p char1))
     (vl-substitute-into-macro-text
          (cdr body)
          subst
          name loc config (cons (car body) acc)))
    ((mv prefix remainder)
     (vl-read-simple-identifier body))
    (str (vl-echarlist->string prefix))
    (look (assoc-equal str subst))
    ((unless look)
     (vl-substitute-into-macro-text
          remainder subst
          name loc config (revappend prefix acc)))
    (replacement-str (cdr look))
    (replacement-echars (vl-echarlist-from-str replacement-str))
    (replacement-fixed
         (vl-change-echarlist-locations replacement-echars loc))
    (acc (revappend replacement-fixed acc)))
   (vl-substitute-into-macro-text
        remainder subst name loc config acc))))

Theorem: booleanp-of-vl-substitute-into-macro-text.successp

(defthm
 booleanp-of-vl-substitute-into-macro-text.successp
 (b*
  (((mv ?successp ?acc)
    (vl-substitute-into-macro-text body subst name loc config acc)))
  (booleanp successp))
 :rule-classes :type-prescription)

Theorem: vl-echarlist-p-of-vl-substitute-into-macro-text.acc

(defthm vl-echarlist-p-of-vl-substitute-into-macro-text.acc
        (implies (and (force (vl-echarlist-p body))
                      (force (vl-echarlist-p acc)))
                 (b* (((mv ?successp ?acc)
                       (vl-substitute-into-macro-text
                            body subst name loc config acc)))
                     (vl-echarlist-p acc)))
        :rule-classes :rewrite)