-
Notifications
You must be signed in to change notification settings - Fork 0
/
defuns.lisp
12719 lines (11161 loc) · 565 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.6 -- A Computational Logic for Applicative Common Lisp
; Copyright (C) 2024, 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")
; Essay on Cert-data
; In February 2016, Jared Davis requested on behalf of Centaur Technology
; Inc. that we avoid recomputing runic type-prescriptions when including
; certified books. There were two problems: type-prescription rules from an
; earlier included book were sometimes causing horrendous slowdowns in those
; computations while including a later book; and, we can lose nice
; type-prescriptions that were inferred during the proof (first) pass of
; certify-book using local rules, where a similar problem can occur with
; encapsulate.
; In March 2016 we solved these problems by introducing "cert-data" structures,
; which can be stored in certificates or in the state global variable
; 'cert-data. In January 2020 we added cert-data structures for storing the
; results of translation, specifically, of translating bodies of defun(s) and
; defthm events. The new record structure was introduced as
; translate-cert-data-record; see its defrec form for comments. Thus,
; cert-data stores information on runic type-prescriptions as well as results
; from translating defun and defthm bodies. Some day we might save other
; information that could be expensive to recompute.
; The rest of this Essay is in three parts. First, we introduce some general
; notions. Second, we focus on cert-data structures for computing runic type
; prescriptions. Finally, we discuss cert-data structures for avoiding
; re-translation at include-book time, at least for definitions and theorems.
; Part 1: General Notions
; One of the fields in a .cert file is a :CERT-DATA field, which is an alist
; mapping keys to fast-alists. As of this writing there are two keys:
; :TYPE-PRESCRIPTION and :TRANSLATE. Each of the two fast-alists (for the two
; keys) is called a "cert-data entry". See for example cert-data-fal, which
; takes a :cert-data field value from a certificate and creates an alist
; mapping each of the two keys to a cert-data entry (which is a fast-alist).
; (cert-data-fal is normally the identity function, but if the .cert file is
; written without the serialize writer then cert-data-fal serves to create a
; fast-alist to associate with each of those keys.)
; Each of the two entries is a fast-alist whose keys are symbols. In the case
; of a :type-prescription entry, each key is a function symbol whose associated
; value is a type-prescription record. In the case of a :translate entry, each
; key is an event name (currently, a function symbol or the name of a defthm
; event) that is associated with a list of translate-cert-data-record records.
; Note added 7/2022: We have observed that for a book's portcullis commands,
; :CERT-DATA is included for type-prescriptions but not for translations. This
; distinction may well have been unintentional, but it seems harmless. We see
; no reason why the stored type prescriptions for portcullis commands are
; problematic, and since we do not generally expect many defun or defthm events
; among the portcullis commands (other than those evaluated within include-book
; commands), there is little to be lost by ignoring saved translation
; information for these. This distinction in what is stored as cert-data for
; portcullis commands is a byproduct of our process: translation cert-data is
; determined while processing events under certify-book, while
; type-prescription cert-data is determined at the conclusion of such
; processing; see cert-data-for-certificate. To see this distinction, let
; foo.lisp be any trivial book and execute the following commands.
; (defun f1 (x) x) (local (defun f2 (x) x)) (defun g (x) x)
; (certify-book "foo" ?)
; (read-file "foo.cert" state)
; We see that the :CERT-DATA in foo.cert has :TYPE-PRESCRIPTION entries for f1
; and f3, but has no :TRANSLATE entries.
; Part 2: Type Prescriptions
; The following processes support the effective re-use of runic type
; prescriptions.
; (1) When including a certified book, all functions defined at the top level
; (i.e., not inside sub-books) get their runic type-prescriptions (if any)
; from the .cert file -- more specifically, from the value of state global
; 'cert-data, which is bound to the value from the .cert file.
; (2) Runic type-prescriptions are saved after pass1 of certify-book and
; encapsulate. For each :logic-mode defun processed in the second pass at
; the top level (not in an included sub-book), an "intersection" is taken
; of the runic type-prescription from the first pass and the computed runic
; type-prescription computed in the usual way. Note that since a function
; can be defined locally in a locally included book during the first pass
; but in a later defun at the top level in the second pass (which was
; redundant in the first pass), we even save some runic type-prescriptions
; from functions introduced during the first pass that were not introduced
; at the top level.
; Clearly each such rune is a logical consequence of the first pass; hence,
; by conservativity, it is a logical consequence of the second pass. Note
; that we may need to recompute the :corollary, which otherwise might not
; be a term of the theory produced by the second pass.
; (3) The runic type-prescription written to a .cert file is the one that
; exists after the second pass. We save such a rule for every function
; that could be introduced when including the book, which includes the
; top-level portcullis functions and every function introduced by the book
; (even those not processed during pass 2). Function
; newly-defined-top-level-fns provides this information; happily, even
; before we added support for cert-data, that function was already called
; under certify-book-fn to compute a list of function symbols to pass to
; write-expansion-file.
; Now we elaborate on these processes.
; Note that including an already-certified book gives you the specific type
; prescription from the .cert file. If however a book B1 includes another book
; B2 only locally, then the type-prescription computed for B1 might be stronger
; than that from B2, because of our "intersection" of rules in (2) above.
; Suppose we are to determine the runic type-prescription for a given defun.
; If state global 'cert-data has value nil, then we just do the usual iterative
; calculation. Otherwise we are to use that cert-data; but how do we know that
; we should do the "intersection" operation because we are in the pass 2 case,
; described in (2) above? We bind key :pass1-saved to t in the value of state
; global 'cert-data during the second pass (meaning, cert-data is from pass 1).
; If necessary we could have non-nil values that provide more information than
; t, for example, 'acl2::certify-book or 'acl2::encapsulate. We don't bother
; to bind :pass1-saved to nil for other than pass 2; we simply don't bind
; :pass1-saved.
; In (2) above we describe the saving of runic type-prescriptions to use during
; the second pass. In the case of certify-book, however, we do this only for
; the part of the world not in the retraction after pass 1, since there is no
; need to save information for defuns already processed before starting pass 2.
; Why do we need the "intersection" operation described in (2) above? That is,
; why not just pick either the runic type-prescription from the first pass or
; compute one for the second pass? The answer is that either may be weaker
; than desired, as illustrated by the following two examples. (These examples
; are for encapsulate, but certify-book has the same issue.)
; (2a) First, here is an example showing that the second pass can do a better
; job computing the runic type-prescription than the first pass. (To see the
; empty 'type-prescriptions we would get for FOO on the first pass, change
; (encapsulate () ...) to (progn ...).)
; (encapsulate
; ()
; (local (include-book "rtl/rel9/support/support/lnot" :dir :system))
; ; Because of the following in-theory event, the cert-data from the first pass
; ; associates no runic type-prescription with FOO.
; (local (in-theory nil))
; (defun fl (x)
; (declare (xargs :guard (real/rationalp x)))
; (floor x 1))
; (defun bits (x i j)
; (declare (xargs :guard (and (natp x) (natp i) (natp j))
; :verify-guards nil))
; (mbe :logic (if (or (not (integerp i))
; (not (integerp j)))
; 0
; (fl (/ (mod x (expt 2 (1+ i))) (expt 2 j))))
; :exec (if (< i j)
; 0
; (logand (ash x (- j))
; (1- (ash 1 (1+ (- i j))))))))
; (defun lnot (x n)
; (declare (xargs :guard (and (natp x) (integerp n) (< 0 n))
; :verify-guards nil))
; (if (natp n)
; (+ -1 (expt 2 n) (- (bits x (1- n) 0)))
; 0))
; (defun foo (x n)
; (lnot x n)))
; ; Using cert-data from the first pass only:
; ; (assert-event (null (getpropc 'foo 'type-prescriptions)))
; ; Computing the runic type-prescription in the second pass:
; (assert-event
; (equal (decode-type-set
; (access type-prescription
; (car (last (getpropc 'foo 'type-prescriptions)))
; :basic-ts))
; '*ts-rational*)
; What we actually get, now, is *ts-integer*, because that's the :basic-ts for
; the runic type-prescription of lnot (and also of binary-logand, bits, and fl)
; from the locally included book, saved from the first pass.
; (2b) To obtain an example showing that the first pass can do a better job
; computing the runic type-prescription than the second pass, simply omit
; (in-theory nil) from the example above. The second pass still gives us
; *ts-rational, as above; but if we change (encapsulate () ...) to (progn ...),
; we see:
; (assert-event
; (equal (decode-type-set
; (access type-prescription
; (car (last (getpropc 'foo 'type-prescriptions)))
; :basic-ts))
; '*ts-non-negative-integer*))
; Let's turn now to our handling of a few thorny issues.
; Suppose we are certifying a book with an encapsulate that locally defines a
; function, f, such that later in the book is a different, non-local definition
; of f. At the end of pass 1 of certify-book we will store a runic type
; prescription for the second definition. Then during pass 2 of certify-book,
; might we make a mistake by associating that type-prescription with the first
; (local) definition of f? No, because local definitions are skipped during
; pass 2. But for robustness, we pass a value for cert-data to
; process-embedded-events, which binds state global cert-data to that value.
; Thus, we override the global cert-data when we process an encapsulate.
; The expansion phase of make-event introduces definitions that are in effect
; local. As in the preceding paragraph, we need to avoid applying the global
; cert-data to such definitions. This problem is solved primarily by arranging
; that protected-eval, via protect-system-state-globals, binds state global
; cert-data to nil. An additional binding of cert-data to nil is made before
; calling make-event-fn2-lst, which handles :OR forms and thus can throw away
; earlier values. In such a case, the runic type-prescription will be
; recomputed during include-book, but we think that such an exception is
; tolerable.
; We are careful to not use cert-data for non-trivial encapsulates. It might
; well be possible to do so correctly, but we would need to be very careful to
; track constraints properly; it seems easy to have a soundness bug due to
; recording insufficient constraints in pass 2 to justify deductions made from
; stronger constraints in pass 1.
; A runic type-prescription rule may contain symbols not present in the
; certification world, as shown below. A similar issue applies to the
; :expansion-alist field of the certificate, which is addressed by finding the
; problematic package names with pkg-names introducing hidden defpkg forms. We
; use that same solution for cert-data. The following example shows how this
; works. First, let's look at a couple of books; notice the package definition
; that is to be made in the certification world of the first book.
; $ cat sub.lisp
; ; (defpkg "FOO" nil)
; ; (certify-book "sub" 1)
;
; (in-package "ACL2")
;
; (defun f2 (x) x)
; $ cat top.lisp
; (in-package "ACL2")
;
; (include-book "sub")
;
; (defmacro my-def ()
; `(defun f (,(intern$ "X" "FOO")) ,(intern$ "X" "FOO")))
;
; (my-def)
; $
; After certification of both books, the :CERT-DATA field of top.cert has the
; following value.
; ((:TYPE-PRESCRIPTION (F 0 (3413 F FOO::X)
; (NIL)
; ((FOO::X) :TYPE-PRESCRIPTION F)
; EQUAL (F FOO::X)
; FOO::X)))
; Thus, a hidden defpkg is generated (here we abbreviate the directory as
; <dir>).
; :BEGIN-PORTCULLIS-CMDS
; (DEFPKG "FOO" NIL NIL
; ("<dir>/sub.lisp")
; T)
; :END-PORTCULLIS-CMDS
; Part 3: Translate
; During the first pass of certify-book, an alist is built up as the value of
; the world global, 'translate-cert-data. (See update-translate-cert-data.)
; This alist will ultimately be the value stored in the :translate entry of the
; :cert-data field of the book's certificate, after making it into a
; fast-alist. When including a book, that field will be the value of the
; cert-data given to process-embedded-events in include-book-fn1.
; That fast-alist will be stored in state global 'cert-data during
; include-book. In order for it to be valid (when consulted via the calls of
; get-translate-cert-data-record), we use function store-cert-data to decide
; when to store into the world global, 'translate-cert-data. We must skip
; results of translation computed on behalf of local events, which will of
; course be irrelevant (or even misleading) when later including the book. We
; also need to skip translations computed during make-event expansion, but that
; happens automatically because we are recording the results in a world global
; and the world is reverted after make-event expansion. We also take other
; measures in store-cert-data. In particular, we sometimes avoid storing
; results computed during the first pass of an encapsulate (which is skipped
; during include-book), though that is not necessary since the world is rolled
; back after that pass -- and note that we don't want to use pass1 encapsulate
; results to avoid translating in pass2, because that would avoid local
; incompatibility checking. (For the same reason, we don't retrieve :translate
; cert-data during the include-book phase of certify-book.) Also, we avoid
; worrying about lambda objects. See store-cert-data for details.
; Remarks (in no particular order).
; (1) We considered explicitly avoiding storing translation results from inside
; progn!, simply because of the unbounded flexibility of progn!. But we view
; it unlikely that progn! would cause a problem, since the only truly obvious
; way to build a confusing cert-data entry (alist) for the :translate key seems
; to be to use redefinition, in which case we write an empty :translate entry
; into the certificate (see cert-data-for-certificate); and besides, progn!
; requires a trust tag, so we are sort of off the hook as far as weird end
; cases are concerned.
; (2) One can certify books in community books directory
; books/system/tests/cert-data/ and look at their certificates with (read-file
; "<bookname>.cert" state), to see the :cert-data field for each book. For
; example, the function f1 in top1.lisp and top1a.lisp is redundant with a
; function in an earlier-included book, so its translated body is not stored in
; the corresponding .cert file; but including top1a.lisp does use the
; translated body when including the sub-book, sub1.lisp.
; (3) We are careful not to retrieve translated terms during make-event
; expansion or other uses of protect-system-state-globals, by binding state
; global cert-data to nil in protect-system-state-globals.
; (4) There could be a very few cases where the saved :translate cert-data
; makes include-book a bit more permissive than it would be otherwise,
; especially if trust tags are involved, though we have tried to minimize this.
; An example is that for flet, translate disallows binding a symbol that is
; also bound in the return-last-table. But since translation was OK at
; certify-book time, we don't mind using the same translation at include-book
; time. Another case is when functions called during macroexpansion (within
; translation) are untouchable when including a book on top of a non-trivial
; world; we don't check for that, though we do check for untouchables in the
; translated terms before retrieval. Another case: We don't re-run calls of
; translate-and-test.
; (5) We have considered saving more translation results. But so far,
; profiling has suggested, using (include-book "centaur/sv/top" :dir :system),
; that the only non-trivial benefit might be in saving results of translating
; event forms. This would presumably involve honsing the (untranslated)
; events, as keys; and we haven't thought through what additional work might be
; necessary (for example, we ignored the case (eq stobjs-out :stobjs-out) in
; translate11 because that shouldn't apply for defun or defthm). Profiling
; suggests that we already lose significant potential speed-up simply by having
; to read larger .cert files, and that problem would be even greater if keys
; are events instead of symbols. (Or maybe we can use the cadr of some event
; forms as symbols?... lots to think about.) Another potential issue is added
; complexity from how trans-eval handles IF lazily, rather than translating the
; entire form at once. So our initial work on :translate cert-data in January,
; 2020, is only for translation of defun(s) and defthm bodies.
; (6) Because of our calls of make-fast-alist in the definition of the function
; cert-data-fal, it is unnecessary to store cert-data entries as fast-alists
; in the .cert file. But profiling has suggested that it is harmless to do so.
; The type-prescription cert-data is already a fast-alists anyhow; we'd have to
; free it if we want to avoid storing it as a fast-alist.
; (7) As a sort of optimization, saving space in .cert files at the expense of
; time: we could perhaps loosen the cons-count-bounded restriction in
; store-cert-data by finding all constant symbols' values in the untranslated
; input and doing a sublis to re-insert those symbols in the translated code,
; and then use sublis in the other direction upon retrieval.
; (8) Note that certain tests for ttags in translate11, such as (assoc-eq fn
; *ttag-fns*), aren't a problem. That's because if a trust tag is active at a
; given non-local event during book certification, then it's still active at
; include-book time, since that could only be defeated by inclusion of a
; sub-book, but ttag settings in a sub-book are local to that sub-book.
(defun cert-data-pair (fn cert-data-entry)
; Cert-data-entry is (cdr (assoc-eq key cert-data)) for some key, e.g., for the
; key, :type-prescription.
(and cert-data-entry ; optimization
(hons-get fn cert-data-entry)))
(defun cert-data-val (fn cert-data-entry)
; Cert-data-entry is (cdr (assoc-eq key cert-data)) for some key, e.g., for the
; key, :type-prescription.
(let ((pair (and cert-data-entry ; optimization
(hons-get fn cert-data-entry))))
(cdr pair)))
(defun cert-data-entry-pair (key state)
; Key is :type-prescription or any other keyword that can be associated in a
; cert-data structure with an entry.
(let ((cert-data (f-get-global 'cert-data state)))
(and cert-data ; optimization
(assoc-eq key cert-data))))
(defun cert-data-entry (key state)
; Key is :type-prescription, :defthm, or any other keyword that can be
; associated in a cert-data structure with an entry. We return a valid
; cert-data entry or nil. Note that cert-data entries are not valid in a local
; or make-event context. See the Essay on Cert-data.
(let ((cert-data (f-get-global 'cert-data state)))
(and cert-data ; optimization
(not (f-get-global 'in-local-flg state))
(int= (f-get-global 'make-event-debug-depth state) 0)
(cdr (assoc-eq key cert-data)))))
(mutual-recursion
(defun contains-lambda-objectp (x)
; This function returns true when the input contains a quoted lambda.
(declare (xargs :guard (pseudo-termp x)))
(cond ((atom x) nil)
((eq (car x) 'quote)
(let ((u (unquote x)))
(and (consp u)
(eq (car u) 'lambda))))
(t (or (contains-lambda-object-listp (cdr x))
(and (flambda-applicationp x)
(contains-lambda-objectp (lambda-body (car x))))))))
(defun contains-lambda-object-listp (x)
(declare (xargs :guard (pseudo-term-listp x)))
(cond ((endp x) nil)
(t (or (contains-lambda-objectp (car x))
(contains-lambda-object-listp (cdr x))))))
)
(defun store-cert-data (listp val wrld state)
; Listp is true when val is a list of terms, false when val is a term.
(and (f-get-global 'certify-book-info state)
(not (f-get-global 'in-local-flg state))
(not ; not inside include-book
(global-val 'include-book-path wrld))
; The next conjunct is optional, as explained in the Essay on Cert-data.
(not ; not "obviously" in encapsulate pass1
(and (in-encapsulatep (global-val 'embedded-event-lst wrld) nil)
(not (eq (ld-skip-proofsp state) 'include-book))))
; The following check may be needlessly conservative. It addresses the
; following concern: translation of quoted lambdas is complicated by
; considerations involving apply$ and loop$. For example, untouchable function
; symbols inside such a quoted object might be a concern -- though probably
; not, since we don't seem to allow function symbols to be both badged and
; untouchable. Rather than think through such issues, we simply skip all
; quoted lambdas. If the need arises, one can look into removing this
; restriction.
(not (if listp
(contains-lambda-object-listp val)
(contains-lambda-objectp val)))
; The following heuristic check could be reconsidered. It is intended to keep
; .cert files from being too big.
(< (cons-count-bounded val)
(fn-count-evg-max-val))))
(defrec translate-cert-data-record
; Warning: Keep the fields in sync with update-translate-cert-data and
; cert-data-for-certificate.
; The form of inputs and value depends on type.
; - For translate-bodies: inputs is the names argument to translate-bodies
; and value is (cons tbodies bindings), where tbodies is the list of
; translated bodies and bindings is the corresponding bindings from
; translate.
; - For defthm: inputs is the name
; and value is the translated body (without making an adjustment for
; ACL2(r)).
((type . inputs) . (value . (fns . vars)))
t)
(defun update-translate-cert-data-fn (name installed-wrld wrld type inputs
value fns vars)
(let* ((old-translate-cert-data (global-val 'translate-cert-data
installed-wrld))
(new (make translate-cert-data-record
:type type
:inputs inputs
:value value
:fns fns
:vars vars))
(old-lst (cdr (assoc-eq name old-translate-cert-data))))
(global-set 'translate-cert-data
(acons name
(cons new old-lst)
old-translate-cert-data)
wrld)))
(defmacro update-translate-cert-data (name installed-wrld wrld
&key type inputs value fns vars)
; Warning: Keep the fields in sync with translate-cert-data-record and
; cert-data-for-certificate.
`(update-translate-cert-data-fn ,name ,installed-wrld ,wrld
,type ,inputs ,value ,fns ,vars))
; 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 arglists
stobjs-in-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)
(collect-non-*-df (car stobjs-in-lst))
(collect-by-position '(:df)
(car stobjs-in-lst)
(car arglists))
(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 arglists)
(cdr stobjs-in-lst)
ctx wrld state-vars))
(x (translate1-cmp+ (car bodies)
(if non-executablep t (car names))
(if non-executablep nil bindings)
(collect-non-*-df (car stobjs-in-lst))
(collect-by-position '(:df)
(car stobjs-in-lst)
(car arglists))
(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 arglists)
(cdr stobjs-in-lst)
ctx wrld state-vars)))
(trans-value (cons x y))))))))))
(defun chk-non-executable-bodies (names arglists bodies non-executablep
mut-rec-p 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 mut-rec-p ctx state))
(t (er soft ctx
"The body of a defun that is marked :non-executable ~
(perhaps implicitly, by the use of defun-nx~@1) must ~
be of the form (prog2$ (throw-nonexec-error ...) ~
...)~@2. The definition of ~x0 is thus illegal. ~
See :DOC defun-nx."
(car names)
(if mut-rec-p
" in some definition under the mutual-recursion"
"")
(if (eq non-executablep :program)
""
", as is laid down by defun-nx"))))))))
(defun collect-untouchable-fns (syms state)
(let ((temp-touchable-fns (f-get-global 'temp-touchable-fns state)))
(cond ((eq temp-touchable-fns t) nil)
(t (let* ((wrld (w state)) ; installed world
(untouchable-fns (global-val 'untouchable-fns wrld))
(int (intersection-eq syms untouchable-fns)))
(cond (temp-touchable-fns
(set-difference-eq int temp-touchable-fns))
(t int)))))))
(defun collect-untouchable-vars (syms state)
(let ((temp-touchable-vars (f-get-global 'temp-touchable-vars state)))
(cond ((eq temp-touchable-vars t) nil)
(t (let* ((wrld (w state)) ; installed world
(untouchable-vars (global-val 'untouchable-vars wrld))
(int (and syms ; optimization
(intersection-eq syms untouchable-vars))))
(cond (temp-touchable-vars
(set-difference-eq int temp-touchable-vars))
(t int)))))))
(defun get-translate-cert-data-record (type lst state)
; Lst is a list of translate-cert-data-record records associated with a single
; name. We return the unique one associated with type, if any, else nil.
; Reasons for returning nil include:
; (a) two or more relevant records (which would necessarily be distinct; see
; update-translate-cert-data);
; (b) function symbols in the translated term that are now untouchable; or
; (c) state global symbols in the translated term, assigned or made unbound,
; that are now untouchable.
(cond ((endp lst) nil)
((eq type (access translate-cert-data-record (car lst) :type))
(cond ((or (get-translate-cert-data-record type (cdr lst) state) ; (a)
(collect-untouchable-fns
(access translate-cert-data-record (car lst) :fns)
state) ; (b)
(collect-untouchable-vars
(access translate-cert-data-record (car lst) :vars)
state)) ; (c)
nil)
(t (car lst))))
(t (get-translate-cert-data-record type (cdr lst) state))))
(defun get-translate-bodies (names cert-data-entry state)
; Cert-data-entry is a valid cert-data entry for the :translate key. It is
; thus a list of translate-cert-data-record records. We return nil or else the
; unique bodies associated with names, checking for untouchables.
(cond ((null names) ; probably always false, but we check, for robustness
nil)
(t (let ((lst (cert-data-val (car names) cert-data-entry)))
(cond
((null lst) ; optimization
nil)
(t (let ((val (get-translate-cert-data-record :translate-bodies
lst
state)))
(and val
(assert$ (equal (access translate-cert-data-record val
:inputs)
names)
(access translate-cert-data-record val
:value))))))))))
(defun translate-bodies (non-executablep names arglists bodies bindings0
stobjs-in-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.
; Normally, this function is called with bindings0 = (pairlis$ names names),
; which indicates that the output signature of each name must be inferred
; during translation and stored in the ultimate value of bindings. But when
; :loop$-recursion is specified, the caller already knows the output signature
; of the fn being defined and will specify it in the call.
(declare (xargs :guard (true-listp bodies)))
(let ((cert-data-entry (cert-data-entry :translate state)))
(let ((cert-data-tbodies-and-bindings
(if cert-data-entry
; Note that we do not need to rule out make-event expansion explicitly, because
; it is already being ruled out: protect-system-state-globals (called by
; protected-eval, which does the evaluation for make-event expansion) binds
; state global 'cert-data to nil.
(get-translate-bodies names cert-data-entry state)
nil)))
(cond
(cert-data-tbodies-and-bindings (value cert-data-tbodies-and-bindings))
(t
(mv-let (erp lst bindings)
(translate-bodies1 (eq non-executablep t) ; not :program
names bodies
bindings0 arglists
stobjs-in-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 "Translate" "~@0" lst))
(non-executablep
(chk-non-executable-bodies names arglists lst
non-executablep (cdr names)
ctx state))
(t (value nil)))
(value (cons lst
(cond ((eq non-executablep t)
(pairlis-x2 names '(nil)))
(t 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 symbol fn is called after replacing each
; mbe call in term by its :logic component. Keep this in sync with the
; ffnnamep nest. Unlike ffnnamep, we assume here that fn is a symbolp.
(declare (xargs :guard (and (symbolp fn)
(pseudo-termp term))))
(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 (loop$-recursion-checkedp
loop$-recursion
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.
; When loop$-recursion is t, we know names is a singleton and that the function
; is indeed recursive. Otherwise, we use ffnnamep-mod-mbe to determine whether
; a singly defined function is recursive.
; 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.
(prog2$
(choke-on-loop$-recursion loop$-recursion-checkedp
names
bodies
'putprop-recursivep-lst)
(cond (loop$-recursion
(putprop (car names) 'recursivep names wrld))
((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)