forked from acl2/acl2
-
Notifications
You must be signed in to change notification settings - Fork 0
/
defthm.lisp
11878 lines (10641 loc) · 525 KB
/
defthm.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.4 -- A Computational Logic for Applicative Common Lisp
; Copyright (C) 2022, 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")
; This file contains the functions that check the acceptable forms for
; the various classes of rules, the functions that generate the rules
; from the forms, and finally the functions that actually do the adding.
; It also contains various history management and command facilities whose
; implementation is intertwined with the storage of rules, e.g., :pr and
; some monitoring stuff.
; The structure of the file is that we first define the checkers and
; generators for each class of rule. Each such section has a header
; like that shown below. When we finish all the individual classes
; we enter the final sections, headed
; Section: Handling a List of Classes
; Section: More History Management and Command Stuff
; Section: The DEFAXIOM Event
; Section: The DEFTHM Event
; Section: Some Convenient Abbreviations for Defthm
;---------------------------------------------------------------------------
; Section: :REWRITE Rules
; In this section we develop the function chk-acceptable-
; rewrite-rule, which checks that all the :REWRITE rules generated
; from a term are legal. We then develop add-rewrite-rule which does
; the actual generation and addition of the rules to the world.
(defun form-of-rewrite-quoted-constant-rule (equiv lhs rhs)
; The Essay on Rewriting Quoted Constants lists three possible forms, 1, 2, or
; 3, of such rules and this function determines which form we're seeing, or nil
; if lhs and rhs are incompatible with any of the forms. Note that a Form 3
; lhs must be unifiable with a quoted constant but we put no restrictions on
; the rhs. Indeed, rhs could be a free variable whose value is selected by
; relieving some hyp!
(cond ((and (not (eq equiv 'equal))
(quotep lhs)
(quotep rhs))
1)
((and (not (eq equiv 'equal))
(nvariablep lhs)
(not (fquotep lhs))
(symbolp (ffn-symb lhs))
(cdr lhs)
(null (cddr lhs))
(variablep (fargn lhs 1))
(eq (fargn lhs 1) rhs))
2)
((or (variablep lhs)
(fquotep lhs)
(member-eq (ffn-symb lhs) *one-way-unify1-implicit-fns*))
3)
(t nil)))
; We use the following functions to determine the sense of the conclusion
; as a :REWRITE rule.
(defun interpret-term-as-rewrite-rule2 (qc-flg name hyps equiv lhs rhs wrld)
; Qc-flg is t if we are processing for a :rewrite-quoted-constant rule rather
; than a :rewrite rule.
(cond
((equal lhs rhs)
(msg
"A ~x0 rule generated from ~x1 is illegal because it rewrites the ~
term ~x2 to itself! This can happen even when you submit a rule whose ~
left and right sides appear to be different, in the case that those two ~
sides represent the same term (for example, after macroexpansion). For ~
general information about rewrite rules in ACL2, see :DOC rewrite. You ~
may wish to consider submitting a DEFTHM event ending with ~
:RULE-CLASSES NIL."
(if qc-flg :rewrite-quoted-constant :rewrite)
name
lhs))
((and qc-flg
(not (form-of-rewrite-quoted-constant-rule equiv lhs rhs)))
(msg
"A :REWRITE-QUOTED-CONSTANT rule generated from ~x0 is illegal because ~
the conclusion is not compatible with any of the allowed forms. To be ~
Form [1], the conclusion must be an equivalence (other than EQUAL) ~
between two quoted constants. To be Form [2], the conclusion must be ~
an equivalence (other than EQUAL) between, on the left, a call of a ~
monadic function symbol on a variable symbol and, on the right, that ~
same variable symbol. To be of Form [3], the conclusion must be an ~
equivalence relation and the left-hand side must be a variable, a ~
quoted constant, or a call of one of the function symbols in ~
*ONE-WAY-UNifY1-IMPLICIT-FNS* so that the left-hand side can match a ~
quoted constant. But the conclusion of ~x0 is ~x1."
name
(list equiv lhs rhs)))
((and (not qc-flg)
(or (variablep lhs)
(fquotep lhs)
(flambda-applicationp lhs)))
(msg
"A :REWRITE rule generated from ~x0 is illegal because it rewrites the ~
~@1 ~x2. For general information about rewrite rules in ACL2, see :DOC ~
rewrite."
name
(cond ((variablep lhs) "variable symbol")
((fquotep lhs) "quoted constant")
((flambda-applicationp lhs) "LET-expression")
(t (er hard 'interpret-term-as-rewrite-rule2
"Implementation error: forgot a case. LHS:~|~x0."
lhs)))
lhs))
(t (let ((bad-synp-hyp-msg (bad-synp-hyp-msg
hyps (all-vars lhs) nil wrld)))
(cond
(bad-synp-hyp-msg
(msg
"A ~x0 rule generated from ~x1 is illegal because ~@2"
(if qc-flg :rewrite-quoted-constant :rewrite)
name
bad-synp-hyp-msg))
(t nil))))))
(defun interpret-term-as-rewrite-rule1 (term equiv-okp ens wrld)
; Here we do the work described in interpret-term-as-rewrite-rule. If
; equiv-okp is nil, then no special treatment is given to equivalence relations
; other than equal, iff, and members of *equality-aliases*.
(cond ((variablep term) (mv 'iff term *t* nil))
((fquotep term) (mv 'iff term *t* nil))
((member-eq (ffn-symb term) *equality-aliases*)
(mv 'equal (remove-lambdas (fargn term 1)) (fargn term 2) nil))
((flambdap (ffn-symb term))
(interpret-term-as-rewrite-rule1
(subcor-var (lambda-formals (ffn-symb term))
(fargs term)
(lambda-body (ffn-symb term)))
equiv-okp ens wrld))
((if equiv-okp
(equivalence-relationp (ffn-symb term) wrld)
(member-eq (ffn-symb term) '(equal iff)))
(let ((lhs (remove-lambdas (fargn term 1))))
(mv-let (equiv ttree)
(cond ((eq (ffn-symb term) 'iff)
(mv-let
(ts ttree)
(type-set lhs nil nil nil ens wrld nil
nil nil)
(cond ((ts-subsetp ts *ts-boolean*)
(mv-let
(ts ttree)
(type-set (fargn term 2) nil nil nil ens
wrld ttree nil nil)
(cond ((ts-subsetp ts *ts-boolean*)
(mv 'equal ttree))
(t (mv 'iff nil)))))
(t (mv 'iff nil)))))
(t (mv (ffn-symb term) nil)))
(mv equiv lhs (fargn term 2) ttree))))
((eq (ffn-symb term) 'not)
(mv 'equal (remove-lambdas (fargn term 1)) *nil* nil))
(t (mv-let (ts ttree)
(type-set term nil nil nil ens wrld nil nil nil)
(cond ((ts-subsetp ts *ts-boolean*)
(mv 'equal (remove-lambdas term) *t* ttree))
(t (mv 'iff (remove-lambdas term) *t* nil)))))))
(defun interpret-term-as-rewrite-rule (qc-flg name hyps term ctx ens wrld)
; NOTE: Term is assumed to have had remove-guard-holders applied, which in
; particular implies that term is in quote-normal form.
; Qc-flg indicates that we are processing a :rewrite-quoted-constant rule.
; This function returns five values. The first can be a msg for printing an
; error message. Otherwise the first is nil, in which case the second is an
; equivalence relation, eqv; the next two are terms, lhs and rhs, such that
; (eqv lhs rhs) is propositionally equivalent to term; and the last is an
; 'assumption-free ttree justifying the claim.
; If ctx is non-nil, then print an observation, with that ctx, when we are
; avoiding the use of an equivalence relation. Otherwise do not print that
; observation.
(mv-let
(eqv lhs rhs ttree)
(interpret-term-as-rewrite-rule1 term t ens wrld)
; Note that we are insensitive to the qc-flg in the above call. We deconstruct
; term the same way whether it's to be used as a :rewrite rule or
; :rewrite-quoted-constant rule. But we then check slightly different
; restrictions.
(let ((msg (interpret-term-as-rewrite-rule2
qc-flg name hyps eqv lhs rhs wrld)))
(cond
(msg
; We try again, this time with equiv-okp = nil to avoid errors for a form such
; as the following. Its evaluation caused a hard Lisp error in Version_4.3
; during the second pass of the encapsulate at the final defthm, and is based
; closely on an example sent to us by Jared Davis.
; (encapsulate
; ()
; (defun my-equivp (x y)
; (equal (nfix x) (nfix y)))
; (local
; (defthm my-equivp-reflexive
; (my-equivp x x)))
; (defequiv my-equivp)
; (defthm my-equivp-reflexive
; (my-equivp x x)))
(mv-let
(eqv2 lhs2 rhs2 ttree2)
(interpret-term-as-rewrite-rule1 term nil ens wrld)
(cond
((interpret-term-as-rewrite-rule2 qc-flg name hyps
eqv2 lhs2 rhs2 wrld)
(mv msg eqv lhs rhs ttree))
(t (prog2$
(and ctx
(observation-cw ctx
"The proposed rewrite rule ~x0 may ~
suggest a conclusion of the form (Equiv ~
Lhs Rhs) where:~| Equiv: ~x1~| Lhs: ~
~x2~| Rhs: ~x3~|But such a rewrite ~
rule would be illegal, so the conclusion ~
is treated as follows instead.~| Equiv: ~
~x4~| Lhs: ~x5~| Rhs: ~x6~|"
name
eqv
(untranslate lhs nil wrld)
(untranslate rhs nil wrld)
eqv2
(untranslate lhs2 nil wrld)
(untranslate rhs2 nil wrld)))
(mv nil eqv2 lhs2 rhs2 ttree2))))))
(t (mv nil eqv lhs rhs ttree))))))
; We inspect the lhs and some hypotheses with the following functions to
; determine if non-recursive defuns will present a problem to the user.
(mutual-recursion
(defun non-recursive-fnnames-alist-rec (term ens wrld acc)
; Accumulate, into acc, an alist that associates each enabled non-recursive
; function symbol fn of term either with the base-symbol of its most recent
; definition rune or with nil. Our meaning of "enabled" and "non-recursive" is
; with respect to that rune (which exists except for lambdas). We associate to
; a value of nil for two cases of the key: a lambda, and when that rune is the
; rune of the original definition. We do not dive into lambda bodies.
(declare (xargs :guard (and (pseudo-termp term)
(enabled-structure-p ens)
(plist-worldp wrld)
(alistp acc))))
(cond
((variablep term) acc)
((fquotep term) acc)
((flambda-applicationp term)
(non-recursive-fnnames-alist-rec-lst
(fargs term) ens wrld
(if (assoc-equal (ffn-symb term) acc)
acc
(acons (ffn-symb term) nil acc))))
(t (non-recursive-fnnames-alist-rec-lst
(fargs term) ens wrld
(cond
((assoc-eq (ffn-symb term) acc)
acc)
(t (let ((def-body (def-body (ffn-symb term) wrld)))
(cond
((and def-body
(enabled-numep (access def-body def-body :nume)
ens)
(not (access def-body def-body :recursivep)))
(let ((sym (base-symbol (access def-body def-body :rune))))
(acons (ffn-symb term)
(if (eq sym (ffn-symb term))
nil
sym)
acc)))
(t acc)))))))))
(defun non-recursive-fnnames-alist-rec-lst (lst ens wrld acc)
(declare (xargs :guard (and (pseudo-term-listp lst)
(enabled-structure-p ens)
(plist-worldp wrld)
(alistp acc))))
(cond ((endp lst) acc)
(t (non-recursive-fnnames-alist-rec-lst
(cdr lst) ens wrld
(non-recursive-fnnames-alist-rec (car lst) ens wrld acc)))))
)
(defun non-recursive-fnnames-alist (term ens wrld)
; See non-recursive-fnnames-alist-rec. (The present function reverses the
; result, to respect the original order of appearance of function symbols.)
(reverse (non-recursive-fnnames-alist-rec term ens wrld nil)))
(defun non-recursive-fnnames-alist-lst (lst ens wrld)
; See non-recursive-fnnames-alist-rec. (The present function takes a list of
; terms; it also reverses the result, to respect the original order of
; appearance of function symbols.)
(reverse (non-recursive-fnnames-alist-rec-lst lst ens wrld nil)))
; The alist just constructed is odd because it may contain some lambda
; expressions posing as function symbols. We use the following function
; to transform those into let's just for printing purposes...
(defun hide-lambdas1 (formals)
; CLTL uses # as the "too deep to show" symbol. But if we use it, we
; print vertical bars around it. Until we modify the printer to support
; some kind of hiding, we'll use Interlisp's ampersand.
(cond ((null formals) nil)
(t (cons (list (car formals) '&)
(hide-lambdas1 (cdr formals))))))
(defun hide-lambdas (lst)
(cond ((null lst) nil)
(t (cons (if (flambdap (car lst))
(list 'let (hide-lambdas1 (lambda-formals (car lst)))
(lambda-body (car lst)))
(car lst))
(hide-lambdas (cdr lst))))))
; Now we develop the stuff to determine if we have a permutative :REWRITE rule.
(defun variantp (term1 term2)
; This function returns two values: A flag indicating whether the two
; terms are variants and the substitution which when applied to term1
; yields term2.
(mv-let (ans unify-subst)
(one-way-unify term1 term2)
(cond
(ans
(let ((range (strip-cdrs unify-subst)))
(mv (and (symbol-listp range)
(no-duplicatesp-equal range))
unify-subst)))
(t (mv nil nil)))))
(mutual-recursion
(defun surrounding-fns1 (vars term fn acc)
; See surrounding-fns for the definition of the notions used below.
; Vars is a list of variables. Term is a term that occurs as an argument in
; some (here unknown) application of the function fn. Acc is either a list of
; function symbols or the special token 'has-lambda. Observe that if term is a
; var in vars, then fn surrounds some var in vars in whatever larger term
; contained the application of fn.
; If term is a var in vars, we collect fn into acc. If term is not a var, we
; collect into acc all the function symbols surrounding any element of vars.
; However, if we ever encounter a lambda application surrounding a var in vars
; (including fn), we set acc to the special token 'has-lambda, and collections
; cease thereafter.
(cond
((variablep term)
(cond
((member-eq term vars)
(if (or (eq acc 'has-lambda)
(not (symbolp fn)))
'has-lambda
(add-to-set-eq fn acc)))
(t acc)))
((fquotep term) acc)
(t (surrounding-fns-lst vars (fargs term) (ffn-symb term) acc))))
(defun surrounding-fns-lst (vars term-list fn acc)
(cond
((null term-list) acc)
(t (surrounding-fns-lst vars (cdr term-list) fn
(surrounding-fns1 vars (car term-list) fn acc)))))
)
(defun surrounding-fns (vars term)
; This function returns the list of all functions fn surrounding, in term, any
; var in vars, except that if that list includes a lambda expression we return
; nil.
; We make this precise as follows. Let us say a function symbol or lambda
; expression, fn, ``surrounds'' a variable v in term if there is a subterm of
; term that is an application of fn and v is among the actuals of that
; application. Thus, in the term (fn (g x) (h (d x)) y), g and d both surround
; x and fn surrounds y. Note that h surrounds no variable.
; Consider the set, s, of all functions fn such that fn surrounds a variable
; var in term, where var is a member of the list of variables var. If s
; contains a lambda expression, we return nil; otherwise we return s.
(cond
((or (variablep term)
(fquotep term))
nil)
(t
(let ((ans (surrounding-fns-lst vars (fargs term) (ffn-symb term) nil)))
(if (eq ans 'has-lambda)
nil
ans)))))
(defun loop-stopper1 (alist vars lhs)
(cond ((null alist) nil)
((member-eq (car (car alist))
(cdr (member-eq (cdr (car alist)) vars)))
(cons (list* (caar alist)
(cdar alist)
(surrounding-fns (list (caar alist) (cdar alist)) lhs))
(loop-stopper1 (cdr alist) vars lhs)))
(t (loop-stopper1 (cdr alist) vars lhs))))
(defun loop-stopper (lhs rhs)
; If lhs and rhs are variants (possibly after expanding lambdas in rhs; see
; below), we return the "expansion" (see next paragraph) of the subset of the
; unifying substitution containing those pairs (x . y) in which a variable
; symbol (y) is being moved forward (to the position of x) in the print
; representation of the term. For example, suppose lhs is (foo x y z) and rhs
; is (foo y z x). Then both y and z are moved forward, so the loop-stopper is
; the "expansion" of '((y . z) (x . y)). This function exploits the fact that
; all-vars returns the set of variables listed in reverse print-order.
; In the paragraph above, the "expansion" of a substitution ((x1 . y1) ... (xn
; . yn)) is the list ((x1 y1 . fns-1) ... (xn yn . fns-n)), where fns-i is the
; list of function symbols of subterms of lhs that contain xi or yi (or both)
; as a top-level argument. Exception: If any such "function symbol" is a
; LAMBDA, then fns-i is nil.
; Note: John Cowles first suggested the idea that led to the idea of invisible
; function symbols as implemented here. Cowles observation was that it would
; be very useful if x and (- x) were moved into adjacency by permutative rules.
; His idea was to redefine term-order so that those two terms were of virtually
; equal weight. Our notion of invisible function symbols and the handling of
; loop-stopper is meant to address Cowles original concern without complicating
; term-order, which is used in places besides permutative rewriting.
(mv-let (ans unify-subst)
(variantp lhs
; We expect lhs and rhs to be the left- and right-hand sides of rewrite rules.
; Thus lhs was created by expanding lambdas, but not rhs. We thus expand
; lambdas here.
(remove-lambdas rhs))
(cond (ans (loop-stopper1 unify-subst (all-vars lhs) lhs))
(t nil))))
(defun remove-irrelevant-loop-stopper-pairs (pairs vars)
; Keep this in sync with irrelevant-loop-stopper-pairs.
(if pairs
(if (and (member-eq (caar pairs) vars)
(member-eq (cadar pairs) vars))
; Note that the use of loop-stopper1 by loop-stopper guarantees that
; machine-constructed loop-stoppers only contain pairs (u v . fns) for
; which u and v both occur in the lhs of the rewrite rule. Hence, it
; is reasonable to include the test above.
(cons (car pairs)
(remove-irrelevant-loop-stopper-pairs (cdr pairs) vars))
(remove-irrelevant-loop-stopper-pairs (cdr pairs) vars))
nil))
(defun put-match-free-value (match-free-value rune wrld)
(cond
((eq match-free-value :all)
(global-set 'free-var-runes-all
(cons rune (global-val 'free-var-runes-all wrld))
wrld))
((eq match-free-value :once)
(global-set 'free-var-runes-once
(cons rune (global-val 'free-var-runes-once wrld))
wrld))
((null match-free-value)
wrld)
(t
(er hard 'put-match-free-value
"Internal ACL2 error (called put-match-free-value with ~
match-free-value equal to ~x0). Please contact the ACL2 implementors."
match-free-value))))
(defun free-vars-in-hyps (hyps bound-vars wrld)
; Let hyps be a list of terms -- the hypotheses to some :REWRITE rule.
; Let bound-vars be a list of variables. We find all the variables that
; will be free-vars in hyps when each variable in bound-vars is bound.
; This would be just (set-difference-eq (all-vars1-lst hyps) bound-vars)
; were it not for the fact that relieve-hyps interprets the hypothesis
; (equal v term), where v is free and does not occur in term, as
; a "let v be term..." instead of as a genuine free variable to be found
; by search.
; Warning: Keep this function and free-vars-in-hyps-considering-bind-free
; in sync.
(cond ((null hyps) nil)
(t (mv-let
(forcep flg)
(binding-hyp-p (car hyps)
(pairlis$ bound-vars bound-vars)
wrld)
; The odd pairlis$ above just manufactures a substitution with bound-vars as
; bound vars so we can use free-varsp to answer the question, "does
; the rhs of the equality contain any free variables?" The range of
; the substitution is irrelevant. If the conjunction above is true, then
; the current hyp is of the form (equiv v term) and v will be chosen
; by rewriting term. V is not a "free variable".
(cond ((and flg (not forcep))
(free-vars-in-hyps (cdr hyps)
(cons (fargn (car hyps) 1)
bound-vars)
wrld))
(t (let ((hyp-vars (all-vars (car hyps))))
(union-eq
(set-difference-eq hyp-vars bound-vars)
(free-vars-in-hyps (cdr hyps)
(union-eq hyp-vars bound-vars)
wrld)))))))))
(defun free-vars-in-hyps-simple (hyps bound-vars)
; This is a simpler variant of free-vars-in-hyps that does not give special
; treatment to terms (equal variable term).
(cond ((null hyps) nil)
(t (let ((hyp-vars (all-vars (car hyps))))
(union-eq (set-difference-eq hyp-vars bound-vars)
(free-vars-in-hyps-simple (cdr hyps)
(union-eq hyp-vars
bound-vars)))))))
(defun free-vars-in-fc-hyps (triggers hyps concls)
; This function determines whether a rule has free variables, given the
; triggers, hyps and conclusions of the rule.
(if (endp triggers)
nil
(let ((vars (all-vars (car triggers))))
(or (free-vars-in-hyps-simple hyps vars)
(or (free-vars-in-hyps-simple concls vars)
(free-vars-in-fc-hyps (cdr triggers) hyps concls))))))
(defun free-vars-in-hyps-considering-bind-free (hyps bound-vars wrld)
; This function is similar to the above free-vars-in-hyps. It
; differs in that it takes into account the effects of bind-free.
; Note that a bind-free hypothesis expands to a call to synp in
; which the first arg denotes the vars that are potentially bound
; by the hyp. This first arg will be either a quoted list of vars
; or 't which we interpret to mean all the otherwise free vars.
; Vars that are potentially bound by a bind-free hyp are not considered
; to be free vars for the purposes of this function.
; Note that a syntaxp hypothesis also expands to a call of synp,
; but that in this case the first arg is 'nil.
; Warning: Keep this function and free-vars-in-hyps in sync.
(cond ((null hyps) nil)
(t (mv-let
(forcep flg)
(binding-hyp-p (car hyps)
(pairlis$ bound-vars bound-vars)
wrld)
; The odd pairlis$ above just manufactures a substitution with bound-vars as
; bound vars so we can use free-varsp to answer the question, "does
; the rhs of the equality contain any free variables?" The range of
; the substitution is irrelevant. If the conjunction above is true, then
; the current hyp is of the form (equiv v term) and v will be chosen
; by rewriting term. V is not a "free variable".
(cond
((and flg (not forcep))
(free-vars-in-hyps-considering-bind-free
(cdr hyps)
(cons (fargn (car hyps) 1) bound-vars)
wrld))
((and (ffn-symb-p (car hyps) 'synp)
(not (equal (fargn (car hyps) 1) *nil*))) ; not syntaxp hyp
(cond
((equal (fargn (car hyps) 1) *t*)
; All free variables are potentially bound. The user will presumably not want
; to see a warning in this case.
nil)
((and (quotep (fargn (car hyps) 1))
(not (collect-non-legal-variableps
(cadr (fargn (car hyps) 1)))))
(free-vars-in-hyps-considering-bind-free
(cdr hyps)
(union-eq (cadr (fargn (car hyps) 1)) bound-vars)
wrld))
(t (er hard 'free-vars-in-hyps-considering-bind-free
"We thought the first argument of synp in this context ~
was either 'NIL, 'T, or else a quoted true list of ~
variables, but ~x0 is not!"
(fargn (car hyps) 1)))))
(t (let ((hyp-vars (all-vars (car hyps))))
(union-eq (set-difference-eq hyp-vars bound-vars)
(free-vars-in-hyps-considering-bind-free
(cdr hyps)
(union-eq hyp-vars bound-vars)
wrld)))))))))
(defun all-vars-in-hyps (hyps)
; We return a list of all the vars mentioned in hyps or, if there is
; a synp hyp whose var-list is 't, we return t.
(cond
((null hyps)
nil)
(t
(let ((vars (all-vars-in-hyps (cdr hyps))))
(cond
((eq vars t) t)
((variablep (car hyps))
(add-to-set-eq (car hyps) vars))
((fquotep (car hyps))
vars)
((eq (ffn-symb (car hyps)) 'synp)
(cond ((equal (fargn (car hyps) 1) *nil*)
vars)
((equal (fargn (car hyps) 1) *t*)
t)
((and (quotep (fargn (car hyps) 1))
(not (collect-non-legal-variableps
(cadr (fargn (car hyps) 1)))))
(union-eq (cadr (fargn (car hyps) 1))
vars))
(t (er hard 'free-vars-in-hyps-considering-bind-free
"We thought the first argument of synp in this context ~
was either 'NIL, 'T, or else a quoted true list of ~
variables, but ~x0 is not!"
(fargn (car hyps) 1)))))
(t
(union-eq (all-vars (car hyps))
vars)))))))
(defun match-free-value (match-free hyps pat wrld)
(or match-free
(and (free-vars-in-hyps hyps (all-vars pat) wrld)
(or (match-free-default wrld)
; We presumably already caused an error if at this point we would find a value
; of t for state global match-free-error.
:all))))
(defun match-free-fc-value (match-free hyps concls triggers wrld)
; This function, based on match-free-value, uses free-vars-in-fc-hyps to
; determine whether free-vars are present in a forward-chaining rule (if so it
; returns nil). If free-vars are not present then it uses the match-free value
; of the rule (given by the match-free arg) or the match-free default value of
; the world to determine the correct match-free value for this particular rule.
(or match-free
(and (free-vars-in-fc-hyps triggers hyps concls)
(or (match-free-default wrld)
:all))))
(defun rule-backchain-limit-lst (backchain-limit-lst hyps wrld flg)
(cond (backchain-limit-lst (cadr backchain-limit-lst))
(t (let ((limit (default-backchain-limit wrld flg)))
(and limit
(cond ((eq flg :meta) limit)
(t (make-list (length hyps)
:initial-element
limit))))))))
(defun create-rewrite-rule (qc-flg rune nume hyps equiv lhs rhs
loop-stopper-lst backchain-limit-lst
match-free-value wrld)
; Qc-flg indicates that we are creating a rewrite-quoted-constant rule. Equiv
; is an equivalence relation name. This function creates a :REWRITE rule of
; subclass 'backchain, 'abbreviation, or 'rewrite-quoted-constant from the
; basic ingredients, preprocessing the hyps and computing the loop-stopper.
(let ((hyps (preprocess-hyps hyps wrld))
(loop-stopper (if loop-stopper-lst
(remove-irrelevant-loop-stopper-pairs
(cadr loop-stopper-lst)
(all-vars lhs))
(loop-stopper lhs rhs))))
(make rewrite-rule
:rune rune
:nume nume
:hyps hyps
:equiv equiv
:lhs lhs
:var-info (free-varsp lhs nil)
:rhs rhs
:subclass (cond (qc-flg 'rewrite-quoted-constant)
((and (null hyps)
(null loop-stopper)
(abbreviationp nil
(all-vars-bag lhs nil)
rhs))
'abbreviation)
(t 'backchain))
:heuristic-info
(if qc-flg
(cons (form-of-rewrite-quoted-constant-rule equiv lhs rhs)
loop-stopper)
loop-stopper)
; If backchain-limit-lst is given, then it is a keyword-alist whose second
; element is a list of values of length (length hyps), and we use this value.
; Otherwise we use the default. This will be either nil -- used directly -- or
; an integer which we expand to a list of (length hyps) copies.
:backchain-limit-lst
(rule-backchain-limit-lst backchain-limit-lst hyps wrld :rewrite)
:match-free match-free-value)))
; The next subsection of our code develops various checkers to help the
; user manage his collection of rules.
(defun hyps-that-instantiate-free-vars (free-vars hyps)
; We determine the hyps in hyps that will be used to instantiate
; the free variables, free-vars, of some rule. Here, variables "bound" by
; calls of bind-free are not considered free in the case of rewrite and linear
; rules, so would not appear among free-vars in those cases.
(cond ((null free-vars) nil)
((intersectp-eq free-vars (all-vars (car hyps)))
(cons (car hyps)
(hyps-that-instantiate-free-vars
(set-difference-eq free-vars (all-vars (car hyps)))
(cdr hyps))))
(t (hyps-that-instantiate-free-vars free-vars (cdr hyps)))))
(mutual-recursion
(defun maybe-one-way-unify (pat term alist)
; We return t if "it is possible" that pat matches term. More accurately, if
; we return nil, then (one-way-unify1 pat term alist) definitely fails. Thus,
; the answer t below is always safe. The answer nil means there is no
; substitution, s extending alist such that pat/s is term.
(cond ((variablep pat)
(let ((pair (assoc-eq pat alist)))
(or (not pair)
(eq pat (cdr pair)))))
((fquotep pat) (equal pat term))
((variablep term) nil)
((fquotep term) t)
((equal (ffn-symb pat) (ffn-symb term))
(maybe-one-way-unify-lst (fargs pat) (fargs term) alist))
(t nil)))
(defun maybe-one-way-unify-lst (pat-lst term-lst alist)
(cond ((endp pat-lst) t)
(t (and (maybe-one-way-unify (car pat-lst) (car term-lst) alist)
(maybe-one-way-unify-lst (cdr pat-lst) (cdr term-lst)
alist)))))
)
(defun maybe-one-way-unify-with-some (pat term-lst alist)
; If we return nil, then there is no term in term-lst such that (one-way-unify
; pat term alist). If we return t, then pat might unify with some member.
(cond ((endp term-lst) nil)
((maybe-one-way-unify pat (car term-lst) alist) t)
(t (maybe-one-way-unify-with-some pat (cdr term-lst) alist))))
(defun maybe-subsumes (cl1 cl2 alist)
; We return t if it is possible that the instance of cl1 via alist subsumes
; cl2. More accurately, if we return nil then cl1 does not subsume cl2.
; Recall what it means for (subsumes cl1 cl2 alist) to return t: cl1/alist' is
; a subset of cl2, where alist' is an extension of alist. Observe that the
; subset check would fail if cl1 contained a literal (P X) and there is no
; literal beginning with P in cl2. More generally, suppose there is a literal
; of cl1 (e.g., (P X)) that unifies with no literal of cl2. Then cl1 could not
; possibly subsume cl2.
; For a discussion of the origin of this function, see subsumes-rewrite-rule.
; It was made more efficient after Version_3.0, by adding an alist argument to
; eliminate the possibility of subsumption in more cases.
; Note that this function does not give special treatment for literals
; satisfying extra-info-lit-p. We intend this function for use in checking
; subsumption of rewrite rules, and extra-info-lit-p has no special role for
; the rewriter.
(cond ((null cl1) t)
((maybe-one-way-unify-with-some (car cl1) cl2 alist)
(maybe-subsumes (cdr cl1) cl2 alist))
(t nil)))
(defun subsumes-rewrite-rule (rule1 rule2 wrld)
; We answer the question: does rule1 subsume rule2? I.e., can rule1
; (probably) be applied whenever rule2 can be? Since we don't check
; the loop-stoppers, the "probably" is warranted. There may be other
; reasons it is warranted. But this is just a heuristic check performed
; as a service to the user.
; One might ask why we do the maybe-subsumes. We do the subsumes
; check on the hyps of two rules with matching :lhs. In a hardware
; related file we were once confronted with a rule1 having :hyps
; ((BOOLEANP A0) (BOOLEANP B0) (BOOLEANP S0) (BOOLEANP C0_IN)
; (BOOLEANP A1) (BOOLEANP B1) (BOOLEANP S1) (BOOLEANP C1_IN)
; ...
; (S_REL A0 B0 C0_IN S0)
; ...)
; and a rule2 with :hyps
; ((BOOLEANP A0) (BOOLEANP B0) (BOOLEANP S0)
; (BOOLEANP A1) (BOOLEANP B1) (BOOLEANP S1)
; ...)
; The subsumes computation ran for over 30 minutes (and was eventually
; aborted). The problem is that the extra variables in rule1, e.g.,
; C0_IN, were matchable in many different ways, e.g., C0_IN <- A0,
; C0_IN <- B0, etc., all of which must be tried in a subsumption
; check. But no matter how you get rid of (BOOLEANP C0_IN) by
; choosing C0_IN, you will eventually run into the S_REL hypothesis in
; rule1 which has no counterpart in rule2. Thus we installed the
; relatively quick maybe-subsumes check. The check scans the :hyps of
; the first rule and determines whether there is some hypothesis that
; cannot possibly be matched against the hyps of the other rule.
; The caller is responsible for insuring that both rules are ordinary
; :rewrite rules (e.g., of :subclass abbreviation, backchain, etc) or
; :rewrite-quoted-constant rules (e.g., :subclass rewrite-quoted-constant).
; This is done by chk-rewrite-rule-warnings when it checks a new :rewrite
; rule only against existing rules in the lemmas property of the top fn, but
; checks a new :rewrite-quoted-constant rule against the rules in the global
; var rewrite-quoted-constant-rules.
; On subsumption of rewrite-quoted-constant rules. Form [1] and [3] rules
; can be treated just like ordinary :rewrite rules. But form [2] rules are
; different because they're of the form (equiv (fn x) x), where it is
; actually x that is matched to the quoted constant and then (fn x) is used
; to compute the new evg. If a form [2] rule were ever party to a
; subsumption check you'd have to swap the orientation of conclusion.
; Furthermore, you'd find it would subsume any rule it was compared to, and
; you would find that no rule (except another form [2] rule) would subsume
; it. It short, it seems pointless to include form [2] rules in subsumption
; checks! Recal that the :heuristic-info field of a rewrite-quoted-constant
; rule is (n . loop-stopper), where n is the form number.
(and (not (eql (car (access rewrite-rule rule1 :heuristic-info)) 2))
(not (eql (car (access rewrite-rule rule2 :heuristic-info)) 2))
(refinementp (access rewrite-rule rule1 :equiv)
(access rewrite-rule rule2 :equiv)
wrld)
(mv-let (ans unify-subst)
(one-way-unify (access rewrite-rule rule1 :lhs)
(access rewrite-rule rule2 :lhs))
(and ans
(maybe-subsumes
(access rewrite-rule rule1 :hyps)
(access rewrite-rule rule2 :hyps)
unify-subst)
(eq (subsumes *init-subsumes-count*
(access rewrite-rule rule1 :hyps)
(access rewrite-rule rule2 :hyps)
unify-subst)
t)))))
(defun find-subsumed-rule-names (lst rule ens wrld)
; Lst is a list of rewrite-rules. Rule is a rewrite-rule. We return
; the names of those elements of lst that are subsumed by rule. We
; skip those rules in lst that are disabled in the global enabled structure
; and those that are META or DEFINITION rules.
(cond ((null lst) nil)
((and (enabled-numep (access rewrite-rule (car lst) :nume)
ens)
(not (eq (access rewrite-rule (car lst) :subclass) 'meta))
(not (eq (access rewrite-rule (car lst) :subclass) 'definition))
(subsumes-rewrite-rule rule (car lst) wrld))
(cons (base-symbol (access rewrite-rule (car lst) :rune))
(find-subsumed-rule-names (cdr lst) rule ens wrld)))
(t (find-subsumed-rule-names (cdr lst) rule ens wrld))))
(defun find-subsuming-rule-names (lst rule ens wrld)
; Lst is a list of rewrite-rules. Rule is a rewrite-rule. We return
; the names of those elements of lst that subsume rule. We skip those
; rules in lst that are disabled and that are META or DEFINITION rules.
(cond ((null lst) nil)
((and (enabled-numep (access rewrite-rule (car lst) :nume)
ens)
(not (eq (access rewrite-rule (car lst) :subclass) 'meta))
(not (eq (access rewrite-rule (car lst) :subclass) 'definition))
(subsumes-rewrite-rule (car lst) rule wrld))
(cons (base-symbol (access rewrite-rule (car lst) :rune))
(find-subsuming-rule-names (cdr lst) rule ens wrld)))
(t (find-subsuming-rule-names (cdr lst) rule ens wrld))))
(defun forced-hyps (lst)
(cond ((null lst) nil)
((and (nvariablep (car lst))
; (not (fquotep (car lst)))
(or (eq (ffn-symb (car lst)) 'force)
(eq (ffn-symb (car lst)) 'case-split)))
(cons (car lst) (forced-hyps (cdr lst))))
(t (forced-hyps (cdr lst)))))
(defun strip-top-level-nots-and-forces (hyps)
(cond
((null hyps)
nil)
(t (mv-let (not-flg atm)
(strip-not (if (and (nvariablep (car hyps))
; (not (fquotep (car hyps)))
(or (eq (ffn-symb (car hyps)) 'force)
(eq (ffn-symb (car hyps)) 'case-split)))
(fargn (car hyps) 1)
(car hyps)))
(declare (ignore not-flg))
(cons atm (strip-top-level-nots-and-forces (cdr hyps)))))))
(defun free-variable-error? (token name ctx wrld state)
(if (and (null (match-free-default wrld))
(f-get-global 'match-free-error state))
(er soft ctx
"The warning above has caused this error in order to make it clear ~
that there are free variables in ~s0 of a ~x1 rule generated from ~
~x2. This error can be suppressed for the rest of this ACL2 ~
session by submitting the following form:~|~%~x3~|~%However, you ~
are advised not to do so until you have read the documentation on ~
``free variables'' (see :DOC free-variables) in order to understand ~
the issues. In particular, you can supply a :match-free value for ~
the :rewrite rule class (see :DOC rule-classes) or a default for ~
the book under development (see :DOC set-match-free-default)."
(if (eq token :forward-chaining)
"some trigger term"
"the hypotheses")
token name '(set-match-free-error nil))
(value nil)))
(defun extend-geneqv-alist (var geneqv alist wrld)
; For each pair (x . y) in alist, x is a variable and y is a geneqv. The
; result extends alist by associating variable var with geneqv, thus extending
; the generated equivalence relation already associated with var in alist.
(put-assoc-eq var
(union-geneqv geneqv (cdr (assoc-eq var alist)) wrld)
alist))
(mutual-recursion