forked from acl2/acl2
-
Notifications
You must be signed in to change notification settings - Fork 0
/
tau.lisp
13148 lines (11276 loc) · 576 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.1 -- A Computational Logic for Applicative Common Lisp
; Copyright (C) 2018, 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 ((null 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 an 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)))))
; Rockwell Addition: A major change is the removal of THEs from
; many terms.
; Essay on the Removal of Guard Holders
; We now develop the code to remove certain trivial calls, such as those
; generated by THE, from a term. Suppose for example that the user types (THE
; type expr); type is translated (using translate-declaration-to-guard) into a
; predicate in one variable. The variable is always VAR. Denote this
; predicate as (guard VAR). Then the entire form (THE type expr) is translated
; into ((LAMBDA (VAR) (THE-CHECK (guard VAR) 'type VAR)) expr). The-check is
; defined to have a guard that logically is its first argument, so when we
; generate guards for the translation above we generate the obligation to prove
; (guard expr). Furthermore, the definition of the-check is such that unless
; the value of state global 'guard-checking-on is :none, executing it in the
; *1* function tests (guard expr) at runtime and signals an error.
; But logically speaking, the definition of (THE-check g x y) is y. Hence,
; (THE type expr)
; = ((LAMBDA (VAR) (THE-check (guard VAR) 'type VAR)) expr)
; = ((LAMBDA (VAR) VAR) expr)
; = expr.
; Observe that this is essentially just the expansion of certain non-rec
; functions (namely, THE-CHECK and the lambda application) and
; IF-normalization.
; We belabor this obvious point because until Version_2.5, we kept the THEs in
; bodies, which injected them into the theorem proving process. We now remove
; them from the stored BODY property. It is not obvious that this is a benign
; change; it might have had unintended side-effects on other processing, e.g.,
; guard generation. But the BODY property has long been normalized with
; certain non-rec fns expanded, and so we argue that the removal of THE could
; have been accomplished by the processing we were already doing.
; But there is another place we wish to remove such ``guard holders.'' We want
; the guard clauses we generate not to have these function calls in them. The
; terms we explore to generate the guards WILL have these calls in them. But
; the output we produce will not, courtesy of the following code which is used
; to strip the guard holders out of a term.
; Starting with Version_2.8 the ``guard holders'' code appears elsewhere,
; because remove-guard-holders needs to be defined before it is called by
; constraint-info.
(mutual-recursion
(defun remove-guard-holders1 (changedp0 term)
; Warning: If you change this function, consider changing :DOC guard-holders.
; We return (mv changedp new-term), where new-term is provably equal to term,
; and where if changedp is nil, then changedp0 is nil and new-term is identical
; to term. The second part can be restated as follows: if changedp0 is true
; then changedp is true (a kind of monotonicity), and if the resulting term is
; distinct from the input term then changedp is true. Intuitively, if changedp
; is true then new-term might be distinct from term but we don't know that
; (especially if changedp0 is true), but if changedp is nil then we know that
; new-term is just term.
; See the Essay on the Removal of Guard Holders.
; WARNING: The resulting term is in quote normal form. We take advantage of
; this fact in our implementation of :by hints, in function
; apply-top-hints-clause1, to increase the chances that the "easy-winp" case
; holds. We also take advantage of this fact in
; interpret-term-as-rewrite-rule, as commented there.
; WARNING. Remove-guard-holders is used in constraint-info,
; induction-machine-for-fn1, and termination-machine, so (remove-guard-holders1
; term) needs to be provably equal to term, for every term, in the ground-zero
; theory. In fact, because of the use in constraint-info, it needs to be the
; case that for any axiomatic event e, (remove-guard-holders e) can be
; substituted for e without changing the logical power of the set of axioms.
; Actually, we want to view the logical axiom added by e as though
; remove-guard-holders had been applied to it, and hence RETURN-LAST,
; MV-LIST, and CONS-WITH-HINT appear in *non-instantiable-primitives*.
(declare (xargs :guard (pseudo-termp term)
:measure (acl2-count term)))
(cond
((variablep term) (mv changedp0 term))
((fquotep term) (mv changedp0 term))
((or (eq (ffn-symb term) 'RETURN-LAST)
(eq (ffn-symb term) 'MV-LIST))
; Recall that PROG2$ (hence, RETURN-LAST) is used to attach the dcl-guardian of
; a LET to the body of the LET for guard generation purposes. A typical call
; of PROG2$ is (PROG2$ dcl-guardian body), where dcl-guardian has a lot of IFs
; in it. Rather than distribute them over PROG2$ and then when we finally get
; to the bottom with things like (prog2$ (illegal ...) body) and (prog2$ T
; body), we just open up the prog2$ early, throwing away the dcl-guardian.
(remove-guard-holders1 t (car (last (fargs term)))))
((eq (ffn-symb term) 'CONS-WITH-HINT)
(mv-let
(changedp1 arg1)
(remove-guard-holders1 nil (fargn term 1))
(declare (ignore changedp1))
(mv-let
(changedp2 arg2)
(remove-guard-holders1 nil (fargn term 2))
(declare (ignore changedp2))
(mv t (mcons-term* 'cons arg1 arg2)))))
((flambdap (ffn-symb term))
(case-match
term
((('LAMBDA ('VAR) ('THE-CHECK & & 'VAR))
val)
(remove-guard-holders1 t val))
((('LAMBDA formals ('RETURN-LAST ''MBE1-RAW & logic))
. args)
; This case handles equality variants. For example, the macroexpansion of
; (member x y) matches this pattern, and we return (member-equal x y). The
; goal here is to deal with the uses of let-mbe in macro definitions of
; equality variants, as for member.
(mv-let
(changedp1 args1)
(remove-guard-holders1-lst args)
(declare (ignore changedp1))
(mv-let
(changedp2 logic2)
(remove-guard-holders1 nil logic)
(declare (ignore changedp2))
(mv t (subcor-var formals args1 logic2)))))
(&
(mv-let
(changedp1 lambda-body)
(remove-guard-holders1 nil (lambda-body (ffn-symb term)))
(mv-let
(changedp2 args)
(remove-guard-holders1-lst (fargs term))
(cond ((or changedp1 changedp2)
(mv t
(mcons-term
(if changedp1
(make-lambda (lambda-formals (ffn-symb term))
lambda-body)
(ffn-symb term))
args)))
(t (mv changedp0 term))))))))
(t (mv-let
(changedp1 args)
(remove-guard-holders1-lst (fargs term))
(cond ((null changedp1)
(cond ((quote-listp args)
(let ((new-term (mcons-term (ffn-symb term)
args)))
(cond ((equal term new-term) ; even if not eq
(mv changedp0 term))
(t (mv t new-term)))))
(t (mv changedp0 term))))
(t (mv t (mcons-term (ffn-symb term) args))))))))
(defun remove-guard-holders1-lst (lst)
(declare (xargs :guard (pseudo-term-listp lst)
:measure (acl2-count lst)))
(cond ((endp lst) (mv nil nil))
(t (mv-let (changedp1 a)
(remove-guard-holders1 nil (car lst))
(mv-let (changedp2 b)
(remove-guard-holders1-lst (cdr lst))
(cond ((or changedp1 changedp2)
(mv t (cons a b)))
(t (mv nil lst))))))))
)
(defun remove-guard-holders (term)
; Return a term equal to term, but slightly simplified. See also the warning
; in remove-guard-holders1.
(declare (xargs :guard (pseudo-termp term)))
(mv-let (changedp result)
(remove-guard-holders1 nil term)
(declare (ignore changedp))
result))
(defun remove-guard-holders-lst (lst)
; Return a list of terms element-wise equal to lst, but slightly simplified.
(mv-let (changedp result)
(remove-guard-holders1-lst lst)
(declare (ignore changedp))
result))
(defun remove-guard-holders1-lst-lst (lst)
(cond ((null lst) (mv nil nil))
(t (mv-let (changedp1 a)
(remove-guard-holders1-lst (car lst))
(mv-let (changedp2 b)
(remove-guard-holders1-lst-lst (cdr lst))
(cond ((or changedp1 changedp2)
(mv t (cons a b)))
(t (mv nil lst))))))))
(defun remove-guard-holders-lst-lst (lst)
; Return a list of clauses element-wise equal to lst, but slightly simplified.
(mv-let (changedp result)
(remove-guard-holders1-lst-lst lst)
(declare (ignore changedp))
result))
; 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 produced 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)))))
(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-in-ttree (ttree ans)
; Ttree is any ttree produced by this system. We sweep it collecting into ans
; every 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
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