Atj-pre-translation-no-aij-types-analysis
Pre-translation step performed by ATJ:
analysis for the :no-aij-types option.
If the :no-aij-types input is t,
the ACL2 code translated to Java must satisfy a number of requirements,
described in the user documentation.
These requirements must be checked after
the pre-translation steps that may remove code,
because the requirements only need to hold for
ACL2 code that is actually translated to Java.
Performing these checks earlier would reject ACL2 code
that would be translated to Java code
that does not use any AIJ types.
We perform these checks after
atj-pre-translation-multiple-values,
so that we can more easily identify translated calls of mv.
We perform these checks before
atj-pre-translation-type-annotation,
so that we can perform the checks
without worrying about the type conversion functions and type annotations,
which would make the checks more complicated to perform.
Subtopics
- Atj-check-no-aij-term
- Check that a term does not use any AIJ types.
- Atj-check-no-aij-type
- Check that an ATJ type is not mapped to an AIJ type.
- Atj-check-no-aij-types+body
- Check that a function to translate to Java
does not use any AIJ types.
- Atj-check-no-aij-type-list
- Lift atj-check-no-aij-type to lists.