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
121
122
123
124
125
126
127
128
129
130
131
132
133
134
|
; Copyright (C) 2024, Matt Kaufmann
; Written by Matt Kaufmann
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
; See README.txt for an overview of this example.
(in-package "ACL2")
; First we redefine comment-window-co so that cw will print to the standard-co
; of state.
(defttag :attach-stobj-demo)
(progn!
(set-raw-mode t)
(defun comment-window-co ()
(standard-co *the-live-state*)))
(defttag nil)
; Set a starting point to undo back through.
(deflabel start)
; Include the book that introduces the mem stobj, and note the rules proved in
; that book (checking that they are redundant).
(include-book "mem")
(set-enforce-redundancy t)
(defthm lookup-update
(implies (and (mem-indexp i)
(mem-indexp j))
(equal (lookup i (update j v mem))
(if (equal i j)
v
(lookup i mem)))))
(defthm update-update-same
(implies (equal i1 i2)
(equal (update i2 v2 (update i1 v1 mem))
(update i2 v2 mem))))
(defthm update-update-different
(implies (and (mem-indexp i1)
(mem-indexp i2)
(not (equal i1 i2)))
(equal (update i2 v2 (update i1 v1 mem))
(update i1 v1 (update i2 v2 mem)))))
(set-enforce-redundancy nil)
; Now do some evaluation, which should produce output showing the use of array
; operations (see the definitions of lookup$c and update$c in mem.lisp).
; Returns nil, with output: @@ Calling: (MEM$C-ARI 2 MEM$C)
(lookup 2 mem)
; Returns <mem>, with output: @@ Calling: (UPDATE-MEM$C-ARI 2 TWO MEM$C)
(update 2 'two mem)
; Returns TWO, with output: @@ Calling: (MEM$C-ARI 2 MEM$C)
(lookup 2 mem)
; Next we do similar testing with mem nested as a field of another stobj, st.
(include-book "nested")
; Returns NIL, with output: @@ Calling: (MEM$C-ARI 2 MEM$C)
(st-lookup 2 st)
; Returns <st>, with output: @@ Calling: (UPDATE-MEM$C-ARI 2 TWO MEM$C)
(st-update 2 'two st)
; Returns TWO, with output: @@ Calling: (MEM$C-ARI 2 MEM$C)
(st-lookup 2 st)
; Start over:
(ubt 'start)
; This time include the book in which mem has mem{ht} as an attachment, so that
; exported operations will be hash-table operations rather than array
; operations.
(include-book "mem-as-ht")
; Check that the rules proved for mem are still present (with having to prove
; them again) when including mem-as-ht.lisp.
(set-enforce-redundancy t)
(defthm lookup-update
(implies (and (mem-indexp i)
(mem-indexp j))
(equal (lookup i (update j v mem))
(if (equal i j)
v
(lookup i mem)))))
(defthm update-update-same
(implies (equal i1 i2)
(equal (update i2 v2 (update i1 v1 mem))
(update i2 v2 mem))))
(defthm update-update-different
(implies (and (mem-indexp i1)
(mem-indexp i2)
(not (equal i1 i2)))
(equal (update i2 v2 (update i1 v1 mem))
(update i1 v1 (update i2 v2 mem)))))
(set-enforce-redundancy nil)
; Now do the evaluation we did before, where this time, they should produce
; output showing the use of hash-table operations (see the definitions of
; lookup{ht}$c and update{ht}$c in mem{ht}.lisp -- those are from the :EXEC
; fields of the stobj mem{ht} that was attached to mem in mem-as-ht.lisp).
; Returns NIL, with output: @@ Calling: (MEM{HT}$C-HT-GET 2 MEM{HT}$C)
(lookup 2 mem)
; Returns <mem>, with output: @@ Calling: (MEM{HT}$C-HT-PUT 2 TWO MEM{HT}$C)
(update 2 'two mem)
; Returns TWO, with output: @@ Calling: (MEM{HT}$C-HT-GET 2 MEM{HT}$C)
(lookup 2 mem)
; Next we do similar testing with mem nested as a field of another stobj, st.
; We expect to see that the attachment to mem, mem{ht}, is being used for
; execution, since the stobj mem was introduced in mem-as-ht.lisp after the
; attach-stobj event in that book.
(include-book "nested")
; Returns NIL, with output: @@ Calling: (MEM{HT}$C-HT-GET 2 MEM{HT}$C)
(st-lookup 2 st)
; Returns <st>, with output: @@ Calling: (MEM{HT}$C-HT-PUT 2 TWO MEM{HT}$C)
(st-update 2 'two st)
; Returns TWO, with output: @@ Calling: (MEM{HT}$C-HT-GET 2 MEM{HT}$C)
(st-lookup 2 st)
|
