sticky-disable - ACL2 Book

other

(in-package "ACL2")

other

(program)

add-stickymacro

(defmacro add-sticky
  (fn &optional (disablep 't))
  (declare (xargs :guard (symbolp fn)))
  `(table sticky-disables
    nil
    (put-assoc-eq ',FN
      ,DISABLEP
      (table-alist 'sticky-disables world))
    :clear))

list-of-add-sticky-callsfunction

(defun list-of-add-sticky-calls
  (fns flg)
  (if (endp fns)
    nil
    (cons `(add-sticky ,(CAR FNS) ,FLG)
      (list-of-add-sticky-calls (cdr fns) flg))))

sticky-disablemacro

(defmacro sticky-disable
  (&rest fns)
  `(progn (in-theory (disable ,@FNS))
    ,@(LIST-OF-ADD-STICKY-CALLS FNS T)))

sticky-enablemacro

(defmacro sticky-enable
  (&rest fns)
  `(progn (in-theory (enable ,@FNS))
    ,@(LIST-OF-ADD-STICKY-CALLS FNS NIL)))

get-sticky-enables-1function

(defun get-sticky-enables-1
  (alist acc)
  (cond ((endp alist) acc)
    ((cdar alist) (get-sticky-enables-1 (cdr alist) acc))
    (t (get-sticky-enables-1 (cdr alist) (cons (caar alist) acc)))))

get-sticky-disables-1function

(defun get-sticky-disables-1
  (alist acc)
  (cond ((endp alist) acc)
    ((cdar alist) (get-sticky-disables-1 (cdr alist) (cons (caar alist) acc)))
    (t (get-sticky-disables-1 (cdr alist) acc))))

get-sticky-enablesfunction

(defun get-sticky-enables
  (world)
  (get-sticky-enables-1 (table-alist 'sticky-disables world)
    nil))

get-sticky-disablesfunction

(defun get-sticky-disables
  (world)
  (get-sticky-disables-1 (table-alist 'sticky-disables world)
    nil))

sticky-include-bookmacro

(defmacro sticky-include-book
  (&rest args)
  `(progn (include-book ,@ARGS)
    (in-theory (set-difference-theories (union-theories (current-theory :here)
          (get-sticky-enables world))
        (get-sticky-disables world)))))