← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/acl2s/defdata/base.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/acl2s/defdata/base.lisp
 
1
#|$ACL2s-Preamble$;
 
2
(include-book ;; Newline to fool ACL2/cert.pl dependency scanner
 
3
 "../portcullis")
 
4
(acl2::begin-book t);$ACL2s-Preamble$|#
 
5
 
 
6
;; [Jared] Marking this book as non-acl2(r) because it attempts to prove:
 
7
;;
 
8
;; (DEFTHM COMMON-LISP::COMPLEX-CONSTRUCTOR-DESTRUCTORS
 
9
;;          (IMPLIES (ACL2-NUMBERP X)
 
10
;;                   (AND (RATIONALP (REALPART X))
 
11
;;                        (RATIONALP (IMAGPART X))))
 
12
;;          :HINTS NIL
 
13
;;          :RULE-CLASSES NIL)
 
14
;;
 
15
;; which, I think, is not a theorem in ACL2(r).
 
16
 
 
17
; cert_param: (non-acl2r)
 
18
 
 
19
(in-package "ACL2S")
 
20
 
 
21
(include-book "splitnat")
 
22
(include-book "switchnat")
 
23
 
 
24
(include-book "defdata-core")
 
25
(include-book "random-state")
 
26
(include-book "enumerators-gen")
 
27
 
 
28
(include-book "library-support")
 
29
 
 
30
(include-book "register-data-constructor")
 
31
(include-book "register-type")
 
32
 
 
33
(include-book "register-combinator")
 
34
(include-book "listof")
 
35
(include-book "alistof")
 
36
(include-book "tau-characterization")
 
37
 
 
38
(include-book "tools/rulesets" :dir :system)
 
39
 
 
40
(include-book "var-book")
 
41
 
 
42
;; (make-event ;TODO make sure to get this working
 
43
;;  (er-progn
 
44
;;   (defdata::set-acl2s-defdata-verbose t)
 
45
;;   (value '(value-triple :invisible)))
 
46
;;  :check-expansion t)
 
47
 
 
48
(defun allp (x)
 
49
  (declare (xargs :mode :logic
 
50
                  :guard t)
 
51
           (ignore x))
 
52
  t)
 
53
 
 
54
;; (defthm allp-is-tau-predicate
 
55
;;   (booleanp (allp x))
 
56
;;   :rule-classes :tau-system)
 
57
 
 
58
;; (defthm allp-is-t
 
59
;;   (equal (allp x) t)
 
60
;;   :rule-classes (:rewrite))
 
61
 
 
62
(in-theory (disable allp))
 
63
 
 
64
; 18 Aug 2014.
 
65
; ALLP aliases TAU explicitly disallows predicates that hide equality to a
 
66
; constant. In particular it does not like the everywhere-true and
 
67
; everywhere-false predicates. So we built special support for these. We will
 
68
; store all aliases of allp in a table. This will be used by subtype-p and
 
69
; disjoint-p functions. Recall that we have given up homebrew datatype
 
70
; relationship graphs in favor of its implicit coding in TAU-DATABASE.
 
71
(table allp-aliases nil)
 
72
(table allp-aliases 'allp 'all :put) ;all will be registered as a defdata type below.
 
73
 
 
74
 
 
75
 
 
76
 
 
77
;; NOTE: ALL should not be used in subtype/disjoint relations
 
78
;; because of a caveat in tau
 
79
 
 
80
;;type constructors == product types
 
81
;;rational number constructor
 
82
;;pair constructor
 
83
(register-data-constructor (consp cons)
 
84
                           ((allp car) (allp cdr))
 
85
                           :rule-classes nil
 
86
                           :verbose t)
 
87
                
 
88
 
 
89
;;jared's oset implementation
 
90
;; (defun set::non-empty-setp (x)
 
91
;;   (declare (xargs :guard t))
 
92
;;   (and (set::setp x)
 
93
;;        (not (set::empty x))))
 
94
 
 
95
;; (register-data-constructor (SET::non-empty-setp SET::insert)
 
96
;;                            ((allp SET::head) (set::setp SET::tail))
 
97
;;                            :proper nil)
 
98
 
 
99
 
 
100
;;symbols
 
101
(register-data-constructor (symbolp intern$)
 
102
                           ((stringp symbol-name) (stringp symbol-package-name))
 
103
                           :rule-classes nil
 
104
                           :proper nil) ;package name destructor fails
 
105
 
 
106
 
 
107
 
 
108
(register-data-constructor (rationalp /)
 
109
                           ((integerp numerator) (posp denominator))
 
110
                           :rule-classes nil
 
111
                           :proper nil)
 
112
 
 
113
 
 
114
 
 
115
 
 
116
;;complex number type
 
117
(register-data-constructor (acl2-numberp complex)
 
118
                           ((rationalp realpart) (rationalp imagpart))
 
119
                           :rule-classes nil
 
120
                           )
 
121
 
 
122
 
 
123
#||
 
124
;;natural numbers
 
125
(defexec succ (x)
 
126
  (declare (xargs :guard (natp x)))
 
127
  (mbe :logic
 
128
       (if (natp x)
 
129
         (1+ x)
 
130
         1)
 
131
       :exec (1+ x)))
 
132
 
 
133
(defun pred (x)
 
134
  (declare (xargs :guard (natp x)))
 
135
  (if (zp x)
 
136
    0
 
137
    (1- x)))
 
138
 
 
139
(defthm succ-pred
 
140
  (implies (posp x)
 
141
           (equal (succ (pred x)) x)))
 
142
 
 
143
(register-data-constructor (posp succ)
 
144
                           (pred))
 
145
||#
 
146
 
 
147
 
 
148
;;characters
 
149
 
 
150
(defconst *character-values* *standard-chars*)
 
151
 
 
152
(defconst *len-character-values* (len *character-values*))
 
153
 
 
154
(defconst *alpha-chars*
 
155
  '(#\A #\B #\C #\D #\E #\F #\G
 
156
    #\H #\I #\J #\K #\L #\M #\N #\O #\P #\Q
 
157
    #\R #\S #\T #\U #\V #\W #\X #\Y #\Z
 
158
    #\a #\b #\c
 
159
    #\d #\e #\f #\g #\h #\i #\j #\k #\l #\m
 
160
    #\n #\o #\p #\q #\r #\s #\t #\u #\v #\w
 
161
    #\x #\y #\z     ))
 
162
 
 
163
(defconst *len-alpha-chars* (len *alpha-chars*))
 
164
 
 
165
(defconst *alpha-low-chars*
 
166
  '(#\a #\b #\c
 
167
    #\d #\e #\f #\g #\h #\i #\j #\k #\l #\m
 
168
    #\n #\o #\p #\q #\r #\s #\t #\u #\v #\w
 
169
    #\x #\y #\z 
 
170
    ))
 
171
 
 
172
(defconst *len-alpha-low-chars* (len *alpha-low-chars*))
 
173
 
 
174
(defconst *alpha-up-chars*
 
175
  '(#\A #\B #\C #\D #\E #\F #\G
 
176
    #\H #\I #\J #\K #\L #\M #\N #\O #\P #\Q
 
177
    #\R #\S #\T #\U #\V #\W #\X #\Y #\Z
 
178
    ))
 
179
 
 
180
(defconst *len-alpha-up-chars* (len *alpha-up-chars*))
 
181
 
 
182
(defconst *alpha-num-chars*
 
183
  '(#\A #\B #\C #\D #\E #\F #\G
 
184
    #\H #\I #\J #\K #\L #\M #\N #\O #\P #\Q
 
185
    #\R #\S #\T #\U #\V #\W #\X #\Y #\Z
 
186
    #\0 #\1 #\2 #\3 #\4 #\5 #\6 #\7 #\8 #\9
 
187
    #\a #\b #\c
 
188
    #\d #\e #\f #\g #\h #\i #\j #\k #\l #\m
 
189
    #\n #\o #\p #\q #\r #\s #\t #\u #\v #\w
 
190
    #\x #\y #\z
 
191
    ))
 
192
 
 
193
(defconst *len-alpha-num-chars* (len *alpha-num-chars*))
 
194
 
 
195
 
 
196
(defthm integerp-mod
 
197
    (implies (and (integerp m)
 
198
                  (integerp n))
 
199
             (integerp (mod m n)))
 
200
  :rule-classes (:rewrite :type-prescription))
 
201
 
 
202
(encapsulate 
 
203
 nil
 
204
 (local (include-book "arithmetic-5/top" :dir :system))
 
205
 
 
206
 (defthm mod-nonnegative-integer-args
 
207
   (implies (and (integerp x)
 
208
                 (integerp y)
 
209
                 (< 0 y))
 
210
            (<= 0 (mod x y)))
 
211
   :rule-classes ((:rewrite :backchain-limit-lst 1)
 
212
                  (:type-prescription)))
 
213
 
 
214
 
 
215
(defun get-character-list-from-positions (l)
 
216
  (declare (xargs :guard (nat-listp l)))
 
217
                  ;:verify-guards nil))
 
218
  (if (endp l)
 
219
    nil
 
220
    (let* ((pos (mod (car l) (len *alpha-num-chars*)))
 
221
           (char (nth pos *alpha-num-chars*)))
 
222
      (cons char (get-character-list-from-positions (cdr l))))))
 
223
 
 
224
(defun get-standard-char-list-from-positions (l)
 
225
  (declare (xargs :guard (nat-listp l)))
 
226
  (if (endp l)
 
227
    nil
 
228
    (let* ((pos (mod (car l) (len *standard-chars*)))
 
229
           (char (nth pos *standard-chars*)))
 
230
      (cons char (get-standard-char-list-from-positions (cdr l))))))
 
231
 
 
232
(defthm get-character-list-from-positions--character-listp
 
233
  (implies (nat-listp l)
 
234
           (and (character-listp (get-character-list-from-positions l))
 
235
                (character-listp (get-standard-char-list-from-positions l))))
 
236
  :hints (("goal" :in-theory (enable standard-char-listp))))
 
237
 
 
238
)
 
239
(in-theory (disable mod))
 
240
;;booleans
 
241
 
 
242
(defconst *boolean-values* '(t nil))
 
243
(defun nth-boolean (n) (nth (mod n 2) *boolean-values*))
 
244
;(define-enumeration-type boolean '(t nil))
 
245
 
 
246
 
 
247
 
 
248
;-------- define some enumerators --------;
 
249
 
 
250
(defun nth-nat (n)
 
251
  (declare (xargs :guard (natp n)))
 
252
  n)
 
253
 
 
254
(defun nat-index (n)
 
255
  (declare (xargs :guard (natp n)))
 
256
  n)
 
257
 
 
258
(defthm nth-nat-index
 
259
  (equal (nat-index (nth-nat n))
 
260
         n))
 
261
 
 
262
(defthm nat-index-nth
 
263
  (equal (nth-nat (nat-index n))
 
264
         n))
 
265
 
 
266
 
 
267
(defexec nth-pos (n)
 
268
  (declare (xargs :guard (natp n)))
 
269
  (mbe :logic
 
270
       (if (natp n)
 
271
         (1+ n)
 
272
         n)
 
273
       :exec (1+ n)))
 
274
 
 
275
(defthm nth-pos-is-posp
 
276
  (implies (natp x)
 
277
           (posp (nth-pos x)))
 
278
  :hints (("goal" :in-theory (enable nth-pos)))
 
279
  :rule-classes (:rewrite :type-prescription))
 
280
 
 
281
(defexec pos-index (i)
 
282
  (declare (xargs :guard (posp i)))
 
283
  (mbe :logic
 
284
       (if (posp i)
 
285
         (1- i)
 
286
         i)
 
287
       :exec (1- i)))
 
288
 
 
289
(defthm nth-pos-index
 
290
  (equal (pos-index (nth-pos n))
 
291
         n))
 
292
 
 
293
(defthm pos-index-nth
 
294
  (implies (and (integerp i)
 
295
                (>= i 1))
 
296
           (equal (nth-pos (pos-index i))
 
297
                  i)))
 
298
 
 
299
 
 
300
(defun pos-multiple-of-threep (v)
 
301
  (if (posp v)
 
302
    (equal 0 (mod v 3))
 
303
    nil)) 
 
304
(defun nth-pos-multiple-of-three (n)
 
305
 (if (natp n) 
 
306
   (* 3 (1+ n))
 
307
   3))
 
308
 
 
309
(defun pos-multiple-of-three-index (i)
 
310
  (if (pos-multiple-of-threep i)
 
311
         (1- (floor i 3))
 
312
         i))
 
313
 
 
314
;;integers
 
315
(defun nth-integer (n)
 
316
  (declare (xargs :guard (natp n)))
 
317
  (let* (;(n (mod n 1000))
 
318
         (mag (floor n 2))
 
319
        (sign (rem n 2)))
 
320
    (if (= sign 0)
 
321
      mag
 
322
      (- -1 mag))))
 
323
 
 
324
(defun nth-integer-between (n lo hi)
 
325
  (declare (xargs :guard (and (natp n)
 
326
                              (integerp lo)
 
327
                              (integerp hi))))
 
328
  (let ((range (nfix (- hi lo))))
 
329
    (+ lo (mod n (1+ range)))))
 
330
 
 
331
(defun integer-index (i)
 
332
  (declare (xargs :guard (integerp i)))
 
333
  (if (< i 0)
 
334
    (1+ (* (- (1+ i)) 2))
 
335
    (* i 2)))
 
336
#||
 
337
(encapsulate nil
 
338
  (local 
 
339
   (include-book "arithmetic-5/top" :dir :system))
 
340
 
 
341
  (defthm nth-pos-multiple-three-type
 
342
    (pos-multiple-of-threep (nth-pos-multiple-of-three n)))
 
343
  
 
344
  
 
345
  (defthm nth-pos-multiple-of-three-index
 
346
    (implies (natp n)
 
347
             (equal (pos-multiple-of-three-index (nth-pos-multiple-of-three n))
 
348
                    n)))
 
349
  
 
350
  (defthm pos-multiple-of-three-index-nth
 
351
    (implies (pos-multiple-of-threep i)
 
352
             (equal (nth-pos-multiple-of-three (pos-multiple-of-three-index i))
 
353
                    i)))    
 
354
 
 
355
  
 
356
  (defthm nth-integer-index
 
357
    (implies 
 
358
     (and (integerp n)
 
359
          (>= n 0))
 
360
     (equal (integer-index (nth-integer n))
 
361
            n)))
 
362
  (defthm integer-index-nth
 
363
    (implies 
 
364
     (integerp i)
 
365
     (equal (nth-integer (integer-index i))
 
366
            i))))
 
367
||#
 
368
 
 
369
;;only strings upto len 1 to 8
 
370
(defun nth-string (n)
 
371
  (declare (xargs :guard (natp n)))
 
372
                  ;:verify-guards nil))
 
373
  (let* ((str-len (1+ (mod n 7)))
 
374
         (char-pos-list (defdata::split-nat str-len n))
 
375
         (charlist (get-character-list-from-positions char-pos-list)))
 
376
    (coerce charlist 'string)))
 
377
 
 
378
(defun standard-stringp (x)
 
379
  (declare (xargs :guard t))
 
380
  (and (stringp x)
 
381
       (standard-char-listp (coerce x 'list))))
 
382
 
 
383
(defun nth-standard-string (n)
 
384
  (declare (xargs :guard (natp n)))
 
385
                  ;:verify-guards nil))
 
386
  (let* ((str-len (1+ (mod n 7)))
 
387
         (char-pos-list (defdata::split-nat str-len n))
 
388
         (charlist (get-standard-char-list-from-positions char-pos-list)))
 
389
    (coerce charlist 'string)))
 
390
 
 
391
(encapsulate 
 
392
 ((nth-symbol (n) t :guard (natp n)))
 
393
 (local (defun nth-symbol (n)
 
394
          (declare (xargs :guard (natp n)))
 
395
          (declare (ignore n))
 
396
          'a)))
 
397
 
 
398
(defun nth-symbol-builtin (n)
 
399
  (declare (xargs :guard (natp n)))
 
400
                 ;:verify-guards nil)) 
 
401
  (intern$ (nth-string n) "ACL2"))
 
402
 
 
403
(defattach nth-symbol nth-symbol-builtin)
 
404
 
 
405
(encapsulate 
 
406
 ((nth-character (n) t :guard (natp n)))
 
407
 (local (defun nth-character (n)
 
408
          (declare (xargs :guard (natp n)))
 
409
          (declare (ignore n))
 
410
          '#\A)))
 
411
 
 
412
(defun nth-character-builtin (n)
 
413
  (declare (xargs :guard (natp n)))
 
414
  (nth (mod n *len-character-values*) *character-values*))
 
415
 
 
416
(defattach nth-character nth-character-builtin)
 
417
 
 
418
(defun nth-alpha-num-character (n)
 
419
  (declare (xargs :guard (natp n)))
 
420
  (nth (mod n *len-alpha-num-chars*) *alpha-num-chars*))
 
421
 
 
422
 
 
423
(defun positive-ratiop (x)
 
424
  (declare (xargs :guard t))
 
425
  (and (rationalp x)
 
426
       (not (integerp x))
 
427
       (> x 0)
 
428
       ))
 
429
 
 
430
(defun nth-positive-ratio (n)
 
431
  (declare (xargs :guard (natp n)))
 
432
  (mbe :logic (if (natp n)
 
433
                 (let* ((two-n-list (defdata::split-nat 2 n))
 
434
                        (alpha  (car two-n-list))
 
435
                        (beta (cadr two-n-list))
 
436
                        (den (+ 2 alpha))
 
437
                        (num (+ (floor beta den) beta)))
 
438
                   (/ num den))
 
439
                 (/ 1 2))
 
440
       :exec (let* ((two-n-list (defdata::split-nat 2 n))
 
441
                    (alpha  (car two-n-list))
 
442
                    (beta (cadr two-n-list))
 
443
                    (den (+ 2 alpha))
 
444
                    (num (+ (floor beta den) beta)))
 
445
               (/ num den))))
 
446
 
 
447
 
 
448
 
 
449
(defun negative-ratiop (x)
 
450
  (declare (xargs :guard t))
 
451
  (and (rationalp x)
 
452
       (not (integerp x))
 
453
       (< x 0)
 
454
       ))
 
455
 
 
456
 
 
457
(defun nth-negative-ratio (n)
 
458
  (declare (xargs :guard (natp n)))
 
459
  (let* ((two-n-list (defdata::split-nat 2 n))
 
460
         (alpha  (car two-n-list))
 
461
         (beta (cadr two-n-list))
 
462
         (den (+ 2 alpha))
 
463
         (num (+ (floor beta den) beta)))
 
464
    (- 0 (/ num den))))
 
465
 
 
466
 
 
467
;(defdata rat (oneof 0 positive-ratio negative-ratio))
 
468
;DOESNT WORK so positive/negative ratio are not consistent types ;TODO
 
469
;(local (include-book "arithmetic-5/top" :dir :system))
 
470
;(thm (nat-listp (defdata::split-nat 2 n)))
 
471
;(thm (positive-ratiop (nth-positive-ratio n)))
 
472
 
 
473
 
 
474
(defun negp (x)
 
475
  (declare (xargs :guard t))
 
476
  (and (integerp x) 
 
477
       (< x 0)
 
478
       ))
 
479
(defun nth-neg (n)
 
480
  (declare (xargs :guard (natp n)))
 
481
  (- -1 n))
 
482
 
 
483
#|
 
484
(defdata int (oneof 0 pos neg))
 
485
(thm (iff (integerp x) (intp x)))
 
486
|#
 
487
 
 
488
(defun nth-positive-rational (n)
 
489
  (declare (xargs :guard (natp n)))
 
490
  (let* ((two-n-list (defdata::split-nat 2 n))
 
491
         (num (nth-pos (car two-n-list)))
 
492
         (den (nth-pos (cadr two-n-list))))
 
493
    (/ num den)))
 
494
 
 
495
(defun nth-negative-rational (n)
 
496
  (declare (xargs :guard (natp n)))
 
497
  (let* ((two-n-list (defdata::split-nat 2 n))
 
498
         (num (nth-neg (car two-n-list)))
 
499
         (den (nth-pos (cadr two-n-list))))
 
500
    (/ num den)))
 
501
(defun positive-rationalp (x)
 
502
  (declare (xargs :guard t))
 
503
  (and (rationalp x) 
 
504
       (> x 0)
 
505
       ))
 
506
(defun negative-rationalp (x)
 
507
  (declare (xargs :guard t))
 
508
  (and (rationalp x) 
 
509
       (< x 0)
 
510
       ))
 
511
 
 
512
;(defdata rational (oneof 0 positive-rational negative-rational))
 
513
(defun nth-rational (n)
 
514
  (declare (xargs :guard (natp n)))
 
515
  (let* ((two-n-list (defdata::split-nat 2 n))
 
516
         (num (nth-integer (car two-n-list)))
 
517
         (den (nth-pos (cadr two-n-list))))
 
518
    (/ num den)))
 
519
 
 
520
 
 
521
 
 
522
(defthm nth-rat-is-ratp
 
523
  (implies (natp x)
 
524
           (rationalp (nth-rational x)))
 
525
  :rule-classes (:rewrite :type-prescription))
 
526
 
 
527
 ;lo included, hi included
 
528
    
 
529
  
 
530
(defun nth-rational-between (n lo hi);inclusive
 
531
  (declare (xargs :guard (and (natp n)
 
532
                              (rationalp lo)
 
533
                              (rationalp hi))))
 
534
 
 
535
  (let* ((two-n-list (defdata::split-nat 2 n))
 
536
         (den (nth-pos (car two-n-list)))
 
537
         (num (nth-integer-between (cadr two-n-list) 0 (1+ den)))
 
538
         (range (- hi lo)))
 
539
    (+ lo (* (/ num den) range))))       
 
540
 
 
541
 
 
542
(defun nth-complex-rational (n)
 
543
  (declare (xargs :guard (natp n)))
 
544
  (let* ((two-n-list (defdata::split-nat 2 n))
 
545
         (rpart (nth-rational (defdata::nfixg (car two-n-list))))
 
546
         (ipart (nth-rational (defdata::nfixg (cadr two-n-list)))))
 
547
    (complex rpart ipart)))
 
548
 
 
549
(encapsulate 
 
550
 ((nth-acl2-number (n) t :guard (natp n)))
 
551
 (local (defun nth-acl2-number (n)
 
552
          (declare (xargs :guard (natp n)))
 
553
          (declare (ignore n))
 
554
          0)))
 
555
 
 
556
(defun nth-acl2-number-builtin (n)
 
557
  (declare (xargs :guard (natp n)))
 
558
  (b* (((mv choice seed)
 
559
        (defdata::switch-nat 4 n)))
 
560
    (case choice
 
561
          (0 (nth-nat seed))
 
562
          (1 (nth-integer seed))
 
563
          (2 (nth-rational seed))
 
564
          (t (nth-complex-rational seed)))))
 
565
 
 
566
(defattach nth-acl2-number nth-acl2-number-builtin)
 
567
 
 
568
;(defdata character-list (listof character))
 
569
;;only strings upto len 1 to 8
 
570
(defun nth-character-list (n)
 
571
  (declare (xargs :guard (natp n)))
 
572
                  ;:verify-guards nil))
 
573
  (let* ((str-len (1+ (mod n 7)))
 
574
         (char-pos-list (defdata::split-nat str-len n))
 
575
         (charlist (get-character-list-from-positions char-pos-list)))
 
576
    charlist))
 
577
 
 
578
(defun nth-standard-char-list (n)
 
579
  (declare (xargs :guard (natp n)))
 
580
                  ;:verify-guards nil))
 
581
  (let* ((str-len (1+ (mod n 7)))
 
582
         (char-pos-list (defdata::split-nat str-len n))
 
583
         (charlist (get-standard-char-list-from-positions char-pos-list)))
 
584
    charlist))
 
585
 
 
586
#||
 
587
(defconst *base-types* '((BOOLEAN 2 *BOOLEAN-VALUES* . BOOLEANP)
 
588
                         (CHARACTER-LIST T NTH-CHARACTER-LIST . CHARACTER-LISTP)
 
589
                         (SYMBOL T NTH-SYMBOL . SYMBOLP)
 
590
                         (STRING T NTH-STRING . STRINGP)
 
591
                         (CHARACTER 62 *CHARACTER-VALUES* . CHARACTERP)
 
592
                         (ACL2-NUMBER T NTH-ACL2-NUMBER . ACL2-NUMBERP)
 
593
                         (COMPLEX-RATIONAL T NTH-COMPLEX-RATIONAL . COMPLEX-RATIONALP)
 
594
                         (RATIONAL T NTH-RATIONAL . RATIONALP)
 
595
                         (POS T NTH-POS . POSP)
 
596
                         (NAT T NTH-NAT . NATP)
 
597
                         (INTEGER T NTH-INTEGER . INTEGERP)))
 
598
(defun nth-all (n)
 
599
  (declare (xargs :guard (natp n))
 
600
                  :verify-guards nil)
 
601
  (let* ((num-types (len *base-types*))
 
602
         (two-n-list (defdata::split-nat 2 n))
 
603
         (choice (mod (car two-n-list) num-types))
 
604
         (seed (cadr two-n-list))
 
605
         (type-info (cdr (nth choice *base-types*)))
 
606
         (type-size (car type-info))
 
607
         (type-enum (cadr type-info)))
 
608
    (if (eq type-size 't) ;inf
 
609
      `(,type-enum ,seed)
 
610
      `(nth ,(mod seed type-size) ,type-enum))))||#
 
611
 
 
612
 
 
613
(defconst *number-testing-limit* 1000)
 
614
 
 
615
;ADDED restricted testing enumerators for all number types
 
616
(defun nth-nat-testing (n)
 
617
  (declare (xargs :guard (natp n)))
 
618
  (let ((n-small (mod n *number-testing-limit*)))
 
619
    (nth-nat n-small)))
 
620
(defun nth-pos-testing (n)
 
621
  (declare (xargs :guard (natp n)))
 
622
  (let ((n-small (mod n *number-testing-limit*)))
 
623
    (nth-pos n-small)))
 
624
(defun nth-neg-testing (n)
 
625
  (declare (xargs :guard (natp n)))
 
626
  (let ((n-small (mod n *number-testing-limit*)))
 
627
    (nth-neg n-small)))
 
628
 
 
629
(defun nth-integer-testing (n)
 
630
  (declare (xargs :guard (natp n)))
 
631
  (let ((n-small (mod n *number-testing-limit*)))
 
632
    (nth-integer n-small)))
 
633
 
 
634
(defun nth-positive-ratio-testing (n)
 
635
  (declare (xargs :guard (natp n)))
 
636
  (let ((n-small (mod n *number-testing-limit*)))
 
637
    (nth-positive-ratio n-small)))
 
638
(defun nth-negative-ratio-testing (n)
 
639
  (declare (xargs :guard (natp n)))
 
640
  (let ((n-small (mod n *number-testing-limit*)))
 
641
    (nth-negative-ratio n-small)))
 
642
(defun nth-rational-testing (n)
 
643
  (declare (xargs :guard (natp n)))
 
644
  (let ((n-small (mod n *number-testing-limit*)))
 
645
    (nth-rational n-small)))
 
646
(defun nth-positive-rational-testing (n)
 
647
  (declare (xargs :guard (natp n)))
 
648
  (let ((n-small (mod n *number-testing-limit*)))
 
649
    (nth-positive-rational n-small)))
 
650
(defun nth-negative-rational-testing (n)
 
651
  (declare (xargs :guard (natp n)))
 
652
  (let ((n-small (mod n *number-testing-limit*)))
 
653
    (nth-negative-rational n-small)))
 
654
(defun nth-acl2-number-testing (n)
 
655
  (declare (xargs :guard (natp n)))
 
656
  (let ((n-small (mod n *number-testing-limit*)))
 
657
    (nth-acl2-number n-small)))
 
658
(defun nth-complex-rational-testing (n)
 
659
  (declare (xargs :guard (natp n)))
 
660
  (let ((n-small (mod n *number-testing-limit*)))
 
661
    (nth-complex-rational n-small)))
 
662
 
 
663
 
 
664
;; (defun atomp (v)
 
665
;;   (declare (xargs :guard t))
 
666
;;   (atom v))
 
667
 
 
668
(defun nth-atom (n)
 
669
  (declare (xargs :guard (natp n)))
 
670
  (b* (((mv choice seed) 
 
671
        (defdata::weighted-switch-nat 
 
672
          '(1  ;nil
 
673
            1  ;t
 
674
            3  ;nat
 
675
            1  ;sym
 
676
            1  ;string
 
677
            2  ;char
 
678
            2  ;acl2-num
 
679
            10 ;rational
 
680
            10 ;pos
 
681
            20 ;0
 
682
            30 ;integer
 
683
            ) n)))
 
684
        
 
685
    (case choice
 
686
          (0 'nil)
 
687
          (1 't)
 
688
          (2 (nth-nat-testing seed));smaller numbers
 
689
          (3 (nth-symbol seed))
 
690
          (4 (nth-string seed))
 
691
          (5 (nth-alpha-num-character seed)) ;(nth-character seed))
 
692
          (6 (nth-acl2-number seed))
 
693
          (7 (nth-rational seed))
 
694
          (8 (nth-pos-testing seed))
 
695
          (9 0)
 
696
          (t (nth-integer-testing seed)))))
 
697
 
 
698
;(defdata atom (oneof acl2-number character symbol string))
 
699
 
 
700
 
 
701
;atoms
 
702
 
 
703
; register-type ought to also test if not prove the following:
 
704
; TODO:Note it does not prove that type is sound neither that is is complete
 
705
; By Type Soundness i mean (thm (implies (natp n) (Tp (nth-T n)))
 
706
; By Type Completeness i mean (thm (implies (Tp x)
 
707
;                                          (equal x (nth-T (T-index x)))) 
 
708
;                                   where (nth-T (T-index x)) = x
 
709
 
 
710
(defmacro register-custom-type  (typename typesize enum pred &key verbose)
 
711
  `(defdata::register-type ,typename :size ,typesize :predicate ,pred :enumerator ,enum :verbose ,verbose))
 
712
 
 
713
(register-custom-type nat t nth-nat natp)
 
714
 
 
715
(register-custom-type pos t nth-pos posp)
 
716
 
 
717
(register-custom-type neg t nth-neg negp )
 
718
(register-custom-type integer t nth-integer integerp )
 
719
(register-custom-type positive-ratio t nth-positive-ratio  positive-ratiop)
 
720
(register-custom-type negative-ratio t nth-negative-ratio  negative-ratiop )
 
721
(register-custom-type positive-rational t nth-positive-rational  positive-rationalp )
 
722
(register-custom-type negative-rational t nth-negative-rational  negative-rationalp )
 
723
(register-custom-type rational t nth-rational  rationalp )
 
724
(register-custom-type complex-rational t nth-complex-rational  complex-rationalp )
 
725
(register-custom-type acl2-number t nth-acl2-number  acl2-numberp )
 
726
(register-custom-type boolean 2 nth-boolean  booleanp );taken care of by define-enumeration-type
 
727
(register-custom-type symbol t nth-symbol  symbolp)
 
728
 
 
729
(verify-termination acl2::legal-constantp)
 
730
(verify-guards acl2::legal-constantp)
 
731
(defun proper-symbolp (x)
 
732
  (declare (xargs :guard t))
 
733
  (and (symbolp x)
 
734
       (not (or (keywordp x);a keyword
 
735
                (booleanp x);t or nil
 
736
                (acl2::legal-constantp x)))))
 
737
 
 
738
(in-theory (disable acl2::legal-constantp))
 
739
 
 
740
(defconst *nice-symbol-names*
 
741
  '(x y z a b c i j k p q r s u v w l d e f g h m n))
 
742
 
 
743
(defun nth-proper-symbol (n)
 
744
  (declare (xargs :guard (natp n)))
 
745
  (let ((psym (nth-symbol n)))
 
746
    (if (proper-symbolp psym)
 
747
        psym
 
748
      (nth (mod n (len *nice-symbol-names*)) *nice-symbol-names*))))
 
749
 
 
750
(register-custom-type proper-symbol t nth-proper-symbol proper-symbolp)
 
751
 
 
752
(defun nth-character-uniform (m seed)
 
753
    (declare (ignorable m))
 
754
     (declare (type (unsigned-byte 31) seed))
 
755
     (declare (xargs :guard (and (natp m)
 
756
                                 (unsigned-byte-p 31 seed))))
 
757
     (mv-let (n seed)
 
758
             (defdata::random-natural-seed seed)
 
759
             (mv (nth-character n) (the (unsigned-byte 31) seed))))
 
760
   
 
761
(defdata::register-type character :size 62 :enumerator nth-character :predicate characterp :enum/acc nth-character-uniform)
 
762
 
 
763
 
 
764
 
 
765
 
 
766
;(define-enumeration-type standard-char *standard-chars*)
 
767
(defun nth-standard-char (n)
 
768
  (declare (xargs :guard (natp n)))
 
769
  (nth (mod n 96) *standard-chars*))
 
770
(register-custom-type standard-char 96 nth-standard-char standard-char-p)
 
771
(register-custom-type string t nth-string stringp)
 
772
(register-custom-type standard-string t nth-standard-string standard-stringp)
 
773
(register-custom-type atom t nth-atom atom);instead of atomp Exception
 
774
 
 
775
;added the above atom primitive types in the data-type graph using register-custom-type
 
776
 
 
777
;custom type
 
778
(defconst *z-values* '(0 -1 "a" 1/3 :a)) ;for zp
 
779
(defun nth-z (n)
 
780
  (declare (xargs :guard (natp n)))
 
781
  (nth (mod n 5) *z-values*))
 
782
(defun nth-z-uniform (m seed)
 
783
    (declare (ignorable m))
 
784
     (declare (type (unsigned-byte 31) seed))
 
785
     (declare (xargs :guard (and (natp m)
 
786
                                 (unsigned-byte-p 31 seed))))
 
787
     (mv-let (n seed)
 
788
             (defdata::random-natural-seed seed)
 
789
             (mv (nth-z n) (the (unsigned-byte 31) seed))))
 
790
(defdata::register-type z :size t :enumerator nth-z :predicate zp :enum/acc nth-z-uniform)
 
791
 
 
792
 
 
793
;Subtype relations betweem the above
 
794
;pos is a subtype of nat (Note the direction)
 
795
(defdata-subtype pos nat)
 
796
 
 
797
;nat is a subtype of integer
 
798
(defdata-subtype nat integer)
 
799
(defdata-subtype neg integer)
 
800
(defdata-subtype integer rational)
 
801
(defdata-subtype positive-ratio rational)
 
802
(defdata-subtype positive-rational rational) ;Aug 18 2011
 
803
(defdata-subtype negative-ratio rational)
 
804
(defdata-subtype negative-rational rational) ;Aug 18 2011
 
805
(defdata-subtype complex-rational acl2-number)
 
806
(defdata-subtype rational acl2-number)
 
807
(defdata-subtype acl2-number atom)
 
808
(defdata-subtype boolean symbol)
 
809
(defdata-subtype proper-symbol symbol)
 
810
 
 
811
(defdata-subtype standard-char character :hints (("Goal" :in-theory (enable standard-char-p))))
 
812
(defdata-subtype character atom)
 
813
(defdata-subtype string atom)
 
814
(defdata-subtype symbol atom)
 
815
 
 
816
(defdata ratio (oneof positive-ratio negative-ratio)) 
 
817
 
 
818
 
 
819
(defdata-subtype ratio rational) 
 
820
 
 
821
;added 26th Sep '13
 
822
(defdata-subtype neg negative-rational)
 
823
(defdata-subtype pos positive-rational) 
 
824
(defdata-subtype negative-rational z)
 
825
(defdata-subtype ratio z)
 
826
(defdata-subtype complex-rational z)
 
827
(defdata-subtype symbol z)
 
828
(defdata-subtype character z)
 
829
(defdata-subtype string z)
 
830
(defdata-disjoint pos z)
 
831
 
 
832
(defdata-subtype standard-string string)
 
833
 
 
834
 
 
835
;Disjoint relations between the above types
 
836
(defdata-disjoint acl2-number character)
 
837
(defdata-disjoint acl2-number symbol)
 
838
(defdata-disjoint character string)
 
839
(defdata-disjoint character symbol)
 
840
(defdata-disjoint string symbol)
 
841
(defdata-disjoint boolean proper-symbol)
 
842
 
 
843
;lists of atoms
 
844
(defthm termination-tree-enum-cdr
 
845
  (implies (consp x)
 
846
           (and (< (acl2-count (cdr x))
 
847
                   (acl2-count x))
 
848
                (< (acl2-count (car x))
 
849
                   (acl2-count x)))))
 
850
(defthm termination-tree-enum-dec
 
851
  (implies (< (acl2-count x1) (acl2-count x2))
 
852
           (and (< (acl2-count (car x1)) (acl2-count x2))
 
853
                (< (acl2-count (cdr x1)) (acl2-count x2)))))
 
854
(defthm terminination-tree-enum-nth
 
855
  (<= (acl2-count (nth i x))
 
856
              (acl2-count x))
 
857
  :rule-classes (:rewrite :linear))
 
858
 
 
859
(defthm termination-tree-enum-dec2
 
860
  (implies (< (acl2-count x1) (acl2-count x2))
 
861
           (< (acl2-count (nth i x1)) (acl2-count x2)))
 
862
  :hints (("Goal" :in-theory (disable nth))))
 
863
 
 
864
 
 
865
 
 
866
; IMPORTANT: PROPER-CONS is put ahead of all lists, so that in the
 
867
; event of intersecting it with lists, the lists are given preference,
 
868
; by the virtue of appearing earlier in the reverse chronological
 
869
; order of type-metadata table. Lists of various types are certainly
 
870
; more amenable to Cgen/Enumeration than proper-conses.
 
871
 
 
872
;; (defdata list-a (list atom))
 
873
;; (defdata list-aa (list atom atom))
 
874
;; (defdata list-aaa (list atom atom atom))
 
875
 
 
876
;cons
 
877
(defdata cons-atom (cons atom atom))
 
878
 
 
879
(defdata-disjoint cons-atom atom)
 
880
 
 
881
 
 
882
(defdata cons-ca-ca (cons cons-atom cons-atom))         
 
883
(defdata cons-cca-cca (cons cons-ca-ca cons-ca-ca) )
 
884
 
 
885
;; (defdata list-a-ca (list atom cons-atom) )
 
886
;; (defdata list-aa-ca (list atom atom atom cons-atom) )
 
887
;; (defdata list-aa-cca (list atom atom cons-ca-ca) )
 
888
;; (defdata list-aaaa-cccca (list cons-atom cons-cca-cca) )
 
889
;; (defdata list-ca-cca (list cons-atom cons-ca-ca) )
 
890
;; (defdata list-la-la (list list-aa list-aa) )
 
891
 
 
892
 
 
893
;MAJOR CHANGE June 6th 2010, now we have no guards in any enumerators
 
894
(defun nth-proper-cons (n)
 
895
;  (declare (xargs :guard (natp n)))
 
896
  (declare (xargs :mode :program))
 
897
  (b* (((mv choice seed)
 
898
        (defdata::weighted-switch-nat 
 
899
          '(
 
900
            1  ;list-a
 
901
            1  ;list-aa
 
902
            1  ;list-aaa
 
903
            1  ;list-a-ca
 
904
            1  ;list-aa-ca 
 
905
            1  ;list-aa-cca
 
906
            1  ;list-aaaa-cccca
 
907
            1  ;list-ca-cca
 
908
            1  ;list-ca-cccca
 
909
            ) n)))
 
910
 
 
911
       
 
912
 
 
913
    (case choice
 
914
      (0 (list (nth-atom seed)))
 
915
      (1 (b* (((list i1 i2) (defdata::split-nat 2 seed))) (list (nth-atom i1) (nth-atom i2))))
 
916
      (2 (b* (((list i1 i2 i3) (defdata::split-nat 3 seed))) (list (nth-atom i1) (nth-atom i2) (nth-atom i3))))
 
917
      (3 (b* (((list i1 i2 i3) (defdata::split-nat 3 seed))) (list (nth-atom i1) (cons (nth-atom i2) (nth-atom i3))))) ;(nth-list-a-ca seed))
 
918
      (4 (b* (((list i1 i2 i3 i4 i5) (defdata::split-nat 5 seed)))
 
919
           (list (nth-atom i1) (nth-atom i2) (nth-atom i3) (cons (nth-atom i4) (nth-atom i5))))) ;(nth-list-aa-ca  seed))
 
920
      (5 (b* (((list i1 i2 i3 i4 i5 i6) (defdata::split-nat 6 seed)))
 
921
           (list (nth-atom i1) (nth-atom i2) (cons (cons (nth-atom i3) (nth-atom i4)) 
 
922
                                                   (cons (nth-atom i5) (nth-atom i6)))))) ;(list-aa-cca seed))
 
923
      (6 (b* (((list i1 i2 i3 i4 i5) (defdata::split-nat 5 seed)));(list-aaaa-cccca seed)) 
 
924
           (list (nth-cons-atom i1) (cons (cons (nth-cons-atom i2) (nth-cons-atom i3)) 
 
925
                                          (cons (nth-cons-atom i4) (nth-cons-atom i5)))))) 
 
926
      (7 (b* (((list i1 i2 i3 i4 i5) (defdata::split-nat 5 seed)))  ;(list-ca-cca seed))
 
927
           (list (nth-cons-atom i1) (cons (cons (nth-atom i2) (nth-atom i3)) 
 
928
                                          (cons (nth-atom i4) (nth-atom i5))))))
 
929
      (8 (b* (((list i1 i2 i3 i4 i5) (defdata::split-nat 5 seed)))
 
930
           (list (nth-atom i1) (nth-atom i2) (nth-atom i3) (nth-atom i4) (nth-atom i5))))
 
931
      (t '(1  2)))))
 
932
 
 
933
(register-custom-type proper-cons t nth-proper-cons  proper-consp)
 
934
 
 
935
 
 
936
 
 
937
 
 
938
(defdata nat-list (listof nat))
 
939
 
 
940
;; (verify-termination pos-listp) ; pos-listp is in program mode, so we need this.
 
941
;; (verify-guards pos-listp)
 
942
 
 
943
(defdata    pos-list (listof pos))
 
944
 
 
945
(defdata    integer-list (listof integer) )
 
946
(defdata    rational-list (listof rational) )
 
947
(defdata    complex-rational-list (listof complex-rational) )
 
948
 
 
949
(defdata acl2-number-list (listof acl2-number) )
 
950
(defdata boolean-list (listof boolean) )
 
951
(defdata symbol-list    (listof symbol) )
 
952
(defdata::register-type character-list 
 
953
               :size t 
 
954
               :predicate character-listp
 
955
               :enumerator nth-character-list  
 
956
               :prettyified-def (listof character))
 
957
               
 
958
(defdata::register-type standard-char-list 
 
959
               :size t 
 
960
               :predicate  standard-char-listp
 
961
               :enumerator nth-standard-char-list 
 
962
               :prettyified-def (listof standard-char))
 
963
 
 
964
; TAU characterization of standard-char-list (copied and string/replaced from def=>String-list)
 
965
(defthm
 
966
  def=>standard-char-list
 
967
  (and (implies (and (equal v1 'nil))
 
968
                (standard-char-listp v1))
 
969
       (implies (and (standard-char-p v11)
 
970
                     (standard-char-listp v12))
 
971
                (standard-char-listp (cons v11 v12))))
 
972
  :hints (("goal" :in-theory (e/d (standard-char-listp) (standard-char-p))))
 
973
  :rule-classes (:tau-system :rewrite))
 
974
(defthm
 
975
  standard-char-list=>def
 
976
  (and (implies (and (standard-char-listp v1)
 
977
                     (endp v1))
 
978
                (equal v1 'nil))
 
979
       (implies
 
980
        (and (standard-char-listp v1)
 
981
             (consp v1))
 
982
        (and (standard-char-p (car v1))
 
983
             (standard-char-listp (cdr v1)))))
 
984
  :hints (("goal" :in-theory (e/d (standard-char-listp) (standard-char-p))))
 
985
:rule-classes (:tau-system (:forward-chaining :trigger-terms ((standard-char-listp v1)))))
 
986
 
 
987
 
 
988
(defdata string-list (listof string))
 
989
(defdata atom-list (listof atom))
 
990
(defdata-subtype pos-list nat-list)
 
991
(defdata-subtype nat-list integer-list)
 
992
(defdata-subtype integer-list rational-list)
 
993
(defdata-subtype complex-rational-list acl2-number-list)
 
994
(defdata-subtype rational-list acl2-number-list )
 
995
(defdata-subtype acl2-number-list atom-list)
 
996
(defdata-subtype boolean-list symbol-list)
 
997
(defdata-subtype standard-char-list character-list)
 
998
(defdata-subtype character-list atom-list)
 
999
(defdata-subtype string-list atom-list)
 
1000
 
 
1001
(defdata-subtype symbol-list atom-list)
 
1002
 
 
1003
 
 
1004
 
 
1005
;TODO.NOTE: Note that all the enumerators defined below are purely heuristic and 
 
1006
;are not consistent/complete with their respective predicates.
 
1007
 
 
1008
 
 
1009
;; (verify-guards NTH-NAT-LIST) 
 
1010
;; (verify-guards NTH-RATIONAL-LIST)
 
1011
;; (verify-guards NTH-SYMBOL-LIST)
 
1012
;; (verify-guards  NTH-CONS-ATOM)
 
1013
;; (verify-guards NTH-CONS-CA-CA)
 
1014
;; (verify-guards  NTH-STRING-LIST)
 
1015
;; (verify-guards NTH-ATOM-LIST)
 
1016
 
 
1017
(defun nth-all (n)
 
1018
  (declare (xargs :mode :program))
 
1019
  (declare (xargs :guard (natp n)))
 
1020
 
 
1021
           
 
1022
                  ;;:verify-guards nil))
 
1023
  (b* (((mv choice seed)
 
1024
        (defdata::weighted-switch-nat 
 
1025
          '(1  ;nil
 
1026
            1  ;0
 
1027
            1 ;t
 
1028
            1 ;integer
 
1029
            1 ;rational
 
1030
            1  ;nat-list
 
1031
            1  ;sym
 
1032
            1  ;string
 
1033
            2  ;char
 
1034
            1  ;acl2-num
 
1035
            1  ;bool
 
1036
            5 ;nat
 
1037
            5 ;pos
 
1038
            5  ;rational-list
 
1039
            2  ;sym-list
 
1040
            20 ;cons-atom
 
1041
            5  ;charlist
 
1042
            10  ;cons-cons-atom
 
1043
            1  ;stringlist
 
1044
            10  ;atom-list
 
1045
            ) n)))
 
1046
      
 
1047
    (case choice
 
1048
          (0 'nil)
 
1049
          (1 0)
 
1050
          (2 't)
 
1051
          (3 (nth-integer-testing seed))
 
1052
          (4 (nth-rational seed))
 
1053
          (5 (nth-nat-list seed))
 
1054
          (6 (nth-symbol seed))
 
1055
          (7 (nth-string seed))
 
1056
          (8 (nth-alpha-num-character seed)) ;(nth-character seed))
 
1057
          (9 (nth-acl2-number seed))
 
1058
          (10 (nth (mod seed 2) *boolean-values*))
 
1059
          (11 (nth-nat-testing seed))
 
1060
          (12 (nth-pos-testing seed))
 
1061
          (13 (nth-rational-list seed))
 
1062
          (14 (nth-symbol-list seed))
 
1063
          (15 (nth-cons-atom seed))
 
1064
          (16 (nth-character-list seed))
 
1065
          (17 (b* (((list i1 i2) (defdata::split-nat 2 seed))) 
 
1066
                (cons (nth-cons-atom i1) (nth-cons-atom i2)))) ;(cons-ca-ca seed))
 
1067
          (18 (nth-string-list seed))
 
1068
          (19 (nth-atom-list seed))
 
1069
          (t 'nil)))) ;this case should not come up
 
1070
 
 
1071
 
 
1072
(register-custom-type all t nth-all  allp)
 
1073
 
 
1074
 
 
1075
;We will also name a special type, the empty type, which has no elements in its typeset.
 
1076
(defconst *empty-values* '())
 
1077
(defun nth-empty (x)
 
1078
  (declare (ignore x) (xargs :guard (natp x)))
 
1079
  (er hard? 'nth-empty "~| Empty enumerator~%"))
 
1080
;TODO - if type is already registered, then we should be able to pick the predicate
 
1081
;from the table instead of syntactically from the type.
 
1082
(defun emptyp (x)
 
1083
  (declare (ignore x) (xargs :guard t))
 
1084
  nil)
 
1085
 
 
1086
(defthm emptyp-is-tau-predicate 
 
1087
    (booleanp (emptyp x))
 
1088
  :rule-classes :tau-system)
 
1089
 
 
1090
(register-custom-type empty 0 nth-empty emptyp)
 
1091
;NOTE: empty is a special type, so we treat it specially and seperately, rather than the
 
1092
;usual way of going through the data type graph, and it might lead to inconsistency
 
1093
;with the ACL2 axioms about datatypes.
 
1094
 
 
1095
(defdata cons (cons all all))
 
1096
 
 
1097
 
 
1098
;Alist/acons theory
 
1099
(defdata acons (cons (cons all all) all))
 
1100
 
 
1101
;;associated key-value pairs
 
1102
;; (defun aconsp (x)
 
1103
;;   (declare (xargs :guard t))
 
1104
;;   (and (consp x) (consp (car x))))
 
1105
(defun acons-caar (x) (declare (xargs :guard (aconsp x))) (caar x))
 
1106
(defun acons-cdar (x) (declare (xargs :guard (aconsp x))) (cdar x))
 
1107
(defun acons-cdr (x) (declare (xargs :guard (aconsp x))) (cdr x))
 
1108
 
 
1109
(defthm acons-acl2-count-lemma
 
1110
  (equal (acl2-count (acons x1 x2 x3))
 
1111
         (+ 2 (acl2-count x1) (acl2-count x2) (acl2-count x3))))
 
1112
 
 
1113
(in-theory (enable aconsp))
 
1114
(register-data-constructor (aconsp acons)
 
1115
                           ((allp acons-caar) (allp acons-cdar) (allp acons-cdr))
 
1116
                           :rule-classes (:rewrite)
 
1117
                           :verbose t)
 
1118
 
 
1119
(defthm acons-alist-lemma
 
1120
  (implies (alistp x)
 
1121
           (alistp (acons x1 x2 x)))
 
1122
  :rule-classes ((:rewrite :backchain-limit-lst 1)))
 
1123
  
 
1124
; (in-theory (disable acons aconsp acons-caar acons-cdar acons-cdr)) TODO --
 
1125
; Whats the point of acons as a constructor if these functions are not disabled
 
1126
; -- Ohh well, lets ride on cons for now. [2014-09-24 Wed]
 
1127
 
 
1128
 
 
1129
 
 
1130
 
 
1131
(defdata list (oneof cons nil))
 
1132
 
 
1133
(DEFUNS (NTH-TRUE-LIST
 
1134
               (X)
 
1135
               (declare (xargs :mode :program))
 
1136
               (DECLARE (XARGS :guard (natp x) :verify-guards nil
 
1137
                               :MEASURE (NFIX X)))
 
1138
               (IF (OR (NOT (INTEGERP X)) (< X 1))
 
1139
                   'NIL
 
1140
                   (LET ((X (- X 1)))
 
1141
                        (LET ((INFXLST (DEFDATA::SPLIT-NAT 2 X)))
 
1142
                             (CONS (LET ((X (NTH 0 INFXLST))) (NTH-ALL X))
 
1143
                                   (LET ((X (NTH 1 INFXLST)))
 
1144
                                        (NTH-TRUE-LIST X))))))))
 
1145
 
 
1146
(defdata::register-type true-list 
 
1147
               :size t 
 
1148
               :predicate true-listp
 
1149
               :enumerator nth-true-list 
 
1150
               :prettyified-def (listof all))
 
1151
 
 
1152
;some alists
 
1153
 
 
1154
(defdata alist (listof (cons all all)))
 
1155
(defdata symbol-alist (alistof symbol all))
 
1156
(verify-termination character-alistp)
 
1157
(defdata character-alist (alistof character all))
 
1158
(defdata r-symbol-alist (alistof all symbol))
 
1159
(defdata-subtype symbol-alist alist)
 
1160
(defdata-subtype character-alist alist)
 
1161
(defdata-subtype r-symbol-alist alist)
 
1162
 
 
1163
;TODO standard-string-alist has very poor theory support!!
 
1164
;(defdata standard-string-list (listof standard-string))
 
1165
;(defdata-subtype standard-string-list string-list)
 
1166
;(defdata standard-string-alist (alistof standard-string all)) 
 
1167
;(defdata-subtype standard-string-alist alist)
 
1168
 
 
1169
;(verify-guards nth-true-list)
 
1170
(defdata true-list-list (listof true-list))
 
1171
(defdata-subtype true-list-list true-list)
 
1172
 
 
1173
 
 
1174
 
 
1175
;added 26th Sep '13
 
1176
(defdata-subtype cons z)
 
1177
(defdata-subtype list z)
 
1178
 
 
1179
 
 
1180
(defun all-but-zero-nil-tp (x)
 
1181
  (declare (xargs :guard t))
 
1182
  (and (not (equal x 0))
 
1183
       (not (equal x 't))
 
1184
       (not (equal x 'nil))))
 
1185
            
 
1186
(defun nth-all-but-zero-nil-t (n)
 
1187
  (declare (xargs :mode :program))
 
1188
  (declare (xargs :guard (natp n)))
 
1189
 
 
1190
  (b* (((mv choice seed)
 
1191
          (defdata::weighted-switch-nat 
 
1192
            '(1 ;integer
 
1193
              1  ;charlist
 
1194
              1  ;sym
 
1195
              1  ;string
 
1196
              2  ;char
 
1197
              1  ;pos
 
1198
              5 ;positive-ratio
 
1199
              5 ;negative-ratio
 
1200
              5 ;complex-rational
 
1201
              5  ;rational-list
 
1202
              2  ;sym-list
 
1203
              20 ;cons-atom
 
1204
              5  ;nat-list
 
1205
              10  ;cons-cons-atom
 
1206
              1  ;stringlist
 
1207
              10  ;atom-list
 
1208
              ) n)))
 
1209
    
 
1210
    (case choice
 
1211
          (0 (nth-integer-testing seed))
 
1212
          (1 (nth-character-list seed))
 
1213
          (2 (nth-symbol seed))
 
1214
          (3 (nth-string seed))
 
1215
          (4 (nth-character seed))
 
1216
          (5 (nth-pos-testing seed))
 
1217
          (6 (nth-positive-ratio seed))
 
1218
          (7 (nth-negative-ratio seed))
 
1219
          (8 (nth-complex-rational seed))
 
1220
          (9 (nth-rational-list seed))
 
1221
          (10 (nth-symbol-list seed))
 
1222
          (11 (nth-cons-atom seed))
 
1223
          (12 (nth-nat-list seed))
 
1224
          (13 (b* (((list i1 i2) (defdata::split-nat 2 seed))) 
 
1225
                (cons (nth-cons-atom i1) (nth-cons-atom i2)))) ;(cons-ca-ca seed))
 
1226
          (14 (nth-string-list seed))
 
1227
          (15 (nth-atom-list seed))
 
1228
          (t 1))))
 
1229
 
 
1230
(register-custom-type all-but-zero-nil-t t nth-all-but-zero-nil-t  all-but-zero-nil-tp)
 
1231
 
 
1232
            
 
1233
(defun nth-wf-key (n) ;;since nth-all-but-zero-nil-t has strings of length less than 8, it cannot include the ill-formed-key
 
1234
  (declare (xargs :guard (natp n)))
 
1235
  (declare (xargs :mode :program))
 
1236
  (nth-all-but-zero-nil-t n))
 
1237
 
 
1238
(register-custom-type wf-key t nth-wf-key wf-keyp)
 
1239
 
 
1240
;; Same problem as in sets. A nil is also a good-map!
 
1241
;; 3 April 2014
 
1242
;; (defun non-empty-good-map (x)
 
1243
;;   (declare (xargs :guard t))
 
1244
;;   (and (consp x)
 
1245
;;        (good-map x)))
 
1246
 
 
1247
 
 
1248
(defun all-but-nilp (x)
 
1249
  (declare (xargs :guard t))
 
1250
  (not (equal x 'nil)))
 
1251
 
 
1252
; TODO: this is a major hiccup of our map and record implementation, disallowing nil explicitly!!
 
1253
;; (register-data-constructor (non-empty-good-map mset)
 
1254
;;                            ((wf-keyp caar) (all-but-nilp cdar) (good-map cdr))
 
1255
;;                            :proper nil)
 
1256
 
 
1257
 
 
1258
(register-data-constructor (good-map mset)
 
1259
                           ((wf-keyp caar) (allp cdar) (good-map cdr))
 
1260
                           :hints (("Goal" :in-theory (enable good-map)))
 
1261
                           :proper nil)
 
1262
 
 
1263
(defun nth-all-but-nil (n)
 
1264
  (declare (xargs :mode :program))
 
1265
  (declare (xargs :guard (natp n)))
 
1266
  (cond ((eql n 0) 0)
 
1267
        ((eql n 12) t)
 
1268
        (t (nth-all-but-zero-nil-t n))))
 
1269
 
 
1270
(register-custom-type all-but-nil t nth-all-but-nil  all-but-nilp)
 
1271
 
 
1272
(defdata-subtype all-but-zero-nil-t all)
 
1273
(defdata-subtype all-but-nil all) ;make this the pseudo top type!
 
1274
 
 
1275
(defdata-subtype acons cons :hints (("Goal" :in-theory (enable aconsp))))
 
1276
(defdata-subtype cons all-but-nil)
 
1277
(defdata-subtype atom all)
 
1278
(defdata-subtype atom-list true-list)
 
1279
(defdata-subtype alist true-list)
 
1280
(defdata-subtype list all)
 
1281
(defdata-subtype true-list list)
 
1282
 
 
1283
 
 
1284
 
 
1285
 
 
1286
(defdata cons-cccca-cccca (cons cons-cca-cca cons-cca-cca) )
 
1287
(defdata cons-a-ca (cons atom cons-atom) )
 
1288
(defdata cons-a-cca (cons atom cons-ca-ca) )
 
1289
(defdata cons-a-cccca (cons atom cons-cca-cca))
 
1290
(defdata cons-ca-cca (cons cons-atom cons-ca-ca))
 
1291
 
 
1292
(defdata cons-ca-cccca (cons cons-atom cons-cca-cca) )
 
1293
;(verify-guards allp)
 
1294
(defdata cons-all-all-but-zero-nil-t (cons all all-but-zero-nil-t) )
 
1295
 
 
1296
(defun nth-improper-cons (n)
 
1297
;  (declare (xargs :guard (natp n)))
 
1298
  (declare (xargs  :mode :program))
 
1299
  (b* (((mv choice seed)
 
1300
        (defdata::weighted-switch-nat 
 
1301
          '(
 
1302
            1  ;cons-all-all-but-zero-nil-t
 
1303
            1  ;cons-ca-ca
 
1304
            1  ;cons-a-ca
 
1305
            1  ;cons-a-cca
 
1306
            1  ;cons-a-cccca
 
1307
            1  ;cons-cccca-cccca
 
1308
            1  ;cons-ca-cca
 
1309
            1  ;cons-ca-cccca
 
1310
            ) n)))
 
1311
    
 
1312
    (case choice
 
1313
      (0 (nth-cons-all-all-but-zero-nil-t seed))
 
1314
      (1 (nth-cons-ca-ca seed))
 
1315
      (2 (nth-cons-a-ca seed))
 
1316
      (3 (nth-cons-a-cca seed))
 
1317
      (4 (nth-cons-a-cccca seed))
 
1318
      (5 (nth-cons-cccca-cccca seed))
 
1319
      (6 (nth-cons-ca-cca seed))
 
1320
      (7 (nth-cons-ca-cccca seed))
 
1321
      (t '(1 . 2)))))
 
1322
 
 
1323
(register-custom-type improper-cons t nth-improper-cons  improper-consp)
 
1324
 
 
1325
(defdata-subtype improper-cons cons)
 
1326
 
 
1327
 
 
1328
(defdata-subtype proper-cons cons)
 
1329
 
 
1330
;this was missing before and so we werent inferring proper-consp when
 
1331
;type-alist knew both true-listp and proper-consp, and this is common in ACL2
 
1332
(defdata-subtype proper-cons  true-list)
 
1333
 
 
1334
(defdata-disjoint proper-cons improper-cons)
 
1335
(defdata-disjoint atom cons)
 
1336
 
 
1337
 
 
1338
 
 
1339
;new exports
 
1340
;; (defmacro disjoint-p (T1 T2)
 
1341
;;    ":Doc-Section DATA-DEFINITIONS
 
1342
;;   top-level query wether two types are disjoint~/
 
1343
;;   ~c[(disjoint-p T1 T2)] asks the question
 
1344
;;   are T1, T2 disjoint? This call makes a quick
 
1345
;;   lookup into the internal data type graph where
 
1346
;;   disjoint relation information provided by the user
 
1347
;;   in the past is stored and used to compute the
 
1348
;;   disjoint relation closure. If they are pairwise
 
1349
;;   disjoint (according to the computed information)
 
1350
;;   then we get back an affirmative , i.e ~c[t]. otherwise
 
1351
;;   it returns ~c[nil].
 
1352
  
 
1353
;;   ~bv[]
 
1354
;;   Examples:
 
1355
;;   (disjoint-p cons list)
 
1356
;;   (disjoint-p pos acl2-number)
 
1357
;;   (disjoint-p integer complex)
 
1358
;;   ~ev[]                      
 
1359
;;   ~bv[]
 
1360
;;   Usage:
 
1361
;;   (disjoint-p <Type-name1> <Type-name2>)
 
1362
;;   ~ev[]~/
 
1363
;;   "
 
1364
;;    `(trans-eval '(defdata::is-disjoint$$ ',t1 ',t2 defdata::R$ defdata::types-ht$) 'disjoint-p state nil))
 
1365
;  `(is-disjoint ',T1 ',T2 R$ types-ht$))
 
1366
 
 
1367
 
 
1368
;; (defmacro show-all-defdata-types ()
 
1369
;;   `(table-alist 'defdata::types-info-table (w state)))
 
1370
 
 
1371
;; (defmacro subtype-p (T1 T2)
 
1372
;;    ":Doc-Section DATA-DEFINITIONS
 
1373
;;   top-level query wether two types are disjoint~/
 
1374
;;   ~c[(subtype-p T1 T2)] asks the question
 
1375
;;   is T1 a subtype of T2? This call makes a quick
 
1376
;;   lookup into the internal data type graph where
 
1377
;;   subtype relation information provided by the user
 
1378
;;   in the past is stored and used to compute the
 
1379
;;   subtype relation closure. If T1 is indeed a subtype
 
1380
;;   of T2 (according to the computed information)
 
1381
;;   then we get back an affirmative , i.e ~c[t]. otherwise
 
1382
;;   it returns ~c[nil].
 
1383
  
 
1384
;;   ~bv[]
 
1385
;;   Examples:
 
1386
;;   (subtype-p boolean atom)
 
1387
;;   (subtype-p character string)
 
1388
;;   (subtype-p list cons)
 
1389
;;   ~ev[]                      
 
1390
;;   ~bv[]
 
1391
;;   Usage:
 
1392
;;   (subtype-p <Type-name1> <Type-name2>)
 
1393
;;   ~ev[]~/
 
1394
;;   "
 
1395
;;    `(trans-eval '(defdata::is-subtype$$ ',t1 ',t2 defdata::R$ defdata::types-ht$) 'subtype-p state nil))
 
1396
  ;`(is-subtype$$ ',T1 ',T2 R$ types-ht$))
 
1397
 
 
1398
 
 
1399
 
 
1400
 
 
1401
; TODO 29 March 2014
 
1402
; - add oddp and evenp (but do this consistently, these definitions are only valid when we additionally know that v is a integer.
 
1403
(defun nth-even (n) 
 
1404
  (declare (xargs :guard (natp n)))
 
1405
  (* 2 (nth-integer n)))
 
1406
 
 
1407
(defdata::register-type even 
 
1408
               :predicate evenp 
 
1409
               :enumerator nth-even)
 
1410
 
 
1411
(defun nth-odd (n) 
 
1412
  (declare (xargs :guard (natp n)))
 
1413
  (if (evenp n)
 
1414
      (1+ n)
 
1415
    (- n)))
 
1416
 
 
1417
;(defun nth-odd (n) (1+ (* 2 (nth-integer))))
 
1418
(defdata::register-type odd 
 
1419
               :predicate oddp 
 
1420
               :enumerator nth-odd)
 
1421
 
 
1422
(defdata-subtype var symbol)
 
1423
 
 
1424
(in-theory (disable varp))