/usr/share/acl2-7.2dfsg/books/misc/sticky-disable.lisp is in acl2-books-source 7.2dfsg-3.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 | ; Copyright (C) 2013, Regents of the University of Texas
; Written by Matt Kaufmann, 12/13/05
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
(in-package "ACL2")
; Sticky disabling and enabling, implementing an idea suggested by Ray
; Richards by using tables.
; This book introduces the following macros:
; (sticky-disable name1 name2 ...):
; Disables the indicated names, and makes a note that they are to be
; disabled after any call of sticky-include-book.
; (sticky-enable name1 name2 ...):
; Enables the indicated names, and makes a note that they are to be
; enabled after any call of sticky-include-book.
; (sticky-include-book "book-name" ...):
; Exactly the same as include-book, except for the extra disabling and enabling
; noted above.
(program)
(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))
(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))))
(defmacro sticky-disable (&rest fns)
`(progn (in-theory (disable ,@fns))
,@(list-of-add-sticky-calls fns t)))
(defmacro sticky-enable (&rest fns)
`(progn (in-theory (enable ,@fns))
,@(list-of-add-sticky-calls fns nil)))
(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)))))
(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))))
(defun get-sticky-enables (world)
(get-sticky-enables-1 (table-alist 'sticky-disables world) nil))
(defun get-sticky-disables (world)
(get-sticky-disables-1 (table-alist 'sticky-disables world) nil))
(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)))))
|