		Search-engine friendly clone of the ACL2 documentation.

Language

Abstract-syntax

Abstract syntax of Yul.

We introduce an abstract syntax of Yul based on its concrete syntax; more precisely, on the new grammar.

The abstract syntax defined here is fairly close to the concrete syntax, more precisely to the grammar, which already omits lexical entities like whitespace. The reason for this closeness is that we want to keep as much information as possible in the abstract syntax. In some cases our abstract syntax may be broader than the concrete syntax, to keep the definition of the abstract syntax slightly simpler; the important thing is that all the concrete syntax is representable in abstract syntax.

It is not yet clear whether the proper handling of Yul dialects will require extending this abstract syntax with types (which are not present in the new grammar). For now we omit types, but we may revisit this at some point.

Subtopics

Escape: Fixtype of escapes.
Hex-digit-list->chars: Extract the characters from a list of hex digits.
Swcase-list->value-list: Lift swcase->value to lists.
Fundef-list->name-list: Lift fundef->name to lists.
Literal: Fixtype of literals.
Path: Fixtype of paths.
Plain-string: Fixtype of plain strings.
String-element: Fixtype of string elements.
Identifier: Fixtype of identifiers.
Funcall-option: Fixtype of optional function calls.
Expression-option: Fixtype of optional expressions.
Statement-option: Fixtype of optional statements.
Literal-option: Fixtype of optional literals.
Identifier-option: Fixtype of optional identifiers.
Hex-string: Fixtype of hex strings.
Hex-quad: Fixtype of quadruples of hex digits.
Hex-digit: Fixtype of hex digits.
Data-value: Fixtype of data values in Yul objects.
Data-item: Fixtype of data items in Yul objects.
Hex-pair: Fixtype of pairs of hex digits.
Statements-to-fundefs: Filter function definitions out of a list of statements.
String-element-list-result: Fixtype of errors and lists of string elements.
Identifier-identifier-map-result: Fixtype of errors and omaps from identifiers to identifiers.
Swcase-result: Fixtype of errors and swcase clauses (for switch statements).
String-element-result: Fixtype of errors and string elements.
Statement-result: Fixtype of errors and statements.
Literal-result: Fixtype of errors and literals.
Identifier-set-result: Fixtype of errors and osets of identifiers.
Identifier-result: Fixtype of errors and identifiers.
Identifier-list-result: Fixtype of errors and lists of identifiers.
Hex-pair-list-result: Fixtype of errors and lists of hex pairs.
Fundef-result: Fixtype of errors and function definitions.
Funcall-result: Fixtype of errors and function calls.
Expression-result: Fixtype of errors and expressions.
Escape-result: Fixtype of errors and escapes.
Path-result: Fixtype of errors and paths.
Block-result: Fixtype of errors and blocks.
Objects: Fixtypes of Yul objects and related entities.
Statements/blocks/cases/fundefs: Fixtypes of statements, blocks, cases, and function definitions.
Identifier-list: Fixtype of lists of identifiers.
Identifier-set: Fixtype of osets of identifiers.
Identifier-identifier-map: Fixtype of omaps from identifiers to identifiers.
Identifier-identifier-alist: Fixtype of alists from identifiers to identifiers.
String-element-list: Fixtype of string elements.
Path-list: Fixtype of lists of paths.
Hex-pair-list: Fixtype of lists of hex pairs.
Hex-digit-list: Fixtype of lists of hex digits.
Literal-list: Fixtype of lists of literals.
Fundef-list: Fixtype of lists of function definitions.
Expressions/funcalls: Fixtypes of expressions and function calls.
Abstract-syntax-induction-schemas: Some induction schemas based on the Yul abstract syntax.