/usr/share/acl2-4.3/books/misc/definline.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 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 73 74 75 76 77 | ;; 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")
(include-book "doc-section")
(defdoc definline
":Doc-Section misc
Define an inline function~/
Examples:
~bv[]
(include-book \"misc/definline\")
(definline car-alias (x)
(car x))
~ev[]~/
~c[definline] is the same as ~il[defun], but also issues a Common Lisp ``proclaim''
form instructing the compiler to inline later calls to this function. Some Lisps
ignore these ``proclaim'' forms and make inlining worthless. However, inlining
may provide significant gains on other Lisps.
Inlining is usually beneficial for ``small'' non-recursive functions which are
called frequently.")
(defdoc definlined
":Doc-Section misc
Define an inline function and then disable it.~/
~/
This is a ~il[defund]-like version of ~il[definline].")
(defun redefine-inline-fn (name state)
;; has an under-the-hood definition
(declare (xargs :guard t :stobjs state)
(ignorable state))
(prog2$
(cw "Warning: redefine-inline-fn has not been redefined and is doing nothing.")
name))
(defmacro redefine-inline (name)
`(make-event (let ((name (redefine-inline-fn ',name state)))
(value `(value-triple ',name)))
:check-expansion t))
(defmacro definline (name &rest args)
`(progn (defun ,name ,@args)
(redefine-inline ,name)))
(defmacro definlined (name &rest args)
`(progn (defund ,name ,@args)
(redefine-inline ,name)))
(defttag definline)
(progn!
(set-raw-mode t)
(defun redefine-inline-fn (name state)
(unless (live-state-p state)
(er hard? 'redefine-inline-fn
"redefine-inline-fn can only be called on live states."))
(unless (symbolp name)
(er hard? 'redefine-inline-fn
"expected ~x0 to be a symbol." name))
(let* ((wrld (w state))
(stobj-function (getprop name 'stobj-function nil 'current-acl2-world
wrld))
(def (cltl-def-from-name name stobj-function wrld)))
(unless def
(er hard? 'redefine-inline-fn "~x0 does not appear to be defined."))
(eval `(proclaim '(inline ,name)))
(eval def))
name))
(defttag nil)
|