		Search-engine friendly clone of the ACL2 documentation.

Defarbrec-event-generation

Defarbrec-gen-everything

Generate the top-level event.

Signature
(defarbrec-gen-everything fn$ x1...xn$ body$ test updates update-names$ terminates-name$ terminates-witness-name$ terminates-rewrite-name$ measure-name$ nonterminating$ print$ show-only$ call wrld) → event
Arguments: fn$ — Guard (symbolp fn$).; x1...xn$ — Guard (symbol-listp x1...xn$).; body$ — Guard (pseudo-termp body$).; test — Guard (pseudo-termp test).; updates — Guard (pseudo-term-listp updates).; update-names$ — Guard (symbol-listp update-names$).; terminates-name$ — Guard (symbolp terminates-name$).; terminates-witness-name$ — Guard (symbolp terminates-witness-name$).; terminates-rewrite-name$ — Guard (symbolp terminates-rewrite-name$).; measure-name$ — Guard (symbolp measure-name$).; nonterminating$ — Guard (pseudo-termp nonterminating$).; print$ — Guard (defarbrec-printp print$).; show-only$ — Guard (booleanp show-only$).; call — Guard (pseudo-event-formp call).; wrld — Guard (plist-worldp wrld).
Returns: event — A pseudo-event-formp.

This is a progn that consists of the expansion of defarbrec (the encapsulate), followed by an event to extend the defarbrec table, optionally followed by events to print the exported functions (if specified by the :print input). The progn ends with :invisible to avoid printing a return value.

The expansion starts with some implicitly local events to ensure logic mode, avoid errors due to ignored or irrelevant formals in the generated functions, and prevent default and override hints from sabotaging the generated proofs. Then all the local and exported function and lemma events are introduced. The names-to-avoid variable is initialized with the names of the exported events and extended as local names are generated.

If the :print input is :all, the expansion is wrapped to show ACL2's output in response to the submitted events. In this case, a blank line is printed before printing the result, for visual separation.

If :show-only is t, the expansion is printed on the screen and not returned as part of the event to submit, which is in this case is just an :invisible form.

Definitions and Theorems

Function: defarbrec-gen-everything

(defun defarbrec-gen-everything
       (fn$ x1...xn$ body$ test
            updates update-names$ terminates-name$
            terminates-witness-name$
            terminates-rewrite-name$
            measure-name$ nonterminating$
            print$ show-only$ call wrld)
 (declare (xargs :guard (and (symbolp fn$)
                             (symbol-listp x1...xn$)
                             (pseudo-termp body$)
                             (pseudo-termp test)
                             (pseudo-term-listp updates)
                             (symbol-listp update-names$)
                             (symbolp terminates-name$)
                             (symbolp terminates-witness-name$)
                             (symbolp terminates-rewrite-name$)
                             (symbolp measure-name$)
                             (pseudo-termp nonterminating$)
                             (defarbrec-printp print$)
                             (booleanp show-only$)
                             (pseudo-event-formp call)
                             (plist-worldp wrld))))
 (let ((__function__ 'defarbrec-gen-everything))
  (declare (ignorable __function__))
  (b*
   ((names-to-avoid
         (cons fn$
               (append update-names$
                       '(terminates-name$ terminates-witness-name$
                                          terminates-rewrite-name$
                                          measure-name$))))
    (k (defarbrec-gen-var-k fn$ x1...xn$))
    (l (defarbrec-gen-var-l fn$ x1...xn$ k))
    ((mv local-update-fns exported-update-fns)
     (defarbrec-gen-update-fns
          x1...xn$ updates update-names$ k wrld))
    ((mv update-fns-lemma update-fns-lemma-name)
     (defarbrec-gen-update-fns-lemma
          fn$ x1...xn$ test
          update-names$ k names-to-avoid wrld))
    (names-to-avoid (cons update-fns-lemma-name names-to-avoid))
    (terminates-fn (defarbrec-gen-terminates-fn
                        x1...xn$
                        test update-names$ terminates-name$
                        terminates-witness-name$
                        terminates-rewrite-name$ k wrld))
    ((mv local-measure-fn exported-measure-fn)
     (defarbrec-gen-measure-fn
          x1...xn$ test
          update-names$ terminates-witness-name$
          measure-name$ k wrld))
    ((mv measure-fn-natp-lemma
         measure-fn-natp-lemma-name)
     (defarbrec-gen-measure-fn-natp-lemma
          x1...xn$
          measure-name$ k names-to-avoid wrld))
    (names-to-avoid (cons measure-fn-natp-lemma-name
                          names-to-avoid))
    ((mv measure-fn-end-lemma
         measure-fn-end-lemma-name)
     (defarbrec-gen-measure-fn-end-lemma
          x1...xn$
          test update-names$ terminates-name$
          terminates-witness-name$
          measure-name$ k update-fns-lemma-name
          names-to-avoid wrld))
    (names-to-avoid (cons measure-fn-end-lemma-name
                          names-to-avoid))
    ((mv measure-fn-min-lemma
         measure-fn-min-lemma-name)
     (defarbrec-gen-measure-fn-min-lemma
          x1...xn$ test update-names$
          measure-name$ k l names-to-avoid wrld))
    ((mv local-fn-fn exported-fn-fn)
     (defarbrec-gen-fn-fn fn$ x1...xn$ body$
                          updates update-names$ terminates-name$
                          measure-name$ nonterminating$
                          k l measure-fn-natp-lemma-name
                          measure-fn-end-lemma-name
                          measure-fn-min-lemma-name wrld))
    (expansion
     (cons
      'encapsulate
      (cons
       'nil
       (cons
        '(logic)
        (cons
         '(set-ignore-ok t)
         (cons
          '(set-irrelevant-formals-ok t)
          (cons
           '(evmac-prepare-proofs)
           (append
            local-update-fns
            (append
             exported-update-fns
             (cons
              update-fns-lemma
              (cons
               terminates-fn
               (cons
                local-measure-fn
                (cons
                 exported-measure-fn
                 (cons
                  measure-fn-natp-lemma
                  (cons
                   measure-fn-end-lemma
                   (cons
                    measure-fn-min-lemma
                    (cons
                         local-fn-fn
                         (cons exported-fn-fn 'nil))))))))))))))))))
    ((when show-only$)
     (cw "~x0~|" expansion)
     '(value-triple :invisible))
    (expansion-output-p (if (eq print$ :all) t nil))
    (expansion+ (restore-output? expansion-output-p expansion))
    (call$ (defarbrec-filter-call call))
    (extend-table (defarbrec-gen-extend-table
                       fn$ x1...xn$
                       body$ update-names$ terminates-name$
                       measure-name$ call$ expansion))
    (print-result
     (and
      (member-eq print$ '(:result :all))
      (append
         (and expansion-output-p '((cw-event "~%")))
         (defarbrec-gen-print-result
              (append exported-update-fns
                      (cons terminates-fn
                            (cons exported-measure-fn
                                  (cons exported-fn-fn 'nil)))))))))
   (cons 'progn
         (cons expansion+
               (cons extend-table
                     (append print-result
                             '((value-triple :invisible)))))))))