Generate shallowly embedded ACL2 let bindings.
(atj-gen-shallow-let-bindings vars blocks exprs) → block
In the shallow embedding approach, ACL2 lambda expressions (i.e. lets) are handled by assigning the Java expressions generated from the actual parameters passed to the lambda expression to Java local variables corresponding to the formal parameters. This function generates these bindings, given the ACL2 variables that are the formal arguments and the Java expressions to assign to them. Each binding is preceded by the block (if any) generated for the corresponding actual argument of the lambda expression.
Prior to calling this function, the variables of all the lambda expressions have been marked as either `new' or `old' via atj-mark-term. We extract this mark and use it to generate either a variable declaration with initializer (for `new') or an assignment to an existing variable (for `old').
Prior to calling this function, the variables of all the lambda expressions have been annotated via atj-type-annotate-term. Thus, each ACL2 variable name carries its own non-empty list of types, which we use to determine the Java type of the Java variable.
Prior to calling this function, the variables of all the lambda expressions have been renamed via atj-rename-term. Thus, we directly turn each ACL2 variable into a Java variable name (after removing the type annotations).
Function:
(defun atj-gen-shallow-let-bindings (vars blocks exprs) (declare (xargs :guard (and (symbol-listp vars) (jblock-listp blocks) (jexpr-listp exprs)))) (declare (xargs :guard (and (int= (len blocks) (len vars)) (int= (len exprs) (len vars))))) (let ((__function__ 'atj-gen-shallow-let-bindings)) (declare (ignorable __function__)) (b* (((when (endp vars)) nil) (var (car vars)) (expr (car exprs)) ((mv var new?) (atj-unmark-var var)) ((mv var types) (atj-type-unannotate-var var)) (jvar (symbol-name var)) (var-block (if new? (jblock-locvar (atj-gen-shallow-jtype types) jvar expr) (jblock-asg (jexpr-name jvar) expr))) (first-block (append (car blocks) var-block)) (rest-block (atj-gen-shallow-let-bindings (cdr vars) (cdr blocks) (cdr exprs)))) (append first-block rest-block))))
Theorem:
(defthm jblockp-of-atj-gen-shallow-let-bindings (implies (jblock-listp blocks) (b* ((block (atj-gen-shallow-let-bindings vars blocks exprs))) (jblockp block))) :rule-classes :rewrite)