Generate the code of a test method that is specific to the deep embedding approach.
(atj-gen-deep-test-code test-function test-inputs test-outputs comp-var java-class$) → (mv arg-block ares-block call-block jres-block comp-block)
This is used by atj-gen-test-method,
which generates a Java method
to run one of the tests specified in the
The first block returned by this function
builds the input values of the test,
and assigns them to an array variable.
The block also assigns the function's name to a variable.
The array and function name are both arguments to the
The second block returned by this function builds the output value of the test and assigns it to a variable. If the test has multiple values, they are grouped into a list: in the deep embedding, mv values are always treated as lists.
The third block returned by this function
calls the
The fourth block returned by this function is always empty. But we return it for uniformity with atj-gen-shallow-test-code.
The fifth block returned by this function compares the test output with the call output for equality, assigning the boolean result to a variable. The name of this variable is passed as argument to this function, since it is also used in atj-gen-test-method, thus preventing this and that function to go out of sync in regard to this shared variable name.
Function:
(defun atj-gen-deep-test-code (test-function test-inputs test-outputs comp-var java-class$) (declare (xargs :guard (and (symbolp test-function) (atj-test-value-listp test-inputs) (atj-test-value-listp test-outputs) (stringp comp-var) (stringp java-class$)))) (let ((__function__ 'atj-gen-deep-test-code)) (declare (ignorable __function__)) (b* (((mv arg-block arg-exprs & jvar-value-index) (atj-gen-test-values test-inputs "value" 1 t nil)) (arg-block (append arg-block (jblock-locvar (jtype-array *aij-type-value*) "functionArguments" (jexpr-newarray-init *aij-type-value* arg-exprs)) (jblock-locvar *aij-type-symbol* "functionName" (atj-gen-symbol test-function t nil)))) ((mv ares-block ares-exprs & &) (atj-gen-test-values test-outputs "value" jvar-value-index t nil)) (ares-expr (if (and (consp ares-exprs) (not (consp (cdr ares-exprs)))) (car ares-exprs) (jexpr-smethod *aij-type-value* "makeList" ares-exprs))) (ares-block (append ares-block (jblock-locvar *aij-type-value* "acl2Result" ares-expr))) (call-expr (jexpr-smethod (jtype-class java-class$) "call" (list (jexpr-name "functionName") (jexpr-name "functionArguments")))) (call-block (jblock-locvar *aij-type-value* "javaResult" call-expr)) (comp-expr (jexpr-method "acl2Result.equals" (list (jexpr-name "javaResult")))) (comp-block (jblock-locvar (jtype-boolean) comp-var comp-expr))) (mv arg-block ares-block call-block nil comp-block))))
Theorem:
(defthm jblockp-of-atj-gen-deep-test-code.arg-block (b* (((mv ?arg-block ?ares-block ?call-block ?jres-block ?comp-block) (atj-gen-deep-test-code test-function test-inputs test-outputs comp-var java-class$))) (jblockp arg-block)) :rule-classes :rewrite)
Theorem:
(defthm jblockp-of-atj-gen-deep-test-code.ares-block (b* (((mv ?arg-block ?ares-block ?call-block ?jres-block ?comp-block) (atj-gen-deep-test-code test-function test-inputs test-outputs comp-var java-class$))) (jblockp ares-block)) :rule-classes :rewrite)
Theorem:
(defthm jblockp-of-atj-gen-deep-test-code.call-block (b* (((mv ?arg-block ?ares-block ?call-block ?jres-block ?comp-block) (atj-gen-deep-test-code test-function test-inputs test-outputs comp-var java-class$))) (jblockp call-block)) :rule-classes :rewrite)
Theorem:
(defthm jblockp-of-atj-gen-deep-test-code.jres-block (b* (((mv ?arg-block ?ares-block ?call-block ?jres-block ?comp-block) (atj-gen-deep-test-code test-function test-inputs test-outputs comp-var java-class$))) (jblockp jres-block)) :rule-classes :rewrite)
Theorem:
(defthm jblockp-of-atj-gen-deep-test-code.comp-block (b* (((mv ?arg-block ?ares-block ?call-block ?jres-block ?comp-block) (atj-gen-deep-test-code test-function test-inputs test-outputs comp-var java-class$))) (jblockp comp-block)) :rule-classes :rewrite)