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
|
; 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 the GNU General Public License as published by
; the Free Software Foundation; either version 2 of the License, or
; (at your option) any later version.
; 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)))))))
|
