/usr/share/acl2-6.5/books/misc/definline.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 | ;; definline.lisp - The definline and definlined macros.
;; Jared Davis <jared@cs.utexas.edu>
;;
;; This file is in the public domain. You can freely redistribute it and
;; modify it for any purpose. This file comes with absolutely no warranty,
;; including the implied warranties of merchantibility and fitness for a
;; particular purpose.
(in-package "ACL2")
(defmacro definline (name formals &rest args)
":Doc-Section defun
Alias for ~ilc[defun-inline]~/
Examples:
~bv[]
(include-book \"misc/definline\")
(definline car-alias (x)
(car x))
~ev[]
~c[definline] is a wrapper for ~ilc[defun-inline].
We probably shouldn't have this wrapper. But until ACL2 5.0 there was no
~c[defun-inline], and ~c[definline] was implemented using a ~il[trust-tag].
When ~c[defun-inline] was introduced, we already had many books with
~c[definline] and liked the shorter name, so we dropped the trust tag and
turned it into a wrapper for ~c[defun-inline].~/~/"
`(defun-inline ,name ,formals . ,args))
(defmacro definlined (name formals &rest args)
":Doc-Section defun
Alias for ~ilc[defund-inline]~/
This is a ~il[defund]-like version of ~il[definline].~/~/"
`(defund-inline ,name ,formals . ,args))
(local
(progn
(defun test (x)
(declare (xargs :guard (natp x)))
(+ 1 x))
(definline test2 (x)
(declare (xargs :guard (natp x)))
(+ 1 x))
(defun f (x) (test x))
(defun g (x) (test2 x))
;; (disassemble$ 'f) ;; not inlined, as expected
;; (disassemble$ 'g) ;; inlined, as expected
))
|