-
Notifications
You must be signed in to change notification settings - Fork 1
/
translate.lisp
19615 lines (16875 loc) · 867 KB
/
translate.lisp
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
; ACL2 Version 8.4 -- A Computational Logic for Applicative Common Lisp
; Copyright (C) 2020, 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")
(mutual-recursion
(defun termp (x w)
(declare (xargs :guard (plist-worldp-with-formals w)))
(cond ((atom x) (legal-variablep x))
((eq (car x) 'quote)
(and (consp (cdr x))
(null (cddr x))))
((symbolp (car x))
(let ((arity (arity (car x) w)))
(and arity
(term-listp (cdr x) w)
(eql (length (cdr x)) arity))))
((and (consp (car x))
(true-listp (car x))
(eq (car (car x)) 'lambda)
(eql 3 (length (car x)))
(arglistp (cadr (car x)))
(termp (caddr (car x)) w)
(null (set-difference-eq
(all-vars (caddr (car x)))
(cadr (car x))))
(term-listp (cdr x) w)
(eql (length (cadr (car x)))
(length (cdr x))))
t)
(t nil)))
(defun term-listp (x w)
(declare (xargs :guard (plist-worldp-with-formals w)))
(cond ((atom x) (equal x nil))
((termp (car x) w) (term-listp (cdr x) w))
(t nil)))
)
(defun term-list-listp (l w)
(declare (xargs :guard (plist-worldp-with-formals w)))
(if (atom l)
(equal l nil)
(and (term-listp (car l) w)
(term-list-listp (cdr l) w))))
(defun computed-hint-tuple-listp (x wrld)
(cond
((consp x)
(let ((tuple (car x)))
(and (true-listp tuple)
(eq (car tuple) 'EVAL-AND-TRANSLATE-HINT-EXPRESSION)
(booleanp (caddr tuple))
(termp (cadddr tuple) wrld)
(computed-hint-tuple-listp (cdr x) wrld))))
(t (null x))))
(table default-hints-table nil nil
:guard
(case key
((t) (true-listp val))
(:override (computed-hint-tuple-listp val world))
(t nil)))
(table default-hints-table nil nil :clear)
(defun macro-args (x w)
(declare (xargs :guard (and (symbolp x) (plist-worldp w))))
(getpropc x 'macro-args
'(:error "We thought macro-args was only called if there were ~
(zero or more) macro-args.")
w))
(defconst *macro-expansion-ctx* "macro expansion")
(defun error-trace-suggestion (two-leading-spaces)
; Warning: Do not eliminate the message about print-gv without first reading
; the comment about it in ev-fncall-guard-er-msg.
(declare (xargs :mode :program))
(msg "~s0To debug see :DOC print-gv, see :DOC trace, and see :DOC wet."
(if two-leading-spaces
" "
"")))
(defun ignored-attachment-msg (ignored-attachment)
(cond (ignored-attachment (msg "~|~%Note that because of logical ~
considerations, attachments (including ~x0) ~
must not be called in this context. See ~
:DOC ignored-attachment."
ignored-attachment))
(t "")))
(defun ev-fncall-null-body-er-msg (ignored-attachment fn args)
(cond
((eq fn :non-exec)
; This is a special case for calls of (non-exec form), where in this case, args
; is form.
(assert$
(null ignored-attachment) ; This case has nothing to do with attachments.
(msg "ACL2 has been instructed to cause an error because of an attempt ~
to evaluate the following form (see :DOC non-exec):~|~% ~
~x0.~|~%~@1"
args ; actually, the form
(error-trace-suggestion nil))))
((consp fn)
; This is a special case for errors detected by the code that supports the
; evaluation (at the top-level of the ACL2 loop) of terms ancestrally dependent
; upon the constrained functions in the apply$ development. In particular, if
; (consp fn) is true -- which only happens when we're executing the attachments
; for those constrained functions -- then fn is the msg we're supposed to
; return. The basic idea is that those attachments detect a wide variety of
; errors and rather than produce a single generic error message (as we would do
; if this clause were eliminated) we let the caller formulate the message.
; Note: We could assert (msgp fn) but it is weaker than the assertion below.
(assert$
(and (stringp (car fn))
(alistp (cdr fn))) ; character-alistp isn't defined yet...
fn))
(t (msg "ACL2 cannot ev the call of non-executable function ~x0 on ~
argument list:~|~%~x1~@2~|~%~@3"
fn
args
(ignored-attachment-msg ignored-attachment)
(error-trace-suggestion nil)))))
(defun ev-fncall-null-body-erp (fn)
; Warning: Keep this in sync with hide-with-comment.
`(ev-fncall-null-body-er . ,fn))
(defun ev-fncall-null-body-er (ignored-attachment fn args latches)
(mv (ev-fncall-null-body-erp fn)
(ev-fncall-null-body-er-msg ignored-attachment fn args)
latches))
(defun ev-fncall-creator-er-msg (fn)
(msg
"An attempt has been made to call the stobj creator function ~x0. This ~
error is being reported even though guard-checking may have been turned ~
off, because ACL2 does not support non-compliant live stobj manipulation. ~
~ If you did not explicitly call ~x0 then this error is probably due to ~
an attempt to evaluate a with-local-stobj form directly in the top-level ~
loop. Such forms are only allowed in the bodies of functions and in ~
theorems. Also see :DOC with-local-stobj.~@1"
fn
(error-trace-suggestion t)))
(defun unknown-pkg-error-msg (fn pkg-name)
(msg
"The call ~x0 is illegal because the argument is not the name of a package ~
currently known to ACL2."
(list fn pkg-name)))
(defun illegal-msg ()
(msg "Evaluation aborted.~@0"
(error-trace-suggestion t)))
(defun program-only-er-msg (fn args safe-mode)
(msg
"The call ~x0~|is an illegal call of a function that has been marked as ~
``program-only,'' presumably because it has special raw Lisp code~@1. ~
See :DOC program-only for further explanation and a link to possible ~
workarounds."
(cons fn args)
(if safe-mode
" and safe-mode is active"
"")))
(defconst *safe-mode-guard-er-addendum*
; We could add, as a reason for using safe-mode, the application of
; magic-ev-fncall to :program-mode functions. But that might scare off
; beginners, and is sufficiently covered by "another operation">
" The guard is being checked because this function is a primitive and a ~
\"safe\" mode is being used for defconst, defpkg, macroexpansion, or ~
another operation where safe mode is required.")
(defun find-first-non-nil (lst)
(cond ((endp lst) nil)
(t (or (car lst)
(find-first-non-nil (cdr lst))))))
; For a discussion of stobj latching, see Stobj Latching below.
(defun latch-stobjs1 (stobjs-out vals latches)
(cond ((endp stobjs-out) latches)
((car stobjs-out)
(let ((temp (assoc-eq (car stobjs-out) latches)))
(cond
; Suppose (car stobjs-out) is some stobj, $st, and (car vals) is the
; new value, val. We wish to bind '$st in latches to val. It is an
; error if we can't find a binding for '$st. Otherwise, put-assoc-eq
; will do the job. But in the special, live, case, val is EQ to the
; current binding of '$st in latches, because all the objects are
; live. In this case, we can avoid the put-assoc-eq and just leave
; latches unchanged. The clause below is safe whether val is a live
; object or not: if it's the same thing as what is there, the
; put-assoc-eq won't change latches anyway. But the real intent of
; this clause is make the final value of latches, in general, EQ to
; the original value of latches.
((not temp)
(er hard! 'latch-stobjs
"We are trying to latch a value for the single-threaded ~
object named ~x0, but there is no entry for that name in ~
the stobj latches provided. The possible latch names are ~
~&1.~#2~[~/ This error most likely is caused by the ~
attempt to ev a form that is not ``supposed'' to mention ~
stobjs but does. Often when dealing with forms that are ~
not supposed to mention stobjs we call ev with last ~
argument NIL and then ignore the resulting latches.~]"
(car stobjs-out)
(strip-cars latches)
(if latches 0 1)))
((eq (cdr temp) (car vals))
; Two live stobjs are the same iff they are eq. This is kind of a cheat; see
; the comment about the use of rassoc-eq in actual-stobjs-out1.
(latch-stobjs1 (cdr stobjs-out)
(cdr vals)
latches))
(t
(latch-stobjs1 (cdr stobjs-out)
(cdr vals)
(put-assoc-eq (car stobjs-out)
(car vals)
latches))))))
(t (latch-stobjs1 (cdr stobjs-out)
(cdr vals)
latches))))
(defun latch-stobjs (stobjs-out vals latches)
; Update the latches so that it contains the stobj objects returned in
; val. Val is either a single value or a list of 2 or more values, as
; indicated by stobjs-out. If stobjs-out is nil it is treated as a
; list of as many nils as necessary and no change is made to val. If
; latches is nil, we do nothing. This means that we are not recording
; the ``current'' stobjs and one must be careful to obey the
; restrictions in the Essay on EV.
(cond ((null latches) latches)
((null stobjs-out) latches)
((null (cdr stobjs-out))
(cond ((car stobjs-out)
; We call latch-stobjs1 rather than put-assoc-eq to get the error check.
(latch-stobjs1 stobjs-out (list vals) latches))
(t latches)))
(t (latch-stobjs1 stobjs-out vals latches))))
(defun actual-stobjs-out1 (stobjs-in arg-exprs)
(declare (xargs :guard (and (symbol-listp stobjs-in)
(true-listp arg-exprs)
(= (length stobjs-in)
(length arg-exprs)))))
(cond ((endp stobjs-in)
(assert$ (null arg-exprs) nil))
(t (cond ((or (null (car stobjs-in))
(eq (car stobjs-in) 'state)
(eq (car stobjs-in) (car arg-exprs)))
(actual-stobjs-out1 (cdr stobjs-in) (cdr arg-exprs)))
(t (acons (car stobjs-in)
(car arg-exprs)
(actual-stobjs-out1 (cdr stobjs-in)
(cdr arg-exprs))))))))
(defun apply-symbol-alist (alist lst acc)
; Alist represents a function to apply to each element of lst, a list of
; symbols. (This function is the identity on elements not in the domain of
; alist.) The resulting list is accumulated into acc and reversed.
(cond ((endp lst) (reverse acc))
(t (apply-symbol-alist alist
(cdr lst)
(cons (let ((pair (assoc-eq (car lst) alist)))
(cond (pair (cdr pair))
(t (car lst))))
acc)))))
(defun apply-inverse-symbol-alist (alist lst acc)
; See apply-symbol-alist. Here, though, we apply the inverse of the mapping
; represented by alist. We assume that the cdrs of alist are suitable for
; testing with eq (i.e., symbols or stobjs).
(cond ((endp lst) (reverse acc))
(t (apply-inverse-symbol-alist
alist
(cdr lst)
(cons (let ((pair (rassoc-eq (car lst) alist)))
(cond (pair (car pair))
(t (car lst))))
acc)))))
(defun actual-stobjs-out (fn arg-exprs wrld)
(declare (xargs :guard (and (symbolp fn)
(not (member-eq fn *stobjs-out-invalid*))
(true-listp arg-exprs)
(plist-worldp wrld))))
(let ((stobjs-out (stobjs-out fn wrld)))
(cond ((all-nils stobjs-out) ; optimization for common case
stobjs-out)
(t (let ((stobjs-in (stobjs-in fn wrld)))
(let ((alist (actual-stobjs-out1 stobjs-in arg-exprs)))
(cond (alist (apply-symbol-alist alist stobjs-out nil))
(t stobjs-out))))))))
#-acl2-loop-only
(defvar **1*-as-raw*
; When a *1* function is called and this variable is true, that function should
; behave as its corresponding raw Lisp function, except that critical guards
; for stobj updaters are checked. We can live with that rather vague
; specification because this variable is nil unless we are under the call of a
; program mode function.
; For the sake of simplicity in the discussion below, we ignore the possibility
; that guard-checking is set to :none or :all and we ignore safe-mode. Also,
; we assume that the value of state global 'check-invariant-risk is non-nil, as
; should always be the case unless someone is hacking; otherwise, the effect of
; this variable is defeated.
; Oneify-cltl-code uses this variable, **1*-as-raw*, to arrange that when a
; *1* :logic-mode function that calls mbe is itself called under a *1*
; :program-mode function, then the :exec code of that mbe call is evaluated,
; not the :logic code. Our approach is basically as follows. Globally,
; **1*-as-raw* is nil. But we arrange the following, and explain below.
;
; (a) The *1* code for an invariant-risk :program mode function binds
; **1*-as-raw* to t.
;
; (b) The *1* code for an mbe call reduces to its *1* :exec code when
; **1*-as-raw* is true.
;
; (c) Raw-ev-fncall binds **1*-as-raw* to nil for :logic mode functions.
;
; (d) Oneify binds **1*-as-raw* to nil when ec-call is applied to a :logic
; mode function.
; Without invariant-risk, none of this would be necessary: a :program mode
; function call would lead to raw Lisp evaluation, where each mbe call
; macroexpands to its :exec code. But with invariant-risk, we need to stick
; with *1* execution in order to avoid making ill-guarded stobj updater calls,
; in which case (a) and (b) save us from execution of :logic code from an mbe
; call. Note that the use of :exec code from mbe calls can be important for
; performance, as pointed out by Jared Davis.
; To see why we need (c), consider the following example.
; (defstobj st (fld :type integer :initially 0))
;
; (defun lgc (st)
; (declare (xargs :mode :logic
; :stobjs st
; :verify-guards nil))
; (mbe :logic (prog2$ (cw "@@@LOGIC@@@~%")
; (update-fld 3 st))
; :exec (prog2$ (cw "@@@EXEC@@@~%")
; (update-fld 4 st))))
;
; (defun foo (state st)
; (declare (xargs :mode :program :stobjs (state st)))
; (let ((st (update-fld 7 st)))
; (mv-let (erp val state)
; (trans-eval
; '(thm (equal (with-local-stobj
; st
; (mv-let (val st)
; (let ((st (lgc st)))
; (mv (fld st) st))
; val))
; 4)) 'top state t)
; (mv erp val state st))))
; The proof should fail when calling (foo state st), since logically, the value
; of the with-local-stobj form is 3, not 4. But since foo has invariant-risk,
; **1*-as-raw* is bound to t when calling *1*foo, so we might expect that
; evaluation of the mbe form under (lgc st) would use the :exec form, leading
; erroneously to a successful proof! However, we bind **1*-as-raw* to nil in
; raw-ev-fncall precisely to avoid such a problem.
; To see why we need (d), see the example in a comment in oneify that starts
; with "(defun f-log".
nil)
(defun translated-acl2-unwind-protectp4 (term)
; This hideous looking function recognizes those terms that are the
; translations of (acl2-unwind-protect "expl" body cleanup1 cleanup2). The
; acl2-unwind-protect macro expands into an MV-LET and that MV-LET is
; translated in one of two ways, depending on whether or not the two cleanup
; forms are equal. We look for both translations. We return 4 results. The
; first is t or nil according to whether term is of one of the two forms. If
; nil, the other results are nil. If term is of either form, we return in the
; other three results: body, cleanup1 and cleanup2 such that term is equivalent
; to (acl2-unwind-protect "expl" body cleanup1 cleanup2).
; WARNING: This function must be kept in sync with the defmacro of
; acl2-unwind-protect, the translate1 clauses dealing with mv-let and let, and
; the defmacro of mv-let.
(case-match
term
((('LAMBDA (mv . vars)
(('LAMBDA ('ACL2-UNWIND-PROTECT-ERP
'ACL2-UNWIND-PROTECT-VAL 'STATE . vars)
('IF 'ACL2-UNWIND-PROTECT-ERP
('(LAMBDA (STATE ACL2-UNWIND-PROTECT-VAL
ACL2-UNWIND-PROTECT-ERP)
(CONS ACL2-UNWIND-PROTECT-ERP
(CONS ACL2-UNWIND-PROTECT-VAL
(CONS STATE 'NIL))))
cleanup1 'ACL2-UNWIND-PROTECT-VAL 'ACL2-UNWIND-PROTECT-ERP)
('(LAMBDA (STATE ACL2-UNWIND-PROTECT-VAL
ACL2-UNWIND-PROTECT-ERP)
(CONS ACL2-UNWIND-PROTECT-ERP
(CONS ACL2-UNWIND-PROTECT-VAL
(CONS STATE 'NIL))))
cleanup2 'ACL2-UNWIND-PROTECT-VAL 'ACL2-UNWIND-PROTECT-ERP)))
'(MV-NTH '0 mv)
'(MV-NTH '1 mv)
'(MV-NTH '2 mv)
. vars))
body . vars)
(declare (ignore mv vars))
; Does it matter what mv is? In principle it surely does: if mv is some
; screwy variable then it might be that this term doesn't actually have the
; semantics we are about to ascribe to it. We know mv is not in vars since
; this is a termp and mv and vars are used in the same lambda arglist. But
; what if mv is, say, ACL2-UNWIND-PROTECT-ERP? Is the semantics affected?
; No: mv's binding, no matter what name we chose outside of vars, is
; unaffected. Similarly, the names in vars are irrelevant, given that we know
; they don't include ACL2-UNWIND-PROTECT-ERP, etc., which is assured by the
; same observation that term is a termp.
(mv t body cleanup1 cleanup2))
((('LAMBDA (mv . vars)
(('LAMBDA ('ACL2-UNWIND-PROTECT-ERP
'ACL2-UNWIND-PROTECT-VAL 'STATE . vars)
('(LAMBDA (STATE ACL2-UNWIND-PROTECT-VAL
ACL2-UNWIND-PROTECT-ERP)
(CONS ACL2-UNWIND-PROTECT-ERP
(CONS ACL2-UNWIND-PROTECT-VAL
(CONS STATE 'NIL))))
cleanup1 'ACL2-UNWIND-PROTECT-VAL 'ACL2-UNWIND-PROTECT-ERP))
'(MV-NTH '0 mv)
'(MV-NTH '1 mv)
'(MV-NTH '2 mv)
. vars))
body . vars)
(declare (ignore mv vars))
; See comment above.
(mv t body cleanup1 cleanup1))
(& (mv nil nil nil nil))))
(defun translated-acl2-unwind-protectp (term)
; Just for convenience we define the predicate version of translated-acl2-
; unwind-protectp4 to return t or nil according to whether term is the
; translation of an acl2-unwind-protect expression.
(mv-let (ans body cleanup1 cleanup2)
(translated-acl2-unwind-protectp4 term)
(declare (ignore body cleanup1 cleanup2))
ans))
; Essay on EV
; Ev, below, will take the following arguments:
; (ev form alist state latches hard-error-returns-nilp aok)
; It returns (mv erp val latches').
; Ev is actually defined in terms of ev-rec, an analogous function that
; takes the ACL2 world rather than state.
; Hard-error-returns-nil is explained in the comment in hard-error.
; We do not deal with it further below.
; Aok is short for "Attachments are OK", and as the name suggests,
; allows the use of attachments when non-nil. This parameter is discussed at
; some length near the end of this Essay. Till then, we assume that its value
; is nil.
; Imprecise Spec: If erp is t, some evaluation error occurred (e.g.,
; an unbound variable was encountered). Otherwise, erp is nil, val is
; the value of form under alist, and latches' is the final value of
; all the single-threaded objects after the evaluation of form.
; But there are many subtle issues here having to do with the handling
; of single-threaded objects. In the following discussion we use
; (bump state) as a generic function that changes state, as by
; incrementing a global variable in state and returning the modified
; state.
; Assumptions on the input to EV:
; (0) If latches is nil, then either form is known not to modify any
; stobjs (in which case it really doesn't matter what latches is) or
; else there are no live stobjs in alist. In short, if latches is
; nil, we don't keep track of the current values of the stobjs but you
; better not ev a form on a live object (because it will actually
; change the object but not record the new current value on latches).
; (1) If latches is non-nil, then if a stobj name, such as STATE, is bound
; in alist to some value s then
; (1a) s is of the correct shape for that stobj and
; (1b) that stobj name is bound in latches to s.
; Informally, the initial values of the stobjs in alist are identical
; to their initial current values and consistent with the stobj
; definitions.
; (2) If alist binds a stobj name to a live object, then form must be
; single-threaded.
; Clarification of the output spec:
; If no stobj names are bound in alist to live objects, then the
; latches on input may be nil and the final latches may
; be ignored.
; If form is not single-threaded, the meaning of the final latches
; is essentially random.
; In the most common case (where we are using ev to evaluate a form
; typed by the user at the top-level), state is *the-live-state*, all
; the stobj names are bound in alist to their current live objects
; (including 'state to *the-live-state*), and form is single-threaded.
; Observations about the Assumptions
; The only way alist can bind a stobj name to a live object is if we
; did that in our own source code. In particular, a user cannot write
; (list (cons 'state state) (cons '$s $s)), unless the user has access to
; something like coerce-state-to-object. These comments assume such
; magic functions have been made untouchable.
; No live object can be in the final latches unless they were
; there to begin with. If a live object is in the final current
; stobjs, then it was put there by a stobj producing fncall. But that
; would mean there was a live stobj in alist. That, in turn, means
; the same live object was originally in the initial current stobjs.
; Thus, the only time live objects appear in the final latches
; is if we're in our own source code.
; We guarantee, via functions like trans-eval, that assumptions (1)
; and (2) are met in all our calls of ev.
; Further Discussion of the Assumptions:
; Suppose that the symbol 'state is bound in alist to s. Suppose the
; value of the formal parameter state is d. Both s and d are
; state-ps. We call the latter state d because it is the state from
; which ev obtains the definitions of the functions. We also use d to
; determine whether guards should be checked. D is not changed in ev,
; except to decrement the big clock in it to ensure termination.
; By assumption (1), we know that the binding of state in
; latches is s, initially. But in general, the two bindings
; can differ: the binding of state in alist is the initial value of
; state and the binding in the final latches is the final value
; of state.
; Generally speaking, d is *the-live-state*. Indeed, at one point we
; believed:
; The Bogus Live State Claim for :Program Mode Functions: If a
; :program mode function takes STATE as an argument then the function
; can only be evaluated on the live state.
; Below I give a ``proof'' of this claim, for a call of ev stemming
; from a legal form typed by the user to the top-level ACL2 loop.
; Then I give a counterexample!
; ``PROOF:'' The call was translated. Since ev is a :program mode
; function, the call cannot appear in a theorem or other context in
; which the stobj restrictions were not enforced. Hence, the only
; allowable term in the state slot is state itself. Hence, state must
; be *the-live-state*, as it is at the top of LP.
; Now here is a way to run ev from within the loop on a state other
; than the live state: Ev a call of ev. Here is what to execute inside the
; loop.
; (defttag t)
; (remove-untouchable ev t)
; (let ((st (build-state)))
; (ev `(ev 'a '((a . 1)) ',st 'nil 'nil 't) nil state nil nil t))
; The outermost state above is indeed the live one, but the inner ev is
; executed on a dummy state. The computation above produces the result
; (NIL (NIL 1 NIL) NIL).
; The inner state object has to pass the state-p predicate if guard checking is
; enabled in the outer state. If guard checking is turned off in the live
; state, the following example shows the inner ev running on something that is
; not even a state-p. At one time we could make this example work by first
; evaluating the remove-untouchable form above and then :set-guard-checking
; nil; but now we get a hard ACL2 error about program-only functions.
; (ev '(ev 'a '((a . 1)) '(nil nil nil nil nil 0) 'nil 'nil 't)
; nil state nil nil t)
; The 0, above, is the big-clock-entry and must be a non-negative integer. The
; result, when we could compute a result, was (NIL (NIL 1 NIL) NIL).
; Finally, the example below shows the inner ev running a function,
; foo, defined in the dummy world. It doesn't matter if foo is
; defined in the live state or not. The example below shows the state
; returned by build-state at the time of this writing, but modified to
; have a non-trivial CURRENT-ACL2-WORLD setting giving FORMALS and a
; BODY to the symbol FOO.
; (ev '(ev '(foo a)
; '((a . 1))
; '(NIL NIL
; ((ACCUMULATED-TTREE)
; (AXIOMSP)
; (BDDNOTES)
; (CERTIFY-BOOK-FILE)
; (CONNECTED-BOOK-DIRECTORY)
; (CURRENT-ACL2-WORLD
; . ((foo formals . (x)) (foo body . (cons 'dummy-foo x))))
; (CURRENT-PACKAGE . "ACL2")
; (EVISCERATE-HIDE-TERMS)
; (FMT-HARD-RIGHT-MARGIN . 77)
; (FMT-SOFT-RIGHT-MARGIN . 65)
; (GSTACKP)
; (GUARD-CHECKING-ON . T)
; #+acl2-infix (INFIXP)
; (INHIBIT-OUTPUT-LST SUMMARY)
; (IN-LOCAL-FLG . NIL)
; (LD-LEVEL . 0)
; (LD-REDEFINITION-ACTION)
; (LD-SKIP-PROOFSP)
; (PROMPT-FUNCTION . DEFAULT-PRINT-PROMPT)
; (PROOF-TREE-CTX)
; (PROOFS-CO
; . ACL2-OUTPUT-CHANNEL::STANDARD-CHARACTER-OUTPUT-0)
; (SKIPPED-PROOFSP)
; (STANDARD-CO
; . ACL2-OUTPUT-CHANNEL::STANDARD-CHARACTER-OUTPUT-0)
; (STANDARD-OI
; . ACL2-OUTPUT-CHANNEL::STANDARD-OBJECT-INPUT-0)
; (TIMER-ALIST)
; (TRIPLE-PRINT-PREFIX . " ")
; (UNDONE-WORLDS-KILL-RING NIL NIL NIL)
; (UNTOUCHABLE-FNS)
; (UNTOUCHABLE-VARS)
; (WINDOW-INTERFACEP)
; (WORMHOLE-NAME))
; NIL NIL 4000000
; NIL NIL 1 NIL NIL NIL NIL NIL NIL)
; 'nil 'nil 't) nil state nil nil t)
; The output of the ev above was (NIL (NIL (DUMMY-FOO . 1) NIL) NIL).
; The above example can be made slightly more interesting by replacing
; the three occurrences of FOO by EV. It still produces the same
; thing and illustrate the fact that EV doesn't mean what you might
; think it means once you get into an EV!
; The intuition that ``d must be *the-live-state*'' is only true at
; the outermost call of EV. But things take care of themselves inside
; subsequent calls because, if d is not *the-live-state*, EV just runs
; as defined, whatever that means.
; Stobj Latching: How Do We Compute the Final Latches?
; This is simpler than it at first appears: First, we map over the
; term in evaluation order. Every time we apply a function symbol to
; a list of (evaluated) terms, we ``latch'' into latches each of
; the stobj values indicated by the symbol's stobjs-out.
; The order of the sweep is controlled by ev and ev-lst. But all the
; latching is done by ev-fncall. This is surprising because ev-fncall
; does not handle LAMBDAs and translation has entirely eliminated all
; MV-LETs and MVs.
; Let us consider some examples to see why this works -- and to drive
; home some points it took me a while to see. In the following,
; (defun bump (state) (f-put-global 'bump (@ bump) state))
; (defun bump3 (x state) (let ((state (bump state))) (mv nil x state)))
; Consider the translate (==>) of
; :trans (let ((state (bump state)))
; (mv a state b))
; ==>
; ((LAMBDA (STATE B A)
; (CONS A (CONS STATE (CONS B 'NIL))))
; (BUMP STATE)
; B A)
; Sweep order is (BUMP STATE), B, A, and then the CONS nest. Of these, only
; the BUMP has a non-trivial stobjs-out. We latch the state coming out of
; (BUMP STATE).
; :trans (mv-let (erp val state)
; (bump3 x state)
; (mv (and erp val) (cons erp val) state))
; ==>
; ((LAMBDA (MV)
; ((LAMBDA (ERP VAL STATE)
; (CONS (IF ERP VAL 'NIL)
; (CONS (CONS ERP VAL)
; (CONS STATE 'NIL))))
; (MV-NTH '0 MV)
; (MV-NTH '1 MV)
; (MV-NTH '2 MV)))
; (BUMP3 X STATE))
; We latch the third value of (BUMP3 X STATE), when we ev-fncall
; BUMP3. No other function causes us to latch, so that is the final
; latches.
; :trans (mv-let (erp val state)
; (bump3 x state)
; (let ((state (bump state)))
; (mv erp val state)))
; ==>
; ((LAMBDA (MV)
; ((LAMBDA (ERP VAL STATE)
; ((LAMBDA (STATE VAL ERP)
; (CONS ERP (CONS VAL (CONS STATE 'NIL))))
; (BUMP STATE)
; VAL ERP))
; (MV-NTH '0 MV)
; (MV-NTH '1 MV)
; (MV-NTH '2 MV)))
; (BUMP3 X STATE))
; We latch the third value of (BUMP3 X STATE), when we ev-fncall BUMP3.
; The next non-trivial stobjs-out function we ev-fncall is the BUMP.
; We latch its result, which gives us the final latches.
; The restrictions imposed by translate ensure that we will never
; encounter terms like (fn a (bump state) b (bump state) c) where
; there is more than one latched stobj coming out of an arglist. But
; we do not exploit this fact. We just latch every stobj-out as we go
; across the args. Similarly, the translate restrictions ensure that
; if a stobj is returned by some function, then it gets out. So we
; can latch it when it is returned by the function, even though it
; apparently goes into a CONS nest, say, from which it may not, a
; priori, get out.
; We close with a discussion of the final argument of ev and many other
; evaluator functions, aok. In short: The safe value for aok is nil, but it is
; more powerful (fewer aborts) to use t rather than nil for aok, if that is
; sound. Unless you are writing ACL2 system code, it probably is sound to use
; t. But now we discuss in more depth the question of assigning a value to
; aok.
; Most or all of the evaluator functions (ev, ev-fncall, trans-eval,
; simple-translate-and-eval, etc.) have a final argument called aok, which is
; mnemonic for "attachments OK". The conservative value to use is nil, which
; means that no attachments (in the sense of defattach) will be used by the
; evaluator. But if you want attachments to be allowed by the evaluator, then
; use aok = t.
; In ACL2's own source code, aok is usually t, but it is (and must of course,
; be) nil whenever we are simplifying terms during a proof. See the Essay on
; Defattach for related discussion.
; Here, in brief, is the logical story (which is important to understand when
; deciding to use aok=t). The evaluator functions can all be thought of as
; producing a result that is provably equal to a given term. But the question
; is: Provably equal in what formal theory? The "official" theory of the
; current ACL2 world has nothing to do with attachments, and is the theory for
; which we have a prover. So if the rewriter, say, wants to use ev-fncall to
; replace one term by another, the input and output terms should be provably
; equal without attachments, which is why we use aok=nil in the call of
; ev-fncall under rewrite. On the other hand, in the top-level loop we
; presumably want to use all attachments -- the whole point of (defattach f g)
; for an encapsulated f and defined g is to evaluate under the equation (equal
; (f x) (g x)). So the call of trans-eval under ld-read-eval-print has aok=t.
; Thus, if you are calling simple-translate-and-eval for something like hints,
; then probably it's fine to use aok=t -- hints don't affect soundness and one
; might want to take advantage of attachments. As ACL2 evolves, many of its
; system functions may be encapsulated with default attachments, so one will
; want to use aok=t whenever possible in order to avoid an "undefined function"
; error when such a system function is called.
(defun acl2-system-namep (name wrld)
; Warning: keep this in sync with acl2-system-namep-state.
; Name is a name defined in wrld. We determine whether it is one of ours or is
; user-defined.
; If name is not defined -- more precisely, if we have not yet laid down an
; 'absolute-event-number property for it -- then we return nil except in the
; boot-strap world.
(declare (xargs :guard (and (symbolp name) (plist-worldp wrld))))
(cond ((global-val 'boot-strap-flg wrld) t)
(t (getpropc name 'predefined nil wrld))))
(defun acl2-system-namep-state (name state)
; Warning: keep this in sync with acl2-system-namep. See comments there.
(cond ((f-get-global 'boot-strap-flg state) t)
(t (getpropc name 'predefined))))
#+acl2-loop-only
(encapsulate
; We introduce big-n and decrement-big-n with no axioms. We could certainly
; add axioms, namely that (big-n) is a positive integer and decrement-big-n
; decrements, but we choose not to do so. Instead, we keep these axiom-free
; and introduce executable versions in program mode, just below. We imagine
; that n is a positive integer larger than the lengths of all computations that
; will ever take place with ACL2, and that decrement-big-n is 1-. We also make
; big-n untouchable, since without that we have been able to prove nil, as
; follows:
; (in-package "ACL2")
; (defun foo () (big-n))
; (defthm bad1 (equal (foo) '(nil)) :rule-classes nil)
; (defthm bad2
; (equal (big-n) '(nil))
; :hints (("Goal" :use bad1 :in-theory (disable (foo))))
; :rule-classes nil)
; (defun bar () 0)
; (defthm bad3
; (equal (bar) '(nil))
; :hints (("Goal" :by (:functional-instance bad2 (big-n bar))))
; :rule-classes nil)
; (defthm bad
; nil
; :hints (("Goal" :use bad3))
; :rule-classes nil)
; We also make decrement-big-n and zp-big-n untouchable, just because we are a
; bit paranoid here.
(((big-n) => *)
((decrement-big-n *) => *)
((zp-big-n *) => *))
(logic)
(local (defun big-n ()
0))
(local (defun decrement-big-n (n)
(declare (ignore n))
0))
(local (defun zp-big-n (n)
(declare (ignore n))
nil)))
#-acl2-loop-only
(progn
; (defconstant *big-n-special-object* '(nil . nil)) has been moved to
; acl2.lisp, to avoid a CLISP compiler warning.
(defun big-n () *big-n-special-object*)
(defmacro decrement-big-n (n)
`(if (eq ,n *big-n-special-object*)
*big-n-special-object*
(1- ,n)))
(defmacro zp-big-n (n)
`(if (eq ,n *big-n-special-object*)
nil
(zp ,n))))
#-acl2-loop-only
(defparameter *ev-shortcut-okp*
; The code for ev-fncall-rec has a shortcut, calling raw-ev-fncall to execute
; using *1* functions. Because the *1* functions use (live) state globals
; guard-checking-on and safe-mode, these need to agree with the corresponding
; parameters of ev-fncall-rec in order for it to be sound to call
; raw-ev-fncall. We may bind *ev-shortcut-okp* to t when we know that this
; agreement is ensured.
; There are times where avoiding the shortcut can get us into trouble. In
; particular, we have seen a case where the logic code for an ev-nest function
; produced nil for a call of state-p or state-p1 on *the-live-state*.
nil)
(defun w-of-any-state (st)
; This returns (w state) but, unlike w, st is not (known to be)
; single-threaded, so it can be used on the binding of 'STATE in the latches of
; a call of a function in the ev nest. In the raw Lisp case, we have the same
; f-get-global code as in the definition of w. For the logic, we open up
; f-get-global and then get-global to get the body below.
#-acl2-loop-only
(cond ((live-state-p st)
(return-from w-of-any-state (f-get-global 'current-acl2-world st))))
(cdr (assoc 'current-acl2-world (global-table st))))
(defun untranslate-preprocess-fn (wrld)
(declare (xargs :guard (plist-worldp wrld)))
(cdr (assoc-eq 'untranslate-preprocess (table-alist
'user-defined-functions-table
wrld))))
(defmacro untranslate* (term iff-flg wrld)
; We need to call untranslate in ev-fncall-guard-er and ev-fncall-msg, where we
; have not yet called ev-fncall. So we define this version of untranslate now
; and defer untranslate (and untranslate-lst) until after defining the ev
; family of functions. We document in the guard below our expectation that
; wrld is a symbol, in order to avoid any overhead (e.g., from defabbrev).
(declare (xargs :guard (symbolp wrld)))
`(untranslate1 ,term
,iff-flg
(untrans-table ,wrld)
(untranslate-preprocess-fn ,wrld)
,wrld))
(defun save-ev-fncall-guard-er (fn guard stobjs-in args w)
; Warning: If you change this definition, consider changing :doc
; make-wormhole-status, which references this definition.
(wormhole-eval 'ev-fncall-guard-er-wormhole
'(lambda ()
(make-wormhole-status
; Here we pass nil for the old "status", so that we will update the status
; unconditionally. That can avoid an expensive equality test when a logical
; world or other large structure belongs to args.
nil
:ENTER
(list fn guard stobjs-in args w)))
nil))
(defrec attachment
; See the Essay on Merging Attachment Records.
((g . ext-succ) . (components . pairs))
nil)
(defrec attachment-component
; See the Essay on Merging Attachment Records.
((ext-anc . ord-anc) . path)
nil)
(defun attachment-record-pairs (records acc)
(cond ((endp records)
acc)
(t (attachment-record-pairs
(cdr records)
(append (access attachment (car records) :pairs)
acc)))))
(defun all-attachments (wrld)
; This function returns all attachment pairs except for attachments to warrants