• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
          • Transformations
          • Language
            • Abstract-syntax
            • Dynamic-semantics
            • Concrete-syntax
              • Lexer
                • Lex-keyword
                • Lex-group-escape-sequence-single
                • Lex-symbol
                • Lex-rest-of-block-comment-fns
                • Lex-group-for-hex-string
                • Lex-hex-digit
                • Lex-group-escape-sequence-body
                • Lex-whitespace-char
                • Lex-string-literal
                • Lex-literal
                • Lex-identifier-start
                • Lex-hex-string
                • Lex-single-quoted-printable
                • Lex-double-quoted-printable
                • Lex-group-optional-underbar-and-two-hex-digits
                • Lex-escape-sequence
                • Lex-token
                • Lex-not-star-or-slash
                • Lex-not-lf-or-cr
                • Lex-group-squoted-or-escape
                • Lex-group-dquoted-or-escape
                • Lex-optional-sequence-of-2hex-digits
                • Lex-decimal-number
                • Lex-lexeme
                • Lex-identifier-rest
                • Lex-end-of-line-comment
                • Lex-nonzero-decimal-digit
                • Lex-repetition-*-optional-underbar-and-two-hex-digits
                • Lex-not-star
                • Lex-comment
                • Lex-boolean
                • Lex-block-comment
                • Lex-uppercase-letter
                • Lex-lowercase-letter
                • Lex-identifier
                • Lex-hex-number
                • Lex-decimal-digit
                • Lex-squote
                • Lex-repetition-4-hex-digits
                • Lex-optional-underbar
                • Lex-dquote
                • Lex-repetition-*-squoted-or-escape
                • Lex-repetition-*-dquoted-or-escape
                • Lex-repetition-*-whitespace-char
                • Lex-repetition-*-identifier-rest
                • Lex-repetition-2-hex-digits
                • Lex-lf
                • Lex-cr
                • Lex-repetition-*-not-lf-or-cr
                • Lex-repetition-*-decimal-digit
                • Lexemeize-yul
                • Lex-repetition-*-lexeme
                • Lex-repetition-*-hex-digit
                • *defparse-yul-group-table*
                • Lex-whitespace
                • Lexemeize-yul-bytes
                • *defparse-yul-repetition-table*
                • *defparse-yul-option-table*
              • Parser
              • Grammar-old
              • Grammar
              • Tokenizer
            • Static-soundness
            • Static-semantics
            • Errors
          • Yul-json
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Lists-light
        • Axe
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Concrete-syntax

Lexer

An executable lexer of Yul.

This is a simple lexer for the Yul lexical grammar. The grammar is defined in ABNF. See grammar.

The primary API for lexing Yul is lexemeize-yul and lexemeize-yul-bytes.

The lexer is defined in three sections:

  1. Generation of specialized generator macros for this lexer.
  2. Table of lexing functions for groups, options, and repetitions that occur internally to Yul grammar rules.
  3. Definitions of lexing functions, most of which are just calls to macros that generate the functions, but some of which are hand-written due to limitations in the current parser generators.

Subtopics

Lex-keyword
Parse a keyword.
Lex-group-escape-sequence-single
Parse a ( squote / dquote / %s"\" / %s"n" / %s"r" / %s"t" / lf / cr ).
Lex-symbol
Parse a symbol.
Lex-rest-of-block-comment-fns
Mutually recursive part of block comment lexing.
Lex-group-for-hex-string
Parse a ( dquote [ 2hex-digit *( [ "_" ] 2hex-digit ) ] dquote / squote [ 2hex-digit *( [ "_" ] 2hex-digit ) ] squote ).
Lex-hex-digit
Parse a hex-digit.
Lex-group-escape-sequence-body
Parse a ( ( squote / dquote / %s"\" / %s"n" / %s"r" / %s"t" / lf / cr ) / %s"u" 4hex-digit / %s"x" 2hex-digit ).
Lex-whitespace-char
Parse a whitespace-char.
Lex-string-literal
Parse a string-literal.
Lex-literal
Parse a literal.
Lex-identifier-start
Parse a identifier-start.
Lex-hex-string
Parse a hex-string.
Lex-single-quoted-printable
Parse a single-quoted-printable.
Lex-double-quoted-printable
Parse a double-quoted-printable.
Lex-group-optional-underbar-and-two-hex-digits
Parse a ( [ "_" ] 2hex-digit ).
Lex-escape-sequence
Parse a escape-sequence.
Lex-token
Parse a token.
Lex-not-star-or-slash
Parse a not-star-or-slash.
Lex-not-lf-or-cr
Parse a not-lf-or-cr.
Lex-group-squoted-or-escape
Parse a ( single-quoted-printable / escape-sequence ).
Lex-group-dquoted-or-escape
Parse a ( double-quoted-printable / escape-sequence ).
Lex-optional-sequence-of-2hex-digits
Parse a [ 2hex-digit *( [ "_" ] 2hex-digit ) ].
Lex-decimal-number
Parse a decimal-number.
Lex-lexeme
Parse a lexeme.
Lex-identifier-rest
Parse a identifier-rest.
Lex-end-of-line-comment
Parse a end-of-line-comment.
Lex-nonzero-decimal-digit
Parse a nonzero-decimal-digit.
Lex-repetition-*-optional-underbar-and-two-hex-digits
Parse a *( [ "_" ] 2hex-digit ).
Lex-not-star
Parse a not-star.
Lex-comment
Parse a comment.
Lex-boolean
Parse a boolean.
Lex-block-comment
Parse a block-comment.
Lex-uppercase-letter
Parse a uppercase-letter.
Lex-lowercase-letter
Parse a lowercase-letter.
Lex-identifier
Parse a identifier.
Lex-hex-number
Parse a hex-number.
Lex-decimal-digit
Parse a decimal-digit.
Lex-squote
Parse a squote.
Lex-repetition-4-hex-digits
Lex exactly 4 hexadecimal digits.
Lex-optional-underbar
Parse a [ "_" ].
Lex-dquote
Parse a dquote.
Lex-repetition-*-squoted-or-escape
Parse a *( single-quoted-printable / escape-sequence ).
Lex-repetition-*-dquoted-or-escape
Parse a *( double-quoted-printable / escape-sequence ).
Lex-repetition-*-whitespace-char
Parse a *whitespace-char.
Lex-repetition-*-identifier-rest
Parse a *identifier-rest.
Lex-repetition-2-hex-digits
Lex exactly 2 hexadecimal digits.
Lex-lf
Parse a lf.
Lex-cr
Parse a cr.
Lex-repetition-*-not-lf-or-cr
Parse a *not-lf-or-cr.
Lex-repetition-*-decimal-digit
Parse a *decimal-digit.
Lexemeize-yul
Lexes the bytes of yul-string into a list of lexemes.
Lex-repetition-*-lexeme
Parse a *lexeme.
Lex-repetition-*-hex-digit
Parse a *hex-digit.
*defparse-yul-group-table*
Table of group parsing functions.
Lex-whitespace
Lex rule whitespace = 1*whitespace-char.
Lexemeize-yul-bytes
Lexes the bytes into a list of lexemes.
*defparse-yul-repetition-table*
Table of repetition parsing functions.
*defparse-yul-option-table*
Table of option parsing functions.