Syntax-abstraction
Mapping from concrete to abstract syntax, for Leo code.
The abstract syntax is an abstraction of the concrete syntax. Here we define the abstraction mapping from CSTs to ASTs.
For now our abstraction mapping has weak guards and many run-time checks.
We plan to turn things around eventually,
i.e. to have strong guards and ideally no run-time checks.
This may involve the development of
some more general support in our ABNF library for this.
Subtopics
- Abs-*-hexadecimal-digit-to-nat
- Abstract a *hexadecimal-digit to a natural number,
interpreting the digits in big endian.
- Abs-*-decimal-digit-to-nat
- Abstract a *decimal-digit to a natural number,
interpreting the digits in big endian.
- Chars+exprs
- Fixtype of pairs consisting of
a list of Leo characters and a list of expressions.
- Abs-transition-declaration
- Abstract a transition-declaration to a function declaration.
- Abs-not-double-quote-or-backslash-or-line-feed-or-carriage-return
- Abstract a not-double-quote-or-backslash-or-line-feed-or-carriage-return to a Leo character.
- Abs-named-type
- Abstract a named-type to a type.
- Chars+exprs-result
- Fixtype of errors and lists of pairs consisting of
a list of Leo characters and a list of expressions.
- Abs-*-lowercaseletter/decimaldigit
- Abstract a *( lowercase-letter / decimal-digit )
to a list of ACL2 characters.
- Abs-*-letter/decimaldigit/underscore
- Abstract a *( letter / digit / "_" )
to a list of ACL2 characters.
- Abs-*-comma-struct-component-declaration
- Abstract a *( "," struct-component-declaration ) to a list of compdecl.
- Abs-hexadecimal-digit-to-nat
- Abstract a hexadecimal-digit to a natural number.
- Abs-assignment-operator
- Abstract an assignment-operator to an assignment operator.
- Abs-struct-component-declarations
- Abstract a struct-component-declarations to a list of compdecl.
- Abs-lowercaseletter/decimaldigit
- Abstract a ( lowercase-letter / decimal-digit )
to an ACL2 character.
- Abs-letter/decimaldigit/underscore
- Abstract a ( letter / decimal-digit / "_" )
to an ACL2 character.
- Abs-increment-statement
- Abstract an increment-statement to a Leo increment statement.
- Abs-group-coordinate
- Abstract a group-coordinate to a group literal coordinate.
- Abs-function-parameter
- Abstract a function-parameter to a function parameter.
- Abs-function-declaration
- Abstract a function-declaration to a function declaration.
- Abs-decrement-statement
- Abstract an decrement-statement to a Leo decrement statement.
- Abs-unsigned-literal
- Abstract an unsigned-literal to an unsigned literal.
- Abs-record-declaration
- Abstract a record-declaration to a struct declaration.
- Abs-mapping-declaration
- Abstract a mapping-declaration to a mapping declaration.
- Abs-variable-declaration
- Abstract a variable-declaration to a variable declaration.
- Abs-signed-literal
- Abstract a signed-literal to a signed literal.
- Abs-constant-declaration
- Abstract a constant-declaration to a constant declaration.
- Abs-*-comma-function-parameter
- Abstract a *( "," function-parameter )
to a list of function parameters.
- Abs-unicode-character-escape
- Abstract a unicode-character-escape to a Leo character.
- Abs-struct-declaration
- Abstract a struct-declaration to a struct declaration.
- Abs-struct-component-declaration
- Abstract a struct-component-declaration to a compdecl.
- Abs-simple-character-escape
- Abstract a simple-character-escape to a Leo character.
- Abs-finalizer
- Abstract a [ finalizer ] to a Leo finalizer.
- Abs-decimal-digit-to-nat
- Abstract a decimal-digit to a natural number.
- Abs-comma-struct-component-declaration
- Abstract a ( "," struct-component-declaration ) to a compdecl.
- Abs-affine-group-literal
- Abstract an affine-group-literal to an affine group literal.
- Check-literal-is-string-literal
- Check if a literal is a string literal,
returning its list of characters if successful.
- Abs-*-annotation
- Abstract a *annotation to a list of annotations.
- Abs-variable-or-free-constant
- Abstract a variable-or-free-constant to an identifier.
- Abs-string-literal-element
- Abstract a string-literal-element to a Leo character.
- Abs-program-item
- Abstract a program-item to a topdecl.
- Abs-program-declaration
- Abstract a program-declaration to a programdecl.
- Abs-print-arguments
- Abstract a print-arguments to print arguments.
- Abs-octal-digit-to-nat
- Abstract an octal-digit to a natural number.
- Abs-finalize-statement
- Abstract a finalize-statement to a Leo finalize statement.
- Abs-declaration
- Abstract a declaration to a top-level declaration.
- Abs-decimal-digit-to-char
- Abstract a decimal-digit to an ACL2 character.
- Abs-console-statement
- Abstract a console-statement to a console statement.
- Abs-assignment-statement
- Abstract an assignment-statement to a statement.
- Abs-ascii-character-escape
- Abstract an ascii-character-escape to a Leo character.
- *binary-opcall-name-to-binop*
- Binary operator call to binop.
- Abs-?-function-parameters
- Abstract a [ function-parameters ]
to list of function parameters.
- Abs-*-string-literal-element
- Abstract a *string-literal-element to a list of Leo characters.
- Abs-*-import-declaration
- Abstract a *declaration to a list of import declarations.
- Abs-uppercase-letter
- Abstract an uppercase-letter to an ACL2 character.
- Abs-unsigned-type
- Abstract an unsigned-type to an unsigned type.
- Abs-signed-type
- Abstract a signed-type to an signed type.
- Abs-return-statement
- Abstract a return-statement to a statement.
- Abs-product-group-literal
- Abstract a product-group-literal to a product group literal.
- Abs-print-call
- Abstract a print-call to a console function call.
- Abs-named-primitive-type
- Abstract a named-primitive-type to a type.
- Abs-lowercase-letter
- Abstract a lowercase-letter to an ACL2 character.
- Abs-import-declaration
- Abstract a import-declaration to an importdecl.
- Abs-identifier
- Abstract an identifier to an identifier.
- Abs-function-parameters
- Abstract a function-parameters to a list of function parameters.
- Abs-comma-function-parameter
- Abstract a ( "," function-parameter )
to a function parameters.
- Abs-?-output-type
- Abstract an optional type (parsed from [ "->" type ] to a type-option.
- Abs-*-declaration
- Abstract a *declaration to a list of top-level declarations.
- Abs-unit-expression
- Abstract a unit-expression to a expression.
- Abs-string-literal
- Abstract a string-literal to a string literal.
- Abs-program-id
- Abstract a program-id to a programid.
- Abs-numeric-literal
- Abstract a numeric-literal to a numeric literal.
- Abs-letter
- Abstract a letter to an ACL2 character.
- Abs-integer-literal
- Abstract an integer-literal to an integer literal.
- Abs-double-quote-escape
- Abstract a double-quote-escape to a Leo character.
- Abs-carriage-return-escape
- Abstract a carriage-return-escape to a Leo character.
- Abs-boolean-literal
- Abstract a boolean-literal to a boolean literal.
- Abs-atomic-literal
- Abstract an atomic-literal to an atomic literal.
- Abs-assert-call
- Abstract an assert-call to a console function call.
- Abs-arithmetic-type
- Abstract an arithmetic-type to an arithmetic type.
- Abs-address-literal
- Abstract an address-literal to an address literal.
- Check-optional-equals-p
- Check if a tree is [ "=" ].
- Abs-?-finalizer
- Abstract a [ finalizer ] to a finalizer-option.
- Abs-*-program-item
- Abstract a *program-item to a list of topdecl.
- Abs-scalar-literal
- Abstract a scalar-literal to a scalar literal.
- Abs-null-character-escape
- Abstract a null-character-escape to a Leo character.
- Abs-locator
- Abstract a locator to a Leo locator.
- Abs-integer-type
- Abstract an integer-type to an integer type.
- Abs-horizontal-tab-escape
- Abstract a horizontal-tab-escape to a Leo character.
- Abs-field-literal
- Abstract a field-literal to a field literal.
- Abs-console-call
- Abstract a console-call to a console function call.
- Abs-backslash-escape
- Abstract a backslash-escape to a Leo character.
- Abs-annotation
- Abstract an annotation to an annotation.
- Check-?-comma
- Check if a tree is [ "," ].
- Abs-unit-type
- Abstract a unit-type to a type.
- Abs-string-type
- Abstract a string-type to the string type.
- Abs-scalar-type
- Abstract a scalar-type to the scalar type.
- Abs-literal
- Abstract a literal to a literal.
- Abs-line-feed-escape
- Abstract a line-feed-escape to a Leo character.
- Abs-double-quote
- Abstract a double-quote to a Leo character.
- Abs-boolean-type
- Abstract a boolean-type to the boolean type.
- Abs-address-type
- Abstract an address-type to the address type.
- Empty-optional-tree-p
- Abs-numeral
- Abstract a numeral to a natural number.
- Abs-group-type
- Abstract a group-type to the group type.
- Abs-file
- Abstract a file to a file.
- Abs-field-type
- Abstract a field-type to the field type.
- Unop-for-opcall-name
- Accessor function for *unary-opcall-name-to-unop*.
- Binop-for-opcall-name
- Accessor function for *binary-opcall-name-to-binop*.
- Abs-safe-nonascii
- Abstract a safe-nonascii to a Leo character.
- *unary-opcall-name-to-unop*
- Unary operator call to unop.
- Abs-?-expression-*-comma-expression-?-comma
- Abstract a [ expression *( "," expression ) [ "," ] ]
to a list of expressions.
- Abs-*-comma-struct-component-initializer
- Abstract a *( "," struct-component-initializer )
to a struct-init-list.
- Abs-1*-comma-expression
- Abstract 1*( "," expression ) to a list of expressions.
- Abs-*-statement
- Abstract a *statement to a list of statements.
- Abs-*-comma-type
- Abstract *( "," type ) to a list of types.
- Abs-*-comma-expression
- Abstract a *( "," expression ) to a list of expressions.
- Abs-unary-operator-call
- Abstract a unary-operator-call to an expression.
- Abs-unary-expression
- Abstract a unary-expression to an expression.
- Abs-tuple-expression
- Abstract a tuple-expression to an expression.
- Abs-tuple-component-expression
- Abstract a tuple-component-expression to an expression.
- Abs-struct-expression
- Abstract a struct-expression to an expression.
- Abs-struct-component-initializer
- Abstract a struct-component-initializer to a struct-init.
- Abs-struct-component-expression
- Abstract a struct-component-expression to an expression.
- Abs-shift-expression
- Abstract a shift-expression to an expression.
- Abs-primary-expression
- Abstract a primary-expression to an expression.
- Abs-postfix-expression
- Abstract a postfix-expression to an expression.
- Abs-ordering-expression
- Abstract an ordering-expression to an expression.
- Abs-multiplicative-expression
- Abstract a multiplicative-expression to an expression.
- Abs-function-arguments
- Abstract a function-arguments to a list of expressions.
- Abs-free-function-call
- Abstract a free-function-call to an expression.
- Abs-exponential-expression
- Abstract an exponential-expression to an expression.
- Abs-exclusive-disjunctive-expression
- Abstract a exclusive-disjunctive-expression to an expression.
- Abs-equality-expression
- Abstract an equality-expression to an expression.
- Abs-disjunctive-expression
- Abstract a disjunctive-expression to an expression.
- Abs-conjunctive-expression
- Abstract a conjunctive-expression to an expression.
- Abs-conditional-ternary-expression
- Abstract a conditional-ternary-expression to an expression.
- Abs-conditional-statement
- Abstract a conditional-statement to a statement.
- Abs-conditional-disjunctive-expression
- Abstract a conditional-disjunctive-expression to an expression.
- Abs-conditional-conjunctive-expression
- Abstract a conditional-conjunctive-expression to an expression.
- Abs-comma-struct-component-initializer
- Abstract a "," struct-component-initializer to a struct-init.
- Abs-comma-expression
- Abstract a ( "," expression ) to an expression.
- Abs-block
- Abstract a block to a list of statements.
- Abs-binary-operator-call
- Abstract a binary-operator-call to an expression.
- Abs-binary-expression
- Abstract a binary-expression to an expression.
- Abs-additive-expression
- Abstract an additive-expression to an expression.
- Abs-1*-comma-type
- Abstract 1*( "," type ) to a list of types.
- Abs-type
- Abstract a type to a type.
- Abs-tuple-type
- Abstract a tuple-type to a tuple type.
- Abs-statement
- Abstract a statement to a statement.
- Abs-operator-call
- Abstract an operator-call to an expression.
- Abs-loop-statement
- Abstract a loop-statement to a statement.
- Abs-expression
- Abstract an expression to an expression.
- Abs-comma-type
- Abstract a ( "," type ) to a type.
- Abs-branch
- Abstract a branch to a branch.
