		Search-engine friendly clone of the ACL2 documentation.

Defund-sk

Defund-sk-implementation

Implementation of defund-sk.

We extract the :thm-enable input, if any, and we validate it. We pass the remaining inputs to defun-sk unchanged, and let defun-sk catch all the errors on those inputs.

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 :constrain is nil (which is also the default), t, or another symbol. If it is nil, we disable the name of the function. Otherwise, we disable the definition rule, whose name is determined by the value of :constrain: if t, the name of the rule is the function name followed by -definition; otherwise, its value is the name of the definition rule.

Second, in order to disable the rewrite rule, we need to find out if there is a :thm-name option. If there is, and its value is not nil, that is the name of the rule to disable. If there is no :thm-name option or its value is nil, then we need to find the quantifier (universal or existential) in order to determine the rule name. If the quantifier is universal, the rule name is obtained by adding -necc after the function name; if the quantifier is existential, the rule name is obtained by adding -suff after the function name.

Definitions and Theorems

Function: defund-sk-extract-thm-enable

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

Function: defund-sk-names-to-disable

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

Function: defund-sk-fn

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