-
Notifications
You must be signed in to change notification settings - Fork 0
/
translate.lisp
9026 lines (7946 loc) · 397 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 6.4 -- A Computational Logic for Applicative Common Lisp
; Copyright (C) 2014, Regents of the University of Texas
; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
; (C) 1997 Computational Logic, Inc. See the documentation topic NOTE-2-0.
; This program is free software; you can redistribute it and/or modify
; it under the terms of the LICENSE file distributed with ACL2.
; This program is distributed in the hope that it will be useful,
; but WITHOUT ANY WARRANTY; without even the implied warranty of
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
; LICENSE for more details.
; Written by: Matt Kaufmann and J Strother Moore
; email: [email protected] and [email protected]
; Department of Computer Science
; University of Texas at Austin
; Austin, TX 78712 U.S.A.
(in-package "ACL2")
(mutual-recursion
(defun termp (x 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
(true-listp (cdr x))
(eql (length (cdr x)) arity)
(term-listp (cdr x) w))))
((and (consp (car x))
(true-listp (car x))
(eq (car (car x)) 'lambda)
(equal 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)
(equal (length (cadr (car x)))
(length (cdr x))))
t)
(t nil)))
(defun term-listp (x w)
(cond ((atom x) (equal x nil))
((termp (car x) w) (term-listp (cdr x) w))
(t nil)))
)
(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)
(getprop x 'macro-args
'(:error "We thought macro-args was only called if there ~
were (zero or more) macro-args.")
'current-acl2-world 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))))
(t (msg "ACL2 cannot ev the call of undefined function ~x0 on argument ~
list:~|~%~x1~@2~|~%~@3"
fn
args
(ignored-attachment-msg ignored-attachment)
(error-trace-suggestion nil)))))
(defun ev-fncall-null-body-er (ignored-attachment fn args latches)
(mv t
(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,'' and hence has special raw Lisp code. This call is ~
illegal because program-only functions are only allowed to invoke their ~
raw Lisp code, but in this case there was an attempt to invoke executable ~
counterpart code ~#1~[because of guard-checking (see :DOC ~
guard-evaluation-table)~/because it is being called under a ``safe mode'' ~
that is used, for example, during macroexpansion~]."
(cons fn args)
(if safe-mode 1 0)))
(defconst *safe-mode-guard-er-addendum*
" 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)))
#-acl2-loop-only
((eq (cdr temp) (car vals))
(latch-stobjs1 (cdr stobjs-out)
(cdr vals)
latches))
(t
#-acl2-loop-only
(er hard! 'latch-stobjs1
"We had thought that the values in user-stobj-alist match up ~
with the values of corresponding stobjs. Please contact ~
the ACL2 implementors.")
#+acl2-loop-only
(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))))
#-acl2-loop-only
; We deliberately do not assign a value for the following. It is let-bound in
; ev and friends and assigned during the evaluation of *1* functions. If we
; call *1* functions directly in raw Lisp, we will presumably get an
; unbound-variable error, but at least that will call our attention to the fact
; that it should be bound before calling *1* functions.
(defvar *raw-guard-warningp*)
(defun actual-stobjs-out1 (stobjs-in args user-stobj-alist)
(cond ((endp stobjs-in)
(assert$ (null args) nil))
(t (let ((rest (actual-stobjs-out1 (cdr stobjs-in) (cdr args)
user-stobj-alist)))
(cond ((or (null (car stobjs-in))
(eq (car stobjs-in) 'state))
rest)
(t (let ((pair (rassoc-equal (car args) user-stobj-alist)))
(assert$ pair
(cond ((eq (car stobjs-in) (car pair))
rest)
(t (acons (car stobjs-in)
(car pair)
rest)))))))))))
(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 args wrld user-stobj-alist)
(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 args user-stobj-alist)))
(cond (alist (apply-symbol-alist alist stobjs-out nil))
(t stobjs-out))))))))
#-acl2-loop-only
(defvar *mbe-as-exec*
; 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 *ignore-invariant-risk* is 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, *mbe-as-exec*, 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,
; *mbe-as-exec* is nil. But we arrange the following, and explain below.
;
; (a) The *1* code for an invariant-risk :program mode function binds
; *mbe-as-exec* to t.
;
; (b) The *1* code for an mbe call reduces to its :exec code when *mbe-as-exec*
; is true.
;
; (c) Raw-ev-fncall binds *mbe-as-exec* to nil for :logic mode functions.
;
; (d) Oneify binds *mbe-as-exec* 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,
; *mbe-as-exec* 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 *mbe-as-exec* to nil in
; raw-ev-fncall precisely to avoid such a probem.
; To see why we need (d), see the example in a comment in oneify that starts
; with "(defun f-log".
nil)
#-acl2-loop-only
(defun raw-ev-fncall (fn args latches w user-stobj-alist
hard-error-returns-nilp aok)
(the #+acl2-mv-as-values (values t t t)
#-acl2-mv-as-values t
(let* ((*aokp* aok)
(pair (assoc-eq 'state latches))
(w (if pair (w (cdr pair)) w)) ; (cdr pair) = *the-live-state*
(throw-raw-ev-fncall-flg t)
(*mbe-as-exec*
; We defeat the *mbe-as-exec* optimization so that when we use raw-ev-fncall to
; evaluate a call of a :logic mode term, all of the evaluation will take place
; in the logic. Note that we don't restrict this special treatment to
; :common-lisp-compliant functions, because such a function might call an
; :ideal mode function wrapped in ec-call. But we do restrict to :logic mode
; functions, since they cannot call :program mode functions and hence there
; cannot be a subsidiary rebinding of *mbe-as-exec* to t.
(if (logicalp fn w)
nil
*mbe-as-exec*))
(*1*fn (*1*-symbol fn))
(applied-fn (cond
((fboundp *1*fn) *1*fn)
((and (global-val 'boot-strap-flg w)
(not (global-val 'boot-strap-pass-2 w)))
fn)
(t
(er hard 'raw-ev-fncall
"We had thought that *1* functions were ~
always defined outside the first pass of ~
initialization, but the *1* function for ~
~x0, which should be ~x1, is not."
fn *1*fn))))
(stobjs-out
(cond ((eq fn 'return-last)
; Things can work out fine if we imagine that return-last returns a single
; value: in the case of (return-last ... (mv ...)), the mv returns a list and
; we just pass that along.
'(nil))
; The next form was originally conditionalized with #+acl2-extra-checks, but we
; want to do this unconditionally.
(latches ; optimization
(actual-stobjs-out fn args w user-stobj-alist))
(t (stobjs-out fn w))))
(val (catch 'raw-ev-fncall
(cond ((not (fboundp fn))
(er hard 'raw-ev-fncall
"A function, ~x0, that was supposed to be ~
defined is not. Supposedly, this can only ~
arise because of aborts during undoing. ~
There is no recovery from this erroneous ~
state."
fn)))
(prog1
(let ((*hard-error-returns-nilp*
hard-error-returns-nilp))
#-acl2-mv-as-values
(apply applied-fn args)
#+acl2-mv-as-values
(cond ((null (cdr stobjs-out))
(apply applied-fn args))
(t (multiple-value-list
(apply applied-fn args)))))
(setq throw-raw-ev-fncall-flg nil))))
; It is important to rebind w here, since we may have updated state since the
; last binding of w.
(w (if pair
; We use the live state now if and only if we used it above, in which case (cdr
; pair) = *the-live-state*.
(w (cdr pair))
w)))
; Observe that if a throw to 'raw-ev-fncall occurred during the
; (apply fn args) then the local variable throw-raw-ev-fncall-flg
; is t and otherwise it is nil. If a throw did occur, val is the
; value thrown.
(cond
(throw-raw-ev-fncall-flg
(mv t (ev-fncall-msg val w user-stobj-alist) latches))
(t #-acl2-mv-as-values ; adjust val for the multiple value case
(let ((val
(cond
((null (cdr stobjs-out)) val)
(t (cons val
(mv-refs (1- (length stobjs-out))))))))
(mv nil
val
; The next form was originally conditionalized with #+acl2-extra-checks, with
; value latches when #-acl2-extra-checks; but we want this unconditionally.
(latch-stobjs stobjs-out ; adjusted to actual-stobjs-out
val
latches)))
#+acl2-mv-as-values ; val already adjusted for multiple value case
(mv nil
val
; The next form was originally conditionalized with #+acl2-extra-checks, with
; value latches when #-acl2-extra-checks; but we want this unconditionally.
(latch-stobjs stobjs-out ; adjusted to actual-stobjs-out
val
latches)))))))
(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 it occurs in a
; definition body (i.e., stobjs-out of translate11 is non-t) or in a
; definition (i.e., stobjs-out is t). 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 ('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 body)
('MV-NTH ''1 body)
('MV-NTH ''2 body)
. vars)
(declare (ignore vars))
(mv t body cleanup1 cleanup2))
(& (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))
(defun stobjp (x known-stobjs w)
; We recognize whether x is to be treated as a stobj name. Known-stobjs is a
; list of all such names, or else T, standing for all stobj names in w. During
; translation, only certain known stobjs in w are considered stobjs, as per the
; user's :stobjs declare xargs. If you want to know whether x has been defined
; as a stobj in w, use known-stobjs = t.
; Slight abuse permitted: Sometimes known-stobjs will be a list of stobj flags!
; E.g., we might supply (NIL NIL STATE NIL $S) where (STATE $S) is technically
; required. But we should never ask if NIL is a stobj because we only ask this
; of variable symbols. But just to make this an ironclad guarantee, we include
; the first conjunct below.
(and x
(symbolp x)
(if (eq known-stobjs t)
(getprop x 'stobj nil 'current-acl2-world w)
(member-eq x known-stobjs))))
; 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 a concrete form.
; First, go outside the loop and call (build-state) to obtain a dummy
; state. I will write that '(NIL ... NIL). At present, it has 15
; components, most of which are nil, but some, like the initial global
; table, are non-trivial. Then inside the loop execute:
; (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. To make this
; example work, first evaluate :set-guard-checking nil.
; (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 is (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)
; (INFIXP)
; (INHIBIT-OUTPUT-LST SUMMARY)
; (IN-LOCAL-FLG . NIL)
; (LD-LEVEL . 0)
; (LD-REDEFINITION-ACTION)
; (LD-SKIP-PROOFSP)
; (MORE-DOC-MAX-LINES . 45)
; (MORE-DOC-MIN-LINES . 35)
; (MORE-DOC-STATE)
; (PRINT-DOC-START-COLUMN . 15)
; (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 is (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)
; 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.
(cond ((global-val 'boot-strap-flg wrld) t)
(t (getprop name 'predefined nil 'current-acl2-world wrld))))
#+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 *) => *))
(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*