forked from acl2/acl2
-
Notifications
You must be signed in to change notification settings - Fork 0
/
defuns.lisp
9760 lines (8534 loc) · 429 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 8.1 -- A Computational Logic for Applicative Common Lisp
; Copyright (C) 2018, Regents of the University of Texas
; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
; (C) 1997 Computational Logic, Inc. See the documentation topic NOTE-2-0.
; This program is free software; you can redistribute it and/or modify
; it under the terms of the LICENSE file distributed with ACL2.
; This program is distributed in the hope that it will be useful,
; but WITHOUT ANY WARRANTY; without even the implied warranty of
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
; LICENSE for more details.
; Written by: Matt Kaufmann and J Strother Moore
; email: [email protected] and [email protected]
; Department of Computer Science
; University of Texas at Austin
; Austin, TX 78712 U.S.A.
(in-package "ACL2")
; 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
reclassifying-all-programp
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
; For the application of verify-termination to a function that has already
; been admitted, we avoid failure due to an untouchable function or variable.
:temp-touchable-fns
(or reclassifying-all-programp
(f-get-global 'temp-touchable-fns
state))
:temp-touchable-vars
(or reclassifying-all-programp
(f-get-global 'temp-touchable-vars
state))))
(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. Moreover, we rely in function termination-theorem-fn-subst
; (and its supporting functions) that the properties are placed in the order in
; which the names are defined: (mutual-recursion (defun name1 ...) (defun name2
; ... ...)) pushes a property for name1 onto a world with property for name2,
; etc.
(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))))
; Formerly, we defined termination-machines and some of its supporting
; functions here. But we moved them to history-management.lisp in order to
; support the definition of termination-theorem-clauses.
; 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 were not enough args to get the one at
; pos. This can happen in a mutually recursive clique where 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.
; Moved remove-built-in-clauses and clean-up-clause-set to
; history-management.lisp.
; Formerly, we defined measure-clauses-for-clique and some of its supporting
; functions here. But we moved them to history-management.lisp in order to
; support the definition of termination-theorem-clauses.
(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 measure-debug 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 measure-debug
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
cl-set-ttree :skip state)))
(pprogn
(increment-timer 'other-time state)
(let ((displayed-goal (prettyify-clause-set cl-set
(let*-abstractionp state)
wrld))
(simp-phrase (tilde-*-simp-phrase cl-set-ttree)))
(mv-let
(col state)
(cond
((ld-skip-proofsp state)
(mv 0 state))
((null t-machines)
(io? event nil (mv col state)
(names)
(fmt "Since ~&0 is non-recursive, its admission is trivial."
(list (cons #\0 names))
(proofs-co state)
state
nil)
:default-bindings ((col 0))))
((null cl-set)
(io? event nil (mv col state)
(measure-alist wrld rel names)
(fmt "The admission of ~&0 ~#0~[is~/are~] trivial, using ~@1 ~
and the measure ~*2"
(list (cons #\0 names)
(cons #\1 (tilde-@-well-founded-relation-phrase
rel wrld))
(cons #\2 (tilde-*-measure-phrase
measure-alist wrld)))
(proofs-co state)
state
(term-evisc-tuple nil state))
:default-bindings ((col 0))))
(t
(io? event nil (mv col state)
(cl-set-ttree displayed-goal simp-phrase measure-alist wrld
rel names)
(fmt "For the admission of ~&0 we will use ~@1 and the ~
measure ~*2 The non-trivial part of the measure ~
conjecture~#3~[~/, given ~*4,~] is~@5~%~%Goal~%~Q67."
(list (cons #\0 names)
(cons #\1 (tilde-@-well-founded-relation-phrase
rel wrld))
(cons #\2 (tilde-*-measure-phrase
measure-alist wrld))
(cons #\3 (if (nth 4 simp-phrase) 1 0))
(cons #\4 simp-phrase)
(cons #\5 (if (tagged-objectsp 'sr-limit
cl-set-ttree)
" as follows (where the ~
subsumption/replacement limit ~
affected this analysis; see :DOC ~
case-split-limitations)."
""))
(cons #\6 displayed-goal)
(cons #\7 (term-evisc-tuple nil state)))
(proofs-co state)
state
nil)
:default-bindings ((col 0)))))
(pprogn
(increment-timer 'print-time state)
(cond
((null cl-set)
; If the io? above did not print because 'event is inhibited, then col is nil.
; Just to keep ourselves sane, we will set it to 0.
(value (cons (or col 0) cl-set-ttree)))
(t
(mv-let
(erp ttree state)
(prove (termify-clause-set cl-set)
(make-pspv ens wrld state
:displayed-goal displayed-goal
:otf-flg otf-flg)
hints ens wrld ctx state)
(cond (erp
(let ((erp-msg
(cond
((subsetp-eq
'(summary error)
(f-get-global 'inhibit-output-lst state))
; This case is an optimization, in order to avoid the computations below, in
; particular of termination-machines. Note that erp-msg is potentially used in
; error output -- see the (er soft ...) form below -- and it is also
; potentially used in summary output, when print-summary passes to
; print-failure the first component of the error triple returned below.
nil)
(t
(msg
"The proof of the measure conjecture for ~&0 ~
has failed.~@1"
names
(if (equal
t-machines
(termination-machines
names bodies
(make-list (length names)
:initial-element
:all)))
""
(msg "~|**NOTE**: The use of declaration ~
~x0 would change the measure ~
conjecture, perhaps making it easier ~
to prove. See :DOC ruler-extenders."
'(xargs :ruler-extenders :all))))))))
(mv-let
(erp val state)
(er soft ctx "~@0~|" erp-msg)
(declare (ignore erp val))
(mv (msg "~@0 " erp-msg) nil state))))
(t
(mv-let (col state)
(io? event nil (mv col state)
(names)
(fmt "That completes the proof of the ~
measure theorem for ~&1. Thus, we ~
admit ~#1~[this function~/these ~
functions~] under the principle of ~
definition."
(list (cons #\1 names))
(proofs-co state)
state
nil)
:default-bindings ((col 0)))
(pprogn
(increment-timer 'print-time state)
(value
(cons
(or col 0)
(cons-tag-trees
cl-set-ttree ttree)))))))))))))))))))
; When we succeed in proving termination, we will store the
; justification properties.
(defun putprop-justification-lst (measure-alist subset-lst mp rel
ruler-extenders-lst
subversive-p wrld)
; Each function has a 'justification property. The value of the property
; is a justification record.
(cond ((null measure-alist) wrld)
(t (putprop-justification-lst
(cdr measure-alist) (cdr subset-lst) mp rel (cdr ruler-extenders-lst)
subversive-p
(putprop (caar measure-alist)
'justification
(make justification
:subset
; The following is equal to (all-vars (cdar measure-alist)), but since we
; already have it available, we use it rather than recomputing this all-vars
; call.
(car subset-lst)
:subversive-p subversive-p
:mp mp
:rel rel
:measure (cdar measure-alist)
:ruler-extenders (car ruler-extenders-lst))
wrld)))))
(defun union-equal-to-end (x y)
; This is like union-equal, but where a common element is removed from the
; second argument instead of the first.
(cond ((intersectp-equal x y)
(append x (set-difference-equal y x)))
(t (append x y))))
(defun cross-tests-and-calls3 (tacs tacs-lst)
(cond ((endp tacs-lst) nil)
(t
(let ((tests1 (access tests-and-calls tacs :tests))
(tests2 (access tests-and-calls (car tacs-lst) :tests)))
(cond ((some-element-member-complement-term tests1 tests2)
(cross-tests-and-calls3 tacs (cdr tacs-lst)))
(t (cons (make tests-and-calls
:tests (union-equal-to-end tests1 tests2)
:calls (union-equal
(access tests-and-calls tacs
:calls)
(access tests-and-calls (car tacs-lst)
:calls)))
(cross-tests-and-calls3 tacs (cdr tacs-lst)))))))))
(defun cross-tests-and-calls2 (tacs-lst1 tacs-lst2)
; See cross-tests-and-calls.
(cond ((endp tacs-lst1) nil)
(t (append (cross-tests-and-calls3 (car tacs-lst1) tacs-lst2)
(cross-tests-and-calls2 (cdr tacs-lst1) tacs-lst2)))))
(defun cross-tests-and-calls1 (tacs-lst-lst acc)
; See cross-tests-and-calls.
(cond ((endp tacs-lst-lst) acc)
(t (cross-tests-and-calls1 (cdr tacs-lst-lst)
(cross-tests-and-calls2 (car tacs-lst-lst)
acc)))))
(defun sublis-tests-rev (test-alist acc)
; Each element of test-alist is a pair (test . alist) where test is a term and
; alist is either an alist or the atom :no-calls, which we treat as nil. Under
; that interpretation, we return the list of all test/alist, in reverse order
; from test-alist.
(cond ((endp test-alist) acc)
(t (sublis-tests-rev
(cdr test-alist)
(let* ((test (caar test-alist))
(alist (cdar test-alist))
(inst-test (cond ((or (eq alist :no-calls)
(null alist))
test)
(t (sublis-expr alist test)))))
(cons inst-test acc))))))
(defun all-calls-test-alist (names test-alist acc)
(cond ((endp test-alist) acc)
(t (all-calls-test-alist
names
(cdr test-alist)
(let* ((test (caar test-alist))
(alist (cdar test-alist)))
(cond ((eq alist :no-calls)
acc)
(t
(all-calls names test alist acc))))))))
(defun cross-tests-and-calls (names top-test-alist top-calls tacs-lst-lst)
; We are given a list, tacs-lst-lst, of lists of non-empty lists of
; tests-and-calls records. Each such record represents a list of tests
; together with a corresponding list of calls. Each way of selecting elements
; <testsi, callsi> in the ith member of tacs-lst-lst can be viewed as a "path"
; through tacs-lst-lst (see also discussion of a matrix, below). We return a
; list containing a tests-and-calls record formed for each path: the tests, as
; the union of the tests of top-test-alist (viewed as a list of entries
; test/alist; see sublis-tests-rev) and the testsi; and the calls, as the union
; of the top-calls and the callsi.
; We can visualize the above discussion by forming a sort of matrix as follows.
; The columns (which need not all have the same length) are the elements of
; tacs-lst-lst; typically, for some call of a function in names, each column
; contains the tests-and-calls records formed from an argument of that call
; using induction-machine-for-fn1. A "path", as discussed above, is formed by
; picking one record from each column. The order of records in the result is
; probably not important, but it seems reasonable to give priority to the
; records from the first argument by starting with all paths containing the
; first record of the first argument; and so on.
; Note that the records are in the desired order for each list in tacs-lst-lst,
; but are in reverse order for top-test-alist, and also tacs-lst-lst is in
; reverse order, i.e., it corresponds to the arguments of some function call
; but in reverse argument order.
; For any tests-and-calls record: we view the tests as their conjunction, we
; view the calls as specifying substitutions, and we view the measure formula
; as the implication specifying that the substitutions cause an implicit
; measure to go down, assuming the tests. Logically, we want the resulting
; list of tests-and-calls records to have the following properties.
; - Coverage: The disjunction of the tests is provably equivalent to the
; conjunction of the tests in top-test-alist.
; - Disjointness: The conjunction of any two tests is provably equal to nil.
; - Measure: Each measure formula is provable.
; We assume that each list in tacs-lst-lst has the above three properties, but
; with top-test-alist being the empty list (that is, with conjunction of T).
; It's not clear as of this writing that Disjointness is necessary. The others
; are critical for justifying the induction schemes that will ultimately be
; generated from the tests-and-calls records.
; (One may imagine an alternate approach that avoids taking this sort of cross
; product, by constructing induction schemes with inductive hypotheses of the
; form (implies (and <conjoined_path_of_tests> <calls_for_that_path>)). But
; then the current tests-and-calls data structure and corresponding heuristics
; would have to be revisited.)
(let ((full-tacs-lst-lst
(append tacs-lst-lst
(list
(list (make tests-and-calls
:tests (sublis-tests-rev top-test-alist nil)
:calls (all-calls-test-alist names
top-test-alist
top-calls)))))))
(cross-tests-and-calls1
(cdr full-tacs-lst-lst)
(car full-tacs-lst-lst))))
(mutual-recursion
(defun induction-machine-for-fn1 (names body alist test-alist calls
ruler-extenders merge-p)
; At the top level, this function builds a list of tests-and-calls for the
; given body of a function in names, a list of all the mutually recursive fns
; in a clique. 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. As we recur, we are considering body/alist, with accumulated tests
; consisting of test/a for test (test . a) in test-alist (but see :no-calls
; below, treated as the nil alist), and accumulated calls (already
; instantiated).
; To understand this algorithm, let us first consider the case that there are
; no lambda applications in body, which guarantees that alist will be empty on
; every recursive call, and ruler-extenders is nil. We explore body,
; accumulating into the list of tests (really, test-alist, but we defer
; discussion of the alist aspect) as we dive: for (if x y z), we accumulate x
; as we dive into y, and we accumulate the negation of x as we dive into z.
; When we hit a term u for which we are blocked from diving further (because we
; have encountered other than an if-term, or are diving into the first argument
; of an if-term), we collect up all the tests, reversing them to restore them
; to the order in which they were encountered from the top, and we collect up
; all calls of functions in names that are subterms of u or of any of the
; accumulated tests. From the termination analysis we know that assuming the
; collected tests, the arguments for each call are suitably smaller than the
; formals of the function symbol of that call, where of course, for a test only
; the tests superior to it are actually necessary.
; There is a subtle aspect to the handling of the tests in the above algorithm.
; To understand it, consider the following example. Suppose names is (f), p is
; a function symbol, 'if is in ruler-extenders, and body is:
; (if (consp x)
; (if (if (consp x)
; (p x)
; (p (f (cons x x))))
; x
; (f (cdr x)))
; x)
; Since 'if is in ruler-extenders, termination analysis succeeds because the
; tests leading to (f (cons x x)) are contradictory. But with the naive
; algorithm described above, when we encounter the term (f (cdr x)) we would
; create a tests-and-calls record that collects up the call (f (cons x x)); yet
; clearly (cons x x) is not smaller than the formal x under the default measure
; (acl2-count x), even assuming (consp x) and (not (p (f (cons x x)))).
; Thus it is unsound in general to collect all the calls of a ruling test when
; 'if is among the ruler-extenders. But we don't need to do so anyhow, because
; we will collect suitable calls from the first argument of an 'if test as we
; dive into it, relying on cross-tests-and-calls to incorporate those calls, as
; described below. We still have to note the test as we dive into the true and
; false branches of an IF call, but that test should not contribute any calls
; when the recursion bottoms out under one of those branches.
; A somewhat similar issue arises with lambda applications in the case that
; :lambdas is among the ruler-extenders. Consider the term ((lambda (x) (if
; <test> <tbr> <fbr>)) <arg>). With :lambdas among the ruler-extenders, we
; will be diving into <arg>, and not every call in <arg> may be assumed to be
; "smaller" than the formals as we are exploring the body of the lambda. So we
; need to collect up the combination of <test> and an alist binding lambda
; formals to actuals (in this example, binding x to <arg>, or more generally,
; the instantiation of <arg> under the existing bindings). That way, when the
; recursion bottoms out we can collect calls explicitly in that test (unless
; 'if is in ruler-extenders, as already described), instantiating them with the
; associated alist. If we instead had collected up the instantiated test, we
; would also have collected all calls in <arg> above when bottoming out in the
; lambda body, and that would be a mistake (as discussed above, since not every
; call in arg is relevant).
; So when the recursion bottoms out, some tests should not contribute any
; calls, and some should be instantiated with a corresponding alist. As we
; collect a test when we recur into the true or false branch of an IF call, we
; thus actually collect a pair consisting of the test and a corresponding
; alist, signifying that for every recursive call c in the test, the actual
; parameter list for c/a is known to be "smaller" than the formals. If
; ruler-extenders is the default, then all calls of the instantiated test are
; known to be "smaller", so we pair the instantiated test with nil. But if 'if
; is in the ruler-extenders, then we do not want to collect any calls of the
; test -- as discussed above, cross-tests-and-calls will take care of them --
; so we pair the instantiated test with the special indicator :no-calls.
; The merge-p argument concerns the question of whether exploration of a term
; (if test tbr fbr) should create two tests-and-calls records even if there are
; no recursive calls in tbr or fbr. For backward compatibility, the answer is
; "no" if we are exploring according to the conventional notion of "rulers".
; But now imagine a function body that has many calls of 'if deep under
; different arguments of some function call. If we create separate records as
; in the conventional case, the induction scheme may explode when we combine
; these cases with cross-tests-and-calls -- it will be as though we clausified
; even before starting the induction proof proper. But if we avoid such a
; priori case-splitting, then during the induction proof, it is conceivable
; that many of these potential separate cases could be dispatched with
; rewriting, thus avoiding so much case splitting.
; So if merge-p is true, then we avoid creating tests-and-calls records when
; both branches of an IF term have no recursive calls. We return (mv flag
; tests-and-calls-lst), where if merge-p is true, then flag is true exactly
; when a call of a function in names has been encountered. For backward
; compatibility, merge-p is false except when we the analysis has taken
; advantage of ruler-extenders. If merge-p is false, then the first returned
; value is irrelevant.
; Note: Perhaps some calls of reverse can be omitted, though that might ruin
; some regressions. Our main concern for replayability has probably been the
; order of the tests, not so much the order of the calls.