-
Notifications
You must be signed in to change notification settings - Fork 0
/
interface-raw.lisp
10335 lines (9019 loc) · 460 KB
/
interface-raw.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.3 -- 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")
; This file, interface-raw.lisp, contains parts of ACL2 which we
; cannot code in ACL2 because they require constructs not in ACL2, such
; as calling the compiler.
; We start with a section that was originally in acl2-fns.lisp, but was moved
; here when sharp-atsign-read started using several functions defined in the
; sources, to avoid compiler warnings.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; SUPPORT FOR #@
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defmacro sharp-atsign-read-er (str &rest format-args)
`(progn (loop (when (null (read-char-no-hang stream nil nil t))
(return)))
(error (concatenate 'string ,str ". See :DOC set-iprint.")
,@format-args)))
(defun sharp-atsign-read (stream char n &aux (state *the-live-state*))
(declare (ignore char n))
(let (ch
bad-ch
(zero-code (char-code #\0))
(index 0)
(iprint-last-index (iprint-last-index state)))
(loop
(when (eql (setq ch (read-char stream t nil t))
#\#)
(return))
(let ((digit (- (char-code ch) zero-code)))
(cond ((or (< digit 0)
(> digit 9))
(when (not bad-ch)
(setq bad-ch ch))
(return))
(t
(setq index (+ digit (* 10 index)))))))
(cond
(bad-ch
(sharp-atsign-read-er
"Non-digit character ~s following #@~s"
bad-ch index))
((symbol-value (f-get-global 'certify-book-info state))
(sharp-atsign-read-er
"Illegal reader macro during certify-book, #@~s#"
index))
((iprint-ar-illegal-index index state)
(sharp-atsign-read-er
"Out-of-bounds index in #@~s#"
index))
(t
(let ((old-read-state ; bind special
*iprint-read-state*))
(cond
((eq old-read-state nil)
(iprint-ar-aref1 index state))
(t
(let ((new-read-state-order (if (<= index iprint-last-index)
'<=
'>)))
(cond
((eq old-read-state t)
(setq *iprint-read-state*
(cons index new-read-state-order))
(iprint-ar-aref1 index state))
((eq (cdr old-read-state)
new-read-state-order) ; both > or both <=
(iprint-ar-aref1 index state))
(t
(multiple-value-bind
(index-before index-after)
(cond
((eq (cdr old-read-state) '<=)
(values index (car old-read-state)))
(t ; (eq (cdr old-read-state) '>)
(values (car old-read-state) index)))
(sharp-atsign-read-er
"Attempt to read a form containing both an index~%~
created before the most recent rollover (#@~s#) and~%~
an index created after that rollover (#@~s#)"
index-before index-after))))))))))))
(defun define-sharp-atsign ()
(set-new-dispatch-macro-character
#\#
#\@
#'sharp-atsign-read))
(eval-when
; Note: CMUCL build breaks without the check below for a compiled function.
#-cltl2
(load eval)
#+cltl2
(:load-toplevel :execute)
(when (compiled-function-p! 'sharp-atsign-read)
(let ((*readtable* *acl2-readtable*))
(define-sharp-atsign))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; EVALUATION
; Essay on Evaluation in ACL2
; This essay is structured as follows. Terminology is explained below.
; A. Introduction
; B. Specification of the problem
; C. Sketch of correctness proof
; D. Why safe mode is necessary
; E. The template for oneification of function definitions
; F. Remarks
; Let us begin.
; A. Introduction
; Evaluation in ACL2, which takes place in the ACL2 loop and during theorem
; proving, is based on the way evaluation was done in Nqthm. The idea is to
; "oneify" the body of a definition by replacing functions by their so-called
; "executable counterparts," sometimes called "*1* functions." Also see :doc
; evaluation. The primitives have *1* functions that reflect their logical
; definitions, so that for example (*1*car x), or more precisely
; (acl2_*1*_lisp::car x), returns nil when x is an atom -- except that an error
; occurs if we are checking guards (or are in so-called safe mode, as explained
; below). Defined functions have *1* function counterparts that are defined,
; roughly speaking, by replacing each function call in their bodies by a call
; of the corresponding *1* function.
; The evaluation mechanism in ACL2 changed radically in v1-8, when guards were
; removed from the logic. It has changed again in Version_2.6, due to a hole
; in the existing mechanism, as we explain in Part D of this Essay, below.
; B. Specification of the problem
; Our specification begins with the introduction of three notions of evaluation
; and three notions of macroexpansion. Evaluation is relative to an (implicit)
; environment, which binds variables to ACL2 values, and operates on ACL2 terms
; that are free of macro calls. If we want to discuss evaluation of terms that
; involve macro calls, we will compose macroexpansion and evaluation. This
; composition represents the way that both Common Lisp and the ACL2 loop
; evaluate forms. We also assume that there is no distinction between
; evaluation of compiled and interpreted code. Finally, we assume that for all
; of these sorts of evaluation and expansion, macros are expanded before
; function and macro bodies are stored; this is how things are done in the ACL2
; logic and with *1* functions, and it had better be equivalent to how a Common
; Lisp does its evaluation and expansion.
; We extend classes of function symbols to classes of terms in the obvious way:
; a :logic mode term is one whose function symbols are all :logic mode function
; symbols, and similarly for the notion of :common-lisp-compliant.
; Here then are the notions promised above.
; ACL2 logical evaluation: This procedure is an interpreter that computes
; using definitions in the logic and obvious properties of primitives (e.g.,
; (stringp "abc") returns t).
; ACL2 loop evaluation: This is the procedure used in the ACL2 loop, using
; so-called *1* functions (and higher-level routines such as raw-ev-fncall).
; Common Lisp evaluation: As the name implies, this procedure is the one used
; by Common Lisp.
; ACL2 logical macroexpansion: This is any procedure that carries out the
; usual macroexpansion algorithm (outside-in), but entirely using ACL2
; definitions, including those of :program mode functions. We assume that
; macros have already been similarly expanded in function bodies, before
; evaluation begins. Macro bodies are evaluated using ACL2 logical
; evaluation. This procedure is embodied in the ACL2 definition of the
; function translate.
; ACL2 loop macroexpansion: This is the procedure that ACL2 actually applies
; in order to create terms from user input. Ideally this procedure returns
; the same results as does ACL2 logical macroexpansion; the distinction here
; is between what an appropriate interpreter would return (ACL2 logical
; macroexpansion) and how ACL2 actually translates a term (ACL2 loop
; macroexpansion). ACL2 loop macroexpansion always takes place in safe mode.
; Common Lisp macroexpansion: This is how Common Lisp (actually, an arbitrary
; but fixed implementation) macroexpands forms.
; As an aside, we note the following fact that is useful in establishing the
; guarantees below, but whose proof we omit here.
; (*) If a :common-lisp-compliant function is applied to arguments that
; satisfy its guard (using Common Lisp evaluation), without error, then the
; result agrees with that produced by ACL2 logical evaluation.
; Now our top-level guarantees about evaluation and macroexpansion are as
; follows, where for brevity, "evaluation" of a given type is the composition
; of macroexpansion and evaluation for that type.
; (1) If ACL2 evaluates a :logic mode form without error, then the value
; returned equals the result of ACL2 logical (macroexpansion and) evaluation
; of that form.
; (2) If furthermore that evaluation in done with guard-checking on and the
; result of ACL2 logical macroexpansion is a :common-lisp-compliant term,
; then any non-erroneous Common Lisp evaluation returns that same value.
; C. Sketch of correctness proof
; We now outline a proof of these guarantees by breaking them into the
; following sequence of claims. We write "weakly implements" to mean that two
; procedures give equivalent results on given inputs when they both return
; without error, and we write "implements" if the condition can be weakened to
; assume only that the first procedure returns without error. That is, proc1
; implements proc2 iff proc1 weakly implements proc2 and whenever proc1 returns
; without error, then so does proc2. Above, "equivalent" means identical
; except as explained otherwise below. Implicit in this notion is that the
; input is appropriate for the procedures; for example, our notions of
; evaluation assume that all function symbols in the input are either ACL2
; primitive functions or have been defined as functions (not macros) in ACL2.
; A more rigorous argument would proceed by induction on the length of
; histories, showing that the properties in question hold when one extends the
; history with new function and macro definitions.
; (1a) ACL2 loop evaluation implements ACL2 logical evaluation on :logic mode
; terms and, provided safe mode is used, on arbitrary terms.
; (1b) ACL2 loop macroexpansion implements ACL2 logical macroexpansion.
; (2a) ACL2 loop evaluation in safe mode weakly implements Common Lisp
; evaluation. The same claim holds if the assumption of safe mode is
; replaced by the assumption that guard-checking is on, provided that the
; input form expands to a :common-lisp-compliant term.
; (2b) ACL2 loop macroexpansion weakly implements Common Lisp macroexpansion,
; where results r1 (from ACL2 loop macroexpansion) and r2 (from Common Lisp
; macroexpansion) are considered equivalent if for any environment, the ACL2
; loop evaluation of r1 with guard-checking on returns the same result as the
; Common Lisp evaluation of r2, provided both evaluations return without
; error.
; Sketch of proof that guarantees hold. Clearly (1) follows from (1a) and
; (1b), while (2) follows from (1b) and (2b). (1a) follows by inspection of
; the template presented below, using (*) above. (1b) follows from (1a) by
; computational induction on the macroexpansion, because ACL2 loop
; macroexpansion and ACL2 logical macroexpansion differ only in the use of loop
; or logical evaluation of macro bodies. The first part of (2a) is argued
; similarly to (1a), while the second part is actually quite trivial by
; inspection of the template below. Finally, (2b) follows from (2a) by a
; computational induction just as (1b) follows from (1a), with a bit of
; complication. When we encounter a call of a macro first introduced in ACL2
; (either during the boot-strap or by a user), then we evaluate the same macro
; body for ACL2 loop evaluation as for Common Lisp evaluation, except that this
; body has first been macroexpanded using ACL2 loop macroexpansion and Common
; Lisp macroexpansion, respectively. But these may be viewed as equivalent by
; the inductive hypothesis (where for purposes of this proof we pretend that
; macroexpansion of the body takes place as part of the process). In the other
; case, the macro already has a Common Lisp definition (as a function or
; macro), and we have arranged that (2) holds. For example, the ACL2 loop
; macroexpansion of (append x y z) is (binary-append x (binary-append y z)),
; and Common Lisp evaluation of the former clearly agrees with ACL2 loop
; evaluation of the latter. Q.E.D.
; D. Why safe mode is necessary
; The soundness of ACL2 potentially rests on the principle of not calling raw
; Lisp counterparts of functions with arguments outside their intended domains,
; as specified by their guards. Here we give three examples illustrating why
; we introduced safe mode in Version_2.6. The third one is a proof of nil!
; Example 1. In our first example below, the defun of bar should fail. It
; does indeed fail starting with Version_2.6, but not in Version_2.5 or (we
; believe) several versions before that. We discuss below how this can lead
; to unsoundness.
; (defmacro foo (x) (car x))
; (set-guard-checking nil)
; (defun bar (y)
; (declare (xargs :verify-guards t))
; (cons (foo y) y))
; :q
; (trace bar)
; (lp)
; Now, the result of evaluating (bar 3) looks as shown below. Notice that the
; Common Lisp function bar is called. If the Common Lisp evaluation of the
; form (car 'y) had returned 1 or 2 (say) instead of breaking, then the Common
; Lisp evaluation of (bar 3) would have returned (cons 1 3) or (cons 2 3),
; respectively. This evaluation could be reflected in theorems (equal (bar 3)
; i) [i=1,2] proved in books certified in two different Common Lisp
; implementations of ACL2. We could then prove nil by including both books
; into the same session. Lest one think that one needs different Lisp
; implementations to expose unsoundness, imagine a single Lisp in which (car
; 'y) sometimes returns 1 and sometimes returns 2.
; ACL2 >(bar 3)
; 1> (ACL2_*1*_ACL2::BAR 3)>
; 2> (BAR 3)>
;
; Error: Y is not of type LIST.
; Fast links are on: do (si::use-fast-links nil) for debugging
; Error signalled by CAR.
; Broken at COND. Type :H for Help.
; ACL2>>
; Here is what ACL2 Version_2.6 prints in an attempt to define function bar,
; above, with guard-checking off.
; ACL2 >(defun bar (y) (foo y))
;
;
; ACL2 Error in ( DEFUN BAR ...): The guard for the function symbol
; CAR, which is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments
; in the call (CAR 'Y). The guard is being checked because this function
; is a primitive and a "safe" mode is being used, perhaps for macroexpansion.
;
;
;
; ACL2 Error in ( DEFUN BAR ...): In the attempt to macroexpand the
; form (FOO Y), evaluation of the macro body caused an error.
;
;
; Summary
; Form: ( DEFUN BAR ...)
; Rules: NIL
; Warnings: None
; Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
;
; ******** FAILED ******** See :DOC failure ******** FAILED ********
; ACL2 >
; Example 2. Unlike the previous example, this one causes problems even when
; guard-checking is on. (Thanks to Pete Manolios for helping to construct this
; example, which is simpler than an earlier one we had.)
; (defun my-endp-0 ()
; (declare (xargs :mode :program))
; (endp 0))
; (defmacro bad-macro ()
; (my-endp-0))
; :q
; (trace my-endp-0 endp)
; (lp)
; (thm (equal (bad-macro) 1))
; Now look at the following Version_2.5 trace. It highlights a behavior of
; Version_2.5: when a :program mode function (here, my-endp-0) is
; called on arguments satisfying its guard (here, implicitly t), the
; corresponding raw Lisp function is invoked. Thus guards are not checked on
; its subroutines (here, endp). In this example, endp is being called on an
; argument not satisfying its guard. In the abstract, this is problematic
; because we use guards to restrict primitives to arguments for which the
; result is implementation independent. If the result of (endp 0) can depend
; on the implementation, we could prove nil as described in the preceding
; example.
; ACL2 !>(thm (equal (bad-macro) 1))
; 1> (ACL2_*1*_ACL2::MY-ENDP-0)>
; 2> (MY-ENDP-0)>
; 3> (ENDP 0)>
;
; Error: 0 is not of type LIST.
; Fast links are on: do (si::use-fast-links nil) for debugging
; Error signalled by SYSTEM::TRACE-CALL.
; Broken at COND. Type :H for Help.
; ACL2>>
; The example above may seem contrived (because it is!). However, our foray
; into this territory began on a rather similar but real example. In Allegro
; 6.0, the character (code-char (+ 128 65)) is upper case; in particular it is
; not equal to the result of applying char-downcase to it. However, this is
; not the case for Allegro 5.0.1. Since the result is
; implementation-dependent, it is natural to restrict the application of
; code-char to standard characters, using ACL2's guard mechanism. But the
; example above show that we can bypass such restrictions by using macros.
; Example 3. We can prove nil in Version_2.5 by certifying the following two
; books. The only cheats are that the first book needs to be certified after
; executing the following in the ACL2 loop:
; (set-guard-checking nil)
; First book, call it "ex":
; (in-package "ACL2")
;
; (defun my-eq (x y)
; (declare (xargs :guard t ; "bad" guard
; :mode :program))
; (eq x y))
;
; (defmacro bad-macro ()
; (my-eq '(a b) '(a b)))
;
; (set-verify-guards-eagerness 0)
;
; (local (verify-termination my-eq))
;
; (defun bad-fn ()
; (bad-macro))
;
; (defthm bad-thm
; (bad-fn)
; :rule-classes nil)
; Second book, which includes the one above::
; (in-package "ACL2")
;
; (local (include-book "ex"))
;
; (defthm very-bad
; nil
; :hints (("Goal" :use bad-thm))
; :rule-classes nil)
; In Version_2.6 we get an error when we try to certify the first book above
; ("ex"):
; ACL2 Error in ( DEFUN BAD-FN ...): The guard for the function symbol
; EQ, which is (IF (SYMBOLP X) T (SYMBOLP Y)), is violated by the arguments
; in the call (EQ '(A B) '(A B)). The guard is being checked because
; this function is a primitive and a "safe" mode is being used, perhaps
; for macroexpansion.
;
;
;
; ACL2 Error in ( DEFUN BAD-FN ...): In the attempt to macroexpand the
; form (BAD-MACRO), evaluation of the macro body caused an error.
; As the first message just above suggests, in Version_2.6 we prevent the bad
; behavior illustrated by the examples above by introducing a "safe mode" for
; use during macroexpansion, in which guards are checked on built-in functions.
; Finally, note that we do not attempt to fix the following "problem." That
; is, the behavior for the example below is unchanged from Version_2.5 to
; Version_2.6. The point is that for macroexpansion to behave properly, we
; really need only guarantee consistency between the logic and Common Lisp; it
; is acceptable if in some modes we get errors even when errors are not
; necessary.
; (defun mac-fn (x) (declare (xargs :guard (consp x))) x)
; (defmacro mac (x) (mac-fn x))
; (defun bar (x) (mac x)) ; fails
; :set-guard-checking nil
; (defun bar (x) (mac x)) ; succeeds
; E. The template for oneification of function definitions
; Before we present this template, we give a bit of history and show an
; example.
; The following example shows how *1* functions are handled in Version_2.5 and
; before. The ACL2 definition is:
; (defun foo (x)
; (declare (xargs :mode :logic :guard (true-listp x)))
; (if (endp x) 3 (+ 1 (foo (cdr x)))))
; Here is the executable-counterpart in Version_2.5, in gcl:
; ACL2>(symbol-function 'ACL2_*1*_ACL2::FOO) ; in gcl, ACL2 Version_2.5
; (LISP:LAMBDA-BLOCK ACL2_*1*_ACL2::FOO (X)
; (LABELS ((ACL2_*1*_ACL2::FOO (X)
; (IF (ACL2_*1*_LISP::ENDP X) '3
; (ACL2_*1*_ACL2::BINARY-+ '1
; (ACL2_*1*_ACL2::FOO (ACL2_*1*_LISP::CDR X))))))
; (LET ((ACL2_*1*_ACL2::FOO (SYMBOL-CLASS 'FOO (W *THE-LIVE-STATE*)))
; (GUARD-CHECKING-ON
; (F-GET-GLOBAL 'GUARD-CHECKING-ON *THE-LIVE-STATE*)))
; (COND
; ((LET ((*HARD-ERROR-RETURNS-NILP*
; (OR *HARD-ERROR-RETURNS-NILP*
; (NOT GUARD-CHECKING-ON))))
; (IF (EQ ACL2_*1*_ACL2::FOO :IDEAL)
; (ACL2_*1*_ACL2::TRUE-LISTP X) (TRUE-LISTP X)))
; (IF (EQ ACL2_*1*_ACL2::FOO :IDEAL) (ACL2_*1*_ACL2::FOO X)
; (FOO X)))
; (GUARD-CHECKING-ON
; (THROW-RAW-EV-FNCALL
; (LIST 'EV-FNCALL-GUARD-ER 'FOO (LIST X) '(TRUE-LISTP X)
; '(NIL))))
; (T (ACL2_*1*_ACL2::FOO X))))))
; Notice the inefficiency of needlessly checking guards in Version_2.5 in the
; :ideal case when guard-checking is off. We fix that problem in Version_2.6,
; but more importantly, we implement a "safe mode" to be used during
; macroexpansion, so that we can trust that ACL2 and Common Lisp agree when
; they are supposed to, thus avoiding the sort of problem illustrated above
; (function bar and macro mac). We make this idea precise in our discussion of
; "Guarantees", above.
; ACL2>(symbol-function 'ACL2_*1*_ACL2::FOO) ; in gcl, ACL2 Version_2.6
; (LISP:LAMBDA-BLOCK ACL2_*1*_ACL2::FOO (X)
; (LABELS ((ACL2_*1*_ACL2::FOO (X)
; (IF (ACL2_*1*_LISP::ENDP X) '3
; (ACL2_*1*_ACL2::BINARY-+ '1
; (ACL2_*1*_ACL2::FOO (ACL2_*1*_LISP::CDR X))))))
; (COND
; ((TRUE-LISTP X) (RETURN-FROM ACL2_*1*_ACL2::FOO (FOO X)))
; ((F-GET-GLOBAL 'GUARD-CHECKING-ON *THE-LIVE-STATE*)
; (RETURN-FROM ACL2_*1*_ACL2::FOO
; (THROW-RAW-EV-FNCALL
; (LIST 'EV-FNCALL-GUARD-ER 'FOO (LIST X) '(TRUE-LISTP X)
; '(NIL))))))
; (ACL2_*1*_ACL2::FOO X)))
; Next, we present a basic template (outline, really) for defining executable
; counterparts. Note that as in the code for Version_2.5, we may optimize away
; consideration of the guard when the guard is t (either implicitly or
; explicitly). Furthermore, we do some optimization when the symbol-class of
; the function is :common-lisp-compliant, as we do in Version_2.5 for :program
; vs. :logic mode.
; The template below uses some abbreviations <...>, which are defined below the
; template. See also oneify-cltl-code for more details, special cases, and
; optimizations. There we also handle the guarded-primitive-p case, which
; pertains to built-in defined functions that need to be responsible for
; checking their guards in safe-mode. That does not however deal with true
; primitives, which are not defined. For those, safe-mode is handled with
; calls of gv in their defun-*1* definitions.
; Finally, this template is only approximate and not necessarily up-to-date.
; It is intended to give a sense of how oneify-cltl-code works; see the code
; for up-to-date comments. You may be better off simply by tracing
; oneify-cltl-code with hiding of the wrld argument, for example with
; (trace! (oneify-cltl-code :entry t :native t))
; -- and then executing each of the following test cases. Follow each of these
; with (trace$ foo) to see oneification for allowing tracing of recursive calls
; when guard-checking is :none. Then execute :u before the next defun. Oh,
; and try guard violations too.
; (defun foo (x)
; (declare (xargs :guard t))
; (if (natp x) (if (zp x) 0 (* x (foo (1- x)))) 0))
; (defun foo (x)
; (declare (xargs :guard t :verify-guards nil))
; (if (natp x) (if (zp x) 0 (* x (foo (1- x)))) 0))
; (defun foo (x)
; (declare (xargs :guard t :mode :program))
; (if (natp x) (if (zp x) 0 (* x (foo (1- x)))) 0))
;
; (defun foo (x)
; (declare (xargs :guard (natp x)))
; (if (zp x) 0 (* x (foo (1- x)))))
; (defun foo (x)
; (declare (xargs :guard (natp x) :mode :program))
; (if (zp x) 0 (* x (foo (1- x)))))
; (defun foo (x)
; (declare (xargs :guard (natp x) :verify-guards nil))
; (if (zp x) 0 (* x (foo (1- x)))))
;
; ; This one reports a guard violation with guard-checking set to :all but not
; ; when it is set to t.
; (defun foo (x)
; (declare (xargs :guard (evenp x) :verify-guards nil))
; (if (zp x) 0 (* x (foo (1- x)))))
;
; (defun foo (x)
; (if (zp x) 0 (* x (foo (1- x)))))
; (defun <*1*fn> <formals>
; <wormhole-test-for-functions-with-user-stobjs>
; (let ((<class> (symbol-class '<fn> (w *the-live-state*))))
; (cond ((eq <class> :common-lisp-compliant)
; (cond
; ((or (equal <guard> *t*)
; (not (eq <guard-checking-on> :none))
; (acl2-system-namep name wrld))
; (cond (<guard> ; avoid <*1*guard> since guard is known compliant
; (cond (<live-stobjp-test> ; test can often be omitted
; (return-from <*1*fn> (<fn> . <formals>)))))
; (<guard-checking-on> <fail_guard>))
;
; ; Otherwise fall through to final call of *1* function.
;
; )
;
; ; The next case is not needed for our guarantees. Rather, it ensures that
; ; evaluation with guard checking on really does check guards at each function
; ; call.
;
; ((and <guard-checking-on>
; (not <*1*guard>))
; <fail_guard>)
; ((or (eq <guard-checking-on> :all)
; (and <safe>
; (eq <class> :program)))
; (return-from <*1*fn> *1*body))
; ((eq <class> :program)
; (return-from <*1*fn> (<fn> . <formals>)))
;
; ; If we fall through to here, then we compute in the logic, avoiding further
; ; guard checks in recursive calls (where a "special" declaration will take
; ; care of this if we are in a mutual-recursion nest).
;
; (maybe-warn-for-guard <fn>)))
;
; ; In the case (eq <class> :program), we conclude by laying down the call (<fn>
; ; . <formals>). Otherwise, we lay down the following code.
;
; (labels
;
; ; The following local definition of <*1*fn> executes calls of <fn> in the
; ; logic, without guard-checking (except for primitives under safe-mode; see
; ; below). Note that it is always legitimate for this local function to cause
; ; an error, so if we want to save space we can fail here, in particular for
; ; :program mode functions encountered during the boot-strap, at least outside
; ; (say) axioms.lisp -- although that would presumably eliminate the ability to
; ; call those functions in macro definitions.
;
; ((<*1*fn>
; <formals>
;
; ; Certain functions can take the live state as an argument, and yet do
; ; not ``properly'' handle it in their logic code. Consider for
; ; example (princ$ '(a b) *standard-co* state). With guard-checking
; ; off, and a live state, this form used to cause a hard error. The
; ; problem was that the logical body of princ$ (actually, its
; ; oneification) was being executed. Consider calling a function such
; ; as open-output-channels, which is really a call of nth, on a live
; ; state! We believe that our problem is solved by disallowing calls
; ; of certain built-in functions on a live state argument, when passing
; ; to their oneified bodies. These functions are those in
; ; *super-defun-wart-stobjs-in-alist*, since these are the ones that
; ; pass the state on as though it were a legitimate state object, i.e.,
; ; to functions that take non-state values as arguments.
;
; ; Other functions, such as those defined under defstobj, may have a stobj
; ; name as an argument but do not have an appropriate 'stobjs-in
; ; setting in the world, because we have not yet declared that the
; ; stobj name is a stobj. These latter functions are characterized by
; ; having a non-nil stobj-flag, said flag being the stobj name. We
; ; compute here the appropriate stobjs-in.
;
; <fail_if_live_stobj> ; laid down only in cases as described above
; *1*body))
; (*1*fn . formals)))))
;
; WHERE:
;
; <*1*guard>
; =
; oneification of guard
;
; <formals>
; =
; list of formals, e.g., (x1 ... xn)
;
; <guard-checking-on>
; =
; (f-get-global 'guard-checking-on *the-live-state*)
;
; <guard>
; =
; [guard of the function being defined]
;
; <fail_guard>
; =
; (throw-raw-ev-fncall
; (list 'ev-fncall-guard-er '<fn> (list x) '<guard> '(nil) nil))
;
; <fail_safe>
; =
; (throw-raw-ev-fncall
; (list 'ev-fncall-guard-er '<fn> (list x) '<guard> '(nil) t))
;
; <class>
; =
; <*1*fn>
;
; <*1*fn>
; =
; (*1*-symbol <fn>)
;
; <fn>
; =
; [function symbol being defined]
;
; <safe>
; =
; (f-get-global 'safe-mode *the-live-state*)
;
; <fail_if_live_stobj>
; =
; code for protecting against executing <*1*body> on live stobjs
;
; <live-stobjp-test>
; =
; test that all of the stobj parameters to the function are indeed the "live"
; stobjs. This is required because the Common Lisp code for stobj access and
; update functions assumes, starting in v2-8, that user-defined stobj parameters
; are live, a restriction enforced by the corresponding *1* functions before
; passing to Common Lisp.
;
; <wormhole-test-for-functions-with-user-stobjs>
; =
; a test that is generated to check if one is evaluating a function with
; user-defined stobjs in a wormhole (no wormhole test is performed if the
; function does not take user-defined stobjs as arguments). Only proper updates
; on state are allowed inside wormholes since the wormhole can properly "undo"
; these side effects upon completion. No such mechanism exists for user-defined
; stobjs and thus the test. Before v2-8, this wormhole test was performed in the
; stobj update primitives directly, but it is now performed in the *1* function
; as a matter of efficiency. The exclusion of read access of user-defined stobjs
; in wormholes simplifies the code to generate the *1* body and while technically
; unnecessary, does not seem to be a relevant over-restriction in practice.
; F. Remarks
; Remark 1. Notice that safe mode does not by itself force guard-checking in
; all cases, nor does soundness of safe mode require guard-checking as long as
; we do check guards when evaluating calls of functions that are built into
; Common Lisp. We ensure this in the macro gv, which is changed in Version_2.6
; to cause an error when in safe mode.
; Remark 2. Consider, in the body of *1*fn, the case that <guard-checking-on>
; holds. If we were to replace it with (or guard-checking-on program) then we
; would always check guards when in program mode, which would give backward
; compatibility: this scheme would behave exactly as the scheme from
; Version_2.5 for and before did when the new scheme is used in other than safe
; mode. But we have decided that starting with Version_2.6, we will no longer
; check guards for :program mode functions when 'guard-checking-on has value
; nil (though starting with Version_3.0 you can get this effect when
; 'guard-checking-on has value :none). After all, even with guard-checking on
; in Version_2.5 you can get nasty Lisp breaks, since we slip directly into
; Common Lisp when a guard holds even though guards cannot be verified for
; :program mode functions.
; End of Essay on Evaluation in ACL2
; ONEIFICATION
; Here are the *1* functions. They should be kept in sync with
; *primitive-formals-and-guards*. We could probably get by with avoiding
; defining those in the list *oneify-primitives*, for example since want to
; avoid calling "slow" functions, e.g., *1*cons instead of cons. But we prefer
; to follow the simple rule that every function has a *1* counterpart, which is
; easy to remember. Moreover, in the case of IF we really do want to define
; *1*if to cause an error, because we insist that the oneification of if remain
; lazy.
; WARNING: Any hand-coded *1* definitions for other than the primitives, such
; as the one for mv-list (see below), must be handled in add-trip and
; compile-uncompiled-*1*-defuns (see the handling there of mv-list).
(defmacro gv (fn args val)
(sublis `((funny-fn . ,fn)
(funny-args . ,args))
`(let ((gc-on (not (gc-off *the-live-state*))))
(if (or gc-on
(f-get-global 'safe-mode *the-live-state*))
(throw-raw-ev-fncall
(list 'ev-fncall-guard-er
'funny-fn
,(cons 'list 'funny-args)
(guard-raw 'funny-fn (w *the-live-state*))
(stobjs-in 'funny-fn (w *the-live-state*))
(not gc-on)))
,val))))
; We must hand-code the *1* functions for mv-list and return-last, because
; otherwise they will simply call mv-list and return-last (resp.), which can be
; wrong: in the case of return-last, we need the first argument to be a quotep
; for the raw-Lisp macro return-last to do more than lay down a progn.
(defun-*1* mv-list (input-arity x)
(declare (ignore input-arity))
x)
(defun-*1* return-last (fn x y)
(cond ((and (equal fn 'mbe1-raw)
(f-get-global 'safe-mode *the-live-state*))
; Since return-last is a special form, we can decide how we want to view it
; with respect to guards. We have decided to check its guard only when in safe
; mode, which is the minimal case needed in order to fix a soundness bug
; related to mbe; see note-4-3. The following log shows what happened in a
; preliminary implementation of that bug fix, in which oneify laid down a
; *1*return-last call unconditionally; note the unfortunate call of the :exec
; function, f2. Of course, that call is not the fault of the old version of
; *1*return-last, which is a function called after its arguments are already
; evaluated; there are other places (ev-rec and oneify) where we avoid even
; calling *1*return-last. But if we do get to this call, for example by way of
; expand-abbreviations calling ev-fncall, at least we can limit the equality
; check here to the case of safe-mode (which is presumably nil, for example,
; under expand-abbreviations).
; ACL2 !>(defn f1 (x) x)
; [[... output omitted ...]]
; F1
; ACL2 !>(defn f2 (x) x)
; [[... output omitted ...]];
; F2
; ACL2 !>(defun f (x) (mbe :logic (f1 x) :exec (f2 x)))
; [[... output omitted ...]]
; F
; ACL2 !>(trace$ f f1 f2)
; ((F) (F1) (F2))
; ACL2 !>(f 3)
; 1> (ACL2_*1*_ACL2::F 3)
; 2> (ACL2_*1*_ACL2::F2 3)
; 3> (F2 3)
; <3 (F2 3)
; <2 (ACL2_*1*_ACL2::F2 3)
; 2> (ACL2_*1*_ACL2::F1 3)
; 3> (F1 3)
; <3 (F1 3)
; <2 (ACL2_*1*_ACL2::F1 3)
; <1 (ACL2_*1*_ACL2::F 3)
; 3
; ACL2 !>
(if (equal x y)
y
(gv return-last (fn x y)
y)))
(t y)))
; We must hand-code the *1* function for wormhole-eval because if it were
; automatically generated it would look like this:
; (defun ACL2_*1*_ACL2::WORMHOLE-EVAL (qname qlambda free-vars)
; (wormhole-eval qname qlambda free-vars))
; (To see where this code would be generated, find the comment beginning
; "Optimization in a common case" in oneify-cltl-code.)
; But the body of the *1* defun above violates the requirement that the
; wormhole-eval macro always be applied to a quoted name and lambda expression.
; In particular, if the default optimized code above is generated and then
; given to raw lisp, a hard error results when the wormhole-eval macro tries to
; cadr into qname. So what should be here? Intuitively we ought to lay down
; code that checks that qlambda is a well-formed and appropriate lambda
; expression and then apply it to the wormhole status of the wormhole with the
; name qname. But in fact this *1* function should never be called except from
; within the theorem prover when we are evaluating wormhole-eval on quoted
; constants. Thus, we just return nil, it's logical value, without attempting
; to do any of the wormhole stuff.
(defun-*1* wormhole-eval (qname qlambda free-vars)
(declare (ignore qname qlambda free-vars))
nil)
; Keep the rest of these in sync with the completion-of-* axioms in
; axioms.lisp.
(defun-*1* acl2-numberp (x)
(numberp x))
(defun-*1* binary-* (x y)
(the number
(if (numberp x)
(if (numberp y)
(* x y)
(gv binary-* (x y) 0))
(gv binary-* (x y) 0))))
(defun-*1* binary-+ (x y)
(the number
(if (numberp x)
(if (numberp y)
(+ (the number x) (the number y))
(gv binary-+ (x y) x))
(gv binary-+ (x y)
(if (numberp y)
y
0)))))
(defun-*1* unary-- (x)
(the number
(if (numberp x)
(- x)
(gv unary-- (x) 0))))
(defun-*1* unary-/ (x)
(the number
(if (and (numberp x) (not (= x 0)))
(/ x)
(gv unary-/ (x) 0))))
(defun-*1* < (x y)
; If one regards (gv op args val) simply as val, then we can prove that
; the body below is equivalent to the let-expression used for val. Put
; another way, if we use << as the "familiar" less-than on the rationals
; then this definition of < is equivalent to
; (< x y) = (let ((x1 (if (acl2-numberp x) x 0))
; (y1 (if (acl2-numberp y) y 0)))
; (or (<< (realpart x1) (realpart y1))
; (and (= (realpart x1) (realpart y1))
; (<< (imagpart x1) (imagpart y1)))))
; The consideration of the case where both x and y are rational is just
; an optimization.
(if (and (rationalp x)
(rationalp y))
(< (the rational x) (the rational y))
(gv < (x y)
(let ((x1 (if (numberp x) x 0))
(y1 (if (numberp y) y 0)))
(or (< (realpart x1) (realpart y1))
(and (= (realpart x1) (realpart y1))
(< (imagpart x1) (imagpart y1))))))))
(defun-*1* apply (x y)
(error "We have called apply on ~s and ~s, but we thought we were rid of apply."
x y))
(defun-*1* bad-atom<= (x y)
(cond ((and (bad-atom x) (bad-atom y))
; The following should never happen.
(error "We have called (the executable-counterpart of) bad-atom<= on ~
~s and ~s, but bad-atom<= has no Common Lisp definition."
x y))
(t (gv bad-atom<= (x y) nil))))
(defun-*1* car (x)
(cond
((consp x)
(car x))
((null x)
nil)
(t (gv car (x) nil))))
(defun-*1* cdr (x)
(cond
((consp x)
(cdr x))
((null x)
nil)
(t (gv cdr (x) nil))))
(defun-*1* char-code (x)
(if (characterp x)
(char-code x)
(gv char-code (x) 0)))
(defun-*1* characterp (x)
(characterp x))
(defun-*1* code-char (x)
(if (and (integerp x)
(>= x 0)
(< x 256))
(code-char x)
(gv code-char (x) (code-char 0))))
(defun-*1* complex (x y)
(complex (the rational (if (rationalp x) x (gv complex (x y) 0)))
(the rational (if (rationalp y) y (gv complex (x y) 0)))))
(defun-*1* complex-rationalp (x)
(complexp x))
;; Historical Comment from Ruben Gamboa:
;; I added this function to recognize the complex numbers.
#+:non-standard-analysis
(defun-*1* complexp (x)
(complexp x))
(defun-*1* coerce (x y)
(cond
((equal y 'list)
(if (stringp x)
(coerce x 'list)
(gv coerce (x y) nil)))
((character-listp x)
(if (equal y 'string)
(coerce x 'string)
(gv coerce (x y) (coerce x 'string))))
(t
(gv coerce (x y)
(coerce (make-character-list x) 'string)))))