Atj-pre-translation-disjunctions
Pre-translation step performed by ATJ:
replacement of (if a a b) calls with or calls.
This is done in the shallow embedding.
ACL2 turns untranslated calls of the form (or a b)
into translated calls of the form (if a a b).
This pre-translation step performs the inverse transformation,
so that the ACL2-to-Java translation step can
more readily recognize this kind of calls
and treat them specially.
Note that this pre-translation step
turns (if a a b) into (or a b)
even when the original untranslated term was (if a a b).
But this is harmelss, as the two untranslated terms are equivalent,
at least functionally (assuming that a has no side effects).
Subtopics
- Atj-restore-or-calls-in-term
- Restore or calls in a translated term.
