• 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
              • Parser
                • Parse-keyword
                • Parse-variable-declaration
                • Parse-symbol
                • Parse-literal
                • Parse-identifier
                • Hex-chars-and-uscores-to-hex-string-rest-element-list
                • Parse-assignment-statement
                • Parse-identifier-and-open-paren
                • Parse-*-comma-identifier
                • Parse-*-.-identifier
                • Parse-continue-statement
                • Parse-*-comma-path
                • Parse-path
                • Parse-leave-statement
                • Parse-break-statement
                • Cst2ast-hex-string
                • Cst2ast-string-literal-content
                • Cst2ast-escape-sequence
                • Cst2ast-string-literal-contents
                • Cst2ast-quoted-printable
                • Parse-yul
                • Cst2ast-string-literal
                • Parse-yul-bytes
                • Cst2ast-hex-number
                • Cst2ast-uhhhh
                • Cst2ast-literal-kind
                • Cst2ast-decimal-number
                • Cst2ast-xhh
                • Cst2ast-single-char
                • Cst2ast-boolean
                • Parse-*-case-clause
                • Looks-like-hex-string-fringe
                • Cst2ast-hex-digit-char-list
                • Parse-*-statement
                • Parse-*-comma-expression
                • Parse-switch-statement
                • Parse-if-statement
                • Parse-for-statement
                • Parse-expression
                • Parse-case-clause
                • Parse-fundef
                • Parse-function-call
                • Parse-block
                • *single-quote-tree-list*
                • *double-quote-tree-list*
                • *yul-keywords*
                • *single-quoted-content-rulenames*
                • *list-leafterm-x*
                • *list-leafterm-u*
                • *list-leafterm-92*
                • *double-quoted-content-rulenames*
                • *yul-symbols*
              • 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

Parser

An executable parser of Yul.

This is a simple parser for Yul code. The parser lexes and tokenizes according to the lexical grammar rules, and then parses according to the syntactic grammar rules. See grammar.

The primary API for parsing Yul is parse-yul and parse-yul-bytes.

Subtopics

Parse-keyword
Attempts to eat the named keyword.
Parse-variable-declaration
Attempts to eat a variable declaration and build a statement AST node of kind :variable-single or :variable-multi.
Parse-symbol
Attempts to eat the named symbol, returning either the list of remaining tokens or a reserr.
Parse-literal
Attempts to eat a literal and build a literal AST node.
Parse-identifier
Attempts to eat an identifier token and build an identifier AST node.
Hex-chars-and-uscores-to-hex-string-rest-element-list
Map the characters of a hex string after the first two to a list of hex string elements.
Parse-assignment-statement
Attempts to eat an assignment statement and build a statement AST node of kind :assign-single or :assign-multiple.
Parse-identifier-and-open-paren
Attempts to eat an identifier and a following open parenthesis, and build an identifier AST node.
Parse-*-comma-identifier
Parses zero or more occurrences of '"," identifier' and returns a list of identifier AST nodes.
Parse-*-.-identifier
Parses zero or more occurrences of '"." identifier' and returns a list of identifier AST nodes.
Parse-continue-statement
Attempts to eat a "continue" keyword and build a statement AST node of kind :continue.
Parse-*-comma-path
Parses zero or more occurrences of '"," path' and returns a list of path AST nodes.
Parse-path
Attempts to eat a path and build a path AST node.
Parse-leave-statement
Attempts to eat a "leave" keyword and build a statement AST node of kind :leave.
Parse-break-statement
Attempts to eat a "break" keyword and build a statement AST node of kind :break.
Cst2ast-hex-string
Given a :nonleaf tree with rulename "hex-string", return the appropriate literal AST node.
Cst2ast-string-literal-content
Cst2ast-escape-sequence
Cst2ast-string-literal-contents
Cst2ast-quoted-printable
Given a :nonleaf tree for rulename "single-quoted-printable" or "double-quoted-printable", returns a string-element-char.
Parse-yul
Parses a Yul source program string into abstract syntax.
Cst2ast-string-literal
Given a :nonleaf tree with rulename "string-literal", return the appropriate literal AST node.
Parse-yul-bytes
Parses the Yul source program bytes into abstract syntax.
Cst2ast-hex-number
Given a :nonleaf tree with rulename "hex-number", return the appropriate literal AST node.
Cst2ast-uhhhh
Cst2ast-literal-kind
Given a tree under :nonleaf literal, return the appropriate literal AST node.
Cst2ast-decimal-number
Given a :nonleaf ABNF tree with rulename "decimal-number", return the appropriate literal AST node.
Cst2ast-xhh
Cst2ast-single-char
Cst2ast-boolean
Given a :nonleaf tree with rulename "boolean", return the appropriate literal AST node.
Parse-*-case-clause
Eats as many case clauses and possible (zero or more).
Looks-like-hex-string-fringe
Cst2ast-hex-digit-char-list
Parse-*-statement
Eats as many statements as possible (zero or more).
Parse-*-comma-expression
Parses zero or more occurrences of '"," expression' and returns a list of expression AST nodes.
Parse-switch-statement
Eats a switch statement and builds a statement AST node of kind :switch.
Parse-if-statement
Eats an if statement and builds a statement AST node of kind :if.
Parse-for-statement
Eats a for statement and builds a statement AST node of kind :for.
Parse-expression
Attempts to eat an expression and build an expression AST node.
Parse-case-clause
Eats a case clause for a switch statement and builds an swcase AST node.
Parse-fundef
Eats a function definition and builds a fundef AST node.
Parse-function-call
Attempts to eat a function call and build a funcall AST node.
Parse-block
Eats a block (delimited by { }) and builds a block AST node.
*single-quote-tree-list*
A CST for the single quote start or end of a Yul string.
*double-quote-tree-list*
A CST for the double quote start or end of a Yul string.
*yul-keywords*
*single-quoted-content-rulenames*
*list-leafterm-x*
*list-leafterm-u*
*list-leafterm-92*
*double-quoted-content-rulenames*
*yul-symbols*