← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/2004/matthews-vroon/support/tiny-fib-example/defstobj+.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/2004/matthews-vroon/support/tiny-fib-example/defstobj+.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
;This book was created by Daron Vroon on August 10, 2004
 
4
 
 
5
;The purpose of this book is to define a macro, defstobj+, which
 
6
;defines a defstobj, functions that copy to and from the defstobj from
 
7
;and to a non-stobj of similar shape, and theorems that these functions
 
8
;are logically the identity.
 
9
 
 
10
;This gets challenging if the stobj has arrays in it. These must be
 
11
;copied element by element using the element accessor defined by the
 
12
;defstobj. For example, consider the following stobj from the tiny
 
13
;machine (developed at Rockwell Collins, and published in the ACL2 case
 
14
;studies book):
 
15
 
 
16
;(defstobj tiny-state
 
17
;  (progc :type (unsigned-byte 10)
 
18
;         :initially 0)
 
19
;  (mem :type (array (signed-byte 32) (1024))
 
20
;       :initially 0)
 
21
;  (dtos :type (unsigned-byte 10)
 
22
;        :initially 0)
 
23
;  (ctos :type (unsigned-byte 10)
 
24
;        :initially 0)
 
25
;  :inline t)
 
26
 
 
27
;Copying the non-array elements is simple, using the update-progc and
 
28
;progc functions. The mem field only has accessors for its elements, so
 
29
;it must be copied one element at a time:
 
30
 
 
31
;(defun copy-to-tiny-state-mem
 
32
;  (n mem tiny-state)
 
33
;  (declare (xargs :stobjs (tiny-state)
 
34
;                  :measure (acl2-count (1+ n))
 
35
;                  :guard
 
36
;                  (and (memp mem)
 
37
;                       (equal (length mem) 1024)
 
38
;                       (natp n)
 
39
;                       (<= n 1024))))
 
40
;  (if (or (zp n) (< 1024 n))
 
41
;      tiny-state
 
42
;    (let* ((n (1- n))
 
43
;           (tiny-state (update-memi n (nth n mem) tiny-state)))
 
44
;      (copy-to-tiny-state-mem n mem tiny-state))))
 
45
 
 
46
;and
 
47
 
 
48
;(defun copy-from-tiny-state-mem (n tiny-state)
 
49
;         (declare (xargs :stobjs (tiny-state)
 
50
;                         :guard (and (natp n) (<= n 1024))))
 
51
;         (if (zp n)
 
52
;             nil
 
53
;             (cons (memi (- 1024 n) tiny-state)
 
54
;                   (copy-from-tiny-state-mem (1- n)
 
55
;                                             tiny-state))))
 
56
 
 
57
;Proving that each of these behaves correctly requires a 2 step
 
58
;process. First we need to prove a more general theorem proven by
 
59
;induction over n. Then we can prove the overall theorem that the
 
60
;functions work correctly when n = (len (nth *memi* tiny-state)). 
 
61
;Rather than do this two step process for every array field of every
 
62
;stobj defined using defstobj+, we define generic versions of array
 
63
;copying functions that are very similar to the ones defined
 
64
;above. These are called copy-to-stobj-array and
 
65
;copy-from-stobj-array. See their definitions below. Once they are
 
66
;defined, we prove that they do what we want (basically, that they are
 
67
;noops). The defstobj+ macro then simply defines array copy functions
 
68
;such as the ones above, and proves that they are logically equivalent
 
69
;to the generic functions.
 
70
 
 
71
;The only other difficulty of this macro is the guard proofs for the
 
72
;functions it generates (such as the ones above). In order to prove
 
73
;these, we need to prove that each array field is a true-list and that
 
74
;every element of those arrays is of the appropriate type. However,
 
75
;these are useful theorems in general, so we export them from defstobj+
 
76
;as well. Another "bonus" of this macro is a function that is logically
 
77
;identical to the stobj recognizer predicate, but works on
 
78
;non-stobjs. In our running example, the defstobj above creates a
 
79
;function called tiny-statep that is a recognizer predicate for the
 
80
;stobj. Our macro also includes a function called logical-tiny-statep
 
81
;which is logically equivalent to tiny-statep, but works on
 
82
;non-stobjs. We then immediately prove this fact and turn off the
 
83
;definition.
 
84
 
 
85
;USAGE
 
86
 
 
87
;Simply call defstobj+ like you would defstobj. It should work in any
 
88
;package. The only problem we have found is if you define the stobj to
 
89
;have a name in a package different than the current package. For
 
90
;example
 
91
 
 
92
;(defstobj+ FOO::tiny-state
 
93
;  (progc :type (unsigned-byte 10)
 
94
;         :initially 0)
 
95
;  (mem :type (array (signed-byte 32) (1024))
 
96
;       :initially 0)
 
97
;  (dtos :type (unsigned-byte 10)
 
98
;        :initially 0)
 
99
;  (ctos :type (unsigned-byte 10)
 
100
;        :initially 0)
 
101
;  :inline t)
 
102
 
 
103
;will break if you are in package BAR. This is due to the fact that
 
104
;defstobj (which is called by this macro) puts all of the functions
 
105
;it generates into the current package instead of the package of the
 
106
;stobj name. Since we haven't found a way of getting at the current
 
107
;package in a macro, we cannot follow suit. When we try to use
 
108
;functions generated by the defstobj, we call them in the package of
 
109
;the name of the stobj, and everything breaks.
 
110
 
 
111
;When you have successfully run defstobj+, you get everything that a
 
112
;defstobj generates. In addition, you get the following:
 
113
 
 
114
;(DEFUN COPY-TO-c (COPY c) ...) ;puts all the data in COPY into the stobj c.
 
115
 
 
116
;(DEFTHM COPY-TO-c-NOOP
 
117
;  (IMPLIES (AND (cP X)
 
118
;                (cP Y))
 
119
;           (EQUAL (COPY-TO-c X Y)
 
120
;                  X)))
 
121
 
 
122
;(DEFTHM COPY-TO-c-IGNORES-SECOND-ARG
 
123
;  (IMPLIES (AND (cP X)
 
124
;                (CP Y))
 
125
;           (EQUAL (EQUAL (COPY-TO-c COPY X)
 
126
;                         (COPY-TO-c COPY Y))
 
127
;                  T)))
 
128
 
 
129
;(DEFUN COPY-FROM-c (c) ...) ;creates a non-stobj that is logically identical to c.
 
130
 
 
131
;(DEFTHM COPY-FROM-c-NOOP
 
132
;  (IMPLIES (cP c)
 
133
;           (EQUAL (COPY-FROM-c c) c)))
 
134
 
 
135
;(DEFUN LOGICAL-cP (X) ...) ;logically equivalent to cP, but x doesn't need to
 
136
;                           ;be a stobj. 
 
137
;(DEFTHM LOGICAL-cP-cP
 
138
;  (EQUAL (LOGICAL-cP X)
 
139
;         (cP X)))
 
140
 
 
141
;where c is the name of your stobj. In addition, for each array field,
 
142
;a of c, you get the following:
 
143
 
 
144
;(DEFTHM aP-TRUE-LISTP
 
145
;  (IMPLIES (aP X) (TRUE-LISTP X)))
 
146
 
 
147
;(DEFTHM aP-NTH-TYPE
 
148
;  (IMPLIES (AND (aP X) (NATP N) (< N (LEN X)))
 
149
;           (typep(NTH N X))))
 
150
 
 
151
;(DEFUN COPY-TO-c-a (N a c) ...) ;called by COPY-TO-c
 
152
;(DEFUN COPY-FROM-c-a (N c) ...) ;called by COPY-FROM-c
 
153
 
 
154
;where typep is the predicate associated with the type of elements in
 
155
;a. To see what the predicate is for a given type, see the ACL2
 
156
;documentation topic type-spec.
 
157
 
 
158
;Including this book also provides some useful theorems about
 
159
;update-nth, nth, and a couple other functions. To turn these off,
 
160
;simply run the form:
 
161
 
 
162
;(in-theory (disable defstobj+-theory))
 
163
 
 
164
;Don't worry about the macro, it turns on everything it needs locally.
 
165
 
 
166
;MODIFIED by Daron Vroon on October 18, 2004:
 
167
 
 
168
;I've added a with-copy-of-stobj macro. The usage is identical to that
 
169
;of with-local-stobj (see ACL2 documentation). However, instead of
 
170
;creating a blank copy of the stobj for the form, it creates a copy of
 
171
;the current version of the stobj.
 
172
 
 
173
;For our purposes, this is useful since we can take the current state
 
174
;of our machine and run it forward to see what happens without
 
175
;actually changing the state of the machine.
 
176
 
 
177
;Basically, the macro uses copy-from- and copy-to- functions as
 
178
;follows. First, the macro creates a non-stobj copy of the stobj. Then
 
179
;it calls with-local-stobj to create a local copy of the stobj. Before
 
180
;computing anything, it puts the contents of the non-stobj copy into
 
181
;the local stobj. Finally, it performs the computation given by the
 
182
;user using the local copy.
 
183
 
 
184
(local
 
185
 ;; [Jared] changed this to use arithmetic-3 instead of 2
 
186
 (include-book "arithmetic-3/bind-free/top" :dir :system))
 
187
 
 
188
 
 
189
;we only want the stuff in this book + ground-zero theory for our
 
190
;proofs. so we have defstobj+-before and defstobj+-after.
 
191
(deflabel defstobj+-before)
 
192
 
 
193
;;;firstn
 
194
 
 
195
(local
 
196
 (defun firstn (n l)
 
197
   (declare (xargs :guard (and (true-listp l)
 
198
                               (integerp n)
 
199
                               (<= 0 n))))
 
200
   (cond ((endp l) nil)
 
201
         ((zp n) nil)
 
202
         (t (cons (car l)
 
203
                  (firstn (1- n) (cdr l)))))))
 
204
 
 
205
;;;lastn
 
206
 
 
207
(local
 
208
 (defun lastn (n a)
 
209
   (declare (xargs :guard (and (natp n))))
 
210
   (if (or (atom a) (zp n))
 
211
       a (lastn (1- n) (cdr a)))))
 
212
 
 
213
 
 
214
(local
 
215
  (defthm car-lastn
 
216
    (equal (car (lastn n x))
 
217
           (nth n x))
 
218
    :hints (("Goal" :in-theory (enable nth)))))
 
219
 
 
220
(local
 
221
 (defthm cdr-lastn
 
222
   (implies (and (natp n)
 
223
                 (true-listp x))
 
224
            (equal (cdr (lastn n x))
 
225
                   (lastn (1+ n) x)))))
 
226
 
 
227
(local
 
228
 (defthm consp-lastn
 
229
   (implies (and (< n (len x))
 
230
                 (<= 0 n))
 
231
            (consp (lastn n x)))))
 
232
 
 
233
(local
 
234
 (defthm lastn-alt-def
 
235
   (implies (and (natp n)
 
236
                 (true-listp x)
 
237
                 (< n (len x)))
 
238
            (equal (lastn n x)
 
239
                   (cons (nth n x)
 
240
                         (lastn (1+ n) x))))
 
241
   :hints (("goal" 
 
242
            :in-theory (disable car-lastn cdr-lastn lastn)
 
243
            :use (car-lastn cdr-lastn)))))
 
244
 
 
245
(local
 
246
 (defthm lastn-nil
 
247
   (implies (and (true-listp x)
 
248
                 (<= (len x) n)
 
249
                 (natp n))
 
250
            (equal (lastn n x)
 
251
                   nil))))
 
252
 
 
253
(local
 
254
 (defthm lastn-0
 
255
   (equal (lastn 0 x) x)))
 
256
 
 
257
(local (in-theory (disable lastn)))
 
258
 
 
259
;;;;;;;;;;;;;;;update-nth/nth stuff;;;;;;;;;;;;;;;;;;;;;;;
 
260
;i'm not sure exactly how much of this is necessary. i just grabbed
 
261
;these theorems from tiny.lisp
 
262
 
 
263
(defthm nth-update-nth2
 
264
   (equal
 
265
    (nth n1 (update-nth n2 v l))
 
266
    (if (equal (nfix n1) (nfix n2))
 
267
        v
 
268
      (nth n1 l)))
 
269
  :hints (("goal" :in-theory (enable update-nth nth))))
 
270
 
 
271
(defthm nth-update-nth-1
 
272
  (implies
 
273
    (not (equal (nfix n1) (nfix n2)))
 
274
   (equal
 
275
    (nth n1 (update-nth n2 v l))
 
276
    (nth n1 l))))
 
277
 
 
278
(defthm nth-update-nth-2
 
279
  (implies
 
280
    (equal (nfix n1) (nfix n2))
 
281
   (equal
 
282
    (nth n1 (update-nth n2 v l))
 
283
    v)))
 
284
 
 
285
(defun repeat (n v)
 
286
  (if (zp n)
 
287
      nil
 
288
    (cons v (repeat (1- n) v))))
 
289
 
 
290
(defthm update-nth-nil
 
291
  (equal (update-nth i v nil)
 
292
         (append (repeat i nil) (list v)))
 
293
  :hints (("goal" :in-theory (enable update-nth))))
 
294
 
 
295
(defthm update-nth-nth-noop-helper
 
296
  (implies
 
297
   (and (<= 0 n) (< n (len l)))
 
298
   (equal (update-nth n (nth n l) l) l))
 
299
  :hints (("goal" :in-theory (enable nth update-nth))))
 
300
 
 
301
(defthm update-nth-nth-noop
 
302
  (implies
 
303
   (and (<= 0 n) (< n (len l1)) (equal (nth n l1) (nth n l2)))
 
304
   (equal (update-nth n (nth n l2) l1) l1)))
 
305
 
 
306
;; order update-nth terms based on update field value
 
307
(defthm update-nth-update-nth-diff
 
308
  (implies
 
309
   (not (equal (nfix i1) (nfix i2)))
 
310
   (equal (update-nth i1 v1 (update-nth i2 v2 l))
 
311
          (update-nth i2 v2 (update-nth i1 v1 l))))
 
312
  :hints (("goal" :in-theory (enable update-nth nfix)))
 
313
  :rule-classes ((:rewrite :loop-stopper ((i1 i2)))))
 
314
 
 
315
(defthm update-nth-update-nth-same
 
316
  (equal (update-nth i v1 (update-nth i v2 l))
 
317
         (update-nth i v1 l))
 
318
  :hints (("goal" :in-theory (enable update-nth))))
 
319
 
 
320
(defthm len-repeat
 
321
  (equal (len (repeat i v)) (nfix i))
 
322
  :hints (("goal" :in-theory (enable nfix))))
 
323
 
 
324
(defthm len-update-nth-better
 
325
  (equal (len (update-nth i v l)) (max (1+ (nfix i)) (len l)))
 
326
  :hints (("goal" :in-theory (enable update-nth max))))
 
327
 
 
328
(defthm car-update-nth
 
329
  (equal (car (update-nth i v l)) (if (zp i) v (car l)))
 
330
  :hints (("goal" :in-theory (enable update-nth))))
 
331
 
 
332
(defthm cdr-update-nth
 
333
 (equal (cdr (update-nth n x y))
 
334
        (if (zp n) (cdr y) (update-nth (1- n) x (cdr y)))))
 
335
 
 
336
;;;copy-from-stobj stuff
 
337
 
 
338
(defun copy-from-stobj-array (n array)
 
339
  (if (zp n)
 
340
      nil
 
341
    (cons (nth (- (len array) n) array)
 
342
          (copy-from-stobj-array (1- n) array))))
 
343
 
 
344
(local
 
345
 (defthm copy-from-stobj-array-noop-l1
 
346
   (implies (and (natp n)
 
347
                 (true-listp array)
 
348
                 (<= n (len array)))
 
349
            (equal (copy-from-stobj-array n array)
 
350
                   (lastn (- (len array) n) array)))))
 
351
 
 
352
(in-theory (disable copy-from-stobj-array))
 
353
 
 
354
(defthm copy-from-stobj-array-noop
 
355
  (implies (and (equal n (len array))
 
356
                (true-listp array))
 
357
           (equal (copy-from-stobj-array n array)
 
358
                  array))
 
359
  :hints (("goal" :use ((:instance copy-from-stobj-array-noop-l1
 
360
                                   (n (len array)))))))
 
361
 
 
362
;;;copy-to-stobj stuff;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
363
 
 
364
(defun copy-to-stobj-array (n mem1 mem2)
 
365
  (if (or (zp n)
 
366
          (< (len mem2) n))
 
367
      mem2
 
368
    (let* ((n (1- n))
 
369
           (mem2 (update-nth n (nth n mem1) mem2)))
 
370
      (copy-to-stobj-array n mem1 mem2))))
 
371
 
 
372
(local
 
373
 (defthm cdr-copy-to-stobj-array
 
374
   (implies (and (consp mem2)
 
375
                 (<= n (len mem2))
 
376
                 (natp n))
 
377
            (equal (cdr (copy-to-stobj-array n mem1 mem2))
 
378
                   (copy-to-stobj-array (1- n) (cdr mem1) (cdr mem2))))
 
379
   :hints (("Goal" :in-theory (enable update-nth nth)))))
 
380
 
 
381
(local
 
382
 (defthm car-copy-to-stobj-array
 
383
   (implies (and (consp mem2)
 
384
                 (<= n (len mem2))
 
385
                 (posp n))
 
386
            (equal (car (copy-to-stobj-array n mem1 mem2))
 
387
                   (car mem1)))
 
388
   :hints (("Goal" :in-theory (enable update-nth nth)))))
 
389
 
 
390
(in-theory (disable copy-to-stobj-array))
 
391
 
 
392
(local
 
393
 (defun sub1-cdr-cdr-induction (n x1 x2)
 
394
   (if (zp n)
 
395
       (cons x1 x2)
 
396
     (sub1-cdr-cdr-induction (1- n) (cdr x1) (cdr x2)))))
 
397
 
 
398
(local
 
399
 (defthm copy-to-stobj-array-firstn
 
400
   (implies (and (consp mem1)
 
401
                 (consp mem2)
 
402
                 (equal (len mem1)
 
403
                        (len mem2))
 
404
                 (<= n (len mem1))
 
405
                 (natp n))
 
406
            (equal (firstn n (copy-to-stobj-array n mem1 mem2))
 
407
                   (firstn n mem1)))
 
408
   :hints (("Goal" :in-theory (enable update-nth nth)
 
409
            :induct (sub1-cdr-cdr-induction n mem1 mem2)))))
 
410
 
 
411
(local
 
412
 (defthm firstn-with-large-index
 
413
   (implies (and (<= (len l) (nfix n))
 
414
                 (true-listp l))
 
415
            (equal (firstn n l) l))
 
416
   :hints (("goal" :in-theory (enable nfix)))))
 
417
 
 
418
(local
 
419
 (defthm true-listp-copy-to-stobj-array
 
420
   (implies (true-listp x)
 
421
            (true-listp (copy-to-stobj-array n y x)))
 
422
   :hints (("Goal" :in-theory (enable copy-to-stobj-array)))))
 
423
 
 
424
(local
 
425
 (defthm len-copy-to-stobj-array
 
426
   (implies (<= n (len x))
 
427
            (equal (len (copy-to-stobj-array n y x))
 
428
                   (len x)))
 
429
   :hints (("Goal" :in-theory (enable copy-to-stobj-array)))))
 
430
 
 
431
(defthm copy-to-stobj-array-noop
 
432
  (implies (and (equal n (len mem1))
 
433
                (equal n (len mem2))
 
434
                (consp mem1)
 
435
                (consp mem2)
 
436
                (true-listp mem1)
 
437
                (true-listp mem2))
 
438
           (equal (copy-to-stobj-array n mem1 mem2)
 
439
                  mem1))
 
440
  :hints (("goal" :use copy-to-stobj-array-firstn)))
 
441
 
 
442
;;;copy-to-stobj-array ignores 2nd argument.
 
443
 
 
444
(local
 
445
 (defun sub1-cdr-cdr-cdr-induction (n x1 x2 x3)
 
446
   (if (zp n)
 
447
       (list x1 x2 x3)
 
448
     (sub1-cdr-cdr-cdr-induction (1- n) (cdr x1) (cdr x2) (cdr x3)))))
 
449
 
 
450
(local
 
451
 (defthm copy-to-stobj-array-ignores-second-arg-l1
 
452
   (implies (and (natp n)
 
453
                 (<= n (len mem2))
 
454
                 (equal (len mem2) (len mem3)))
 
455
            (equal (equal (firstn n (copy-to-stobj-array n mem1 mem2))
 
456
                          (firstn n (copy-to-stobj-array n mem1 mem3)))
 
457
                   t))
 
458
   :hints (("Goal" :induct (sub1-cdr-cdr-cdr-induction n mem1 mem2 mem3)))))
 
459
 
 
460
(defthm copy-to-stobj-array-ignores-second-arg
 
461
  (implies (and (true-listp mem2)
 
462
                (true-listp mem3)
 
463
                (equal n (len mem2))
 
464
                (equal n (len mem3)))
 
465
           (equal (equal (copy-to-stobj-array n mem1 mem2)
 
466
                         (copy-to-stobj-array n mem1 mem3))
 
467
                  t))
 
468
  :hints (("Goal" :use copy-to-stobj-array-ignores-second-arg-l1)))
 
469
 
 
470
;;;other helpful theorems:
 
471
 
 
472
(defthm len-0-atom
 
473
 (equal (equal 0 (len x))
 
474
          (atom x)))
 
475
 
 
476
;(defthmd nth-constant-open
 
477
;  (implies (and (syntaxp (quotep n))
 
478
;                (natp n))
 
479
;           (equal (nth n x)
 
480
;                  (if (equal n 0) (car x) (nth (1- n) (cdr x))))))
 
481
 
 
482
(defthmd cons-equal-car
 
483
  (equal (equal x (cons (car x) rest))
 
484
         (and (consp x)
 
485
              (equal (cdr x) rest))))
 
486
 
 
487
(defthm len>0-consp
 
488
  (implies (< 0 (len x))
 
489
           (consp x)))
 
490
 
 
491
(defthm add-cancel
 
492
  (implies (and (syntaxp (quotep x))
 
493
                (syntaxp (quotep z))
 
494
                (rationalp y)
 
495
                (rationalp z))
 
496
           (equal (equal (+ x y) z)
 
497
                  (equal y (+ (- x) z)))))
 
498
 
 
499
(deflabel defstobj+-after)
 
500
 
 
501
(deftheory defstobj+-theory
 
502
  (set-difference-theories (current-theory 'defstobj+-after)
 
503
                           (current-theory 'defstobj+-before)))
 
504
 
 
505
;and now, the macro:
 
506
 
 
507
;snagged this from Dave Greve's work. It turns a list of symbols into
 
508
;a single string that is the concatination of the names of those symobols
 
509
(defun symbol-list-to-string (list)
 
510
  (declare (xargs :guard (symbol-listp list)))
 
511
  (if (consp list)
 
512
      (concatenate 'string 
 
513
                   (symbol-name (car list))
 
514
                   (symbol-list-to-string (cdr list)))
 
515
    ""))
 
516
                   
 
517
;again, snagged from Dave Greve. This concatinates symbols. The
 
518
;resulting symbol is put in the same package as the witness.
 
519
(defmacro join-symbols (witness &rest rst)
 
520
  `(intern-in-package-of-symbol (symbol-list-to-string (list ,@rst))
 
521
                                ,witness))
 
522
 
 
523
;this generates all the stuff necessary for each array field
 
524
(defun generate-array-theorems (stobj-name field-name elt-type len)
 
525
  (declare (xargs :mode :program))
 
526
  (let* ((x (join-symbols stobj-name 'x))
 
527
         (n (join-symbols stobj-name 'n))
 
528
         (field-predicate (join-symbols stobj-name field-name 'p))
 
529
         (field-get (join-symbols stobj-name field-name 'i))
 
530
         (field-update (join-symbols stobj-name 'update- field-get))
 
531
         (field-index (join-symbols stobj-name '* field-name 'i*))
 
532
         (stobj-predicate (join-symbols stobj-name stobj-name 'p))
 
533
         (thm1name (join-symbols stobj-name 
 
534
                                 field-predicate 
 
535
                                 '-true-listp))
 
536
         (thm2name (join-symbols stobj-name 
 
537
                                 field-predicate 
 
538
                                 '-nth-type))
 
539
         (copy-to-name (join-symbols stobj-name
 
540
                                     'copy-to-
 
541
                                     stobj-name
 
542
                                     '-
 
543
                                     field-name))
 
544
         (thm3name (join-symbols stobj-name
 
545
                                 copy-to-name
 
546
                                 '-copy-to-stobj-array))
 
547
         (copy-from-name (join-symbols stobj-name
 
548
                                       'copy-from-
 
549
                                       stobj-name
 
550
                                       '-
 
551
                                       field-name))
 
552
         (thm4name (join-symbols stobj-name
 
553
                                 copy-from-name
 
554
                                 '-copy-from-stobj-array)))
 
555
    (list
 
556
     `(defthm ,thm1name
 
557
        (implies (,field-predicate ,x)
 
558
                 (true-listp ,x)))
 
559
     `(defthm ,thm2name
 
560
        (implies (and (,field-predicate ,x)
 
561
                      (natp ,n)
 
562
                      (< ,n (len ,x)))
 
563
                 ,(translate-declaration-to-guard elt-type `(nth ,n ,x) nil)))
 
564
     `(defun ,copy-to-name (,n ,field-name ,stobj-name)
 
565
        (declare (xargs :stobjs (,stobj-name)
 
566
                        :measure (acl2-count (1+ ,n)) ;needed?
 
567
                        :guard (and (,field-predicate ,field-name)
 
568
                                    (equal (length ,field-name) ,len)
 
569
                                    (natp ,n)
 
570
                                    (<= ,n ,len))))
 
571
        (if (or (zp ,n)
 
572
                (< ,len ,n))
 
573
            ,stobj-name
 
574
          (let* ((,n (1- ,n))
 
575
                 (,stobj-name (,field-update ,n (nth ,n ,field-name) ,stobj-name)))
 
576
            (,copy-to-name ,n ,field-name ,stobj-name))))
 
577
     `(local
 
578
       (defthm ,thm3name
 
579
         (implies (and (< ,field-index (len ,stobj-name))
 
580
                       (equal (len (nth ,field-index ,stobj-name)) ,len))
 
581
                  (equal (,copy-to-name ,n ,field-name ,stobj-name)
 
582
                         (update-nth 
 
583
                          ,field-index
 
584
                          (copy-to-stobj-array ,n 
 
585
                                               ,field-name 
 
586
                                               (nth ,field-index ,stobj-name))
 
587
                          ,stobj-name)))
 
588
         :hints (("goal" :in-theory (enable copy-to-stobj-array)))))
 
589
     `(in-theory (disable ,copy-to-name))
 
590
     `(defun ,copy-from-name (,n ,stobj-name)
 
591
        (declare (xargs :stobjs (,stobj-name)
 
592
                        :guard (and (natp ,n)
 
593
                                    (<= ,n ,len))))
 
594
        (if (zp ,n)
 
595
            nil
 
596
          (cons (,field-get (- ,len ,n) ,stobj-name)
 
597
                (,copy-from-name (1- ,n) ,stobj-name))))
 
598
     `(local
 
599
       (defthm ,thm4name
 
600
         (implies (,stobj-predicate ,stobj-name)
 
601
                  (equal (,copy-from-name ,n ,stobj-name)
 
602
                         (copy-from-stobj-array ,n 
 
603
                                                (nth ,field-index 
 
604
                                                     ,stobj-name))))
 
605
         :hints (("goal" :in-theory (enable copy-from-stobj-array))))))))
 
606
 
 
607
;this gets the type of a field from its definition.
 
608
(defun get-type-from-field-declaration (fd)
 
609
  (cond ((endp fd) t)
 
610
        ((equal (car fd) :type) (cadr fd))
 
611
        (t (get-type-from-field-declaration (cdr fd)))))
 
612
 
 
613
;this generates all the theorems and defuns necessary.
 
614
;stobj-name is the name of the stobj (duh)
 
615
;field-defs is the list of field definitions left to be processed
 
616
;lsp is the list of predicates for the logical stobj predicate (aka lsp)
 
617
;ct keeps track of the actions necessary to copy to a stobj
 
618
;cf keeps track of the actions necessary to copy from a stobj
 
619
;array-thms keeps track of all the events generated for all the array fields
 
620
;len keeps track of the number of field-defs processed so far. at the end, it gives
 
621
;    us the length of the stobj.
 
622
(defun generate-defstobj+-aux (stobj-name field-defs lsp ct cf array-thms len)
 
623
  (declare (xargs :mode :program))
 
624
  (let ((x (join-symbols stobj-name 'x))
 
625
        (y (join-symbols stobj-name 'y))
 
626
        (copy (join-symbols stobj-name 'copy)))
 
627
    (if (endp field-defs) ;when we are done, put everything together.
 
628
        (let* ((stobj-predicate (join-symbols stobj-name stobj-name 'p))
 
629
               (lsp-name (join-symbols stobj-name 'logical- stobj-predicate))
 
630
               (thm1name (join-symbols stobj-name lsp-name '- stobj-predicate))
 
631
               (copy-to-name (join-symbols stobj-name 'copy-to- stobj-name))
 
632
               (copy-from-name (join-symbols stobj-name 'copy-from- stobj-name))
 
633
               (thm2name (join-symbols stobj-name copy-to-name '-noop))
 
634
               (thm3name (join-symbols stobj-name 
 
635
                                       copy-to-name 
 
636
                                       '-ignores-second-arg))
 
637
               (thm4name (join-symbols stobj-name copy-from-name '-noop)))
 
638
          `((defun ,lsp-name (,x)
 
639
              (declare (xargs :guard t))
 
640
              (and (true-listp ,x)
 
641
                   (equal (len ,x) ,len)
 
642
                   ,@lsp))
 
643
            (defthm ,thm1name
 
644
              (equal (,lsp-name ,x)
 
645
                     (,stobj-predicate ,x)))
 
646
            (in-theory (disable ,lsp-name))
 
647
            ,@array-thms
 
648
            (defun ,copy-to-name (,copy ,stobj-name)
 
649
              (declare (xargs :stobjs (,stobj-name)
 
650
                              :guard (,lsp-name ,copy)))
 
651
              (let* ,ct ,stobj-name))
 
652
            (defthm ,thm2name
 
653
              (implies (and (,stobj-predicate ,x)
 
654
                            (,stobj-predicate ,y))
 
655
                       (equal (,copy-to-name ,x ,y)
 
656
                              ,x))
 
657
              :hints (("goal" :in-theory (enable cons-equal-car))))
 
658
            (defthm ,thm3name
 
659
              (implies (and (,stobj-predicate ,x)
 
660
                            (,stobj-predicate ,y))
 
661
                       (equal (equal (,copy-to-name ,copy ,x)
 
662
                                     (,copy-to-name ,copy ,y))
 
663
                              t)))
 
664
            (defun ,copy-from-name (,stobj-name)
 
665
              (declare (xargs :stobjs (,stobj-name)))
 
666
              (list ,@(reverse cf)))
 
667
            (defthm ,thm4name
 
668
              (implies (,stobj-predicate ,stobj-name)
 
669
                       (equal (,copy-from-name ,stobj-name)
 
670
                              ,stobj-name))
 
671
              :hints (("goal" :in-theory (enable cons-equal-car))))
 
672
            (in-theory (disable ,copy-to-name ,copy-from-name))))
 
673
      (if (not (consp (car field-defs))) ;if the item is :inline, t, or nil, just continue.
 
674
          (generate-defstobj+-aux stobj-name (cdr field-defs) lsp ct cf array-thms len)
 
675
        (let* ((fd (car field-defs))
 
676
               (fname (car fd))
 
677
               (type (get-type-from-field-declaration (cdr fd)))
 
678
               (field-predicate (join-symbols stobj-name fname 'p)))
 
679
          (if (and (consp type)
 
680
                   (eq (car type) 'array))
 
681
              (let ((flen (caaddr type))
 
682
                    (elt-type (cadr type))
 
683
                    (field-index (join-symbols stobj-name '* fname 'i*))
 
684
                    (copy-to-name (join-symbols stobj-name 
 
685
                                                'copy-to- 
 
686
                                                stobj-name
 
687
                                                '-
 
688
                                                fname))
 
689
                    (copy-from-name (join-symbols stobj-name
 
690
                                                  'copy-from-
 
691
                                                  stobj-name
 
692
                                                  '-
 
693
                                                  fname)))
 
694
                (generate-defstobj+-aux 
 
695
                 stobj-name
 
696
                 (cdr field-defs)
 
697
                 (cons `(,field-predicate (nth ,field-index ,x))
 
698
                       (cons `(equal (len (nth ,field-index ,x)) ,flen)
 
699
                             lsp))
 
700
                 (cons `(,stobj-name (,copy-to-name ,flen (nth ,field-index ,copy) ,stobj-name))
 
701
                       ct)
 
702
                 (cons `(,copy-from-name ,flen ,stobj-name) cf)
 
703
                 (append (generate-array-theorems stobj-name fname elt-type flen)
 
704
                         array-thms)
 
705
                 (1+ len)))
 
706
            (let ((field-index (join-symbols stobj-name '* fname '*))
 
707
                  (field-update (join-symbols stobj-name 'update- fname)))
 
708
              (generate-defstobj+-aux
 
709
               stobj-name
 
710
               (cdr field-defs)
 
711
               (cons `(,field-predicate (nth ,field-index ,x))
 
712
                     lsp)
 
713
               (cons `(,stobj-name (,field-update (nth ,field-index ,copy) ,stobj-name))
 
714
                     ct)
 
715
               (cons `(,fname ,stobj-name) cf)
 
716
               array-thms
 
717
               (1+ len)))))))))
 
718
 
 
719
;(generate-defstobj+-aux 'tiny-state 
 
720
;                        '((progc :type (unsigned-byte 10) :initially 0)
 
721
;                          (mem :type (array (signed-byte 32) (1024)) :initially 0)
 
722
;                          (dtos :type (unsigned-byte 10) :initially 0)
 
723
;                          (ctos :type (unsigned-byte 10) :initially 0)
 
724
;                          :inline t)
 
725
;                        nil
 
726
;                        nil
 
727
;                        nil
 
728
;                        nil
 
729
;                        0)
 
730
 
 
731
;makes the encapsulate, and seperates everything for generate-defstobj+-aux
 
732
(defun generate-defstobj+ (dlist)
 
733
  (declare (xargs :mode :program))
 
734
  `(encapsulate
 
735
    ()
 
736
    (local (in-theory (union-theories (theory 'ground-zero)
 
737
                                      (theory 'defstobj+-theory))))
 
738
    (defstobj ,@dlist)    
 
739
    ,@(generate-defstobj+-aux (car dlist) (cdr dlist) nil nil nil nil 0)))
 
740
 
 
741
;the final product:
 
742
(defmacro defstobj+ (name &rest args)
 
743
  (generate-defstobj+ (cons name args))) 
 
744
 
 
745
;added October 18, 2004 by Daron Vroon:
 
746
 
 
747
(defmacro with-copy-of-stobj (stobj mv-let-form)
 
748
  (let ((copy-from-stobj (join-symbols stobj 'copy-from- stobj))
 
749
        (copy-to-stobj (join-symbols stobj 'copy-to- stobj)))
 
750
    `(let ((stobj (,copy-from-stobj ,stobj)))
 
751
       (with-local-stobj
 
752
        ,stobj
 
753
        (mv-let ,(nth 1 mv-let-form)
 
754
                (let ((,stobj (,copy-to-stobj stobj ,stobj)))
 
755
                  ,(nth 2 mv-let-form))
 
756
                ,(nth 3 mv-let-form))))))