		Search-engine friendly clone of the ACL2 documentation.

Expdata-event-generation

Expdata-gen-new-fn

Generate the new function definition.

Signature
(expdata-gen-new-fn old$ arg-surjmaps res-surjmaps predicate$ new$ new-enable$ verify-guards$ untranslate$ appcond-thm-names wrld) → (mv new-fn-local-event new-fn-exported-event)
Arguments: old$ — Guard (symbolp old$).; arg-surjmaps — Guard (expdata-symbol-surjmap-alistp arg-surjmaps).; res-surjmaps — Guard (expdata-pos-surjmap-alistp res-surjmaps).; predicate$ — Guard (booleanp predicate$).; new$ — Guard (symbolp new$).; new-enable$ — Guard (booleanp new-enable$).; verify-guards$ — Guard (booleanp verify-guards$).; untranslate$ — Guard (untranslate-specifier-p untranslate$).; appcond-thm-names — Guard (symbol-symbol-alistp appcond-thm-names).; wrld — Guard (plist-worldp wrld).
Returns: new-fn-local-event — A pseudo-event-formp.; new-fn-exported-event — A pseudo-event-formp.

The macro used to introduce the new function is determined by whether the new function must be enabled or not, and non-executable or not. We make it non-executable if and only if old is non-executable.

The new function has the same formal arguments as the old function.

If the new function is recursive, its well-founded relation is the same as the old function's. The new function uses all ruler extenders, in case the old function's termination depends on any ruler extender.

Guard verification is deferred; see expdata-gen-new-fn-verify-guards.

If the old function returns a multi-value result, we adjust the body of the new function to do the same.

Definitions and Theorems

Function: expdata-gen-new-fn

(defun expdata-gen-new-fn (old$ arg-surjmaps res-surjmaps predicate$
                                new$ new-enable$ verify-guards$
                                untranslate$ appcond-thm-names wrld)
 (declare
     (xargs :guard (and (symbolp old$)
                        (expdata-symbol-surjmap-alistp arg-surjmaps)
                        (expdata-pos-surjmap-alistp res-surjmaps)
                        (booleanp predicate$)
                        (symbolp new$)
                        (booleanp new-enable$)
                        (booleanp verify-guards$)
                        (untranslate-specifier-p untranslate$)
                        (symbol-symbol-alistp appcond-thm-names)
                        (plist-worldp wrld))))
 (let ((__function__ 'expdata-gen-new-fn))
  (declare (ignorable __function__))
  (b*
   ((macro (function-intro-macro new-enable$
                                 (non-executablep old$ wrld)))
    (formals (formals old$ wrld))
    (body
        (expdata-gen-new-fn-body old$ arg-surjmaps
                                 res-surjmaps predicate$ new$ wrld))
    (body (if (> (number-of-results old$ wrld) 1)
              (mvify body)
            body))
    (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))))
    (guard
       (expdata-gen-new-fn-guard old$ arg-surjmaps predicate$ wrld))
    (guard (conjoin (flatten-ands-in-lit guard)))
    (guard (untranslate guard nil wrld))
    (recursive (recursivep old$ nil wrld))
    (wfrel? (if recursive (well-founded-relation old$ wrld)
              nil))
    (measure?
         (if recursive
             (expdata-gen-new-fn-measure old$ arg-surjmaps wrld)
           nil))
    (termination-hints?
      (if recursive
       (expdata-gen-new-fn-termination-hints appcond-thm-names
                                             old$ arg-surjmaps wrld)
       nil))
    (local-event
     (cons
      'local
      (cons
       (cons
        macro
        (cons
         new$
         (cons
          formals
          (cons
           (cons
            'declare
            (cons
             (cons
                 'xargs
                 (append (and recursive
                              (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$
       (cons
        formals
        (cons
         (cons
          'declare
          (cons
           (cons
              'xargs
              (append
                   (and recursive
                        (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))))