		Search-engine friendly clone of the ACL2 documentation.

Defsoft-implementation

Ensure-defun-sk-rule-same-funvars

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 — Always nil.

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.

Definitions and Theorems

Function: ensure-defun-sk-rule-same-funvars

(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))))