		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-code-generation

Atj-gen-shallow-all-pkg-fields

Generate all the fields of the class for all the ACL2 packages.

Signature
(atj-gen-shallow-all-pkg-fields pkgs quoted-symbols quoted-symbols-by-pkg methods-by-pkg) → fields-by-pkg
Arguments: pkgs — Guard (string-listp pkgs).; 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-by-pkg — Type (string-jfieldlist-alistp fields-by-pkg), given (string-listp pkgs).

We go through all the packages in pkgs and construct an alist from the packages there to the corresponding fields lists (i.e. the fields of the class that corresponds to the package). If there are no fields for a package, we do not add an entry for the package in the alist.

Definitions and Theorems

Function: atj-gen-shallow-all-pkg-fields

(defun atj-gen-shallow-all-pkg-fields
       (pkgs quoted-symbols
             quoted-symbols-by-pkg methods-by-pkg)
 (declare
   (xargs
        :guard (and (string-listp pkgs)
                    (symbol-listp quoted-symbols)
                    (string-symbollist-alistp quoted-symbols-by-pkg)
                    (string-jmethodlist-alistp methods-by-pkg))))
 (let ((__function__ 'atj-gen-shallow-all-pkg-fields))
   (declare (ignorable __function__))
   (b* (((when (endp pkgs)) nil)
        (pkg (car pkgs))
        (first-fields (atj-gen-shallow-pkg-fields
                           pkg quoted-symbols
                           quoted-symbols-by-pkg methods-by-pkg))
        (rest-fields (atj-gen-shallow-all-pkg-fields
                          (cdr pkgs)
                          quoted-symbols
                          quoted-symbols-by-pkg methods-by-pkg)))
     (if (null first-fields)
         rest-fields
       (acons pkg first-fields rest-fields)))))

Theorem: string-jfieldlist-alistp-of-atj-gen-shallow-all-pkg-fields

(defthm string-jfieldlist-alistp-of-atj-gen-shallow-all-pkg-fields
 (implies
    (string-listp pkgs)
    (b* ((fields-by-pkg (atj-gen-shallow-all-pkg-fields
                             pkgs quoted-symbols
                             quoted-symbols-by-pkg methods-by-pkg)))
      (string-jfieldlist-alistp fields-by-pkg)))
 :rule-classes :rewrite)