Ensure that a function, if introduced by `defun-sk`,
has an associated rewrite rule (the one generated by `defun-sk`
that depends on exactly the same function variables
that the function's matrix depends on.

- Signature
(ensure-defun-sk-rule-same-funvars fn ctx state) → (mv erp nothing state)

- Arguments
`fn`—Guard (symbolp fn) .- Returns
`nothing`— Alwaysnil .

We collect
the function variables that the `defun-sk` matrix depends on
and the ones that the `defun-sk` rewrite rule depends on;
we ensure that they are the same function variables.
It seems unlikely that this check will ever fail in practice,
but `defun-sk` allows custom rules (for universal quantifiers)
that might somehow change the dependencies on function variables;
for now we do not support this situation,
but we might recosider this if some compelling example comes up.
Unless the rewrite rule is a custom one,
this check is always expected to pass.

**Function: **

(defun ensure-defun-sk-rule-same-funvars (fn ctx state) (declare (xargs :stobjs (state))) (declare (xargs :guard (symbolp fn))) (let ((__function__ 'ensure-defun-sk-rule-same-funvars)) (declare (ignorable __function__)) (b* ((wrld (w state)) ((unless (defun-sk-p fn wrld)) (value nil)) (rule-name (defun-sk-rewrite-name fn wrld)) (rule-body (formula rule-name nil wrld)) (fn-matrix (defun-sk-matrix fn wrld)) (rule-funvars (funvars-of-term rule-body wrld)) (matrix-funvars (funvars-of-term fn-matrix wrld)) ((when (set-equiv rule-funvars matrix-funvars)) (value nil)) ((unless (eq (defun-sk-rewrite-kind fn wrld) :custom)) (value (raise "Internal error: ~ the DEFUN-SK function ~x0 has a matrix ~x1 that depends on the function variables ~&2 ~ but a non-custom rewrite rule ~x3 that depends on the function variables ~&4. This was not expected to happen." fn fn-matrix matrix-funvars rule-body rule-funvars)))) (er-soft+ ctx t nil "The DEFUN-SK function ~x0 has a matrix ~x1 that depends on the function variables ~&2 ~ but a custom rewrite rule ~x3 that depends on the function variables ~&4." fn fn-matrix matrix-funvars rule-body rule-funvars))))