-
Notifications
You must be signed in to change notification settings - Fork 0
/
type-set-b.lisp
12759 lines (11127 loc) · 553 KB
/
type-set-b.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")
;; Historical Comment from Ruben Gamboa:
;; I changed this value from 7 to 10 to make room for the
;; positive-, negative-, and complex-irrationals.
(defconst *number-of-numeric-type-set-bits*
#+:non-standard-analysis 10
#-:non-standard-analysis 7)
(defconst *type-set-binary-+-table-list*
(let ((len (expt 2 *number-of-numeric-type-set-bits*)))
(cons (list :header
:dimensions (list len len)
:maximum-length (1+ (* len len))
:default *ts-acl2-number*
:name '*type-set-binary-+-table*)
(type-set-binary-+-alist (1- len) (1- len) nil))))
(defconst *type-set-binary-+-table*
(compress2 'type-set-binary-+-table
*type-set-binary-+-table-list*))
(defconst *type-set-binary-*-table-list*
(let ((len (expt 2 *number-of-numeric-type-set-bits*)))
(cons (list :header
:dimensions (list len len)
:maximum-length (1+ (* len len))
:default *ts-acl2-number*
:name '*type-set-binary-*-table*)
(type-set-binary-*-alist (1- len) (1- len) nil))))
(defconst *type-set-binary-*-table*
(compress2 'type-set-binary-*-table
*type-set-binary-*-table-list*))
;; Historical Comment from Ruben Gamboa:
;; As a consequence of the extra numeric arguments, I had to
;; change this table from 6 to 8, to make room for the positive
;; and negative irrationals.
(defconst *type-set-<-table-list*
#+:non-standard-analysis
(cons (list :header
:dimensions '(256 256)
:maximum-length (1+ (* 256 256))
:name '*type-set-<-table*)
(type-set-<-alist 255 255 nil))
#-:non-standard-analysis
(cons (list :header
:dimensions '(64 64)
:maximum-length (1+ (* 64 64))
:name '*type-set-<-table*)
(type-set-<-alist 63 63 nil))
)
(defconst *type-set-<-table*
(compress2 'type-set-<-table
*type-set-<-table-list*))
; Essay on Enabling, Enabled Structures, and Theories
; The rules used by the system can be "enabled" and "disabled". In a
; break with Nqthm, this is true even of :COMPOUND-RECOGNIZER rules.
; We develop that code now. Some of the fundamental concepts here are
; that of "rule names" or "runes" and their associated numeric
; correspondents, numes. We also explain "mapping pairs," "rule name
; designators", "theories," (both "common theories" and "runic
; theories") and "enabled structures".
(defun assoc-equal-cdr (x alist)
; Like assoc-equal but compares against the cdr of each pair in alist.
(declare (xargs :mode :logic ; might as well put this into :logic mode
:guard (alistp alist)))
(cond ((endp alist) nil)
((equal x (cdar alist)) (car alist))
(t (assoc-equal-cdr x (cdr alist)))))
(defun runep (x wrld)
; This function returns non-nil iff x is a rune, i.e., a "rule name,"
; in wrld. When non-nil, the value of this function is the nume of
; the rune x, i.e., the index allocated to this rule name in the
; enabled array. This function returns nil on fake-runes! See the
; essay on fake-runes below.
; To clear up the confusion wrought by the proliferation of
; nomenclature surrounding rules and the ways by which one might refer
; to them, I have recently adopted more colorful nomenclature than the
; old "rule name," "rule index," "rule id," etc. To wit,
; rune (rule name):
; an object that is syntactically of the form (token symb . x), where
; token is one of the rule-class tokens, e.g., :REWRITE, :META, etc.,
; symb is a symbolp with a 'runic-mapping-pairs property, and x is
; either nil or a positive integer that distinguishes this rune from
; others generated from different :rule-classes that share the same
; token and symb. We say that (token symb . x) is "based" on the
; symbol symb. Formally, rn is a rune iff it is of the form (& symb
; . &), symb is a symbolp with a non-nil runic-info and rn is in the
; range of the mapping-pairs of that runic-info. This is just another
; way of saying that the range of the mapping pairs of a symbol is a
; complete list of all of the runes based on that symbol. Each rule
; in the system has a unique rune that identifies it. The user may
; thus refer to any rule by its rune. An ordered list of runes is a
; theory (though we also permit some non-runes in theories presented
; by the user). Each rune has a status, enabled or disabled, as given
; by an enabled structure. I like the name "rune" because its
; etymology (from "rule name") is clear and it connotes an object that
; is at once obscure, atomic, and yet clearly understood by the
; scholar.
; nume (the numeric counterpart of a rune):
; a nonnegative integer uniquely associated with a rune. The nume of
; a rune tells us where in the enabled array we find the status of the
; rune.
; runic mapping pair:
; a pair, (nume . rune), consisting of a rune and its numeric
; counterpart, nume. The 'runic-mapping-pairs property of a symbol is
; the list of all runic mapping pairs whose runes are based on the
; given symbol. The 'runic-mapping-pairs value is ordered by
; ascending numes, i.e., the first nume in the list is the least. The
; primary role of runic mapping pairs is to make it more efficient to
; load a theory (ideally a list of runes) into an enabled structure.
; That process requires that we assemble an ACL2 array, i.e., an alist
; mapping array indices (numes) to their values (runes) in the array.
; We do that by collecting the runic mapping pairs of each rune in the
; theory. We also use these pairs to sort theories: theories are kept
; in descending nume order to make intersection and union easier. To
; sort a theory we replace each rune in it by its mapping pair, sort
; the result by descending cars, and then strip out the runes to obtain
; the answer. More on this when we discuss sort-by-fnume.
; event name:
; The symbol, symb, in a rune (token symb . x), is an event name.
; Some event names are allowed in theories, namely, those that are the
; base symbols of runes. In such usage, an event name stands for one
; or more runes, depending on what kind of event it names. For
; example, if APP is the name of a defun'd function, then when APP
; appears in a theory it stands for the rune (:DEFINITION APP). If
; ASSOC-OF-APP is a lemma name, then when it appears in a theory it
; stands for all the runes based on that name, e.g., if that event
; introduced two rewrite rules and an elim rule, then ASSOC-OF-APP
; would stand for (:REWRITE ASSOC-OF-APP . 1), (:REWRITE ASSOC-OF-APP
; . 2), and (:ELIM ASSOC-OF-APP). This use of event names allows them
; to be confused with rule names.
; Historical Footnote: In nqthm, the executable-counterpart of the
; function APP actually had a distinct name, *1*APP, and hence we
; established the expectation that one could prevent the use of that
; "rule" while allowing the use of the other. We now use the runes
; (:DEFINITION APP) and (:EXECUTABLE-COUNTERPART APP) to identify
; those two rules added by a defun event. In fact, the defun adds a
; third rule, named by the rune (:TYPE-PRESCRIPTION APP). In fact, we
; were driven to the invention of runes as unique rule names when we
; added type-prescription lemmas.
(declare (xargs :guard
(if (and (consp x)
(consp (cdr x))
(symbolp (cadr x)))
(and (plist-worldp wrld)
(alistp (getpropc (cadr x) 'runic-mapping-pairs nil
wrld)))
t)))
(cond ((and (consp x)
(consp (cdr x))
(symbolp (cadr x)))
(car
(assoc-equal-cdr x
(getpropc (cadr x) 'runic-mapping-pairs nil wrld))))
(t nil)))
; Essay on Fake-Runes
; The system has many built in rules that, for regularity, ought to
; have names and numes but don't because they can never be disabled.
; In addition, we sometimes wish to have a rune-like object we can use
; as a mark, without having to worry about the possibility that a
; genuine rune will come along with the same identity. Therefore, we
; have invented the notion of "fake-runes." Fake runes are constants.
; By convention, the constant name is always of the form
; *fake-rune-...* and the value of every fake rune is always
; (:FAKE-RUNE-... nil). Since no rule class will ever start with the
; words "fake rune" this convention will survive the introduction of
; all conceivable new rule classes. It is important that fake runes
; be based on the symbol nil. This way they are assigned the nume
; nil by fnume (below) and will always be considered enabled. The
; function runep does NOT recognize fake runes. Fake runes cannot be
; used in theories, etc.
; The fake runes are:
; *fake-rune-for-anonymous-enabled-rule*
; This fake rune is specially recognized by push-lemma and ignored. Thus, if
; you wish to invent a rule that you don't wish to name or worry will be
; disabled, give the rule this :rune and the :nume nil.
; *fake-rune-for-linear*
; This fake rune is a signal that linear arithmetic was used.
; *fake-rune-for-type-set*
; This fake rune is used by type-set to record that built-in facts about
; primitive functions were used.
; *fake-rune-for-cert-data*
; This fake rune is a signal that information was used that was retrieved from
; either the first pass of an encapsulate or certify-book, or from the
; certificate of a certified book.
; WARNING: If more fake runes are added, deal with them in *fake-rune-alist*.
(defmacro base-symbol (rune)
; The "base symbol" of the rune (:token symbol . x) is symbol.
; Note: The existence of this function and the next one suggest that
; runes are implemented abstractly. Ooooo... we don't know how runes
; are really laid out. But this just isn't true. We use car to get
; the token of a rune and we use cddr to get x, above. But for some
; reason we defined and began to use base-symbol to get the base
; symbol. In any case, if the structure of runes is changed, all
; mention of runes will have to be inspected.
`(cadr ,rune))
(defmacro strip-base-symbols (runes)
`(strip-cadrs ,runes))
(defun fnume (rune wrld)
; Rune has the shape of a rune. We return its nume. Actually, this function
; admits every fake-rune as a "rune" and returns nil on it (by virtue of the
; fact that the base-symbol of a fake rune is nil and hence there are no
; mapping pairs). This fact may be exploited by functions which have obtained
; a fake rune as the name of some rule and wish to know its nume so they can
; determine if it is enabled. More generally, this function returns nil if
; rune is not a rune in the given world, wrld. Nil is treated as an enabled
; nume by enabled-runep but not by active-runep.
(declare (xargs :guard
(and (plist-worldp wrld)
(consp rune)
(consp (cdr rune))
(symbolp (base-symbol rune))
(alistp (getpropc (base-symbol rune)
'runic-mapping-pairs nil wrld)))))
(car
(assoc-equal-cdr rune
(getpropc (base-symbol rune) 'runic-mapping-pairs nil
wrld))))
(defun frunic-mapping-pair (rune wrld)
; Rune must be a rune in wrld. We return its mapping pair.
(assoc-equal-cdr rune
(getpropc (base-symbol rune) 'runic-mapping-pairs nil
wrld)))
(defun fn-rune-nume (fn nflg xflg wrld)
; Fn must be a function symbol, not a lambda expression. We return
; either the rune (nflg = nil) or nume (nflg = t) associated with
; either (:DEFINITION fn) (xflg = nil) or (:EXECUTABLE-COUNTERPART fn)
; (xflg = t). This function knows the layout of the runic mapping
; pairs by DEFUNS -- indeed, it knows the layout for all function
; symbols whether DEFUNd or not! See the Essay on the Assignment of
; Runes and Numes by DEFUNS. If fn is a constrained function we
; return nil for all combinations of the flags.
(let* ((runic-mapping-pairs
(getpropc fn 'runic-mapping-pairs nil wrld))
(pair (if xflg (cadr runic-mapping-pairs) (car runic-mapping-pairs))))
(if nflg (car pair) (cdr pair))))
(defun definition-runes (fns xflg wrld)
(cond ((null fns) nil)
(t (cons (fn-rune-nume (car fns) nil xflg wrld)
(definition-runes (cdr fns) xflg wrld)))))
(defun get-next-nume (lst)
; We return the next available nume in lst, which is a cdr of the
; current world. We scan down lst, looking for the most recently
; stored 'runic-mapping-pairs entry. Suppose we find it, ((n1 .
; rune1) (n2 . rune2) ... (nk . runek)). Then the next rune will get
; the nume nk+1, which is also just n1+k, where k is the length of the
; list of mapping pairs. Note: If we see (name runic-mapping-pairs .
; atm) where atm is an atom, then atm is :acl2-property-unbound or
; nil, and we keep going. Such tuples appear in part because in
; redefinition the 'runic-mapping-pairs property is "nil'd" out.
(cond ((null lst)
#+acl2-metering (meter-maid 'get-next-nume 100)
0)
((and (eq (cadr (car lst)) 'runic-mapping-pairs)
(consp (cddr (car lst))))
#+acl2-metering (meter-maid 'get-next-nume 100)
(+ (car (car (cddr (car lst))))
(length (cddr (car lst)))))
(t
#+acl2-metering (setq meter-maid-cnt (1+ meter-maid-cnt))
(get-next-nume (cdr lst)))))
; We now formalize the notion of "theory". We actually use two
; different notions of theory here. The first, which is formalized by
; the predicate theoryp, is what the user is accustomed to thinking of
; as a theory. Formally, it is a truelist of rule name designators,
; each of which designates a set of runes. The second is what we
; call a "runic theory" which is an ordered list of runes, where the
; ordering is by descending numes. We sometimes refer to theories as
; "common theories" to distinguish them from runic theories. To every
; common theory there corresponds a runic theory obtained by unioning
; together the runes designated by each element of the common theory.
; We call this the runic theory "corresponding" to the common one.
(defun deref-macro-name-lst (macro-name-lst macro-aliases)
(cond ((atom macro-name-lst) nil)
(t (cons (deref-macro-name (car macro-name-lst) macro-aliases)
(deref-macro-name-lst (cdr macro-name-lst) macro-aliases)))))
(defconst *abbrev-rune-alist*
'((:d . :definition)
(:e . :executable-counterpart)
(:i . :induction)
(:r . :rewrite)
(:t . :type-prescription)))
(defun translate-abbrev-rune (x macro-aliases)
(declare (xargs :guard (alistp macro-aliases)))
(let ((kwd (and (consp x)
(consp (cdr x))
(symbolp (cadr x))
(cdr (assoc-eq (car x) *abbrev-rune-alist*)))))
(cond (kwd (list* kwd
(deref-macro-name (cadr x) macro-aliases)
(cddr x)))
(t x))))
(defun rule-name-designatorp (x macro-aliases wrld)
; A rule name designator is an object which denotes a set of runes. We call
; that set of runes the "runic interpretation" of the designator. A rune, x,
; is a rule name designator, denoting {x}. A symbol, x, with a
; 'runic-mapping-pairs property is a designator and denotes either
; {(:DEFINITION x)} or else the entire list of runes in the
; runic-mapping-pairs, depending on whether there is a :DEFINITION rune. A
; symbol x that is a theory name is a designator and denotes the runic theory
; value. Finally, a singleton list, (fn), is a designator if fn is a function
; symbol; it designates {(:EXECUTABLE-COUNTERPART fn)}.
; For example, if APP is a function symbol then its runic interpretation is
; {(:DEFINITION APP)}. If ASSOC-OF-APP is a defthm event with, say, three rule
; classes then its runic interpretation is a set of three runes, one for each
; rule generated. The idea here is to maintain some consistency with the Nqthm
; way of disabling names. If the user disables APP then only the symbolic
; definition is disabled, not the executable-counterpart, while if ASSOC-OF-APP
; is disabled, all such rules are disabled.
; When true, we return the symbol on which the set of rune is based. This
; information, which involves the application of deref-macro-name, can be
; useful to callers; see check-theory-msg1.
; Note: We purposely do not define a function "runic-interpretation" which
; returns runic interpretation of a designator. The reason is that we would
; have to cons that set up for every designator except theories. The main
; reason we'd want such a function is to define the runic theory corresponding
; to a common one. We do that below (in
; convert-theory-to-unordered-mapping-pairs1) and open-code "runic
; interpretation."
(cond ((symbolp x)
(let ((x (deref-macro-name x macro-aliases)))
(cond
((getpropc x 'runic-mapping-pairs nil wrld)
x)
(t (and (not (eq (getpropc x 'theory t wrld) t))
x)))))
((and (consp x)
(null (cdr x))
(symbolp (car x)))
(let* ((fn (deref-macro-name (car x) macro-aliases)))
(and (function-symbolp fn wrld)
(runep (list :executable-counterpart fn) wrld)
fn)))
(t (let ((x (translate-abbrev-rune x macro-aliases)))
(and (runep x wrld)
(base-symbol x))))))
(defun theoryp1 (lst macro-aliases wrld)
(cond ((atom lst) (null lst))
((rule-name-designatorp (car lst) macro-aliases wrld)
(theoryp1 (cdr lst) macro-aliases wrld))
(t nil)))
(defun theoryp (lst wrld)
; A (common) theory is a truelist of rule name designators. It is
; possible to turn a theory into a list of runes (which is, itself, a
; theory). That conversion is done by coerce-to-runic-theory.
(theoryp1 lst (macro-aliases wrld) wrld))
; Now we define what a "runic theory" is.
(defun runic-theoryp1 (prev-nume lst wrld)
; We check that lst is an ordered true list of runes in wrld, where
; the ordering is by descending numes. Prev-nume is the nume of the
; previously seen element of lst (or nil if we are at the top-level).
(cond ((atom lst) (null lst))
(t
(let ((nume (runep (car lst) wrld)))
(cond ((and nume
(or (null prev-nume)
(> prev-nume nume)))
(runic-theoryp1 nume (cdr lst) wrld))
(t nil))))))
(defun runic-theoryp (lst wrld)
; A "runic theory" (wrt wrld) is an ordered truelist of runes (wrt wrld), where
; the ordering is that imposed by the numes of the runes, greatest numes first.
; This function returns t or nil according to whether lst is a runic theory in
; wrld. Common theories are converted into runic-theories in order to do such
; operations as union and intersection. Our theory processing functions all
; yield runic-theories. We can save some time in those functions by checking
; if an input theory is in fact a runic theory: if so, we need not sort it.
(runic-theoryp1 nil lst wrld))
; When we start manipulating theories, e.g., unioning them together,
; we will actually first convert common theories into runic theories.
; We keep runic theories ordered so it is easier to intersect and
; union them. However, this raises a slightly technical question,
; namely the inefficiency of repeatedly going to the property lists of
; the basic symbols of the runes to recover (by a search through the
; mapping pairs) the measures by which we compare runes (i.e., the
; numes). We could order theories lexicographically -- there is no
; reason that theories have to be ordered by nume until it is time to
; load the enabled structure. We could also obtain the measure of
; each rune and cons the two together into a mapping pair and sort
; that list on the cars. This would at least save the repeated
; getprops at the cost of copying the list twice (once to pair the
; runes with their numes and once to strip out the final list of
; runes).
; We have compared these three schemes in a slightly simpler setting:
; sorting lists of symbols. The sample list was the list of all event
; names in the initial world, i.e., every symbol in the initial world
; with an 'absolute-event-number property. The lexicographic
; comparison was done with string<. The measure (analogous to the
; nume) was the 'absolute-event-number. We used exactly the same tail
; recursive merge routine used here, changing only the comparator
; expression. The version that conses the nume to the rune before
; sorting paid the price of the initial and final copying. The times
; to sort the 2585 symbols were:
; lexicographic: 1.29 seconds
; getprops: 1.18 seconds
; cars: 0.68 seconds
; We have decided to go the car route. The argument that it does a
; lot of unnecessary consing is unpersuasive in light of the amount of
; consing done by sorting. For example right off the bat in sort we
; divide the list into its evens and odds, thus effectively copying
; the entire list. The point is that as it has always been coded,
; sort produces a lot of garbaged conses, so it is not as though
; copying the list twice is a gross insult to the garbage collector.
; We exhibit some performance measures of our actual theory manipulation
; functions later. See Essay on Theory Manipulation Performance.
; Consider a runic theory. We want to "augment" it by consing onto
; every rune its nume. Common theories cannot be augmented until they
; are converted into runic ones. Naively, then we want to consider two
; transformations: how to convert a common theory to a runic one, and
; how to augment a runic theory. It turns out that the first
; transformation is messier than you'd think due to the possibility
; that distinct elements of the common theory designate duplicate
; runes. More on this later. But no matter what our final design, we
; need the second capability, since we expect that the theory
; manipulation functions will often be presented with runic theories.
; So we begin by augmentation of runic theories.
; Our goal is simply to replace each rune by its frunic-mapping-pair.
; But frunic-mapping-pair has to go to the property list of the basic
; symbol of the rune and then search through the 'runic-mapping-pairs
; for the pair needed. But in a runic theory, it will often be the
; case that adjacent runes have the same symbol, e.g., (:REWRITE LEMMA
; . 1), (:REWRITE LEMMA . 2), ... Furthermore, the second rune will
; occur downstream of the first in the 'runic-mapping-pairs of their
; basic symbol. So by keeping track of where we found the last
; mapping pair we may be able to find the next one faster.
(defun find-mapping-pairs-tail1 (rune mapping-pairs)
; Rune is a rune and mapping-pairs is some tail of the
; 'runic-mapping-pairs property of its basic symbol. Furthermore, we
; know that we have not yet passed the pair for rune in mapping-pairs.
; We return the tail of mapping-pairs whose car is the pair for rune.
(cond ((null mapping-pairs)
; At one time we caused a hard error here, because we expected that this case
; never happens. However, it can happen upon redefinition, when rune is no
; longer a rune. Here are two examples.
; Example 1:
; (defthm my-thm (equal (car (cons x x)) x))
; (deftheory my-thy (current-theory :here))
; (redef!)
; (defthm my-thm (equal (cdr (cons x x)) x)
; :hints (("Goal" :in-theory (theory 'my-thy))))
; Example 2:
; (defthm my-thm (equal (car (cons x x)) x))
; (deftheory my-thy (current-theory :here))
; (redef!)
; (defthm my-thm (equal (cdr (cons x x)) x) :rule-classes nil)
; (in-theory (theory 'my-thy))
; As of October 2017 we believe that this code has been in place for many
; years, and at this point it seems that the value of the hard error is
; outweighed by avoiding presentation to users of this obscure error message.
nil)
((equal rune (cdr (car mapping-pairs))) mapping-pairs)
(t (find-mapping-pairs-tail1 rune (cdr mapping-pairs)))))
(defun find-mapping-pairs-tail (rune mapping-pairs wrld)
; Rune is a rune and mapping-pairs is some tail of the
; 'runic-mapping-pairs property of some basic symbol -- but not
; necessarily rune's. If it is rune's then rune has not yet been seen
; among those pairs. If it is not rune's, then we get rune's from
; world. In any case, we return a mapping-pairs list whose car is the
; mapping pair for rune.
(cond ((and mapping-pairs
(eq (base-symbol rune) (cadr (cdr (car mapping-pairs)))))
(find-mapping-pairs-tail1 rune mapping-pairs))
(t (find-mapping-pairs-tail1 rune
(getpropc (base-symbol rune)
'runic-mapping-pairs
nil
wrld)))))
(defun augment-runic-theory1 (lst mapping-pairs wrld ans)
; Lst is a runic theory. We iteratively accumulate onto ans the
; mapping pair corresponding to each element of lst. Mapping-pairs is
; the tail of some 'runic-mapping-pairs property and is used to speed
; up the retrieval of the pair for the first rune in lst. See
; find-mapping-pairs-tail for the requirements on mapping-pairs. The
; basic idea is that as we cdr through lst we also sweep through
; mapping pairs (they are ordered the same way). When the rune we get
; from lst is based on the same symbol as the last one, then we find
; its mapping pair in mapping-pairs. When it is not, we switch our
; attention to the 'runic-mapping-pairs of the new basic symbol.
(cond
((null lst) ans)
(t (let ((mapping-pairs
(find-mapping-pairs-tail (car lst) mapping-pairs wrld)))
(cond
(mapping-pairs
(augment-runic-theory1 (cdr lst)
(cdr mapping-pairs)
wrld
(cons (car mapping-pairs) ans)))
(t
(augment-runic-theory1 (cdr lst)
mapping-pairs
wrld
ans)))))))
(defun augment-runic-theory (lst wrld)
; We pair each rune in the runic theory lst with its nume, returning an
; augmented runic theory.
(augment-runic-theory1 (reverse lst) nil wrld nil))
; Ok, so now we know how to augment a runic theory. How about
; converting common theories to runic ones? That is harder because of
; the duplication problem. For example, '(APP APP) is a common
; theory, but the result of replacing each designator by its rune,
; '((:DEFINITION app) (:DEFINITION app)), is not a runic theory! It
; gets worse. Two distinct designators might designate the same rune.
; For example, LEMMA might designate a collection of :REWRITE rules
; while (:REWRITE LEMMA . 3) designates one of those same rules. To
; remove duplicates we actually convert the common theory first to a
; list of (possibly duplicated and probably unordered) mapping pairs
; and then use a bizarre sort routine which removes duplicates. While
; converting a common theory to a unordered and duplicitous list of
; mapping pairs we simply use frunic-mapping-pair to map from a rune
; to its mapping pair; that is, we don't engage in the clever use of
; tails of the mapping pairs properties because we don't expect to see
; too many runes in a common theory, much less for two successive
; runes to be ordered properly.
(defconst *bad-runic-designator-string*
"This symbol was expected to be suitable for theory expressions; see :DOC ~
theories, in particular the discussion of runic designators. One possible ~
source of this problem is an attempt to include an uncertified book with a ~
deftheory event that attempts to use the above symbol in a deftheory event.")
(defun convert-theory-to-unordered-mapping-pairs1 (lst macro-aliases wrld ans)
; Note: another function that deals in runic mapping pairs is
; monitorable-runes-from-mapping-pairs.
; This is the place we give meaning to the "runic interpretation" of a
; rule name designator. Every element of lst is a rule name
; designator.
(cond
((null lst) ans)
((symbolp (car lst))
(let ((temp (getpropc (deref-macro-name (car lst) macro-aliases)
'runic-mapping-pairs nil wrld)))
(cond
((and temp
(eq (car (cdr (car temp))) :DEFINITION)
(eq (car (cdr (cadr temp))) :EXECUTABLE-COUNTERPART))
(convert-theory-to-unordered-mapping-pairs1
(cdr lst) macro-aliases wrld
(if (equal (length temp) 4)
; Then we have an :induction rune. See the Essay on the Assignment of Runes
; and Numes by DEFUNS.
(cons (car temp) (cons (cadddr temp) ans))
(cons (car temp) ans))))
(temp
(convert-theory-to-unordered-mapping-pairs1
(cdr lst) macro-aliases wrld (revappend temp ans)))
(t
; In this case, we know that (car lst) is a theory name. Its 'theory
; property is the value of the theory name and is a runic theory. We
; must augment it. The twisted use of ans below -- passing it into
; the accumulator of the augmenter -- is permitted since we don't care
; about order.
(convert-theory-to-unordered-mapping-pairs1
(cdr lst) macro-aliases wrld
(augment-runic-theory1
(reverse (getpropc (car lst) 'theory
`(:error ,*bad-runic-designator-string*)
wrld))
nil
wrld
ans))))))
((null (cdr (car lst)))
(convert-theory-to-unordered-mapping-pairs1
(cdr lst) macro-aliases wrld
(cons (cadr (getpropc (deref-macro-name (car (car lst)) macro-aliases)
'runic-mapping-pairs
`(:error ,*bad-runic-designator-string*)
wrld))
ans)))
(t (convert-theory-to-unordered-mapping-pairs1
(cdr lst) macro-aliases wrld
(cons (frunic-mapping-pair (translate-abbrev-rune (car lst)
macro-aliases)
wrld)
ans)))))
(defun convert-theory-to-unordered-mapping-pairs (lst wrld)
; This function maps a common theory into a possibly unordered and/or
; duplicitous list of mapping pairs.
(convert-theory-to-unordered-mapping-pairs1
lst (macro-aliases wrld) wrld nil))
; Now we develop a merge sort routine that has four interesting
; properties. First, it sorts arbitrary lists of pairs, comparing on
; their cars which are assumed to be rationals. Second, it can be
; told whether to produce an ascending order or a descending order.
; Third, it deletes all but one occurrence of any element with the
; same car as another. Fourth, its merge routine is tail recursive
; and so can handle very long lists. (The sort routine is not tail
; recursive, but it cuts the list in half each time and so can handle
; long lists too.)
(defun duplicitous-cons-car (x y)
; This is like (cons x y) in that it adds the element x to the list y,
; except that it does not if the car of x is the car of the first element
; of y.
(cond ((equal (car x) (caar y)) y)
(t (cons x y))))
(defun duplicitous-revappend-car (lst ans)
; Like revappend but uses duplicitous-cons-car rather than cons.
(cond ((null lst) ans)
(t (duplicitous-revappend-car (cdr lst)
(duplicitous-cons-car (car lst) ans)))))
(defun duplicitous-merge-car (parity lst1 lst2 ans)
; Basic Idea: Lst1 and lst2 must be appropriately ordered lists of
; pairs. Comparing on the cars of respective pairs, we merge the two
; lists, deleting all but one occurrence of any element with the same
; car as another.
; Terminology: Suppose x is some list of pairs and that the car of
; each pair is a rational. We say x is a "measured list" because the
; measure of each element is given by the car of the element. We
; consider two orderings of x. The "parity t" ordering is that in
; which the cars of x are ascending. The "parity nil" ordering is
; that in which the cars of x are descending. E.g., in the parity t
; ordering, the first element of x has the least car and the last
; element of x has the greatest.
; Let lst1 and lst2 be two measured lists. This function merges lst1
; and lst2 to produce output in the specified parity. However, it
; assumes that its two main inputs, lst1 and lst2, are ordered in the
; opposite parity. That is, if we are supposed to produce output that
; is ascending (parity = t) then the input must be descending (parity
; = nil). This odd requirement allows us to do the merge in a tail
; recursive way, accumulating the answers onto ans. We do it tail
; recursively because we are often called upon to sort huge lists and
; the naive approach has blown the stack of AKCL.
(cond ((null lst1) (duplicitous-revappend-car lst2 ans))
((null lst2) (duplicitous-revappend-car lst1 ans))
((if parity
(> (car (car lst1)) (car (car lst2)))
(< (car (car lst1)) (car (car lst2))))
(duplicitous-merge-car parity (cdr lst1) lst2 (duplicitous-cons-car (car lst1) ans)))
(t (duplicitous-merge-car parity lst1 (cdr lst2) (duplicitous-cons-car (car lst2) ans)))))
(defun duplicitous-sort-car (parity lst)
; Let lst be a list of runes. If parity = t, we sort lst so that the
; numes of the resulting list are ascending; if parity = nil, the
; numes of the resulting list are descending.
; Note: This function is neat primarily because the merge function is
; tail recursive. It is complicated by the entirely extraneous
; requirement that it delete duplicates. The neat thing is that as it
; descends through lst, cutting it in half each time, it recursively
; orders the parts with the opposite sense of ordering. That is, to
; sort into ascending order it recursively sorts the two parts into
; descending order, which it achieves by sorting their parts into
; ascending order, etc.
(cond ((null (cdr lst)) lst)
(t (duplicitous-merge-car parity
(duplicitous-sort-car (not parity) (evens lst))
(duplicitous-sort-car (not parity) (odds lst))
nil))))
(defun augment-theory (lst wrld)
; See also related function runic-theory.
; Given a (common) theory we convert it into an augmented runic
; theory. That is, we replace each designator in lst by the
; appropriate runes, pair each rune with its nume, sort the result and
; remove duplications. In the special case that lst is in fact a
; runic theory -- i.e., is already a properly sorted list of runes --
; we just augment it directly. We expect this case to occur often.
; The various theory manipulation functions take common theories as
; their inputs but produce runic theories as their outputs.
; Internally, they all operate by augmenting the input theory,
; computing with the augmented theory, and then dropping down to the
; corresponding runic theory at the end with strip-cdrs. Thus if two
; such functions are nested in a user-typed theory expression, the
; inner one will generally have non-runic user-typed input but will
; produce runic output as input for the next one. By recognizing
; runic theories as a special case we hope to improve the efficiency
; with which theory expressions are evaluated, by saving the sorting.
(declare (xargs :guard (theoryp lst wrld)))
(cond ((runic-theoryp lst wrld)
(augment-runic-theory lst wrld))
(t (duplicitous-sort-car
nil
(convert-theory-to-unordered-mapping-pairs lst wrld)))))
(defmacro assert$-runic-theoryp (runic-theory-expr wrld)
; Comment out one of the following two definitions.
;;; Faster, without checking:
(declare (ignore wrld))
runic-theory-expr
;;; Slower, with checking:
; `(let ((thy ,runic-theory-expr))
; (assert$ (runic-theoryp thy ,wrld)
; thy))
)
(defun runic-theory (lst wrld)
; Lst is a common theory. We convert it to a runic theory.
; See also related function augment-theory.
(cond ((runic-theoryp lst wrld) lst)
(t (assert$-runic-theoryp
(strip-cdrs
(duplicitous-sort-car
nil
(convert-theory-to-unordered-mapping-pairs lst wrld)))
wrld))))
; We now develop the foundations of the concept that a rune is "enabled" in the
; current theory. In ACL2, the user can get "into" a theory with the in-theory
; event, which is similar in spirit to in-package but selects a theory as the
; "current" theory. A rune is said to be "enabled" if it is a member of the
; runic theory corresponding to the current (common) theory and is said to be
; "disabled" otherwise.
; Historical Note about Nqthm
; Nqthm had no explicit notion of the current theory. However, implicitly,
; nqthm contained a current theory and the events ENABLE and DISABLE allowed
; the user to add a name to it or delete a name from it. The experimental
; xnqthm, mentioned elsewhere in this system, introduced the notion of theories
; and tied them to enabling and disabling, following suggestions and patches
; implemented by Bill Bevier during the Kit proofs (and implemented in
; Pc-Nqthm, and extended in Nqthm-1992). The ACL2 notion of theory is much
; richer because it allows one to compute the value of theories using functions
; defined within the logic. (end of note)
; Suppose we have a theory which has been selected as current. This may be the
; globally current theory, as set by the in-theory event, or it may be a
; locally current theory, as set by the in-theory hint to defthm or defun. We
; must somehow process the current theory so that we can quickly answer the
; question "is rune enabled?" We now develop the code for doing that.
; The structure defined below is used as a fast way to represent a theory:
(defrec enabled-structure
; WARNING: Keep this in sync with enabled-structurep.
((index-of-last-enabling . theory-array)
(array-name . array-length)
array-name-root . array-name-suffix)
t)
(defun enabled-structure-p (ens)
; We use this function in the guards of other functions.
(declare (xargs :guard t))
(and (weak-enabled-structure-p ens)
(array1p (access enabled-structure ens
:array-name)
(access enabled-structure ens
:theory-array))
(symbolp (access enabled-structure ens
:array-name))
(signed-byte-p 30 (access enabled-structure ens
:array-length))
(signed-byte-p 30 (access enabled-structure ens
:index-of-last-enabling))
; The following must be true in order for the array access in enabled-numep to
; be in bounds.
(< (access enabled-structure ens
:index-of-last-enabling)
(access enabled-structure ens
:array-length))
(character-listp (access enabled-structure ens
:array-name-root))
(natp (access enabled-structure ens
:array-name-suffix))
(equal (access enabled-structure ens
:array-length)
(car (dimensions (access enabled-structure ens
:array-name)
(access enabled-structure ens
:theory-array))))))
; The following invariant is maintained in all instances of this structure.
; Theory-array is an array1p whose array length is array-length. Furthermore
; array-name is a symbol of the form rootj, root is the array-name-root (as a
; list of characters) and j is the array-name-suffix (which however is not
; always used; see load-theory-into-enabled-structure). Thus, if i is a
; nonnegative integer less than array-length, then (acl2-aref1 array-name
; theory-array i) has a satisfied guard. Furthermore, important to efficiency
; but irrelevant to correctness, it will always be the case that the von
; Neumann array associated with array-name is in fact theory-array. Thus the
; above expression executes quickly. To get a new array name, should one ever
; be needed, it can suffice to increment the array-name-suffix and build a name
; from that new value. However, if we hope to use parallel evaluation in the
; waterfall, we instead make a unique name based on each clause-id. See
; load-theory-into-enabled-structure.
; The theory-array of an enabled-structure for a given common theory is (except
; for the header entry) just the augmented runic theory corresponding to the
; given common theory. That is, the ACL2 array alist we need to construct for
; a theory maps each array index to a non-nil value. The non-nil value we
; choose is in fact the corresponding rune. It would suffice, for purposes of
; enabling, to store T in the array to signify enabledness. By storing the
; rune itself we make it possible to determine what runic theory is in the
; array. (There is no general purpose way to map from a nume to its rune
; (short of looking through the whole world).)
; The global variable 'global-enabled-structure contains an instance of the
; enabled-structure record in which the array-name is ENABLED-ARRAY-0,
; array-name-root is the list of characters in "ENABLED-ARRAY-" and the
; array-name-suffix is 0. A rune with nume n is (globally) enabled in the
; current world iff either n is greater than the index-of-last-enabling or
; array[n] is non-nil. This is just the computation done by enabled-numep,
; below.
; The in-theory event loads the 'global-enabled-structure with the theory-value
; and sets the index-of-last-enabling to the maximum nume at that time. This
; structure is passed into prove and thus into rewrite, etc.
; When an in-theory hint setting is provided we change the array name
; appropriately and load the local theory into that structure. We flush each
; such array in order to allow it to be garbage collected; see
; restore-hint-settings-in-pspv.
; Historical Note about Nqthm
; In nqthm we solved this problem by having a list of temporarily disabled
; names which was bound when there were local enabling hint settings. That
; implementation suffered because if hundreds of names were enabled locally the
; time spent searching the list was excessive. In xnqthm we solved that
; problem by storing the enabled status on the property list of each name. We
; could do that here. However, that implementation suffered from the fact that
; if a proof attempt was aborted then we had to carefully clean up the property
; list structures so that they once again reflected the current (global)
; theory. The beauty of the ACL2 approach is that local hint settings have no
; affect on the global theory and yet involve no overhead.
; A delicacy of the current implementation however concerns the relation
; between the global enabled structure and undoing. If the world is backed up
; to some previous point, the 'global-enabled-structure extant there is exposed
; and we are apparently ready to roll. However, the von Neumann array named by
; that structure may be out-dated in the sense that it contains a now undone
; theory. Technically there is nothing wrong with this, but if we let it
; persist things would be very slow because the attempt to access the
; applicative array would detect that the von Neumann array is out of date and
; would result in a linear search of the applicative array. We must therefore
; compress the applicative array (and hence reload the von Neumann one)
; whenever we back up.
; Finally, there is one last problem. Eventually the array-size of the array
; in one of these structures will be too small. This manifests itself when the
; maximum rule index at the time we load the structure is equal to or greater
; than the array-length. At that time we grow the array size by 500.
; Here is how we use an enabled structure, ens, to determine if a nume, rune,
; or function is enabled.
(defun enabled-numep (nume ens)
; This function takes a nume (or nil) and determines if it is enabled
; in the enabled structure ens. We treat nil as though it were
; enabled.
(declare (type (or null (integer 0 *))
nume)
(xargs :guard (enabled-structure-p ens)))
(cond ((null nume) t)
((> nume
(the-fixnum
(access enabled-structure ens :index-of-last-enabling)))