		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Vl-substitute-into-macro-text

Signature
(vl-substitute-into-macro-text body subst name loc acc ppst) → (mv successp acc ppst)
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).; 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).

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 acc ppst)
 (declare (xargs :stobjs (ppst)))
 (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-echarlist-p acc))))
 (let ((__function__ 'vl-substitute-into-macro-text))
  (declare (ignorable __function__))
  (b*
   ((body (vl-echarlist-fix body))
    (acc (vl-echarlist-fix acc))
    ((when (atom body)) (mv t acc ppst))
    (char1 (vl-echar->char (first body)))
    ((when (eql char1 #\`))
     (b*
      (((when (and (consp (cdr body))
                   (member (vl-echar->char (second body))
                           '(#\" #\`))))
        (case
         (vl-echar->char (second body))
         (#\"
          (b* ((acc (cons (second body) acc)))
           (vl-substitute-into-macro-text (cddr body)
                                          subst name loc acc ppst)))
         (#\`
            (vl-substitute-into-macro-text (cddr body)
                                           subst name loc acc ppst))
         (otherwise (mv (impossible) acc ppst))))
       ((when (and (consp (cdr body))
                   (consp (cddr body))
                   (consp (cdddr body))
                   (eql (vl-echar->char (second body)) #\\)
                   (eql (vl-echar->char (third body)) #\`)
                   (eql (vl-echar->char (fourth body))
                        #\")))
        (b* ((acc (list* (fourth body)
                         (second body)
                         acc)))
          (vl-substitute-into-macro-text (cddddr body)
                                         subst name loc acc ppst))))
      (vl-substitute-into-macro-text
           (cdr body)
           subst name loc (cons (car body) acc)
           ppst)))
    ((when (eql char1 #\"))
     (b*
      (((mv string prefix remainder)
        (vl-read-string body
                        (vl-lexstate-init (vl-ppst->config))))
       ((unless string)
        (let
         ((ppst
           (vl-ppst-fatal
               :msg "~a0: bad string literal in macro text for ~s1."
               :args (list loc name))))
         (mv nil acc ppst)))
       (acc (revappend prefix acc)))
      (vl-substitute-into-macro-text
           remainder subst name loc acc ppst)))
    ((when (eql char1 #\\))
     (vl-substitute-into-macro-text
          (cdr body)
          subst name loc (cons (car body) acc)
          ppst))
    ((when (eql char1 #\/))
     (b*
      (((when (vl-matches-string-p "//" body))
        (let
         ((ppst
           (vl-ppst-fatal
            :msg
            "~a0: //-style comment in macro text for ~s1? ~
                                 Jared thinks this shouldn't happen."
            :args (list loc name))))
         (mv nil acc ppst)))
       ((when (vl-matches-string-p "/*" body))
        (b*
         (((mv successp prefix remainder)
           (vl-read-through-literal "*/" (cddr body)))
          ((unless successp)
           (let
            ((ppst
              (vl-ppst-fatal
               :msg
               "~a0: unterminated /* ... */ style ~
                                       comment in macro text for ~s1?  Jared ~
                                       thinks this shouldn't happen."
               :args (list loc name))))
            (mv nil acc ppst)))
          (acc (revappend (list* (first body)
                                 (second body)
                                 prefix)
                          acc)))
         (vl-substitute-into-macro-text
              remainder subst name loc acc ppst))))
      (vl-substitute-into-macro-text
           (cdr body)
           subst name loc (cons (car body) acc)
           ppst)))
    ((unless (vl-simple-id-head-p char1))
     (vl-substitute-into-macro-text
          (cdr body)
          subst name loc (cons (car body) acc)
          ppst))
    ((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 (revappend prefix acc)
          ppst))
    (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 acc ppst))))

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

(defthm booleanp-of-vl-substitute-into-macro-text.successp
  (b*
    (((mv ?successp ?acc ?ppst)
      (vl-substitute-into-macro-text body subst name loc acc ppst)))
    (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
  (b*
    (((mv ?successp ?acc ?ppst)
      (vl-substitute-into-macro-text body subst name loc acc ppst)))
    (vl-echarlist-p acc))
  :rule-classes :rewrite)