		Search-engine friendly clone of the ACL2 documentation.

Defun-inst-implementation

Defun-inst-plain-events

Generate a list of events to submit, when instantiating a plain second-order function.

Signature
(defun-inst-plain-events fun sofun inst options ctx state) → (mv erp events+result+funvars state)
Arguments: fun — Guard (symbolp fun).; sofun — Guard (plain-sofunp sofun (w state)).; options — Guard (keyword-value-listp options).; ctx — Context for errors.
Returns: erp — booleanp flag of the error triple.; events+result+funvars — A tuple (events result funvars) where events is a pseudo-event-form-listp, result is a maybe-pseudo-event-formp, and funvars is a funvar-listp.

Also return the defun2 or defun event form, without the termination hints. This is printed when :print is :result.

Also return the function variables that the new function depends on.

Only the :verify-guards, :enable, and :print options may be present.

We add fun to the table of second-order functions iff it is second-order.

If sofun (and consequently fun) is recursive, we extend the instantiation with (sofun . fun), to ensure that the recursive calls are properly transformed.

Definitions and Theorems

Function: defun-inst-plain-events

(defun defun-inst-plain-events (fun sofun inst options ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp fun)
                             (keyword-value-listp options)
                             (plain-sofunp sofun (w state)))))
 (let ((__function__ 'defun-inst-plain-events))
  (declare (ignorable __function__))
  (b*
   ((wrld (w state))
    ((unless (subsetp (evens options)
                      '(:verify-guards :enable :print)))
     (er-soft+
      ctx t nil
      "Only the input keywords ~
                   :VERIFY-GUARDS, :ENABLE, and :PRINT are allowed, ~
                   because ~x0 is a plain second-order function."
      sofun))
    (verify-guards
         (let ((verify-guards-option
                    (assoc-keyword :verify-guards options)))
           (if verify-guards-option (cadr verify-guards-option)
             (guard-verified-p sofun wrld))))
    (enable (let ((enable-option (assoc-keyword :enable options)))
              (if enable-option (cadr enable-option)
                (fundef-enabledp sofun state))))
    (sofun-body (ubody sofun wrld))
    (sofun-measure (if (recursivep sofun nil wrld)
                       (measure sofun wrld)
                     nil))
    (sofun-guard (uguard sofun wrld))
    (fsbs (if sofun-measure (acons sofun fun inst)
            inst))
    (fun-body (fun-subst-term fsbs sofun-body wrld))
    (fun-body-funvars (funvars-of-term fun-body wrld))
    (fun-body (untranslate fun-body nil wrld))
    (fun-measure (fun-subst-term inst sofun-measure wrld))
    (fun-measure-funvars (funvars-of-term fun-measure wrld))
    (fun-measure (untranslate fun-measure nil wrld))
    (fun-guard (fun-subst-term inst sofun-guard wrld))
    (fun-guard-funvars (funvars-of-term fun-guard wrld))
    (fun-guard (untranslate fun-guard t wrld))
    (sofun-tt-name (cons ':termination-theorem
                         (cons sofun 'nil)))
    (sofun-tt-formula (and (recursivep sofun nil wrld)
                           (termination-theorem sofun wrld)))
    (fsbs (ext-fun-subst-term sofun-tt-formula inst wrld))
    (fun-tt-proof (sothm-inst-proof sofun-tt-name fsbs wrld))
    (hints (if fun-measure
               (cons ':hints
                     (cons (cons (cons '"Goal" fun-tt-proof) 'nil)
                           'nil))
             nil))
    (measure
         (if fun-measure (cons ':measure (cons fun-measure 'nil))
           nil))
    (formals (formals sofun wrld))
    (funvars (remove-duplicates
                  (append fun-body-funvars
                          fun-measure-funvars fun-guard-funvars)))
    (defun-event
     (cons
      'defun
      (cons
       fun
       (cons
        formals
        (cons
         (cons
          'declare
          (cons
           (cons 'xargs
                 (cons ':guard
                       (cons fun-guard
                             (cons ':verify-guards
                                   (cons verify-guards
                                         (append measure hints))))))
           'nil))
         (cons fun-body 'nil))))))
    (result
     (cons
      (if funvars 'defun2 'defun)
      (cons
       fun
       (cons
        formals
        (cons
         (cons
          'declare
          (cons
            (cons 'xargs
                  (cons ':guard
                        (cons fun-guard
                              (cons ':verify-guards
                                    (cons verify-guards measure)))))
            'nil))
         (cons fun-body 'nil))))))
    (disable-event?
         (if enable nil
           (cons (cons 'in-theory
                       (cons (cons 'disable (cons fun 'nil))
                             'nil))
                 'nil)))
    (table-event?
     (if funvars
      (cons
           (cons 'table
                 (cons 'second-order-functions
                       (cons (cons 'quote (cons fun 'nil))
                             (cons (cons 'quote (cons funvars 'nil))
                                   'nil))))
           'nil)
      nil)))
   (value (list (cons defun-event
                      (append disable-event? table-event?))
                result funvars)))))