• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Fgl
      • Vwsim
      • Vl
        • Syntax
        • Loader
          • Preprocessor
          • Vl-loadconfig
          • Vl-loadstate
          • Lexer
            • Lex-strings
            • Lex-identifiers
            • Vl-typo-uppercase-p
            • Vl-typo-number-p
            • Vl-typo-lowercase-p
            • Lex-numbers
            • Chartypes
            • Vl-lex
            • Defchar
            • Tokens
            • Lex-keywords
            • Lexstate
              • Vl-lexstate-p
                • Vl-lexstate
                  • Make-vl-lexstate
                  • Change-vl-lexstate
                  • Honsed-vl-lexstate
                  • Make-honsed-vl-lexstate
                  • Vl-lexstate->xorops
                  • Vl-lexstate->timelitsp
                  • Vl-lexstate->strextsp
                  • Vl-lexstate->starops
                  • Vl-lexstate->remops
                  • Vl-lexstate->quotesp
                  • Vl-lexstate->poundops
                  • Vl-lexstate->plusops
                  • Vl-lexstate->onestepp
                  • Vl-lexstate->lessops
                  • Vl-lexstate->kwdtable
                  • Vl-lexstate->gtops
                  • Vl-lexstate->extintsp
                  • Vl-lexstate->eqops
                  • Vl-lexstate->dotops
                  • Vl-lexstate->dollarops
                  • Vl-lexstate->divops
                  • Vl-lexstate->dashops
                  • Vl-lexstate->colonops
                  • Vl-lexstate->barops
                  • Vl-lexstate->bangops
                  • Vl-lexstate->andops
                • Vl-plaintoken-alistp
                • *vl-2012-strict-lexstate*
                • Vl-lexstate->plainalist
                • Vl-lexstate-init
                • *vl-2005-strict-lexstate*
                • *vl-2012-lexstate*
                • *vl-2005-lexstate*
              • Make-test-tokens
              • Lexer-utils
              • Lex-comments
              • Vl-typo-uppercase-list-p
              • Vl-typo-lowercase-list-p
              • Vl-typo-number-list-p
            • 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-lexstate-p

    Vl-lexstate

    Raw constructor for vl-lexstate-p structures.

    Syntax:

    (vl-lexstate kwdtable bangops poundops 
                 remops andops starops plusops dashops 
                 dotops divops colonops lessops gtops 
                 eqops xorops barops dollarops quotesp 
                 strextsp timelitsp extintsp onestepp)

    This is the lowest-level constructor for vl-lexstate-p structures. It simply conses together a structure with the specified fields.

    Note: It's generally better to use macros like make-vl-lexstate or change-vl-lexstate instead. These macros lead to more readable and robust code, because you don't have to remember the order of the fields.

    The vl-lexstate-p structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see honsed-vl-lexstate instead.

    Definition

    This is an ordinary constructor function introduced by defaggregate.

    Function: vl-lexstate

    (defun vl-lexstate (kwdtable bangops poundops
                                 remops andops starops plusops dashops
                                 dotops divops colonops lessops gtops
                                 eqops xorops barops dollarops quotesp
                                 strextsp timelitsp extintsp onestepp)
      (declare (xargs :guard (and (vl-keyword-table-p kwdtable)
                                  (vl-plaintoken-alistp bangops)
                                  (vl-plaintoken-alistp poundops)
                                  (vl-plaintoken-alistp remops)
                                  (vl-plaintoken-alistp andops)
                                  (vl-plaintoken-alistp starops)
                                  (vl-plaintoken-alistp plusops)
                                  (vl-plaintoken-alistp dashops)
                                  (vl-plaintoken-alistp dotops)
                                  (vl-plaintoken-alistp divops)
                                  (vl-plaintoken-alistp colonops)
                                  (vl-plaintoken-alistp lessops)
                                  (vl-plaintoken-alistp gtops)
                                  (vl-plaintoken-alistp eqops)
                                  (vl-plaintoken-alistp xorops)
                                  (vl-plaintoken-alistp barops)
                                  (vl-plaintoken-alistp dollarops)
                                  (booleanp quotesp)
                                  (booleanp strextsp)
                                  (booleanp timelitsp)
                                  (booleanp extintsp)
                                  (booleanp onestepp))))
      (cons (cons (cons (cons kwdtable bangops)
                        (cons poundops (cons remops andops)))
                  (cons (cons starops (cons plusops dashops))
                        (cons dotops (cons divops colonops))))
            (cons (cons (cons lessops gtops)
                        (cons eqops (cons xorops barops)))
                  (cons (cons dollarops (cons quotesp strextsp))
                        (cons timelitsp (cons extintsp onestepp))))))