		Search-engine friendly clone of the ACL2 documentation.

Deffold-map-event-generation

Deffold-map-gen-everything

Generate all the events.

Signature
(deffold-map-gen-everything suffix types targets extra-args overrides parents-presentp parents short-presentp short long-presentp long fty-table print) → event
Arguments: suffix — Guard (symbolp suffix).; types — Guard (symbol-listp types).; targets — Guard (symbol-listp targets).; extra-args — Guard (true-listp extra-args).; overrides — Guard (alistp overrides).; parents-presentp — Guard (booleanp parents-presentp).; short-presentp — Guard (booleanp short-presentp).; long-presentp — Guard (booleanp long-presentp).; fty-table — Guard (alistp fty-table).; print — Guard (acl2::evmac-input-print-p print).
Returns: event — Type (acl2::pseudo-event-formp event).

Definitions and Theorems

Function: deffold-map-gen-everything

(defun deffold-map-gen-everything
       (suffix types targets
               extra-args overrides parents-presentp
               parents short-presentp short
               long-presentp long fty-table print)
 (declare (xargs :guard (and (symbolp suffix)
                             (symbol-listp types)
                             (symbol-listp targets)
                             (true-listp extra-args)
                             (alistp overrides)
                             (booleanp parents-presentp)
                             (booleanp short-presentp)
                             (booleanp long-presentp)
                             (alistp fty-table)
                             (acl2::evmac-input-print-p print))))
 (let ((__function__ 'deffold-map-gen-everything))
  (declare (ignorable __function__))
  (b*
   ((map-events (deffold-map-gen-cliques-maps
                     types suffix
                     targets extra-args overrides fty-table))
    (xdoc-name (deffold-map-gen-topic-name suffix))
    (xdoc-event
     (cons
      'acl2::defxdoc+
      (cons
        xdoc-name
        (append (and parents-presentp
                     (cons ':parents (cons parents 'nil)))
                (append (and short-presentp
                             (cons ':short (cons short 'nil)))
                        (append (and long-presentp
                                     (cons ':long (cons long 'nil)))
                                '(:order-subtopics t)))))))
    (ruleset-event (cons 'def-ruleset!
                         (cons (deffold-map-gen-ruleset-name suffix)
                               '(nil))))
    (encapsulate
              (cons 'encapsulate
                    (cons 'nil
                          (cons xdoc-event
                                (cons ruleset-event map-events))))
)
    (encapsulate (acl2::restore-output? (eq print :all)
                                        encapsulate)
)
    (print-result
      (if
       (member-eq print '(:result :info))
       (cons (cons 'acl2::cw-event
                   (cons '"~x0~|"
                         (cons (cons 'quote (cons encapsulate 'nil))
                               'nil)))
             'nil)
       nil)))
   (cons 'progn
         (append print-result
                 (cons encapsulate
                       '((value-triple :invisible))))))))

Theorem: pseudo-event-formp-of-deffold-map-gen-everything

(defthm pseudo-event-formp-of-deffold-map-gen-everything
  (b* ((event (deffold-map-gen-everything
                   suffix types targets
                   extra-args overrides parents-presentp
                   parents short-presentp short
                   long-presentp long fty-table print)))
    (acl2::pseudo-event-formp event))
  :rule-classes :rewrite)