Generate the event submitted by `defsoft`.

- Signature
(defsoft-fn fn ctx state) → (mv erp event state)

The `defsoft` macro records an ACL2 function
as a (SOFT) second-order function.
This macro will become the primary one
to introduce second-order functions,
and `defun2`, `defchoose2`, and `defun-sk2`
will be redefined as `defun`, `defchoose`, and `defun-sk`
followed by `defsoft`.

The input `defchoose`,
or otherwise is introduced by `defun-sk`,
or otherwise has an unnormalized body
(which implies that is is introduced by `defun`).
Note that `defun-sk` functions
are internally introduced by `defun`,
so it is important to check for `defun-sk` first.
Functions introduced by `defun` but without an unnormalized body
(such as the built-in program-mode functions)
are disallowed because we cannot calculate
the function variables that such functions depend on.
For the same reason,
constrained functions introduced by `encapsulate` are disallowed.

We collect the function variables that the function depends on,
directly or indirecty; there must be at least one.
If the function is introduced by `defun-sk`,
we also ensure that the associated rewrite rule
does not depend on additional function variables.
If the function is recursive,
we also ensure that the well-founded relation is `o<`.

We print on screen an observation about the function being recorded
and which function variables it depends on.
This can be suppressed
(e.g. when generating `defsoft` events programmatically)
via

**Function: **

(defun defsoft-fn (fn ctx state) (declare (xargs :stobjs (state))) (declare (xargs :guard t)) (let ((__function__ 'defsoft-fn)) (declare (ignorable __function__)) (b* ((wrld (w state)) ((unless (symbolp fn)) (er-soft+ ctx t nil "The input must be a symbol, but it is ~x0 instead." fn)) ((unless (function-symbolp fn wrld)) (er-soft+ ctx t nil "The symbol ~x0 must be a function symbol, ~ but it is not." fn)) ((unless (or (defchoosep fn wrld) (defun-sk-p fn wrld) (ubody fn wrld))) (er-soft+ ctx t nil "The function ~x0 must ~ be introduced by DEFCHOOSE, ~ be introduced by DEFUN-SK, ~ or have a non-NIL unnormalized body." fn)) (funvars (cond ((defchoosep fn wrld) (funvars-of-choice-fn fn wrld)) ((defun-sk-p fn wrld) (funvars-of-quantifier-fn fn wrld)) (t (funvars-of-plain-fn fn wrld)))) (funvars (remove-duplicates-eq funvars)) ((unless (consp funvars)) (er-soft+ ctx t nil "The function ~x0 is not second-order: it depends on no function variables, directly or indirectly." fn)) (table-event (cons 'table (cons 'second-order-functions (cons (cons 'quote (cons fn 'nil)) (cons (cons 'quote (cons funvars 'nil)) 'nil))))) ((er &) (ensure-wfrel-o< fn ctx state)) ((er &) (ensure-defun-sk-rule-same-funvars fn ctx state)) (state (acl2::io? observation nil state (fn funvars) (fms "SOFT: ~ recorded ~x0 as a second-order function ~ that depends on the function variables ~x1.~%" (list (cons #\0 fn) (cons #\1 (acl2::sort-symbol-listp funvars))) *standard-co* state nil)))) (value (cons 'progn (cons table-event (cons (cons 'value-triple (cons (cons 'quote (cons fn 'nil)) 'nil)) 'nil)))))))