Atc-term-recognizers
Recognizers of ACL2 terms for ATC.
The user documentation of ATC
defines various kinds of ACL2 terms
that represent various C constructs.
ATC checks these various kinds of terms
as part of translating them to C.
Here we provide utilities to recognize these terms.
While these utilities are not needed, and are not part of,
ATC's C code generation code,
they may be useful for external tools,
such as APT transformations that work in synergy with ATC.
For now we provide shallow recognizers,
which do not thoroughly check the terms and their subterms,
but that suffice to distinguish the various kinds of terms.
We only provide these recognizers for some kinds of terms for now.
Subtopics
- Atc-stmt-noncval-termp
- Recognize statement terms that are not
expression terms returning C values.
- Atc-pure-c-valued-termp
- Recognize pure expression terms returning C values terms.
- Atc-c-valued-termp
- Recognize expression terms returning C values.
- Atc-boolean-termp
- Recognize expression terms returning booleans.
- *atc-op-type1-type2-fns*
- List of the <op>-<type1>-<type2> functions
described in the user documentation.
- *atc-type1-from-type2-fns*
- List of the <type1>-from-<type2> functions
described in the user documentation.
- *atc-type-base-const-fns*
- List of the <type>-<base>-const functions
described in the user documentation.
- *atc-op-type-fns*
- List of the <op>-<type> functions
described in the user documentation.
- *atc-boolean-from-type-fns*
- List of the boolean-from-<type> functions
described in the user documentation.
