		Search-engine friendly clone of the ACL2 documentation.

Schemalg-event-generation

Schemalg-gen-everything

Generate the top-level event.

Signature
(schemalg-gen-everything old ?f x-x1...xn x-a1...am x y iorel schema ?g ?g0 ?g1 ?h algo algo-enable spec-0 spec-0-enable spec-1 spec-1-enable spec-2 spec-2-enable equal-algo equal-algo-enable new new-enable old-if-new old-if-new-enable verify-guards print show-only call names-to-avoid wrld) → event
Arguments: old — Guard (symbolp old).; ?f — Guard (symbolp ?f).; x-x1...xn — Guard (symbol-listp x-x1...xn).; x-a1...am — Guard (pseudo-term-listp x-a1...am).; x — Guard (symbolp x).; y — Guard (symbolp y).; iorel — Guard (pseudo-lambdap iorel).; schema — Guard (keywordp schema).; ?g — Guard (symbolp ?g).; ?g0 — Guard (symbolp ?g0).; ?g1 — Guard (symbolp ?g1).; ?h — Guard (symbolp ?h).; algo — Guard (symbolp algo).; algo-enable — Guard (booleanp algo-enable).; spec-0 — Guard (symbolp spec-0).; spec-0-enable — Guard (booleanp spec-0-enable).; spec-1 — Guard (symbolp spec-1).; spec-1-enable — Guard (booleanp spec-1-enable).; spec-2 — Guard (symbolp spec-2).; spec-2-enable — Guard (booleanp spec-2-enable).; equal-algo — Guard (symbolp equal-algo).; equal-algo-enable — Guard (booleanp equal-algo-enable).; new — Guard (symbolp new).; new-enable — Guard (booleanp new-enable).; old-if-new — Guard (symbolp old-if-new).; old-if-new-enable — Guard (booleanp old-if-new-enable).; verify-guards — Guard (booleanp verify-guards).; print — Guard (evmac-input-print-p print).; show-only — Guard (booleanp show-only).; call — Guard (pseudo-event-formp call).; names-to-avoid — Guard (symbol-listp names-to-avoid).; wrld — Guard (plist-worldp wrld).
Returns: event — A pseudo-event-formp.

Definitions and Theorems

Function: schemalg-gen-everything

(defun schemalg-gen-everything
       (old ?f x-x1...xn x-a1...am
            x y iorel schema ?g ?g0 ?g1 ?h algo
            algo-enable spec-0 spec-0-enable spec-1
            spec-1-enable spec-2 spec-2-enable
            equal-algo equal-algo-enable
            new new-enable old-if-new
            old-if-new-enable verify-guards print
            show-only call names-to-avoid wrld)
 (declare (xargs :guard (and (symbolp old)
                             (symbolp ?f)
                             (symbol-listp x-x1...xn)
                             (pseudo-term-listp x-a1...am)
                             (symbolp x)
                             (symbolp y)
                             (pseudo-lambdap iorel)
                             (keywordp schema)
                             (symbolp ?g)
                             (symbolp ?g0)
                             (symbolp ?g1)
                             (symbolp ?h)
                             (symbolp algo)
                             (booleanp algo-enable)
                             (symbolp spec-0)
                             (booleanp spec-0-enable)
                             (symbolp spec-1)
                             (booleanp spec-1-enable)
                             (symbolp spec-2)
                             (booleanp spec-2-enable)
                             (symbolp equal-algo)
                             (booleanp equal-algo-enable)
                             (symbolp new)
                             (booleanp new-enable)
                             (symbolp old-if-new)
                             (booleanp old-if-new-enable)
                             (booleanp verify-guards)
                             (evmac-input-print-p print)
                             (booleanp show-only)
                             (pseudo-event-formp call)
                             (symbol-listp names-to-avoid)
                             (plist-worldp wrld))))
 (let ((__function__ 'schemalg-gen-everything))
  (declare (ignorable __function__))
  (b*
   ((spec1...specq
         (case schema
           (:divconq-list-0-1 (list spec-0 spec-1))
           (:divconq-list-0-1-2 (list spec-0 spec-1 spec-2))
           (:divconq-oset-0-1 (list spec-0 spec-1))
           (t (raise "Internal error: unknown schema ~x0."
                     schema))))
    (??f1...?fp-events
         (schemalg-gen-?f1...?fp schema ?g ?g0 ?g1 ?h x-a1...am))
    (x-z1...zm
         (case schema
           (:divconq-list-0-1
                (schemalg-gen-x-z1...zm x-a1...am x-x1...xn x y))
           (:divconq-list-0-1-2
                (schemalg-gen-x-z1...zm x-a1...am x-x1...xn x y))
           (:divconq-oset-0-1
                (schemalg-gen-x-z1...zm x-a1...am x-x1...xn x y))
           (t (raise "Internal error: unknown schema ~x0."
                     schema))))
    ((mv algo-local-event algo-exported-event)
     (schemalg-gen-algo schema algo algo-enable x-z1...zm
                        x ?g ?g0 ?g1 ?h verify-guards))
    ((mv spec-0-local-event
         spec-0-exported-event)
     (schemalg-gen-spec-0 schema spec-0
                          spec-0-enable old x-x1...xn x-a1...am
                          x iorel ?g ?g0 verify-guards wrld))
    ((mv spec-1-local-event
         spec-1-exported-event)
     (schemalg-gen-spec-1 schema spec-1
                          spec-1-enable old x-x1...xn x-a1...am
                          x y iorel ?g1 ?h verify-guards wrld))
    ((mv spec-2-local-event?
         spec-2-exported-event?)
     (if (eq schema :divconq-list-0-1-2)
         (schemalg-gen-spec-2 schema spec-2
                              spec-2-enable old x-x1...xn x-a1...am
                              x y iorel ?h verify-guards wrld)
       (mv nil nil)))
    (equal-algo-event
         (schemalg-gen-equal-algo equal-algo equal-algo-enable
                                  x-z1...zm ?f algo print))
    ((mv new-local-event new-exported-event)
     (schemalg-gen-new new new-enable
                       spec1...specq equal-algo verify-guards))
    ((mv algo-correct-event algo-correct &)
     (schemalg-gen-algo-correct schema x-x1...xn
                                x-a1...am x y iorel algo spec-0
                                spec-1 spec-2 names-to-avoid wrld))
    ((mv old-if-new-local-event
         old-if-new-exported-event)
     (schemalg-gen-old-if-new old-if-new old-if-new-enable
                              old ?f x-x1...xn x-z1...zm x-a1...am
                              x equal-algo new algo algo-correct))
    (encapsulate-events
     (cons
      '(logic)
      (cons
       '(evmac-prepare-proofs)
       (append
        ?f1...?fp-events
        (cons
         algo-local-event
         (cons
          algo-exported-event
          (cons
           spec-0-local-event
           (cons
            spec-0-exported-event
            (cons
             spec-1-local-event
             (cons
              spec-1-exported-event
              (append
               (and spec-2-local-event?
                    (list spec-2-local-event?))
               (append
                (and spec-2-exported-event?
                     (list spec-2-exported-event?))
                (cons
                 equal-algo-event
                 (cons
                   new-local-event
                   (cons new-exported-event
                         (cons algo-correct-event
                               (cons old-if-new-local-event
                                     (cons old-if-new-exported-event
                                           'nil))))))))))))))))))
    (encapsulate (cons 'encapsulate
                       (cons 'nil encapsulate-events))
)
    ((when show-only)
     (if (member-eq print '(:info :all))
         (cw "~%~x0~|" encapsulate)
       (cw "~x0~|" encapsulate))
     '(value-triple :invisible))
    (encapsulate+ (restore-output? (eq print :all)
                                   encapsulate))
    (transformation-table-event
         (record-transformation-call-event call encapsulate wrld))
    (print-result
     (and
      (member-eq print '(:result :info :all))
      (append
       (and (member-eq print '(:info :all))
            '((cw-event "~%")))
       (cons
        (cons 'cw-event
              (cons '"~x0~|"
                    (cons (cons 'quote
                                (cons algo-exported-event 'nil))
                          'nil)))
        (cons
         (cons 'cw-event
               (cons '"~x0~|"
                     (cons (cons 'quote
                                 (cons spec-0-exported-event 'nil))
                           'nil)))
         (cons
          (cons 'cw-event
                (cons '"~x0~|"
                      (cons (cons 'quote
                                  (cons spec-1-exported-event 'nil))
                            'nil)))
          (cons
           (cons 'cw-event
                 (cons '"~x0~|"
                       (cons (cons 'quote
                                   (cons equal-algo-event 'nil))
                             'nil)))
           (cons
            (cons 'cw-event
                  (cons '"~x0~|"
                        (cons (cons 'quote
                                    (cons new-exported-event 'nil))
                              'nil)))
            (cons
             (cons
              'cw-event
              (cons
                  '"~x0~|"
                  (cons (cons 'quote
                              (cons old-if-new-exported-event 'nil))
                        'nil)))
             'nil))))))))))
   (cons 'progn
         (cons encapsulate+
               (cons transformation-table-event
                     (append print-result
                             '((value-triple :invisible)))))))))