Syntax-abstraction
Mapping from concrete to abstract syntax, for PFCS.
The abstract syntax is an abstraction of the concrete syntax. Here we define the abstraction mapping from
the CSTs (concrete syntax trees) that are output by the ABNF parser, to the ASTs (abstract syntax trees) that are used
for downstream analysis and transformation.
In the source code there are some experimental functions using
the macros and theorems generated by deftreeops. As deftreeops develops, we plan to convert this code
to use the new functionality.
Subtopics
- Abs-*-decimal-digit-to-nat
- Abstract a *decimal-digit to a natural number,
interpreting the digits in big endian.
- Abs-?-expression-*-comma-expression
- Abstract a [ expression *( "," expression ) ]
to a list of expressions.
- Abs-?-constraint-*-comma-constraint
- Abstract a [ constraint *( "," constraint ) ]
to a list of constraints.
- Abs-*-letter/decimaldigit/underscore
- Abstract a *( letter / digit / "_" )
to a list of ACL2 characters.
- Abs-letter/decimaldigit/underscore
- Abstract a ( letter / decimal-digit / "_" )
to an ACL2 character.
- Abs-?-identifier-*-comma-identifier
- Abstract a [ identifier *( "," identifier ) ]
to a list of identifiers (strings).
- Abs-*-comma-constraint
- Abstract a *( "," constraint ) to a list of constraints.
- Abs-definition
- Abstract a definition CST to a definition AST.
- Abs-*-comma-identifier
- Abstract a *( "," identifier ) to a list of identifiers.
- Abs-*-comma-expression
- Abstract a *( "," expression ) to a list of expressions.
- Abs-decimal-digit-to-nat
- Abstract a digit to a natural number.
- Abs-*-definition
- Abstract a *definition to a list of definitions.
- Abs-*-constraint
- Abstract a *constraint to a list of constraints.
- Abs-relation-constraint
- Abstract a relation-constraint to a constraint.
- Abs-decimal-digit-to-char
- Abstract a digit to an ACL2 character.
- Abs-uppercase-letter
- Abstract an uppercase-letter to an ACL2 character.
- Abs-lowercase-letter
- Abstract a lowercase-letter to an ACL2 character.
- Abs-equality-constraint
- Abstract an equality-constraint to a constraint.
- Check-optional-minus-sign-p
- Check if a tree is [ "-" ].
- Abs-letter
- Abstract a letter to an ACL2 character.
- Abs-comma-expression
- Abstract a ( "," expression ) to an expression.
- Abs-comma-constraint
- Abstract a ( "," constraint ) to an constraint.
- Abs-integer
- Abstract an integer to an ACL2 int.
- Abs-constraint
- Abstract a constraint to a constraint.
- Abs-comma-identifier
- Abstract a ( "," identifier ) to a string.
- Check-?-comma
- Check if a tree is [ "," ].
- Abs-identifier
- Abstract an identifier to an identifier.
- Abs-system
- Abstract a system CST to a system AST.
- Abs-numeral
- Abstract a numeral to a natural number.
- Abs-primary-expression
- Abstract a primary-expression.
- Abs-multiplication-expression
- Abstract a multiplication-expression.
- Abs-addition-expression
- Abstract a addition-expression.
- Abs-expression
- Abstract an expression to an expression.
