Term-checkers-common
Checkers of ACL2 terms that represent C constructs,
common to ATC and defobject.
The shallow embedding of C in ACL2 defines
representations of C constructs in ACL2.
These are used by atc and defobject,
which check ACL2 terms to see if they represent C constructs,
returning appropriate information if that is the case.
Here we collect some of this checking code on terms,
which is common to atc and defobject.
We plan to organize all of this code more systematically at some point.
Subtopics
- Atc-check-binop
- Check if a term may represent a strict pure binary expression.
- Atc-check-iconst
- Check if a term represents an integer constant.
- Atc-check-unop
- Check if a term may represent a unary expression.
- Atc-check-conv
- Check if a term may represent a conversion.
- Atc-check-symbol-5part
- Check if a symbol consists of five parts separated by dash.
- Atc-check-symbol-4part
- Check if a symbol consists of four parts separated by dash.
- Atc-check-symbol-3part
- Check if a symbol consists of three parts separated by dash.
- Atc-check-symbol-2part
- Check if a symbol consists of two parts separated by dash.
