-
Notifications
You must be signed in to change notification settings - Fork 0
/
basis.lisp
9382 lines (8085 loc) · 374 KB
/
basis.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.
; When we are ready to verify termination in this and later files, we should
; consider changing null to endp in a number of functions.
(in-package "ACL2")
; We need to have state globals bound for prin1$ etc. to work, because of calls
; of with-print-controls. We may also need the dolist form below for tracing,
; which uses current-package for printing and current-acl2-world for
; current-acl2-world suppression. State globals such as 'compiler-enabled,
; whose value depends on the host Common Lisp implementation, are initialized
; here rather than in *initial-global-table*, so that the value of any defconst
; (such as *initial-global-table*) is independent of the host Common Lisp
; implementation. That is important to avoid trivial soundness bugs based on
; variance of a defconst value from one underlying Lisp to another.
#-acl2-loop-only
(initialize-state-globals)
(defun enforce-redundancy-er-args (event-form-var wrld-var)
(list "Enforce-redundancy is active; see :DOC set-enforce-redundancy and ~
see :DOC redundant-events. However, the following event ~@0:~|~%~x1"
`(if (and (symbolp (cadr ,event-form-var))
(decode-logical-name (cadr ,event-form-var) ,wrld-var))
"conflicts with an existing event of the same name"
"is not redundant")
event-form-var))
(defmacro enforce-redundancy (event-form ctx wrld form)
(let ((var 'redun-check-var))
`(let ((,var (and (not (eq (ld-skip-proofsp state)
'include-book))
(cdr (assoc-eq :enforce-redundancy
(table-alist 'acl2-defaults-table
,wrld))))))
(cond ((eq ,var t)
(check-vars-not-free
(,var)
(er soft ,ctx
,@(enforce-redundancy-er-args
event-form wrld))))
(t (pprogn (cond (,var (check-vars-not-free
(,var)
(warning$ ,ctx "Enforce-redundancy"
,@(enforce-redundancy-er-args
event-form wrld))))
(t state))
(check-vars-not-free
(,var)
,form)))))))
; 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 unavailble 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 insure 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 statisfies 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 insure 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.
(declare (xargs :mode :logic
:guard t)
(ignore qname qlambda free-vars))
nil)
(deflock *wormhole-lock*)
#-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.
(let* ((whs (if (car (cadr (cadr qlambda)))
(car (cadr (cadr qlambda))) ; Case (i)
(gensym))) ; Case (ii)
(val (gensym))
(form
; The code we lay down is the same in both cases, because we use the variable whs to
; store the old value of the status to see whether it has changed. But we have
; to generate a name if one isn't supplied.
`(progn
(cond (*wormholep*
(setq *wormhole-status-alist*
(put-assoc-equal
(f-get-global 'wormhole-name
*the-live-state*)
(f-get-global 'wormhole-status
*the-live-state*)
*wormhole-status-alist*))))
(let* ((*wormholep* t)
(,whs (cdr (assoc-equal ,qname *wormhole-status-alist*)))
(,val ,(caddr (cadr qlambda))))
(or (equal ,whs ,val)
(setq *wormhole-status-alist*
(put-assoc-equal ,qname ,val *wormhole-status-alist*)))
nil))))
(cond ((tree-occur-eq :no-wormhole-lock free-vars)
form)
(t `(with-wormhole-lock ,form)))))
(defmacro wormhole (name entry-lambda input form
&key
(current-package 'same current-packagep)
(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))
`(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 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)))))))
(defun global-set (var val wrld)
(declare (xargs :guard (and (symbolp var)
(plist-worldp wrld))))
(putprop var 'global-value val wrld))
(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))))))
(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 two 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 unravelling 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))) #\*))
(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-constantp1 (name)
; This function should correctly distinguish between variables and
; constants for symbols that are known to satisfy
; legal-variable-or-constant-namep. Thus, if name satisfies this
; predicate then it cannot be a variable.
(declare (xargs :guard (symbolp name)))
(or (eq name t)
(eq name nil)
(let ((s (symbol-name name)))
(and (not (= (length s) 0))
(eql (char s 0) #\*)
(eql (char s (1- (length s))) #\*)))))
(defun tilde-@-illegal-variable-or-constant-name-phrase (name)
; Assume that legal-variable-or-constant-namep has failed on name.
; We return a phrase that when printed with ~@0 will complete the
; sentence "Variable names must ...". Observe that the sentence
; could be "Constant names must ...".
(cond ((not (symbolp name)) "be symbols")
((keywordp name) "not be in the KEYWORD package")
((and (legal-constantp1 name)
(equal (symbol-package-name name) *main-lisp-package-name*))
(cons "not be in the main Lisp package, ~x0"
(list (cons #\0 *main-lisp-package-name*))))
((and (> (length (symbol-name name)) 0)
(eql (char (symbol-name name) 0) #\&))
"not start with ampersands")
((and (not (legal-constantp1 name))
(member-eq name *common-lisp-specials-and-constants*))
"not be among certain symbols from the main Lisp package, namely, the ~
value of the list *common-lisp-specials-and-constants*")
((and (not (legal-constantp1 name))
(equal (symbol-package-name name) *main-lisp-package-name*)
(not (member-eq name *common-lisp-symbols-from-main-lisp-package*)))
"either not be in the main Lisp package, or else must be among the ~
imports into ACL2 from that package, namely, the list ~
*common-lisp-symbols-from-main-lisp-package*")
(t "be approved by LEGAL-VARIABLE-OR-CONSTANT-NAMEP and this ~
one wasn't, even though it passes all the checks known to ~
the diagnostic function ~
TILDE-@-ILLEGAL-VARIABLE-OR-CONSTANT-NAME-PHRASE")))
(defun legal-constantp (name)
; A name may be declared as a constant if it has the syntax of a
; variable or constant (see legal-variable-or-constant-namep) and
; starts and ends with a *.
; WARNING: Do not confuse this function with defined-constant.
(eq (legal-variable-or-constant-namep name) 'constant))
(defun defined-constant (name w)
; Name is a defined-constant if it has been declared with defconst.
; If name is a defined-constant then we can show that it satisfies
; legal-constantp, because when a name is declared as a constant we
; insist that it satisfy the syntactic check. But there are
; legal-constantps that aren't defined-constants, e.g., any symbol
; that could be (but hasn't yet been) declared as a constant. We
; check, below, that name is a symbolp just to guard the getprop.
; This function returns the quoted term that is the value of name, if
; name is a constant. That result is always non-nil (it may be (quote
; nil) of course).
(and (symbolp name)
(getprop name 'const nil 'current-acl2-world w)))
(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 genvar1 (pkg-witness char-lst avoid-lst cnt)
; This function generates a symbol in the same package as the symbol
; pkg-witness that is guaranteed to be a legal-variablep and not in avoid-lst.
; We form a symbol by concatenating char-lst and the decimal representation of
; the natural number cnt. Observe the guard below. Since guards are not
; checked in :program code, the user must ensure upon calling this
; function that pkg-witness is a symbol in some package other than the main
; lisp package or the keyword package and that char-lst is a list of characters
; not beginning with * or &. Given that guard, there must exist a sufficiently
; large cnt to make our generated symbol be in the package of pkg-witness (a
; finite number of generated symbols might have been interned in one of the
; non-variable packages).
(declare (xargs :guard (and (let ((p (symbol-package-name pkg-witness)))
(and (not (equal p "KEYWORD"))
(not (equal p *main-lisp-package-name*))))
(consp char-lst)
(not (eql (car char-lst) #\*))
(not (eql (car char-lst) #\&)))))
(let ((sym (intern-in-package-of-symbol
(coerce
(append char-lst
(explode-nonnegative-integer cnt 10 nil))
'string)
pkg-witness)))
(cond ((or (member sym avoid-lst)
; The following call of legal-variablep could soundly be replaced by
; legal-variable-or-constant-namep, given the guard above, but we keep it
; as is for robustness.
(not (legal-variablep sym)))
(genvar1 pkg-witness char-lst avoid-lst (1+ cnt)))
(t sym))))
(defun genvar (pkg-witness prefix n avoid-lst)
; This is THE function that ACL2 uses to generate new variable names.
; Prefix is a string and n is either nil or a natural number. Together we
; call prefix and n the "root" of the variable we generate.
; We generate from prefix a legal variable symbol in the same package as
; pkg-witness that does not occur in avoid-lst. If n is nil, we first try the
; symbol with symbol-name prefix first and otherwise suffix prefix with
; increasingly large naturals (starting from 0) to find a suitable variable.
; If n is non-nil it had better be a natural and we immediately begin trying
; suffixes from there. Since no legal variable begins with #\* or #\&, we tack
; a #\V on the front of our prefix if prefix starts with one of those chars.
; If prefix is empty, we use "V".
; Note: This system will eventually contain a lot of code to generate
; "suggestive" variable names. However, we make the convention that
; in the end every variable name generated is generated by this
; function. Thus, all other code associated with variable name
; generation is heuristic if this one is correct.
(let* ((pkg-witness (cond ((let ((p (symbol-package-name pkg-witness)))
(or (equal p "KEYWORD")
(equal p *main-lisp-package-name*)))
; If pkg-witness is in an inappropriate package, we default it to the
; "ACL2" package.
'genvar)
(t pkg-witness)))
(sym (if (null n) (intern-in-package-of-symbol prefix pkg-witness) nil))
(cnt (if n n 0)))
(cond ((and (null n)
(legal-variablep sym)
(not (member sym avoid-lst)))
sym)
(t (let ((prefix (coerce prefix 'list)))
(cond ((null prefix) (genvar1 pkg-witness '(#\V) avoid-lst cnt))
((and (consp prefix)
(or (eql (car prefix) #\*)
(eql (car prefix) #\&)))
(genvar1 pkg-witness (cons #\V prefix) avoid-lst cnt))
(t (genvar1 pkg-witness prefix avoid-lst cnt))))))))
(defun packn1 (lst)
(declare (xargs :guard (good-atom-listp lst)))
(cond ((endp lst) nil)
(t (append (explode-atom (car lst) 10)
(packn1 (cdr lst))))))
(defun packn (lst)
(declare (xargs :guard (good-atom-listp lst)))
(let ((ans
; See comment in intern-in-package-of-symbol for an explanation of this trick.
(intern (coerce (packn1 lst) 'string)
"ACL2")))
ans))
(defun packn-pos (lst witness)
(declare (xargs :guard (and (good-atom-listp lst)
(symbolp witness))))
(intern-in-package-of-symbol (coerce (packn1 lst) 'string)
witness))
(defun pack2 (n1 n2)
(packn (list n1 n2)))
(defun gen-formals-from-pretty-flags1 (pretty-flags i avoid)
(cond ((endp pretty-flags) nil)
((eq (car pretty-flags) '*)
(let ((xi (pack2 'x i)))
(cond ((member-eq xi avoid)
(let ((new-var (genvar 'genvar ;;; ACL2 package
"GENSYM"
1
avoid)))
(cons new-var
(gen-formals-from-pretty-flags1
(cdr pretty-flags)
(+ i 1)
(cons new-var avoid)))))
(t (cons xi
(gen-formals-from-pretty-flags1
(cdr pretty-flags)
(+ i 1)
avoid))))))
(t (cons (car pretty-flags)
(gen-formals-from-pretty-flags1
(cdr pretty-flags)
(+ i 1)
avoid)))))
(defun gen-formals-from-pretty-flags (pretty-flags)
; Given a list of prettyified stobj flags, e.g., '(* * $S * STATE) we
; generate a proposed list of formals, e.g., '(X1 X2 $S X4 STATE). We
; guarantee that the result is a list of symbols as long as
; pretty-flags. Furthermore, a non-* in pretty-flags is preserved in
; the same slot in the output. Furthermore, the symbol generated for
; each * in pretty-flags is unique and not among the symbols in
; pretty-flags. Finally, STATE is not among the symbols we generate.
(gen-formals-from-pretty-flags1 pretty-flags 1 pretty-flags))
(defun defstub-body (output)
; This strange little function is used to turn an output signature
; spec (in either the old or new style) into a term. It never causes
; an error, even if output is ill-formed! What it returns in that
; case is irrelevant. If output is well-formed, i.e., is one of:
; output result
; * nil
; x x
; state state
; (mv * state *) (mv nil state nil)
; (mv x state y) (mv x state y)
; it replaces the *'s by nil and otherwise doesn't do anything.
(cond ((atom output)
(cond ((equal output '*) nil)
(t output)))
((equal (car output) '*)
(cons nil (defstub-body (cdr output))))
(t (cons (car output) (defstub-body (cdr output))))))
(defun collect-non-x (x lst)
; This function preserves possible duplications of non-x elements in lst.
; We use this fact when we check the legality of signatures.
(declare (xargs :guard (true-listp lst)))
(cond ((endp lst) nil)
((equal (car lst) x)
(collect-non-x x (cdr lst)))
(t (cons (car lst) (collect-non-x x (cdr lst))))))
#+acl2-loop-only
(defmacro defproxy (name args-sig arrow body-sig)
(cond
((not (and (symbol-listp args-sig)
(symbolp arrow)
(equal (symbol-name arrow) "=>")))
(er hard 'defproxy
"Defproxy must be of the form (proxy name args-sig => body-sig), ~
where args-sig is a true-list of symbols. See :DOC defproxy."))
(t
(let ((formals (gen-formals-from-pretty-flags args-sig))
(body (defstub-body body-sig))
(stobjs (collect-non-x '* args-sig)))
`(defun ,name ,formals
(declare (xargs :non-executable :program
:mode :program
,@(and stobjs `(:stobjs ,stobjs)))
(ignorable ,@formals))
; The form of the body below is dictated by function throw-nonexec-error-p.
; Notice that we do not pass the formals to throw-nonexec-error as we do in
; defun-nx-fn, because if the formals contain a stobj then we would violate
; stobj restrictions, which are checked for non-executable :program mode
; functions.
(prog2$ (throw-nonexec-error ',name nil)
,body))))))
#-acl2-loop-only
(defmacro defproxy (name args-sig arrow body-sig)
; Note that a defproxy redefined using encapsulate can generate a warning in
; CLISP (see comment about CLISP in with-redefinition-suppressed), because
; indeed there are two definitions being made for the same name. However, the
; definition generated for a function by encapsulate depends only on the
; function's signature, up to renaming of formals; see the #-acl2-loop-only
; definition of encapsulate. So this redefinition is as benign as the
; redefinition that occurs in raw Lisp with a redundant defun.
`(defstub ,name ,args-sig ,arrow ,body-sig))
; We now use encapsulate to implement defstub. It is handy to do so here,
; rather than in other-events.lisp, since the raw Lisp definition of defproxy
; uses defstub.
(defun defstub-ignores (formals body)
; The test below is sufficient to ensure that the set-difference-equal
; used to compute the ignored vars will not cause an error. We return
; a true list. The formals and body will be checked thoroughly by the
; encapsulate, provided we generate it! Provided they check out, the
; result returned is the list of ignored formals.
(if (and (symbol-listp formals)
(or (symbolp body)
(and (consp body)
(symbol-listp (cdr body)))))
(set-difference-equal
formals
(if (symbolp body)
(list body)
(cdr body)))
nil))
; The following function is used to implement a slighly generalized
; form of macro args, namely one in which we can provide an arbitrary
; number of ordinary arguments terminated by an arbitrary number of
; keyword argument pairs.
(defun partition-rest-and-keyword-args1 (x)
(cond ((endp x) (mv nil nil))
((keywordp (car x))
(mv nil x))
(t (mv-let (rest keypart)
(partition-rest-and-keyword-args1 (cdr x))
(mv (cons (car x) rest)
keypart)))))
(defun partition-rest-and-keyword-args2 (keypart keys alist)
; We return t if keypart is ill-formed as noted below. Otherwise, we
; return ((:keyn . vn) ... (:key1 . v1)).
(cond ((endp keypart) alist)
((and (keywordp (car keypart))
(consp (cdr keypart))
(not (assoc-eq (car keypart) alist))
(member (car keypart) keys))
(partition-rest-and-keyword-args2 (cddr keypart)
keys
(cons (cons (car keypart)
(cadr keypart))
alist)))
(t t)))
(defun partition-rest-and-keyword-args (x keys)
; X is assumed to be a list of the form (a1 ... an :key1 v1 ... :keyk
; vk), where no ai is a keyword. We return (mv erp rest alist), where
; erp is t iff the keyword section of x is ill-formed. When erp is
; nil, rest is '(a1 ... an) and alist is '((:key1 . v1) ... (:keyk
; . vk)).
; The keyword section is ill-formed if it contains a non-keyword in an
; even numbered element, if it binds the same keyword more than once,
; or if it binds a keyword other than those listed in keys.
(mv-let (rest keypart)
(partition-rest-and-keyword-args1 x)
(let ((alist (partition-rest-and-keyword-args2 keypart keys nil)))
(cond
((eq alist t) (mv t nil nil))
(t (mv nil rest alist))))))
(defmacro defstub (name &rest rst)
(mv-let (erp args key-alist)
(partition-rest-and-keyword-args rst '(:doc))
(cond
((or erp
(not (or (equal (length args) 2)
(and (equal (length args) 3)
(symbol-listp (car args))
(symbolp (cadr args))
(equal (symbol-name (cadr args)) "=>")))))
`(er soft 'defstub
"Defstub must be of the form (defstub name formals ~
body) or (defstub name args-sig => body-sig), where ~
args-sig is a true-list of symbols. Both ~
forms permit an optional, final :DOC doc-string ~
argument. See :DOC defstub."))
(t
(let ((doc (cdr (assoc-eq :doc key-alist))))
(cond
((equal (length args) 2)
; Old style
(let* ((formals (car args))
(body (cadr args))
(ignores (defstub-ignores formals body)))
`(encapsulate
((,name ,formals ,body))
(logic)
(local
(defun ,name ,formals
(declare (ignore ,@ignores))
,body))
,@(and (consp body)
(eq (car body) 'mv)
`((defthm ,(packn-pos (list "TRUE-LISTP-" name)
name)
(true-listp (,name ,@formals))
:rule-classes :type-prescription)))
,@(if doc `((defdoc ,name ,doc)) nil))))
(t (let* ((args-sig (car args))
(body-sig (caddr args))
(formals (gen-formals-from-pretty-flags args-sig))
(body (defstub-body body-sig))
(ignores (defstub-ignores formals body))
(stobjs (collect-non-x '* args-sig)))
`(encapsulate
(((,name ,@args-sig) => ,body-sig))
(logic)
(local
(defun ,name ,formals
(declare (ignore ,@ignores)
(xargs :stobjs ,stobjs))
,body))
,@(and (consp body-sig)
(eq (car body-sig) 'mv)
`((defthm ,(packn-pos (list "TRUE-LISTP-" name)
name)
(true-listp (,name ,@formals))
:rule-classes :type-prescription)))
,@(if doc `((defdoc ,name ,doc)) nil))))))))))
(defun lambda-keywordp (x)
(and (symbolp x)
(eql 1 (string<= "&" (symbol-name x)))))
(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 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 ..), (IGNORABE ~
..), or (TYPE ..). The form ~x0 is thus illegal."