/usr/share/acl2-6.3/books/make-event/gen-defun-check.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 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 78 79 80 81 82 83 | ; 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.
; See gen-defun.lisp. The only difference here is that we use :check-expansion
; t (see comment on that below).
(in-package "ACL2")
(program)
(set-state-ok t)
(defun defun-from-body (name body stobjs ctx state)
(let ((stobjs (cond ((and stobjs (symbolp stobjs))
(list stobjs))
(t stobjs))))
(mv-let (erp tbody bindings state)
(translate1 body name (list (cons name name)) stobjs
ctx (w state) state)
(declare (ignore bindings))
(cond (erp (er soft ctx
"Translation of ~X01 failed."
body
(evisc-tuple 4 3 nil nil)))
((ffnnamep name tbody)
(er soft ctx
"Generation of non-recursive definition of ~x0 from ~
body ~X12 failed because the function symbol ~x0 ~
occurs in the body."
name tbody (evisc-tuple 4 3 nil nil)))
(t (let ((vars (merge-sort-symbol-< (all-vars body))))
(value `(defun ,name ,vars
,@(and stobjs
`((declare (xargs :stobjs ,stobjs))))
,body))))))))
(defun gen-name (root index wrld)
(let ((name
(intern-in-package-of-symbol (coerce (packn1 (list root "-" index))
'string)
root)))
(cond ((function-symbolp name wrld)
(gen-name root (1+ index) wrld))
(t name))))
(defmacro gen-defun (&whole ev
body &key stobjs root)
; Stobjs should be a symbol naming a stobj, or a list of such. Root is a
; string or symbol, default 'fn, for use as the prefix of the generated
; function name.
(let ((root (or root 'fn)))
`(make-event
(let ((wrld (w state)))
(defun-from-body
(gen-name ',root 0 wrld)
',body
',stobjs
'gen-defun
state))
:on-behalf-of ,ev
; The following will allow the definitions to fail at include-book time with an
; error message about the expansion changing rather than an error message
; saying that fn-0 (say) is already defined.
:check-expansion t)))
; Examples.
(gen-defun (+ x y))
(gen-defun (* x y))
(gen-defun (* x y y))
(defthm gen-defun-test
(equal (list (fn-0 x y) (fn-1 x y) (fn-2 x y))
(list (+ x y) (* x y) (* x y y)))
:rule-classes nil)
(gen-defun (mv x y state) :stobjs state :root foo)
|