		Search-engine friendly clone of the ACL2 documentation.

Deffold-reduce-event-generation

Deffoldred-gen-everything

Generate all the events.

Signature
(deffoldred-gen-everything suffix types targets extra-args result default combine 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).; result — Guard (symbolp result).; combine — Guard (symbolp combine).; 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: deffoldred-gen-everything

(defun deffoldred-gen-everything
       (suffix types targets extra-args result default
               combine 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)
                             (symbolp result)
                             (symbolp combine)
                             (alistp overrides)
                             (booleanp parents-presentp)
                             (booleanp short-presentp)
                             (booleanp long-presentp)
                             (alistp fty-table)
                             (acl2::evmac-input-print-p print))))
 (let ((__function__ 'deffoldred-gen-everything))
  (declare (ignorable __function__))
  (b*
   ((fold-events (deffoldred-gen-cliques-folds
                      types suffix targets extra-args result
                      default combine overrides fty-table))
    (xdoc-name (deffoldred-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 (deffoldred-gen-ruleset-name suffix)
                               '(nil))))
    (encapsulate
             (cons 'encapsulate
                   (cons 'nil
                         (cons xdoc-event
                               (cons ruleset-event fold-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-deffoldred-gen-everything

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