organize-symbols-by-pkg

(in-package "ACL2")

(define organize-symbols-by-pkg
  ((syms symbol-listp))
  :returns (syms-by-pkg string-symbollist-alistp :hyp :guard)
  :parents (std/basic)
  :short "Organize a list of symbols by their packages."
  :long (topstring (p "The result is an alist from package names (strings)
     to the non-empty lists of the symbols
     that are in the respective packages.")
    (p "The alist has unique keys,
     and each of its values has no duplicates."))
  (organize-symbols-by-pkg-aux syms nil)
  :prepwork ((define organize-symbols-by-pkg-aux
     ((syms symbol-listp) (acc string-symbollist-alistp))
     :returns (syms-by-pkg string-symbollist-alistp :hyp :guard)
     :parents nil
     (b* (((when (endp syms)) acc) (sym (car syms))
         (pkg (symbol-package-name sym))
         (prev-syms-for-pkg (cdr (assoc-equal pkg acc))))
       (organize-symbols-by-pkg-aux (cdr syms)
         (put-assoc-equal pkg
           (add-to-set-eq sym prev-syms-for-pkg)
           acc))))))