		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-code-generation

Atj-gen-shallow-test-code

Generate the code of a test method that is specific to the shallow embedding approach.

Signature
(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)
Arguments: test-function — Guard (symbolp test-function).; test-inputs — Guard (atj-test-value-listp test-inputs).; test-outputs — Guard (atj-test-value-listp test-outputs).; comp-var — Guard (stringp comp-var).; guards$ — Guard (booleanp guards$).; java-class$ — Guard (stringp java-class$).; pkg-class-names — Guard (string-string-alistp pkg-class-names).; fn-method-names — Guard (symbol-string-alistp fn-method-names).; wrld — Guard (plist-worldp wrld).
Returns: arg-block — Type (jblockp arg-block).; ares-block — Type (jblockp ares-block).; call-block — Type (jblockp call-block).; jres-block — Type (jblockp jres-block).; comp-block — Type (jblockp comp-block).

This is used by atj-gen-test-method, which generates a Java method to run one of the tests specified in the :tests input to ATJ. Most of that method's code is the same for deep and shallow embedding. The only varying parts are the ones returned by this function, and by atj-gen-deep-test-code for the deep embedding.

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 argument1, argument2, etc.

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 acl2Result. Otherwise, they are assigned to acl2Result0, acl2Result1, etc., consistently with the zero-based index passed to mv-nth.

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 "KEYWORD" as current package name, which never contains any functions. The method's result is stored into a variable javaResult. The type of the variable is determined from the output types of the function that correspond to the arguments, but if it is an mv class we need to qualify its name with the name of the main Java class generated (the code to do this is not very elegant and should be improved).

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 javaResult, which is an instance of an mv class, to javaResult0, javaResult1, etc.

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.

Definitions and Theorems

Function: atj-gen-shallow-test-code-asgs

(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: jblockp-of-atj-gen-shallow-test-code-asgs.block

(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: string-listp-of-atj-gen-shallow-test-code-asgs.vars

(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: len-of-atj-gen-shallow-test-code-asgs.vars

(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: atj-gen-shallow-test-code-mv-asgs

(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: jblockp-of-atj-gen-shallow-test-code-mv-asgs.block

(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: string-listp-of-atj-gen-shallow-test-code-mv-asgs.vars

(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: len-of-atj-gen-shallow-test-code-mv-asgs.vars

(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: atj-gen-shallow-test-code-comps

(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: jblockp-of-atj-gen-shallow-test-code-comps

(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: atj-gen-shallow-test-code

(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: jblockp-of-atj-gen-shallow-test-code.arg-block

(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: jblockp-of-atj-gen-shallow-test-code.ares-block

(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: jblockp-of-atj-gen-shallow-test-code.call-block

(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: jblockp-of-atj-gen-shallow-test-code.jres-block

(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: jblockp-of-atj-gen-shallow-test-code.comp-block

(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)