/usr/share/acl2-7.2dfsg/books/make-event/logical-tangent.lisp is in acl2-books-source 7.2dfsg-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 | ; Copyright (C) 2006 University of Texas at Austin
; This program is free software; you can redistribute it and/or modify it under
; the terms of Version 2 of the GNU General Public License as published by the
; Free Software Foundation.
; This program is distributed in the hope that it will be useful,
; but WITHOUT ANY WARRANTY; without even the implied warranty of
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
; GNU General Public License for more details.
; You should have received a copy of the GNU General Public License
; along with this program; if not, write to the Free Software
; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
; By Peter Dillinger
;
; Here I use make-event to define a macro LOGICAL-TANGENT, which behaves
; a bit like WORMHOLE, but is a bit different. WORMHOLE provides an LD
; environment in which all STATE changes are reverted after it finishes.
; LOGICAL-TANGENT provides and LD environment in which changes to the WORLD
; and other settings (in *protected-state-globals-for-make-event*) are
; reverted after it finishes. WORMHOLE is logically meaningless.
; LOGICAL-TANGENT takes state (under the hood) and returns a passing
; "error triple". LOGICAL-TANGENT doesn't need the special "tunneling"
; capability of wormholes, as user-defined state globals and stobjs are
; not reverted.
(in-package "ACL2")
(defmacro logical-tangent ()
'((lambda () ; to make this invalid as an embedded event form
(make-event
(mv-let (erp val state)
(ld (standard-oi state)
:ld-error-action (ld-error-action state))
(declare (ignore erp val))
(value '(value-triple :invisible)))))))
|