-
Notifications
You must be signed in to change notification settings - Fork 0
/
tau.lisp
13042 lines (11186 loc) · 571 KB
/
tau.lisp
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
; ACL2 Version 8.6 -- A Computational Logic for Applicative Common Lisp
; Copyright (C) 2024, Regents of the University of Texas
; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
; (C) 1997 Computational Logic, Inc. See the documentation topic NOTE-2-0.
; This program is free software; you can redistribute it and/or modify
; it under the terms of the LICENSE file distributed with ACL2.
; This program is distributed in the hope that it will be useful,
; but WITHOUT ANY WARRANTY; without even the implied warranty of
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
; LICENSE for more details.
; Written by: Matt Kaufmann and J Strother Moore
; email: [email protected] and [email protected]
; Department of Computer Science
; University of Texas at Austin
; Austin, TX 78712 U.S.A.
(in-package "ACL2")
; In this file we define the Tau system, a collection of data structures and
; algorithms for reasoning quickly about monadic predicates. However, we need
; certain basic facilities from the rest of ACL2's sources and we have put them
; all in the following ``prelude.'' See the Essay on the Tau System below for
; a discussion of the tau design.
; Prelude: General-Purpose Functions Having Nothing Specific to do with Tau
; A ``singleton evg list'' is a singleton list with an evg in it. A ``neg-evg
; list'' is a duplicate-free list of singleton evg lists, ordered ascending
; almost according to lexorder. The ``almost'' is due to the fact that we let
; the singleton list containing NIL be the smallest thing in our ordering. So
; a typical neg-evg list might be ((NIL) (0) (1) (2) (A) (B) (C)).
; Foreshadowing: a neg-evg list represents the evgs ruled out by a tau. If a
; tau were to contain the neg-evgs above, then the tau would include the
; conjuncts (not (equal x 'NIL)), (not (equal x '0)), ..., and (not (equal x
; 'C)). We want NIL in the front so that we can rapidly answer the question
; ``does this tau mean the subject is non-NIL?''
; We define the ``almost-lexorder'' function as well as functions for
; determining whether a singleton is a member of a neg-evg list and for
; inserting a singleton into such a list. These functions are optimized
; exploiting the fact that every item compared is known to be a singleton, so
; instead of using lexorder on (x) and (y) we use it on x and y, i.e., we
; always compare just the cars of the lists.
(defun almost-lexorder-singletons (x y)
(cond ((eq (car x) nil) t)
((eq (car y) nil) nil)
(t (lexorder (car x) (car y)))))
; We actually don't use almost-lexorder-singletons in the membership and
; insertion functions because we make special cases for nil.
(defun member-nil-neg-evgs (neg-evg-lst)
(and (consp neg-evg-lst)
(eq (car (car neg-evg-lst)) nil)))
(defun member-neg-evgs1 (evg neg-evg-lst)
; Evg is non-NIL and neg-evg-lst is a neg-evg list that does not contain (NIL).
(cond ((endp neg-evg-lst) nil)
((lexorder (car (car neg-evg-lst)) evg)
(or (equal evg (car (car neg-evg-lst)))
(member-neg-evgs1 evg (cdr neg-evg-lst))))
(t nil)))
(defun member-neg-evgs (x neg-evg-lst)
; X is a singleton list and neg-evg-lst is a neg-evg list -- a list of
; singletons ordered almost with lexorder but with (nil) as the smallest item
; in the ordering. We return t if x is a member of neg-evg-lst and nil
; otherwise.
(cond ((endp neg-evg-lst) nil)
((equal (car x) (car (car neg-evg-lst)))
t)
((eq (car x) nil) nil)
(t (member-neg-evgs1 (car x) (cdr neg-evg-lst)))))
(defun insert-neg-evgs1 (evg x neg-evg-lst)
; X is a singleton evg list containing evg. Evg is non-nil. Neg-evg-lst is a
; neg-evg list that does not contain (NIL) and does not contain x. We insert x
; into neg-evg-lst.
(cond ((endp neg-evg-lst) (cons x nil))
((lexorder (car (car neg-evg-lst)) evg)
(cons (car neg-evg-lst)
(insert-neg-evgs1 evg x (cdr neg-evg-lst))))
(t (cons x neg-evg-lst))))
(defun insert-neg-evgs (x neg-evg-lst)
(cond ((endp neg-evg-lst) (cons x neg-evg-lst))
((eq (car x) nil) (cons x neg-evg-lst))
((eq (car (car neg-evg-lst)) nil)
(cons (car neg-evg-lst)
(insert-neg-evgs1 (car x) x (cdr neg-evg-lst))))
(t (insert-neg-evgs1 (car x) x neg-evg-lst))))
; Now we define some other sorting functions.
(defun merge-car-< (l1 l2)
(cond ((null l1) l2)
((null l2) l1)
((< (car (car l1)) (car (car l2)))
(cons (car l1) (merge-car-< (cdr l1) l2)))
(t (cons (car l2) (merge-car-< l1 (cdr l2))))))
(defun merge-sort-car-< (l)
; Merge-sort, where elements a and b are compared via (car a) < (car b).
(cond ((null (cdr l)) l)
(t (merge-car-< (merge-sort-car-< (evens l))
(merge-sort-car-< (odds l))))))
(defun merge-cadr-< (l1 l2)
(cond ((null l1) l2)
((null l2) l1)
((< (cadr (car l1)) (cadr (car l2)))
(cons (car l1) (merge-cadr-< (cdr l1) l2)))
(t (cons (car l2) (merge-cadr-< l1 (cdr l2))))))
(defun merge-sort-cadr-< (l)
; Merge-sort, where elements a and b are compared via (cadr a) < (cadr b).
(cond ((null (cdr l)) l)
(t (merge-cadr-< (merge-sort-cadr-< (evens l))
(merge-sort-cadr-< (odds l))))))
(defun strip-caddrs (x)
(declare (xargs :guard (all->=-len x 3)))
(cond ((endp x) nil)
(t (cons (caddar x) (strip-caddrs (cdr x))))))
; In forming rules from terms we often strip out individual branches of the
; term, e.g., (implies (and h1 h2) (and c1 (implies h3 c2))) is treated as
; though it were (and (implies (and h1 h2) c1) (implies (and h1 h2 h3) c2)),
; except after distributing the IMPLIES over the concluding ANDs, we do not
; form a term but just traffic in list of pairs (((h1 h2) . c1) ((h1 h2 h3)
; . c2)). This is called ``unprettyifying.''
(defun unprettyify/add-hyps-to-pairs (hyps lst)
; Each element of lst is a pair of the form (hypsi . concli), where hypsi
; is a list of terms. We append hyps to hypsi in each pair.
(cond ((null lst) nil)
(t (cons (cons (append hyps (caar lst)) (cdar lst))
(unprettyify/add-hyps-to-pairs hyps (cdr lst))))))
(defun unprettyify (term)
; This function returns a list of pairs (hyps . concl) such that the
; conjunction of all (implies (and . hyps) concl) is equivalent to
; term. Hyps is a list of hypotheses, implicitly conjoined. Concl
; does not begin with an AND (of course, its a macro, but concl
; doesn't begin with an IF that represents an AND) or IMPLIES.
; In addition concl doesn't begin with an open lambda.
; This function is used to extract the :REWRITE rules from a term.
; Lambdas are sort of expanded to expose the conclusion. They are not
; expanded in the hypotheses, or within a function symbol other than
; the top-level IFs and IMPLIES. But top-level lambdas (those enclosing
; the entire term) are blown away.
; Thus, if you have a proposed :REWRITE rule
; (implies (and p q) (let ((x a)) (equal (f x) b)))
; it will be converted to
; (implies (and p q) (equal (f a) b)).
; The rule
; (let ((x a)) (implies (and (p x) (q x)) (equal (f x) b))) [1]
; will become
; (implies (and (p a) (q a)) (equal (f a) b)). [2]
; But
; (implies (let ((x a)) (and (p x) (q x))) [3]
; (equal (let ((x a)) (f x)) b))
; stays untouched. In general, once you've moved the let into a
; hypothesis it is not seen or opened. Once you move it into the
; equivalence relation of the conclusion it is not seen or opened.
; Note that this processing of lambdas can cause terms to be duplicated
; and simplified more than once (see a in [2] compared to [3]).
(case-match term
(('if t1 t2 t3)
(cond ((equal t2 *nil*)
(append (unprettyify (dumb-negate-lit t1))
(unprettyify t3)))
((equal t3 *nil*)
(append (unprettyify t1)
(unprettyify t2)))
(t (list (cons nil term)))))
(('implies t1 t2)
(unprettyify/add-hyps-to-pairs
(flatten-ands-in-lit t1)
(unprettyify t2)))
((('lambda vars body) . args)
(unprettyify (subcor-var vars args body)))
(& (list (cons nil term)))))
(defun reprettyify (hyps concl wrld)
(cond ((null hyps)
(untranslate concl t wrld))
((null (cdr hyps))
`(IMPLIES ,(untranslate (car hyps) t wrld)
,(untranslate concl t wrld)))
(t `(IMPLIES (AND ,@(untranslate-lst hyps t wrld))
,(untranslate concl t wrld)))))
; Before moving on, we develop the code to translate a type-prescription
; to a term so that we can recognize if a type-prescription can be
; represented as a tau signature rule.
; The next few functions are used to produce the formulas represented by
; type-prescriptions.
(defun convert-returned-vars-to-term-lst (term vars)
(cond ((null vars) nil)
(t (cons (mcons-term* 'equal term (car vars))
(convert-returned-vars-to-term-lst term (cdr vars))))))
(defun implicate (t1 t2)
; We return a term equivalent to (IMPLIES t1 t2).
(declare (xargs :guard (and (pseudo-termp t1)
(pseudo-termp t2))))
(cond ((equal t1 *t*) t2)
((equal t1 *nil*) *t*)
((equal t2 *t*) *t*)
((equal t2 *nil*) (dumb-negate-lit t1))
(t (mcons-term* 'implies t1 t2))))
; We now develop the function that converts a type-set into a term.
(defrec type-set-inverter-rule ((nume . ts) terms . rune) nil)
; A type-set-inverter-rule states that x has type-set ts iff the conjunction of
; terms{X/x} is true. Thus, for example, if :ts is *ts-integer* then :terms is
; '((INTEGERP X)).
; WARNING: See the warning in convert-type-set-to-term if you are ever
; tempted to generalize type-set-inverter-rules to allow hypotheses that
; may be FORCEd or CASE-SPLITd!
; A type-set, s, is a disjunction of the individual bits in it. Thus, to
; create a term whose truth is equivalent to the claim that X has type-set s it
; is sufficient to find any type-set-inverter-rule whose :ts is a subset of s
; and then disjoin the :term of that rule to the result of recursively creating
; the term recognizing s minus :ts. This assumes one has a rule for each
; single type bit.
; The following is the initial setting of the world global variable
; 'type-set-inverter-rules. WARNING: EACH TERM IN :TERMS MUST BE IN TRANSLATED
; FORM. The list is ordered in an important way: the larger type-sets are at
; the front. This ordering is exploited by convert-type-set-to-term-lst which
; operates by finding the largest recognized type set group and knocks it out
; of the type set.
;; Historical Comment from Ruben Gamboa:
;; I added a rule for realp, non-zero real, non-negative real,
;; non-positive real, positive real, negative real, irrational,
;; negative irrational, positive irrational, and complex.
(defconst *initial-type-set-inverter-rules*
(list (make type-set-inverter-rule ;;; 12 (15) bits
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts (ts-complement *ts-cons*)
:terms '((atom x)))
(make type-set-inverter-rule ;;; 7 (10) bits
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts *ts-acl2-number*
:terms '((acl2-numberp x)))
#+:non-standard-analysis
(make type-set-inverter-rule ;;; _ (8) bits
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts *ts-real*
:terms '((realp x)))
(make type-set-inverter-rule ;;; 6 bits
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts *ts-rational*
:terms '((rationalp x)))
(make type-set-inverter-rule ;;; 6 (9) bits
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts (ts-intersection *ts-acl2-number* (ts-complement *ts-zero*))
:terms '((acl2-numberp x) (not (equal x '0))))
#+:non-standard-analysis
(make type-set-inverter-rule ;;; _ (7) bits
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts (ts-intersection *ts-real* (ts-complement *ts-zero*))
:terms '((realp x) (not (equal x '0))))
(make type-set-inverter-rule ;;; 5 bits
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts (ts-intersection *ts-rational* (ts-complement *ts-zero*))
:terms '((rationalp x) (not (equal x '0))))
#+:non-standard-analysis
(make type-set-inverter-rule ;;; _ (5) bits
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts (ts-union *ts-positive-real* *ts-zero*)
:terms '((realp x) (not (< x '0))))
(make type-set-inverter-rule ;;; 4 bits
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts (ts-union *ts-positive-rational* *ts-zero*)
:terms '((rationalp x) (not (< x '0))))
#+:non-standard-analysis
(make type-set-inverter-rule ;;; _ (4) bits
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts (ts-union *ts-negative-real* *ts-zero*)
:terms '((realp x) (not (< '0 x))))
(make type-set-inverter-rule ;;; 3 bits
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts (ts-union *ts-negative-rational* *ts-zero*)
:terms '((rationalp x) (not (< '0 x))))
(make type-set-inverter-rule ;;; 4 bits
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts *ts-integer*
:terms'((integerp x)))
(make type-set-inverter-rule ;;; 3 bits
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts (ts-intersection *ts-integer* (ts-complement *ts-zero*))
:terms '((integerp x) (not (equal x '0))))
#+:non-standard-analysis
(make type-set-inverter-rule ;;; _ (4) bits
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts *ts-positive-real*
:terms'((realp x) (< '0 x)))
(make type-set-inverter-rule ;;; 3 bits
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts *ts-positive-rational*
:terms'((rationalp x) (< '0 x)))
#+:non-standard-analysis
(make type-set-inverter-rule ;;; _ (3) bits
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts *ts-negative-real*
:terms'((realp x) (< x '0)))
(make type-set-inverter-rule ;;; 2 bits
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts *ts-negative-rational*
:terms'((rationalp x) (< x '0)))
(make type-set-inverter-rule ;;; 3 bits
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts (ts-union *ts-positive-integer* *ts-zero*)
:terms '((integerp x) (not (< x '0))))
(make type-set-inverter-rule ;;; 2 bits
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts (ts-union *ts-negative-integer* *ts-zero*)
:terms '((integerp x) (not (< '0 x))))
#+:non-standard-analysis
(make type-set-inverter-rule ;;; _ (2) bits
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts *ts-non-ratio*
:terms'((realp x) (not (rationalp x))))
(make type-set-inverter-rule ;;; 2 bits
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts *ts-ratio*
:terms'((rationalp x) (not (integerp x))))
#+:non-standard-analysis
(make type-set-inverter-rule ;;; _ (1) bit
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts *ts-negative-non-ratio*
:terms'((realp x) (not (rationalp x)) (< x '0)))
(make type-set-inverter-rule ;;; 1 bit
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts *ts-negative-ratio*
:terms'((rationalp x) (not (integerp x)) (< x '0)))
(make type-set-inverter-rule ;;; 1 bit
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts *ts-negative-integer*
:terms'((integerp x) (< x '0)))
#+:non-standard-analysis
(make type-set-inverter-rule ;;; _ (1) bit
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts *ts-positive-non-ratio*
:terms'((realp x) (not (rationalp x)) (< '0 x)))
(make type-set-inverter-rule ;;; 1 bit
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts *ts-positive-ratio*
:terms'((rationalp x) (not (integerp x)) (< '0 x)))
(make type-set-inverter-rule ;;; 2 bits
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts *ts-positive-integer*
:terms'((integerp x) (< '0 x)))
#+:non-standard-analysis
(make type-set-inverter-rule ;;; _ (2) bits
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts *ts-complex*
:terms'((complexp x)))
(make type-set-inverter-rule ;;; 1 bit
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts *ts-integer>1*
:terms'((integerp x) (< '1 x)))
(make type-set-inverter-rule ;;; 1 bit
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts *ts-complex-rational*
:terms'((complex-rationalp x)))
#+:non-standard-analysis
(make type-set-inverter-rule ;;; _ (1) bit
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts *ts-complex-non-rational*
:terms'((complexp x) (not (complex-rationalp x))))
(make type-set-inverter-rule ;;; 1 bit
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts *ts-zero*
:terms'((equal x '0)))
(make type-set-inverter-rule ;;; 1 bit
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts *ts-one*
:terms'((equal x '1)))
(make type-set-inverter-rule ;;; 3 bits
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts *ts-symbol*
:terms'((symbolp x)))
(make type-set-inverter-rule ;;;2 bits
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts *ts-boolean*
:terms'((if (equal x 't) 't (equal x 'nil))))
(make type-set-inverter-rule ;;; 2 bits
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts *ts-cons*
:terms'((consp x)))
(make type-set-inverter-rule ;;; 2 bits
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts *ts-true-list*
:terms'((true-listp x)))
(make type-set-inverter-rule ;;; 1 bit
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts *ts-improper-cons*
:terms'((consp x) (not (true-listp x))))
(make type-set-inverter-rule ;;; 1 bit
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts *ts-proper-cons*
:terms'((consp x) (true-listp x)))
(make type-set-inverter-rule ;;; 1 bit
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts *ts-non-t-non-nil-symbol*
:terms '((symbolp x) (not (equal x 't)) (not (equal x 'nil))))
(make type-set-inverter-rule ;;; 1 bit
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts *ts-t*
:terms'((equal x 't)))
(make type-set-inverter-rule ;;; 1 bit
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts *ts-nil*
:terms'((equal x 'nil)))
(make type-set-inverter-rule ;;; 1 bit
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts *ts-string*
:terms'((stringp x)))
(make type-set-inverter-rule ;;; 1 bit
:nume nil
:rune *fake-rune-for-anonymous-enabled-rule*
:ts *ts-character*
:terms'((characterp x)))))
(defun convert-type-set-to-term-lst (ts rules ens lst ttree)
; We map over the list of type-set-inverter rules and each time we find an
; enabled rule whose :ts is a subset of ts, we accumulate its conjoined :terms
; and its :rune, and knock off those bits of ts. We return (mv lst ttree),
; where lst is a list of terms in the variable X whose disjunction is
; equivalent to ts.
(cond
((null rules) (mv (reverse lst) ttree))
((and (enabled-numep (access type-set-inverter-rule (car rules) :nume) ens)
(ts= (access type-set-inverter-rule (car rules) :ts)
(ts-intersection
(access type-set-inverter-rule (car rules) :ts)
ts)))
(convert-type-set-to-term-lst
(ts-intersection
ts
(ts-complement (access type-set-inverter-rule (car rules) :ts)))
(cdr rules)
ens
(add-to-set-equal
(conjoin (access type-set-inverter-rule (car rules) :terms))
lst)
(push-lemma (access type-set-inverter-rule (car rules) :rune)
ttree)))
(t (convert-type-set-to-term-lst ts (cdr rules) ens lst ttree))))
(defun convert-type-set-to-term1 (x ts flg ens w ttree)
; X is a term and ts a type-set. We generate a term that is provably
; equivalent, in w, to "x has type set ts".
; E.g., if x is the term (FN X Y) and ts is *ts-rational* then our output will
; be (RATIONALP (FN X Y)), whether flg is t or nil. We return (mv term ttree),
; where term is the term and ttree contains the 'lemmas used. We do not use
; disabled type-set-inverters.
; The only time flg matters is the case that flg is true, term is known to be
; Boolean, and ts is *ts-t*. In that case we return x instead of the provably
; equivalent (equal x 'T). If you're trying to explain or show what a type-set
; means, you need to use flg = nil. But if you're trying to assume or prove
; that x has the given type-set, you may use flg = t. See the comment where
; flg is used below for an explanation of why this feature matters.
; Note: This function is just a helper function for convert-type-set-to-term.
; That function is called in several places in the ACL2 code and in a couple of
; books. To save the bother of changing those calls, we named this function
; convert-type-set-to-term1. Convert-type-set-to-term calls it with flg=nil.
; The only place that this function is called directly (and with flg=t) is
; clausify-type-alist, which is used by clausify-assumption.
; Note: It would be a major change to make this function force assumptions.
; If the returned ttree contains 'assumption tags then the primary use of
; this function, namely the expression of type-alists in clausal form so that
; assumptions can be attacked as clauses, becomes problematic. Don't glibly
; generalize type-set-inverter rules to force assumptions.
(cond ((ts= ts *ts-unknown*) (mv *t* ttree))
((and flg
(ts= ts *ts-t*)
(ts-booleanp x ens w))
; We commented out this case for Version_3.5 because of a soundness issue that
; no longer exists (because we don't create type-prescription rules for
; subversive functions; see putprop-type-prescription-lst). We left it
; commented out because we thought it was an unimportant case that hasn't been
; missed. But, while working with Version_6.4, we encountered a proof in a
; script from Warren Hunt that sped up from 77 seconds to 16 seconds when
; including this case. That script generated a lot of forced assumptions, and
; this code is responsible for creating the clauses proved in the forcing
; round. In particular, if a lemma is forced in a context in which one of the
; governing assumptions is (< alpha beta), then that assumption is encoded as
; (equal (< alpha beta) t) in the clause attacked by the forcing round -- if
; those clauses are generated by the code in Version_3.5 through Version_6.4,
; i.e., if flg=nil. But that means the inequality is hidden until the EQUAL is
; rewritten, delaying, for example, tau. In the Hunt script, tau can prove the
; clauses generated with flg = t. So, after Version_6.4 we restored this case,
; conditional on flg.
(mv x ttree))
((ts-complementp ts)
(mv-let (lst ttree)
(convert-type-set-to-term-lst
(ts-complement ts)
(global-val 'type-set-inverter-rules w)
ens nil ttree)
(mv (subst-var x 'x
(conjoin (dumb-negate-lit-lst lst)))
ttree)))
(t (mv-let (lst ttree)
(convert-type-set-to-term-lst
ts
(global-val 'type-set-inverter-rules w)
ens nil ttree)
(mv (subst-var x 'x (disjoin lst)) ttree)))))
(defun convert-type-set-to-term (x ts ens w ttree)
; See the comments in the helper function convert-type-set-to-term1.
; Note that this function is independent of the perhaps misleadingly named
; convert-type-set-to-term-lst. That function applies a list of
; type-set-inverter rules to a type-set, returning a list of disjuncts that
; express it.
(convert-type-set-to-term1 x ts nil ens w ttree))
(defun convert-type-prescription-to-term (tp ens wrld)
; Tp is a type-prescription. We generate a term that expresses it relative to
; the supplied ens. We will usually store this term in the :corollary of tp
; itself; generally the current :corollary field of tp is *t* right now because
; tp was generated by putprop-initial-type-prescriptions. We return
; the generated corollary term and a ttree citing the type-set-inverter
; rules used.
(mv-let (concl ttree)
(convert-type-set-to-term (access type-prescription tp :term)
(access type-prescription tp :basic-ts)
ens wrld nil)
(mv (implicate (conjoin (access type-prescription tp :hyps))
(disjoin
(cons concl
(convert-returned-vars-to-term-lst
(access type-prescription tp :term)
(access type-prescription tp :vars)))))
ttree)))
; The function all-runes-in-ttree, defined below, is typically used by each
; event function to recover the supporting runes from a ttree.
(defun all-runes-in-var-to-runes-alist (alist ans)
(cond ((null alist) ans)
(t (all-runes-in-var-to-runes-alist
(cdr alist)
(union-equal (cdr (car alist)) ans)))))
(defun all-runes-in-var-to-runes-alist-lst (lst ans)
(cond ((endp lst) ans)
(t (all-runes-in-var-to-runes-alist-lst
(cdr lst)
(all-runes-in-var-to-runes-alist (car lst) ans)))))
(defun union-equal-removing-duplicates (x y)
; Returns the same set as (union-equal x y), but is tail recursive and removes
; any duplicates from x.
(declare (xargs :guard (true-listp x)))
(cond ((endp x) y)
(t (union-equal-removing-duplicates
(cdr x)
(add-to-set-equal (car x) y)))))
(defrec summary-data
((runes . use-names)
.
(by-names . clause-processor-fns))
; The use of nil for the cheap flag helps to ensure that when one writes a
; clause-processor function without taking care to return a summary-data record
; (or nil) as the final, non-stobj argument, the error message will point that
; out.
nil)
(defmacro make-summary-data (&key runes use-names by-names clause-processor-fns)
; This macro would of course not be necessary for ACL2 developers, who can just
; as well call MAKE directly. However, make-summary-data provides a documented
; interface that hides the defrec machinery.
`(make summary-data
:runes ,runes
:use-names ,use-names
:by-names ,by-names
:clause-processor-fns ,clause-processor-fns))
(mutual-recursion
(defun all-runes-in-elim-sequence-lst (lst ans)
(cond ((endp lst) ans)
(t (all-runes-in-elim-sequence-lst
(cdr lst)
(all-runes-in-elim-sequence (car lst) ans)))))
(defun all-runes-in-elim-sequence (elim-sequence ans)
; Elim-sequence is a list of elements, each of which is of the form
; (rune rhs lhs alist restricted-vars var-to-runes-alist ttree)
; 0 1 2 3 4 5 6
(cond ((null elim-sequence) ans)
(t (all-runes-in-elim-sequence
(cdr elim-sequence)
(all-runes-in-ttree (nth 6 (car elim-sequence))
(all-runes-in-var-to-runes-alist
(nth 5 (car elim-sequence))
(add-to-set-equal (nth 0 (car elim-sequence))
ans)))))))
(defun all-runes-in-ttree-fc-derivation-lst (lst ans)
(cond ((endp lst) ans)
(t (all-runes-in-ttree-fc-derivation-lst
(cdr lst)
(add-to-set-equal
(access fc-derivation (car lst) :rune)
(all-runes-in-ttree (access fc-derivation (car lst) :ttree)
ans))))))
(defun all-runes-in-ttree-find-equational-poly-lst (lst ans)
(cond ((endp lst) ans)
(t (all-runes-in-ttree-find-equational-poly-lst
(cdr lst)
(let ((val (car lst))) ; Shape: (poly1 . poly2)
(all-runes-in-ttree
(access poly (car val) :ttree)
(all-runes-in-ttree (access poly (cdr val) :ttree)
ans)))))))
(defun all-runes-summary-data-lst (lst ans)
; Lst is a list of tuples of the form (clause-processor-hint summary-data
; . clauses). We collect the runes from those summary-data fields.
(cond ((endp lst) ans)
(t (all-runes-summary-data-lst
(cdr lst)
(let ((summary-data (cadr (car lst))))
(if summary-data
(union-equal-removing-duplicates
(access summary-data summary-data :runes)
ans)
ans))))))
(defun all-runes-in-ttree (ttree ans)
; Ttree is any ttree produced by this system. We sweep it collecting into ans
; every rune (or fake rune) in it.
(cond
((endp ttree) ans)
(t (all-runes-in-ttree
(cdr ttree)
(let ((tag (caar ttree))
(lst (cdar ttree)))
(case
tag
(lemma
; Shape: rune
(union-equal lst ans))
(:by
; Shape: (lmi-lst thm-cl-set constraint-cl k)
; As of this writing, there aren't any runes in an lmi list that are being
; treated as runes. Imagine proving a lemma that is then supplied in a :use
; hint. It shouldn't matter, from the point of view of tracking RUNES, whether
; that lemma created a rewrite rule that is currently disabled or whether that
; lemma has :rule-classes nil.
ans)
(:bye
; Shape: (name . cl), where name is a "new" name, not the name of something
; used.
ans)
(:or
; Shape (parent-cl-id nil-or-branch-number ((user-hint1 . hint-settings1) ...))
; See comment about the :by case above.
ans)
(:use
; Shape: ((lmi-lst (hyp1 ...) cl k) . n)
; See comment for the :by case above.
ans)
(:cases
; Shape: ((term1 ... termn) . clauses)
ans)
(preprocess-ttree
; Shape: ttree
(all-runes-in-ttree-lst lst ans))
(assumption
; Shape: assumption record
ans)
(pt
; Shape: parent tree - just numbers
ans)
(fc-derivation
; Shape: fc-derivation record
(all-runes-in-ttree-fc-derivation-lst lst ans))
(find-equational-poly
; Shape: (poly1 . poly2)
(all-runes-in-ttree-find-equational-poly-lst lst ans))
(variables
; Shape: var-lst
ans)
((splitter-if-intro
splitter-case-split
splitter-immed-forced)
; Shape: rune (Note: objects are a subset 'lemmas objects.)
ans)
(elim-sequence
; Shape: ((rune rhs lhs alist restricted-vars var-to-runes-alist ttree) ...)
(all-runes-in-elim-sequence-lst lst ans))
((literal ;;; Shape: term
hyp-phrase ;;; tilde-@ phrase
equiv ;;; equiv relation
bullet ;;; term
target ;;; term
cross-fert-flg ;;; boolean flg
delete-lit-flg ;;; boolean flg
clause-id ;;; clause-id
binding-lst ;;; alist binding vars to terms
terms ;;; list of terms
restricted-vars ;;; list of vars
evaluator-check-for-rule) ;;; returned by chk-meta-fn-attachments
ans)
((rw-cache-nil-tag
rw-cache-any-tag)
; Shape: rw-cache-entry
ans)
(var-to-runes-alist
; Shape: (...(var . (rune1 ...))...)
(all-runes-in-var-to-runes-alist-lst lst ans))
(ts-ttree
; Shape: ttree
(all-runes-in-ttree-lst lst ans))
((irrelevant-lits
clause)
; Shape: clause
ans)
(hidden-clause
; Shape: t
ans)
(abort-cause
; Shape: symbol
ans)
(bddnote
; Shape: bddnote
; A bddnote has a ttree in it. However, whenever a bddnote is put into a given
; ttree, the ttree from that bddnote is also added to the same given ttree.
; So, we don't really think of a bddnote as containing a "ttree" per se, but
; rather, a sort of data structure that is isomorphic to a ttree.
ans)
(case-limit
; Shape: t
ans)
(sr-limit
; Shape: t
ans)
(dropped-last-literal
; Shape: t
ans)
(:clause-processor
; Shape: (clause-processor-hint summary-data . clauses)
(all-runes-summary-data-lst lst ans))
(otherwise (er hard 'all-runes-in-ttree
"This function must know every possible tag so that ~
it can recover the runes used in a ttree. The ~
unknown tag ~x0, associated with the list of ~
values ~x1, has just been encountered."
tag
lst))))))))
(defun all-runes-in-ttree-lst (lst ans)
(cond ((endp lst) ans)
(t (all-runes-in-ttree-lst (cdr lst)
(all-runes-in-ttree (car lst) ans)))))
)
; Essay on the Tau System
; This essay touches on a wide variety of topics in the design of the tau
; system. It is consequently divided into many subsections with the following
; headers. We recommend scanning this list for subsections of interest; an
; introduction to tau is provided by the first six or so, in order.
; On Tau-Like Terms
; On the Name ``tau''
; On Some Basic Ideas
; On Tau Recognizers -- Part 1
; On the Tau Database and General Design
; On Tau Recognizers -- Part 2
; On Tau Intervals and < versus <=
; On the Tau Data Structure
; On the Built-in Tau and the Abuse of Tau Representation
; On the Additional Restrictions on Tau Fields
; On the Use of ENS by Function Evaluation in the Tau System
; On the Most Basic Implications of Being in an Interval
; On Firing Signature Rules
; On Comparing Bounds
; On the Proof of Correctness of upper-bound-<
; On the Near-Subset Relation for Intervals
; On the Tau Database
; On Closing the Database under Conjunctive Rules
; On Converting Theorems in the World to Tau Rules
; On Tau-Like Terms
; On Loops in Relieving Dependent Hyps in Tau Signature Rules
; On the Tau Msgp Protocol
; On Removal of Ancestor Literals -- The Satriani Hack Prequel
; On the Motivation for Tau-Subrs
; On the Tau Completion Alist (calist)
; On Disjoining Tau
; On the Role of Rewriting in Tau
; On Tau-Clause -- Using Tau to Prove or Mangle Clauses
; On Tau Debugging Features
; On Tau-Like Terms
; The Tau system is a collection of data structures and algorithms for
; reasoning quickly about the things we know to be true about a term. It was
; motivated by our frustration over the time it took ACL2 to do elementary
; guard-like proofs -- ``proofs'' that could be almost instantaneous in a
; strongly typed language. A tau is a representation of a set of ``tau
; recognizers'' denoting the function obtained by conjoining the recognizers.
; To say that e has a given tau is to say that the function denoted by the tau
; is true of e. Informally, ``the'' tau of a term is all the tau-like things
; we know to be true about the term. The tau recognizers include all the named
; Boolean functions of one argument, their negations, and all the functions
; (lambda (x) (EQUAL x '<evg>)) and (lambda (x) (< x '<evg>)), and their
; negations.
; On the Name ``tau''
; ``Tau'' might stand for ``Types Are Unnecessary'' and if it did the name
; would be ironic because this whole idea is a tribute to type checking! The
; truth is that ``tau'' doesn't stand for anything! When we designed this
; system we needed a name for the meta objects denoting the set of monadic
; predicates (``signed tau recognizers'') that we know to hold about a term in
; a given context.
; We were tempted to call such a set a ``type'' of the term but felt that was
; inappropriate because the literature on types is so extensive and we have no
; interest in defending the proposition that our objects are ``types''. We
; really don't think of them as anything more than sets of recognizers known
; known to be true. We could not use the words ``sorts'' or ``kinds'' for
; similar reasons. So we temporarily adopted the name ``recognizer sets''
; abbreviated ``rs.'' But this was an unfortunate acronym for two reasons:
; typically pronounced ``are ess'' it was unclear whether to write ``given an
; rs'' or ``given a rs'' since the former ``sounds right'' when ``rs'' is
; pronounced ``are ess'' but wrong when ``rs'' is read ``recognizer set.''
; Furthermore, is ``rs'' singular or plural? Did we really want to write
; ``Given a set of rses?'' Nevertheless, we got this idea working, in a
; stand-alone way, under the name rs. Only when it was integrated into ACL2
; proper did adopt the name ``tau'' for these objects. We chose ``tau''
; because it had no fixed connotation in the literature, it is short, and it
; started with a pronounced consonant. We use ``tau'' as both a singular noun
; and a plural one. We might say ``t1 is a tau'' and we might say that the
; ``tau of x and y are t1 and t2 respectively''.
; On Some Basic Ideas
; We identify certain expressions as primitive ``tau recognizers'' and then
; develop a data structure, tau, to represent conjunctions of these tau
; recognizers. Speaking precisely in the language of metamathematics, tau
; recognizers and tau are predicates in the semantic sense. In particular in
; ACL2's terms, they represent not function SYMBOLS or TERMS but FUNCTIONS.
; They can be applied to any single object and yield T or NIL to indicate
; whether the object has the property or not. For example, we might wish to
; express the property of being a natural number between 1 and 7, or of being
; an alist mapping 32-bit integers to 32-bit integers. The whole idea of the
; tau system is that by representing primitive tau recognizers as objects and
; allowing the representation of the conjunction and negation of these objects
; we can precompute the implications of some thing having a given property
; independently of whatever thing we might be talking about.
; This leads to another basic idea in the tau system: these precomputed
; relationships between tau properties are stored in a database, so that upon
; learning that an object has one of the properties we can rapidly determine
; all of the tau recognizers it satisfies.
; A third basic idea is that the tau database will not be deduced
; automatically but will be derived from rules proved by the user. The tau
; system mines rules as they are proved and builds its database. Several
; forms of theorems are of interest.
; Boolean:
; (booleanp (f v))
; Eval:
; (p 'const)
; Simple:
; (implies (p v) (q v))
; Conjunctive:
; (implies (and (p1 v) (p2 v) ...) (q v))
; Signature [form 1]:
; (implies (and (p1 x1) (p2 x2) ...)
; (q (f x1 x2 ...)))
; Signature [form 2]:
; (implies (and (p1 x1) (p2 x2) ...)