/usr/share/acl2-6.5/books/misc/find-lemmas.lisp is in acl2-books-source 6.5-2.
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 71 72 | ; Copyright (C) 2013, Regents of the University of Texas
; Written by Matt Kaufmann
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
(in-package "ACL2")
(program)
(defun deref-macro-name-list (fns macro-aliases)
(if (endp fns)
nil
(cons (deref-macro-name (car fns) macro-aliases)
(deref-macro-name-list (cdr fns) macro-aliases))))
(defun find-lemmas-fn (fns omit-boot-strap acc wrld-tail wrld)
(declare (xargs :mode :program))
(let ((fns (deref-macro-name-list fns (macro-aliases wrld))))
(if (or (endp wrld-tail)
(and omit-boot-strap
(and (eq (caar wrld-tail) 'command-landmark)
(eq (cadar wrld-tail) 'global-value)
(equal (access-command-tuple-form (cddar wrld-tail))
'(exit-boot-strap-mode)))))
acc
(let* ((trip (car wrld-tail))
(ev-tuple (and (consp trip)
(eq (car trip) 'event-landmark)
(eq (cadr trip) 'global-value)
(cddr trip)))
(type (and ev-tuple (access-event-tuple-type ev-tuple)))
(namex (and type (access-event-tuple-namex ev-tuple)))
(formula (and namex
(symbolp namex)
(member-eq type '(defthm defaxiom defchoose))
(formula namex t wrld))))
(if (and formula
(subsetp-eq fns (all-fnnames formula)))
(find-lemmas-fn fns omit-boot-strap
(cons (access-event-tuple-form ev-tuple) acc)
(cdr wrld-tail)
wrld)
(find-lemmas-fn fns omit-boot-strap acc (cdr wrld-tail) wrld))))))
(defmacro find-lemmas (fns &optional (omit-boot-strap 't))
(declare (xargs :guard (let ((fns (if (and (true-listp fns)
(eq (car fns) 'quote)
(eql (length fns) 2))
(cadr fns)
fns)))
(or (symbolp fns)
(symbol-listp fns)))))
; (find-lemmas (fn1 fn2 ...)) returns all lemmas in which all of the indicated
; function symbols occur, except those lemmas in the ground-zero world. In
; order to include those as well, give a second argument of nil:
; (find-lemmas (fn1 fn2 ...) nil).
; If fns is a symbol, then fns is replaced by (list fns).
(let ((fns (if (and (true-listp fns)
(eq (car fns) 'quote)
(eql (length fns) 2))
(cadr fns)
fns)))
(let ((fns (cond
((symbolp fns) (list fns))
((symbol-listp fns) fns)
(t (er hard 'find-lemmas
"The first argument to find-lemmas must be a symbol or ~
a list of symbols, but ~x0 is not."
fns)))))
`(find-lemmas-fn ',fns ',omit-boot-strap nil (w state) (w state)))))
|