← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/acl2s/cgen/random.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/cgen/random.lisp
 
1
#|$ACL2s-Preamble$;
 
2
(begin-book);$ACL2s-Preamble$|#
 
3
 
 
4
 
 
5
#|
 
6
 
 
7
  A Simple Random Number Generator              Version 0.1 
 
8
  Jared Davis <jared@cs.utexas.edu>          February 25, 2004
 
9
  
 
10
  This file is in the public domain.  You can freely use it for any
 
11
  purpose without restriction. 
 
12
 
 
13
  This is just a basic pure multiplicative pseudorandom number gen-
 
14
  erator.  *M31* is the 31st mersenne prime, and *P1* is 7^5 which
 
15
  is a primitive root of *M31*, ensuring that our period is M31 - 1.
 
16
  This idea is described in "Elementary Number Theory and its Appli-
 
17
  cations" by Kenneth H. Rosen, Fourth Edition, Addison Wesley 1999,
 
18
  in Chapter 10.1, pages 356-358.
 
19
 
 
20
  The random number generator uses a stobj, rand, to store the seed.
 
21
  You will want to use the following functions:
 
22
 
 
23
    (genrandom <max> rand)
 
24
       Returns (mv k rand) where 0 <= k < max.
 
25
            
 
26
    (update-seed <newseed> rand)
 
27
       Manually switch to a new seed.  By default, a large messy num-
 
28
       ber will be used.  You probably don't need to change it, but 
 
29
       it might be good if you want to be able to reproduce your re-
 
30
       sults in the future.
 
31
 
 
32
  Normally we are not particularly interested in reasoning about ran-
 
33
  dom numbers.  However, we can say that the number k generated is an
 
34
  an integer, and that 0 <= k < max when max is a positive integer. 
 
35
  See the theorems genrandom-minimum and genrandom-maximum. 
 
36
 
 
37
  --
 
38
  
 
39
  Modified slightly by Peter Dillinger, 7 Feb 2008
 
40
  With significant additions by Dimitris Vardoulakis & Peter Dillinger where
 
41
    noted below.
 
42
 
 
43
|#
 
44
 
 
45
(in-package "ACL2")
 
46
(set-verify-guards-eagerness 2)
 
47
 
 
48
 
 
49
(defconst *M31* 2147483647)    
 
50
(defconst *P1* 16807)          
 
51
 
 
52
(defstobj rand
 
53
  (seed :type integer :initially 1382728371))
 
54
 
 
55
 
 
56
 
 
57
(defun getseed (rand)
 
58
  (declare (xargs :stobjs (rand)))
 
59
  (let ((s (seed rand)))
 
60
    (if (and (integerp s) (<= 0 s))
 
61
        s
 
62
      0)))
 
63
 
 
64
(local (defthm getseed-integer
 
65
  (and (integerp (getseed rand))
 
66
       (<= 0 (getseed rand)))
 
67
  :rule-classes :type-prescription))
 
68
 
 
69
(in-theory (disable getseed))
 
70
 
 
71
(defun genrandom (max rand)
 
72
  (declare (xargs :stobjs (rand)
 
73
                  :guard (posp max)))
 
74
  (let* ((new-seed (mod (* *P1* (getseed rand)) *M31*))
 
75
         (rand (update-seed new-seed rand)))
 
76
    (mv (if (zp max)
 
77
          0
 
78
          (mod new-seed max))
 
79
        rand)))
 
80
 
 
81
(encapsulate nil
 
82
 (local (include-book "arithmetic-3/floor-mod/floor-mod" :dir :system))
 
83
 
 
84
 (defthm genrandom-natural
 
85
   (natp (car (genrandom max rand)))
 
86
   :rule-classes :type-prescription)
 
87
 
 
88
 (defthm genrandom-minimum 
 
89
   (<= 0 (car (genrandom max rand)))
 
90
   :rule-classes :linear)
 
91
 
 
92
 (defthm genrandom-maximum
 
93
   (implies (posp max)
 
94
            (<= (car (genrandom max rand)) (1- max)))
 
95
   :rule-classes :linear))
 
96
 
 
97
(in-theory (disable genrandom))
 
98
 
 
99
 
 
100
 
 
101
;=====================================================================;
 
102
; 
 
103
; Begin additions by Peter Dillinger &  Dimitris Vardoulakis
 
104
; Last modified 7 February 2008
 
105
;
 
106
;=====================================================================;
 
107
 
 
108
(defun random-boolean (rand)
 
109
  (declare (xargs :stobjs (rand)))
 
110
  (mv-let (num rand)
 
111
          (genrandom 2 rand)
 
112
          (mv (= 1 num) rand)))
 
113
 
 
114
(defthm random-boolean-type
 
115
  (booleanp (car (random-boolean r)))
 
116
  :rule-classes :type-prescription)
 
117
 
 
118
(in-theory (disable random-boolean))
 
119
 
 
120
;generate naturals according to a pseudo-geometric distribution
 
121
(defun random-natural-basemax (base maxdigits rand)
 
122
  (declare (xargs :stobjs (rand)
 
123
                  :guard (and (posp base)
 
124
                              (natp maxdigits))))
 
125
  (if (or (zp maxdigits) (zp base))
 
126
    (mv 0 rand)
 
127
    (mv-let (v rand)
 
128
            (genrandom (* 2 base) rand)
 
129
            (if (>= v base)
 
130
              (mv-let (v2 rand)
 
131
                      (random-natural-basemax base (1- maxdigits) rand)
 
132
                      (mv (+ (- v base) (* base (nfix v2))) rand))
 
133
              (mv v rand)))))
 
134
 
 
135
(defun random-natural (rand)
 
136
  (declare (xargs :stobjs (rand)))
 
137
  (random-natural-basemax 10 6 rand))
 
138
 
 
139
(defun random-length (rand)
 
140
  (declare (xargs :stobjs (rand)))
 
141
  (random-natural-basemax 4 2 rand))
 
142
 
 
143
(defthm random-natural-basemax-type
 
144
  (natp (car (random-natural-basemax b d r)))
 
145
  :rule-classes :type-prescription)
 
146
 
 
147
(defthm random-natural-type
 
148
  (natp (car (random-natural r)))
 
149
  :rule-classes :type-prescription)
 
150
 
 
151
(defthm random-length-type
 
152
  (natp (car (random-length r)))
 
153
  :rule-classes :type-prescription)
 
154
 
 
155
(in-theory (disable random-natural-basemax
 
156
                    random-natural
 
157
                    random-length))
 
158
 
 
159
 
 
160
 
 
161
 
 
162
; generate indices uniformly within a specified length 
 
163
(defun random-index (len rand)
 
164
  (declare (xargs :stobjs (rand)
 
165
                  :guard (posp len)))
 
166
  (genrandom len rand))
 
167
 
 
168
             
 
169
;generate integers according to a pseudo-geometric distribution
 
170
(defun random-integer (rand)
 
171
  (declare (xargs :stobjs (rand)))
 
172
  (mv-let (sign rand)
 
173
          (random-boolean rand)
 
174
          (mv-let (nat rand)
 
175
                  (random-natural rand)
 
176
                  (mv (if sign nat (- nat))
 
177
                      rand))))
 
178
 
 
179
(defthm random-integer-type
 
180
  (integerp (car (random-integer r)))
 
181
  :rule-classes :type-prescription)
 
182
 
 
183
(in-theory (disable random-integer))
 
184
 
 
185
 
 
186
;or generate integers with a uniform distribution, between i & j (incl.)
 
187
(defun random-int-between (i j rand)
 
188
  (declare (xargs :stobjs (rand)
 
189
                  :guard (and (integerp i)
 
190
                              (integerp j))))
 
191
  (let ((low (ifix (min i j)))
 
192
        (high (ifix (max i j))))
 
193
    (mv-let
 
194
     (num rand)
 
195
     (genrandom (1+ (- high low)) rand)
 
196
     (mv (+ low num) rand))))
 
197
 
 
198
(defthm random-int-between-type
 
199
  (integerp (car (random-int-between i j r)))
 
200
  :rule-classes :type-prescription)
 
201
 
 
202
(defthm random-int-between-lower
 
203
  (implies (and (integerp i)
 
204
                (integerp j)
 
205
                (<= i j))
 
206
           (<= i (car (random-int-between i j r))))
 
207
  :rule-classes :linear)
 
208
 
 
209
(defthm random-int-between-upper
 
210
  (implies (and (integerp i)
 
211
                (integerp j)
 
212
                (<= i j))
 
213
           (>= j (car (random-int-between i j r))))
 
214
  :rule-classes :linear)
 
215
 
 
216
(in-theory (disable random-int-between))
 
217
 
 
218
 
 
219
; generate a signed rational with pseudo-geometric numerator & denominator 
 
220
(defun random-rational (rand)
 
221
  (declare (xargs :stobjs (rand)))
 
222
  (mv-let (numer rand)
 
223
          (random-integer rand)
 
224
          (mv-let (denom-1 rand)
 
225
                  (random-natural rand)
 
226
                  (mv (/ numer
 
227
                         (+ 1 denom-1))
 
228
                      rand))))
 
229
 
 
230
(defthm random-rational-type
 
231
  (rationalp (car (random-rational r)))
 
232
  :rule-classes :type-prescription)
 
233
 
 
234
(in-theory (disable random-rational))
 
235
 
 
236
 
 
237
; pseudo-uniform rational between 0 and 1 (inclusive)
 
238
(defun random-probability (rand)
 
239
  (declare (xargs :stobjs (rand)))
 
240
  (mv-let (a rand)
 
241
          (random-natural rand)
 
242
          (mv-let (b rand)
 
243
                  (random-natural rand)
 
244
                  (let ((denom (* (1+ a) (1+ b))))
 
245
                    (mv-let (numer rand)
 
246
                            (genrandom (1+ denom) rand)
 
247
                            (mv (/ numer denom) rand))))))
 
248
 
 
249
(defthm random-probability-type
 
250
  (rationalp (car (random-probability r)))
 
251
  :rule-classes :type-prescription)
 
252
 
 
253
(defthm random-probability>=0
 
254
  (<= 0 (car (random-probability r)))
 
255
  :rule-classes (:linear :type-prescription)) 
 
256
 
 
257
(encapsulate nil
 
258
  (local (include-book "arithmetic/rationals" :dir :system))
 
259
 
 
260
  #|
 
261
  (local
 
262
   (defthm numerator<=denominator-implies-<=1
 
263
     (implies (and (natp n)
 
264
                   (posp d)
 
265
                   (<= n d))
 
266
              (<= (* (/ d) n)
 
267
                  1))))
 
268
  |#
 
269
  
 
270
  (defthm random-probability<=1
 
271
    (<= (car (random-probability r)) 1)
 
272
    :rule-classes :linear))
 
273
 
 
274
(in-theory (disable random-probability))
 
275
 
 
276
 
 
277
;generate a random rational whose absolute value is lte x
 
278
(defun random-rational-between (x y rand)
 
279
  (declare (xargs :stobjs (rand)
 
280
                  :guard (and (rationalp x)
 
281
                              (rationalp y))))
 
282
  (mv-let (p rand)
 
283
          (random-probability rand)
 
284
          (mv (rfix
 
285
               (if (< x y)
 
286
                 (+ x (* p (- y x)))
 
287
                 (+ y (* p (- x y)))))
 
288
              rand)))
 
289
 
 
290
(defthm random-rational-between-type
 
291
  (rationalp (car (random-rational-between i j r)))
 
292
  :rule-classes :type-prescription)
 
293
 
 
294
(encapsulate nil
 
295
  (local (include-book "arithmetic-3/top" :dir :system))
 
296
  
 
297
  (defthm random-rational-between-lower
 
298
    (implies (and (rationalp i)
 
299
                  (rationalp j)
 
300
                  (<= i j))
 
301
             (<= i (car (random-rational-between i j r))))
 
302
    :rule-classes :linear)
 
303
 
 
304
  (local (defthm random-rational-between-upper-lemma2
 
305
           (implies (and (rationalp i)
 
306
                         (rationalp j)
 
307
                         (rationalp p)
 
308
                         (<= 0 p)
 
309
                         (<= p 1)
 
310
                         (< i j))
 
311
                    (<= (* i p)
 
312
                        (* j p)))
 
313
           :rule-classes nil))
 
314
  
 
315
  (local 
 
316
   (defthm random-rational-between-upper-lemma
 
317
     (implies (and (rationalp i)
 
318
                   (rationalp j)
 
319
                   (rationalp p)
 
320
                   (<= 0 p)
 
321
                   (<= p 1)
 
322
                   (< i j))
 
323
              (<= (+ i (* j p))
 
324
                  (+ j (* i p))))
 
325
     :hints (("Goal" :use (:instance
 
326
                           random-rational-between-upper-lemma2
 
327
                           (p (- 1 p)))))))
 
328
 
 
329
  (defthm random-rational-between-upper
 
330
    (implies (and (rationalp i)
 
331
                  (rationalp j)
 
332
                  (<= i j))
 
333
             (<= (car (random-rational-between i j r)) j))
 
334
    :rule-classes :linear))
 
335
 
 
336
(in-theory (disable random-rational-between))
 
337
 
 
338
 
 
339
 
 
340
;generate non-zero integers according to a pseudo-geometric distribution
 
341
(defun random-nonzero-integer (rand)
 
342
  (declare (xargs :stobjs (rand)))
 
343
  (mv-let (sign rand)
 
344
          (random-boolean rand)
 
345
          (mv-let (nat rand)
 
346
                  (random-natural rand)
 
347
                  (mv (if sign (+ 1 nat) (- -1 nat))
 
348
                      rand))))
 
349
 
 
350
(defthm random-nonzero-integer-type
 
351
  (and (integerp (car (random-nonzero-integer r)))
 
352
       (not (equal (car (random-nonzero-integer r)) 0)))
 
353
  :rule-classes :type-prescription)
 
354
 
 
355
(in-theory (disable random-nonzero-integer))
 
356
 
 
357
 
 
358
 
 
359
 
 
360
; generate a signed rational with pseudo-geometric numerator & denominator 
 
361
(defun random-nonzero-rational (rand)
 
362
  (declare (xargs :stobjs (rand)))
 
363
  (mv-let (numer rand)
 
364
          (random-nonzero-integer rand)
 
365
          (mv-let (denom-1 rand)
 
366
                  (random-natural rand)
 
367
                  (mv (/ numer
 
368
                         (+ 1 denom-1))
 
369
                      rand))))
 
370
 
 
371
(defthm random-nonzero-rational-type
 
372
  (and (rationalp (car (random-nonzero-rational r)))
 
373
       (not (equal (car (random-nonzero-rational r)) 0)))
 
374
  :rule-classes :type-prescription)
 
375
 
 
376
(in-theory (disable random-nonzero-rational))
 
377
 
 
378
 
 
379
; generate a (strictly) complex number from rationals
 
380
(defun random-complex (rand)
 
381
  (declare (xargs :stobjs (rand)))
 
382
  (mv-let (rpart rand)
 
383
          (random-rational rand)
 
384
          (mv-let (ipart rand)
 
385
                  (random-nonzero-rational rand)
 
386
                  (mv (complex rpart ipart) rand))))
 
387
 
 
388
(defthm random-complex-type
 
389
  (complex-rationalp (car (random-complex r)))
 
390
  :rule-classes :type-prescription)
 
391
 
 
392
(in-theory (disable random-complex))
 
393
 
 
394
 
 
395
 
 
396
 
 
397
(defmacro random-element (lst rand-rand)
 
398
  `(mv-let (random-element-macro-idx rand)
 
399
           (random-index (length ,lst) ,rand-rand)
 
400
           (mv (nth random-element-macro-idx ,lst) rand)))
 
401
 
 
402
(defmacro random-element-len (lst len rand-rand)
 
403
  `(if (mbt (<= ,len (len ,lst)))
 
404
     (mv-let (random-element-macro-idx rand)
 
405
             (random-index ,len ,rand-rand)
 
406
             (mv (nth random-element-macro-idx ,lst) rand))
 
407
     (mv (car ,lst) rand)))
 
408
 
 
409
 
 
410
 
 
411
(defconst *standard-chars-len*
 
412
  (len *standard-chars*))
 
413
 
 
414
(defun random-char (rand)
 
415
  (declare (xargs :stobjs (rand)))
 
416
  (random-element-len *standard-chars*
 
417
                      *standard-chars-len*
 
418
                      rand))
 
419
 
 
420
(defthm random-char-type
 
421
  (characterp (car (random-char r)))
 
422
  :rule-classes :type-prescription)
 
423
 
 
424
(in-theory (disable random-char))
 
425
 
 
426
 
 
427
(defun random-char-list-len (len rand)
 
428
  (declare (xargs :stobjs (rand)
 
429
                  :guard (natp len)))
 
430
  (if (zp len)
 
431
    (mv nil rand)
 
432
    (mv-let (c rand)
 
433
            (random-char rand)
 
434
            (mv-let (lst rand)
 
435
                    (random-char-list-len (1- len) rand)
 
436
                    (mv (cons c lst) rand)))))
 
437
 
 
438
(defthm random-char-list-len-type
 
439
  (character-listp (car (random-char-list-len l r)))
 
440
  :rule-classes :type-prescription)
 
441
 
 
442
(in-theory (disable random-char-list-len))
 
443
 
 
444
 
 
445
(defun random-string-len (len rand)
 
446
  (declare (xargs :stobjs (rand)
 
447
                  :guard (natp len)))
 
448
  (mv-let (lst rand)
 
449
          (random-char-list-len len rand)
 
450
          (mv (coerce lst 'string) rand)))
 
451
 
 
452
(defthm random-string-len-type
 
453
  (stringp (car (random-string-len l r)))
 
454
  :rule-classes :type-prescription)
 
455
 
 
456
(in-theory (disable random-string-len))
 
457
 
 
458
 
 
459
;generate a random string of pseudogeometric length
 
460
(defun random-string (rand)
 
461
  (declare (xargs :stobjs (rand)))
 
462
  (mv-let (len rand)
 
463
          (random-length rand)
 
464
          (random-string-len len rand)))
 
465
 
 
466
(defthm random-string-type
 
467
  (stringp (car (random-string r)))
 
468
  :rule-classes :type-prescription)
 
469
 
 
470
(in-theory (disable random-string))
 
471
 
 
472
 
 
473
;generate a random symbol of pseudogeometric length
 
474
(defun random-symbol-same-package (sym rand)
 
475
  (declare (xargs :stobjs (rand)
 
476
                  :guard (symbolp sym)))
 
477
  (mv-let (str rand)
 
478
          (random-string rand)
 
479
          (mv (intern-in-package-of-symbol str sym) rand)))
 
480
 
 
481
(defthm random-symbol-same-package-type
 
482
  (implies (symbolp sym)
 
483
           (symbolp (car (random-symbol-same-package sym r))))
 
484
  :rule-classes :type-prescription)
 
485
 
 
486
(defthmd random-symbol-same-package_expand-package
 
487
  (implies (symbolp sym)
 
488
           (equal (car (random-symbol-same-package sym r))
 
489
                  (intern-in-package-of-symbol
 
490
                   (symbol-name (car (random-symbol-same-package sym r)))
 
491
                   sym))))
 
492
 
 
493
(defthmd random-symbol-same-package_suck-package
 
494
  (implies (symbolp sym)
 
495
           (equal (intern-in-package-of-symbol
 
496
                   (symbol-name (car (random-symbol-same-package sym r)))
 
497
                   sym)
 
498
                  (car (random-symbol-same-package sym r)))))
 
499
 
 
500
(in-theory (disable random-symbol-same-package))
 
501
 
 
502
 
 
503
(defun random-keyword (rand)
 
504
  (declare (xargs :stobjs (rand)))
 
505
  (random-symbol-same-package :acl2-pkg-witness rand))
 
506
 
 
507
(defthm random-keyword-type
 
508
  (symbolp (car (random-keyword r)))
 
509
  :hints (("Goal" :use (:instance random-symbol-same-package_expand-package 
 
510
                        (sym :acl2-pkg-witness))))
 
511
  :rule-classes :type-prescription)
 
512
 
 
513
(encapsulate
 
514
  ()
 
515
 
 
516
; [Jared] Previously keyword-package-intern had the following hints:
 
517
 
 
518
  ;; :hints (("Goal" :use (:instance keyword-package (x str) (y key))))))
 
519
 
 
520
; But in my copy of ACL2 the keyword-package axiom doesn't seem to have any
 
521
; variables, so I'm not sure what's going on.  I've fixed this up to work in
 
522
; my copy, maybe this is right?
 
523
 
 
524
  (local (defthm l0
 
525
           (equal (member-symbol-name str nil)
 
526
                  nil)
 
527
           :hints(("Goal" :in-theory (enable member-symbol-name)))))
 
528
 
 
529
  (local (defthm keyword-package-intern
 
530
           (implies (and (stringp str)
 
531
                         (keywordp key))
 
532
                    (equal (symbol-package-name
 
533
                            (intern-in-package-of-symbol str key))
 
534
                           "KEYWORD"))
 
535
           :hints(("Goal"
 
536
                   :in-theory (disable keyword-package
 
537
                                       SYMBOL-PACKAGE-NAME-INTERN-IN-PACKAGE-OF-SYMBOL)
 
538
                   :use ((:instance keyword-package)
 
539
                         (:instance SYMBOL-PACKAGE-NAME-INTERN-IN-PACKAGE-OF-SYMBOL
 
540
                                    (x str)
 
541
                                    (y key)))))
 
542
           ))
 
543
 
 
544
  (defthm random-keyword-keyword
 
545
    (equal (symbol-package-name (car (random-keyword r)))
 
546
           "KEYWORD")
 
547
    :hints (("Goal" :use (:instance random-symbol-same-package_expand-package 
 
548
                                    (sym :acl2-pkg-witness))))))
 
549
 
 
550
(in-theory (disable random-keyword))
 
551
 
 
552
 
 
553
 
 
554
 
 
555
;some composites
 
556
 
 
557
(defun random-number (rand)
 
558
  (declare (xargs :stobjs (rand)))
 
559
  (mv-let (v rand)
 
560
          (random-index 4 rand)
 
561
          (case v
 
562
                (0 (random-natural rand))
 
563
                (1 (random-integer rand))
 
564
                (2 (random-rational rand))
 
565
                (t (random-complex rand)))))
 
566
 
 
567
(defthm random-number-type
 
568
  (acl2-numberp (car (random-number r)))
 
569
  :rule-classes :type-prescription)
 
570
 
 
571
(in-theory (disable random-number))
 
572
 
 
573
 
 
574
(defconst *acl2-exports-len*
 
575
  (len *acl2-exports*))
 
576
(defconst *common-lisp-symbols-from-main-lisp-package-len*
 
577
  (len *common-lisp-symbols-from-main-lisp-package*))
 
578
 
 
579
(with-output
 
580
 :off (prove observation event)
 
581
 (defun random-symbol (rand)
 
582
   (declare (xargs :stobjs (rand)))
 
583
   (mv-let (v rand)
 
584
           (random-index 8 rand)
 
585
           (case
 
586
            v
 
587
            (0 (random-boolean rand))
 
588
            (1 (random-element-len
 
589
                *acl2-exports*
 
590
                *acl2-exports-len*
 
591
                rand))
 
592
            (2 (random-element-len
 
593
                *common-lisp-symbols-from-main-lisp-package*
 
594
                *common-lisp-symbols-from-main-lisp-package-len*
 
595
                rand))
 
596
            (3 (random-keyword rand))
 
597
            (4 (random-symbol-same-package 'acl2::acl2-pkg-witness rand))
 
598
            (5 (random-symbol-same-package 'acl2-user::acl2-pkg-witness rand))
 
599
            (6 (random-symbol-same-package 'common-lisp::acl2-pkg-witness rand))
 
600
            (t (random-symbol-same-package 'acl2-pc::acl2-pkg-witness rand))))))
 
601
 
 
602
(local (defthm nth-symbol-list
 
603
         (implies (force (symbol-listp l))
 
604
                  (symbolp (nth i l)))
 
605
         :rule-classes :type-prescription))
 
606
 
 
607
(with-output
 
608
 :off (prove observation event)
 
609
 (defthm random-symbol-type
 
610
   (symbolp (car (random-symbol r)))
 
611
   :rule-classes :type-prescription))
 
612
 
 
613
(in-theory (disable random-symbol))
 
614
 
 
615
 
 
616
 
 
617
(with-output
 
618
 :off (prove observation event)
 
619
 (defun random-acl2-symbol (rand)
 
620
   (declare (xargs :stobjs (rand)))
 
621
   (mv-let (v rand)
 
622
           (random-index 5 rand) ; skew toward generated symbols
 
623
           (case
 
624
            v
 
625
            (0 (random-boolean rand))
 
626
            (1 (random-element-len
 
627
                *acl2-exports*
 
628
                *acl2-exports-len*
 
629
                rand))
 
630
            (2 (random-element-len
 
631
                *common-lisp-symbols-from-main-lisp-package*
 
632
                *common-lisp-symbols-from-main-lisp-package-len*
 
633
                rand))
 
634
            (t (random-symbol-same-package 'acl2::acl2-pkg-witness rand))))))
 
635
 
 
636
(with-output
 
637
 :off (prove observation event)
 
638
 (defthm random-acl2-symbol-type
 
639
   (symbolp (car (random-acl2-symbol r)))
 
640
   :hints (("Goal" :use (:instance random-symbol-same-package_expand-package 
 
641
                         (sym 'acl2::acl2-pkg-witness))))
 
642
   :rule-classes :type-prescription))
 
643
 
 
644
(in-theory (disable random-acl2-symbol))
 
645
 
 
646
 
 
647
 
 
648
(defun random-atom (rand)
 
649
  (declare (xargs :stobjs (rand)))
 
650
  (mv-let (v rand)
 
651
          (random-index 4 rand)
 
652
          (case
 
653
           v
 
654
           (0 (random-number rand))
 
655
           (1 (random-char rand))
 
656
           (2 (random-symbol rand))
 
657
           (t (random-string rand)))))
 
658
 
 
659
(defthm random-atom-type
 
660
  (atom (car (random-atom r)))
 
661
  :rule-classes :type-prescription)
 
662
 
 
663
(in-theory (disable random-atom))#|ACL2s-ToDo-Line|#
 
664
 
 
665
 
 
666
 
 
667
 
 
668
 
 
669
 
 
670
 
 
671
 
 
672
#|
 
673
 
 
674
(defconst *atomic-value-types*
 
675
  '(:atom
 
676
     :number
 
677
      :complex
 
678
       :rational
 
679
        :integer
 
680
         :natural
 
681
 
 
682
     :character
 
683
 
 
684
     :symbol
 
685
      :acl2-symbol
 
686
       :boolean
 
687
      :keyword
 
688
     
 
689
     :string))
 
690
 
 
691
(defun random-value (spec rand)
 
692
  (declare (xargs :stobjs (rand)))
 
693
  (if (consp spec)
 
694
    (if (symbolp (car spec))
 
695
      (case (car spec)
 
696
        (quote
 
697
         (if (and (consp (cdr spec))
 
698
                  (null (cddr spec)))
 
699
           (mv (cadr spec) rand)
 
700
           (mv (er hard? 'random-value "Invalid quoted value: ~x0" spec)
 
701
               rand)))
 
702
        (cons
 
703
         (if (and (consp (cdr spec))
 
704
                  (consp (cddr spec))
 
705
                  (null (cdddr spec)))
 
706
           (mv-let (carval rand)
 
707
                   (random-value (cadr spec) rand)
 
708
                   (mv-let (cdrval rand)
 
709
                           (random-value (caddr spec) rand)
 
710
                           (mv (cons carval cdrval) rand)))
 
711
           (mv (er hard? 'random-value "Cons should take two parameters, unlike in ~x0" spec)
 
712
               rand)))
 
713
        (listof
 
714
|#
 
 
b'\\ No newline at end of file'