		Search-engine friendly clone of the ACL2 documentation.

Atj-common-code-generation

Atj-gen-test-value

Generate the Java code for a test value.

Signature
(atj-gen-test-value tvalue jvar-value-base jvar-value-index deep$ guards$) → (mv block expr type new-jvar-value-index)
Arguments: tvalue — Guard (atj-test-valuep tvalue).; jvar-value-base — Guard (stringp jvar-value-base).; jvar-value-index — Guard (posp jvar-value-index).; deep$ — Guard (booleanp deep$).; guards$ — Guard (booleanp guards$).
Returns: block — Type (jblockp block).; expr — Type (jexprp expr).; type — Type (atj-typep type).; new-jvar-value-index — Type (posp new-jvar-value-index), given (posp jvar-value-index).

We use atj-gen-value for a test values; this is why this function has the jvar-value-... arguments and returns the new-jvar-value-index result.

For j test values, we use atj-gen-jboolean and similar functions.

In both cases, we also return the ATJ type of the expression. In the shallow embedding, this will determine the Java type of the local variable that stores the value.

Definitions and Theorems

Function: atj-gen-test-value

(defun atj-gen-test-value (tvalue jvar-value-base
                                  jvar-value-index deep$ guards$)
 (declare (xargs :guard (and (atj-test-valuep tvalue)
                             (stringp jvar-value-base)
                             (posp jvar-value-index)
                             (booleanp deep$)
                             (booleanp guards$))))
 (let ((__function__ 'atj-gen-test-value))
  (declare (ignorable __function__))
  (atj-test-value-case
   tvalue :acl2
   (b* (((mv block expr jvar-value-index)
         (atj-gen-value tvalue.get jvar-value-base
                        jvar-value-index deep$ guards$)))
     (mv block
         expr (atj-type-of-value tvalue.get)
         jvar-value-index))
   :jboolean (mv nil
                 (atj-gen-jboolean (boolean-value->bool tvalue.get))
                 (atj-type-jprim (primitive-type-boolean))
                 jvar-value-index)
   :jchar (mv nil
              (atj-gen-jchar (char-value->nat tvalue.get))
              (atj-type-jprim (primitive-type-char))
              jvar-value-index)
   :jbyte (mv nil
              (atj-gen-jbyte (byte-value->int tvalue.get))
              (atj-type-jprim (primitive-type-byte))
              jvar-value-index)
   :jshort (mv nil
               (atj-gen-jshort (short-value->int tvalue.get))
               (atj-type-jprim (primitive-type-short))
               jvar-value-index)
   :jint (mv nil
             (atj-gen-jint (int-value->int tvalue.get))
             (atj-type-jprim (primitive-type-int))
             jvar-value-index)
   :jlong (mv nil
              (atj-gen-jlong (long-value->int tvalue.get))
              (atj-type-jprim (primitive-type-long))
              jvar-value-index)
   :jboolean[] (mv nil (atj-gen-jboolean-array tvalue.get)
                   (atj-type-jprimarr (primitive-type-boolean))
                   jvar-value-index)
   :jchar[] (mv nil (atj-gen-jchar-array tvalue.get)
                (atj-type-jprimarr (primitive-type-char))
                jvar-value-index)
   :jbyte[] (mv nil (atj-gen-jbyte-array tvalue.get)
                (atj-type-jprimarr (primitive-type-byte))
                jvar-value-index)
   :jshort[] (mv nil (atj-gen-jshort-array tvalue.get)
                 (atj-type-jprimarr (primitive-type-short))
                 jvar-value-index)
   :jint[] (mv nil (atj-gen-jint-array tvalue.get)
               (atj-type-jprimarr (primitive-type-int))
               jvar-value-index)
   :jlong[] (mv nil (atj-gen-jlong-array tvalue.get)
                (atj-type-jprimarr (primitive-type-long))
                jvar-value-index))))

Theorem: jblockp-of-atj-gen-test-value.block

(defthm jblockp-of-atj-gen-test-value.block
  (b* (((mv common-lisp::?block
            ?expr common-lisp::?type
            ?new-jvar-value-index)
        (atj-gen-test-value tvalue jvar-value-base
                            jvar-value-index deep$ guards$)))
    (jblockp block))
  :rule-classes :rewrite)

Theorem: jexprp-of-atj-gen-test-value.expr

(defthm jexprp-of-atj-gen-test-value.expr
  (b* (((mv common-lisp::?block
            ?expr common-lisp::?type
            ?new-jvar-value-index)
        (atj-gen-test-value tvalue jvar-value-base
                            jvar-value-index deep$ guards$)))
    (jexprp expr))
  :rule-classes :rewrite)

Theorem: atj-typep-of-atj-gen-test-value.type

(defthm atj-typep-of-atj-gen-test-value.type
  (b* (((mv common-lisp::?block
            ?expr common-lisp::?type
            ?new-jvar-value-index)
        (atj-gen-test-value tvalue jvar-value-base
                            jvar-value-index deep$ guards$)))
    (atj-typep type))
  :rule-classes :rewrite)

Theorem: posp-of-atj-gen-test-value.new-jvar-value-index

(defthm posp-of-atj-gen-test-value.new-jvar-value-index
  (implies
       (posp jvar-value-index)
       (b* (((mv common-lisp::?block
                 ?expr common-lisp::?type
                 ?new-jvar-value-index)
             (atj-gen-test-value tvalue jvar-value-base
                                 jvar-value-index deep$ guards$)))
         (posp new-jvar-value-index)))
  :rule-classes :rewrite)