		Search-engine friendly clone of the ACL2 documentation.

Isodata-event-generation

Isodata-gen-new-fn

Generate the new function definition.

Signature
(isodata-gen-new-fn old$ arg-isomaps res-isomaps xform-stobjs-p predicate$ undefined$ new$ new-enable$ verify-guards$ untranslate$ compatibility appcond-thm-names wrld) → (mv new-fn-local-event new-fn-exported-event)
Arguments: old$ — Guard (symbolp old$).; arg-isomaps — Guard (isodata-symbol-isomap-alistp arg-isomaps).; res-isomaps — Guard (isodata-pos-isomap-alistp res-isomaps).; xform-stobjs-p — Guard (booleanp xform-stobjs-p).; predicate$ — Guard (booleanp predicate$).; undefined$ — Either :base-case-then, :base-case-else, or a pseudo-termp.; 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 or some stobjs are transformed.

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 isodata-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: isodata-gen-new-fn

(defun isodata-gen-new-fn
       (old$ arg-isomaps res-isomaps xform-stobjs-p
             predicate$ undefined$ new$
             new-enable$ verify-guards$ untranslate$
             compatibility appcond-thm-names wrld)
 (declare
      (xargs :guard (and (symbolp old$)
                         (isodata-symbol-isomap-alistp arg-isomaps)
                         (isodata-pos-isomap-alistp res-isomaps)
                         (booleanp xform-stobjs-p)
                         (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__ 'isodata-gen-new-fn))
  (declare (ignorable __function__))
  (b*
   ((non-executablep (or (non-executablep old$ wrld)
                         xform-stobjs-p))
    (macro (function-intro-macro new-enable$ non-executablep))
    (formals (formals old$ wrld))
    (body (isodata-gen-new-fn-body
               old$ arg-isomaps res-isomaps predicate$
               undefined$ new$ compatibility 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
         (isodata-gen-new-fn-guard old$ arg-isomaps
                                   xform-stobjs-p predicate$ wrld))
    (guard (conjoin (flatten-ands-in-lit guard)))
    (guard (untranslate guard nil wrld))
    (recursive (recursivep old$ nil wrld))
    (wfrel? (if recursive (get-well-founded-relation old$ wrld)
              nil))
    (measure? (if recursive
                  (isodata-gen-new-fn-measure old$ arg-isomaps wrld)
                nil))
    (termination-hints?
         (if recursive (isodata-gen-new-fn-termination-hints
                            appcond-thm-names old$ arg-isomaps 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))))