Implementation of defund-sk.
Even though we delegate most input validation to defun-sk, in order to generate the event to disable the function and the rewrite rules, we need to retrieve some information from the inputs. In doing so, we can assume the inputs to be correct, because if they are not, the generated event will fail at the defun-sk, without reaching the disabling event.
First, we need to find whether
Second, in order to disable the rewrite rule,
we need to find out if there is a
(defun defund-sk-extract-thm-enable (rest) (let ((pos (position-eq :thm-enable rest))) (if (not pos) (mv nil rest) (mv (nth (1+ pos) rest) (append (take pos rest) (nthcdr (+ 2 pos) rest))))))
(defun defund-sk-names-to-disable (name rest-for-defun-sk thm-enable) (mv-let (erp dcls-and-body keyword-alist) (partition-rest-and-keyword-args rest-for-defun-sk *defun-sk-keywords*) (if erp nil (let* ((constrain (cdr (assoc-eq :constrain keyword-alist))) (thm-name (cdr (assoc-eq :thm-name keyword-alist))) (name/defrule (cond ((eq constrain nil) name) ((eq constrain t) (add-suffix name "-DEFINITION")) (t constrain))) (rwrule (or thm-name (let* ((body (car (last dcls-and-body))) (quantifier (car body))) (if (eq quantifier 'forall) (add-suffix name "-NECC") (add-suffix name "-SUFF")))))) (if thm-enable (list name/defrule) (list name/defrule rwrule))))))
(defun defund-sk-fn (name args rest) (mv-let (thm-enable rest-for-defun-sk) (defund-sk-extract-thm-enable rest) (let ((names-to-disable (defund-sk-names-to-disable name rest-for-defun-sk thm-enable))) (cons 'progn (cons (cons 'defun-sk (cons name (cons args rest-for-defun-sk))) (cons (cons 'in-theory (cons (cons 'disable names-to-disable) 'nil)) 'nil))))))