		Search-engine friendly clone of the ACL2 documentation.

Deftreeops-event-generation

Deftreeops-gen-everything

Generate all the events.

Signature
(deftreeops-gen-everything grammar rules prefix print call) → event
Arguments: grammar — Guard (common-lisp::symbolp grammar).; rules — Guard (rulelistp rules).; prefix — Guard (common-lisp::symbolp prefix).; print — Guard (evmac-input-print-p print).; call — Guard (pseudo-event-formp call).
Returns: event — Type (pseudo-event-formp event).

If the :print input is :all, we use restore-output? to restore all the output, which make-event-terse otherwise suppresses.

Definitions and Theorems

Function: deftreeops-gen-everything

(defun deftreeops-gen-everything (grammar rules prefix print call)
 (declare (xargs :guard (and (common-lisp::symbolp grammar)
                             (rulelistp rules)
                             (common-lisp::symbolp prefix)
                             (evmac-input-print-p print)
                             (pseudo-event-formp call))))
 (let ((__function__ 'deftreeops-gen-everything))
  (declare (ignorable __function__))
  (b*
   (((mv matchers matchers-event-alist)
     (deftreeops-gen-matchers grammar prefix print))
    ((mv numrange-infos
         numrange-events numrange-event-alist)
     (deftreeops-gen-all-numrange-infos+events rules prefix print))
    ((mv charval-infos
         charval-events charval-event-alist)
     (deftreeops-gen-all-charval-infos+events rules prefix print))
    ((mv rulename-infos
         rulename-events rulename-event-alist)
     (deftreeops-gen-all-rulename-infos+events
          rules charval-infos prefix print))
    (event-alist (append matchers-event-alist
                         numrange-event-alist charval-event-alist
                         rulename-event-alist))
    (table-value (make-deftreeops-table-value
                      :rulename-info-alist rulename-infos
                      :numrange-info-alist numrange-infos
                      :charval-info-alist charval-infos
                      :event-alist event-alist
                      :call call))
    (event
     (cons
      'defsection
      (cons
       (add-suffix grammar "-TREE-OPERATIONS")
       (cons
        ':parents
        (cons
         (cons grammar 'nil)
         (cons
          ':short
          (cons
           (str::cat "Tree operations specialized to @(tsee "
                     (str::downcase-string (symbol-name grammar))
                     ").")
           (append
            matchers
            (append
             numrange-events
             (append
               charval-events
               (append
                    rulename-events
                    (cons (deftreeops-table-add grammar table-value)
                          'nil))))))))))))
    (event (restore-output? (eq print :all)
                            event)))
   event)))

Theorem: pseudo-event-formp-of-deftreeops-gen-everything

(defthm pseudo-event-formp-of-deftreeops-gen-everything
 (b*
  ((event
       (deftreeops-gen-everything grammar rules prefix print call)))
  (pseudo-event-formp event))
 :rule-classes :rewrite)