• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Fgl
      • Vwsim
      • Vl
        • Syntax
        • Loader
          • Preprocessor
            • Vl-iframe
            • Preprocessor-ifdef-minutia
            • Vl-preprocess
            • Vl-preprocess-loop
            • Vl-includeskips
            • Vl-read-until-end-of-define
            • Vl-define-formallist->defaults
            • Vl-define
            • Vl-expand-define
            • Vl-read-include
            • Vl-substitute-into-macro-text
              • Vl-process-ifdef
              • Ppst
              • Vl-read-define-default-text
              • Vl-process-define
              • Preprocessor-include-minutia
              • Vl-trim-for-preproc
              • Vl-line-up-define-formals-and-actuals
              • Vl-process-undef
              • Vl-split-define-text
              • Vl-def-context
              • Vl-process-endif
              • Scan-backward-for-non-whitespace
              • Vl-ifdef-context
              • Scan-backward-for-whitespace
              • Vl-atvl-atts-text
              • Scan-for-non-whitespace
              • Vl-check-remaining-formals-all-have-defaults
              • Vl-process-else
              • Vl-is-compiler-directive-p
              • Vl-includeskips-controller-lookup
              • Vl-ifdef-use-map
              • Vl-defines
              • Vl-def-use-map
              • Vl-nice-bytes
              • Vl-safe-previous-n
              • Vl-safe-next-n
              • Vl-ppst-pad
              • Vl-filename-to-string-literal
              • Vl-maybe-update-filemap
              • *vl-preprocess-clock*
              • Vl-ppst->warnings
              • Vl-ppst->iskips
              • Vl-ppst->ifdefmap
              • Vl-ppst->idcache
              • Vl-istack
              • Vl-ppst->istack
              • Vl-ppst->includes
              • Vl-ppst->filemap
              • Vl-ppst->defmap
              • Vl-ppst->defines
              • Vl-ppst->config
              • Vl-ppst->bytes
              • Vl-ppst->activep
              • Vl-ppst->acc
              • Vl-ppst-record-ifdef-use
              • Vl-ppst-record-def-use
              • Vl-ifdef-context-list
              • Vl-def-context-list
              • Vl-ppst-update-warnings
              • Vl-ppst-update-istack
              • Vl-ppst-update-iskips
              • Vl-ppst-update-includes
              • Vl-ppst-update-ifdefmap
              • Vl-ppst-update-idcache
              • Vl-ppst-update-filemap
              • Vl-ppst-update-defmap
              • Vl-ppst-update-defines
              • Vl-ppst-update-config
              • Vl-ppst-update-activep
              • Vl-ppst-update-bytes
              • Vl-ppst-update-acc
              • Vl-ppst-unsound-nreverse-acc
            • Vl-loadconfig
            • Vl-loadstate
            • Lexer
            • Parser
            • Vl-load-merge-descriptions
            • Vl-find-basename/extension
            • Vl-load-file
            • Vl-loadresult
            • Scope-of-defines
            • Vl-find-file
            • Vl-flush-out-descriptions
            • Vl-description
            • Vl-read-file
            • Vl-includeskips-report-gather
            • Vl-load-main
            • Extended-characters
            • Vl-load
            • Vl-load-description
            • Vl-descriptions-left-to-load
            • Inject-warnings
            • Vl-preprocess-debug
            • Vl-write-preprocessor-debug-file
            • Vl-read-file-report-gather
            • Vl-load-descriptions
            • Vl-load-files
            • Translate-off
            • Vl-load-read-file-hook
            • Vl-read-file-report
            • Vl-loadstate-pad
            • Vl-load-summary
            • Vl-collect-modules-from-descriptions
            • Vl-loadstate->warnings
            • Vl-iskips-report
            • Vl-descriptionlist
          • Warnings
          • Getting-started
          • Utilities
          • Printer
          • Kit
          • Mlib
          • Transforms
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • 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)