		Search-engine friendly clone of the ACL2 documentation.

Solve-event-generation

Solve-gen-everything

Generate the top-level event.

Signature
(solve-gen-everything old ?f x1...xn matrix method method-rules f f-existsp solution-enable solution-guard solution-guard-hints solution-body solution-hints new new-enable old-if-new old-if-new-enable verify-guards print show-only call names-to-avoid ctx state) → (mv erp event state)
Arguments: old — Guard (symbolp old).; ?f — Guard (symbolp ?f).; x1...xn — Guard (symbol-listp x1...xn).; matrix — Guard (pseudo-termp matrix).; method — Guard (keywordp method).; method-rules — Guard (symbol-listp method-rules).; f — Guard (symbolp f).; f-existsp — Guard (booleanp f-existsp).; solution-enable — Guard (booleanp solution-enable).; solution-guard — An untranslated term.; solution-guard-hints — Guard (true-listp solution-guard-hints).; solution-body — An untranslated term.; solution-hints — Guard (true-listp solution-hints).; 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).
Returns: event — A pseudo-event-formp.

Definitions and Theorems

Function: solve-gen-everything

(defun solve-gen-everything
       (old ?f x1...xn matrix method method-rules f
            f-existsp solution-enable solution-guard
            solution-guard-hints solution-body
            solution-hints new new-enable old-if-new
            old-if-new-enable verify-guards print
            show-only call names-to-avoid ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp old)
                             (symbolp ?f)
                             (symbol-listp x1...xn)
                             (pseudo-termp matrix)
                             (keywordp method)
                             (symbol-listp method-rules)
                             (symbolp f)
                             (booleanp f-existsp)
                             (booleanp solution-enable)
                             (true-listp solution-guard-hints)
                             (true-listp solution-hints)
                             (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))))
 (let ((__function__ 'solve-gen-everything))
  (declare (ignorable __function__))
  (b*
   ((wrld (w state))
    ((er (list solution-local-events
               solution-exported-events
               solution-theorem old-instance &))
     (solve-gen-solution old
                         ?f x1...xn matrix method method-rules f
                         f-existsp solution-enable solution-guard
                         solution-guard-hints solution-body
                         solution-hints verify-guards
                         print names-to-avoid ctx state))
    (new-event (solve-gen-new new new-enable
                              x1...xn ?f f verify-guards print))
    ((mv old-if-new-local-event
         old-if-new-exported-event)
     (solve-gen-old-if-new old-if-new
                           old-if-new-enable old ?f x1...xn
                           new f solution-theorem old-instance))
    (encapsulate-events
     (cons
      '(logic)
      (cons
       '(evmac-prepare-proofs)
       (cons
        '(set-ignore-ok t)
        (cons
         '(set-irrelevant-formals-ok t)
         (append
          solution-local-events
          (append
           solution-exported-events
           (cons
                new-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 '(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 "~%")))
       (append
        (and
         (not f-existsp)
         (cons
          (cons
              'cw-event
              (cons '"~x0~|"
                    (cons (cons 'quote
                                (cons (car solution-exported-events)
                                      'nil))
                          'nil)))
          'nil))
        (cons
         (cons 'cw-event
               (cons '"~x0~|"
                     (cons (cons 'quote (cons new-event 'nil))
                           'nil)))
         (cons
          (cons
            'cw-event
            (cons '"~x0~|"
                  (cons (cons 'quote
                              (cons old-if-new-exported-event 'nil))
                        'nil)))
          'nil)))))))
   (value
      (cons 'progn
            (cons encapsulate+
                  (cons transformation-table-event
                        (append print-result
                                '((value-triple :invisible))))))))))