Atj-gen-deep-lambda
Generate Java code to build
a deeply embedded ACL2 lambda expression.
- Signature
(atj-gen-deep-lambda formals body 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
- formals — Guard (symbol-listp formals).
- body — Guard (pseudo-termp body).
- 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
puts the formals into an array,
builds the body,
builds the lambda expression,
puts it to a local variable,
and returns the local variable.
