		Search-engine friendly clone of the ACL2 documentation.

Parteval-event-generation

Parteval-gen-new-fn

Generate the new function definition.

Signature
(parteval-gen-new-fn old$ static$ new-name$ new-enable$ verify-guards$ untranslate$ case wrld) → (mv local-event exported-event new-formals)
Arguments: old$ — Guard (symbolp old$).; static$ — Guard (symbol-alistp static$).; new-name$ — Guard (symbolp new-name$).; new-enable$ — Guard (booleanp new-enable$).; verify-guards$ — Guard (booleanp verify-guards$).; untranslate$ — Guard (untranslate-specifier-p untranslate$).; case — Guard (member case '(1 2 3)).; wrld — Guard (plist-worldp wrld).
Returns: local-event — A pseudo-event-formp.; exported-event — A pseudo-event-formp.; new-formals — A symbol-listp.

The macro used to introduce the new function is determined by whether the new function must be enabled or not.

The parameters of the new function are the dynamic parameters of the old function, obtained by removing the static parameters from the old function. The parameters of the new function are returned as one of the results.

The new function is recursive only in case 2. The generated termination hints are as in the design notes and parteval-template.lisp.

The guard of the new function is obtained by replacing each yj with cj in the guard of the old function.

Guard verification is deferred, because in case 2 its proof depends on the old-to-new theorem. It is deferred also for cases 1 and 3, even if that is not necessary, for greater simplicity.

Definitions and Theorems

Function: parteval-gen-new-fn

(defun parteval-gen-new-fn
       (old$ static$ new-name$ new-enable$
             verify-guards$ untranslate$ case wrld)
 (declare (xargs :guard (and (symbolp old$)
                             (symbol-alistp static$)
                             (symbolp new-name$)
                             (booleanp new-enable$)
                             (booleanp verify-guards$)
                             (untranslate-specifier-p untranslate$)
                             (member case '(1 2 3))
                             (plist-worldp wrld))))
 (let ((__function__ 'parteval-gen-new-fn))
  (declare (ignorable __function__))
  (b*
   ((macro (function-intro-macro new-enable$ nil))
    (formals (set-difference-eq (formals old$ wrld)
                                (strip-cars static$)))
    (body
        (parteval-gen-new-fn-body old$ static$ new-name$ case wrld))
    (body (case untranslate$
            (:nice (directed-untranslate (ibody old$ wrld)
                                         (ubody old$ wrld)
                                         body nil nil wrld))
            (:nice-expanded
                 (directed-untranslate-no-lets (ibody old$ wrld)
                                               (ubody old$ wrld)
                                               body nil nil wrld))
            ((nil) body)
            (t (untranslate body nil wrld))))
    (wfrel? (and (= case 2)
                 (well-founded-relation old$ wrld)))
    (measure?
         (and (= case 2)
              (untranslate (fsublis-var static$ (measure old$ wrld))
                           nil wrld)))
    (termination-hints?
     (and
      (= case 2)
      (cons
       (cons
        '"Goal"
        (cons
         ':in-theory
         (cons
          'nil
          (cons
              ':use
              (cons (cons ':instance
                          (cons (cons ':termination-theorem
                                      (cons old$ 'nil))
                                (cons ':extra-bindings-ok
                                      (alist-to-doublets static$))))
                    'nil)))))
       'nil)))
    (guard (fsublis-var static$ (uguard old$ wrld)))
    (guard (untranslate guard nil wrld))
    (local-event
     (cons
      'local
      (cons
       (cons
        macro
        (cons
         new-name$
         (cons
          formals
          (cons
           (cons
            'declare
            (cons
             (cons
                 'xargs
                 (append (and (= case 2)
                              (list :well-founded-relation wfrel?
                                    :measure measure?
                                    :hints termination-hints?
                                    :ruler-extenders :all))
                         (cons ':guard
                               (cons guard '(:verify-guards nil)))))
             'nil))
           (cons body 'nil)))))
       'nil)))
    (exported-event
     (cons
      macro
      (cons
       new-name$
       (cons
        formals
        (cons
         (cons
          'declare
          (cons
           (cons
              'xargs
              (append
                   (and (= case 2)
                        (list :well-founded-relation wfrel?
                              :measure measure?
                              :ruler-extenders :all))
                   (cons ':guard
                         (cons guard
                               (cons ':verify-guards
                                     (cons verify-guards$ 'nil))))))
           'nil))
         (cons body 'nil)))))))
   (mv local-event exported-event formals))))