Generate the code of a test method that is specific to the shallow embedding approach.
(atj-gen-shallow-test-code test-function test-inputs test-outputs comp-var guards$ java-class$ pkg-class-names fn-method-names wrld) → (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 separate variables.
We store them into variables,
instead of passing their expressions
directly to the method being tested,
to accurately measure just the time of each call
(see atj-gen-test-method for details),
without the time needed to compute the expressions.
The variables' names are
The second block returned by this function
builds the output values of the test and assigns them to variables.
If there is just one output value,
it is assigned to a variable
The third block returned by this function
calls the Java method that represents the ACL2 function being tested
on the local variables that store the arguments.
Since this code is in a class that is different from
any of the generated Java classes that correspond to ACL2 packages,
the Java method to call must be always preceded by the class name:
thus, we use
The fourth block is empty
if the ACL2 function corresponding to the method being tested
is single-valued.
If instead it is multi-valued,
this block assigns the field of
The fifth block returned by this function compares the test outputs with the call outputs 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-shallow-test-code-asgs (arg-exprs arg-types in-types var-base index guards$) (declare (xargs :guard (and (jexpr-listp arg-exprs) (atj-type-listp arg-types) (atj-type-listp in-types) (stringp var-base) (natp index) (booleanp guards$)))) (declare (xargs :guard (and (= (len arg-exprs) (len arg-types)) (= (len arg-types) (len in-types))))) (let ((__function__ 'atj-gen-shallow-test-code-asgs)) (declare (ignorable __function__)) (cond ((endp arg-exprs) (mv nil nil)) (t (b* ((first-var (str::cat var-base (nat-to-dec-string index))) (first-arg-expr (car arg-exprs)) (first-arg-type (car arg-types)) (first-in-type (car in-types)) (first-expr (atj-adapt-expr-to-type first-arg-expr first-arg-type first-in-type guards$)) (first-jtype (atj-type-to-jitype first-in-type)) (first-block (jblock-locvar first-jtype first-var first-expr)) ((mv rest-block rest-vars) (atj-gen-shallow-test-code-asgs (cdr arg-exprs) (cdr arg-types) (cdr in-types) var-base (1+ index) guards$))) (mv (append first-block rest-block) (cons first-var rest-vars)))))))
Theorem:
(defthm jblockp-of-atj-gen-shallow-test-code-asgs.block (b* (((mv common-lisp::?block ?vars) (atj-gen-shallow-test-code-asgs arg-exprs arg-types in-types var-base index guards$))) (jblockp block)) :rule-classes :rewrite)
Theorem:
(defthm string-listp-of-atj-gen-shallow-test-code-asgs.vars (b* (((mv common-lisp::?block ?vars) (atj-gen-shallow-test-code-asgs arg-exprs arg-types in-types var-base index guards$))) (string-listp vars)) :rule-classes :rewrite)
Theorem:
(defthm len-of-atj-gen-shallow-test-code-asgs.vars (b* (((mv common-lisp::?block ?vars) (atj-gen-shallow-test-code-asgs arg-exprs arg-types in-types var-base index guards$))) (equal (len vars) (len arg-exprs))))
Function:
(defun atj-gen-shallow-test-code-mv-asgs (expr types var-base index) (declare (xargs :guard (and (jexprp expr) (atj-type-listp types) (stringp var-base) (natp index)))) (let ((__function__ 'atj-gen-shallow-test-code-mv-asgs)) (declare (ignorable __function__)) (cond ((endp types) (mv nil nil)) (t (b* ((first-var (str::cat var-base (nat-to-dec-string index))) (first-type (car types)) (first-jtype (atj-type-to-jitype first-type)) (first-expr (jexpr-get-field expr (atj-gen-shallow-mv-field-name index))) (first-block (jblock-locvar first-jtype first-var first-expr)) ((mv rest-block rest-vars) (atj-gen-shallow-test-code-mv-asgs expr (cdr types) var-base (1+ index)))) (mv (append first-block rest-block) (cons first-var rest-vars)))))))
Theorem:
(defthm jblockp-of-atj-gen-shallow-test-code-mv-asgs.block (b* (((mv common-lisp::?block ?vars) (atj-gen-shallow-test-code-mv-asgs expr types var-base index))) (jblockp block)) :rule-classes :rewrite)
Theorem:
(defthm string-listp-of-atj-gen-shallow-test-code-mv-asgs.vars (b* (((mv common-lisp::?block ?vars) (atj-gen-shallow-test-code-mv-asgs expr types var-base index))) (string-listp vars)) :rule-classes :rewrite)
Theorem:
(defthm len-of-atj-gen-shallow-test-code-mv-asgs.vars (b* (((mv common-lisp::?block ?vars) (atj-gen-shallow-test-code-mv-asgs expr types var-base index))) (equal (len vars) (len types))))
Function:
(defun atj-gen-shallow-test-code-comps (ares-vars jres-vars types comp-var) (declare (xargs :guard (and (string-listp ares-vars) (string-listp jres-vars) (atj-type-listp types) (stringp comp-var)))) (declare (xargs :guard (and (= (len jres-vars) (len ares-vars)) (= (len types) (len ares-vars))))) (let ((__function__ 'atj-gen-shallow-test-code-comps)) (declare (ignorable __function__)) (cond ((endp ares-vars) nil) (t (b* ((ares-var (car ares-vars)) (jres-var (car jres-vars)) (type (car types)) (comp-expr (atj-type-case type :jprim (jexpr-binary (jbinop-eq) (jexpr-name ares-var) (jexpr-name jres-var)) :jprimarr (jexpr-smethod (jtype-class "Arrays") "equals" (list (jexpr-name ares-var) (jexpr-name jres-var))) :acl2 (b* ((jtype (atj-type-to-jitype type))) (if (jtype-case jtype :prim) (jexpr-binary (jbinop-eq) (jexpr-name ares-var) (jexpr-name jres-var)) (jexpr-method (str::cat ares-var ".equals") (list (jexpr-name jres-var))))))) (comp-block (jblock-expr (jexpr-binary (jbinop-asg-and) (jexpr-name comp-var) comp-expr))) (rest-block (atj-gen-shallow-test-code-comps (cdr ares-vars) (cdr jres-vars) (cdr types) comp-var))) (append comp-block rest-block))))))
Theorem:
(defthm jblockp-of-atj-gen-shallow-test-code-comps (b* ((block (atj-gen-shallow-test-code-comps ares-vars jres-vars types comp-var))) (jblockp block)) :rule-classes :rewrite)
Function:
(defun atj-gen-shallow-test-code (test-function test-inputs test-outputs comp-var guards$ java-class$ pkg-class-names fn-method-names wrld) (declare (xargs :guard (and (symbolp test-function) (atj-test-value-listp test-inputs) (atj-test-value-listp test-outputs) (stringp comp-var) (booleanp guards$) (stringp java-class$) (string-string-alistp pkg-class-names) (symbol-string-alistp fn-method-names) (plist-worldp wrld)))) (declare (xargs :guard (consp test-outputs))) (let ((__function__ 'atj-gen-shallow-test-code)) (declare (ignorable __function__)) (b* (((mv arg-val-block arg-exprs arg-types jvar-value-index) (atj-gen-test-values test-inputs "value" 1 nil guards$)) (fn-info (atj-get-function-type-info test-function guards$ wrld)) (main-fn-type (atj-function-type-info->main fn-info)) (other-fn-types (atj-function-type-info->others fn-info)) (all-fn-types (cons main-fn-type other-fn-types)) (fn-type? (atj-function-type-of-min-input-types arg-types all-fn-types)) ((unless fn-type?) (raise "Internal error: ~ the argument types ~x0 ~ do not have a corresponding Java overloaded method." arg-types) (mv nil nil nil nil nil)) (in-types (atj-function-type->inputs fn-type?)) (out-types (atj-function-type->outputs fn-type?)) ((unless (= (len arg-types) (len in-types))) (raise "Internal error: ~ the argument types ~x0 ~ differ in number from the function input types ~x1." arg-types in-types) (mv nil nil nil nil nil)) ((mv arg-asg-block arg-vars) (atj-gen-shallow-test-code-asgs arg-exprs arg-types in-types "argument" 1 guards$)) (arg-block (append arg-val-block arg-asg-block)) (singletonp (= (len test-outputs) 1)) ((mv ares-val-block ares-exprs ares-types &) (atj-gen-test-values test-outputs "value" jvar-value-index nil guards$)) ((unless (= (len out-types) (len test-outputs))) (raise "Internal error: ~ the number of output types ~x0 of function ~x1 ~ does not match the number of test outputs ~x2." out-types test-function test-outputs) (mv nil nil nil nil nil)) ((mv ares-asg-block ares-vars) (if singletonp (mv (jblock-locvar (atj-type-to-jitype (car out-types)) "acl2Result" (atj-adapt-expr-to-type (car ares-exprs) (car ares-types) (car out-types) guards$)) (list "acl2Result")) (atj-gen-shallow-test-code-asgs ares-exprs ares-types out-types "acl2Result" 0 guards$))) (ares-block (append ares-val-block ares-asg-block)) (call-expr (jexpr-smethod (jtype-class java-class$) (atj-gen-shallow-fnname test-function pkg-class-names fn-method-names "KEYWORD") (jexpr-name-list arg-vars))) (call-jtype (atj-gen-shallow-jtype out-types)) (call-jtype (if (jtype-case call-jtype :class) (b* ((name (jtype-class->name call-jtype))) (if (and (>= (length name) 3) (eql (char name 0) #\M) (eql (char name 1) #\V) (eql (char name 2) #\_)) (jtype-class (str::cat java-class$ "." name)) call-jtype)) call-jtype)) (call-block (jblock-locvar call-jtype "javaResult" call-expr)) ((mv jres-block jres-vars) (if singletonp (mv nil (list "javaResult")) (atj-gen-shallow-test-code-mv-asgs (jexpr-name "javaResult") out-types "javaResult" 0))) (comp-block (append (jblock-locvar (jtype-boolean) comp-var (jexpr-literal-true)) (atj-gen-shallow-test-code-comps ares-vars jres-vars out-types comp-var)))) (mv arg-block ares-block call-block jres-block comp-block))))
Theorem:
(defthm jblockp-of-atj-gen-shallow-test-code.arg-block (b* (((mv ?arg-block ?ares-block ?call-block ?jres-block ?comp-block) (atj-gen-shallow-test-code test-function test-inputs test-outputs comp-var guards$ java-class$ pkg-class-names fn-method-names wrld))) (jblockp arg-block)) :rule-classes :rewrite)
Theorem:
(defthm jblockp-of-atj-gen-shallow-test-code.ares-block (b* (((mv ?arg-block ?ares-block ?call-block ?jres-block ?comp-block) (atj-gen-shallow-test-code test-function test-inputs test-outputs comp-var guards$ java-class$ pkg-class-names fn-method-names wrld))) (jblockp ares-block)) :rule-classes :rewrite)
Theorem:
(defthm jblockp-of-atj-gen-shallow-test-code.call-block (b* (((mv ?arg-block ?ares-block ?call-block ?jres-block ?comp-block) (atj-gen-shallow-test-code test-function test-inputs test-outputs comp-var guards$ java-class$ pkg-class-names fn-method-names wrld))) (jblockp call-block)) :rule-classes :rewrite)
Theorem:
(defthm jblockp-of-atj-gen-shallow-test-code.jres-block (b* (((mv ?arg-block ?ares-block ?call-block ?jres-block ?comp-block) (atj-gen-shallow-test-code test-function test-inputs test-outputs comp-var guards$ java-class$ pkg-class-names fn-method-names wrld))) (jblockp jres-block)) :rule-classes :rewrite)
Theorem:
(defthm jblockp-of-atj-gen-shallow-test-code.comp-block (b* (((mv ?arg-block ?ares-block ?call-block ?jres-block ?comp-block) (atj-gen-shallow-test-code test-function test-inputs test-outputs comp-var guards$ java-class$ pkg-class-names fn-method-names wrld))) (jblockp comp-block)) :rule-classes :rewrite)