• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
        • Preprocessor
        • Vl-loadconfig
        • 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->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
        • Vl-loadstate
        • Parser
        • Vl-load-merge-descriptions
        • Scope-of-defines
        • Vl-load-file
        • Vl-flush-out-descriptions
        • Vl-description
        • Vl-loadresult
        • Vl-read-file
        • Vl-find-basename/extension
        • Vl-find-file
        • Vl-read-files
        • Extended-characters
        • Vl-load
        • Vl-load-main
        • Vl-load-description
        • Vl-descriptions-left-to-load
        • Inject-warnings
        • Vl-load-descriptions
        • Vl-load-files
        • Vl-load-summary
        • Vl-collect-modules-from-descriptions
        • Vl-descriptionlist
      • Transforms
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • 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)

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