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
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
|
((:FILES "
.:
all.acl2
all.lisp
bridge.acl2
bridge.lisp
copyright
defcode.acl2
defcode.lisp
defstruct-parsing.acl2
defstruct-parsing.lisp
dynamic-make-event.acl2
dynamic-make-event.lisp
dynamic-make-event-test.acl2
dynamic-make-event-test.lisp
hacker.acl2
hacker.lisp
hacker-pkg.lsp
Makefile
progn-bang-enh.acl2
progn-bang-enh.lisp
raw.acl2
raw.lisp
Readme.lsp
redefun.acl2
redefun.lisp
rewrite-code.acl2
rewrite-code.lisp
rewrite-code-pkg.lsp
subsumption.acl2
subsumption.lisp
table-guard.acl2
table-guard.lisp
"
)
(:TITLE "Hacking & Extending ACL2")
(:AUTHOR/S "Peter C. Dillinger") ; With guidance & advice from Matt Kaufmann and Panagiotis Manolios
(:KEYWORDS ; non-empty list of keywords, case-insensitive
"book contributions" "contributed books"
"hacking" "system" "defcode" "redefun" "trust tags" "ttags"
"extensions" "raw mode" "raw lisp"
)
(:ABSTRACT
"This support code is intended as a library to those who wish to use
trust tags to modify or extend core ACL2 behavior. We add some other
constructs to the set of low-level tools enabled by trust tags that make
system modifications easier to specify and keep track of. We also offer
some high-level tools that offer significant benefits (in both ease &
soundness) over more direct methods of overriding behavior. See the
comments in Readme.lsp and individual files for more info.
")
(:PERMISSION ; author/s permission for distribution and copying:
"Copyright (C) 2008 Peter C. Dillinger, the Georgia Tech Research Corporation,
and Northeastern University
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., 51 Franklin Street, Fifth Floor, Boston, MA
02110-1301, USA."))
#|
This was developed as part of ACL2s: "The ACL2 Sedan."
hacker-pkg.lsp
Package & documentation topic/section used in preambles
all.lisp
Book that includes all of the below
bridge.lisp
Book for bridging the gap between ACL2 and raw Lisp
defcode.lisp
Book for the DEFCODE construct (ttag required)
defstruct-parsing.lisp
Book for parsing defstruct calls
dynamic-make-event.lisp
Support for modified events to return a make-event expansion.
dynamic-make-event-test.lisp
A regression test for dynamic-make-event.
hacker.lisp
Basic book with hacking constructs
progn-bang-enh.lisp
Used by defcode.lisp. Subject to change. :)
raw.lisp
Book for making raw definitions in a nice way
redefun.lisp
Book for overriding and rewriting existing definitions
rewrite-code.lisp
Book with tools for rewriting and copying existing code
(used by redefun.lisp)
subsumption.lisp
Book with constructs to do ttag subsumption
table-guard.lisp
An example application of this stuff to allow extension of table
guards, including the acl2-defaults-table.
|#
|
