-
Notifications
You must be signed in to change notification settings - Fork 0
/
basis-a.lisp
8679 lines (7549 loc) · 359 KB
/
basis-a.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) 2022, 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.
; The code in this file was originally placed in several different source
; files, but was moved here in order to support the creation of "toothbrush"
; applications -- that is, so that fewer ACL2 source files need to be loaded in
; order to support ACL2 applications. See community books file
; books/system/toothbrush/README.
(in-package "ACL2")
; Case-match
(defun equal-x-constant (x const)
; x is an arbitrary term, const is a quoted constant, e.g., a list of
; the form (QUOTE guts). We return a term equivalent to (equal x
; const).
(declare (xargs :guard (and (consp const)
(eq (car const) 'quote)
(consp (cdr const)))))
(let ((guts (cadr const)))
(cond ((symbolp guts)
(list 'eq x const))
((or (acl2-numberp guts)
(characterp guts))
(list 'eql x guts))
((stringp guts)
(list 'equal x guts))
(t (list 'equal x const)))))
(defun match-tests-and-bindings (x pat tests bindings)
; We return two results. The first is a list of tests, in reverse
; order, that determine whether x matches the structure pat. We
; describe the language of pat below. The tests are accumulated onto
; tests, which should be nil initially. The second result is an alist
; containing entries of the form (sym expr), suitable for use as the
; bindings in the let we generate if the tests are satisfied. The
; bindings required by pat are accumulated onto bindings and thus are
; reverse order, although their order is actually irrelevant.
; For example, the pattern
; ('equal ('car ('cons u v)) u)
; matches only first order instances of (EQUAL (CAR (CONS u v)) u).
; The pattern
; ('equal (ev (simp x) a) (ev x a))
; matches only second order instances of (EQUAL (ev (simp x) a) (ev x a)),
; i.e., ev, simp, x, and a are all bound in the match.
; In general, the match requires that the cons structure of x be isomorphic
; to that of pat, down to the atoms in pat. Symbols in the pat denote
; variables that match anything and get bound to the structure matched.
; Occurrences of a symbol after the first match only structures equal to
; the binding. Non-symbolp atoms match themselves.
; There are some exceptions to the general scheme described above. A cons
; structure starting with QUOTE matches only itself. A cons structure of the
; form (QUOTE~ sym), where sym is a symbol, is like (QUOTE sym) except it
; matches any symbol with the same symbol-name as sym. The symbols nil and t,
; and all symbols whose symbol-name starts with #\* match only structures equal
; to their values. (These symbols cannot be legally bound in ACL2 anyway, so
; this exceptional treatment does not restrict us further.) Any symbol
; starting with #\! matches only the value of the symbol whose name is obtained
; by dropping the #\!. This is a way of referring to already bound variables
; in the pattern. Finally, the symbol & matches anything and causes no binding.
(declare (xargs :guard (symbol-doublet-listp bindings)))
(cond
((symbolp pat)
(cond
((or (eq pat t)
(eq pat nil)
(keywordp pat))
(mv (cons (list 'eq x pat) tests) bindings))
((let ((len (length (symbol-name pat))))
(and (> len 0)
(eql #\* (char (symbol-name pat) 0))
(eql #\* (char (symbol-name pat) (1- len)))))
(mv (cons (list 'equal x pat) tests) bindings))
((and (> (length (symbol-name pat)) 0)
(eql #\! (char (symbol-name pat) 0)))
(mv (cons (list 'equal x
(intern-in-package-of-symbol
(subseq (symbol-name pat)
1
(length (symbol-name pat)))
pat))
tests)
bindings))
((eq pat '&) (mv tests bindings))
(t (let ((binding (assoc-eq pat bindings)))
(cond ((null binding)
(mv tests (cons (list pat x) bindings)))
(t (mv (cons (list 'equal x (cadr binding)) tests)
bindings)))))))
((atom pat)
(mv (cons (equal-x-constant x (list 'quote pat)) tests)
bindings))
((and (eq (car pat) 'quote)
(consp (cdr pat))
(null (cddr pat)))
(mv (cons (equal-x-constant x pat) tests)
bindings))
((and (eq (car pat) 'quote~)
(consp (cdr pat))
(symbolp (cadr pat))
(null (cddr pat)))
(mv (cons (list 'symbol-name-equal x (symbol-name (cadr pat))) tests)
bindings))
(t (mv-let (tests1 bindings1)
(match-tests-and-bindings (list 'car x) (car pat)
(cons (list 'consp x) tests)
bindings)
(match-tests-and-bindings (list 'cdr x) (cdr pat)
tests1 bindings1)))))
(defun match-clause (x pat forms)
(declare (xargs :guard t))
(mv-let (tests bindings)
(match-tests-and-bindings x pat nil nil)
(list (if (null tests)
t
(cons 'and (reverse tests)))
(cons 'let (cons (reverse bindings) forms)))))
(defun match-clause-list (x clauses)
(declare (xargs :guard (alistp clauses)))
(cond ((consp clauses)
(if (eq (caar clauses) '&)
(list (match-clause x (caar clauses) (cdar clauses)))
(cons (match-clause x (caar clauses) (cdar clauses))
(match-clause-list x (cdr clauses)))))
(t '((t nil)))))
(defmacro case-match (&rest args)
(declare (xargs :guard (and (consp args)
(symbolp (car args))
(alistp (cdr args))
(null (cdr (member-equal (assoc-eq '& (cdr args))
(cdr args)))))))
(cons 'cond (match-clause-list (car args) (cdr args))))
; Essay on Wormholes
; Once upon a time (Version 3.6 and earlier) the wormhole function had a
; pseudo-flg argument which allowed the user a quick way to determine whether
; it was appropriate to incur the expense of going into the wormhole. The idea
; was that the form could have one a free var in it, wormhole-output, and that
; when it was evaluated in raw Lisp that variable was bound to the last value
; returned by the wormhole. Since wormhole always returned nil anyway, this
; screwy semantics didn't matter. However, it was implemented in such a way
; that a poorly constructed pseudo-flg could survive guard verification and yet
; cause a hard error at runtime because during guard verification
; wormhole-output was bound to NIL but in actual evaluation it was entirely
; under the control of the wormhole forms.
; To fix this we have introduced wormhole-eval. It takes two important
; arguments, the name of the wormhole and a lambda expression. Both must be
; quoted. The lambda may have at most one argument but the body may contain
; any variables available in the environment of the wormhole-eval call. (A
; third argument to wormhole-eval is an arbitrary form that uses all the free
; vars of the lambda, thus insuring that translate will cause an error if the
; lambda uses variables unavailable in the context.) The body of the lambda
; must be a single-valued, non-state, non-stobj term.
; The idea is that the lambda expression is applied to the last value of the
; wormhole output and its value is assigned as the last value of the wormhole
; output. Wormhole-eval always returns nil. Translation of a wormhole-eval
; call enforces these restrictions. Furthermore, it translates the body of the
; lambda (even though the lambda is quoted). This is irrelevant since the
; wormhole-eval returns nil regardless of the lambda expression supplied.
; Similarly, translation computes an appropriate third argument to use all the
; free vars, so the user may just write nil there and a suitable form is
; inserted by translate.
; We arrange for wormhole-eval to be a macro in raw lisp that really does what
; is said above.
; To make it bullet-proof, when we generate guard clauses we go inside the
; lambda, generating a new variable symbol to use in place of the lambda formal
; denoting the last value of the wormhole output. Thus, if guard clauses can be
; verified, it doesn't matter what the wormhole actually returns as its value.
; Ev-rec, the interpreter for terms, treats wormhole-eval specially in the
; expected way, as does oneify. Thus, both interpreted and compiled calls of
; wormhole-eval are handled, and guard violations are handled politely.
; Now, how does this allow us to fix the wormhole pseudo-flg problem?
; The hidden global variable in Lisp used to record the status of the various
; wormholes is called *wormhole-status-alist*. The entry in this alist for
; a particular wormhole will be called the wormhole's ``status.'' The lambda
; expression in wormhole-eval maps the wormhole's status to a new status.
; The status of a wormhole is supposed to be a cons whose car is either :ENTER
; or :SKIP. However, in the absence of verifying the guards on the code inside
; wormholes and in light of the fact that users can set the status by
; manipulating wormhole-status in the wormhole it is hard to ensure that the
; status is always as supposed. So we code rather defensively.
; When the ``function'' wormhole is called it may or may not actually enter a
; wormhole. ``Entering'' the wormhole means invoking the form on the given
; input, inside a side-effects undoing call of ld. That, in turn, involves
; setting up the ld specials and then reading, translating, and evaluating
; forms. Upon exit, cleanup must be done. So entering is expensive.
; Whether it enters the wormhole or not depends on the wormhole's status, and
; in particular it depends on what we call the wormhole's ``entry code''
; computed from the status as follows.
; If the wormhole's status satisfies wormhole-statusp then the situation is
; simple: wormhole enters the wormhole if the status is :ENTER and doesn't if
; the status is :SKIP. But we compute the entry code defensively: the entry
; code is :SKIP if and only if the wormhole's status is a cons whose car is
; :SKIP. Otherwise, the entry code is :ENTER.
; If we enter the wormhole, we take the wormhole input argument and stuff it
; into (@ wormhole-input), allowing the user to see it inside the ld code. We
; take the wormhole status and stuff it into (@ wormhole-status), allowing the
; user to see it and probably change it with (assign wormhole-status...). When
; we exit ld, we take (@ wormhole-status) and put it back into the hidden
; *wormhole-status-alist*.
; One subtlety arises: How to make wormholes re-entrant... The problem is that
; sometimes the current status is in the hidden alist and other times it is in
; (@ wormhole-status). So when we try to enter a new wormhole from within a
; wormhole -- which always happens by calling wormhole-eval -- the first thing
; we do is stuff the current (@ wormhole-status) into the hidden
; *wormhole-status-alist*. This means that the lambda expression for the new
; entrance is applied, it is applied to the ``most recent'' value of the status
; of that particular wormhole. The natural undoing of wormhole effects
; implements the restoration of (@ wormhole-status) upon exit from the
; recursive wormhole.
; If we wanted to convert our system code to logic mode we would want to verify
; the guards of the lambda bodies and the wormhole-status after ld. See the
; comment in push-accp. Here is a proposal for how to do that. First, insist
; that wormhole names are symbols. Indeed, they must be one argument,
; guard-verified Boolean functions. The guard for a call of wormhole-eval on a
; wormhole named foo should include the conjunct (foo nil) to ensure that the
; initial value of the status is acceptable. The guard on the body of (lambda
; (whs) body) should be extended to include the hypothesis that (foo whs) is
; true and that (foo whs) --> (foo body) is true. We should then change
; wormhole so that if it calls ld it tests foo at runtime after the ld returns
; so we know that the final status satisfies foo. If we do this we can safely
; assume that every status seen by a lambda body in wormhole-eval will satisfy
; the foo invariant.
(defun wormhole-statusp (whs)
(declare (xargs :mode :logic :guard t))
(or (equal whs nil)
(and (consp whs)
(or (eq (car whs) :ENTER)
(eq (car whs) :SKIP)))))
(defun wormhole-entry-code (whs)
; Keep this function in sync with the inline code in wormhole1.
(declare (xargs :mode :logic :guard t))
(if (and (consp whs)
(eq (car whs) :SKIP))
:SKIP
:ENTER))
(defun wormhole-data (whs)
(declare (xargs :mode :logic :guard t))
(if (consp whs)
(cdr whs)
nil))
(defun set-wormhole-entry-code (whs code)
(declare (xargs :mode :logic
:guard (or (eq code :ENTER)
(eq code :SKIP))))
(if (consp whs)
(if (eq (car whs) code)
whs
(cons code (cdr whs)))
(if (eq code :enter)
whs
(cons :skip whs))))
(defun set-wormhole-data (whs data)
(declare (xargs :mode :logic :guard t))
(if (consp whs)
(if (equal (cdr whs) data)
whs
(cons (car whs) data))
(cons :enter data)))
(defun make-wormhole-status (old-status new-code new-data)
(declare (xargs :mode :logic
:guard (or (eq new-code :ENTER)
(eq new-code :SKIP))))
(if (consp old-status)
(if (and (eq new-code (car old-status))
(equal new-data (cdr old-status)))
old-status
(cons new-code new-data))
(cons new-code new-data)))
; (defthm wormhole-status-guarantees
; (if (or (eq code :enter)
; (eq code :skip))
; (and (implies (wormhole-statusp whs)
; (wormhole-statusp (set-wormhole-entry-code whs code)))
; (implies (wormhole-statusp whs)
; (wormhole-statusp (set-wormhole-data whs data)))
; (equal (wormhole-entry-code (set-wormhole-entry-code whs code))
; code)
; (equal (wormhole-data (set-wormhole-data whs data))
; data)
; (implies (wormhole-statusp whs)
; (equal (wormhole-data (set-wormhole-entry-code whs code))
; (wormhole-data whs)))
; (implies (wormhole-statusp whs)
; (equal (wormhole-entry-code
; (set-wormhole-data whs data))
; (wormhole-entry-code whs)))
; (implies (wormhole-statusp whs)
; (wormhole-statusp (make-wormhole-status whs code data)))
; (equal (wormhole-entry-code (make-wormhole-status whs code data))
; code)
; (equal (wormhole-data (make-wormhole-status whs code data))
; data))
; t)
; :rule-classes nil)
;
; (verify-guards wormhole-status-guarantees)
; In particular, given a legal code, set-wormhole-entry-code preserves
; wormhole-statusp and always returns an object with the given entry code
; (whether the status was well-formed or not). Furthermore, the guards on
; these functions are verified. Thus, they can be called safely even if the
; user has messed up our wormhole status. Of course, if the user has messed up
; the status, there is no guarantee about what happens inside the wormhole.
(defun tree-occur-eq (x y)
; Does symbol x occur in the cons tree y?
(declare (xargs :guard (symbolp x)))
(cond ((consp y)
(or (tree-occur-eq x (car y))
(tree-occur-eq x (cdr y))))
(t (eq x y))))
#+acl2-loop-only
(defun wormhole-eval (qname qlambda free-vars)
; A typical call of this function is
; (wormhole-eval 'my-wormhole
; '(lambda (output) (p x y output))
; (list x y))
; And the pragmatic semantics is that the lambda expression is applied to the
; last output of the wormhole my-wormhole, the result of of the application is
; stuffed back in as the last output, and the function logically returns nil.
; Note that free vars in the lambda must listed. This is so that the free vars
; of this wormhole-eval expression consists of the free vars of the lambda,
; even though the lambda appears quoted. Translate automatically replaces the
; lambda expression constant by the translated version of that same constant,
; and it replaces the supposed list of free vars by the actual free vars. So
; in fact the user calling wormhole-eval can just put nil in the free-vars arg
; and let translate fill it in. Translate can mangle the arguments of
; wormhole-eval because it always returns nil, regardless of its arguments.
; The guard is declared below to be t but actually we compute the guard for the
; body of the quoted lambda, with some fiddling about the bound variable.
; (Remember: the quoted lambda of wormhole-eval is unrelated to apply$.)
(declare (xargs :mode :logic
:guard t)
(ignore qname qlambda free-vars))
nil)
(deflock *wormhole-lock*)
#-acl2-loop-only
(defun put-assoc-equal-destructive (key val alist)
(let ((pair (assoc-equal key alist)))
(cond (pair (setf (cdr pair) val)
alist)
(t (acons key val alist)))))
(defun wormhole-eval-early-null-exit-p (qlambda)
; This function recognizes quoted lambdas that are subject to the wormhole-eval
; optimization of returning immediately when the wormhole-data is nil, which is
; reasonable since the old and new status are then equal.
(case-match qlambda
(('quote ('lambda (whs)
('let ((info ('wormhole-data whs)))
('cond (('null info) whs) . &))))
(declare (ignore info whs))
t)
(& nil)))
#-acl2-loop-only
(defmacro wormhole-eval (qname qlambda free-vars)
(declare (xargs :guard t))
; All calls of wormhole-eval that have survived translation are of a special
; form. Qname is a quoted object (used as the name of a wormhole), and qlambda
; is of one of the two forms:
; (i) (quote (lambda (whs) body)), or
; (ii) (quote (lambda () body))
; where whs (``wormhole status'') is a legal variable symbol, body is a fully
; translated term that may involve whs and other variables which returns one
; result. We furthermore know that the free vars in the lambda are the free
; vars of the term free-vars, which is typically just a list-expression of
; variable names supplied by translate. Finally, we know that whs appears as
; the lambda formal iff it is used in body.
; Wormholes may have arbitrary objects for names, so qname is not necessarily a
; quoted symbol. This may be the first entry into the wormhole of that name,
; in which case the most recent output of the wormhole is understood to be nil.
; Logically this function always returns nil. Actually, it applies the lambda
; expression to either (i) ``the most recent output'' of the named wormhole or
; (ii) no arguments, appropriately, and stores the result as the most recent
; output, and then returns nil.
; For efficiency we use put-assoc-equal-destructive below instead of put-assoc.
; When considering a similar use of put-assoc-equal-destructive elsewhere --
; specifically, in ev-rec and in a cleanup form in wormhole1 -- then we should
; think about whether locks might be needed for ACL2(p). We do have a lock
; here, by default.
(let* ((whs (car (cadr (cadr qlambda)))) ; non-nil in Case (i) only
(early-null-exit-p (and whs
(wormhole-eval-early-null-exit-p qlambda)))
(val (gensym))
(form1
`(progn
(cond (*wormholep*
(setq *wormhole-status-alist*
(put-assoc-equal-destructive
(f-get-global 'wormhole-name
*the-live-state*)
(f-get-global 'wormhole-status
*the-live-state*)
*wormhole-status-alist*))))
(let* ((*wormholep* t)
,@(and whs ; Case (i)
(not early-null-exit-p) ; otherwise bind whs later
`((,whs
(cdr (assoc-equal ,qname
*wormhole-status-alist*)))))
(,val ,(caddr (cadr qlambda))))
; At one time we skipped the following setq in the case that (equal ,whs ,val),
; where ,whs was unconditionally bound above. However, that equality test can
; be expensive, so we avoid it.
(setq *wormhole-status-alist*
(put-assoc-equal-destructive ,qname
,val
*wormhole-status-alist*))
nil)))
(form2 (cond ((tree-occur-eq :no-wormhole-lock free-vars)
form1)
(t `(with-wormhole-lock ,form1)))))
(cond (early-null-exit-p ; hence whs is non-nil
`(let ((,whs (cdr (assoc-equal ,qname
*wormhole-status-alist*))))
(cond ((null (wormhole-data ,whs))
; Wormhole-data doesn't change (see wormhole-eval-early-null-exit-p), so we
; simply return.
nil)
(t ,form2))))
(t form2))))
(defmacro wormhole (name entry-lambda input form
&key
(current-package 'same current-packagep)
(useless-runes 'same useless-runesp)
(ld-skip-proofsp 'same ld-skip-proofspp)
(ld-redefinition-action 'save ld-redefinition-actionp)
(ld-prompt ''wormhole-prompt)
(ld-missing-input-ok 'same ld-missing-input-okp)
(ld-pre-eval-filter 'same ld-pre-eval-filterp)
(ld-pre-eval-print 'same ld-pre-eval-printp)
(ld-post-eval-print 'same ld-post-eval-printp)
(ld-evisc-tuple 'same ld-evisc-tuplep)
(ld-error-triples 'same ld-error-triplesp)
(ld-error-action 'same ld-error-actionp)
(ld-query-control-alist 'same ld-query-control-alistp)
(ld-verbose 'same ld-verbosep)
(ld-user-stobjs-modified-warning ':same))
; Warning: Keep this in sync with f-get-ld-specials, f-put-ld-specials,
; *initial-ld-special-bindings*, ld-alist-raw, chk-acceptable-ld-fn1-pair, and
; ld.
`(with-wormhole-lock
(prog2$
(wormhole-eval ,name ,entry-lambda
; It is probably harmless to allow a second lock under the one above, but there
; is no need, so we avoid it.
:no-wormhole-lock)
(wormhole1
,name
,input
,form
(list
,@(append
(if current-packagep
(list `(cons 'current-package ,current-package))
nil)
(if useless-runesp
(list `(cons 'useless-runes ,useless-runes))
nil)
(if ld-skip-proofspp
(list `(cons 'ld-skip-proofsp ,ld-skip-proofsp))
nil)
(if ld-redefinition-actionp
(list `(cons 'ld-redefinition-action
,ld-redefinition-action))
nil)
(list `(cons 'ld-prompt ,ld-prompt))
(if ld-missing-input-okp
(list `(cons 'ld-missing-input-ok ,ld-missing-input-ok))
nil)
(if ld-pre-eval-filterp
(list `(cons 'ld-pre-eval-filter ,ld-pre-eval-filter))
nil)
(if ld-pre-eval-printp
(list `(cons 'ld-pre-eval-print ,ld-pre-eval-print))
nil)
(if ld-post-eval-printp
(list `(cons 'ld-post-eval-print ,ld-post-eval-print))
nil)
(if ld-evisc-tuplep
(list `(cons 'ld-evisc-tuple ,ld-evisc-tuple))
nil)
(if ld-error-triplesp
(list `(cons 'ld-error-triples ,ld-error-triples))
nil)
(if ld-error-actionp
(list `(cons 'ld-error-action ,ld-error-action))
nil)
(if ld-query-control-alistp
(list `(cons 'ld-query-control-alist ,ld-query-control-alist))
nil)
(if ld-verbosep
(list `(cons 'ld-verbose ,ld-verbose))
nil)
(if (eq ld-user-stobjs-modified-warning :same)
(list `(cons 'ld-user-stobjs-modified-warning
,ld-user-stobjs-modified-warning))
nil)))))))
(defun lambda-keywordp (x)
(and (symbolp x)
(eql 1 (string<= "&" (symbol-name x)))))
(defun legal-variable-or-constant-namep (name)
; This function checks the syntax of variable or constant name
; symbols. In all cases, name must be a symbol that is not in the
; keyword package or among *common-lisp-specials-and-constants*
; (except t and nil), or in the main Lisp package but outside
; *common-lisp-symbols-from-main-lisp-package*, and that does not
; start with an ampersand. The function returns 'constant, 'variable,
; or nil.
; WARNING: T and nil are legal-variable-or-constant-nameps
; because we want to allow their use as constants.
; We now allow some variables (but still no constants) from the main Lisp
; package. See *common-lisp-specials-and-constants*. The following note
; explains why we have been cautious here.
; Historical Note
; This package restriction prohibits using some very common names as
; variables or constants, e.g., MAX and REST. Why do we do this? The
; reason is that there are a few such symbols, such as
; LAMBDA-LIST-KEYWORDS, which if bound or set could cause real
; trouble. Rather than attempt to identify all of the specials of
; CLTL that are prohibited as ACL2 variables, we just prohibit them
; all. One might be reminded of Alexander cutting the Gordian Knot.
; We could spend a lot of time unraveling complex questions about
; specials in CLTL or we can get on with it. When ACL2 prevents you
; from using REST as an argument, you should see the severed end of a
; once tangled rope.
; For example, akcl and lucid (and others perhaps) allow you to define
; (defun foo (boole-c2) boole-c2) but then (foo 3) causes an error.
; Note that boole-c2 is recognized as special (by
; system::proclaimed-special-p) in lucid, but not in akcl (by
; si::specialp); in fact it's a constant in both. Ugh.
; End of Historical Note.
(and (symbolp name)
(cond
((or (eq name t) (eq name nil))
'constant)
(t (let ((p (symbol-package-name name)))
(and (not (equal p "KEYWORD"))
(let ((s (symbol-name name)))
(cond
((and (not (= (length s) 0))
(eql (char s 0) #\*)
(eql (char s (1- (length s))) #\*))
; It was an oversight that a symbol with a symbol-name of "*" has always been
; considered a constant rather than a variable. The intention was to view "*"
; as a delimiter -- thus, even "**" is probably OK for a constant since the
; empty string is delimited. But it doesn't seem important to change this
; now. If we do make such a change, consider the following (at least).
; - Be sure to rule out * in any package as a stobj name, since in a signature,
; such a symbol denotes a non-stobj (see for example collect-non-* and see
; mentions of "*" in functions that involve signatures).
; - It will be necessary to update :doc defconst.
; - Fix the error message for, e.g., (defconst foo::* 17), so that it doesn't
; say "does not begin and end with the character *".
; - Make sure the error message is correct for (defun foo (*) *). It should
; probably complain about the main Lisp package, not about "the syntax of a
; constant".
(if (equal p *main-lisp-package-name*)
nil
'constant))
((and (not (= (length s) 0))
(eql (char s 0) #\&))
nil)
((equal p *main-lisp-package-name*)
(and (not (member-eq
name
*common-lisp-specials-and-constants*))
(member-eq
name
*common-lisp-symbols-from-main-lisp-package*)
'variable))
(t 'variable)))))))))
(defun legal-variablep (name)
; Name may be used as a variable if it has the syntax of a variable
; (see legal-variable-or-constant-namep) and does not have the syntax of
; a constant, i.e., does not start and end with a *.
(eq (legal-variable-or-constant-namep name) 'variable))
(defun arglistp1 (lst)
; Every element of lst is a legal-variablep.
(cond ((atom lst) (null lst))
(t (and (legal-variablep (car lst))
(arglistp1 (cdr lst))))))
(defun arglistp (lst)
(and (arglistp1 lst)
(no-duplicatesp-eq lst)))
(defun find-first-bad-arg (args)
; This function is only called when args is known to be a non-arglistp
; that is a true list. It returns the first bad argument and a string
; that completes the phrase "... violates the rules because it ...".
(declare (xargs :guard (and (true-listp args)
(not (arglistp args)))))
(cond
;;((null args) (mv nil nil)) -- can't happen, given the guard!
((not (symbolp (car args))) (mv (car args) "is not a symbol"))
((legal-constantp1 (car args))
(mv (car args) "has the syntax of a constant"))
((lambda-keywordp (car args))
(mv (car args) "is a lambda keyword"))
((keywordp (car args))
(mv (car args) "is in the KEYWORD package"))
((member-eq (car args) *common-lisp-specials-and-constants*)
(mv (car args) "belongs to the list *common-lisp-specials-and-constants* ~
of symbols from the main Lisp package"))
((member-eq (car args) (cdr args))
(mv (car args) "occurs more than once in the list"))
((and (equal (symbol-package-name (car args)) *main-lisp-package-name*)
(not (member-eq (car args)
*common-lisp-symbols-from-main-lisp-package*)))
(mv (car args) "belongs to the main Lisp package but not to the list ~
*common-lisp-symbols-from-main-lisp-package*"))
(t (find-first-bad-arg (cdr args)))))
(defun process-defabbrev-declares (decls)
(cond ((endp decls) ())
; Here we do a cheap check that the declare form is illegal. It is tempting to
; use collect-declarations, but it take state. Anyhow, there is no soundness
; issue; the user will just be a bit surprised when the error shows up later as
; the macro defined by the defabbrev is applied.
((not (and (consp (car decls))
(eq (caar decls) 'DECLARE)
(true-list-listp (cdar decls))
(subsetp-eq (strip-cars (cdar decls))
'(IGNORE IGNORABLE TYPE))))
(er hard 'process-defabbrev-declares
"In a DEFABBREV form, each expression after the argument list ~
but before the body must be of the form (DECLARE decl1 .. ~
declk), where each dcli is of the form (IGNORE ..), (IGNORABLE ~
..), or (TYPE ..). The form ~x0 is thus illegal."
(car decls)))
(t
(cons (kwote (car decls))
(process-defabbrev-declares (cdr decls))))))
(defun defabbrev1 (lst)
(declare (xargs :guard (true-listp lst)))
(cond ((null lst) nil)
(t (cons (list 'list (list 'quote (car lst)) (car lst))
(defabbrev1 (cdr lst))))))
(defmacro defabbrev (fn args &rest body)
(cond ((null body)
(er hard (cons 'defabbrev fn)
"The body of this DEFABBREV form is missing."))
((not (true-listp args))
(er hard (cons 'defabbrev fn)
"The formal parameter list for a DEFABBREV must be a true list. ~
The argument list ~x0 is thus illegal."
args))
((not (arglistp args))
(mv-let (culprit explan)
(find-first-bad-arg args)
(er hard (cons 'defabbrev fn)
"The formal parameter list for a DEFABBREV must be a ~
list of distinct variables, but ~x0 does not meet these ~
conditions. The element ~x1 ~@2."
args culprit explan)))
(t
(mv-let (doc-string-list body)
(if (and (stringp (car body))
(cdr body))
(mv (list (car body)) (cdr body))
(mv nil body))
(cond ((null body)
(er hard (cons 'defabbrev fn)
"This DEFABBREV form has a doc string but no ~
body."))
((and (consp (car (last body)))
(eq (caar (last body)) 'declare))
(er hard (cons 'defabbrev fn)
"The body of this DEFABBREV form is a DECLARE ~
form, namely ~x0. This is illegal and probably ~
is not what was intended."
(car (last body))))
(t
`(defmacro ,fn ,args
,@doc-string-list
(list 'let
(list ,@(defabbrev1 args))
,@(process-defabbrev-declares
(butlast body 1))
',(car (last body))))))))))
; Essay on Evisceration
; We have designed the pretty printer so that it can print an
; "eviscerated" object, that is, an object that has had certain
; substructures removed. We discuss the prettyprinter in the Essay on
; the ACL2 Prettyprinter. The pretty printer has a flag, eviscp,
; which indicates whether the object has been eviscerated or not. If
; not, then the full object is printed as it stands. If so, then
; certain substructures of it are given special interpretation by the
; printer. In particular, when the printer encounters a cons of the
; form (:evisceration-mark . x) then x is a string and the cons is
; printed by printing the characters in x (without the double
; gritches).
; object pretty printed output
; (:evisceration-mark . "#") #
; (:evisceration-mark . "...") ...
; (:evisceration-mark . "<state>") <state>
; (:evisceration-mark . ":EVISCERATION-MARK") :EVISCERATION-MARK
; So suppose you have some object and you want to print it, implementing
; the CLTL conventions for *print-level* and *print-length*. Then you
; must first scan it, inserting :evisceration-mark forms where
; appropriate. But what if it contains some occurrences of
; :evisceration-mark? Then you must use evisceration mechanism to print
; them correctly! Once you have properly eviscerated the object, you can
; call the prettyprinter on it, telling it that the object has been
; eviscerated. If, on the other hand, you don't want to eviscerate it,
; then you needn't sweep it to protect the native :evisceration-marks:
; just call the prettyprinter with the eviscp flag off.
(defconst *evisceration-mark* :evisceration-mark)
; Note: It is important that the evisceration-mark be a keyword.
; One reason is that (:evisceration-mark . ":EVISCERATION-MARK")
; couldn't be used to print a non-keyword because the package might
; need to be printed. Another is that we exploit the fact that no
; event name nor any formal is *evisceration-mark*. See
; print-ldd-full-or-sketch. Furthermore, if the particular keyword
; chosen is changed, alter *anti-evisceration-mark* below!
(defconst *evisceration-hash-mark* (cons *evisceration-mark* "#"))
(defconst *evisceration-ellipsis-mark* (cons *evisceration-mark* "..."))
(defconst *evisceration-world-mark*
(cons *evisceration-mark* "<world>"))
(defconst *evisceration-state-mark*
(cons *evisceration-mark* "<state>"))
(defconst *evisceration-error-triple-marks*
(list nil nil *evisceration-state-mark*))
(defconst *evisceration-hiding-mark*
(cons *evisceration-mark* "<hidden>"))
(defconst *anti-evisceration-mark*
(cons *evisceration-mark* ":EVISCERATION-MARK"))
(defmacro evisceratedp (eviscp x)
; Warning: The value of x should be a consp.
`(and ,eviscp (eq (car ,x) *evisceration-mark*)))
; Essay on Iprinting
; Through Version_3.4, when ACL2 eviscerated a form using a print-level or
; print-length from an evisc-tuple, the resulting # and ... made it impossible
; to read the form back in. We have implemented "iprinting" (think
; "interactive printing") to deal with this problem. Our implementation uses
; an "iprint array", or "iprint-ar" for short, as described below. Now, when
; iprinting is enabled, then instead of # or ... we will see #@i# for i = 1, 2,
; etc. See :doc set-iprint for more information at the user level. In brief,
; the idea is to maintain a state global 'iprint-ar whose value is an ACL2
; array that associates each such i with its hidden value. (This use of #@i#
; allows us also to think of "iprinting" as standing for "index printing" or "i
; printing".)
; We implement this idea by modifying the recursive subroutines of eviscerate
; to accumulate each association of a positive i with its hidden value. When
; fmt (or fms, etc.) is called, eviscerate-top or eviscerate-stobjs-top will be
; called in order to update the existing 'iprint-ar with those new
; associations.
; We use index 0 to store the most recent i for which #@i# has been printed,
; assuming iprinting is enabled, or else (list i) if iprinting is disabled. We
; call such i the last-index, and it is initially 0. Note that state global
; 'iprint-ar is thus always bound to an installed ACL2 array.
; When state global 'iprint-fal has a non-nil value (which is exactly when
; set-iprint was last called with a non-nil value of :share), it is a
; fast-alist that inverts iprint-ar in the following sense: for every pair (i
; . v) in iprint-ar with 1 <= i <= last-index, (v . i) is in the value of
; 'iprint-fal. See :doc set-iprint for more about :share.
; We have to face a fundamental question: Do we use acons or aset1 as we
; encounter a new form to assign to some #@i# during those recursive
; subroutines? The latter is dangerous in case we interrupt before installing
; the result in the state global. So it's tempting to use acons -- but it
; could be inefficient to compress the iprint-ar on each top-level call. So
; instead we use acons to build up a new alist from scratch. Then at the
; top level, we apply aset1 for each entry if we can do so without needing to
; ``rollover'', i.e., set the last-index back to 0; otherwise we call compress1
; rather than making a series of aset1 calls. With luck this final step will
; be fast and unlikely to be interrupted from the time the first aset1 or
; compress1 is applied until the state global 'iprint-ar is updated.
; Let's also comment on why we have a soft and a hard bound (as described in
; :doc set-iprint). In general we allow indices to increase between successive
; top-level invocations, so that the user can read back in any forms that were
; printed. But the soft bound forces a rollover at the top level of LD when the
; last-index exceeds that bound, so that we don't hold on to a potentially
; unbounded amount of space for the objects in the iprint-ar. The hard bound
; (which generally exceeds the soft bound) steps in if the last-index exceeds
; it after pretty-printing a single form. Thus, if there are large objects and
; very long runs between successive top-level forms, space can be
; reclaimed. The hard bound is therefore probably less likely to be of use.
; We maintain the invariant that the dimension of state global 'iprint-ar
; exceeds the hard bound. Thus, when we update the 'iprint-ar in the normal
; case that the hard bound is not exceeded, then the dimension will not be
; exceeded either; that is, every update will be with an index that is in
; bounds. In order to maintain this invariant, the hard bound is untouchable,
; and its setter function compresses the global iprint-ar with a new dimension
; that exceeds the specified hard bound. Therefore the hard bound must be a
; number, not nil. Notice that with this invariant, we can avoid compressing
; twice when we roll over upon exceeding the hard or soft bound: we first reset
; the last-index to 0 and then do the compression, rather than compressing once
; for the increased dimension and once for the rollover.
; We also maintain the invariant that the maximum-length of the 'iprint-ar is
; always at least four times its dimension. See the comment about this in
; rollover-iprint-ar.
; It is tempting to cause an error when the user submits a form containing some
; #@j# and #@k# such that j <= last-index < k. In such a case, k is from
; before the rollover and j is from after the rollover, so these couldn't have
; been stored during a prettyprint of the same form. By default we avoid this
; restriction, because the user might want to read a list that includes some
; forms prettyprinted before the last rollover and other forms printed after
; the last rollover. But if iprint sharing is on, then a subform that had been
; printed before rollover might include iprint indices that have since changed,
; which might be highly confusing. So we make the above restriction on indices
; when iprint sharing is on, as documented in :doc set-iprint.
; We need to be sure that the global iprint-ar is installed as an ACL2 array, in
; order to avoid slow-array-warnings. See the comment in
; push-wormhole-undo-formi for how we deal with this issue in the presence of
; wormholes.
; End of Essay on Iprinting
(defconst *sharp-atsign-ar* ; see get-sharp-atsign
(let ((dim (1+ *iprint-hard-bound-default*)))
(compress1
'sharp-atsign-ar
(cons `(:HEADER :DIMENSIONS (,dim)
:MAXIMUM-LENGTH ,(1+ dim) ; no duplicates expected
:NAME sharp-atsign-ar)
(sharp-atsign-alist *iprint-hard-bound-default* nil)))))
(defun get-sharp-atsign (i)
; If i is below the hard bound, then we get the string #@i# from a fixed array,
; so that we don't have to keep consing up that string.
(declare (xargs :guard (posp i)))
(cond ((<= i *iprint-hard-bound-default*)
(aref1 'sharp-atsign-ar *sharp-atsign-ar* i))
(t (make-sharp-atsign i))))
(defun update-iprint-alist-fal (iprint-alist iprint-fal-new iprint-fal-old val)
; We are doing iprinting. Iprint-alist is either a positive integer,
; representing the last-index but no accumulated iprint-alist, or else is a
; non-empty alist of entries (i . val_i). See the Essay on Iprinting.
(let ((pair (and iprint-fal-old
(or (hons-get val iprint-fal-new)
(hons-get val iprint-fal-old)))))
(cond (pair
(mv (cdr pair) iprint-alist iprint-fal-new))
((consp iprint-alist)
(let ((index (1+ (caar iprint-alist))))
(mv index
(acons index val iprint-alist)
(and iprint-fal-old
(hons-acons val index iprint-fal-new)))))
(t
(let ((index (1+ iprint-alist)))
(mv index
(acons index val nil)
(and iprint-fal-old
(hons-acons val index iprint-fal-new))))))))
; We now define the most elementary eviscerator, the one that implements
; *print-level* and *print-length*. In this same pass we also arrange to
; hide any object in alist, where alist pairs objects with their
; evisceration strings -- or if not a string, with the appropriate
; evisceration pair.
(mutual-recursion
(defun eviscerate1 (x v max-v max-n alist evisc-table hiding-cars
iprint-alist iprint-fal-new iprint-fal-old eager-p)
; Iprint-alist is either a symbol, indicating that we are not doing iprinting; a
; positive integer, representing the last-index but no accumulated iprint-alist;
; or an accumulated alist of entries (i . val_i). See the Essay on Iprinting.
; Note that if iprint-alist is a symbol, then it is nil if no evisceration has
; been done based on print-length or print-level, else t.