		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-code-generation

Atj-gen-shallow-pkg-fields

Generate all the fields of the class for an ACL2 package.

Signature
(atj-gen-shallow-pkg-fields pkg quoted-symbols quoted-symbols-by-pkg methods-by-pkg) → fields
Arguments: pkg — Guard (stringp pkg).; quoted-symbols — Guard (symbol-listp quoted-symbols).; quoted-symbols-by-pkg — Guard (string-symbollist-alistp quoted-symbols-by-pkg).; methods-by-pkg — Guard (string-jmethodlist-alistp methods-by-pkg).
Returns: fields — Type (jfield-listp fields).

We generate fields for the symbols in quoted-symbols-by-pkg (i.e. the quoted symbols that appear in the bodies of the ACL2 functions that are translated to Java, organized by package) that are associated to pkg. These are all symbols whose package name is pkg.

If the class for the package has any methods, we also generate fields for the symbols in quoted-symbols (i.e. all the symbols in quoted-symbols-by-pkg, in a flat list) that are imported by pkg. This enables the unqualified reference to them in those methods; see atj-gen-shallow-symbol.

We sort all the fields, so that they appear in that order.

Definitions and Theorems

Function: atj-gen-shallow-pkg-fields

(defun atj-gen-shallow-pkg-fields
       (pkg quoted-symbols
            quoted-symbols-by-pkg methods-by-pkg)
 (declare
   (xargs
        :guard (and (stringp pkg)
                    (symbol-listp quoted-symbols)
                    (string-symbollist-alistp quoted-symbols-by-pkg)
                    (string-jmethodlist-alistp methods-by-pkg))))
 (let ((__function__ 'atj-gen-shallow-pkg-fields))
   (declare (ignorable __function__))
   (b*
     ((syms (cdr (assoc-equal pkg quoted-symbols-by-pkg)))
      (imported-syms
           (and (cdr (assoc-equal pkg methods-by-pkg))
                (intersection-eq quoted-symbols (pkg-imports pkg))))
      (all-syms (append syms imported-syms))
      (all-fields (atj-gen-shallow-symbol-fields all-syms)))
     (mergesort-jfields all-fields))))

Theorem: jfield-listp-of-atj-gen-shallow-pkg-fields

(defthm jfield-listp-of-atj-gen-shallow-pkg-fields
  (b* ((fields (atj-gen-shallow-pkg-fields
                    pkg quoted-symbols
                    quoted-symbols-by-pkg methods-by-pkg)))
    (jfield-listp fields))
  :rule-classes :rewrite)