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
119
120
|
(in-package "ACL2")
; Modification by Matt K. after v4-3: Removed :load-compiled-file :comp, which
; was part of all three include-book forms just below, in support of
; provisional certification. Presumably the indicated books have already been
; compiled by now, anyhow.
; were in portcullis:
(include-book "defcode" :ttags ((defcode)))
(include-book "rewrite-code")
(include-book "redefun")
#|
table-guard.lisp
----------------
By Peter Dillinger, ca. 2006
This is an example application of the hacking books which modifies ACL2 to
allow extending table guards.
|#
(program)
(set-state-ok t)
(defttag table-guard) ; need to do some evil stuff
; rewrite the table code to allow guard changes if a ttag is active
(progn+touchable
:all
(redefun+rewrite
table-fn1
(:carpat (cond
((and (iff mv-p (cdr stobjs-out))
(equal old-tterm tterm))
%redundant%)
(old-guard
%er1%)
((getpropc name 'table-alist nil %wrld%)
%er2%)
(t
%rest%))
:repl (cond
((and (iff mv-p (cdr stobjs-out))
(equal old-tterm tterm))
%redundant%)
((and old-guard (not (ttag %wrld%)))
%er1%)
((and (getpropc name 'table-alist nil %wrld%)
(not (ttag %wrld%)))
%er2%)
(t
%rest%))
:vars (%redundant%
%er1%
%er2%
%wrld%
%rest%)
:mult 1)))
(defttag nil) ; end of evil stuff
; name: name of table whose guard to rewrite
; rewrite-spec: like in redefun+rewrite (see rewrite-code.lisp)
; hints: for proving that old-guard implies new-guard
; skip-proof: t if you want to skip proving old-guard implies new-guard
;
; proof is used as a sanity check mostly.
(defmacro rewrite-table-guard (name rewrite-spec &key hints skip-proof)
(declare (xargs :guard (symbolp name)))
`(make-event
(er-let* ((old-guard (table ,name nil nil :guard))
; Matt K. mod 5/10/2023: Accommodate the case that the table-guard returns (mv
; successp msg); see :DOC table. But note that we are changing the table guard
; to return just the success flag; the custom message is lost.
(old-guard (value (if (eq (car old-guard) :mv)
`(car ,(cdr old-guard))
old-guard)))
(new-guard-cons (er-rewrite-form (list old-guard)
.,rewrite-spec)))
(er-progn
(if ',skip-proof
(value nil)
(thm-fn `(implies ,old-guard ,(car new-guard-cons))
state nil ',hints nil nil))
(value `(table ,',name nil nil :guard ,(car new-guard-cons)))))))
; adds specified key to acl2-defaults-table with guard for its value.
; also defines a setter macro.
(defmacro add-acl2-defaults-table-key (name val-guard)
(declare (xargs :guard (keywordp name)))
(let* ((name-str (symbol-name name))
(set-sym (intern (string-append "SET-" name-str) "ACL2")))
`(progn
(rewrite-table-guard
acl2-defaults-table
(:carpat %body%
:vars %body%
:repl (if (eq key ',name)
,val-guard
%body%)))
(defmacro ,set-sym (v)
`(with-output :off summary
(progn (table acl2-defaults-table ,',name ',v)
(table acl2-defaults-table ,',name)))))))
#| test case:
(defttag t)
(add-acl2-defaults-table-key :termination-method
(member-eq val '(:foo :bar :baz)))
(set-termination-method :foo)
|#
|
