• 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-parse-define-actual
              • Vl-parse-define-actuals
              • 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
    • Vl-expand-define

    Vl-parse-define-actuals

    Collect the arguments to a macro, like `max(a+b, c).

    Signature
    (vl-parse-define-actuals name echars loc ppst) 
      → 
    (mv successp actuals remainder ppst)
    Arguments
    name — Name of macro being expanded, e.g., max, for error messages.
        Guard (stringp name).
    echars — Text that follows the initial open paren, or that follows a comma.
        Guard (vl-echarlist-p echars).
    loc — Location information in case of error messages.
        Guard (vl-location-p loc).
    Returns
    successp — Type (booleanp successp).
    actuals — Type (string-listp actuals).
    remainder — Remainder of the input stream after eating all the actuals and also the closing paren.
        Type (vl-echarlist-p remainder).

    Definitions and Theorems

    Function: vl-parse-define-actuals

    (defun vl-parse-define-actuals (name echars loc ppst)
      (declare (xargs :stobjs (ppst)))
      (declare (xargs :guard (and (stringp name)
                                  (vl-echarlist-p echars)
                                  (vl-location-p loc))))
      (let ((__function__ 'vl-parse-define-actuals))
        (declare (ignorable __function__))
        (b* (((mv successp morep actual1 echars ppst)
              (vl-parse-define-actual name echars loc nil nil ppst))
             ((unless successp)
              (mv nil nil echars ppst))
             ((unless morep)
              (mv t (list actual1) echars ppst))
             ((mv successp rest-actuals echars ppst)
              (vl-parse-define-actuals name echars loc ppst))
             ((unless successp)
              (mv nil nil echars ppst)))
          (mv t (cons actual1 rest-actuals)
              echars ppst))))

    Theorem: booleanp-of-vl-parse-define-actuals.successp

    (defthm booleanp-of-vl-parse-define-actuals.successp
      (b* (((mv ?successp ?actuals ?remainder ?ppst)
            (vl-parse-define-actuals name echars loc ppst)))
        (booleanp successp))
      :rule-classes :type-prescription)

    Theorem: string-listp-of-vl-parse-define-actuals.actuals

    (defthm string-listp-of-vl-parse-define-actuals.actuals
      (b* (((mv ?successp ?actuals ?remainder ?ppst)
            (vl-parse-define-actuals name echars loc ppst)))
        (string-listp actuals))
      :rule-classes :rewrite)

    Theorem: vl-echarlist-p-of-vl-parse-define-actuals.remainder

    (defthm vl-echarlist-p-of-vl-parse-define-actuals.remainder
      (b* (((mv ?successp ?actuals ?remainder ?ppst)
            (vl-parse-define-actuals name echars loc ppst)))
        (vl-echarlist-p remainder))
      :rule-classes :rewrite)