alistof

(defun alistof-theory-events
  (name keybody
    valbody
    new-types
    kwd-alist
    wrld)
  (declare (ignorable valbody))
  (declare (xargs :mode :program))
  (b* ((m (append new-types
         (table-alist 'type-metadata-table
           wrld))) (a (table-alist 'type-alias-table
          wrld))
      (pred (predicate-name name
          a
          m))
      ((when (not (proper-symbolp pred))) (er hard?
          'alistof-theory-events
          "~| Couldnt find predicate name for ~x0.~%"
          name))
      ((mv symbol-alist-subtypep
         ?keypred) (if (and (proper-symbolp keybody)
            (assoc-eq keybody m))
          (mv (subtype-p (predicate-name keybody
                a
                m)
              'symbolp
              wrld)
            (predicate-name keybody
              a
              m))
          (mv nil :undef)))
      (disabled (get1 :disabled kwd-alist))
      (curr-pkg (get1 :current-package kwd-alist))
      (pkg-sym (pkg-witness curr-pkg))
      (local-events-template nil)
      (export-defthms-template *alistof-export-defthms*)
      (features (and symbol-alist-subtypep
          '(:symbol-alist-subtype-p)))
      (splice-alist `((_disabled-runes_ . ,DEFDATA::DISABLED)))
      (atom-alist `((_pred_ . ,DEFDATA::PRED) (_keypred_ . ,DEFDATA::KEYPRED)))
      (str-alist `(("_PRED_" . ,(SYMBOL-NAME DEFDATA::PRED)) ("_KEYPRED_" . ,(SYMBOL-NAME DEFDATA::KEYPRED))))
      (local-events (template-subst local-events-template
          :features features
          :splice-alist splice-alist
          :atom-alist atom-alist
          :str-alist str-alist
          :pkg-sym pkg-sym))
      (export-defthms (template-subst export-defthms-template
          :features features
          :splice-alist splice-alist
          :atom-alist atom-alist
          :str-alist str-alist
          :pkg-sym pkg-sym))
      (all-defthm-names (get-event-names export-defthms))
      (theory-name (get1 :theory-name kwd-alist)))
    `(,@(AND DEFDATA::LOCAL-EVENTS
       `((DEFDATA::LOCAL (PROGN . ,DEFDATA::LOCAL-EVENTS)))) ,@DEFDATA::EXPORT-DEFTHMS
      (def-ruleset! ,DEFDATA::THEORY-NAME
        ',DEFDATA::ALL-DEFTHM-NAMES))))

(defun alistof-theory-ev
  (p top-kwd-alist wrld)
  (b* (((cons name a) p) ((assocs pdef new-types kwd-alist) a)
      (kwd-alist (append kwd-alist top-kwd-alist)))
    (case-match pdef
      (('alistof key-body val-body) (alistof-theory-events name
          key-body
          val-body
          new-types
          kwd-alist
          wrld))
      (& 'nil))))

(defun user-alistof-theory-events
  (ps kwd-alist wrld)
  (b* ((events (user-alistof-theory-events1 ps
         kwd-alist
         wrld)))
    (and (consp events)
      (append `((commentary ,(DEFDATA::GET1 :PRINT-COMMENTARY DEFDATA::KWD-ALIST)
           "~| Alistof theory events...~%") (value-triple (progn$ (time-tracker :alistof-theory-events :end)
              (time-tracker :alistof-theory-events :init :times '(2 7)
                :interval 5
                :msg "Elapsed runtime in theory events for alistof is ~st secs;~|~%")
              :invisible)))
        events))))