Filtering...

organize-symbols-by-name

books/std/basic/organize-symbols-by-name

Included Books

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