-
Notifications
You must be signed in to change notification settings - Fork 104
/
Copy pathother-processes.lisp
2428 lines (2073 loc) · 106 KB
/
other-processes.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) 2025, 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: Kaufmann@cs.utexas.edu and Moore@cs.utexas.edu
; Department of Computer Science
; University of Texas at Austin
; Austin, TX 78712 U.S.A.
(in-package "ACL2")
; Our top-level function for generating variables attempts to feed
; genvar roots that generate names suggestive of the term being
; replaced by the variable. We now develop the code for generating
; these roots. It involves a recursive descent through a term. At
; the bottom, we see variable symbols, e.g., ABC123, and we wish to
; generate the root '("ABC" . 124).
(defun strip-final-digits1 (lst)
; See strip-final-digits.
(cond ((null lst) (mv "" 0))
((member (car lst) '(#\0 #\1 #\2 #\3 #\4 #\5 #\6 #\7 #\8 #\9))
(mv-let (str n)
(strip-final-digits1 (cdr lst))
(mv str (+ (let ((c (car lst)))
(case c
(#\0 0)
(#\1 1)
(#\2 2)
(#\3 3)
(#\4 4)
(#\5 5)
(#\6 6)
(#\7 7)
(#\8 8)
(otherwise 9)))
(* 10 n)))))
(t (mv (coerce (reverse lst) 'string) 0))))
(defun strip-final-digits (str)
; Given a string, such as "ABC123", we strip off the final digits in it,
; and compute the number they represent. We return two things,
; the string and the number, e.g., "ABC" and 123.
(strip-final-digits1 (reverse (coerce str 'list))))
; For non-variable, non-quote terms we try first the idea of
; generating a name based on the type of the term. The following
; constant associates with selected type sets the names of some
; variables that we find pleasing and suggestive of the type. When we
; generalize a term we look at its type and if it is a subtype of one
; of those listed we prefer to use the variables given. The first
; variable in each family is additionally used as the root for a
; gensym, should it come to that. This list can be extended
; arbitrarily without affecting soundness, as long as (a) the car of
; each pair below is a type set and (b) the cdr is a true-list of
; symbols. Arbitrary overlaps between the types and between the
; symbols are permitted.
;; Historical Comment from Ruben Gamboa:
;; I changed rational to real and complex-rational to complex in
;; the list below, since the new types are supersets of the old types,
;; so it should be harmless.
(defconst *var-families-by-type*
(list (cons *ts-integer* '(I J K L M N))
(cons #+:non-standard-analysis
*ts-real*
#-:non-standard-analysis
*ts-rational*
'(R S I J K L M N))
(cons #+:non-standard-analysis
*ts-complex*
#-:non-standard-analysis
*ts-complex-rational*
'(Z R S I J K L M N))
(cons *ts-cons* '(L LST))
(cons *ts-boolean* '(P Q R))
(cons *ts-symbol* '(A B C D E))
(cons *ts-string* '(S STR))
(cons *ts-character* '(C CH))))
; The following function is used to find the family of vars, given the
; type set of a term:
(defun assoc-ts-subsetp (ts alist)
; Like assoc except we compare with ts-subsetp.
(cond ((null alist) nil)
((ts-subsetp ts (caar alist)) (car alist))
(t (assoc-ts-subsetp ts (cdr alist)))))
; And here is how we look for an acceptable variable.
(defun first-non-member-eq (lst1 lst2)
; Return the first member of lst1 that is not a member-eq of lst2.
(cond ((null lst1) nil)
((member-eq (car lst1) lst2)
(first-non-member-eq (cdr lst1) lst2))
(t (car lst1))))
; If the above techniques don't lead to a choice we generate a string
; from the term by abbreviating the first symbol in the term. Here is
; how we abbreviate:
(defun abbreviate-hyphenated-string1 (str i maximum prev-c)
; We return a list of characters that, when coerced to a string,
; abbreviates string str from position i to (but not including) maximum.
; Currently, it returns the first character after each block of "hyphens"
; and the last character. Thus, "PITON-TEMP-STK" is abbreviated
; "PTSK".
; If prev-char is T it means we output the character we last saw.
; If prev-char is NIL it means the character we last saw was a "hyphen".
; Otherwise, prev-char is the previous character. "Hyphen" here means
; any one of several commonly used "word separators" in symbols.
; This function can be changed arbitrarily as long as it returns a
; list of characters.
(cond
((< i maximum)
(let ((c (char str i)))
(cond
((member c '(#\- #\_ #\. #\/ #\+))
(abbreviate-hyphenated-string1 str (1+ i) maximum nil))
((null prev-c)
(cons c (abbreviate-hyphenated-string1 str (1+ i) maximum t)))
(t (abbreviate-hyphenated-string1 str (1+ i) maximum c)))))
((characterp prev-c) (list prev-c))
(t nil)))
(defun abbreviate-hyphenated-string (str)
; The function scans a string and collects the first and last character
; and every character immediately after a block of "hyphens" as defined
; above.
(let ((lst (abbreviate-hyphenated-string1 str 0 (length str) nil)))
(coerce
(cond ((or (null lst)
(member (car lst) *suspiciously-first-numeric-chars*))
(cons #\V lst))
(t lst))
'string)))
; Just as strip-final-digits produces the genvar root for a variable,
; the following function produces the genvar root for a nonvariable term.
(defun generate-variable-root1 (term avoid-lst type-alist ens wrld)
; Term is a nonvariable, non-quote term. This function returns two
; results, str and n, such that (str . n) is a "root" for genvar.
; In fact, it tries to return a root that when fed to genvar will
; create a variable symbol that is suggestive of term and which does
; not occur in avoid-lst. But the function is correct as long as it
; returns any root, which could be any string.
(mv-let
(ts ttree)
(type-set term t nil type-alist ens wrld nil nil nil)
; Note: We don't really know that the guards have been checked and we
; don't split on the 'assumptions we have forced. But our only use of
; type set here is heuristic. This also explains why we just use the
; global enabled structure and ignore the ttree.
(declare (ignore ttree))<
F438
/div>
(let* ((family (cdr (assoc-ts-subsetp ts *var-families-by-type*)))
(var (first-non-member-eq family avoid-lst)))
(cond (var
; If the type set of term is one of those for which we have a var family
; and some member of that family does not occur in avoid-lst, then we will
; use the symbol-name of var as the root from which to generate a
; variable symbol for term. This will almost certainly result in the
; generation of the symbol var by genvar. The only condition under which
; this won't happen is if var is an illegal variable symbol, in which case
; genvar will suffix it with some sufficiently large natural.
(mv (symbol-name var) nil))
(family
; If we have a family for this type of term but all the members are
; to be avoided, we'll genvar from the first member of the family and
; we might as well start suffixing immediately (from 0) because we
; know the unsuffixed var is in avoid-lst.
(mv (symbol-name (car family)) 0))
(t
; Otherwise, we will genvar from an abbreviated version of the "first
; symbol" in term.
(mv (abbreviate-hyphenated-string
(symbol-name
(cond ((variablep term) 'z) ; never happens
((fquotep term) 'z) ; never happens
((flambda-applicationp term) 'z)
(t (ffn-symb term)))))
nil))))))
; And here we put them together with one last convention. The
; root for (CAR ...) is just the root for ..., except we force
; there to be a suffix. Thus, the root for (CAR X4) is going to be
; ("X" . 5).
(defun generate-variable-root (term avoid-lst type-alist ens wrld)
(cond
((variablep term)
(mv-let (str n)
(strip-final-digits (symbol-name term))
(mv str (1+ n))))
((fquotep term) (mv "CONST" 0))
((eq (ffn-symb term) 'car)
(mv-let (str n)
(generate-variable-root (fargn term 1) avoid-lst type-alist ens
wrld)
(mv str (or n 0))))
((eq (ffn-symb term) 'cdr)
(mv-let (str n)
(generate-variable-root (fargn term 1) avoid-lst type-alist ens
wrld)
(mv str (or n 0))))
(t (generate-variable-root1 term avoid-lst type-alist ens wrld))))
(defun generate-variable (term avoid-lst type-alist ens wrld)
; We generate a legal variable symbol that does not occur in avoid-lst. We use
; term, type-alist, ens, and wrld in a heuristic way to suggest a preferred
; name for the symbol. Generally speaking, the symbol we generate will be used
; to replace term in some conjecture, so we try to generate a symbol that we
; think "suggests" term.
(mv-let (str n)
(generate-variable-root term avoid-lst type-alist ens wrld)
(genvar (find-pkg-witness term) str n avoid-lst)))
(defun generate-variable-lst (term-lst avoid-lst type-alist ens wrld)
; And here we generate a list of variable names sequentially, one for
; each term in term-lst.
; See also generate-variable-lst-simple, which only requires the first two of
; the formals above.
(cond ((null term-lst) nil)
(t
(let ((var (generate-variable (car term-lst) avoid-lst
type-alist ens wrld)))
(cons var (generate-variable-lst (cdr term-lst)
(cons var avoid-lst)
type-alist ens wrld))))))
; That completes the code for generating new variable names.
; An elim-rule, as declared below, denotes a theorem of the form
; (implies hyps (equal lhs rhs)), where rhs is a variable symbol and
; lhs involves the terms destructor-terms, each of which is of the
; form (dfn v1 ... vn), where the vi are distinct variables and {v1
; ... vn} are all the variables in the formula. We call rhs the
; "crucial variable". It is the one we will "puff up" to eliminate
; the destructor terms. For example, in (CONSP X) -> (CONS (CAR X)
; (CDR X)) = X, X is the crucial variable and puffing it up to (CONS A
; B) we can eliminate (CAR X) and (CDR X). We store an elim-rule
; under the function symbol, dfn, of each destructor term. The rule
; we store for (dfn v1 ... vn) has that term as the car of destructor-
; terms and has crucial-position j where (nth j '(v1 ... vn)) = rhs.
; (Thus, the crucial-position is the position in the args at which the
; crucial variable occurs and for these purposes we enumerate the args
; from 0 (as by nth) rather than from 1 (as by fargn).)
; The following is now defined in rewrite.lisp.
; (defrec elim-rule
; (((nume . crucial-position) . (destructor-term . destructor-terms))
; (hyps . equiv)
; (lhs . rhs)
; . rune) nil)
(defun occurs-nowhere-else (var args c i)
; Index the elements of args starting at i. Scan all args except the
; one with index c and return nil if var occurs in one of them and t
; otherwise.
(cond ((null args) t)
((int= c i)
(occurs-nowhere-else var (cdr args) c (1+ i)))
((dumb-occur var (car args)) nil)
(t (occurs-nowhere-else var (cdr args) c (1+ i)))))
(defun first-nomination (term votes nominations)
; See nominate-destructor-candidate for an explanation.
(cons (cons term (cons term votes))
nominations))
(defun second-nomination (term votes nominations)
; See nominate-destructor-candidate for an explanation.
(cond ((null nominations) nil)
((equal term (car (car nominations)))
(cons (cons term
(union-equal votes (cdr (car nominations))))
(cdr nominations)))
(t (cons (car nominations)
(second-nomination term votes (cdr nominations))))))
(defun some-hyp-probably-nilp (hyps type-alist ens wrld)
; The name of this function is meant to limit its use to heuristics.
; In fact, if this function says some hyp is probably nil then in fact
; some hyp is known to be nil under the given type-alist, wrld and
; some forced 'assumptions.
; Since the function actually ignores 'assumptions generated, its use
; must be limited to heuristic situations. When it says "yes, some
; hyp is probably nil" we choose not to pursue the establishment of
; those hyps.
(cond
((null hyps) nil)
(t (mv-let
(knownp nilp ttree)
(known-whether-nil
(car hyps) type-alist ens (ok-to-force-ens ens)
nil ; dwp
wrld nil)
(declare (ignore ttree))
(cond ((and knownp nilp) t)
(t (some-hyp-probably-nilp (cdr hyps) type-alist ens wrld)))))))
(mutual-recursion
(defun sublis-expr (alist term)
; Alist is of the form ((a1 . b1) ... (ak . bk)) where the ai and bi are
; all terms. We substitute bi for each occurrence of ai in term.
; Thus, if the ai are distinct variables, this function is equivalent to
; sublis-var. We do not look for ai's properly inside of quoted objects.
; Thus,
; (sublis-expr '(('3 . x)) '(f '3)) = '(f x)
; but
; (sublis-expr '(('3 . x)) '(f '(3 . 4))) = '(f '(3 . 4)).
(let ((temp (assoc-equal term alist)))
(cond (temp (cdr temp))
((variablep term) term)
((fquotep term) term)
(t (cons-term (ffn-symb term)
(sublis-expr-lst alist (fargs term)))))))
(defun sublis-expr-lst (alist lst)
(cond ((null lst) nil)
(t (cons (sublis-expr alist (car lst))
(sublis-expr-lst alist (cdr lst))))))
)
(defun most-recent-enabled-elim-rule1 (lst ens)
; This function finds the first elim-rule in lst whose whose :nume is
; enabled-numep.
(cond ((endp lst) nil)
((enabled-numep (access elim-rule (car lst) :nume) ens)
(car lst))
(t (most-recent-enabled-elim-rule1 (cdr lst) ens))))
(defun most-recent-enabled-elim-rule (fn wrld ens)
; This function finds the first elim-rule for fn whose whose :nume is
; enabled-numep.
(let ((lst (getpropc fn 'eliminate-destructors-rules nil wrld)))
(and lst ; optimization
(most-recent-enabled-elim-rule1 lst ens))))
(defun nominate-destructor-candidate
(term eliminables type-alist clause ens wrld votes nominations)
; This function recognizes candidates for destructor elimination. It
; is assumed that term is a non-variable, non-quotep term. To be a
; candidate the term must not be a lambda application and the function
; symbol of the term must have an enabled destructor elimination rule.
; Furthermore, the crucial argument position of the term must be
; occupied by a variable symbol that is a member of the eliminables,
; that occurs only in equiv-hittable positions within the clause,
; and that occurs nowhere else in the arguments of the term, or else
; the crucial argument position must be occupied by a term that itself
; is recursively a candidate. (Note that if the crucial argument is
; an eliminable term then when we eliminate it we will introduce a
; suitable distinct var into the crucial argument of this term and
; hence it will be eliminable.) Finally, the instantiated hypotheses
; of the destructor elimination rule must not be known nil under the
; type-alist.
; Votes and nominations are accumulators. Votes is a list of terms
; that contain term and will be candidates if term is eliminated.
; Nominations are explained below.
; If term is a candidate we either "nominate" it, by adding a
; "nomination" for term to the running accumulator nominations, or
; else we "second" a prior nomination for it. A nomination of a term
; is a list of the form (dterm . votes) where dterm is the innermost
; eliminable candidate in term and votes is a list of all the terms
; that will be eliminable if dterm is eliminated. To "second" a
; nomination is simply to add yourself as a vote.
; For example, if X is eliminable then (CAR (CAR (CAR X))) is a
; candidate. If nominations is initially nil then at the conclusion
; of this function it will be
; (((CAR X) (CAR X) (CAR (CAR X)) (CAR (CAR (CAR X))))).
; We always return a nominations list.
(cond
((flambda-applicationp term) nominations)
(t (let ((rule (most-recent-enabled-elim-rule (ffn-symb term) wrld ens)))
(cond
((null rule)
nominations)
(t (let ((crucial-arg (nth (access elim-rule rule :crucial-position)
(fargs term))))
(cond
((variablep crucial-arg)
; Next we wish to determine that every occurrence of the crucial
; argument -- outside of the destructor nests themselves -- is equiv
; hittable. For example, for car-cdr-elim, where we have A as the
; crucial arg (meaning term, above, is (CAR A) or (CDR A)), we wish to
; determine that every A in the clause is equal-hittable, except those
; A's occurring inside the (CAR A) and (CDR A) destructors. Suppose
; the clause is p(A,(CAR A),(CDR A)). The logical explanation of what
; elim does is to replace the A's not in the destructor nests by (CONS
; (CAR A) (CDR A)) and then generalize (CAR A) to HD and (CDR A) to
; TL. This will produce p((CONS HD TL), HD, TL). Observe that we do
; not actually hit the A's inside the CAR and CDR. So we do not
; require that they be equiv-hittable. (This situation actually
; arises in the elim rule for sets, where equiv tests equality on the
; canonicalizations. In this setting, equiv is not a congruence for
; the destructors.) So the question then is how do we detect that all
; the ``naked'' A's are equiv-hittable? We ``ought'' to generalize
; away the instantiated destructor terms and then ask whether all the
; A's are equiv-hittable. But we do not want to pay the price of
; generating n distinct new variable symbols. So we just replace
; every destructor term by NIL. This creates a ``pseudo-clause;'' the
; ``terms'' in it are not really legal -- NIL is not a variable
; symbol. We only use this pseudo-clause to answer the question of
; whether the crucial variable, which certainly isn't NIL, is
; equiv-hittable in every occurrence.
(let* ((alist (pairlis$
(fargs
(access elim-rule rule :destructor-term))
(fargs term)))
(inst-destructors
(sublis-var-lst
alist
(cons (access elim-rule rule :destructor-term)
(access elim-rule rule :destructor-terms))))
(pseudo-clause (sublis-expr-lst
(pairlis$ inst-destructors nil)
clause)))
(cond
((not (every-occurrence-equiv-hittablep-in-clausep
(access elim-rule rule :equiv)
crucial-arg
pseudo-clause ens wrld))
nominations)
((assoc-equal term nominations)
(second-nomination term votes nominations))
((member crucial-arg eliminables)
(cond
((occurs-nowhere-else crucial-arg
(fargs term)
(access elim-rule rule
:crucial-position)
0)
(let* ((inst-hyps
(sublis-var-lst alist
(access elim-rule rule :hyps))))
(cond
((some-hyp-probably-nilp inst-hyps
type-alist ens wrld)
nominations)
(t (first-nomination term votes nominations)))))
(t nominations)))
(t nominations))))
(t (nominate-destructor-candidate crucial-arg
eliminables
type-alist
clause
ens
wrld
(cons term votes)
nominations))))))))))
(mutual-recursion
(defun nominate-destructor-candidates
(term eliminables type-alist clause ens wrld nominations)
; We explore term and accumulate onto nominations all the nominations.
(cond ((variablep term) nominations)
((fquotep term) nominations)
(t (nominate-destructor-candidates-lst
(fargs term)
eliminables
type-alist
clause
ens
wrld
(nominate-destructor-candidate term
eliminables
type-alist
clause
ens
wrld
nil
nominations)))))
(defun nominate-destructor-candidates-lst
(terms eliminables type-alist clause ens wrld nominations)
(cond ((null terms) nominations)
(t (nominate-destructor-candidates-lst
(cdr terms)
eliminables
type-alist
clause
ens
wrld
(nominate-destructor-candidates (car terms)
eliminables
type-alist
clause
ens
wrld
nominations)))))
)
; We next turn to the problem of choosing which candidate we will eliminate.
; We want to eliminate the most complicated one. We measure them with
; max-level-no, which is also used by the defuns principle to store the
; level-no of each fn. Max-level-no was originally defined here, but it is
; mutually recursive with get-level-no, a function we call earlier in the ACL2
; sources, in sort-approved1-rating1.
(defun sum-level-nos (lst wrld)
; Lst is a list of non-variable, non-quotep terms. We sum the
; level-no of the function symbols of the terms. For the level no of
; a lambda expression we use the max level no of its body, just as
; would be done if a non-recursive function with the same body were
; being applied.
(cond ((null lst) 0)
(t (+ (if (flambda-applicationp (car lst))
(max-level-no (lambda-body (ffn-symb (car lst))) wrld)
(or (getpropc (ffn-symb (car lst)) 'level-no
nil wrld)
0))
(sum-level-nos (cdr lst) wrld)))))
(defun pick-highest-sum-level-nos (nominations wrld dterm max-score)
; Nominations is a list of pairs of the form (dterm . votes), where
; votes is a list of terms. The "score" of a dterm is the
; sum-level-nos of its votes. We scan nominations and return a dterm
; with maximal score, assuming that dterm and max-score are the
; winning dterm and its score seen so far.
(cond
((null nominations) dterm)
(t (let ((score (sum-level-nos (cdr (car nominations)) wrld)))
(cond
((> score max-score)
(pick-highest-sum-level-nos (cdr nominations) wrld
(caar nominations) score))
(t
(pick-highest-sum-level-nos (cdr nominations) wrld
dterm max-score)))))))
(defun select-instantiated-elim-rule (clause type-alist eliminables ens wrld)
; Clause is a clause to which we wish to apply destructor elimination.
; Type-alist is the type-alist obtained by assuming all literals of cl nil.
; Eliminables is the list of legal "crucial variables" which can be
; "puffed up" to do an elim. For example, to eliminate (CAR X), X
; must be puffed up to (CONS A B). X is the crucial variable in (CAR
; X). Upon entry to the destructor elimination process we consider
; all the variables eliminable (except the ones historically
; introduced by elim). But once we get going within the elim process,
; the only eliminable variables are the ones we introduce ourselves
; (because they won't be eliminable by subsequent processes since they
; were introduced by elim).
; If there is at least one nomination for an elim, we choose the one
; with maximal score and return an instantiated version of the
; elim-rule corresponding to it. Otherwise we return nil.
(let ((nominations
(nominate-destructor-candidates-lst clause
eliminables
type-alist
clause
ens
wrld
nil)))
(cond
((null nominations) nil)
(t
(let* ((dterm (pick-highest-sum-level-nos nominations wrld nil -1))
(rule (most-recent-enabled-elim-rule (ffn-symb dterm) wrld ens))
(alist (pairlis$ (fargs (access elim-rule rule :destructor-term))
(fargs dterm))))
(change elim-rule rule
:hyps (sublis-var-lst alist (access elim-rule rule :hyps))
:lhs (sublis-var alist (access elim-rule rule :lhs))
:rhs (sublis-var alist (access elim-rule rule :rhs))
:destructor-term
(sublis-var alist (access elim-rule rule :destructor-term))
:destructor-terms
(sublis-var-lst
alist
(access elim-rule rule :destructor-terms))))))))
; We now take a break from elim and develop the code for the generalization
; that elim uses. We want to be able to replace terms by variables
; (sublis-expr, above), we want to be able to restrict the new variables by
; noting type-sets of the terms replaced, and we want to be able to use
; generalization rules provided in the database.
(defun type-restriction-segment (cl terms vars type-alist ens wrld)
; Warning: This function calls clausify using the sr-limit from the world, not
; from the rewrite-constant. Do not call this function from the simplifier
; without thinking about passing in the sr-limit.
; Cl is a clause. Terms is a list of terms and is in 1:1
; correspondence with vars, which is a list of vars. Type-alist is
; the result of assuming false every literal of cl. This function
; returns three results. The first is a list of literals that can be
; disjoined to cl without altering the validity of cl. The second is
; a subset of vars. The third is an extension of ttree. Technically
; speaking, this function may return any list of terms with the
; property that every term in it is false (under the assumptions in
; type-alist) and any subset of vars, provided the ttree returned is
; an extension of ttree and justifies the falsity of the terms
; returned. The final ttree must be 'assumption-free and is if the
; initial ttree is also.
; As for motivation, we are about to generalize cl by replacing each
; term in terms by the corresponding var in vars. It is sound, of
; course, to restrict the new variable to have whatever properties the
; corresponding term has. This function is responsible for selecting
; the restrictions we want to place on each variable, based on
; type-set reasoning alone. Thus, if t is known to have properties h1
; & ... & hk, then we can include (not h1), ..., (not hk) in our first
; answer to restrict the variable introduced for t. We will include
; the corresponding var in our second answer to indicate that we have
; a type restriction on that variable.
; We do not want our type restrictions to cause the new clause to
; explode into cases. Therefore, we adopt the following heuristic.
; We convert the type set of each term t into a term (hyp t) known to
; be true of t. We negate (hyp t) and clausify the result. If that
; produces a single clause (segment) then that segment is added to our
; answer. Otherwise, we add no restriction. There are probably
; better ways to do this than to call the full-blown
; convert-type-set-to-term and clausify. But this is simple, elegant,
; and lets us take advantage of improvements to those two utilities.
(cond
((null terms) (mv nil nil nil))
(t
(mv-let
(ts ttree1)
(type-set (car terms) nil nil type-alist ens wrld nil nil nil)
(mv-let
(term ttree1)
(convert-type-set-to-term (car terms) ts ens wrld ttree1)
(let ((clauses (clausify (dumb-negate-lit term) nil t
; Notice that we obtain the sr-limit from the world; see Warning above.
(sr-limit wrld))))
(mv-let
(lits restricted-vars ttree)
(type-restriction-segment cl
(cdr terms)
(cdr vars)
type-alist ens wrld)
(cond ((null clauses)
; If the negation of the type restriction term clausifies to the empty set
; of clauses, then the term is nil. Since we get to assume it, we're done.
; But this can only happen if the type-set of the term is empty. We don't think
; this will happen, but we test for it nonetheless, and toss a nil hypothesis
; into our answer literals if it happens.
(mv (add-to-set-equal *nil* lits)
(cons (car vars) restricted-vars)
(cons-tag-trees ttree1 ttree)))
((and (null (cdr clauses))
(not (null (car clauses))))
; If there is only one clause and it is not the empty clause, we'll
; assume everything in it. (If the clausify above produced '(NIL)
; then the type restriction was just *t* and we ignore it.) It is
; possible that the literals we are about to assume are already in cl.
; If so, we are not fooled into thinking we've restricted the new var.
(cond
((subsetp-equal (car clauses) cl)
(mv lits restricted-vars ttree))
(t (mv (disjoin-clauses (car clauses) lits)
(cons (car vars) restricted-vars)
(cons-tag-trees ttree1 ttree)))))
(t
; There may be useful type information we could extract, but we don't.
; It is always sound to exit here, giving ourselves no additional
; assumptions.
(mv lits restricted-vars ttree))))))))))
(mutual-recursion
(defun subterm-one-way-unify (pat term)
; This function searches pat for a non-variable non-quote subterm s such that
; (one-way-unify s term) returns t and a unify-subst. If it finds one, it
; returns t and the unify-subst. Otherwise, it returns two nils.
(cond ((variablep pat) (mv nil nil))
((fquotep pat) (mv nil nil))
(t (mv-let (ans alist)
(one-way-unify pat term)
(cond (ans (mv ans alist))
(t (subterm-one-way-unify-lst (fargs pat) term)))))))
(defun subterm-one-way-unify-lst (pat-lst term)
(cond
((null pat-lst) (mv nil nil))
(t (mv-let (ans alist)
(subterm-one-way-unify (car pat-lst) term)
(cond (ans (mv ans alist))
(t (subterm-one-way-unify-lst (cdr pat-lst) term)))))))
)
; The following is now defined in rewrite.lisp.
; (defrec generalize-rule (nume formula . rune) nil)
(defun apply-generalize-rule (gen-rule term ens)
; Gen-rule is a generalization rule, and hence has a name and a
; formula component. Term is a term which we are intending to
; generalize by replacing it with a new variable. We return two
; results. The first is either t or nil indicating whether gen-rule
; provides a useful restriction on the generalization of term. If the
; first result is nil, so is the second. Otherwise, the second result
; is an instantiation of the formula of gen-rule in which term appears.
; Our heuristic for deciding whether to use gen-rule is: (a) the rule
; must be enabled, (b) term must unify with a non-variable subterm of
; the formula of the rule, (c) the unifying substitution must leave no
; free vars in that formula, and (d) the function symbol of term must
; not occur in the instantiation of the formula except in the
; occurrences of term itself.
(cond
((not (enabled-numep (access generalize-rule gen-rule :nume) ens))
(mv nil nil))
(t (mv-let
(ans unify-subst)
(subterm-one-way-unify (access generalize-rule gen-rule :formula)
term)
(cond
((null ans)
(mv nil nil))
((free-varsp (access generalize-rule gen-rule :formula)
unify-subst)
(mv nil nil))
(t (let ((inst-formula (sublis-var unify-subst
(access generalize-rule
gen-rule
:formula))))
(cond ((ffnnamep (ffn-symb term)
(subst-expr 'x term inst-formula))
(mv nil nil))
(t (mv t inst-formula))))))))))
(defun generalize-rule-segment1 (generalize-rules term ens)
; Given a list of :GENERALIZE rules and a term we return two results:
; the list of instantiated negated formulas of those applicable rules
; and the runes of all applicable rules. The former list is suitable
; for splicing into a clause to add the formulas as hypotheses.
(cond
((null generalize-rules) (mv nil nil))
(t (mv-let (ans formula)
(apply-generalize-rule (car generalize-rules) term ens)
(mv-let (formulas runes)
(generalize-rule-segment1 (cdr generalize-rules)
term ens)
(cond (ans (mv (add-literal (dumb-negate-lit formula)
formulas nil)
(cons (access generalize-rule
(car generalize-rules)
:rune)
runes)))
(t (mv formulas runes))))))))
(defun generalize-rule-segment (terms vars ens wrld)
; Given a list of terms and a list of vars in 1:1 correspondence, we
; return two results. The first is a clause segment containing the
; instantiated negated formulas derived from every applicable
; :GENERALIZE rule for each term in terms. This segment can be spliced
; into a clause to restrict the range of a generalization of terms.
; The second answer is an alist pairing some of the vars in vars to
; the runes of all :GENERALIZE rules in wrld that are applicable to the
; corresponding term in terms. The second answer is of interest only
; to output routines.
(cond
((null terms) (mv nil nil))
(t (mv-let (segment1 runes1)
(generalize-rule-segment1 (global-val 'generalize-rules wrld)
(car terms) ens)
(mv-let (segment2 alist)
(generalize-rule-segment (cdr terms) (cdr vars) ens wrld)
(cond
((null runes1) (mv segment2 alist))
(t (mv (disjoin-clauses segment1 segment2)
(cons (cons (car vars) runes1) alist)))))))))
(defun generalize1 (cl type-alist terms vars ens wrld)
; Cl is a clause. Type-alist is a type-alist obtained by assuming all
; literals of cl false. Terms and vars are lists of terms and
; variables, respectively, in 1:1 correspondence. We assume no var in
; vars occurs in cl. We generalize cl by substituting vars for the
; corresponding terms. We restrict the variables by using type-set
; information about the terms and by using :GENERALIZE rules in wrld.
; We return four results. The first is the new clause. The second
; is a list of the variables for which we added type restrictions.
; The third is an alist pairing some variables with the runes of
; generalization rules used to restrict them. The fourth is a ttree
; justifying our work; it is 'assumption-free.
(mv-let (tr-seg restricted-vars ttree)
(type-restriction-segment cl terms vars type-alist ens wrld)
(mv-let (gr-seg alist)
(generalize-rule-segment terms vars ens wrld)
(mv (sublis-expr-lst (pairlis$ terms vars)
(disjoin-clauses tr-seg
(disjoin-clauses gr-seg
cl)))
restricted-vars
alist
ttree))))
; This completes our brief flirtation with generalization. We now
; have enough machinery to finish coding destructor elimination.
; However, it might be noted that generalize1 is the main subroutine
; of the generalize-clause waterfall processor.
(defun apply-instantiated-elim-rule (rule cl type-alist avoid-vars ens wrld)
; This function takes an instantiated elim-rule, rule, and applies it to a
; clause cl. Avoid-vars is a list of variable names to avoid when we generate
; new ones. See eliminate-destructors-clause for an explanation of that.
; An instantiated :ELIM rule has hyps, lhs, rhs, and destructor-terms, all
; instantiated so that the car of the destructor terms occurs somewhere in the
; clause. To apply such an instantiated :ELIM rule to a clause we assume the
; hyps (adding their negations to cl), we generalize away the destructor terms
; occurring in the clause and in the lhs of the rule, and then we substitute
; that generalized lhs for the rhs into the generalized cl to obtain the final
; clause. The generalization step above may involve adding additional
; hypotheses to the clause and using generalization rules in wrld.
; We return three things. The first is the clause described above, which
; implies cl when the hyps of the rule are known to be true, the second is the
; set of elim variables we have just introduced into it, and the third is a
; list describing this application of the rune of the rule, as explained below.
; The list returned as the third value will become an element in the
; 'elim-sequence list in the ttree of the history entry for this elimination
; process. The "elim-sequence element" we return has the form:
; (rune rhs lhs alist restricted-vars var-to-runes-alist ttree)
; and means "use rune to replace rhs by lhs, generalizing as specified by alist
; (which maps destructors to variables), restricting the restricted-vars
; variables by type (as justified by ttree) and restricting the
; var-to-runes-alist variables by the named generalize rules." The ttree is
; 'assumption-free.
(let* ((rune (access elim-rule rule :rune))
(hyps (access elim-rule rule :hyps))
(lhs (access elim-rule rule :lhs))
(rhs (access elim-rule rule :rhs))
(dests (access elim-rule rule :destructor-terms))
(negated-hyps (dumb-negate-lit-lst hyps)))
(mv-let
(contradictionp type-alist0 ttree0)
(type-alist-clause negated-hyps nil nil type-alist ens wrld
nil nil)
; Before Version_2.9.3, we just punted when contradictionp is true here, and
; this led to infinite loops reported by Sol Swords and then (shortly
; thereafter) Doug Harper, who both sent examples. Our initial fix was to punt
; without going into the infinite loop, but then we implemented the current
; scheme in which we simply perform the elimination without generating clauses
; for the impossible "pathological" cases corresponding to falsity of each of
; the instantiated :elim rule's hypotheses. Both fixes avoid the infinite loop
; in both examples. We kept the present fix because at the time it actually
; proved the latter example (shown here) without induction:
; (include-book "ihs/@logops" :dir :system)
; (thm (implies (integerp (* 1/2 n)) (equal (mod n 2) 0)))
; However, the fix was buggy. When we fixed those bugs after Version_3.6.1,
; the thm above no longer proved; but we still avoided the infinite loop. That
; loop is easily seen in the following example sent by Eric Smith, which proved
; from Versions 2.9.3 through 3.6.1 by exploiting that bug and looped in
; Versions before 2.9.3:
; (defthmd true-listp-of-cdr
; (implies (true-listp (cdr x))
; (true-listp x))
; :hints (("Goal" :in-theory (disable true-listp))))
(let* ((type-alist (if contradictionp type-alist type-alist0))
(cl-with-hyps (disjoin-clauses negated-hyps cl))
(elim-vars (generate-variable-lst dests
(all-vars1-lst cl-with-hyps
avoid-vars)
type-alist ens wrld))
(alist (pairlis$ dests elim-vars))
(generalized-lhs (sublis-expr alist lhs)))
(cond
(contradictionp
; The negation of the clause implies that the type-alist holds, and thus one of
; the negated-hyps holds. Then since contradictionp is true, the conjunction
; of the hyps implies the clause. That is, *true-clause* implies cl when the
; hyps of the rule are known to be true.
(mv *true-clause*
nil ; actual-elim-vars
(list rune rhs
generalized-lhs
alist
nil ; restricted-vars
nil ; var-to-runes-alist
ttree0)))
(t
(let* ((cl-with-hyps (disjoin-clauses negated-hyps cl))
(elim-vars (generate-variable-lst dests
(all-vars1-lst cl-with-hyps
avoid-vars)
type-alist ens wrld)))
(mv-let (generalized-cl-with-hyps
restricted-vars
var-to-runes-alist
ttree)