• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • 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
      • 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-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-code-generation

Atj-gen-everything

Generate the main Java file, the environment-building Java file, and optionally the test Java file.

Signature

(atj-gen-everything deep$ 
                    guards$ no-aij-types$ java-package$ 
                    java-class$ output-subdir output-file$ 
                    output-file-env$ output-file-test$ 
                    tests$ pkgs fns-to-translate 
                    call-graph verbose$ ctx state) 
 
  → 
(mv erp val state)

Arguments

deep$ — Guard (booleanp deep$).

guards$ — Guard (booleanp guards$).

no-aij-types$ — Guard (booleanp no-aij-types$).

java-package$ — Guard (maybe-stringp java-package$).

java-class$ — Guard (stringp java-class$).

output-subdir — Guard (stringp output-subdir).

output-file$ — Guard (stringp output-file$).

output-file-env$ — Guard (stringp output-file-env$).

output-file-test$ — Guard (maybe-stringp output-file-test$).

tests$ — Guard (atj-test-listp tests$).

pkgs — Guard (string-listp pkgs).

fns-to-translate — Guard (symbol-listp fns-to-translate).

call-graph — Guard (symbol-symbollist-alistp call-graph).

verbose$ — Guard (booleanp verbose$).

ctx — Guard (ctxp ctx).

We set the soft and hard right margins to very large values to avoid line breaks in virtually all cases. Setting these margins to ``infinity'' is not supported.

We always generate the main Java file. We generate the environment-building Java file if :no-aij-types is nil. We generate the test Java file if :tests is not nil.

We pass the alist from ACL2 package names to Java class names from one file generation function to another. This is nil in the deep embedding approach.

Definitions and Theorems

Function: atj-gen-everything

(defun atj-gen-everything
       (deep$ guards$ no-aij-types$ java-package$
              java-class$ output-subdir output-file$
              output-file-env$ output-file-test$
              tests$ pkgs fns-to-translate
              call-graph verbose$ ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (booleanp deep$)
                             (booleanp guards$)
                             (booleanp no-aij-types$)
                             (maybe-stringp java-package$)
                             (stringp java-class$)
                             (stringp output-subdir)
                             (stringp output-file$)
                             (stringp output-file-env$)
                             (maybe-stringp output-file-test$)
                             (atj-test-listp tests$)
                             (string-listp pkgs)
                             (symbol-listp fns-to-translate)
                             (symbol-symbollist-alistp call-graph)
                             (booleanp verbose$)
                             (ctxp ctx))))
 (let ((__function__ 'atj-gen-everything))
  (declare (ignorable __function__))
  (state-global-let*
   ((fmt-soft-right-margin 1000000 set-fmt-soft-right-margin)
    (fmt-hard-right-margin 1000000 set-fmt-hard-right-margin))
   (b*
    (((er &)
      (atj-gen-output-subdir output-subdir java-package$ ctx state))
     ((mv pkg-class-names fn-method-names state)
      (atj-gen-main-file deep$ guards$
                         no-aij-types$ java-package$ java-class$
                         output-file$ pkgs fns-to-translate
                         call-graph verbose$ state))
     (state
         (if no-aij-types$ state
           (atj-gen-env-file deep$ guards$ java-package$
                             java-class$ output-file-env$
                             pkgs fns-to-translate verbose$ state)))
     (state
      (if tests$
          (atj-gen-test-file deep$ guards$
                             no-aij-types$ java-package$ java-class$
                             output-file-test$ tests$ verbose$
                             pkg-class-names fn-method-names state)
        state)))
    (value nil)))))