• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
        • Bv
        • Imp-language
        • Event-macros
        • Java
          • Atj
            • Atj-implementation
              • Atj-types
              • Atj-java-primitive-array-model
              • Atj-java-abstract-syntax
              • Atj-input-processing
              • Atj-java-pretty-printer
              • Atj-code-generation
                • Atj-gen-test-method
                • Atj-shallow-code-generation
                • Atj-common-code-generation
                  • Atj-gen-value
                    • Atj-gen-values
                    • Atj-gen-list
                  • Atj-chars-to-jhexcodes
                  • Atj-gen-test-value
                  • Atj-gen-test-main-method
                  • Atj-gen-value-flat
                  • Atj-gen-test-values
                  • Atj-gen-jlocvar-indexed
                  • Atj-gen-pkg-method
                  • Atj-gen-symbol
                  • Atj-gen-jstring
                  • Atj-gen-init-method
                  • Atj-gen-char
                  • Atj-gen-string
                  • Atj-gen-pkg-name
                  • Atj-gen-integer
                  • Atj-gen-test-method-name
                  • Atj-gen-paramlist
                  • Atj-gen-pkg-method-name
                  • Atj-gen-run-tests
                  • Atj-gen-jshort-array
                  • Atj-gen-jboolean-array
                  • Atj-gen-test-failures-field
                  • Atj-gen-pkgs
                  • Atj-gen-jlong-array
                  • Atj-gen-jint-array
                  • Atj-gen-jchar-array
                  • Atj-gen-jchar
                  • Atj-gen-jbyte-array
                  • Atj-char-to-jhexcode
                  • Atj-gen-pkg-methods
                  • Atj-gen-number
                  • Atj-gen-symbols
                  • Atj-gen-static-initializer
                  • Atj-gen-rational
                  • Atj-gen-jlong
                  • Atj-gen-jboolean
                  • Atj-gen-jbigint
                  • Atj-gen-jshort
                  • Atj-gen-jint
                  • Atj-gen-jbyte
                  • *atj-gen-pkg-name-alist*
                • Atj-shallow-quoted-constant-generation
                • Atj-pre-translation
                • Atj-gen-everything
                • Atj-name-translation
                • Atj-gen-test-cunit
                • Atj-gen-test-class
                • Atj-gen-main-file
                • Atj-post-translation
                • Atj-deep-code-generation
                • Atj-gen-test-methods
                • Atj-gen-test-file
                • Atj-gen-env-file
                • Atj-gen-output-subdir
              • Atj-java-primitives
              • Atj-java-primitive-arrays
              • Atj-type-macros
              • Atj-java-syntax-operations
              • Atj-fn
              • Atj-library-extensions
              • Atj-java-input-types
              • Atj-test-structures
              • Aij-notions
              • Atj-macro-definition
            • Atj-tutorial
          • Aij
          • Language
        • Bitcoin
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Lists-light
        • Axe
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Atj-common-code-generation

Atj-gen-value

Generate Java code to build an ACL2 value.

Signature
(atj-gen-value value jvar-value-base jvar-value-index deep$ guards$) 
  → 
(mv block expr new-jvar-value-index)
Arguments
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).
new-jvar-value-index — Type (posp new-jvar-value-index), given (posp jvar-value-index).

For a cons pair that is also a true list, the generated code builds all the elements and then calls Acl2Value.makeList() (a variable arity method) with the elements; the result is cast to Acl2ConsPair. For a cons pair that is not a true list, the generated code builds the car, sets a local variable to it, builds the cdr, sets another local variable to it, and then calls Acl2ConsValue.make() with the two local variables.

The deep$ and guards$ arguments are passed from atj-gen-value to atj-gen-symbol, atj-gen-char, and atj-gen-string only at the top level; this is so that we generate Java boolean, character, and string expressions for ACL2 boolean, character, and string values, in the shallow embedding with guards. But at the non-top levels, these flags are set to t and nil, because ACL2 booleans, characters, and strings are represented as Acl2Symbol, Acl2Character, and Acl2String instances inside other values (conses).

Function: atj-gen-value

(defun atj-gen-value (value jvar-value-base
                            jvar-value-index deep$ guards$)
 (declare (xargs :guard (and (stringp jvar-value-base)
                             (posp jvar-value-index)
                             (booleanp deep$)
                             (booleanp guards$))))
 (let ((__function__ 'atj-gen-value))
  (declare (ignorable __function__))
  (cond
    ((characterp value)
     (mv nil (atj-gen-char value deep$ guards$)
         jvar-value-index))
    ((stringp value)
     (mv nil (atj-gen-string value deep$ guards$)
         jvar-value-index))
    ((symbolp value)
     (mv nil (atj-gen-symbol value deep$ guards$)
         jvar-value-index))
    ((integerp value)
     (mv nil (atj-gen-integer value)
         jvar-value-index))
    ((rationalp value)
     (mv nil (atj-gen-rational value)
         jvar-value-index))
    ((acl2-numberp value)
     (mv nil (atj-gen-number value)
         jvar-value-index))
    ((true-listp value)
     (atj-gen-list value jvar-value-base jvar-value-index))
    ((consp value)
     (atj-gen-cons value jvar-value-base jvar-value-index))
    (t (prog2$ (raise "Internal error: the value ~x0 is a bad atom."
                      value)
               (mv nil (jexpr-name "this-is-irrelevant")
                   jvar-value-index))))))

Function: atj-gen-values

(defun atj-gen-values (values jvar-value-base jvar-value-index)
 (declare (xargs :guard (and (true-listp values)
                             (stringp jvar-value-base)
                             (posp jvar-value-index))))
 (let ((__function__ 'atj-gen-values))
  (declare (ignorable __function__))
  (cond
    ((endp values)
     (mv nil nil jvar-value-index))
    (t (b* (((mv first-block first-expr jvar-value-index)
             (atj-gen-value (car values)
                            jvar-value-base jvar-value-index t nil))
            ((mv rest-block rest-jexprs jvar-value-index)
             (atj-gen-values (cdr values)
                             jvar-value-base jvar-value-index)))
         (mv (append first-block rest-block)
             (cons first-expr rest-jexprs)
             jvar-value-index))))))

Function: atj-gen-list

(defun atj-gen-list (list jvar-value-base jvar-value-index)
  (declare (xargs :guard (and (true-listp list)
                              (stringp jvar-value-base)
                              (posp jvar-value-index))))
  (declare (xargs :guard (consp list)))
  (let ((__function__ 'atj-gen-list))
    (declare (ignorable __function__))
    (b* (((mv block exprs jvar-value-index)
          (atj-gen-values list jvar-value-base jvar-value-index))
         (expr (jexpr-smethod *aij-type-value* "makeList" exprs)))
      (mv block (jexpr-cast *aij-type-cons* expr)
          jvar-value-index))))

Function: atj-gen-cons

(defun atj-gen-cons (conspair jvar-value-base jvar-value-index)
  (declare (xargs :guard (and (consp conspair)
                              (stringp jvar-value-base)
                              (posp jvar-value-index))))
  (let ((__function__ 'atj-gen-cons))
    (declare (ignorable __function__))
    (b* (((unless (mbt (consp conspair)))
          (mv nil (jexpr-name "this-is-irrelevant")
              jvar-value-index))
         ((mv car-block car-expr jvar-value-index)
          (atj-gen-value (car conspair)
                         jvar-value-base jvar-value-index t nil))
         ((mv car-locvar-block
              car-jvar jvar-value-index)
          (atj-gen-jlocvar-indexed *aij-type-value* jvar-value-base
                                   jvar-value-index car-expr))
         ((mv cdr-block cdr-expr jvar-value-index)
          (atj-gen-value (cdr conspair)
                         jvar-value-base jvar-value-index t nil))
         ((mv cdr-locvar-block
              cdr-jvar jvar-value-index)
          (atj-gen-jlocvar-indexed *aij-type-value* jvar-value-base
                                   jvar-value-index cdr-expr))
         (block (append car-block car-locvar-block
                        cdr-block cdr-locvar-block))
         (expr (jexpr-smethod *aij-type-cons* "make"
                              (list (jexpr-name car-jvar)
                                    (jexpr-name cdr-jvar)))))
      (mv block expr jvar-value-index))))

Theorem: return-type-of-atj-gen-value.block

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

Theorem: return-type-of-atj-gen-value.expr

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

Theorem: return-type-of-atj-gen-value.new-jvar-value-index

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

Theorem: return-type-of-atj-gen-values.block

(defthm return-type-of-atj-gen-values.block
  (b* (((mv common-lisp::?block
            ?exprs ?new-jvar-value-index)
        (atj-gen-values values
                        jvar-value-base jvar-value-index)))
    (jblockp block))
  :rule-classes :rewrite)

Theorem: return-type-of-atj-gen-values.exprs

(defthm return-type-of-atj-gen-values.exprs
  (b* (((mv common-lisp::?block
            ?exprs ?new-jvar-value-index)
        (atj-gen-values values
                        jvar-value-base jvar-value-index)))
    (and (jexpr-listp exprs)
         (equal (len exprs) (len values))))
  :rule-classes :rewrite)

Theorem: return-type-of-atj-gen-values.new-jvar-value-index

(defthm return-type-of-atj-gen-values.new-jvar-value-index
  (implies (posp jvar-value-index)
           (b* (((mv common-lisp::?block
                     ?exprs ?new-jvar-value-index)
                 (atj-gen-values values
                                 jvar-value-base jvar-value-index)))
             (posp new-jvar-value-index)))
  :rule-classes :rewrite)

Theorem: return-type-of-atj-gen-list.block

(defthm return-type-of-atj-gen-list.block
  (b* (((mv common-lisp::?block
            ?expr ?new-jvar-value-index)
        (atj-gen-list list jvar-value-base jvar-value-index)))
    (jblockp block))
  :rule-classes :rewrite)

Theorem: return-type-of-atj-gen-list.expr

(defthm return-type-of-atj-gen-list.expr
  (b* (((mv common-lisp::?block
            ?expr ?new-jvar-value-index)
        (atj-gen-list list jvar-value-base jvar-value-index)))
    (jexprp expr))
  :rule-classes :rewrite)

Theorem: return-type-of-atj-gen-list.new-jvar-value-index

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

Theorem: return-type-of-atj-gen-cons.block

(defthm return-type-of-atj-gen-cons.block
  (b* (((mv common-lisp::?block
            ?expr ?new-jvar-value-index)
        (atj-gen-cons conspair
                      jvar-value-base jvar-value-index)))
    (jblockp block))
  :rule-classes :rewrite)

Theorem: return-type-of-atj-gen-cons.expr

(defthm return-type-of-atj-gen-cons.expr
  (b* (((mv common-lisp::?block
            ?expr ?new-jvar-value-index)
        (atj-gen-cons conspair
                      jvar-value-base jvar-value-index)))
    (jexprp expr))
  :rule-classes :rewrite)

Theorem: return-type-of-atj-gen-cons.new-jvar-value-index

(defthm return-type-of-atj-gen-cons.new-jvar-value-index
  (implies (posp jvar-value-index)
           (b* (((mv common-lisp::?block
                     ?expr ?new-jvar-value-index)
                 (atj-gen-cons conspair
                               jvar-value-base jvar-value-index)))
             (posp new-jvar-value-index)))
  :rule-classes :rewrite)

Subtopics

Atj-gen-values
Atj-gen-list