/usr/share/acl2-4.3/books/wp-gen/shared.lisp is in acl2-books-source 4.3-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 | (in-package "ACL2")
;; Some shared functions
;; Recursively collect the list of unique variables (symbols) used in
;; a term or list of terms
(mutual-recursion
(defun collect-vars (q)
(if (atom q)
(if (symbolp q)
(if (and (not (equal q nil)) (not (equal q t)))
(list q)
nil)
nil)
(collect-vars-list (cdr q)))) ;; collect vars from the list of args
(defun collect-vars-list (q-list)
(if (atom q-list) nil
(let ((car-syms (collect-vars (car q-list))))
(if car-syms (union-equal car-syms (collect-vars-list (cdr q-list)))
(collect-vars-list (cdr q-list))))))
)
;; Return the list of keys from an alist
(defun get-alist-keys (al)
(if (atom al)
nil
(cons (caar al)
(get-alist-keys (cdr al)))))
;; Return the list of vals from an alist
(defun get-alist-vals (al)
(if (atom al)
nil
(cons (cdar al)
(get-alist-vals (cdr al)))))
|