Generate all the fields of the class for an ACL2 package.
(atj-gen-shallow-pkg-fields pkg quoted-symbols quoted-symbols-by-pkg methods-by-pkg) → fields
We generate fields for the symbols in
If the class for the package has any methods,
we also generate fields for the symbols in
We sort all the fields, so that they appear in that order.
Function:
(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:
(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)