/usr/share/acl2-6.3/books/tools/pack.lisp is in acl2-books-source 6.3-5.
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 | (in-package "ACL2")
(mutual-recursion
(defun pack-list (args)
(declare (xargs :measure (acl2-count args)
:guard t
:verify-guards nil))
(if (atom args)
nil
(if (atom (cdr args))
(pack-tree (car args))
(append (pack-tree (car args))
(cons #\Space
(pack-list (cdr args)))))))
(defun pack-tree (tree)
(declare (xargs :measure (acl2-count tree)
:guard t))
(if (atom tree)
(if (or (acl2-numberp tree)
(characterp tree)
(stringp tree)
(symbolp tree))
(explode-atom tree 10)
'(#\Space))
(append (cons #\( (pack-tree (car tree)))
(cons #\Space (pack-list (cdr tree)))
(list #\))))))
(defun pack-term (args)
(declare (xargs :guard t
:verify-guards nil))
(intern (coerce (pack-list args) 'string) "ACL2"))
(defmacro pack (&rest args)
`(pack-term (list ,@args)))
|