		Search-engine friendly clone of the ACL2 documentation.

Atj-input-processing

Atj-pkgs-to-translate

Collect all the ACL2 packages to be translated to Java.

Signature
(atj-pkgs-to-translate verbose$ state) → pkgs
Arguments: verbose$ — Guard (booleanp verbose$).
Returns: pkgs — Type (string-listp pkgs).

Here `translate to Java' really means `build a Java representation of'.

For now we return all the current packages. In the future, it might be possible to reduce them to just the ones referenced by the functions to be translated to Java.

Definitions and Theorems

Function: atj-show-pkgs

(defun atj-show-pkgs (pkgs)
  (declare (xargs :guard (string-listp pkgs)))
  (let ((__function__ 'atj-show-pkgs))
    (declare (ignorable __function__))
    (if (endp pkgs)
        nil
      (b* ((- (cw "  ~s0~%" (car pkgs))))
        (atj-show-pkgs (cdr pkgs))))))

Theorem: null-of-atj-show-pkgs

(defthm null-of-atj-show-pkgs
  (b* ((nothing (atj-show-pkgs pkgs)))
    (null nothing))
  :rule-classes :rewrite)

Function: atj-pkgs-to-translate

(defun atj-pkgs-to-translate (verbose$ state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (booleanp verbose$)))
  (let ((__function__ 'atj-pkgs-to-translate))
    (declare (ignorable __function__))
    (b* ((pkgs (known-packages+ state))
         ((run-when verbose$)
          (cw "~%Known ACL2 packages:~%")
          (atj-show-pkgs pkgs)))
      pkgs)))

Theorem: string-listp-of-atj-pkgs-to-translate

(defthm string-listp-of-atj-pkgs-to-translate
  (b* ((pkgs (atj-pkgs-to-translate verbose$ state)))
    (string-listp pkgs))
  :rule-classes :rewrite)