-
Notifications
You must be signed in to change notification settings - Fork 0
/
defuns.lisp
9209 lines (8046 loc) · 402 KB
/
defuns.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 6.4 -- A Computational Logic for Applicative Common Lisp
; Copyright (C) 2014, 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")
; Rockwell Addition: A major change is the provision of non-executable
; functions. These are typically functions that use stobjs but which
; are translated as though they were theorems rather than definitions.
; This is convenient (necessary?) for specifying some stobj
; properties. These functions will have executable counterparts that
; just throw. These functions will be marked with the property
; non-executablep.
(defconst *mutual-recursion-ctx-string*
"( MUTUAL-RECURSION ( DEFUN ~x0 ...) ...)")
(defun translate-bodies1 (non-executablep names bodies bindings
known-stobjs-lst ctx wrld state-vars)
; Non-executablep should be t or nil, to indicate whether or not the bodies are
; to be translated for execution. In the case of a function introduced by
; defproxy, non-executablep will be nil.
(cond ((null bodies) (trans-value nil))
(t (mv-let
(erp x bindings2)
(translate1-cmp (car bodies)
(if non-executablep t (car names))
(if non-executablep nil bindings)
(car known-stobjs-lst)
(if (and (consp ctx)
(equal (car ctx)
*mutual-recursion-ctx-string*))
(msg "( MUTUAL-RECURSION ... ( DEFUN ~x0 ...) ~
...)"
(car names))
ctx)
wrld state-vars)
(cond
((and erp
(eq bindings2 :UNKNOWN-BINDINGS))
; We try translating in some other order. This attempt isn't complete; for
; example, the following succeeds, but it fails if we switch the first two
; definitions. But it's cheap and better than nothing; without it, the
; unswitched version would fail, too. If this becomes an issue, consider the
; potentially quadratic algorithm of first finding one definition that
; translates successfully, then another, and so on, until all have been
; translated.
; (set-state-ok t)
; (set-bogus-mutual-recursion-ok t)
; (program)
; (mutual-recursion
; (defun f1 (state)
; (let ((state (f-put-global 'last-m 1 state)))
; (f2 state)))
; (defun f2 (state)
; (let ((state (f-put-global 'last-m 1 state)))
; (f3 state)))
; (defun f3 (state)
; state))
(trans-er-let*
((y (translate-bodies1 non-executablep
(cdr names)
(cdr bodies)
bindings
(cdr known-stobjs-lst)
ctx wrld state-vars))
(x (translate1-cmp (car bodies)
(if non-executablep t (car names))
(if non-executablep nil bindings)
(car known-stobjs-lst)
(if (and (consp ctx)
(equal (car ctx)
*mutual-recursion-ctx-string*))
(msg "( MUTUAL-RECURSION ... ( DEFUN ~x0 ...) ~
...)"
(car names))
ctx)
wrld state-vars)))
(trans-value (cons x y))))
(erp (mv erp x bindings2))
(t (let ((bindings bindings2))
(trans-er-let*
((y (translate-bodies1 non-executablep
(cdr names)
(cdr bodies)
bindings
(cdr known-stobjs-lst)
ctx wrld state-vars)))
(trans-value (cons x y))))))))))
(defun chk-non-executable-bodies (names arglists bodies non-executablep ctx
state)
; Note that bodies are in translated form.
(cond ((endp bodies)
(value nil))
(t (let ((name (car names))
(body (car bodies))
(formals (car arglists)))
; The body should generally be a translated form of (prog2$
; (throw-nonexec-error 'name (list . formals)) ...), as laid down by
; defun-nx-fn. But we make an exception for defproxy, i.e. (eq non-executablep
; :program), since it won't be true in that case and we don't care that it be
; true, as we have a program-mode function that does a throw.
(cond ((throw-nonexec-error-p body
(and (not (eq non-executablep
:program))
name)
formals)
(chk-non-executable-bodies
(cdr names) (cdr arglists) (cdr bodies)
non-executablep ctx state))
(t (er soft ctx
"The body of a defun that is marked :non-executable ~
(perhaps implicitly, by the use of defun-nx) must ~
be of the form (prog2$ (throw-nonexec-error ...) ~
...)~@1. The definition of ~x0 is thus illegal. ~
See :DOC defun-nx."
(car names)
(if (eq non-executablep :program)
""
" that is laid down by defun-nx"))))))))
(defun translate-bodies (non-executablep names arglists bodies known-stobjs-lst
ctx wrld state)
; Translate the bodies given and return a pair consisting of their translations
; and the final bindings from translate. Note that non-executable :program
; mode functions need to be analyzed for stobjs-out, because they are proxies
; (see :DOC defproxy) for encapsulated functions that may replace them later,
; and we need to guarantee to callers that those stobjs-out do not change with
; such replacements.
(declare (xargs :guard (true-listp bodies)))
(mv-let (erp lst bindings)
(translate-bodies1 (eq non-executablep t) ; not :program
names bodies
(pairlis$ names names)
known-stobjs-lst
ctx wrld (default-state-vars t))
(er-progn
(cond (erp ; erp is a ctx, lst is a msg
(er soft erp "~@0" lst))
(non-executablep
(chk-non-executable-bodies names arglists lst
non-executablep ctx state))
(t (value nil)))
(cond ((eq non-executablep t)
(value (cons lst (pairlis-x2 names '(nil)))))
(t (value (cons lst bindings)))))))
; The next section develops our check that mutual recursion is
; sensibly used.
(defun chk-mutual-recursion-bad-names (lst names bodies)
(cond ((null lst) nil)
((ffnnamesp names (car bodies))
(chk-mutual-recursion-bad-names (cdr lst) names (cdr bodies)))
(t
(cons (car lst)
(chk-mutual-recursion-bad-names (cdr lst) names (cdr bodies))))))
(defconst *chk-mutual-recursion-string*
"The definition~#0~[~/s~] of ~&1 ~#0~[does~/do~] not call any of ~
the other functions being defined via ~
mutual recursion. The theorem prover ~
will perform better if you define ~&1 ~
without the appearance of mutual recursion. See ~
:DOC set-bogus-mutual-recursion-ok to get ~
ACL2 to handle this situation differently.")
(defun chk-mutual-recursion1 (names bodies warnp ctx state)
(cond
((and warnp
(warning-disabled-p "mutual-recursion"))
(value nil))
(t
(let ((bad (chk-mutual-recursion-bad-names names names bodies)))
(cond ((null bad) (value nil))
(warnp
(pprogn
(warning$ ctx ("mutual-recursion")
*chk-mutual-recursion-string*
(if (consp (cdr bad)) 1 0)
bad)
(value nil)))
(t (er soft ctx
*chk-mutual-recursion-string*
(if (consp (cdr bad)) 1 0)
bad)))))))
(defun chk-mutual-recursion (names bodies ctx state)
; We check that names has at least 1 element and that if it has
; more than one then every body calls at least one of the fns in
; names. The idea is to ensure that mutual recursion is used only
; when "necessary." This is not necessary for soundness but since
; mutually recursive fns are not handled as well as singly recursive
; ones, it is done as a service to the user. In addition, several
; error messages and other user-interface features exploit the presence
; of this check.
(cond ((null names)
(er soft ctx
"It is illegal to use MUTUAL-RECURSION to define no functions."))
((null (cdr names)) (value nil))
(t
(let ((bogus-mutual-recursion-ok
(cdr (assoc-eq :bogus-mutual-recursion-ok
(table-alist 'acl2-defaults-table (w state))))))
(if (eq bogus-mutual-recursion-ok t)
(value nil)
(chk-mutual-recursion1 names bodies
(eq bogus-mutual-recursion-ok :warn)
ctx state))))))
; We now develop put-induction-info.
(mutual-recursion
(defun ffnnamep-mod-mbe (fn term)
; We determine whether the function fn (possibly a lambda-expression) is used
; as a function in term', the result of expanding mbe calls (and equivalent
; calls) in term. Keep this in sync with the ffnnamep nest. Unlike ffnnamep,
; we assume here that fn is a symbolp.
(cond ((variablep term) nil)
((fquotep term) nil)
((flambda-applicationp term)
(or (ffnnamep-mod-mbe fn (lambda-body (ffn-symb term)))
(ffnnamep-mod-mbe-lst fn (fargs term))))
((eq (ffn-symb term) fn) t)
((and (eq (ffn-symb term) 'return-last)
(quotep (fargn term 1))
(eq (unquote (fargn term 1)) 'mbe1-raw))
(ffnnamep-mod-mbe fn (fargn term 3)))
(t (ffnnamep-mod-mbe-lst fn (fargs term)))))
(defun ffnnamep-mod-mbe-lst (fn l)
(declare (xargs :guard (and (symbolp fn)
(pseudo-term-listp l))))
(if (null l)
nil
(or (ffnnamep-mod-mbe fn (car l))
(ffnnamep-mod-mbe-lst fn (cdr l)))))
)
; Here is how we set the recursivep property.
; Rockwell Addition: The recursivep property has changed. Singly
; recursive fns now have the property (fn) instead of fn.
(defun putprop-recursivep-lst (names bodies wrld)
; On the property list of each function symbol is stored the 'recursivep
; property. For nonrecursive functions, the value is implicitly nil but no
; value is stored (see comment below). Otherwise, the value is a true-list of
; fn names in the ``clique.'' Thus, for singly recursive functions, the value
; is a singleton list containing the function name. For mutually recursive
; functions the value is the list of every name in the clique. This function
; stores the property for each name and body in names and bodies.
; WARNING: We rely on the fact that this function puts the same names into the
; 'recursivep property of each member of the clique, in our handling of
; being-openedp.
(cond ((int= (length names) 1)
(cond ((ffnnamep-mod-mbe (car names) (car bodies))
(putprop (car names) 'recursivep names wrld))
(t
; Until we started using the 'def-bodies property to answer most questions
; about recursivep (see macro recursivep), it was a good idea to put a
; 'recursivep property of nil in order to avoid having getprop walk through an
; entire association list looking for 'recursivep. Now, this less-used
; property is just in the way.
wrld)))
(t (putprop-x-lst1 names 'recursivep names wrld))))
(defrec tests-and-call (tests call) nil)
; In nqthm this record was called TEST-AND-CASE and the second component was
; the arglist of a recursive call of the function being analyzed. Because of
; the presence of mutual recursion, we have renamed it tests-and-call and the
; second component is a "recursive" call (possibly mutually recursive).
(mutual-recursion
(defun all-calls (names term alist ans)
; Names is a list of defined function symbols. We accumulate into ans all
; terms u/alist such that for some f in names, u is a subterm of term that is a
; call of f. The algorithm just explores term looking for calls, and
; instantiate them as they are found.
; Our answer is in reverse print order (displaying lambda-applications
; as LETs). For example, if a, b and c are all calls of fns in names,
; then if term is (foo a ((lambda (x) c) b)), which would be printed
; as (foo a (let ((x b)) c)), the answer is (c b a).
(cond ((variablep term) ans)
((fquotep term) ans)
((flambda-applicationp term)
(all-calls names
(lambda-body (ffn-symb term))
(pairlis$ (lambda-formals (ffn-symb term))
(sublis-var-lst alist (fargs term)))
(all-calls-lst names (fargs term) alist ans)))
(t (all-calls-lst names
(fargs term)
alist
(cond ((member-eq (ffn-symb term) names)
(add-to-set-equal
(sublis-var alist term)
ans))
(t ans))))))
(defun all-calls-lst (names lst alist ans)
(cond ((null lst) ans)
(t (all-calls-lst names
(cdr lst)
alist
(all-calls names (car lst) alist ans)))))
)
(defun all-calls-alist (names alist ans)
; This function processes an alist and computes all the calls of fns
; in names in the range of the alist and accumulates them onto ans.
(cond ((null alist) ans)
(t (all-calls-alist names (cdr alist)
(all-calls names (cdar alist) nil ans)))))
(defun termination-machine1 (tests calls ans)
; This function makes a tests-and-call with tests tests for every call
; in calls. It accumulates them onto ans so that if called initially
; with ans=nil the result is a list of tests-and-call in the reverse
; order of the calls.
(cond ((null calls) ans)
(t (termination-machine1 tests
(cdr calls)
(cons (make tests-and-call
:tests tests
:call (car calls))
ans)))))
(mutual-recursion
; This clique is identical to the ffnnamesp/ffnnamesp-lst clique, except that
; here we assume that every element of fns is a symbol.
(defun ffnnamesp-eq (fns term)
(cond ((variablep term) nil)
((fquotep term) nil)
((flambda-applicationp term)
(or (member-eq (ffn-symb term) fns)
(ffnnamesp-eq fns (lambda-body (ffn-symb term)))
(ffnnamesp-eq-lst fns (fargs term))))
((member-eq (ffn-symb term) fns) t)
(t (ffnnamesp-eq-lst fns (fargs term)))))
(defun ffnnamesp-eq-lst (fns l)
(if (null l)
nil
(or (ffnnamesp-eq fns (car l))
(ffnnamesp-eq-lst fns (cdr l)))))
)
(defun member-eq-all (a lst)
(or (eq lst :all)
(member-eq a lst)))
(mutual-recursion
(defun termination-machine (names body alist tests ruler-extenders)
; This function builds a list of tests-and-call records for all calls in body
; of functions in names, but substituting alist into every term in the result.
; At the top level, body is the body of a function in names and alist is nil.
; Note that we don't need to know the function symbol to which the body
; belongs; all the functions in names are considered "recursive" calls. Names
; is a list of all the mutually recursive fns in the clique. Alist maps
; variables in body to actuals and is used in the exploration of lambda
; applications.
; For each recursive call in body a tests-and-call is returned whose tests are
; all the tests that "rule" the call and whose call is the call. If a rules b
; then a governs b but not vice versa. For example, in (if (g (if a b c)) d e)
; a governs b but does not rule b. The reason for taking this weaker notion of
; governance is that we can show that the tests-and-calls are together
; sufficient to imply the tests-and-calls generated by induction-machine. The
; notion of "rules" is extended by ruler-extenders; see :doc
; acl2-defaults-table and see :doc ruler-extenders.
(cond
((or (variablep body)
(fquotep body))
nil)
((flambda-applicationp body)
(let ((lambda-body-result
(termination-machine names
(lambda-body (ffn-symb body))
(pairlis$ (lambda-formals (ffn-symb body))
(sublis-var-lst alist (fargs body)))
tests
ruler-extenders)))
(cond
((member-eq-all :lambdas ruler-extenders)
(union-equal (termination-machine-for-list names
(fargs body)
alist
tests
ruler-extenders)
lambda-body-result))
(t
(termination-machine1
(reverse tests)
(all-calls-lst names
(fargs body)
alist
nil)
lambda-body-result)))))
((eq (ffn-symb body) 'if)
(let* ((inst-test (sublis-var alist
; Since (remove-guard-holders x) is provably equal to x, the machine we
; generate using it below is equivalent to the machine generated without it.
(remove-guard-holders (fargn body 1))))
(branch-result
(append (termination-machine names
(fargn body 2)
alist
(cons inst-test tests)
ruler-extenders)
(termination-machine names
(fargn body 3)
alist
(cons (dumb-negate-lit inst-test)
tests)
ruler-extenders))))
(cond
((member-eq-all 'if ruler-extenders)
(append (termination-machine names
(fargn body 1)
alist
tests
ruler-extenders)
branch-result))
(t
(termination-machine1
(reverse tests)
(all-calls names (fargn body 1) alist nil)
branch-result)))))
((and (eq (ffn-symb body) 'return-last)
(quotep (fargn body 1))
(eq (unquote (fargn body 1)) 'mbe1-raw))
; It is sound to treat return-last as a macro for logic purposes. We do so for
; (return-last 'mbe1-raw exec logic) both for induction and for termination.
; We could probably do this for any return-last call, but for legacy reasons
; (before introduction of return-last after v4-1) we restrict to 'mbe1-raw.
(termination-machine names
(fargn body 3) ; (return-last 'mbe1-raw exec logic)
alist
tests
ruler-extenders))
((member-eq-all (ffn-symb body) ruler-extenders)
(let ((rec-call (termination-machine-for-list names (fargs body) alist
tests ruler-extenders)))
(if (member-eq (ffn-symb body) names)
(cons (make tests-and-call
:tests (reverse tests)
:call (sublis-var alist body))
rec-call)
rec-call)))
(t (termination-machine1 (reverse tests)
(all-calls names body alist nil)
nil))))
(defun termination-machine-for-list (names bodies alist tests ruler-extenders)
(cond ((endp bodies) nil)
(t (append (termination-machine names (car bodies) alist tests
ruler-extenders)
(termination-machine-for-list names (cdr bodies) alist tests
ruler-extenders)))))
)
(defun termination-machines (names bodies ruler-extenders-lst)
; This function builds the termination machine for each function defined
; in names with the corresponding body in bodies. A list of machines
; is returned.
(cond ((null bodies) nil)
(t (cons (termination-machine names (car bodies) nil nil
(car ruler-extenders-lst))
(termination-machines names (cdr bodies)
(cdr ruler-extenders-lst))))))
; We next develop the function that guesses measures when the user has
; not supplied them.
(defun proper-dumb-occur-as-output (x y)
; We determine whether the term x properly occurs within the term y, insisting
; in addition that if y is an IF expression then x occurs properly within each
; of the two output branches.
; For example, X does not properly occur in X or Z. It does properly occur in
; (CDR X) and (APPEND X Y). It does properly occur in (IF a (CDR X) (CAR X))
; but not in (IF a (CDR X) 0) or (IF a (CDR X) X).
; This function is used in always-tested-and-changedp to identify a formal to
; use as the measured formal in the justification of a recursive definition.
; We seek a formal that is tested on every branch and changed in every
; recursion. But if (IF a (CDR X) X) is the new value of X in some recursion,
; then it is not really changed, since if we distributed the IF out of the
; recursive call we would see a call in which X did not change.
(cond ((equal x y) nil)
((variablep y) nil)
((fquotep y) nil)
((eq (ffn-symb y) 'if)
(and (proper-dumb-occur-as-output x (fargn y 2))
(proper-dumb-occur-as-output x (fargn y 3))))
(t (dumb-occur-lst x (fargs y)))))
(defun always-tested-and-changedp (var pos t-machine)
; Is var involved in every tests component of t-machine and changed
; and involved in every call, in the appropriate argument position?
; In some uses of this function, var may not be a variable symbol
; but an arbitrary term.
(cond ((null t-machine) t)
((and (dumb-occur-lst var
(access tests-and-call
(car t-machine)
:tests))
(let ((argn (nth pos
(fargs (access tests-and-call
(car t-machine)
:call)))))
; If argn is nil then it means there was no enough args to get the one at pos.
; This can happen in a mutually recursive clique not all clique members have the
; same arity.
(and argn
(proper-dumb-occur-as-output var argn))))
(always-tested-and-changedp var pos (cdr t-machine)))
(t nil)))
(defun guess-measure (name defun-flg args pos t-machine ctx wrld state)
; T-machine is a termination machine, i.e., a lists of tests-and-call. Because
; of mutual recursion, we do not know that the call of a tests-and-call is a
; call of name; it may be a call of a sibling of name. We look for the first
; formal that is (a) somehow tested in every test and (b) somehow changed in
; every call. Upon finding such a var, v, we guess the measure (acl2-count v).
; But what does it mean to say that v is "changed in a call" if we are defining
; (foo x y v) and see a call of bar? We mean that v occurs in an argument to
; bar and is not equal to that argument. Thus, v is not changed in (bar x v)
; and is changed in (bar x (mumble v)). The difficulty here of course is that
; (mumble v) may not be being passed as the new value of v. But since this is
; just a heuristic guess intended to save the user the burden of typing
; (acl2-count x) a lot, it doesn't matter.
; If we fail to find a measure we cause an error.
; Pos is initially 0 and is the position in the formals list of the first
; variable listed in args. Defun-flg is t if we are guessing a measure on
; behalf of a function definition and nil if we are guessing on behalf of a
; :definition rule. It affects only the error message printed.
(cond ((null args)
(cond
((null t-machine)
; Presumably guess-measure was called here with args = NIL, for example if
; :set-bogus-mutual-recursion allowed it. We pick a silly measure that will
; work. If it doesn't work (hard to imagine), well then, we'll find out when
; we try to prove termination.
(value (mcons-term* (default-measure-function wrld) *0*)))
(t
(er soft ctx
"No ~#0~[:MEASURE~/:CONTROLLER-ALIST~] was supplied with the ~
~#0~[definition of~/proposed :DEFINITION rule for~] ~x1. Our ~
heuristics for guessing one have not made any suggestions. ~
No argument of the function is tested along every branch of ~
the relevant IF structure and occurs as a proper subterm at ~
the same argument position in every recursive call. You must ~
specify a ~#0~[:MEASURE. See :DOC defun.~/:CONTROLLER-ALIST. ~
~ See :DOC definition.~@2~] Also see :DOC ruler-extenders ~
for how to affect how much of the IF structure is explored by ~
our heuristics."
(if defun-flg 0 1)
name
(cond
(defun-flg "")
(t " In some cases you may wish to use the :CONTROLLER-ALIST ~
from the original (or any previous) definition; this may ~
be seen by using :PR."))))))
((always-tested-and-changedp (car args) pos t-machine)
(value (mcons-term* (default-measure-function wrld) (car args))))
(t (guess-measure name defun-flg (cdr args) (1+ pos)
t-machine ctx wrld state))))
(defun guess-measure-alist (names arglists measures t-machines ctx wrld state)
; We either cause an error or return an alist mapping the names in
; names to their measures (either user suggested or guessed).
; Warning: The returned alist, a, should have the property that (strip-cars a)
; is equal to names. We rely on that property in put-induction-info.
(cond ((null names) (value nil))
((equal (car measures) *no-measure*)
(er-let* ((m (guess-measure (car names)
t
(car arglists)
0
(car t-machines)
ctx wrld state)))
(er-let* ((alist (guess-measure-alist (cdr names)
(cdr arglists)
(cdr measures)
(cdr t-machines)
ctx wrld state)))
(value (cons (cons (car names) m)
alist)))))
(t (er-let* ((alist (guess-measure-alist (cdr names)
(cdr arglists)
(cdr measures)
(cdr t-machines)
ctx wrld state)))
(value (cons (cons (car names) (car measures))
alist))))))
; We now embark on the development of prove-termination, which must
; prove the justification theorems for each termination machine and
; the measures supplied/guessed.
(defun remove-built-in-clauses (cl-set ens oncep-override wrld state ttree)
; We return two results. The first is a subset of cl-set obtained by deleting
; all built-in-clauseps and the second is the accumulated ttrees for the
; clauses we deleted.
(cond
((null cl-set) (mv nil ttree))
(t (mv-let
(built-in-clausep ttree1)
(built-in-clausep
; We added defun-or-guard-verification as the caller arg of the call of
; built-in-clausep below. This addition is a little weird because there is no
; such function as defun-or-guard-verification; the caller argument is only
; used in trace reporting by forward-chaining. If we wanted to be more precise
; about who is responsible for this call, we'd have to change a bunch of
; functions because this function is called by clean-up-clause-set which is in
; turn called by prove-termination, guard-obligation-clauses, and
; verify-valid-std-usage (which is used in the non-standard defun-fn1). We
; just didn't think it mattered so much as to to warrant changing all those
; functions.
'defun-or-guard-verification
(car cl-set) ens oncep-override wrld state)
; Ttree is known to be 'assumption free.
(mv-let
(new-set ttree)
(remove-built-in-clauses (cdr cl-set) ens oncep-override wrld state
(cons-tag-trees ttree1 ttree))
(cond (built-in-clausep (mv new-set ttree))
(t (mv (cons (car cl-set) new-set) ttree))))))))
(defun length-exceedsp (lst n)
(cond ((null lst) nil)
((= n 0) t)
(t (length-exceedsp (cdr lst) (1- n)))))
(defun clean-up-clause-set (cl-set ens wrld ttree state)
; Warning: The set of clauses returned by this function only implies the input
; set. They are thought to be equivalent only if the input set contains no
; tautologies. See the caution in subsumption-replacement-loop.
; This function removes subsumed clauses from cl-set, does replacement (e.g.,
; if the set includes the clauses {~q p} and {q p} replace them both with {p}),
; and removes built-in clauses. It returns two results, the cleaned up clause
; set and a ttree justifying the deletions and extending ttree. The returned
; ttree is 'assumption free (provided the incoming ttree is also) because all
; necessary splitting is done internally.
; Bishop Brock has pointed out that it is unclear what is the best order in
; which to do these two checks. Subsumption-replacement first and then
; built-in clauses? Or vice versa? We do a very trivial analysis here to
; order the two. Bishop is not to blame for this trivial analysis!
; Suppose there are n clauses in the initial cl-set. Suppose there are b
; built-in clauses. The cost of the subsumption-replacement loop is roughly
; n*n and that of the built-in check is n*b. Contrary to all common sense let
; us suppose that the subsumption-replacement loop eliminates redundant clauses
; at the rate, r, so that if we do the subsumption- replacement loop first at a
; cost of n*n we are left with n*r clauses. Note that the worst case for r is
; 1 and the smaller r is, the better; if r were 1/100 it would mean that we
; could expect subsumption-replacement to pare down a set of 1000 clauses to
; just 10. More commonly perhaps, r is just below 1, e.g., 99 out of 100
; clauses are unaffected. To make the analysis possible, let's assume that
; built-in clauses crop up at the same rate! So,
; n^2 + bnr = cost of doing subsumption-replacement first = sub-first
; bn + (nr)^2 = cost of doing built-in clauses first = bic-first
; Observe that when r=1 the two costs are the same, as they should be. But
; generally, r can be expected to be slightly less than 1.
; Here is an example. Let n = 10, b = 100 and r = 99/100. In this example we
; have only a few clauses to consider but lots of built in clauses, and we have
; a realistically low expectation of hits. The cost of sub-first is 1090 but
; the cost of bic-first is 1098. So we should do sub-first.
; On the other hand, if n=100, b=20, and r=99/100 we see sub-first costs 11980
; but bic-first costs 11801, so we should do built-in clauses first. This is a
; more common case.
; In general, we should do built-in clauses first when sub-first exceeds
; bic-first.
; n^2 + bnr >= bn + (nr)^2 = when we should do built-in clauses first
; Solving we get:
; n > b/(1+r).
; Indeed, if n=50 and b=100 and r=99/100 we see the costs of the two equal
; at 7450.
(cond
((let ((sr-limit (sr-limit wrld)))
(and sr-limit (> (length cl-set) sr-limit)))
(pstk
(remove-built-in-clauses
cl-set ens (match-free-override wrld) wrld state
(add-to-tag-tree 'sr-limit t ttree))))
((length-exceedsp cl-set (global-val 'half-length-built-in-clauses wrld))
(mv-let (cl-set ttree)
(pstk
(remove-built-in-clauses cl-set ens
(match-free-override wrld)
wrld state ttree))
(mv (pstk
(subsumption-replacement-loop
(merge-sort-length cl-set) nil nil))
ttree)))
(t (pstk
(remove-built-in-clauses
(pstk
(subsumption-replacement-loop
(merge-sort-length cl-set) nil nil))
ens (match-free-override wrld) wrld state ttree)))))
(defun measure-clause-for-branch (name tc measure-alist rel wrld)
; Name is the name of some function, say f0, in a mutually recursive
; clique. Tc is a tests-and-call in the termination machine of f0 and hence
; contains some tests and a call of some function in the clique, say,
; f1. Measure-alist supplies the measures m0 and m1 for f0 and f1.
; Rel is the well-founded relation we are using.
; We assume that the 'formals for all the functions in the clique have
; already been stored in wrld.
; We create a set of clauses equivalent to
; tests -> (rel m1' m0),
; where m1' is m1 instantiated as indicated by the call of f1.
(let* ((f0 name)
(m0 (cdr (assoc-eq f0 measure-alist)))
(tests (access tests-and-call tc :tests))
(call (access tests-and-call tc :call))
(f1 (ffn-symb call))
(m1-prime (subcor-var
(formals f1 wrld)
(fargs call)
(cdr (assoc-eq f1 measure-alist))))
(concl (mcons-term* rel m1-prime m0)))
(add-literal concl
(dumb-negate-lit-lst tests)
t)))
(defun measure-clauses-for-fn1 (name t-machine measure-alist rel wrld)
(cond ((null t-machine) nil)
(t (conjoin-clause-to-clause-set
(measure-clause-for-branch name
(car t-machine)
measure-alist
rel
wrld)
(measure-clauses-for-fn1 name
(cdr t-machine)
measure-alist
rel
wrld)))))
(defun measure-clauses-for-fn (name t-machine measure-alist mp rel wrld)
; We form all of the clauses that are required to be theorems for the admission
; of name with the given termination machine and measures. Mp is the "domain
; predicate" for the well-founded relation rel, or else mp is t meaning rel is
; well-founded on the universe. (For example, mp is o-p when rel is o<.) For
; the sake of illustration, suppose the defun of name is simply
; (defun name (x)
; (declare (xargs :guard (guard x)))
; (if (test x) (name (d x)) x))
; Assume mp and rel are o-p and o<. Then we will create clauses equivalent
; to:
; (o-p (m x))
; and
; (test x) -> (o< (m (d x)) (m x)).
; Observe that the guard of the function is irrelevant!
; We return a set of clauses which are implicitly conjoined.
(cond
((eq mp t)
(measure-clauses-for-fn1 name t-machine measure-alist rel wrld))
(t (conjoin-clause-to-clause-set
(add-literal (mcons-term* mp (cdr (assoc-eq name measure-alist)))
nil t)
(measure-clauses-for-fn1 name t-machine measure-alist rel wrld)))))
(defun measure-clauses-for-clique (names t-machines measure-alist mp rel wrld)
; We assume we can obtain from wrld the 'formals for each fn in names.
(cond ((null names) nil)
(t (conjoin-clause-sets
(measure-clauses-for-fn (car names)
(car t-machines)
measure-alist
mp rel
wrld)
(measure-clauses-for-clique (cdr names)
(cdr t-machines)
measure-alist
mp rel
wrld)))))
(defun tilde-*-measure-phrase1 (alist wrld)
(cond ((null alist) nil)
(t (cons (msg (cond ((null (cdr alist)) "~p1 for ~x0.")
(t "~p1 for ~x0"))
(caar alist)
(untranslate (cdar alist) nil wrld))
(tilde-*-measure-phrase1 (cdr alist) wrld)))))
(defun tilde-*-measure-phrase (alist wrld)
; Let alist be an alist mapping function symbols, fni, to measure terms, mi.
; The fmt directive ~*0 will print the following, if #\0 is bound to
; the output of this fn:
; "m1 for fn1, m2 for fn2, ..., and mk for fnk."
; provided alist has two or more elements. If alist contains
; only one element, it will print just "m1."
; Note the final period at the end of the phrase! In an earlier version
; we did not add the period and saw a line-break between the ~x1 below
; and its final period.
; Thus, the following fmt directive will print a grammatically correct
; sentence ending with a period: "For the admission of ~&1 we will use
; the measure ~*0"
(list* "" "~@*" "~@* and " "~@*, "
(cond
((null (cdr alist))
(list (cons "~p1."
(list (cons #\1
(untranslate (cdar alist) nil wrld))))))
(t (tilde-*-measure-phrase1 alist wrld)))
nil))
(defun find-?-measure (measure-alist)
(cond ((endp measure-alist) nil)
((let* ((entry (car measure-alist))
(measure (cdr entry)))
(and (consp measure)
(eq (car measure) :?)
entry)))
(t (find-?-measure (cdr measure-alist)))))
(defun prove-termination (names t-machines measure-alist mp rel hints otf-flg
bodies ctx ens wrld state ttree)
; Given a list of the functions introduced in a mutually recursive clique,
; their t-machines, the measure-alist for the clique, a domain predicate mp on
; which a certain relation, rel, is known to be well-founded, a list of hints
; (obtained by joining all the hints in the defuns), and a world in which we
; can find the 'formals of each function in the clique, we prove the theorems
; required by the definitional principle. In particular, we prove that each
; measure is an o-p and that in every tests-and-call in the t-machine of each
; function, the measure of the recursive calls is strictly less than that of
; the incoming arguments. If we fail, we cause an error.
; This function produces output describing the proofs. It should be the first
; output-producing function in the defun processing on every branch through
; defun. It always prints something and leaves you in a clean state ready to
; begin a new sentence, but may leave you in the middle of a line (i.e., col >
; 0).
; If we succeed we return two values, consed together as "the" value in this
; error/value/state producing function. The first value is the column produced
; by our output. The second value is a ttree in which we have accumulated all
; of the ttrees associated with each proof done.
; This function is specially coded so that if t-machines is nil then it is a
; signal that there is only one element of names and it is a non-recursive
; function. In that case, we short-circuit all of the proof machinery and
; simply do the associated output. We coded it this way to preserve the
; invariant that prove-termination is THE place the defun output is initiated.
; This function increments timers. Upon entry, any accumulated time is charged
; to 'other-time. The printing done herein is charged to 'print-time and the
; proving is charged to 'prove-time.
(mv-let
(cl-set cl-set-ttree)
(cond ((and (not (ld-skip-proofsp state))
t-machines)
(clean-up-clause-set
(measure-clauses-for-clique names
t-machines
measure-alist
mp rel
wrld)
ens
wrld ttree state))
(t (mv nil ttree)))
(cond
((and (not (ld-skip-proofsp state))
(find-?-measure measure-alist))
(let* ((entry (find-?-measure measure-alist))
(fn (car entry))
(measure (cdr entry)))
(er soft ctx
"A :measure of the form (:? v1 ... vk) is only legal when the ~
defun is redundant (see :DOC redundant-events) or when skipping ~
proofs (see :DOC ld-skip-proofsp). The :measure ~x0 supplied for ~
function symbol ~x1 is thus illegal."
measure fn)))
(t
(er-let*
((cl-set-ttree (accumulate-ttree-and-step-limit-into-state