• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • 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

Honsed-vl-lexstate

Raw constructor for honsed vl-lexstate-p structures.

Syntax:

(honsed-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 identical to vl-lexstate, except that we hons the structure we are creating.

Definition

This is an ordinary honsing constructor introduced by defaggregate.

Function: honsed-vl-lexstate

(defun honsed-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))))
 (mbe
    :logic (vl-lexstate kwdtable bangops poundops
                        remops andops starops plusops dashops
                        dotops divops colonops lessops gtops
                        eqops xorops barops dollarops quotesp
                        strextsp timelitsp extintsp onestepp)
    :exec
    (hons (hons (hons (hons kwdtable bangops)
                      (hons poundops (hons remops andops)))
                (hons (hons starops (hons plusops dashops))
                      (hons dotops (hons divops colonops))))
          (hons (hons (hons lessops gtops)
                      (hons eqops (hons xorops barops)))
                (hons (hons dollarops (hons quotesp strextsp))
                      (hons timelitsp (hons extintsp onestepp)))))))