• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Set
      • C
      • Soft
      • Bv
      • Imp-language
      • Ethereum
      • 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-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-deep-term-fns
                  • Atj-gen-deep-fnapp
                  • Atj-gen-deep-lambda
                  • Atj-gen-deep-term
                  • Atj-gen-deep-terms
                • Atj-gen-deep-test-code
                • Atj-gen-deep-fndef-method
                • Atj-gen-deep-fnapp
                • Atj-gen-deep-env-class
                • Atj-gen-deep-env-cunit
                • Atj-gen-deep-lambda
                • Atj-gen-deep-qconst
                • Atj-gen-deep-main-class
                • Atj-gen-deep-term
                • Atj-gen-deep-terms
                • Atj-gen-deep-build-method
                • Atj-gen-deep-call-method
                • Atj-gen-deep-main-cunit
                • Atj-gen-deep-fndef-method-name
                • Atj-gen-deep-fndef-methods
                • Atj-gen-deep-fndefs
                • Atj-gen-deep-formals
                • Atj-gen-deep-var
              • 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
      • Riscv
      • Bitcoin
      • Zcash
      • Yul
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Axe
      • Lists-light
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Atj-deep-code-generation

Atj-gen-deep-term-fns

Functions to generate Java code to build deeply embedded ACL2 terms.

Definitions and Theorems

Function: atj-gen-deep-fnapp

(defun atj-gen-deep-fnapp (fn args jvar-value-base
                              jvar-value-index jvar-term-base
                              jvar-term-index jvar-lambda-base
                              jvar-lambda-index guards$)
 (declare (xargs :guard (and (pseudo-termfnp fn)
                             (pseudo-term-listp args)
                             (stringp jvar-value-base)
                             (posp jvar-value-index)
                             (stringp jvar-term-base)
                             (posp jvar-term-index)
                             (stringp jvar-lambda-base)
                             (posp jvar-lambda-index)
                             (booleanp guards$))))
 (let ((__function__ 'atj-gen-deep-fnapp))
  (declare (ignorable __function__))
  (b*
   (((mv fn args)
     (if (and (eq fn 'if)
              (= (len args) 3)
              (equal (first args) (second args)))
         (mv 'or
             (list (first args) (third args)))
       (mv fn args)))
    ((mv fn-block fn-expr jvar-value-index
         jvar-term-index jvar-lambda-index)
     (if (symbolp fn)
         (mv nil
             (jexpr-smethod *aij-type-named-fn*
                            "make" (list (atj-gen-symbol fn t nil)))
             jvar-value-index
             jvar-term-index jvar-lambda-index)
       (atj-gen-deep-lambda (lambda-formals fn)
                            (lambda-body fn)
                            jvar-value-base
                            jvar-value-index jvar-term-base
                            jvar-term-index jvar-lambda-base
                            jvar-lambda-index guards$)))
    ((mv args-block arg-exprs jvar-value-index
         jvar-term-index jvar-lambda-index)
     (atj-gen-deep-terms args jvar-value-base
                         jvar-value-index jvar-term-base
                         jvar-term-index jvar-lambda-base
                         jvar-lambda-index guards$))
    (args-expr (jexpr-newarray-init *aij-type-term* arg-exprs))
    (fnapp-expr (jexpr-smethod *aij-type-fn-app*
                               "make" (list fn-expr args-expr)))
    ((mv fnapp-locvar-block
         fnapp-jvar jvar-term-index)
     (atj-gen-jlocvar-indexed *aij-type-term* jvar-term-base
                              jvar-term-index fnapp-expr)))
   (mv (append fn-block args-block fnapp-locvar-block)
       (jexpr-name fnapp-jvar)
       jvar-value-index
       jvar-term-index jvar-lambda-index))))

Function: atj-gen-deep-lambda

(defun atj-gen-deep-lambda (formals body jvar-value-base
                                    jvar-value-index jvar-term-base
                                    jvar-term-index jvar-lambda-base
                                    jvar-lambda-index guards$)
 (declare (xargs :guard (and (symbol-listp formals)
                             (pseudo-termp body)
                             (stringp jvar-value-base)
                             (posp jvar-value-index)
                             (stringp jvar-term-base)
                             (posp jvar-term-index)
                             (stringp jvar-lambda-base)
                             (posp jvar-lambda-index)
                             (booleanp guards$))))
 (let ((__function__ 'atj-gen-deep-lambda))
   (declare (ignorable __function__))
   (b* ((formals-expr (atj-gen-deep-formals formals))
        ((mv body-block body-expr jvar-value-index
             jvar-term-index jvar-lambda-index)
         (atj-gen-deep-term body jvar-value-base
                            jvar-value-index jvar-term-base
                            jvar-term-index jvar-lambda-base
                            jvar-lambda-index guards$))
        (lambda-expr
             (jexpr-smethod *aij-type-lambda*
                            "make" (list formals-expr body-expr)))
        ((mv lambda-locvar-block
             lambda-jvar jvar-lambda-index)
         (atj-gen-jlocvar-indexed *aij-type-lambda* jvar-lambda-base
                                  jvar-lambda-index lambda-expr)))
     (mv (append body-block lambda-locvar-block)
         (jexpr-name lambda-jvar)
         jvar-value-index
         jvar-term-index jvar-lambda-index))))

Function: atj-gen-deep-term

(defun atj-gen-deep-term (term jvar-value-base
                               jvar-value-index jvar-term-base
                               jvar-term-index jvar-lambda-base
                               jvar-lambda-index guards$)
 (declare (xargs :guard (and (pseudo-termp term)
                             (stringp jvar-value-base)
                             (posp jvar-value-index)
                             (stringp jvar-term-base)
                             (posp jvar-term-index)
                             (stringp jvar-lambda-base)
                             (posp jvar-lambda-index)
                             (booleanp guards$))))
 (let ((__function__ 'atj-gen-deep-term))
  (declare (ignorable __function__))
  (cond
     ((variablep term)
      (mv nil (atj-gen-deep-var term)
          jvar-value-index
          jvar-term-index jvar-lambda-index))
     ((fquotep term)
      (b* (((mv block expr jvar-value-index)
            (atj-gen-deep-qconst (unquote term)
                                 jvar-value-base jvar-value-index)))
        (mv block expr jvar-value-index
            jvar-term-index jvar-lambda-index)))
     (t (atj-gen-deep-fnapp (ffn-symb term)
                            (fargs term)
                            jvar-value-base
                            jvar-value-index jvar-term-base
                            jvar-term-index jvar-lambda-base
                            jvar-lambda-index guards$)))))

Function: atj-gen-deep-terms

(defun atj-gen-deep-terms (terms jvar-value-base
                                 jvar-value-index jvar-term-base
                                 jvar-term-index jvar-lambda-base
                                 jvar-lambda-index guards$)
  (declare (xargs :guard (and (pseudo-term-listp terms)
                              (stringp jvar-value-base)
                              (posp jvar-value-index)
                              (stringp jvar-term-base)
                              (posp jvar-term-index)
                              (stringp jvar-lambda-base)
                              (posp jvar-lambda-index)
                              (booleanp guards$))))
  (let ((__function__ 'atj-gen-deep-terms))
    (declare (ignorable __function__))
    (if (endp terms)
        (mv nil nil jvar-value-index
            jvar-term-index jvar-lambda-index)
      (b* (((mv first-block expr jvar-value-index
                jvar-term-index jvar-lambda-index)
            (atj-gen-deep-term (car terms)
                               jvar-value-base
                               jvar-value-index jvar-term-base
                               jvar-term-index jvar-lambda-base
                               jvar-lambda-index guards$))
           ((mv rest-block exprs jvar-value-index
                jvar-term-index jvar-lambda-index)
            (atj-gen-deep-terms (cdr terms)
                                jvar-value-base
                                jvar-value-index jvar-term-base
                                jvar-term-index jvar-lambda-base
                                jvar-lambda-index guards$)))
        (mv (append first-block rest-block)
            (cons expr exprs)
            jvar-value-index
            jvar-term-index jvar-lambda-index)))))

Theorem: return-type-of-atj-gen-deep-fnapp.block

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

Theorem: return-type-of-atj-gen-deep-fnapp.expr

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

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

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

Theorem: return-type-of-atj-gen-deep-fnapp.new-jvar-term-index

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

Theorem: return-type-of-atj-gen-deep-fnapp.new-jvar-lambda-index

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

Theorem: return-type-of-atj-gen-deep-lambda.block

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

Theorem: return-type-of-atj-gen-deep-lambda.expr

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

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

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

Theorem: return-type-of-atj-gen-deep-lambda.new-jvar-term-index

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

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

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

Theorem: return-type-of-atj-gen-deep-term.block

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

Theorem: return-type-of-atj-gen-deep-term.expr

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

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

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

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

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

Theorem: return-type-of-atj-gen-deep-term.new-jvar-lambda-index

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

Theorem: return-type-of-atj-gen-deep-terms.block

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

Theorem: return-type-of-atj-gen-deep-terms.exprs

(defthm return-type-of-atj-gen-deep-terms.exprs
  (b* (((mv common-lisp::?block
            ?exprs ?new-jvar-value-index
            ?new-jvar-term-index
            ?new-jvar-lambda-index)
        (atj-gen-deep-terms terms jvar-value-base
                            jvar-value-index jvar-term-base
                            jvar-term-index jvar-lambda-base
                            jvar-lambda-index guards$)))
    (jexpr-listp exprs))
  :rule-classes :rewrite)

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

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

Theorem: return-type-of-atj-gen-deep-terms.new-jvar-term-index

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

Theorem: return-type-of-atj-gen-deep-terms.new-jvar-lambda-index

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

Subtopics

Atj-gen-deep-fnapp

Generate Java code to build a deeply embedded ACL2 function call.

Atj-gen-deep-lambda

Generate Java code to build a deeply embedded ACL2 lambda expression.

Atj-gen-deep-term

Generate Java code to build a deeply embedded ACL2 term.

Atj-gen-deep-terms

Lift atj-gen-deep-term to lists.