Atj-gen-shallow-mv-let
Generate a shallowly embedded ACL2 mv-let.
- Signature
(atj-gen-shallow-mv-let term jvar-tmp-base jvar-tmp-index
pkg-class-names fn-method-names
curr-pkg qpairs guards$ wrld)
→
(mv successp block expr new-jvar-tmp-index)
- Arguments
- term — Guard (pseudo-termp term).
- 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
- successp — Type (booleanp successp).
- block — Type (jblockp block).
- expr — Type (jexprp expr).
- new-jvar-tmp-index — Type (posp new-jvar-tmp-index), given (posp jvar-tmp-index).
This is the first thing we try on every term
(see atj-gen-shallow-term):
if the term is an mv-let,
we translate it to Java here and return a success value as first result,
so that the caller can propagate the results;
otherwise, the first result is nil,
the other results are irrelevant,
and the caller will handle the term
knowing that it is not an mv-let.
First, we check whether the term
is a marked and annotated mv-let;
see atj-check-marked-annotated-mv-let-call.
If it is, we proceed as follows.
We recursively translate to Java
the term assigned to the mv variable;
this must have multiple types.
Then we translate the let binding itself to Java,
obtaining a local variable declaration or assignment
(depending on the new/old marking of the mv variable)
for the multiple value.
Then we translate the let bindings for the components,
and finally the body term.