		Search-engine friendly clone of the ACL2 documentation.

Defmake-self-event-generation

Defmake-self-gen-clique

Generate the events for a type clique.

Signature
(defmake-self-gen-clique clique-name fty-table make-self-table) → (mv er? events)
Arguments: clique-name — Guard (symbolp clique-name).; fty-table — Guard (alistp fty-table).; make-self-table — Guard (alistp make-self-table).
Returns: er? — Type (acl2::maybe-msgp er?).; events — Type (acl2::pseudo-event-form-listp events).

Definitions and Theorems

Function: defmake-self-gen-clique

(defun defmake-self-gen-clique
       (clique-name fty-table make-self-table)
 (declare (xargs :guard (and (symbolp clique-name)
                             (alistp fty-table)
                             (alistp make-self-table))))
 (let ((__function__ 'defmake-self-gen-clique))
  (declare (ignorable __function__))
  (b*
   (((reterr) nil)
    ((when (assoc-eq clique-name make-self-table))
     (retok nil))
    (clique (flextypes-with-name clique-name fty-table))
    ((unless clique)
     (retmsg$ "Internal error: No type (clique) with name ~x0."
              clique-name))
    ((unless (flextypes-p clique))
     (retmsg$ "Internal error: malformed type clique ~x0."
              clique))
    (members (flextypes->types clique))
    ((unless (and (consp members)
                  (true-listp (cdr members))))
     (retmsg$
          "Internal error: malformed members of type clique ~x0."
          clique))
    ((when (endp members))
     (retmsg$ "Internal error: empty type clique ~x0."
              clique))
    (member-names (flextype-list->name-list members))
    (clique-name-make-self (defmake-self-gen-name clique-name))
    (mutrecp (< 1 (len members)))
    (definition-events (defmake-self-gen-types
                            members mutrecp
                            member-names fty-table make-self-table))
    (table-events
         (defmake-self-gen-table-events clique-name member-names))
    ((unless mutrecp)
     (retok (append definition-events table-events)))
    (defines-event
     (cons
      'defines
      (cons
       clique-name-make-self
       (cons
        ':parents
        (cons
         (cons (defmake-self-gen-topic-name clique-name)
               'nil)
         (append
          definition-events
          (cons
           ':hints
           (cons
            '(("Goal" :in-theory (enable o< o-finp)))
            (cons
             ':flag-local
             (cons
              'nil
              (cons
               ':prepwork
               (cons
                '((set-bogus-mutual-recursion-ok t))
                (cons
                 '///
                 (cons
                  (cons
                   'deffixequiv-mutual
                   (cons
                    clique-name-make-self
                    '(:hints
                        (("Goal"
                              :in-theory (disable (tau-system)))))))
                  'nil)))))))))))))))
   (retok (cons defines-event table-events)))))

Theorem: maybe-msgp-of-defmake-self-gen-clique.er?

(defthm maybe-msgp-of-defmake-self-gen-clique.er?
  (b* (((mv ?er? ?events)
        (defmake-self-gen-clique
             clique-name fty-table make-self-table)))
    (acl2::maybe-msgp er?))
  :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-defmake-self-gen-clique.events

(defthm pseudo-event-form-listp-of-defmake-self-gen-clique.events
  (b* (((mv ?er? ?events)
        (defmake-self-gen-clique
             clique-name fty-table make-self-table)))
    (acl2::pseudo-event-form-listp events))
  :rule-classes :rewrite)

Theorem: true-listp-of-defmake-self-gen-clique.events

(defthm true-listp-of-defmake-self-gen-clique.events
  (b* (((mv ?er? ?events)
        (defmake-self-gen-clique
             clique-name fty-table make-self-table)))
    (true-listp events))
  :rule-classes :type-prescription)