|
|
|---|
|
|
|
|---|
Generate a shallowly embedded ACL2 term.
(atj-gen-shallow-term term jvar-tmp-base jvar-tmp-index
pkg-class-names fn-method-names
curr-pkg qpairs guards$ wrld)
→
(mv block expr new-jvar-tmp-index)Prior to calling this function, the term has been type-annotated via atj-type-annotate-term. Thus, we first unwrap it and decompose its wrapper.
Prior to calling this function, the ACL2 variables have been renamed, via atj-rename-term, so that they have the right names as Java variables. Thus, if the ACL2 term is a variable, we remove its type annotation and generate a Java variable with the same name. Then we wrap it with a Java conversion, if needed.
First we try to process the term as an mv-let, via a separate code generation function. If this succeeds, we just return. Otherwise, we process the term by cases (variable, quoted constants, etc.), knowing that it is not an mv-let.
If the ACL2 term is a quoted constant, we represent it as its value. We wrap the resulting expression with a Java conversion, if needed.
If the ACL2 term is a named function call, we first generate code to compute the actual arguments and then we use a separate code generation function to handle the different kinds of named function calls. If instead the ACL2 term is a call of a lambda expression, we first generate code to compute the actual arguments, and then we use a separate code generation function for the lambda expression.