		Search-engine friendly clone of the ACL2 documentation.

Restrict-event-generation

Restrict-gen-new

Generate the new function definition.

Signature
(restrict-gen-new old restriction undefined new new-enable verify-guards wrld) → (mv local-event exported-event new-body)
Arguments: old — Guard (symbolp old).; restriction — Guard (pseudo-termp restriction).; undefined — Guard (pseudo-termp undefined).; new — Guard (symbolp new).; new-enable — Guard (booleanp new-enable).; verify-guards — Guard (booleanp verify-guards).; wrld — Guard (plist-worldp wrld).
Returns: local-event — A pseudo-event-formp.; exported-event — A pseudo-event-formp.; new-body — A pseudo-termp.

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.

The body of the new function is obtained from the body of the old function by replacing every occurrence of the old function with the new function (a no-op if the old function is not recursive), and then wrapping the resulting term with a conditional that tests the restricting predicate, as described in the documentation. Thus, the new function is recursive iff the old function is. If the old function is non-executable, the non-executable wrapper is removed first.

If the new function is recursive, its well-founded relation and measure are the same as the old function's. Following the design notes, the termination of the new function is proved in the empty theory, using the termination theorem of the old function; this should work also if the function is reflexive, because of the automatic functional instantiation described in (6) of the lemma instance documentation. The new function uses all ruler extenders, in case the old function's termination depends on any ruler extender.

The guard of the new function is obtained by conjoining the restricting predicate after the guard of the old function, as described in the documentation. Since the restriction test follows from the guard, it is wrapped with mbt$.

Guard verification is deferred; see restrict-gen-verify-guards.

Definitions and Theorems

Function: restrict-gen-new

(defun restrict-gen-new (old restriction undefined
                             new new-enable verify-guards wrld)
 (declare (xargs :guard (and (symbolp old)
                             (pseudo-termp restriction)
                             (pseudo-termp undefined)
                             (symbolp new)
                             (booleanp new-enable)
                             (booleanp verify-guards)
                             (plist-worldp wrld))))
 (let ((__function__ 'restrict-gen-new))
  (declare (ignorable __function__))
  (b*
   ((macro
       (function-intro-macro new-enable (non-executablep old wrld)))
    (formals (formals old wrld))
    (old-body (if (non-executablep old wrld)
                  (unwrapped-nonexec-body old wrld)
                (ubody old wrld)))
    (new-body-core (sublis-fn-simple (acons old new nil)
                                     old-body))
    (new-body
         (cons 'if
               (cons (cons 'mbt$ (cons restriction 'nil))
                     (cons new-body-core (cons undefined 'nil)))))
    (new-body (untranslate new-body nil wrld))
    (recursive (recursivep old nil wrld))
    (wfrel? (and recursive
                 (well-founded-relation old wrld)))
    (measure? (and recursive
                   (untranslate (measure old wrld)
                                nil wrld)))
    (termination-hints?
     (and
      recursive
      (cons
           (cons '"Goal"
                 (cons ':in-theory
                       (cons 'nil
                             (cons ':use
                                   (cons (cons ':termination-theorem
                                               (cons old 'nil))
                                         'nil)))))
           'nil)))
    (old-guard (guard old nil wrld))
    (new-guard (if (equal old-guard restriction)
                   old-guard
                 (conjoin2 old-guard restriction)))
    (new-guard (untranslate new-guard t wrld))
    (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 new-guard '(:verify-guards nil)))))
             'nil))
           (cons new-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 new-guard
                                (cons ':verify-guards
                                      (cons verify-guards 'nil))))))
           'nil))
         (cons new-body 'nil)))))))
   (mv local-event exported-event new-body))))