Atj-gen-shallow-lambda
Generate a shallowly embedded ACL2 lambda expression,
applied to given Java expressions as arguments.
- Signature
(atj-gen-shallow-lambda formals
body arg-blocks arg-exprs src-types
dst-types jvar-tmp-base jvar-tmp-index
pkg-class-names fn-method-names
curr-pkg qpairs guards$ wrld)
→
(mv block expr new-jvar-tmp-index)
- Arguments
- formals — Guard (symbol-listp formals).
- body — Guard (pseudo-termp body).
- arg-blocks — Guard (jblock-listp arg-blocks).
- arg-exprs — Guard (jexpr-listp arg-exprs).
- src-types — Guard (atj-type-listp src-types).
- dst-types — Guard (atj-type-listp dst-types).
- jvar-tmp-base — Guard (stringp jvar-tmp-base).
- jvar-tmp-index — Guard (posp jvar-tmp-index).
- pkg-class-names — Guard (string-string-alistp pkg-class-names).
- fn-method-names — Guard (symbol-string-alistp fn-method-names).
- curr-pkg — Guard (stringp curr-pkg).
- qpairs — Guard (cons-pos-alistp qpairs).
- guards$ — Guard (booleanp guards$).
- wrld — Guard (plist-worldp wrld).
- Returns
- block — Type (jblockp block), given (jblock-listp arg-blocks).
- expr — Type (jexprp expr).
- new-jvar-tmp-index — Type (posp new-jvar-tmp-index), given (posp jvar-tmp-index).
We generate let bindings for the formal parameters.
Then we generate Java code for the body of the lambda expression.