Generate a list of events to submit, when instantiating a plain second-order function.
(defun-inst-plain-events fun sofun inst options ctx state) → (mv erp events+result+funvars state)
Also return the defun2 or defun event form,
without the termination hints.
This is printed when
Also return the function variables that the new function depends on.
Only the
We add
If
Function:
(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)))))