← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/2000/sumners1/cdeq/cdeq-defs.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/2000/sumners1/cdeq/cdeq-defs.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
;;;; we will need a book on record ops and theorems
 
4
 
 
5
(include-book "records")
 
6
(include-book "../../../../ordinals/e0-ordinal")
 
7
 
 
8
#|----------------------------------------------------------------------------|#
 
9
 
 
10
;;;; BEGIN auxiliary definitions ;;;;
 
11
 
 
12
(defun add-set (e x)
 
13
  (if (member e x) x (cons e x)))
 
14
 
 
15
(defun add-in-range (lo hi x)
 
16
  (declare (xargs :measure (nfix (1+ (- hi lo)))))
 
17
  (if (and (integerp hi)
 
18
           (integerp lo)
 
19
           (<= lo hi))
 
20
      (add-in-range lo (1- hi) (add-set hi x))
 
21
    x))
 
22
 
 
23
(defun add-nums-in (case x)
 
24
  (cond ((endp (cdr case)) x)
 
25
        ((consp (car case))
 
26
         (add-in-range (caar case)
 
27
                       (cadar case)
 
28
                       (add-nums-in (cdr case) x)))
 
29
        (t (add-set (car case)
 
30
                    (add-nums-in (cdr case) x)))))
 
31
 
 
32
(defun locase-nums (cases)
 
33
  (if (endp cases) ()
 
34
    (add-nums-in (car cases)
 
35
                 (locase-nums (cdr cases)))))
 
36
 
 
37
(defun loc-in-range (loc range)
 
38
  (and (consp range)
 
39
       (>= loc (first range))
 
40
       (<= loc (second range))))
 
41
 
 
42
(defun loc-in-when (loc case)
 
43
  (and (consp (rest case))
 
44
       (or (equal loc (first case))
 
45
           (loc-in-range loc (first case))
 
46
           (loc-in-when loc (rest case)))))
 
47
 
 
48
(defun gen-locase (loc cases)
 
49
  (cond ((endp cases) ())
 
50
        ((loc-in-when loc (first cases))
 
51
         (cons (first (last (first cases)))
 
52
               (gen-locase loc (rest cases))))
 
53
        (t (gen-locase loc (rest cases)))))
 
54
 
 
55
(defun gen-locases (locs cases)
 
56
  (if (endp locs) '((t t))
 
57
    (cons (list (first locs)
 
58
                (cons 'and (gen-locase (first locs) cases)))
 
59
          (gen-locases (rest locs) cases))))
 
60
 
 
61
;;;; a useful macro for defining large case splits on program locations
 
62
;;;; in predicates. This is used extensively in the invariant definitions
 
63
 
 
64
(defmacro locase (loc &rest cases)
 
65
  (list* 'case loc (gen-locases (locase-nums cases) cases)))
 
66
 
 
67
(defthm nil-update-absorbed
 
68
  (implies (not (g a r))
 
69
           (equal (s a nil r) r))
 
70
  :hints (("Goal" 
 
71
           :use (:instance s-same-g)
 
72
           :in-theory (disable s-same-g))))
 
73
 
 
74
 
 
75
;; some initial defintions
 
76
 
 
77
(defmacro in-range (x lo hi)
 
78
  `(and (integerp ,x)
 
79
        (>= ,x ,lo)
 
80
        (<= ,x ,hi)))
 
81
 
 
82
; The following was removed with the addition of natp-compound-recognizer to
 
83
; ACL2 2.9.2.
 
84
;(defthm natp-compound-recognizer
 
85
;  (iff (natp x)
 
86
;       (and (integerp x) (>= x 0)))
 
87
;  :rule-classes :compound-recognizer)
 
88
 
 
89
(in-theory (disable natp))
 
90
 
 
91
; The following was removed with the addition of natp-compound-recognizer to
 
92
; ACL2 2.9.2.
 
93
;(defthm posp-compound-recognizer
 
94
;  (iff (posp x)
 
95
;       (and (integerp x) (> x 0)))
 
96
;  :rule-classes :compound-recognizer)
 
97
 
 
98
(in-theory (disable posp))
 
99
 
 
100
 
 
101
(encapsulate 
 
102
 (((maxf) => *))
 
103
 (local (defun maxf () 1))
 
104
 (defthm maxf-is-positive-natural
 
105
   (posp (maxf))
 
106
   :rule-classes :type-prescription))
 
107
 
 
108
(defun thf (ndx)
 
109
  (if (and (posp ndx) (<= ndx (maxf))) ndx 1))
 
110
 
 
111
(defthm thf-is-<=-maxf (<= (thf ndx) (maxf)))
 
112
 
 
113
(in-theory (disable thf))
 
114
 
 
115
(defun indexp (i N)
 
116
  (and (posp i) (<= i N) (posp N)))
 
117
 
 
118
(defthm indexp-thf-ndx-maxf
 
119
  (indexp (thf ndx) (maxf)))
 
120
 
 
121
(in-theory (disable indexp))
 
122
 
 
123
 
 
124
(defmacro top (a) `(car ,a))
 
125
(defmacro tag (a) `(cdr ,a))
 
126
 
 
127
(defmacro top+1 (a)
 
128
  `(cons (1+ (top ,a)) (tag ,a)))
 
129
 
 
130
(defmacro top=0 (a)
 
131
  `(cons 0 (tag ,a)))
 
132
 
 
133
(defmacro tag+1 (a)
 
134
  `(cons (top ,a) (1+ (tag ,a))))
 
135
 
 
136
(defmacro agep (a)
 
137
  `(and (natp (top ,a)) (natp (tag ,a))))
 
138
 
 
139
(defun age<< (x y)
 
140
  (or (< (tag x) (tag y))
 
141
      (and (equal (tag x) (tag y))
 
142
           (< (top x) (top y)))))
 
143
 
 
144
 
 
145
(defun mend (bot top mem)
 
146
  (declare (xargs :measure (nfix (- bot top))))
 
147
  (and (integerp bot)
 
148
       (integerp top)
 
149
       (> bot top)
 
150
       (cons (<- mem (1- bot))
 
151
             (mend (1- bot) top mem))))
 
152
 
 
153
 
 
154
(defun val (x) (if (natp x) x 0))
 
155
 
 
156
(defthm val-type-prescription
 
157
  (natp (val x))
 
158
  :rule-classes :type-prescription)
 
159
 
 
160
(in-theory (disable val))
 
161
 
 
162
(defun one-eltp (x)
 
163
  (and (consp x) (atom (rest x))))
 
164
 
 
165
(defun get-top (d)
 
166
  (if (endp (rest d)) 
 
167
      (and (consp d) (val (first d)))
 
168
    (get-top (rest d))))
 
169
 
 
170
(defun drop-top (d)
 
171
  (if (endp (rest d)) 
 
172
      ()
 
173
    (cons (first d) (drop-top (rest d)))))
 
174
 
 
175
(defmacro get-bot (d) `(and (consp ,d) (val (first ,d))))
 
176
 
 
177
(defmacro drop-bot (d) `(rest ,d))
 
178
 
 
179
(defmacro push-bot (x d) `(cons ,x ,d))
 
180
 
 
181
 
 
182
;; various auxiliary theorems about mending and ages ;;
 
183
 
 
184
(defthm mend-bounded-to-bot-top
 
185
  (implies (and (integerp bot) 
 
186
                (integerp x) 
 
187
                (>= x bot))
 
188
           (equal (mend bot top (-> mem x y))
 
189
                  (mend bot top mem))))
 
190
 
 
191
(defthm mend-atom-bot<=top
 
192
  (implies (and (integerp top)
 
193
                (integerp bot))
 
194
           (equal (consp (mend bot top mem))
 
195
                  (> bot top))))
 
196
 
 
197
(defthm get-top-of-mend-is-top
 
198
  (implies (and (integerp bot)
 
199
                (integerp top)
 
200
                (> bot top))
 
201
           (equal (get-top (mend bot top mem))
 
202
                  (val (<- mem top)))))
 
203
 
 
204
(defthm drop-top-mend-is-mend-top1+
 
205
  (implies (and (integerp bot)
 
206
                (integerp top))
 
207
           (equal (drop-top (mend bot top mem))
 
208
                  (mend bot (1+ top) mem))))
 
209
 
 
210
(defthm one-eltp-mend-iff-bot=top+1
 
211
  (implies (and (integerp bot)
 
212
                (integerp top))
 
213
           (equal (one-eltp (mend bot top mem))
 
214
                  (equal bot (1+ top)))))
 
215
 
 
216
(in-theory (disable one-eltp))
 
217
 
 
218
(defthm mend-<=-bot-top-equals-nil
 
219
  (implies (<= bot top)
 
220
           (not (mend bot top mem))))
 
221
 
 
222
(defthm additive-factoid1
 
223
  (implies (and (integerp x) (integerp y))
 
224
           (equal (+ (- x) x y) y)))
 
225
 
 
226
(defthm mend-top+1-unwind-hack
 
227
  (implies (and (equal x (1+ bot)) 
 
228
                (integerp bot)
 
229
                (integerp top) 
 
230
                (<= top bot))
 
231
           (equal (mend x top mem)
 
232
                  (cons (<- mem bot)
 
233
                        (mend bot top mem)))))
 
234
 
 
235
 
 
236
(defthm agep-age<<-top+1
 
237
  (implies (agep a) 
 
238
           (age<< a (top+1 a))))
 
239
 
 
240
(defthm agep-age<<-tag+1-top=0
 
241
  (implies (agep a) 
 
242
           (age<< a (tag+1 (top=0 a)))))
 
243
 
 
244
(defthm age<<-transitive-top+1
 
245
  (implies (age<< a b)
 
246
           (age<< a (top+1 b))))
 
247
 
 
248
(defthm age<<-transitive-tag+1-top=0
 
249
  (implies (age<< a b)
 
250
           (age<< a (tag+1 (top=0 b)))))
 
251
 
 
252
(defthm age<<-irreflexive
 
253
  (not (age<< x x)))
 
254
 
 
255
(defthm age<<-trichotomy
 
256
  (implies (and (agep x) (agep y)
 
257
                (not (age<< y x)))
 
258
           (iff (age<< x y)
 
259
                (not (equal x y)))))
 
260
 
 
261
(defthm age<<-is-asymmetric
 
262
  (implies (age<< a b)
 
263
           (not (age<< b a))))
 
264
 
 
265
(in-theory (disable age<<))
 
266
 
 
267
(defthm agep-implies-top+1-not-equal
 
268
  (implies (agep x) (not (equal x (top+1 x)))))
 
269
 
 
270
(defthm agep-implies-tag+1-top=0-not-equal
 
271
  (implies (agep x) (not (equal x (cons 0 (1+ (cdr x)))))))
 
272
 
 
273
(defthm age<<-top+1-hack1
 
274
  (implies (and (agep a)
 
275
                (equal b (top+1 a)))
 
276
           (age<< a b)))
 
277
 
 
278
(defthm age<<-top+1-hack2
 
279
  (implies (and (age<< a b)
 
280
                (equal c (top+1 b)))
 
281
           (age<< a c)))
 
282
 
 
283
(defthm tag<-implies-age<<
 
284
  (implies (< (tag x) (tag y))
 
285
           (age<< x y))
 
286
  :hints (("Goal" :in-theory (enable age<<))))
 
287
 
 
288
(defthm age<<-implies-tag<=
 
289
  (implies (age<< x y)
 
290
           (<= (tag x) (tag y)))
 
291
  :hints (("Goal" :in-theory (enable age<<)))
 
292
  :rule-classes :forward-chaining)
 
293
 
 
294
(defthm forward-chain-unfortunate
 
295
  (implies (and (<= x y)
 
296
                (equal z (1+ y)))
 
297
           (< x z))
 
298
  :rule-classes :forward-chaining)
 
299
 
 
300
;;;; some macros for defining accessors from records
 
301
 
 
302
(defmacro new (x) `(<- ,x :new))
 
303
(defmacro old (x) `(<- ,x :old))
 
304
(defmacro itm (x) `(<- ,x :itm))
 
305
(defmacro loc (x) `(<- ,x :loc))
 
306
(defmacro emt (x) `(<- ,x :emt))
 
307
(defmacro dtm (x) `(<- ,x :dtm))
 
308
 
 
309
(defmacro bot (x) `(<- ,x :bot))
 
310
(defmacro mem (x) `(<- ,x :mem))
 
311
(defmacro age (x) `(<- ,x :age))
 
312
(defmacro ret (x) `(<- ,x :ret))
 
313
(defmacro deq (x) `(<- ,x :deq))
 
314
(defmacro ctr (x) `(<- ,x :ctr))
 
315
(defmacro one (x) `(<- ,x :one))
 
316
(defmacro clk (x) `(<- ,x :clk))
 
317
 
 
318
(defmacro xitm  (x) `(<- ,x :xitm))
 
319
(defmacro xctr  (x) `(<- ,x :xctr))
 
320
(defmacro xone  (x) `(<- ,x :xone))
 
321
(defmacro xzero (x) `(<- ,x :xzero))
 
322
(defmacro xsafe (x) `(<- ,x :xsafe))
 
323
 
 
324
(defmacro shr (x) `(<- ,x :shr))
 
325
(defmacro tvs (x) `(<- ,x :tvs))
 
326
(defmacro onr (x) `(<- ,x :onr))
 
327
 
 
328
(defmacro ndx (x) `(<- ,x :ndx))
 
329
(defmacro dtm (x) `(<- ,x :dtm))
 
330
(defmacro psh (x) `(<- ,x :psh))
 
331
 
 
332
(defmacro st8 (x) `(<- ,x :st8))
 
333
(defmacro stl (x) `(<- ,x :stl))
 
334
(defmacro xgo (x) `(<- ,x :xgo))
 
335
 
 
336
(defmacro >s  (&rest x) `(update s ,@x))
 
337
(defmacro >f  (&rest x) `(update f ,@x))
 
338
(defmacro >o  (&rest x) `(update o ,@x))
 
339
(defmacro >st (&rest x) `(update st ,@x))
 
340
(defmacro >in (&rest x) `(update in ,@x))
 
341
(defmacro >_  (&rest x) `(update () ,@x))
 
342
 
 
343
;;;; END auxiliary definitions ;;;;
 
344
 
 
345
#|----------------------------------------------------------------------------|#
 
346
 
 
347
;;;; BEGIN cdeq step functions ;;;;
 
348
 
 
349
(defun c-thf-s (f s)
 
350
  (case (loc f)
 
351
        (8  (if (equal (age s) (old f)) 
 
352
                (>s :age (new f))
 
353
              s))
 
354
        (10 (>s :ret (itm f) :clk (1+ (clk s))))
 
355
        (t  s)))
 
356
 
 
357
(defun c-thf-f (f s)
 
358
  (case (loc f)
 
359
        (0  (>f :loc 1))
 
360
        (1  (>f :loc 2 :old (age s)))
 
361
        (2  (>f :loc 3 :bot (bot s)))
 
362
        (3  (>f :loc (if (> (bot f) (top (old f))) 5 4)))
 
363
        (4  (>f :loc 0 :ret nil))
 
364
        (5  (>f :loc 6 :itm (val (<- (mem s) (top (old f))))))
 
365
        (6  (>f :loc 7 :new (old f)))                    
 
366
        (7  (>f :loc 8 :new (top+1 (new f))))            
 
367
        (8  (>f :loc 9 :new (if (equal (age s) (old f)) 
 
368
                                 (age s) (new f))))
 
369
        (9  (>f :loc (if (equal (old f) (new f)) 10 11)))
 
370
        (10 (>f :loc 0 :ret (itm f)))
 
371
        (11 (>f :loc 0 :ret nil))
 
372
        (t  (>f :loc 0))))                        
 
373
 
 
374
(defun c-onr-s (o s)
 
375
  (case (loc o)
 
376
        (5  (>s :bot (bot o)))
 
377
        (9  (>s :ret (itm o) :clk (1+ (clk s))))
 
378
        (10 (>s :bot 0))
 
379
        (14 (if (equal (age s) (old o))
 
380
                (>s :age (new o))
 
381
              s))
 
382
        (16 (>s :ret (itm o) :clk (1+ (clk s))))
 
383
        (17 (>s :age (new o)))
 
384
        (20 (>s :mem (-> (mem s) (bot o) (dtm o))))
 
385
        (22 (>s :bot (bot o)))
 
386
        (t  s)))
 
387
 
 
388
(defun c-onr-o (p d o s)
 
389
  (case (loc o)
 
390
        (0  (if p (>o :loc 19 :dtm d) 
 
391
              (>o :loc 1)))
 
392
        (1  (>o :loc 2 :bot (bot s)))
 
393
        (2  (>o :loc (if (= (bot o) 0) 3 4)))
 
394
        (3  (>o :loc 0 :ret nil))
 
395
        (4  (>o :loc 5 :bot (1- (bot o))))
 
396
        (5  (>o :loc 6))
 
397
        (6  (>o :loc 7 :itm (val (<- (mem s) (bot o)))))
 
398
        (7  (>o :loc 8 :old (age s)))
 
399
        (8  (>o :loc (if (> (bot o) (top (old o))) 9 10)))
 
400
        (9  (>o :loc 0 :ret (itm o)))
 
401
        (10 (>o :loc 11))                                  
 
402
        (11 (>o :loc 12 :new (top=0 (old o))))             
 
403
        (12 (>o :loc 13 :new (tag+1 (new o))))             
 
404
        (13 (>o :loc (if (= (bot o) (top (old o))) 14 17)))
 
405
        (14 (>o :loc 15 :new (if (equal (age s) (old o))
 
406
                                 (age s) (new o))))
 
407
        (15 (>o :loc (if (equal (old o) (new o)) 16 17)))
 
408
        (16 (>o :loc 0 :ret (itm o)))
 
409
        (17 (>o :loc 18))
 
410
        (18 (>o :loc 0 :ret nil))
 
411
        (19 (>o :loc 20 :bot (bot s)))                     
 
412
        (20 (>o :loc 21))                                    
 
413
        (21 (>o :loc 22 :bot (1+ (bot o))))                
 
414
        (t  (>o :loc 0))))
 
415
 
 
416
(DEFUN cdeq (st in)
 
417
  (let* ((ndx (thf (ndx in)))
 
418
         (dtm (dtm in))
 
419
         (psh (psh in))
 
420
         (tvs (tvs st))
 
421
         (shr (shr st))
 
422
         (onr (onr st))
 
423
         (thf (<- tvs ndx)))
 
424
    (if (ndx in)
 
425
        (>st :tvs (-> tvs ndx (c-thf-f thf shr))
 
426
             :shr (c-thf-s thf shr))
 
427
      (>st :onr (c-onr-o psh dtm onr shr)
 
428
           :shr (c-onr-s onr shr)))))
 
429
 
 
430
;;;; END cdeq step functions ;;;;
 
431
 
 
432
#|----------------------------------------------------------------------------|#
 
433
 
 
434
;;;; BEGIN cdeq+ step functions ;;;;
 
435
 
 
436
(defun i-thf-s (f s)
 
437
  (case (loc f)
 
438
        (8  (if (equal (age s) (old f)) 
 
439
                (>s :age (new f)
 
440
                    :xctr (1+ (xctr s)))
 
441
              s))
 
442
        (10 (>s :ret (itm f) :clk (1+ (clk s))))
 
443
        (t  s)))
 
444
 
 
445
(defun i-thf-f (f s)
 
446
  (case (loc f)
 
447
        (0  (>f :loc 1))                                  
 
448
        (1  (>f :loc 2 
 
449
                :old (age s) 
 
450
                :xctr (xctr s)))
 
451
        (2  (>f :loc 3 
 
452
                :bot (bot s) 
 
453
                :xitm (and (> (bot s) (top (age s)))
 
454
                           (val (<- (mem s) (top (age s)))))))
 
455
        (3  (>f :loc (if (> (bot f) (top (old f))) 5 4)))
 
456
        (4  (>f :loc 0 :ret nil))
 
457
        (5  (>f :loc 6 :itm (val (<- (mem s) (top (old f))))))
 
458
        (6  (>f :loc 7 :new (old f)))                    
 
459
        (7  (>f :loc 8 :new (top+1 (new f))))            
 
460
        (8  (>f :loc 9 :new (if (equal (age s) (old f)) 
 
461
                                (age s) (new f))))
 
462
        (9  (>f :loc (if (equal (old f) (new f)) 10 11)))
 
463
        (10 (>f :loc 0 :ret (itm f)))
 
464
        (11 (>f :loc 0 :ret nil))
 
465
        (t  (>f :loc 0))))
 
466
 
 
467
(defun i-onr-s (o s)
 
468
  (case (loc o)
 
469
        (5  (>s :bot (bot o)
 
470
                :xsafe (<= (bot o) (top (age s)))))
 
471
        (7  (>s :xsafe (<= (bot s) (top (age s)))))
 
472
        (9  (>s :ret (itm o) :clk (1+ (clk s))))
 
473
        (10 (>s :bot 0))
 
474
        (14 (if (equal (age s) (old o))
 
475
                (>s :age (new o)
 
476
                    :xctr (1+ (xctr s))
 
477
                    :xsafe nil)
 
478
              s))
 
479
        (16 (>s :ret (itm o) :clk (1+ (clk s))))
 
480
        (17 (>s :age (new o)
 
481
                :xctr (1+ (xctr s))
 
482
                :xsafe nil))
 
483
        (20 (>s :mem (-> (mem s) (bot o) (dtm o))))
 
484
        (22 (>s :bot (bot o)))
 
485
        (t  s)))
 
486
 
 
487
(defun i-onr-o (p d o s)
 
488
  (case (loc o)
 
489
        (0  (if p (>o :loc 19 :dtm d) 
 
490
              (>o :loc 1)))
 
491
        (1  (let ((o (>o :loc 2 :bot (bot s))))
 
492
              (if (= (bot s) 0)
 
493
                  (>o :xitm nil)
 
494
                o)))
 
495
        (2  (>o :loc (if (= (bot o) 0) 3 4)))
 
496
        (3  (>o :loc 0 :ret nil :xzero t))
 
497
        (4  (>o :loc 5 :bot (1- (bot o))))
 
498
        (5  (>o :loc 6  
 
499
                :xitm (and (>= (bot o) (top (age s)))
 
500
                           (val (<- (mem s) (bot o))))
 
501
                :xctr (and (= (bot o) (top (age s)))
 
502
                           (xctr s))))
 
503
        (6  (>o :loc 7 :itm (val (<- (mem s) (bot o)))))
 
504
        (7  (>o :loc 8 
 
505
                :old (age s)
 
506
                :xitm (and (>= (bot o) (top (age s)))
 
507
                           (xitm o))
 
508
                :xctr (if (and (not (xctr o))
 
509
                               (= (bot o) (top (age s))))
 
510
                          (xctr s)
 
511
                        (xctr o))))
 
512
        (8  (if (> (bot o) (top (old o)))
 
513
                (>o :loc 9 :xctr nil :xzero nil)
 
514
              (>o :loc 10)))
 
515
        (9  (>o :loc 0 :ret (itm o)))
 
516
        (10 (>o :loc 11))                                  
 
517
        (11 (>o :loc 12 :new (top=0 (old o))))             
 
518
        (12 (>o :loc 13 :new (tag+1 (new o))))             
 
519
        (13 (>o :loc (if (= (bot o) (top (old o))) 14 17)))
 
520
        (14 (let ((o (>o :loc 15)))
 
521
              (if (equal (age s) (old o))
 
522
                  (>o :new (age s)
 
523
                      :xctr nil
 
524
                      :xzero t)
 
525
                o)))              
 
526
        (15 (>o :loc (if (equal (old o) (new o)) 16 17)))
 
527
        (16 (>o :loc 0 :ret (itm o)))
 
528
        (17 (>o :loc 18 :xctr nil :xzero t))
 
529
        (18 (>o :loc 0 :ret nil))
 
530
        (19 (>o :loc 20 :bot (bot s)))                     
 
531
        (20 (>o :loc 21))                                    
 
532
        (21 (>o :loc 22 :bot (1+ (bot o))))
 
533
        (22 (>o :loc 0  :xzero nil))
 
534
        (t  (>o :loc 0))))
 
535
 
 
536
(DEFUN cdeq+ (st in)
 
537
  (let* ((ndx (thf (ndx in)))
 
538
         (dtm (dtm in))
 
539
         (psh (psh in))
 
540
         (tvs (tvs st))
 
541
         (shr (shr st))
 
542
         (onr (onr st))
 
543
         (thf (<- tvs ndx)))
 
544
    (if (ndx in)
 
545
        (>st :tvs (-> tvs ndx (i-thf-f thf shr))
 
546
             :shr (i-thf-s thf shr))
 
547
      (>st :onr (i-onr-o psh dtm onr shr)
 
548
           :shr (i-onr-s onr shr)))))
 
549
 
 
550
;;;; END cdeq+ step functions ;;;;
 
551
 
 
552
#|----------------------------------------------------------------------------|#
 
553
 
 
554
;;;; BEGIN intr step functions ;;;;
 
555
 
 
556
(defun m-thf-s (f s)
 
557
  (case (loc f)
 
558
        (2 (if (and (itm f)
 
559
                    (= (ctr f) (ctr s)))
 
560
               (>s :deq (drop-top (deq s))
 
561
                   :ctr (1+ (ctr s)))
 
562
             s))
 
563
        (3 (>s :ret (itm f) :clk (1+ (clk s))))
 
564
        (t s)))
 
565
 
 
566
(defun m-thf-f (f s)
 
567
  (case (loc f)
 
568
        ;; popTop
 
569
        (0 (>f :loc 1 :ctr (ctr s)))
 
570
        (1 (>f :loc 2 :itm (get-top (deq s))))
 
571
        (2 (>f :loc (if (and (itm f)
 
572
                             (= (ctr s) (ctr f)))
 
573
                        3 0)))
 
574
        (t (>f :loc 0))))
 
575
 
 
576
(defun m-onr-s (o s)
 
577
  (case (loc o)
 
578
        (1 (>s :deq (drop-bot (deq s))))
 
579
        (3 (if (or (= (ctr o) (ctr s))
 
580
                   (and (atom (deq s))
 
581
                        (implies (itm o) (ctr o))
 
582
                        (not (xzero o))))
 
583
               (>s :ctr (1+ (ctr s)))
 
584
             s))
 
585
        (4 (>s :ret (itm o) :clk (1+ (clk s))))
 
586
        (5 (>s :deq (push-bot (dtm o) (deq s))))
 
587
        (t s)))
 
588
 
 
589
(defun m-onr-o (p d o s)
 
590
  (case (loc o)
 
591
        (0 (if p (>o :loc 5 :dtm d)
 
592
             (>o :loc 1)))
 
593
        ;; popBottom
 
594
        (1 (>o :loc 2 
 
595
               :itm (get-bot (deq s))
 
596
               :ctr (and (one-eltp (deq s))
 
597
                         (ctr s))))
 
598
        (2 (let ((o (>o :loc 3)))
 
599
             (cond ((or (not (itm o))
 
600
                        (consp (deq s))
 
601
                        (= (ctr o) (ctr s)))
 
602
                    o)
 
603
                   ((not (ctr o)) (>o :ctr (ctr s)))
 
604
                   (t (>o :itm nil)))))
 
605
        (3 (>o :loc (if (and (itm o)
 
606
                             (implies (ctr o)
 
607
                                      (= (ctr o) (ctr s))))
 
608
                        4 0)
 
609
               :xzero (implies (itm o) (ctr o))
 
610
               :ctr nil))
 
611
        (5 (>o :loc 0 :xzero nil))
 
612
        ;; pushBottom
 
613
        (t (>o :loc 0))))
 
614
 
 
615
(DEFUN intr (st in)
 
616
  (let* ((ndx (thf (ndx in)))
 
617
         (dtm (dtm in))
 
618
         (psh (psh in))
 
619
         (tvs (tvs st))
 
620
         (shr (shr st))
 
621
         (onr (onr st))
 
622
         (thf (<- tvs ndx)))
 
623
    (if (ndx in)
 
624
        (>st :tvs (-> tvs ndx (m-thf-f thf shr))
 
625
             :shr (m-thf-s thf shr))
 
626
      (>st :onr (m-onr-o psh dtm onr shr)
 
627
           :shr (m-onr-s onr shr)))))
 
628
 
 
629
;;;; END intr step functions ;;;;
 
630
 
 
631
#|----------------------------------------------------------------------------|#
 
632
 
 
633
;;;; BEGIN intr+ step functions ;;;;
 
634
 
 
635
(defun r-thf-s (f s)
 
636
  (case (loc f)
 
637
        (2 (if (and (itm f)
 
638
                    (= (ctr f) (ctr s)))
 
639
               (>s :deq (drop-top (deq s))
 
640
                   :ctr (1+ (ctr s)))
 
641
             s))
 
642
        (3 (>s :ret (itm f) :clk (1+ (clk s))))
 
643
        (t s)))
 
644
 
 
645
(defun r-thf-f (f s)
 
646
  (let ((f (>f :xgo 
 
647
               (and (consp (deq s))
 
648
                    (or (= (loc f) 0) 
 
649
                        (xgo f))))))
 
650
    (case (loc f)
 
651
          ;; popTop
 
652
          (0 (>f :loc 1 :ctr (ctr s)))
 
653
          (1 (>f :loc 2 :itm (get-top (deq s))))
 
654
          (2 (>f :loc (if (and (itm f)
 
655
                               (= (ctr s) (ctr f)))
 
656
                          3 0)))
 
657
          (t (>f :loc 0)))))
 
658
 
 
659
(defun r-onr-s (o s)
 
660
  (case (loc o)
 
661
        (1 (>s :deq (drop-bot (deq s))))
 
662
        (3 (if (or (= (ctr o) (ctr s))
 
663
                   (and (atom (deq s)) 
 
664
                        (implies (itm o) (ctr o))
 
665
                        (not (xzero o))))
 
666
               (>s :ctr (1+ (ctr s)))
 
667
             s))
 
668
        (4 (>s :ret (itm o) :clk (1+ (clk s))))
 
669
        (5 (>s :deq (push-bot (dtm o) (deq s))))
 
670
        (t s)))
 
671
 
 
672
(defun r-onr-o (p d o s)
 
673
  (case (loc o)
 
674
        (0 (if p (>o :loc 5 :dtm d)
 
675
             (>o :loc 1)))
 
676
        ;; popBottom
 
677
        (1 (>o :loc 2 
 
678
               :itm (get-bot (deq s))
 
679
               :ctr (and (one-eltp (deq s))
 
680
                         (ctr s))))
 
681
        (2 (let ((o (>o :loc 3)))
 
682
             (cond ((or (not (itm o))
 
683
                        (consp (deq s))
 
684
                        (= (ctr o) (ctr s)))
 
685
                    o)
 
686
                   ((not (ctr o)) (>o :ctr (ctr s)))
 
687
                   (t (>o :itm nil)))))
 
688
        (3 (>o :loc (if (and (itm o)
 
689
                             (implies (ctr o)
 
690
                                      (= (ctr o) (ctr s))))
 
691
                        4 0)
 
692
               :xzero (implies (itm o) (ctr o))
 
693
               :ctr nil))
 
694
        (5 (>o :loc 0 :xzero nil))
 
695
        ;; pushBottom
 
696
        (t (>o :loc 0))))
 
697
 
 
698
(DEFUN intr+ (st in)
 
699
  (let* ((ndx (thf (ndx in)))
 
700
         (dtm (dtm in))
 
701
         (psh (psh in))
 
702
         (tvs (tvs st))
 
703
         (shr (shr st))
 
704
         (onr (onr st))
 
705
         (thf (<- tvs ndx)))
 
706
    (if (ndx in)
 
707
        (>st :tvs (-> tvs ndx (r-thf-f thf shr))
 
708
             :shr (r-thf-s thf shr))
 
709
      (>st :onr (r-onr-o psh dtm onr shr)
 
710
           :shr (r-onr-s onr shr)))))
 
711
 
 
712
;;;; END intr+ step functions ;;;;
 
713
 
 
714
#|----------------------------------------------------------------------------|#
 
715
 
 
716
;;;; BEGIN spec step function ;;;;
 
717
 
 
718
(DEFUN spec (st in)
 
719
  (let ((ndx (thf (ndx in)))
 
720
        (dtm (dtm in))
 
721
        (tvs (tvs st))
 
722
        (s (shr st))
 
723
        (o (onr st))
 
724
        (deq (deq (shr st))))
 
725
    (if (ndx in)
 
726
        (cond ((<- tvs ndx)
 
727
               (>st :tvs (-> tvs ndx nil)
 
728
                    :shr (>s :ret (<- tvs ndx)
 
729
                             :clk (1+ (clk s)))))
 
730
              ((and (itm o) (equal (st8 o) 'pop)
 
731
                    (atom deq) (stl in))
 
732
               (>st :tvs (-> tvs ndx (itm o))
 
733
                    :onr (>o :itm nil)))
 
734
              (t
 
735
               (>st :tvs (-> tvs ndx (get-top deq))
 
736
                    :shr (>s :deq (drop-top deq)))))
 
737
      (case (st8 o)
 
738
            (push (>st :onr (>o :st8 'idle)
 
739
                       :shr (>s :deq (push-bot (dtm o) deq))))
 
740
            (pop  (if (itm o)
 
741
                      (>st :onr (>o :st8 'idle :itm nil)
 
742
                           :shr (>s :ret (itm o) 
 
743
                                    :clk (1+ (clk s))))
 
744
                    (>st :onr (>o :st8 'idle))))
 
745
            (idle (if (psh in)
 
746
                      (>st :onr (>o :st8 'push :dtm dtm))
 
747
                    (>st :onr (>o :st8 'pop :itm (get-bot deq))
 
748
                         :shr (>s :deq (drop-bot deq)))))))))
 
749
 
 
750
;;;; END spec step function ;;;;
 
751
 
 
752
#|----------------------------------------------------------------------------|#
 
753
 
 
754
;;;; BEGIN label function ;;;;
 
755
 
 
756
(DEFUN label (st)
 
757
  (list (ret (shr st)) 
 
758
        (clk (shr st)) 
 
759
        (dtm (onr st))))
 
760
 
 
761
;;;; END label function ;;;;
 
762
 
 
763
#|----------------------------------------------------------------------------|#
 
764