Atj-gen-deep-fnapp
Generate Java code to build
a deeply embedded ACL2 function call.
- Signature
(atj-gen-deep-fnapp fn args jvar-value-base
jvar-value-index jvar-term-base
jvar-term-index jvar-lambda-base
jvar-lambda-index guards$)
→
(mv block expr
new-jvar-value-index new-jvar-term-index
new-jvar-lambda-index)
- Arguments
- fn — Guard (pseudo-termfnp fn).
- args — Guard (pseudo-term-listp args).
- jvar-value-base — Guard (stringp jvar-value-base).
- jvar-value-index — Guard (posp jvar-value-index).
- jvar-term-base — Guard (stringp jvar-term-base).
- jvar-term-index — Guard (posp jvar-term-index).
- jvar-lambda-base — Guard (stringp jvar-lambda-base).
- jvar-lambda-index — Guard (posp jvar-lambda-index).
- guards$ — Guard (booleanp guards$).
- Returns
- block — Type (jblockp block).
- expr — Type (jexprp expr).
- new-jvar-value-index — Type (posp new-jvar-value-index), given (posp jvar-value-index).
- new-jvar-term-index — Type (posp new-jvar-term-index), given (posp jvar-term-index).
- new-jvar-lambda-index — Type (posp new-jvar-lambda-index), given (posp jvar-lambda-index).
The generated code
builds the named function or lambda expression,
builds the argument terms,
puts them into an array,
builds the call,
puts it to a local variable,
and returns the local variable.
Terms of the form (if a a b) are treated as (or a b),
i.e. the generated code builds a term of the form (or a b).
In ACL2, or is a macro:
an untranslated term (or a b) is translated to (if a a b),
which, if executed as such by AIJ, would evaluate a twice.
(ACL2 relies on the underlying Lisp platform to optimize this situation.)
AIJ provides support for a ``pseudo-function'' or
that evaluates its arguments non-strictly;
see the documentation of AIJ for details.
Thus, ATJ recognizes (translated) terms of the form (if a a b),
which are likely derived from (or a b),
and represents them in AIJ via the or pseudo-function.
