		Search-engine friendly clone of the ACL2 documentation.

Atj-common-code-generation

Atj-gen-jlocvar-indexed

Generate a Java declaration for an indexed local variable.

Signature
(atj-gen-jlocvar-indexed var-type var-base var-index var-init?) → (mv locvar-block var-name new-var-index)
Arguments: var-type — Type of the local variable.
Guard (jtypep var-type).; var-base — Base name of the local variable.
Guard (stringp var-base).; var-index — Index of the local variable.
Guard (natp var-index).; var-init? — Initializer of the local variable.
Guard (maybe-jexprp var-init?).
Returns: locvar-block — Type (jblockp locvar-block).; var-name — The name of the local variable.
Type (stringp var-name).; new-var-index — The updated variable index.
Type (natp new-var-index), given (natp var-index).

The name of the local variable to use is obtained by adding the next variable index after the base name. The index is incremented and returned because it has been used, and the next variable with the same name must use the next index.

For convenience of the callers of this function, the local variable declaration is returned in a singleton block.

Definitions and Theorems

Function: atj-gen-jlocvar-indexed

(defun atj-gen-jlocvar-indexed
       (var-type var-base var-index var-init?)
 (declare (xargs :guard (and (jtypep var-type)
                             (stringp var-base)
                             (natp var-index)
                             (maybe-jexprp var-init?))))
 (let ((__function__ 'atj-gen-jlocvar-indexed))
   (declare (ignorable __function__))
   (b* ((var-name (str::cat var-base (nat-to-dec-string var-index)))
        (var-index (1+ var-index))
        (locvar-block (jblock-locvar var-type var-name var-init?)))
     (mv locvar-block var-name var-index))))

Theorem: jblockp-of-atj-gen-jlocvar-indexed.locvar-block

(defthm jblockp-of-atj-gen-jlocvar-indexed.locvar-block
  (b* (((mv ?locvar-block ?var-name ?new-var-index)
        (atj-gen-jlocvar-indexed
             var-type var-base var-index var-init?)))
    (jblockp locvar-block))
  :rule-classes :rewrite)

Theorem: stringp-of-atj-gen-jlocvar-indexed.var-name

(defthm stringp-of-atj-gen-jlocvar-indexed.var-name
  (b* (((mv ?locvar-block ?var-name ?new-var-index)
        (atj-gen-jlocvar-indexed
             var-type var-base var-index var-init?)))
    (stringp var-name))
  :rule-classes :rewrite)

Theorem: natp-of-atj-gen-jlocvar-indexed.new-var-index

(defthm natp-of-atj-gen-jlocvar-indexed.new-var-index
  (implies (natp var-index)
           (b* (((mv ?locvar-block ?var-name ?new-var-index)
                 (atj-gen-jlocvar-indexed
                      var-type var-base var-index var-init?)))
             (natp new-var-index)))
  :rule-classes :rewrite)

Theorem: posp-of-atj-gen-jlocvar-indexed-new-var-index

(defthm posp-of-atj-gen-jlocvar-indexed-new-var-index
 (implies
  (posp var-index)
  (posp
   (mv-nth 2
           (atj-gen-jlocvar-indexed var-type
                                    var-base var-index var-init)))))