1
#| KAS - Kernel Architecture Simplifier |#
5
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
6
#| Some logical functions needed to define KAS operation |#
7
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
11
(defun symbol-appendp (x) (or (symbolp x) (stringp x) (natp x)))
13
(defun dec-to-string (d)
14
(case d (0 "0") (1 "1") (2 "2") (3 "3") (4 "4") (5 "5") (6 "6") (7 "7") (8 "8") (t "9")))
16
(defun nat-to-string (n)
17
(string-append (if (zp (floor n 10)) "" (nat-to-string (floor n 10)))
18
(dec-to-string (mod n 10))))
20
(defun symbol-append-string (x)
21
(cond ((symbolp x) (symbol-name x))
23
(t (nat-to-string x))))
25
(defun symbol-binary-append (x y)
26
(declare (xargs :guard (and (symbol-appendp x) (symbol-appendp y))))
27
;; (intern-in-package-of-symbol (string-append (symbol-name x) (symbol-name y)) x))
28
(intern (string-append (symbol-append-string x) (symbol-append-string y)) "ACL2"))
30
(defmacro symbol-append (symb1 symb2 &rest symbs)
31
`(symbol-binary-append ,symb1 ,(if (endp symbs) symb2 `(symbol-append ,symb2 ,@symbs))))
33
(defun make-hyps-and-args-list (n)
34
(if (zp n) () (cons (symbol-append 'x n) (make-hyps-and-args-list (1- n)))))
36
(defun make-hyps-and-fn (n)
37
`(defun ,(symbol-append 'hyps-and- n) ,(make-hyps-and-args-list n)
38
(and ,(symbol-append 'x n)
39
,(cons (symbol-append 'hyps-and- (1- n))
40
(make-hyps-and-args-list (1- n))))))
42
(defun make-hyps-and-fns (n r)
43
(if (zp n) r (make-hyps-and-fns (1- n) (cons (make-hyps-and-fn n) r))))
47
(defun siv (x) (declare (ignore x)) t)
48
(defthm siv-rewrite (equal (siv x) t))
49
(in-theory (disable siv (siv)))
52
(defmacro sieve (x) `(siv (quote ,x)))
53
(defun hyps-and-0 () ())
54
(defmacro make-hyps-and-functions (n)
55
(declare (xargs :guard (natp n)))
56
(cons 'progn (make-hyps-and-fns n ())))
57
(make-hyps-and-functions 63) ; greater value can cause CCL compiler warnings
59
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
60
#| ACL2 interface macros and functions |#
61
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
65
(defmacro kern-comp ()
73
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
74
#| definition of stobj+ macros |#
75
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
77
; We define a bunch of macros for defining functions which use stobj+'s.
78
; Basically, these macros lift the main program from overnotating several
79
; common structures encountered in programming with stobjs.
81
(defmacro kern-fixnum-size () 61)
82
(defmacro my-fixnum (x) `(the (signed-byte ,(kern-fixnum-size)) ,x))
84
(defun gen-stobj+-renaming (flds stb)
86
(let ((name (caar flds))
88
(append (if (member-eq type '(:fixnum :object))
90
(symbol-append 'get- name))
91
(list (symbol-append 'update- name)
92
(symbol-append 'set- name))
93
(list (symbol-append name 'p)
94
(symbol-append stb '- name 'p)))
95
(list (list (symbol-append name 'i)
96
(symbol-append 'get- name))
97
(list (symbol-append 'update- name 'i)
98
(symbol-append 'set- name))
99
(list (symbol-append name 'p)
100
(symbol-append stb '- name 'p))
101
(list (symbol-append 'resize- name)
102
(symbol-append stb '-resize- name))
103
(list (symbol-append name '-length)
104
(symbol-append 'length- name))))
105
(gen-stobj+-renaming (cdr flds) stb)))))
107
(defun process-stobj+-fields (flds)
109
(cons (cons (caar flds)
111
(:fixnum `(:type (signed-byte ,(kern-fixnum-size))
113
(:fixnum-array `(:type (array (signed-byte ,(kern-fixnum-size)) (0))
118
(:object-array `(:type (array T (0))
121
(otherwise (er hard 'process-stobj+-fields
122
"ill-formed stobj+ definition"))))
123
(process-stobj+-fields (cdr flds)))))
125
(defun stobj+-resize-funcs (flds stb)
126
(cond ((endp flds) ())
127
((member-eq (cadar flds) '(:fixnum :object))
128
(stobj+-resize-funcs (cdr flds) stb))
130
(cons `(defun ,(symbol-append 'resize- (caar flds))
132
(declare (xargs :stobjs ,stb))
133
(if (eql size (,(symbol-append 'length- (caar flds)) ,stb))
135
(prog2$ (and (,(symbol-append 'get- stb '-resize-array-display)
138
(quote ,(symbol-append 'resize- (caar flds)))
140
(,(symbol-append stb '-resize- (caar flds)) size ,stb))))
141
(stobj+-resize-funcs (cdr flds) stb)))))
143
(defun stobj+-clear-arr-funcs (flds stb)
144
(cond ((endp flds) ())
145
((member-eq (cadar flds) '(:fixnum :object))
146
(stobj+-clear-arr-funcs (cdr flds) stb))
148
(let ((clear-arr-fn (symbol-append `clear-arr- (caar flds)))
149
(set-arr-fn (symbol-append 'set- (caar flds)))
150
(clear-obj (if (eq (cadar flds) :fixnum-array) 0 nil)))
151
(cons `(defun ,clear-arr-fn (N ,stb)
152
(declare (xargs :stobjs ,stb)
153
(type (signed-byte ,(kern-fixnum-size)) N))
156
(declare (type (signed-byte ,(kern-fixnum-size)) N))
157
(let ((,stb (,set-arr-fn N ,clear-obj ,stb)))
158
(,clear-arr-fn N ,stb)))))
159
(stobj+-clear-arr-funcs (cdr flds) stb))))))
161
(defun stobj+-clear-func (flds stb)
165
(:fixnum (list (symbol-append 'set- (caar flds)) 0 stb))
166
(:object (list (symbol-append 'set- (caar flds)) nil stb))
167
(t (list (symbol-append 'clear-arr- (caar flds))
168
(list (symbol-append 'length- (caar flds)) stb)
170
(stobj+-clear-func (cdr flds) stb))))
172
(defun built-in-stobj+-fields (stobj-name)
173
(list (list (symbol-append stobj-name '-resize-array-display) :object)))
175
(defmacro define-stobj+ (stobj-name &rest fields)
176
(let ((fields (append fields (built-in-stobj+-fields stobj-name))))
178
(append (list `(defstobj ,stobj-name
179
,@(process-stobj+-fields fields)
181
:renaming ,(gen-stobj+-renaming fields stobj-name)))
182
(stobj+-resize-funcs fields stobj-name)
183
(stobj+-clear-arr-funcs fields stobj-name)
184
(list `(defun ,(symbol-append 'clear- stobj-name)
186
(declare (xargs :stobjs ,stobj-name))
187
(let* ,(stobj+-clear-func fields stobj-name)
190
;; now we define some macros for defining record-arrays. These are records stored consecutively
191
;; in possibly different arrays which are declared with special types.
193
(defun stobj+-record-fields-fn (stb fields array object type ctr)
195
(let ((field (first fields)))
196
(list* `(defmacro ,(symbol-append object (intern "." "ACL2") field)
198
,(let ((form `(list ',(symbol-append 'get- array)
200
`(list ',(symbol-append array '-arr-ndx) ,object)
202
(list ',(symbol-append array '-arr-ndx) ,object)
205
(if (eq type :fixnum)
206
`(list 'my-fixnum ,form)
208
`(defmacro ,(symbol-append object '.set- field)
210
(list ',(symbol-append 'set- array)
212
`(list ',(symbol-append array '-arr-ndx) ,object)
214
(list ',(symbol-append array '-arr-ndx) ,object)
216
,(if (eq type :fixnum)
217
`(list 'my-fixnum ,field)
220
(stobj+-record-fields-fn stb (rest fields) array object type (1+ ctr))))))
222
(defun stobj+-record-fields (fields stb object)
224
(let* ((fld (first fields))
226
(rcd-size (len (third fld))))
227
(cons `(defmacro ,(symbol-append (second fld) '-arr-ndx)
230
`(list '*^ (list 'my-fixnum ,object) ,rcd-size)
231
`(list 'my-fixnum ,object)))
232
(append (stobj+-record-fields-fn stb (third fld) array object (first fld) 0)
233
(stobj+-record-fields (rest fields) stb object))))))
235
(defun resize-rcd-arr-calls (fields stb)
237
(let ((array (second (first fields)))
238
(rcd-size (length (third (first fields)))))
239
(cons (list stb (list (symbol-append 'resize- array)
240
`(*^ (+^ ptr extra 1) ,rcd-size)
242
(resize-rcd-arr-calls (rest fields) stb)))))
244
(defun merge-fields-into-list (fields)
246
(append (third (first fields))
247
(merge-fields-into-list (rest fields)))))
249
(defun merge-fields-into-object-arr (fields)
250
(let ((obj-arr (second (assoc :object fields))))
252
(list (list :object obj-arr (merge-fields-into-list fields)))
255
(defmacro define-stobj+-record-array (stb object merge-into-obj-arr &rest fields)
256
(let ((fields (if merge-into-obj-arr
257
(merge-fields-into-object-arr fields)
259
(let ((array (second (first fields)))
260
(rcd-size (len (third (first fields)))))
262
`(defabbrev ,(symbol-append 'num-of- object)
264
(let ((size (,(symbol-append 'length- array) ,stb)))
265
(declare (type (signed-byte ,(kern-fixnum-size)) size))
266
(floor^ size ,rcd-size)))
267
`(defabbrev ,(symbol-append 'ensure- object)
269
(declare (type (signed-byte ,(kern-fixnum-size)) ptr extra))
270
(let ((size (,(symbol-append 'length- array) ,stb)))
271
(declare (type (signed-byte ,(kern-fixnum-size)) size))
272
(if (<^ (*^ (1+^ ptr) ,rcd-size) size)
274
(let* ,(resize-rcd-arr-calls fields stb)
276
`(defabbrev ,(symbol-append 'restrict- object)
278
(declare (type (signed-byte ,(kern-fixnum-size)) ptr))
279
(let ((size (,(symbol-append 'length- array) ,stb)))
280
(if (=^ (*^ (1+^ ptr) ,rcd-size) size)
283
(let* ,(resize-rcd-arr-calls fields stb)
285
(stobj+-record-fields fields stb object)))))
287
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
288
#| utility functions and macros |#
289
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
291
(defun kern-monitor-comp () nil) ; enable/disable monitor code at compile-time
292
(defun kern-monitor-run () nil) ; enable/disable monitor code at run-time
293
(defun kern-assert-comp () t) ; enable/disable assert code at compile-time
294
(defun kern-merge-arrays () nil) ; should be NIL for GCL, T for Franz
296
; enables for various inline checks for compiled code
298
(defun kern-enable-check-<^s () nil)
299
(defun kern-enable-check-fixns () nil)
300
(defun kern-enable-temp-recording () t)
302
; kern-display is a simple macro which is used to add some display code
303
; kern-monitor actually performs a test to see if it should display or not and
304
; can be disabled at compile
306
(defmacro kern-display (&rest x)
307
(declare (xargs :guard (>= (len x) 1)))
308
`(prog2$ (cw ,@(butlast x 1)) ,(car (last x))))
310
(defmacro kern-monitor (&rest x)
311
(declare (xargs :guard (>= (len x) 2)))
312
(if (kern-monitor-comp)
313
`(prog2$ (and (kern-monitor-run)
315
(cw ,@(butlast (cdr x) 1)))
319
; kern-assert is used to declare an assertion which is checked before
320
; evaluating the body term provided.
322
(defmacro kern-force-assert (mbt body)
323
(let ((r (if (atom mbt) (list mbt) mbt)))
324
`(prog2$ (and (not (eq ,mbt t))
325
(er hard (quote (assert ,@r))
326
"assert non-T value: ~x0"
330
(defmacro kern-assert (mbt body)
331
(if (kern-assert-comp)
332
`(kern-force-assert ,mbt ,body)
335
; The macro define-stobj+-record-array is defined in stobjp.lisp. This is
336
; simply a wrapper macro.
338
(defmacro define-kern-record-array (record &rest fields)
339
`(define-stobj+-record-array ls$ ,record
343
(defmacro define-user-record-array (record &rest fields)
344
`(define-stobj+-record-array us$ ,record
348
; We often wish to pass back multiple values such that the first is a fixnum.
349
; This declares that the first value in the mv is a fixnum which keeps it from
350
; being boxed (mainly of use in GCL).
352
(defmacro mv^ (x &rest rest)
353
`(mv (my-fixnum ,x) ,@rest))
355
; We now define the letk which is our general purpose let-form which
356
; automatically includes the necessary fixnum declarations, introduces mv-lets
357
; when appropriate, and handles propogation of errors (when appropriate). We
358
; use a variable and function name scheme to allow the letk macro determine the
359
; "type" of the variable and function calls. Basically in any letk binding, the
360
; first return value is always a fixnum unless it is a stobj (which is either
361
; 'state or ends in the character #\$). For functions, if a function ends in a
362
; #\! character then it may return an "error" which will need to be propagated.
363
; The letk macro is essentially written for the kernel functions in this file
364
; and really should not be used in any other context. If a more generic let
365
; form could be conceived which achieved the uses here, then please make the
366
; suggestion to the ACL2 maintainers.
368
(defun is-letk-stobj-var (x)
372
(let ((s (symbol-name x)))
373
(eql (char s (1- (length s))) #\$)))))
375
(defun is-letk-object-var (x)
378
(let ((s (symbol-name x)))
379
(eql (char s (1- (length s))) #\.))))
381
(defun is-letk-fixnum-var (x)
383
(not (or (booleanp x)
385
(is-letk-stobj-var x)
386
(is-letk-object-var x)))))
388
(defun drop-list-last (x)
389
(if (endp (rest x)) ()
391
(drop-list-last (rest x)))))
393
(defun legal-var-listp (x)
396
(or (symbolp (car x))
400
(legal-var-listp (cdr x)))))
402
(defun letk-binding-entryp (x)
405
(legal-var-listp (drop-list-last x))
406
(or (atom (car (last x)))
407
(symbolp (caar (last x))))))
409
(defun letk-bindingp (x)
412
(letk-binding-entryp (first x))
413
(letk-bindingp (rest x)))))
415
(defmacro letk (bind rslt)
416
(declare (xargs :guard (letk-bindingp bind)))
418
(let ((b (first bind)))
420
(let* ((lhs (first b))
421
(is-fixn (is-letk-fixnum-var lhs))
422
(rhs (if (and is-fixn (kern-enable-check-fixns))
423
`(the (signed-byte ,(kern-fixnum-size)) ,(second b))
427
`((declare (type (signed-byte ,(kern-fixnum-size)) ,lhs))))
428
(letk (,@(rest bind)) ,rslt)))
429
(let* ((lhs (drop-list-last b))
431
(is-fixn (is-letk-fixnum-var (first lhs))))
434
`((declare (type (signed-byte ,(kern-fixnum-size)) ,(first lhs)))))
435
,(let ((body `(letk (,@(rest bind)) ,rslt)))
436
(if (and is-fixn (kern-enable-check-fixns))
437
`(let ((,(first lhs) (the (signed-byte ,(kern-fixnum-size)) ,(first lhs))))
438
(declare (type (signed-byte ,(kern-fixnum-size)) ,(first lhs)))
442
(defun defunk-fixnum-vars (vars)
443
(cond ((endp vars) ())
444
((is-letk-fixnum-var (first vars))
446
(defunk-fixnum-vars (rest vars))))
447
(t (defunk-fixnum-vars (rest vars)))))
449
(defun defunk-type-declare (vars)
450
(let ((vars (defunk-fixnum-vars vars)))
451
(and vars `((declare (type (signed-byte ,(kern-fixnum-size)) ,@vars))))))
453
(defun defunk-stobj-vars (vars)
454
(cond ((endp vars) ())
455
((is-letk-stobj-var (first vars))
457
(defunk-stobj-vars (rest vars))))
458
(t (defunk-stobj-vars (rest vars)))))
460
(defun defunk-stobj-declare (vars)
461
(let ((vars (defunk-stobj-vars vars)))
462
(and vars `((declare (xargs :stobjs ,vars))))))
464
(defconst *defunk-sig-vars*
465
'(a b c d e f g h i j k l m n o p q r s t u v w x y z))
467
(defun defunk-create-sig (args vars)
468
(cond ((endp args) ())
469
((is-letk-stobj-var (first args))
471
(defunk-create-sig (rest args) vars)))
473
(er hard 'defunk-create-sig
477
(defunk-create-sig (rest args) (rest vars))))))
480
(defun defunk-mv-sig (term)
483
(mv^ (defunk-create-sig (rest term) *defunk-sig-vars*))
484
(if (or (defunk-mv-sig (third term)) (defunk-mv-sig (fourth term))))
485
(letk (defunk-mv-sig (third term)))
486
(cond (defunk-cond-sig (rest term)))
487
(case (defunk-cond-sig (rest (rest term))))
488
((kern-assert kern-error prog2$) (defunk-mv-sig (third term))))))
490
(defun defunk-cond-sig (conds)
492
(or (defunk-mv-sig (second (first conds)))
493
(defunk-cond-sig (rest conds)))))
496
(defconst *kern-fixnum-ops*
497
'(+^ -^ *^ floor^ logand^ my-fixnum lognot^
498
logior^ logxor^ mod^ expt^ max^ min^ ash^
499
abs^ er0 1+^ 1-^ mask^ dctx-0 kern-make-opcd))
502
(defun defunk-fixnum-body (term)
504
((is-letk-fixnum-var term) t)
506
(t (case (first term)
507
(if (or (defunk-fixnum-body (third term))
508
(defunk-fixnum-body (fourth term))))
509
(letk (defunk-fixnum-body (third term)))
510
(cond (defunk-cond-fixnum (rest term)))
511
(case (defunk-cond-fixnum (rest (rest term))))
512
((kern-assert kern-error prog2$)
513
(defunk-fixnum-body (fourth term)))
514
(t (member-eq (first term) *kern-fixnum-ops*))))))
516
(defun defunk-cond-fixnum (conds)
518
(or (defunk-fixnum-body (second (first conds)))
519
(defunk-cond-fixnum (rest conds)))))
522
(defun defunk-tag-body (body)
523
(if (defunk-fixnum-body body) `(my-fixnum ,body)
524
(let ((sig (defunk-mv-sig body)))
525
(if sig `(the-mv ,sig (signed-byte ,(kern-fixnum-size)) ,body)
528
(defun defunk-make-binds (vars)
530
(cons (list (first vars) (first vars))
531
(defunk-make-binds (rest vars)))))
533
(defconst *defunk-body-primitives*
534
'(+ * 1+ = 1- - /= <= < > >=
535
+^ *^ 1+^ =^ 1-^ -^ /=^ <=^ <^ >^ >=^
536
mod mod^ floor floor^ expt expt^
538
logand logand^ logior logior^
539
lognot lognot^ logxor logxor^
541
mask^ mv mv^ my-fixnum
542
er er0 prog2$ cw ev-fncall-w
543
fn-count-evg lexorder
544
if not implies and or iff
545
acl2-numberp rationalp integerp consp
546
characterp symbolp stringp
547
booleanp termp keywordp
548
true-listp symbol-listp
549
cons null atom endp list list* push-lemma
550
car cdr caar cdar cadr cddr cadar
551
first second third fourth fifth
552
sixth seventh eighth ninth tenth
553
rest last butlast nth nthcdr update-nth
554
append length reverse revappend string-append
555
acons assoc assoc-eq assoc-equal
556
strip-cars strip-cdrs
557
numerator denominator realpart imagpart
558
char-code char code-char
559
symbol-name symbol-package-name
560
intern intern-in-package-of-symbol
563
member-eq member member-equal
566
(defconst *defunk-body-prefixes*
567
'(get- set- length- resize- ensure- num-of- restrict-
568
candidate. undo. qobj. rule. oper. node. opcd. memo. loop.))
570
(defun str-has-prefix (x y i)
571
(or (>= i (length y))
572
(and (< i (length x))
573
(eql (char x i) (char y i))
574
(str-has-prefix x y (1+ i)))))
576
(defun symb-has-prefix (x y)
577
(str-has-prefix (symbol-name x)
581
(defun symb-prefixes (x lst)
582
(and (not (endp lst))
583
(or (symb-has-prefix x (first lst))
584
(symb-prefixes x (rest lst)))))
586
(defun is-kern-primitive (op)
587
(or (member-eq op *defunk-body-primitives*)
588
(symb-prefixes op *defunk-body-prefixes*)))
590
(defun map-kern-op (op)
591
(if (is-kern-primitive op) op (symbol-append 'kern- op)))
594
(defun add-kern-to-calls (term)
595
(cond ((atom term) term)
596
((eq (first term) 'quote) term)
597
((eq (first term) 'cond)
599
(add-kern-to-conds (rest term))))
600
((eq (first term) 'case)
602
(add-kern-to-calls (second term))
603
(add-kern-to-binds (rest (rest term)))))
604
((eq (first term) 'letk)
606
(add-kern-to-binds (second term))
607
(add-kern-to-calls (third term))))
609
(cons (map-kern-op (first term))
610
(add-kern-to-args (rest term))))))
612
(defun add-kern-to-args (args)
614
(cons (add-kern-to-calls (first args))
615
(add-kern-to-args (rest args)))))
617
(defun add-kern-to-binds (binds)
619
(cons (append (butlast (first binds) 1)
620
(add-kern-to-args (last (first binds))))
621
(add-kern-to-binds (rest binds)))))
623
(defun add-kern-to-conds (conds)
625
(cons (add-kern-to-args (first conds))
626
(add-kern-to-conds (rest conds)))))
629
(defun mk-defunk (name vars inlined decls body)
630
(kern-assert (and (symbolp name)
632
(let* ((name (map-kern-op name))
633
(body (add-kern-to-calls body))
634
(body (if (kern-enable-check-fixns)
635
`(letk ,(defunk-make-binds (defunk-fixnum-vars vars))
639
`(defabbrev ,name ,vars ,@decls
640
,@(defunk-type-declare vars)
641
,(defunk-tag-body body))
642
`(defun ,name ,vars ,@decls
643
,@(defunk-type-declare vars)
644
,@(defunk-stobj-declare vars)
645
,(defunk-tag-body body))))))
647
(defun parse-defunk-args (args)
648
(let* ((inlined (and (consp args)
649
(eq (first args) :inline)))
650
(args (if inlined (rest args) args)))
651
(mv inlined (butlast args 1) (car (last args)))))
653
(defmacro defunk (name vars &rest args)
655
(let ((body (add-kern-to-calls vars)))
656
(list 'defmacro (symbol-append 'kern- name) ()
657
(list 'let (list (list 'x body)) (list 'list ''quote 'x))))
658
(mv-let (inlined decls body) (parse-defunk-args args)
659
(mk-defunk name vars inlined decls body))))
661
(defun split-defunks (fns)
662
(if (endp fns) (mv () ())
663
(let ((fn (first fns)))
664
(kern-assert (and (true-listp fn)
666
(eq (first fn) 'defunk))
667
(mv-let (inlined decls body)
668
(parse-defunk-args (rest (rest (rest fn))))
669
(let ((fn (mk-defunk (second fn) (third fn)
670
inlined decls body)))
671
(mv-let (abbrevs funcs)
672
(split-defunks (rest fns))
673
(if (and (consp fn) (eq (first fn) 'defabbrev))
674
(mv (cons fn abbrevs) funcs)
675
(mv abbrevs (cons fn funcs))))))))))
677
(defmacro mutual-recursionk (&rest fns)
678
(mv-let (abbrevs funcs) (split-defunks fns)
679
(cons 'progn (append abbrevs (list (cons 'mutual-recursion funcs))))))
681
;; a node which has been "promoted" or is persistent will have a pointer value
684
;; we exclude 0 = (node-btm) as a special node
685
(defunk promoted (x) :inline (>^ x 0))
686
(defunk temp-node (x) :inline (<^ x 0))
688
(defunk node< (x y) :inline
689
(assert (and (promoted x)
693
(defmacro kern-check-<^ (x y ctx)
694
(if (kern-enable-check-<^s)
697
(er0 hard ,ctx "expected decreasing ~x0 < ~x1" ,x ,y)))
700
; We now defined several macros which are "fixnum" verions of existing
701
; functions and primitives.
703
(defmacro -^ (x &rest y)
704
(if (consp y) `(my-fixnum (- (my-fixnum ,x) (my-fixnum ,(first y))))
705
`(my-fixnum (- (my-fixnum ,x)))))
706
(defmacro +^ (x &rest y)
707
(if (endp y) `(my-fixnum ,x)
708
`(my-fixnum (+ (my-fixnum ,x) (+^ ,(first y) ,@(rest y))))))
709
(defmacro *^ (x &rest y)
710
(if (endp y) `(my-fixnum ,x)
711
`(my-fixnum (* (my-fixnum ,x) (*^ ,(first y) ,@(rest y))))))
712
(defmacro 1+^ (x) `(my-fixnum (1+ (my-fixnum ,x))))
713
(defmacro 1-^ (x) `(my-fixnum (1- (my-fixnum ,x))))
714
(defmacro ash^ (x y) `(my-fixnum (ash (my-fixnum ,x) (my-fixnum ,y))))
715
(defmacro =^ (x y) `(eql (my-fixnum ,x) (my-fixnum ,y)))
716
(defmacro <^ (x y) `(< (my-fixnum ,x) (my-fixnum ,y)))
717
(defmacro mod^ (x y) `(my-fixnum (mod (my-fixnum ,x) (my-fixnum ,y))))
718
(defmacro floor^ (x y) `(my-fixnum (floor (my-fixnum ,x) (my-fixnum ,y))))
719
(defmacro expt^ (x y) `(my-fixnum (expt (my-fixnum ,x) (my-fixnum ,y))))
720
(defmacro lognot^ (x) `(my-fixnum (lognot (my-fixnum ,x))))
721
(defmacro logand^ (x &rest y)
722
`(my-fixnum ,(if (endp y) x `(logand (my-fixnum ,x) (logand^ ,(first y) ,@(rest y))))))
723
(defmacro logior^ (x &rest y)
724
`(my-fixnum ,(if (endp y) x `(logior (my-fixnum ,x) (logior^ ,(first y) ,@(rest y))))))
725
(defmacro logxor^ (x &rest y)
726
`(my-fixnum ,(if (endp y) x `(logxor (my-fixnum ,x) (logxor^ ,(first y) ,@(rest y))))))
728
(defmacro mask^ (x y) `(my-fixnum (logand ,x ,y)))
730
(defmacro /=^ (x y) `(not (=^ ,x ,y)))
731
(defmacro <=^ (x y) `(<= (my-fixnum ,x) (my-fixnum ,y)))
732
(defmacro >^ (x y) `(<^ ,y ,x))
733
(defmacro >=^ (x y) `(<=^ ,y ,x))
735
(defmacro max^ (x &rest r)
741
(defmacro min^ (x &rest r)
747
(defmacro er0 (&rest args) `(prog2$ (er ,@args) 0))
749
; The following macro is simply a wrapper for getprop. The
750
; variable wrld is captured from the current context and is
751
; expected to be the current ACL2 world.
753
(defmacro kern-getprop (name prop)
754
`(getprop ,name ,prop nil 'current-acl2-world wrld))
756
; (defunk zp (x) :inline (or (not (integerp x)) (<=^ x 0)))
757
(defunk zp (x) :inline (<=^ x 0))
758
(defunk absf (x) :inline (if (<^ x 0) (-^ x) x))
759
(defunk is-boolean (x.) :inline (or (eq x. t) (eq x. nil)))
760
(defunk is-natrual (x.) :inline (and (integerp x.) (>= x. 0)))
761
(defunk is-trace-mark (x.) :inline (or (is-boolean x.) (eq x. :all)))
763
(defunk spcs (n) (if (zp n) "" (string-append " " (spcs (1- n)))))
765
(defunk max-fixnum (1- (expt 2 60)))
766
(defunk min-fixnum (- (expt 2 60)))
767
(defunk maximum-array-size (max-fixnum))
769
(defunk fixnump (x) :inline
772
(<= x (max-fixnum))))
774
(kern-comp) ;; compile to get macros compiled
776
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
777
#| ls$ stobj, structures, and access functions |#
778
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
780
; We now define the stobj used in the kernel functions. The stobj is called
781
; ls$ which stands for "logic state stobj".
784
(node-stor :fixnum-array)
785
(node-hash :fixnum-array)
786
(alloc-nodes :fixnum)
787
(num-of-nodes :fixnum)
788
(quote-stor :object-array)
789
(quote-hash :fixnum-array)
794
(trans-stor :fixnum-array)
795
(trans-hash :fixnum-array)
796
(alloc-trans :fixnum)
797
(num-trans-nodes :fixnum)
798
(memo-stor :fixnum-array)
799
(loop-stack :fixnum-array)
800
(loop-stk-top :fixnum)
801
(op-obj-stor :object-array)
802
(op-fix-stor :fixnum-array)
803
(next-op-ndx :fixnum)
804
(op-hash :fixnum-array)
805
(undo-stk :fixnum-array)
806
(undo-chains :fixnum-array)
808
(undo-free-list :fixnum)
809
(rule-fix-stor :fixnum-array)
810
(rule-obj-stor :object-array)
811
(next-rule-ndx :fixnum)
812
(curr-ctx-stk :fixnum-array)
813
(curr-ctx-top :fixnum)
814
(current-world :object)
815
(current-ens :object)
816
(var-chg-stk :fixnum)
817
(current-age :fixnum)
818
(bchain-limit :fixnum)
819
(next-extend-age :fixnum)
820
(current-dctx :fixnum)
821
(warned-ctx-depth :object)
822
(current-clock :fixnum)
823
(output-verbose :object)
824
(kern-size-param :object)
826
(flip-nil-fns :object)
827
(allow-context-reduction :object)
828
(initial-rule-trace-descriptor :object)
829
(initial-node-prune-depth :object)
830
(rew-call-depth :fixnum) ;; only used for debugging
833
(define-kern-record-array memo
834
(:fixnum memo-stor (opcd rslt dcv arg0 arg1 arg2)))
836
(define-kern-record-array undo
837
(:fixnum undo-stk (node rep dcv chain)))
839
(define-kern-record-array qobj
840
(:object quote-stor (obj uniq-chain)))
842
(define-kern-record-array oper
843
(:object op-obj-stor (name is-var is-if is-equal non-nil rules boolp assume-tbr assume-fbr))
844
(:fixnum op-fix-stor (next-stk bound narg uniq-chain num-nodes num-trans exec)))
846
(define-kern-record-array rule
847
(:object rule-obj-stor (rune sieves enabled traced))
848
(:fixnum rule-fix-stor (ctr tryctr lhs rhs op hyps)))
850
(define-kern-record-array loop
851
(:fixnum loop-stack (rule node)))
853
; We may use more than one memo slot if the num. args for the fn is greater
854
; than 3. In order to facilitate this definition, we include the following
855
; definition of arg access/update functions
857
(defunk opcd-memo-mrkr -1)
858
(defunk max-memo-narg 9)
859
(defunk num-1memo-args 3)
861
(defunk memo.arg (x i) :inline
862
(assert (<^ i (max-memo-narg))
867
(3 (memo.rslt (1+^ x)))
868
(4 (memo.dcv (1+^ x)))
869
(5 (memo.arg0 (1+^ x)))
870
(6 (memo.arg1 (1+^ x)))
871
(t (memo.arg2 (1+^ x))))))
873
(defunk memo.set-arg (x i v) :inline
874
(assert (<^ i (max-memo-narg))
876
(0 (memo.set-arg0 x v))
877
(1 (memo.set-arg1 x v))
878
(2 (memo.set-arg2 x v))
879
(3 (memo.set-rslt (1+^ x) v))
880
(4 (memo.set-dcv (1+^ x) v))
881
(5 (memo.set-arg0 (1+^ x) v))
882
(6 (memo.set-arg1 (1+^ x) v))
883
(t (memo.set-arg2 (1+^ x) v)))))
885
; We include a "wrapper" for oper.uniq which checks if the uniq-ptr retrieved
886
; is strictly less than o. This should be an invariant of the construction of
887
; nodes, but we add this "wrapper" to help in admitting various functions which
888
; traverse nodes. BOZO -- need to check if this affects performance appreciably
889
; and note here whether or not it does.
891
(defunk oper.uniq (o) :inline
892
(letk ((uniq (oper.uniq-chain o)))
893
(check-<^ uniq o 'oper.uniq)))
895
(defunk oper.set-uniq (o uniq) :inline
896
(oper.set-uniq-chain o uniq))
898
; We include a "wrapper" for qobj.uniq which checks if the uniq-ptr retrieved
899
; is strictly less than q. This should be an invariant of the construction of
900
; nodes, but we add this "wrapper" to help in admitting various functions which
901
; traverse nodes. BOZO -- need to check if this affects performance appreciably
902
; and note here whether or not it does.
904
(defunk qobj.uniq (q) :inline
905
(letk ((uniq (qobj.uniq-chain q)))
906
(check-<^ uniq q 'qobj.uniq)))
908
(defunk qobj.set-uniq (q uniq) :inline
909
(qobj.set-uniq-chain q uniq))
912
;; A node consists of the following fields (each encoded in a fixnum) at an
913
;; offset from a base address for the node:
915
;; offset 0: <vcnt[14],fcnt[14]>,<in-ctx>,<user-mark>,<op[18],equal[1],if[1],var[1],narg[9]> <-- count[28],user-mark[1],in-ctx[1],opcd[30]
916
;; offset -1: rep[60]/age[60]
917
;; offset -2: dcv[60]
918
;; offset -3: uniq[60]
919
;; offset -4: arg1[60]
922
(defunk avg-num-args 3)
923
(defunk base-node-alloc 4)
924
(defunk base-trans-alloc 1)
926
(defunk var-mask (ash 1 10))
927
(defunk non-var-mask (lognot (var-mask)))
928
(defunk if-mask (ash (var-mask) 1))
929
(defunk equal-mask (ash (if-mask) 1))
930
(defunk opndx-shft (ash (equal-mask) 1))
931
(defunk narg-mask (1- (var-mask)))
932
(defunk opcd-mask (1- (ash 1 30)))
933
(defunk in-ctx-mask (ash 1 31))
934
(defunk in-ctx-flip (lognot (in-ctx-mask)))
935
(defunk user-mark-mask (ash 1 32))
936
(defunk user-mark-flip (lognot (user-mark-mask)))
938
(defunk size-shft (ash 1 32))
939
(defunk non-size-mask (1- (size-shft)))
940
(defunk size-mask (lognot (non-size-mask)))
941
(defunk vcnt-shft (ash 1 14))
942
(defunk fcnt-mask (1- (vcnt-shft)))
944
(defunk max-num-args (narg-mask))
945
(defunk max-num-fns (- (ash 1 18) 2))
946
(defunk max-size-valu (1- (ash 1 28)))
947
(defunk size-btm (max-size-valu))
948
(defunk max-fcnt-valu (fcnt-mask))
949
(defunk max-vcnt-valu (1- (ash 1 14)))
952
(defunk opcd.is-var (o) :inline (=^ (logand^ o (var-mask)) (var-mask)))
953
(defunk opcd.is-if (o) :inline (=^ (logand^ o (if-mask)) (if-mask)))
954
(defunk opcd.is-equal (o) :inline (=^ (logand^ o (equal-mask)) (equal-mask)))
955
(defunk opcd.narg (o) :inline (logand^ o (narg-mask)))
956
(defunk opcd.index (o) :inline (floor^ o (opndx-shft)))
958
(defunk make-opcd (narg var. is-if. is-eq. ndx) :inline
959
(logior^ (*^ ndx (opndx-shft))
960
(if is-eq. (equal-mask) 0)
961
(if is-if. (if-mask) 0)
962
(if var. (var-mask) 0)
965
(defunk get-size-fcnt (size) :inline (logand^ size (fcnt-mask)))
966
(defunk get-size-vcnt (size) :inline (floor^ size (vcnt-shft)))
967
(defunk make-node-size (vcnt fcnt) :inline (logior^ (*^ vcnt (vcnt-shft)) fcnt))
969
(defunk node.set-opcd (n szop) :inline (if (promoted n) (set-node-stor n szop ls$) (set-trans-stor (-^ n) szop ls$)))
970
(defunk node.opcd (n) :inline (logand^ (if (promoted n) (my-fixnum (get-node-stor n ls$)) (my-fixnum (get-trans-stor (-^ n) ls$))) (opcd-mask)))
971
(defunk node.size (n) :inline (floor^ (if (promoted n) (my-fixnum (get-node-stor n ls$)) (my-fixnum (get-trans-stor (-^ n) ls$))) (size-shft)))
973
(defunk node.in-ctx (n) :inline
974
(assert (promoted n) (=^ (logand^ (get-node-stor n ls$) (in-ctx-mask)) (in-ctx-mask))))
975
(defunk node.set-in-ctx (n in-ctx.) :inline
976
(assert (promoted n) (set-node-stor n (if in-ctx. (logior^ (get-node-stor n ls$) (in-ctx-mask))
977
(logand^ (get-node-stor n ls$) (in-ctx-flip))) ls$)))
979
(defunk node.user-mark (n) :inline
980
(=^ (logand^ (get-node-stor n ls$) (user-mark-mask)) (user-mark-mask)))
981
(defunk node.set-user-mark (n user-mark.) :inline
982
(set-node-stor n (if user-mark. (logior^ (get-node-stor n ls$) (user-mark-mask))
983
(logand^ (get-node-stor n ls$) (user-mark-flip))) ls$))
985
(defunk node.rep (n) :inline (if (promoted n) (my-fixnum (get-node-stor (1-^ n) ls$)) (node-btm)))
986
(defunk node.set-rep (n rep) :inline (assert (promoted n) (set-node-stor (1-^ n) rep ls$)))
988
(defunk node.dcv (n) :inline (assert (promoted n) (get-node-stor (-^ n 2) ls$)))
989
(defunk node.set-dcv (n dcv) :inline (assert (promoted n) (set-node-stor (-^ n 2) dcv ls$)))
991
; We include a "wrapper" for node.uniq which checks if the uniq-ptr retrieved
992
; is strictly less than the node id n passed in. This should be an invariant of
993
; the construction of nodes, but we add this "wrapper" to help in admitting
994
; various functions which traverse nodes. BOZO -- need to check if this affects
995
; performance appreciably and note here whether or not it does.
997
(defunk node.uniq (n) :inline (assert (promoted n) (letk ((uniq (get-node-stor (-^ n 3) ls$))) (check-<^ uniq n 'node.uniq))))
998
(defunk node.set-uniq (n uniq) :inline (assert (promoted n) (set-node-stor (-^ n 3) uniq ls$)))
1001
; Some special node ids. (node-btm) is a special node which denotes "no
1002
; value". NOTE -- it is important that 0 is not a legal node value (for
1003
; multiple reasons). So, actual node ids should always begin with node id 1.
1012
(defunk dctx-btm -1)
1013
(defunk dcv-empty 0)
1016
; NOTE -- While the preceding constants may look "symbolic", it is important
1017
; that these constants keep the value for which they are declared.
1019
(defunk opcd-quote (make-opcd 1 nil nil nil 1))
1020
(defunk opcd-if (make-opcd 3 nil t nil 2))
1021
(defunk opcd-equal (make-opcd 2 nil nil t 3))
1022
(defunk opcd-cons (make-opcd 2 nil nil nil 4))
1023
(defunk opcd-hide (make-opcd 1 nil nil nil 5))
1024
(defunk opcd-fail (make-opcd 1 nil nil nil 6))
1026
(defunk node-nil (1+ (base-node-alloc)))
1027
(defunk node-t (+ (node-nil) (base-node-alloc) 1))
1029
; We include a "wrapper" for node.arg which checks if the arg retrieved is
1030
; strictly less than the node id n passed in. This should be an invariant of
1031
; the construction of nodes, but we add this "wrapper" to help in admitting
1032
; various functions which traverse nodes. BOZO -- need to check if this affects
1033
; performance appreciably and note here whether or not it does.
1035
(defunk node.arg (n i) :inline
1036
(letk ((promoted. (promoted n))
1037
(alloc (if promoted. (base-node-alloc) (base-trans-alloc)))
1038
(n+ (if promoted. n (-^ n)))
1039
(ptr (-^ n+ (+^ alloc i)))
1041
(get-node-stor ptr ls$)
1042
(get-trans-stor ptr ls$))))
1043
(assert (or (temp-node n)
1044
(=^ (node.opcd n) (opcd-quote))
1047
(oper.name (opcd.index (node.opcd n)))
1048
(opcd.narg (node.opcd n))
1049
(opcd.is-var (node.opcd n))))
1052
(defunk node.set-arg (n i arg) :inline
1053
(letk ((promoted. (promoted n))
1054
(alloc (if promoted. (base-node-alloc) (base-trans-alloc)))
1055
(n+ (if promoted. n (-^ n)))
1056
(ptr (-^ n+ (+^ alloc i))))
1057
(assert (or (temp-node n)
1058
(=^ (node.opcd n) (opcd-quote))
1061
(oper.name (opcd.index (node.opcd n)))
1062
(opcd.narg (node.opcd n))
1063
(node-to-term arg)))
1065
(set-node-stor ptr arg ls$)
1066
(set-trans-stor ptr arg ls$)))))
1068
;; The function node-to-term is used to generate final results and to provide
1069
;; feedback in debugging. We generate an "illegal term" for (node-btm), but we
1070
;; want these to show up in the case this function is being used for
1071
;; debugging. We filter these "illegal terms" out when doing final result
1072
;; printing. This function may also be too "expensive" since it does not
1073
;; memoize the term structure created, but in this case, the user is in trouble
1074
;; already since the term which results will either be viewed by the user or
1075
;; used subsequently by ACL2 and as such, the ability to memoize common
1076
;; subterms would be irrelevant (although we could return a lambda expression
1077
;; and perhaps this is the more appropriate path to take).
1080
(defunk node-to-term1 (node ls$)
1081
(if (=^ node (node-btm)) :btm
1082
(letk ((opcd (node.opcd node))
1083
(op (opcd.index opcd)))
1084
(cond ((opcd.is-var opcd)
1086
((=^ opcd (opcd-quote))
1087
(list 'quote (qobj.obj (node.arg node 0))))
1089
(cons (oper.name op)
1090
(args-to-terms (opcd.narg opcd) 0 node ls$)))))))
1092
(defunk args-to-terms (n i node ls$)
1094
(cons (node-to-term1 (node.arg node i) ls$)
1095
(args-to-terms (1-^ n) (1+^ i) node ls$))))
1098
(defunk node-to-term (node) :inline (node-to-term1 node ls$))
1100
(defunk funcall (op. args.) :inline
1101
(ev-fncall-w op. args. (get-current-world ls$)
1102
nil ; user-stobj-alist (guess from Matt K. after v4-3)
1105
nil ; hard-error-returns-nilp
1108
(defmacro kern-error (err-string node rslt)
1109
`(prog2$ (kern-print-stats ls$)
1110
(prog2$ (cw " Final Term on Error: ~| ~p0 ~|~|" (kern-prune-node-term ,node))
1111
(prog2$ (er hard 'kernel-simplify ,err-string)
1114
(kern-comp) ;; compile to get macros compiled
1117
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
1118
#| functions defining a stats printing function |#
1119
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
1121
(defunk merge-histograms (x. y.)
1122
(cond ((endp x.) y.)
1124
((< (cadar x.) (cadar y.))
1126
(merge-histograms (cdr x.) y.)))
1128
(merge-histograms x. (cdr y.))))))
1130
(defunk split-histogram (x. y. n)
1131
(if (or (endp x.) (zp n)) (mv x. y.)
1132
(split-histogram (cdr x.) (cons (car x.) y.) (1-^ n))))
1134
(defunk sort-histogram (x.)
1135
(if (endp (cdr x.)) x.
1136
(letk ((y. z. (split-histogram x. () (floor^ (length x.) 2))))
1137
(merge-histograms (sort-histogram y.)
1138
(sort-histogram z.)))))
1140
(defunk get-rule-histogram (n r. ls$)
1143
(r. (if (>^ (rule.ctr n) 0)
1144
(cons (list (rule.rune n)
1148
(get-rule-histogram n r. ls$))))
1150
(defunk compute-rule-histogram () :inline
1151
(sort-histogram (get-rule-histogram (num-of-rule) () ls$)))
1153
(defunk get-rule-try-histogram (n r. ls$)
1156
(r. (if (>^ (rule.tryctr n) 0)
1157
(cons (list (rule.rune n)
1161
(get-rule-try-histogram n r. ls$))))
1163
(defunk compute-rule-try-histogram () :inline
1164
(sort-histogram (get-rule-try-histogram (num-of-rule) () ls$)))
1166
(defunk get-node-histogram (n r. ls$)
1169
(r. (if (>^ (oper.num-nodes n) 0)
1170
(cons (list (if (eq (oper.name n) 'quote)
1176
(get-node-histogram n r. ls$))))
1178
(defunk compute-node-histogram () :inline
1179
(sort-histogram (get-node-histogram (num-of-oper) () ls$)))
1181
(defunk get-trans-histogram (n r. ls$)
1184
(r. (if (>^ (oper.num-trans n) 0)
1185
(cons (list (if (eq (oper.name n) 'quote)
1191
(get-trans-histogram n r. ls$))))
1193
(defunk compute-trans-histogram () :inline
1194
(sort-histogram (get-trans-histogram (num-of-oper) () ls$)))
1196
(defunk histogram-to-ttree (histogram. ttree.)
1197
(if (endp histogram.) ttree.
1198
(histogram-to-ttree (cdr histogram.)
1199
(push-lemma (caar histogram.) ttree.))))
1201
(defunk print-loop-stack (n l r. ls$)
1202
(if (or (zp n) (zp l)) r.
1203
(print-loop-stack (1-^ n) (1-^ l)
1204
(cons (rule.rune (loop.rule l)) r.)
1207
(defunk compute-rule-stack () :inline
1208
(print-loop-stack 100 (1-^ (get-loop-stk-top ls$)) () ls$))
1211
(defunk prune-print-term1 (x. n)
1212
(cond ((atom x.) x.)
1213
((eq (first x.) 'quote) x.)
1216
(prune-print-args (rest x.) (1-^ n))))))
1218
(defunk prune-print-args (a. n)
1220
(cons (prune-print-term1 (first a.) n)
1221
(prune-print-args (rest a.) n))))
1225
(if (and (integerp n) (>= n 0) (< n (max-fixnum))) n 0))
1227
(defunk prune-node-term (x) :inline
1228
(prune-print-term1 (node-to-term x) (fixfix (get-initial-node-prune-depth ls$))))
1230
(defunk print-suffix-stack (n l r. ls$)
1231
(if (or (zp n) (zp l)) r.
1232
(print-suffix-stack (1-^ n) (1-^ l)
1233
(cons (list (rule.rune (loop.rule l))
1234
(prune-node-term (loop.node l)))
1238
(defunk compute-suffix-stack () :inline
1239
(print-suffix-stack 10 (1-^ (get-loop-stk-top ls$)) () ls$))
1241
(defunk print-stats (ls$)
1242
(letk ((rule-hist. (compute-rule-histogram))
1243
(try-hist. (compute-rule-try-histogram))
1244
(node-hist. (compute-node-histogram))
1245
(trans-hist. (compute-trans-histogram))
1246
(ttree. (histogram-to-ttree rule-hist. ()))
1247
(rule-stk. (compute-rule-stack))
1248
(stk-terms. (compute-suffix-stack))
1249
(num-promo (get-num-of-nodes ls$))
1250
(num-trans (get-num-trans-nodes ls$))
1251
(num-nodes (+^ num-promo num-trans)))
1252
(or (not (get-output-verbose ls$))
1253
(cw "--- KAS Num. Nodes: ~p0 ~|" num-nodes)
1254
(cw " Num. Promoted Nodes: ~p0 ~|" num-promo)
1255
(cw " Num. Current Temp. Nodes: ~p0 ~|" num-trans)
1256
(cw " Applied Rule Histogram: ~| ~p0 ~|~%" rule-hist.)
1257
(cw " Attempted Rule Histogram: ~| ~p0 ~|~%" try-hist.)
1258
(cw " Promoted Node Histogram: ~| ~p0 ~|~%" node-hist.)
1259
(cw " Temporary Node Histogram: ~| ~p0 ~|~%" trans-hist.)
1261
(cw " Pending Rule Stack (top 100): ~| ~p0 ~|~%" rule-stk.))
1263
(cw " Rule Stack With Terms (top 10): ~| ~p0 ~|~%" stk-terms.))
1267
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
1268
#| functions defining various hash codes used in the kernel |#
1269
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
1271
; The following macro defines the bound on the node indexes which are used
1272
; throughout the kernel code to efficiently encode terms. This bound is
1273
; necessary due to the requirements of the subsequent hashing function for
1274
; newly created nodes.
1276
(defunk hash-index-string (index mask string. acc)
1278
(letk ((index (1-^ index))
1279
(acc (logand^ mask (+^ acc (char-code (char string. index))))))
1280
(hash-index-string index mask string. acc))))
1282
(defunk hash-index-evg (evg. hash-mask)
1289
(* 17 (denominator evg.))))
1290
((acl2-numberp evg.)
1291
(+^ (hash-index-evg (realpart evg.) hash-mask)
1292
(hash-index-evg (imagpart evg.) hash-mask)))
1294
(+^ (floor^ hash-mask 4) (char-code evg.)))
1296
(*^ 19 (hash-index-evg (symbol-name evg.) hash-mask)))
1298
(hash-index-string (length evg.) hash-mask evg. (floor^ hash-mask 2)))
1300
(assert (consp evg.)
1301
(+^ (hash-index-evg (car evg.) hash-mask)
1302
(*^ 2 (hash-index-evg (cdr evg.) hash-mask))))))))
1304
;; modify the following number to adjust the various params used in allocating
1305
;; the kernel simplifier data structures.
1307
(defunk static-param (expt 2 12))
1308
(defunk op-hash-tbl-size (floor (static-param) 8))
1309
(defunk op-hash-tbl-mask (1- (op-hash-tbl-size)))
1311
(defunk fn-hash-code (name.) :inline
1312
(letk ((str. (symbol-name name.)))
1313
(hash-index-string (length str.) (op-hash-tbl-mask) str. 0)))
1315
(defunk mult-kern-mask (1- (expt 2 28)))
1316
(defunk add-kern-mask (1- (expt 2 58)))
1317
(defunk add-kern-mod 1021) ;; greatest prime < 1024
1319
(defunk hash-step (arg mask acc) :inline
1320
(logand^ (+^ (logand^ (*^ (logand^ acc (mult-kern-mask))
1321
(logand^ arg (mult-kern-mask)))
1323
(logand^ arg (add-kern-mask))
1324
(mod^ acc (add-kern-mod)))
1327
(defunk hash-args (n i acc mask x ls$)
1329
(hash-args (1-^ n) (1+^ i)
1330
(hash-step (node.arg x i) mask acc)
1333
(defunk hash-arg-list (args. acc mask ls$)
1334
(if (endp args.) acc
1335
(hash-arg-list (rest args.)
1336
(hash-step (first args.) mask acc)
1339
(defunk hash-node (node) :inline
1340
(letk ((opcd (node.opcd node))
1341
(narg (opcd.narg opcd))
1342
(mask (get-hash-mask ls$)))
1343
(hash-step opcd mask (hash-args narg 0 1 mask node ls$))))
1345
(defunk hash-signature (sig.) :inline
1346
(letk ((opcd (first sig.))
1348
(mask (get-hash-mask ls$)))
1349
(hash-step opcd mask (hash-arg-list args. 1 mask ls$))))
1352
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
1353
#| auxiliary functions supporting main kernel loop and user fn updates |#
1354
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
1356
(defunk lookup-opcd (op name. var. ls$)
1359
((and (equal name. (oper.name op))
1360
(eq var. (oper.is-var op)))
1361
(make-opcd (oper.narg op)
1366
(t (lookup-opcd (oper.uniq op) name. var. ls$))))
1368
(defunk find-fn-opcd (name.) :inline
1369
(letk ((op (get-op-hash (fn-hash-code name.) ls$)))
1370
(lookup-opcd op name. nil ls$)))
1372
(defunk find-var-opcd (name.) :inline
1373
(letk ((op (get-op-hash (fn-hash-code name.) ls$)))
1374
(lookup-opcd op name. t ls$)))
1376
(defunk oper-stor-incr (floor (static-param) 8))
1377
(defunk rule-stor-incr (floor (static-param) 8))
1379
(defunk alloc-rule-ndx (ls$)
1380
(letk ((ndx (get-next-rule-ndx ls$))
1381
(ls$ (ensure-rule ndx (rule-stor-incr)))
1382
(ls$ (set-next-rule-ndx (1+^ ndx) ls$)))
1385
(defunk arg-list= (n i x args. ls$)
1386
(cond ((zp n) (endp args.))
1388
((/=^ (node.arg x i) (first args.)) nil)
1389
(t (arg-list= (1-^ n) (1+^ i) x (rest args.) ls$))))
1391
(defunk args= (n i x y ls$)
1393
((/=^ (node.arg x i) (node.arg y i)) nil)
1394
(t (args= (1-^ n) (1+^ i) x y ls$))))
1396
(defunk node= (x y) :inline
1398
(and (not (and (promoted x) (promoted y)))
1399
(node=fn x y 0 0 nil ls$))))
1401
(defunk node=fn (x y n i args-p. ls$)
1404
(and (node= (node.arg x i) (node.arg y i))
1405
(node=fn x y (1-^ n) (1+^ i) t ls$)))
1406
(assert (and (/=^ x (node-btm))
1408
(letk ((opcd-x (node.opcd x))
1409
(opcd-y (node.opcd y)))
1410
(and (=^ opcd-x opcd-y)
1411
(letk ((narg (opcd.narg opcd-x)))
1412
(node=fn x y narg 0 t ls$)))))))
1414
(defunk find-uniq-sig (node opcd args. ls$)
1415
(cond ((zp node) (node-btm))
1416
((and (=^ (node.opcd node) opcd)
1417
(arg-list= (opcd.narg opcd) 0 node args. ls$))
1419
(t (find-uniq-sig (node.uniq node) opcd args. ls$))))
1421
(defunk find-uniq-node (node opcd x ls$)
1422
(cond ((zp node) (node-btm))
1423
((and (=^ (node.opcd node) opcd)
1424
(args= (opcd.narg opcd) 0 node x ls$))
1426
(t (find-uniq-node (node.uniq node) opcd x ls$))))
1428
(defunk copy-new-args (n y i x ls$)
1430
(letk ((ls$ (node.set-arg x i (node.arg y i))))
1431
(copy-new-args (1-^ n) y (1+^ i) x ls$))))
1433
(defunk add-size (x y) :inline
1434
(if (or (=^ x (size-btm))
1437
(letk ((fcnt (+^ (get-size-fcnt x)
1439
(vcnt (+^ (get-size-vcnt x)
1440
(get-size-vcnt y))))
1441
(if (not (and (<^ fcnt (max-fcnt-valu))
1442
(<^ vcnt (max-vcnt-valu))))
1444
(make-node-size vcnt fcnt)))))
1446
(defunk compute-args-size (i n x rslt ls$)
1448
(compute-args-size (1+^ i) (1-^ n) x
1449
(add-size (node.size (node.arg x i)) rslt)
1452
(defunk compute-node-size (size opcd narg x) :inline
1453
(cond ((/=^ size (size-btm)) size)
1454
((=^ opcd (opcd-quote)) (make-node-size 0 1))
1455
((opcd.is-var opcd) (make-node-size 1 0))
1456
((=^ narg 0) (make-node-size 0 1))
1457
(t (compute-args-size 0 narg x 0 ls$))))
1459
(defunk all-args-prom (x n i ls$)
1461
(and (promoted (node.arg x i))
1462
(all-args-prom x (1-^ n) (1+^ i) ls$))))
1464
(defunk args-promoted (x) :inline
1465
(all-args-prom x (opcd.narg (node.opcd x)) 0 ls$))
1467
(defmacro kern-record-temp-alloc ()
1468
(if (kern-enable-temp-recording)
1470
(letk ((ndx (opcd.index opcd))
1471
(num-trans (oper.num-trans ndx))
1472
(ls$ (oper.set-num-trans ndx (1+^ num-trans))))
1476
(defunk allocate-node (opcd size promote. ls$)
1477
(letk ((temp. (not promote.))
1478
(narg (opcd.narg opcd))
1479
(num-of-nodes (if temp. (get-num-trans-nodes ls$) (get-num-of-nodes ls$)))
1480
(alloc-nodes (if temp. (get-alloc-trans ls$) (get-alloc-nodes ls$)))
1481
(node-step (get-node-step ls$))
1482
(base-alloc (if temp. (base-trans-alloc) (base-node-alloc)))
1483
(min-alloc (+^ alloc-nodes narg base-alloc))
1484
(length (if temp. (length-trans-stor ls$) (length-node-stor ls$)))
1485
(ls$ (if (>=^ min-alloc length)
1486
(letk ((new-length (+^ min-alloc
1489
(if temp. (base-trans-alloc)
1490
(base-node-alloc)))))))
1491
(if temp. (resize-trans-stor new-length ls$)
1492
(resize-node-stor new-length ls$)))
1494
(node (1-^ min-alloc))
1496
(letk ((ls$ (set-alloc-trans min-alloc ls$))
1497
(ls$ (set-num-trans-nodes (1+^ num-of-nodes) ls$)))
1499
(letk ((ls$ (set-alloc-nodes min-alloc ls$))
1500
(ls$ (set-num-of-nodes (1+^ num-of-nodes) ls$)))
1502
(node (if temp. (-^ node) node))
1503
(ls$ (node.set-opcd node (logand^ (logand^ (logior^ opcd (*^ size (size-shft)))
1504
(in-ctx-flip)) ; clear the in-ctx bit on allocation
1505
(user-mark-flip)))) ; clear the user-mark bit on allocation
1506
(ls$ (record-temp-alloc)))
1509
(defunk complete-promoted-init (new chain hash opcd ls$)
1510
(letk ((ls$ (node.set-uniq new chain))
1511
(ls$ (node.set-rep new (node-btm)))
1512
(ls$ (node.set-dcv new (dcv-empty)))
1513
(ls$ (set-node-hash hash new ls$))
1514
(ndx (opcd.index opcd))
1515
(num-nodes (oper.num-nodes ndx))
1516
(ls$ (oper.set-num-nodes ndx (1+^ num-nodes))))
1519
(defunk make-arg-list (n i x ls$)
1521
(cons (node.arg x i)
1522
(make-arg-list (1-^ n) (1+^ i) x ls$))))
1524
(defunk signature-to-node (sig. ls$)
1525
(find-uniq-sig (get-node-hash (hash-signature sig.) ls$)
1526
(first sig.) (rest sig.) ls$))
1528
(defunk node-to-signature (node ls$)
1529
(letk ((opcd (node.opcd node))
1530
(narg (opcd.narg opcd)))
1531
(cons opcd (make-arg-list narg 0 node ls$))))
1533
(defunk install-node (x promote. ls$)
1534
(if (eq promote. (promoted x))
1536
(letk ((temp. (not promote.))
1537
(opcd (node.opcd x))
1538
(size (node.size x))
1539
(narg (opcd.narg opcd))
1540
(size (compute-node-size size opcd narg x))
1541
(hash (if temp. 0 (hash-node x)))
1542
(chain (if temp. 0 (get-node-hash hash ls$)))
1543
(node (if temp. (node-btm) (find-uniq-node chain opcd x ls$))))
1544
(assert (not (and temp. (opcd.is-var opcd)))
1545
(assert (or temp. (=^ opcd (opcd-quote)) (args-promoted x))
1546
(if (/=^ node (node-btm))
1548
(letk ((new ls$ (allocate-node opcd size promote. ls$))
1549
(ls$ (copy-new-args narg x 0 new ls$)))
1550
(if temp. (mv^ new ls$)
1551
(complete-promoted-init new chain hash opcd ls$)))))))))
1553
(defunk install-node-memo (opcd x hash ls$)
1554
(assert (args-promoted x)
1555
(letk ((narg (opcd.narg opcd))
1556
(size (node.size x))
1557
(size (compute-node-size size opcd narg x))
1558
(chain (get-node-hash hash ls$))
1559
(new ls$ (allocate-node opcd size t ls$))
1560
(ls$ (copy-new-args narg x 0 new ls$))
1561
(x ls$ (complete-promoted-init new chain hash opcd ls$)))
1564
(defunk quote-obj-incr (floor (static-param) 4))
1565
(defunk quote-hash-size (* (quote-obj-incr) 2))
1566
(defunk quote-hash-mask (1- (quote-hash-size)))
1568
(defunk find-quote-obj (ptr obj. ls$)
1569
(cond ((zp ptr) (qobj-btm))
1570
((equal (qobj.obj ptr) obj.) ptr)
1571
(t (find-quote-obj (qobj.uniq ptr) obj. ls$))))
1573
(defunk make-quote (obj. ls$)
1574
(letk ((hash (hash-index-evg obj. (quote-hash-mask)))
1575
(chain (get-quote-hash hash ls$))
1576
(qobj (find-quote-obj chain obj. ls$)))
1577
(if (/=^ qobj (qobj-btm))
1579
(letk ((x (get-next-quote ls$))
1580
(ls$ (ensure-qobj x (quote-obj-incr)))
1581
(ls$ (qobj.set-obj x obj.))
1582
(ls$ (qobj.set-uniq x chain))
1583
(ls$ (set-quote-hash hash x ls$))
1584
(ls$ (set-next-quote (1+^ x) ls$)))
1587
(defunk create-quote (obj.) :inline
1588
(letk ((v ls$ (make-quote obj. ls$))
1589
(x ls$ (allocate-node (opcd-quote) (size-btm) nil ls$))
1590
(ls$ (node.set-arg x 0 v)))
1591
(install-node x t ls$)))
1593
(defunk install-quote (obj. ls$)
1594
(cond ((eq obj. t) (mv^ (node-t) ls$))
1595
((eq obj. nil) (mv^ (node-nil) ls$))
1596
(t (create-quote obj.))))
1598
(defunk install-var-oper (name. ls$)
1599
(letk ((hash (fn-hash-code name.))
1600
(chain (get-op-hash hash ls$))
1601
(opcd (lookup-opcd chain name. t ls$))
1602
(ndx (if (/=^ opcd (opcd-btm))
1604
(get-next-op-ndx ls$)))
1605
(ls$ (if (/=^ opcd (opcd-btm))
1607
(letk ((ls$ (ensure-oper ndx (oper-stor-incr)))
1608
(ls$ (oper.set-uniq ndx chain))
1609
(ls$ (set-op-hash hash ndx ls$))
1610
(ls$ (set-next-op-ndx (1+^ ndx) ls$))
1611
(ls$ (oper.set-next-stk ndx (opcd-btm)))
1612
(ls$ (oper.set-bound ndx (node-btm))))
1614
(ls$ (oper.set-name ndx name.))
1615
(ls$ (oper.set-is-var ndx t))
1616
(ls$ (oper.set-rules ndx ()))
1617
(ls$ (oper.set-narg ndx 0))
1618
(ls$ (oper.set-num-nodes ndx 0))
1619
(ls$ (oper.set-num-trans ndx 0))
1620
(ls$ (oper.set-exec ndx (node-btm)))
1621
(ls$ (oper.set-boolp ndx nil))
1622
(ls$ (oper.set-assume-tbr ndx nil))
1623
(ls$ (oper.set-assume-fbr ndx nil))
1624
(ls$ (oper.set-is-if ndx nil))
1625
(ls$ (oper.set-is-equal ndx nil))
1626
(ls$ (oper.set-non-nil ndx nil)))
1629
(defunk get-var-opcode (name. ls$)
1630
(letk ((opcd (find-var-opcd name.)))
1631
(if (/=^ opcd (opcd-btm))
1633
(letk ((op ls$ (install-var-oper name. ls$)))
1634
(mv^ (make-opcd 0 t nil nil op) ls$)))))
1636
(defunk install-var (name. ls$)
1637
(letk ((opcd ls$ (get-var-opcode name. ls$))
1638
(x ls$ (allocate-node opcd (size-btm) nil ls$))
1639
(x ls$ (install-node x t ls$)))
1643
(defunk term-to-node (term. ls$)
1646
(assert (symbolp term.)
1647
(install-var term. ls$)))
1648
((eq (first term.) 'quote)
1649
(install-quote (second term.) ls$))
1650
((and (consp (first term.))
1651
(eq (first (first term.)) 'lambda))
1652
(mv^ (er0 hard 'term-to-node
1653
"should not encounter lambdas in mapping term to node")
1656
(letk ((opcd (find-fn-opcd (first term.)))
1657
(narg (opcd.narg opcd)))
1658
(if (or (=^ opcd (opcd-btm))
1659
(/=^ narg (length (rest term.))))
1660
(mv^ (er0 hard 'term-to-node
1661
"could not locate appropriate opcode for term ~x0 ~x1"
1664
(letk ((x ls$ (allocate-node opcd (size-btm) nil ls$))
1665
(ls$ (rest-to-args (rest term.) 0 x ls$)))
1666
(install-node x t ls$)))))))
1668
(defunk rest-to-args (args. i x ls$)
1669
(if (endp args.) ls$
1670
(letk ((arg ls$ (term-to-node (first args.) ls$))
1671
(ls$ (node.set-arg x i arg)))
1672
(rest-to-args (rest args.) (1+^ i) x ls$))))
1676
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
1677
#| functions implementing undo-stk and depth ctx (dctx) |#
1678
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
1681
(defunk undo-stk-increment 12286)
1682
(defunk undo-chains-increment 1048)
1684
(defunk dctx-max-rep (- (fixnum-size) 2))
1685
(defunk dcv-max-rep (1- (ash 1 (1+ (dctx-max-rep)))))
1687
(defunk alloc-undo-ptr (ls$)
1688
(letk ((free (get-undo-free-list ls$)))
1689
(if (/=^ free (undo-btm))
1690
(letk ((ls$ (set-undo-free-list (undo.chain free) ls$)))
1692
(letk ((top (get-undo-top ls$))
1693
(ls$ (ensure-undo top (undo-stk-increment)))
1694
(ls$ (set-undo-top (1+^ top) ls$)))
1697
(defunk memo-args= (x m n i ls$)
1699
(and (=^ (node.arg x i) (memo.arg m i))
1700
(memo-args= x m (1-^ n) (1+^ i) ls$))))
1702
(defunk find-max-dctx (dcv dcx)
1703
(cond ((zp dcx) (dctx-0))
1704
((/=^ (logand^ (ash^ 1 dcx) dcv) 0) dcx)
1705
(t (find-max-dctx dcv (1-^ dcx)))))
1707
(defunk max-in-dcv (dcv) :inline
1708
(if (=^ dcv (dcv-empty)) (dctx-0) (find-max-dctx dcv (dctx-max-rep))))
1710
(defunk create-new-undo (x dcv old-r old-d ls$)
1711
(if (=^ dcv (dcv-empty)) ls$
1712
(letk ((dcx (max-in-dcv dcv))
1713
(chain (get-undo-chains dcx ls$))
1714
(uptr ls$ (alloc-undo-ptr ls$))
1715
(ls$ (undo.set-node uptr x))
1716
(ls$ (undo.set-rep uptr old-r))
1717
(ls$ (undo.set-dcv uptr old-d))
1718
(ls$ (undo.set-chain uptr chain))
1719
(ls$ (set-undo-chains dcx uptr ls$)))
1722
(defunk create-update-rep (node new-r dcv ls$)
1723
(if (>=^ dcv (dcv-max-rep)) ls$
1724
(letk ((old-r (node.rep node))
1725
(old-d (node.dcv node))
1726
(ls$ (create-new-undo node dcv old-r old-d ls$))
1727
(ls$ (node.set-rep node new-r))
1728
(ls$ (node.set-dcv node dcv)))
1731
;; The following is the ratio from entries in the unique node hash-table and
1732
;; the memo-table. Since we reuse the hashing function, we have to divide down
1733
;; the hash address in order to get the memo table address.
1735
(defunk hash-memo-divisor 4)
1737
(defunk check-memos (x ls$)
1740
(letk ((opcd (node.opcd x))
1741
(narg (opcd.narg opcd)))
1742
(if (or (>^ narg (max-memo-narg))
1743
(not (args-promoted x)))
1745
(letk ((h (hash-node x))
1746
(node (find-uniq-node (get-node-hash h ls$) opcd x ls$)))
1747
(if (/=^ node (node-btm))
1749
(letk ((m (floor^ h (hash-memo-divisor)))
1750
(m-opcd (memo.opcd m))
1751
(match. (and (=^ opcd m-opcd)
1752
(or (<=^ narg (num-1memo-args))
1753
(=^ (memo.opcd (1+^ m))
1755
(memo-args= x m narg 0 ls$))))
1758
(letk ((node ls$ (install-node-memo opcd x h ls$))
1759
(ls$ (if (/=^ (node.rep node) (node-btm)) ls$
1760
(create-update-rep node (memo.rslt m) (memo.dcv m) ls$))))
1761
(mv^ node ls$))))))))))
1763
(defunk memo-copy-args (m x n i ls$)
1765
(letk ((ls$ (memo.set-arg m i (node.arg x i))))
1766
(memo-copy-args m x (1-^ n) (1+^ i) ls$))))
1768
(defunk create-memo-if-needed (x rep dcv ls$)
1769
(assert (and (temp-node x) (>^ rep 0))
1770
(letk ((opcd (node.opcd x))
1771
(narg (opcd.narg opcd)))
1772
(if (or (>^ narg (max-memo-narg))
1773
(not (args-promoted x))
1774
(>=^ dcv (dcv-max-rep)))
1776
(letk ((m (floor^ (hash-node x) (hash-memo-divisor)))
1777
(ls$ (memo.set-opcd m opcd))
1778
(ls$ (memo.set-rslt m rep))
1779
(ls$ (memo.set-dcv m dcv))
1780
(ls$ (memo-copy-args m x narg 0 ls$))
1781
(ls$ (if (<=^ narg (num-1memo-args)) ls$
1782
(memo.set-opcd (1+^ m) (opcd-memo-mrkr))))
1783
(ls$ (create-new-undo (-^ m) dcv (node-btm) (dcv-btm) ls$)))
1786
(defunk update-rep (node rep dcv id ls$)
1787
(declare (ignore id))
1788
(assert (or (and (>=^ dcv (dcv-btm))
1789
(/=^ node (node-btm))
1790
(/=^ (node.opcd node) (opcd-quote)))
1791
(list dcv node rep (node.opcd node)))
1792
(cond ((=^ rep (node-btm))
1793
(assert (promoted node)
1794
(node.set-rep node (node-btm))))
1796
(create-memo-if-needed node rep dcv ls$))
1799
(letk ((ls$ (node.set-rep node rep))
1800
(ls$ (node.set-dcv node (dcv-empty))))
1802
((=^ (node.rep node) rep) ls$)
1803
(t (create-update-rep node rep dcv ls$)))))
1805
(defunk pop-undo-stk-fn (uptr depth ls$)
1807
(prog2$ (er0 hard 'pop-undo-stk-fn
1808
"An internal error in the KAS algorithm has been detected. ~
1809
Please notify current maintainer of KAS")
1813
(letk ((node (undo.node uptr))
1814
(chain (undo.chain uptr))
1815
(ls$ (cond ((=^ node (node-btm))
1816
(letk ((dcv (undo.dcv uptr)))
1817
(if (=^ dcv (dcv-btm))
1818
(node.set-in-ctx (undo.rep uptr) nil)
1819
(set-curr-ctx-stk dcv (undo.rep uptr) ls$))))
1821
(letk ((ls$ (node.set-rep node (undo.rep uptr)))
1822
(ls$ (node.set-dcv node (undo.dcv uptr))))
1824
(t (memo.set-opcd (-^ node) (opcd-btm))))) ;; clear the memo
1825
(free (get-undo-free-list ls$))
1826
(ls$ (undo.set-chain uptr free))
1827
(ls$ (set-undo-free-list uptr ls$)))
1828
(pop-undo-stk-fn chain (1-^ depth) ls$)))))
1830
(defunk pop-undo-stk (dcx) :inline
1831
(letk ((undo (get-undo-chains dcx ls$))
1832
(ls$ (set-undo-chains dcx (undo-btm) ls$))
1833
(ls$ (pop-undo-stk-fn undo (1+^ (get-undo-top ls$)) ls$)))
1836
(defunk create-new-dctx (ls$)
1837
(letk ((dcx (get-current-dctx ls$))
1839
(ls$ (if (<=^ (ash^ 1 dcx) (dcv-max-rep)) ls$
1840
(prog2$ (and (not (get-warned-ctx-depth ls$))
1841
(cw "NOTE: context depth exceeded maximum ctx. limit. performance will be hindered."))
1842
(set-warned-ctx-depth t ls$))))
1843
(ls$ (if (<^ dcx (length-undo-chains ls$))
1846
(+^ dcx (undo-chains-increment)) ls$)))
1847
(ls$ (set-undo-chains dcx (node-btm) ls$))
1848
(ls$ (set-current-dctx dcx ls$)))
1851
(defunk restore-previous-state (dcx- dcx+ age ls$)
1852
(letk ((ls$ (pop-undo-stk dcx+))
1853
(ls$ (set-current-dctx dcx- ls$))
1854
(ls$ (set-current-age age ls$)))
1857
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
1858
#| heuristic for generating case splits implemented as a sieve |#
1859
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
1861
(defunk non-nilp (x) :inline
1863
(letk ((opcd (node.opcd x)))
1864
(or (and (/=^ x (node-nil))
1865
(=^ opcd (opcd-quote)))
1866
(oper.non-nil (opcd.index opcd))))))
1868
(defunk is-boolp (x) :inline
1871
(oper.boolp (opcd.index (node.opcd x)))))
1873
;; The following is the user stobj which can be used to store whatever
1874
;; data the user wants to maintain during the simplification process.
1876
(dynamic-user-state-obj :object)
1877
(candidate-stor :fixnum-array)
1878
(candidate-hash :fixnum-array)
1879
(candidate-mask :fixnum)
1880
(candidate-step :fixnum)
1881
(next-candidate :fixnum)
1882
(candidate-stk :fixnum-array)
1883
(candidate-top :fixnum)
1887
(define-user-record-array candidate
1888
(:fixnum candidate-stor (node weight tst chain)))
1890
(defunk candidate-tbl-init (sp) (floor (expt 2 sp) 64))
1891
(defunk candidate-tbl-step (sp) (candidate-tbl-init sp))
1892
(defunk candidate-hash-size (sp) (* (candidate-tbl-init sp) 2))
1893
(defunk candidate-hash-mask (sp) (- (candidate-hash-size sp) 1))
1895
(defunk init-candidate-hash (n us$)
1898
(us$ (set-candidate-hash n (node-btm) us$)))
1899
(init-candidate-hash n us$))))
1901
(defunk user-init (ls$ us$)
1902
(letk ((sp (get-kern-size-param ls$))
1903
(us$ (set-opcd-bv (opcd-btm) us$))
1904
(us$ (set-dynamic-user-state-obj nil us$))
1905
(us$ (resize-candidate-hash (candidate-hash-size sp) us$))
1906
(us$ (init-candidate-hash (candidate-hash-size sp) us$))
1907
(us$ (set-candidate-mask (candidate-hash-mask sp) us$))
1908
(us$ (ensure-candidate (candidate-tbl-init sp) 0))
1909
(us$ (set-candidate-step (candidate-tbl-step sp) us$))
1910
(us$ (set-next-candidate (1+^ (node-btm)) us$))
1911
(us$ (resize-candidate-stk (candidate-hash-size sp) us$))
1912
(us$ (set-candidate-top 0 us$)))
1915
; We implement a heuristic for introducing case-splits. The basic idea is to
1916
; case-split on the most frequently referenced term which appears in the test
1917
; of an if (or is equated in the test of an if).
1919
; 1. Introduce entry for each candidate node
1920
; 2. Weighted count of all references to candidate nodes
1921
; 3. determination of heaviest candidate in weighting
1922
; -- and clear the hash-table at the same time.
1924
(defunk hash-candidate (node) :inline
1925
(logand^ node (get-candidate-mask us$)))
1927
(defunk find-candidate-in-chain (cand node us$)
1928
(cond ((zp cand) (node-btm))
1929
((=^ (candidate.node cand) node) cand)
1930
(t (find-candidate-in-chain (candidate.chain cand) node us$))))
1932
(defunk add-candidate-node (node tst us$)
1933
(letk ((hash (hash-candidate node))
1934
(chain (get-candidate-hash hash us$))
1935
(cand (find-candidate-in-chain chain node us$)))
1936
(if (/=^ cand (node-btm)) us$
1937
(letk ((cand (get-next-candidate us$))
1938
(us$ (ensure-candidate cand (get-candidate-step us$)))
1939
(us$ (candidate.set-node cand node))
1940
(us$ (candidate.set-weight cand 0))
1941
(us$ (candidate.set-tst cand tst))
1942
(us$ (candidate.set-chain cand chain))
1943
(us$ (set-candidate-hash hash cand us$))
1944
(us$ (set-next-candidate (1+^ cand) us$)))
1945
(if (/=^ chain (node-btm)) us$
1946
(letk ((top (get-candidate-top us$))
1947
(us$ (set-candidate-stk top hash us$))
1948
(us$ (set-candidate-top (1+^ top) us$)))
1952
(defunk if-subterm (x ls$)
1953
(letk ((opcd (node.opcd x)))
1955
((=^ opcd (opcd-quote)) nil)
1956
((opcd.is-var opcd) nil)
1957
((opcd.is-if opcd) t)
1958
(t (if-subterm-args (opcd.narg opcd) 0 x ls$)))))
1960
(defunk if-subterm-args (n i x ls$)
1962
(or (if-subterm (node.arg x i) ls$)
1963
(if-subterm-args (1-^ n) (1+^ i) x ls$))))
1966
(defunk add-candidate-nodes (opcd x ls$ us$)
1967
(if (not (opcd.is-if opcd)) us$
1968
(letk ((tst (node.arg x 0)))
1969
(if (or (not (is-boolp tst)) (if-subterm tst ls$)) us$
1970
(letk ((us$ (add-candidate-node tst tst us$)))
1971
(if (/=^ (node.opcd tst) (opcd-equal)) us$
1972
(add-candidate-node (node.arg tst 0) tst us$)))))))
1975
(defunk add-candidates-for-node (x ls$ us$)
1976
(letk ((opcd (node.opcd x)))
1977
(if (or (=^ opcd (opcd-quote)) (opcd.is-var opcd)) us$
1978
(letk ((us$ (add-candidate-nodes opcd x ls$ us$)))
1979
(add-candidates-for-args (opcd.narg opcd) 0 x ls$ us$)))))
1981
(defunk add-candidates-for-args (n i x ls$ us$)
1983
(letk ((us$ (add-candidates-for-node (node.arg x i) ls$ us$)))
1984
(add-candidates-for-args (1-^ n) (1+^ i) x ls$ us$))))
1987
(defunk case-split-candidates (x ls$ us$)
1988
(letk ((opcd (node.opcd x)))
1990
((or (=^ opcd (opcd-quote))
1993
((and (opcd.is-if opcd)
1994
(not (if-subterm (node.arg x 0) ls$)))
1995
(letk ((us$ (case-split-candidates (node.arg x 1) ls$ us$)))
1996
(case-split-candidates (node.arg x 2) ls$ us$)))
1997
((=^ (opcd.narg opcd) 1)
1998
(case-split-candidates (node.arg x 0) ls$ us$))
2000
(add-candidates-for-node x ls$ us$)))))
2003
;; An upper bound on the weight for any candidate. We use this as
2004
;; a cap on nodes which may get too much weight due to reconvergent
2005
;; nodes (in those cases, we are probably already in trouble), and
2006
;; we need a mechanism to ensure that we maintain fixnums.
2007
(defunk max-candidate-weight (expt 2 20))
2009
(defunk adjust-candidate-weight (x weight us$)
2010
(letk ((hash (hash-candidate x))
2011
(chain (get-candidate-hash hash us$))
2012
(cand (find-candidate-in-chain chain x us$)))
2013
(if (=^ cand (node-btm)) us$
2014
(letk ((curr (candidate.weight cand))
2015
(new (if (and (<^ curr (max-candidate-weight))
2016
(<^ weight (max-candidate-weight))
2017
(<^ (+^ curr weight) (max-candidate-weight)))
2019
(max-candidate-weight)))
2020
(us$ (candidate.set-weight cand new)))
2023
(defunk decrement-weight (weight decr) :inline
2024
(if (>^ weight decr) (-^ weight decr) 1))
2027
(defunk weigh-case-splits (x weight ls$ us$)
2028
(letk ((opcd (node.opcd x)))
2030
((or (=^ opcd (opcd-quote))
2034
(letk ((br-w (decrement-weight weight 2))
2035
(us$ (weigh-case-splits (node.arg x 1) br-w ls$ us$))
2036
(us$ (weigh-case-splits (node.arg x 2) br-w ls$ us$)))
2037
(weigh-case-splits (node.arg x 0) (decrement-weight weight 1) ls$ us$)))
2039
(letk ((us$ (adjust-candidate-weight x weight us$)))
2040
(weigh-case-split-args (opcd.narg opcd) 0 x weight ls$ us$))))))
2042
(defunk weigh-case-split-args (n i x w ls$ us$)
2044
(letk ((us$ (weigh-case-splits (node.arg x i) w ls$ us$)))
2045
(weigh-case-split-args (1-^ n) (1+^ i) x w ls$ us$))))
2048
(defunk find-better-candidate (cand max us$)
2049
(cond ((zp cand) max)
2050
((=^ max (node-btm)) cand)
2051
((>^ (candidate.weight cand) (candidate.weight max))
2052
(find-better-candidate (candidate.chain cand) cand us$))
2053
(t (find-better-candidate (candidate.chain cand) max us$))))
2055
(defunk find-and-clear-split (ptr max us$)
2056
(if (zp ptr) (mv^ max us$)
2057
(letk ((ptr (1-^ ptr))
2058
(hash (get-candidate-stk ptr us$))
2059
(cand (get-candidate-hash hash us$))
2060
(max (find-better-candidate cand max us$))
2061
(us$ (set-candidate-hash hash (node-btm) us$)))
2062
(find-and-clear-split ptr max us$))))
2064
(defunk determine-case-split (us$)
2065
(letk ((top (get-candidate-top us$))
2066
(cand us$ (find-and-clear-split top (node-btm) us$)))
2067
(if (=^ cand (node-btm))
2068
(mv^ (node-btm) us$)
2069
(letk ((split (candidate.tst cand))
2070
(us$ (set-candidate-top 0 us$))
2071
(us$ (set-next-candidate (1+^ (node-btm)) us$)))
2074
(defunk valid-case-split (x) :inline
2075
(and (/=^ x (node-btm))
2077
(letk ((opcd (node.opcd x)))
2078
(and (/=^ opcd (opcd-quote))
2079
(not (opcd.is-var opcd))))))
2081
;; initial weight which is distributed differently through if args
2082
;; and added to the weights accumulating in the candidate table.
2083
(defunk initial-case-split-weight 32)
2085
(defunk generate-case-split (sieve. x ls$ us$)
2086
(letk ((n (second sieve.))
2087
(opcd (node.opcd n)))
2088
(if (not (opcd.is-var opcd))
2090
(letk ((var (opcd.index opcd))
2091
(us$ (case-split-candidates x ls$ us$))
2092
(us$ (weigh-case-splits x (initial-case-split-weight) ls$ us$))
2093
(split us$ (determine-case-split us$)))
2094
(mv (and (valid-case-split split)
2095
(list (list :set-var-bound var
2096
(node-to-signature split ls$))))
2099
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
2100
#| user function stobj (us$) and user function call |#
2101
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
2103
; The user-fn responds with an answer and a list of "update"s to the kernel
2104
; logic state stobj ls$. The reason we use this interface is to restrict (in a
2105
; clear logical sense) what "effects" the user-fn can have on ls$ (which stores
2106
; all of the information relevant to the soundness of the kernel
2107
; simplifier). The following updates are currently supported/allowed:
2109
; (:set-var-bound <var> <node>) <var> is nfix index, <node> is nfix index
2110
; (:set-rule-sieves <rule> <sieves>)
2111
; (:set-rule-enabled <rule> <flag>) <rule> is nfix index, <flag> is boolean
2112
; (:set-rule-always <rule> <flag>) <rule> is nfix index, <flag> is boolean
2113
; (:set-rule-ctr <rule> <ctr>)
2114
; (:set-node-step <step>) <step> is nfix
2115
; (:set-node-limit <limit>) <limit> is nfix
2116
; (:change-rule-order <rule> <pos>) <rule> is nfix index, <pos> is natural
2117
; (:set-rule-traced <rule> <mark>)
2118
; (:set-user-mark <node> <mark>)
2120
;;;; nfix is a natural fixnum
2122
; The function process-update does not place any assumptions on the
2123
; update structure from the user-fn, so some checks are required.
2125
(defunk first-oper-ndx 1)
2126
(defunk first-rule-ndx 1)
2128
(defunk drop-rule (rules. ndx)
2129
(cond ((endp rules.) ())
2130
((=^ (car rules.) ndx) (cdr rules.))
2131
(t (cons (car rules.)
2132
(drop-rule (cdr rules.) ndx)))))
2134
(defunk place-rule (rules. ndx pos)
2135
(if (or (zp pos) (endp rules.))
2138
(place-rule (cdr rules.) ndx (1-^ pos)))))
2140
(defunk move-rule (rules. ndx pos)
2141
(place-rule (drop-rule rules. ndx) ndx pos))
2143
(defunk is-legal-rule (rule. ls$)
2144
(and (fixnump rule.)
2145
(>=^ rule. (first-rule-ndx))
2146
(<^ rule. (get-next-rule-ndx ls$))))
2148
(defunk is-legal-oper (op. ls$)
2150
(>=^ op. (first-oper-ndx))
2151
(<^ op. (get-next-op-ndx ls$))))
2153
(defunk is-legal-sig-args (sig.)
2156
(fixnump (first sig.))
2157
(is-legal-sig-args (rest sig.)))))
2159
(defunk is-legal-sig (sig.)
2161
(fixnump (first sig.))
2162
(is-legal-sig-args (rest sig.))))
2164
(defunk legal-sieves (sieves.)
2166
(and (consp sieves.)
2167
(consp (first sieves.))
2168
(keywordp (first (first sieves.)))
2169
(true-listp (rest (first sieves.)))
2170
(legal-sieves (rest sieves.)))))
2172
(defunk install-arg-as-node (arg. ls$)
2173
(if (termp arg. (get-current-world ls$))
2174
(term-to-node arg. ls$)
2175
(term-to-node (list 'quote arg.) ls$)))
2177
(defunk install-sieve-args (args. ls$)
2180
(letk ((node ls$ (install-arg-as-node (first args.) ls$))
2181
(rst. ls$ (install-sieve-args (rest args.) ls$)))
2182
(mv (cons node rst.) ls$))))
2184
(defunk install-sieves (sieves. ls$)
2187
(letk ((args. ls$ (install-sieve-args (rest (first sieves.)) ls$))
2188
(rst. ls$ (install-sieves (rest sieves.) ls$)))
2189
(mv (acons (first (first sieves.)) args. rst.) ls$))))
2191
(defunk er-process-update-arg (msg.) :inline
2192
(er hard 'process-update
2193
"ill-formed user-fn update. message: ~x0 update: ~x1"
2196
(defunk er-process-update (msg.) :inline
2197
(prog2$ (er-process-update-arg msg.) ls$))
2199
(defunk pu-bool (x.) :inline
2200
(if (is-boolean x.) x. (er-process-update-arg "expected boolean value")))
2202
(defunk pu-nat (x. lo. hi.) :inline
2203
(if (and (fixnump x.)
2204
(or (null lo.) (>= x. lo.))
2205
(or (null hi.) (<= x. hi.)))
2207
(er-process-update-arg "expected natural number")))
2209
(defunk find-rule-id (rules. rune. ls$)
2210
(cond ((endp rules.) nil)
2211
((equal (rule.rune (first rules.)) rune.)
2213
(t (find-rule-id (rest rules.) rune. ls$))))
2215
(defunk pu-rule (x.) :inline
2216
(if (is-legal-rule x. ls$) x.
2218
(er-process-update-arg "expected legal rule or rune")
2219
(letk ((op. (car x.))
2221
(opcd (find-fn-opcd op.)))
2222
(if (=^ opcd (opcd-btm))
2223
(er-process-update-arg "could not find rune base op.")
2224
(letk ((rule. (find-rule-id (oper.rules op.) rune. ls$)))
2226
(er-process-update-arg "could not find rule for rune")
2229
(defunk pu-free-var (x.) :inline
2230
(if (not (is-legal-oper x. ls$))
2231
(er-process-update-arg "expected legal free var. name")
2232
(if (/=^ (oper.bound x.) (node-btm))
2233
(er-process-update-arg "expected free var. to be unbound")
2236
(defunk pu-signature-node (x.) :inline
2237
(if (not (is-legal-sig x.))
2238
(er-process-update-arg "expected legal node signature")
2239
(letk ((n. (signature-to-node x. ls$)))
2240
(if (= n. (node-btm))
2241
(er-process-update-arg "expected signature to define existing promoted node")
2244
(defunk pu-sieves (x.) :inline
2245
(if (legal-sieves x.) x.
2246
(er-process-update-arg "expected well-formed list of sieves")))
2248
(defunk pu-trace-mark (x.) :inline
2249
(if (is-trace-mark x.) x.
2250
(er-process-update-arg "expected t/nil, :all, or symbol-list for trace mark")))
2252
(defunk set-var-bound (var node) :inline
2253
(letk ((ls$ (oper.set-bound var node))
2254
(ls$ (oper.set-next-stk var (get-var-chg-stk ls$)))
2255
(ls$ (set-var-chg-stk var ls$)))
2258
(defunk process-update (upd. ls$)
2259
(if (not (true-listp upd.))
2260
(er-process-update "expected update to be a true list")
2261
(letk ((cmd. (first upd.))
2266
(set-var-bound (pu-free-var a1.) (pu-signature-node a2.)))
2268
(letk ((sieves. ls$ (install-sieves (pu-sieves a2.) ls$)))
2269
(rule.set-sieves (pu-rule a1.) sieves.)))
2271
(rule.set-enabled (pu-rule a1.) (pu-bool a2.)))
2273
(rule.set-ctr (pu-rule a1.) (pu-nat a2. 0 nil)))
2275
(set-node-step (pu-nat a1. 1 (maximum-array-size)) ls$))
2277
(set-node-limit (pu-nat a1. 1 (maximum-array-size)) ls$))
2279
(letk ((rule (pu-rule a1.))
2281
(pos. (pu-nat a2. 0 nil)))
2282
(oper.set-rules op (move-rule (oper.rules op) rule pos.))))
2284
(rule.set-traced (pu-rule a1.) (pu-trace-mark a2.)))
2286
(node.set-user-mark (pu-signature-node a1.) (pu-bool a2.)))
2287
(t (er-process-update "illegal command encountered in update"))))))
2289
(defunk process-updates (updates. ls$)
2290
(if (atom updates.) ls$
2291
(letk ((ls$ (process-update (first updates.) ls$)))
2292
(process-updates (rest updates.) ls$))))
2294
(defunk maximum-p-fn-count (1- (expt 2 19)))
2297
(defunk node-aux-cnt (x typ. ls$)
2298
(letk ((opcd (node.opcd x)))
2299
(cond ((=^ opcd (opcd-quote))
2300
(if (not (eq typ. :quote-fns)) 0
2301
(mask^ (fn-count-evg (qobj.obj (node.arg x 0)))
2302
(maximum-p-fn-count))))
2303
((opcd.is-var opcd) (if (eq typ. :vars) 1 0))
2304
(t (+^ (if (eq typ. :fns) 1 0)
2305
(args-aux-cnt x (opcd.narg opcd) 0 typ. 0 ls$))))))
2307
(defunk args-aux-cnt (x n i typ. r ls$)
2309
(letk ((r (+^ r (node-aux-cnt (node.arg x i) typ. ls$))))
2310
(args-aux-cnt x (1-^ n) (1+^ i) typ. r ls$))))
2313
(defunk node-var-cnt (x) :inline
2314
(node-aux-cnt x :vars ls$))
2316
(defunk node-fn-cnt (x) :inline
2317
(node-aux-cnt x :fns ls$))
2319
(defunk node-q-fn-cnt (x) :inline
2320
(node-aux-cnt x :quote-fns ls$))
2323
(defunk lex-order (x y ls$)
2324
(letk ((opcd-x (node.opcd x))
2325
(opcd-y (node.opcd y)))
2326
(or (<^ opcd-x opcd-y)
2327
(and (=^ opcd-x opcd-y)
2328
(if (=^ opcd-x (opcd-quote))
2329
(letk ((x-o. (qobj.obj (node.arg x 0)))
2330
(y-o. (qobj.obj (node.arg y 0))))
2331
(and (not (equal x-o. y-o.))
2332
(lexorder x-o. y-o.)))
2333
(args-order (opcd.narg opcd-x) 0 x y ls$))))))
2335
(defunk args-order (n i x y ls$)
2337
((lex-order (node.arg x i) (node.arg y i) ls$) t)
2338
((not (node= (node.arg x i) (node.arg y i))) nil)
2339
(t (args-order (1-^ n) (1+^ i) x y ls$))))
2342
(defunk term-order (x y ls$)
2343
(and (/=^ x (node-btm))
2345
(letk ((x-size (node.size x))
2346
(y-size (node.size y)))
2347
(if (and (/=^ x-size (size-btm))
2348
(/=^ y-size (size-btm))
2349
(/=^ x-size y-size))
2351
(letk ((x-cnt (node-var-cnt x))
2352
(y-cnt (node-var-cnt y)))
2353
(or (<^ x-cnt y-cnt)
2354
(and (=^ x-cnt y-cnt)
2355
(letk ((x-cnt (node-fn-cnt x))
2356
(y-cnt (node-fn-cnt y)))
2357
(or (<^ x-cnt y-cnt)
2358
(and (=^ x-cnt y-cnt)
2359
(letk ((x-cnt (node-q-fn-cnt x))
2360
(y-cnt (node-q-fn-cnt y)))
2361
(or (<^ x-cnt y-cnt)
2362
(and (=^ x-cnt y-cnt)
2363
(lex-order x y ls$))))))))))))))
2365
(defunk bdd< (x y op-bv) :inline
2366
(and (/=^ x (node-btm))
2368
(letk ((op-x (node.opcd x)))
2369
(and (=^ op-x op-bv)
2370
(letk ((op-y (node.opcd y)))
2371
(cond ((=^ op-y op-bv)
2374
(letk ((y (node.arg y 0))
2375
(op-y (node.opcd y)))
2376
(and (=^ op-y op-bv)
2380
(defunk bdd-order-p (x y ls$ us$)
2381
(letk ((op-bv1 (get-opcd-bv us$))
2382
(op-bv2 (if (=^ op-bv1 (opcd-btm)) (find-fn-opcd 'bv) op-bv1)))
2383
(if (=^ op-bv2 (opcd-btm))
2384
(mv (er hard 'bdd-order-p "could not locate opcd for operator bv") us$)
2385
(letk ((us$ (if (=^ op-bv1 (opcd-btm)) (set-opcd-bv op-bv2 us$) us$)))
2386
(mv (bdd< x y op-bv2) us$)))))
2388
(defunk bound-node (x) :inline
2389
(letk ((opcd (node.opcd x)))
2390
(if (opcd.is-var opcd)
2391
(oper.bound (opcd.index opcd))
2394
(defunk create-sieve-arg (x ls$)
2395
(letk ((rep (node.rep x))
2396
(bound (bound-node x)))
2397
(cond ((/=^ bound (node-btm)) (node-to-term bound))
2398
((>^ rep 0) (node-to-term rep))
2399
(t (node-to-term x)))))
2401
(defunk create-sieve-args (args. ls$)
2403
(cons (create-sieve-arg (first args.) ls$)
2404
(create-sieve-args (rest args.) ls$))))
2406
(defunk process-fast-sieve (sieve.) :inline
2407
(case (first sieve.)
2408
(:quotep (=^ (node.opcd (bound-node (second sieve.)))
2410
(:non-nilp (non-nilp (bound-node (second sieve.))))
2411
(:boolp (is-boolp (bound-node (second sieve.))))
2412
(:termordp (term-order (bound-node (second sieve.))
2413
(bound-node (third sieve.))
2415
(:nodeordp (node< (bound-node (second sieve.))
2416
(bound-node (third sieve.))))
2419
(defunk process-slow-sieve (sieve. x ls$ us$)
2420
(case (first sieve.)
2421
(:bddordp (bdd-order-p (bound-node (second sieve.))
2422
(bound-node (third sieve.))
2424
(:case-split (generate-case-split sieve. x ls$ us$))
2427
(defunk process-user-sieve (sieve. r ls$ us$)
2428
(if (not (eq (first sieve.) :funcall))
2430
(letk ((rune. (rule.rune r))
2431
(args. (create-sieve-args (rest sieve.) ls$)))
2432
(if (not (and (consp (first args.))
2433
(eq (first (first args.)) 'quote)
2434
(symbolp (second (first args.)))))
2435
(mv (er hard 'process-sieve
2436
"In applying ~x0: first argument to :funcall sieve should be quoted name of function: ~x1"
2437
rune. (first args.))
2439
(letk ((op. (second (first args.)))
2440
(args. (rest args.))
2441
(st. (get-dynamic-user-state-obj us$))
2442
(wrld. (get-current-world ls$))
2443
(erp. val. (funcall op. (list args. st. wrld.))))
2445
(mv (er hard 'process-sieve
2446
"In applying ~x0: encountered error in evaluating sieve: ~x1"
2453
(= (length val.) 3))
2454
(letk ((us$ (set-dynamic-user-state-obj (third val.) us$)))
2455
(mv (first val.) (second val.) us$)))
2457
(mv (er hard 'process-sieve
2458
"In applying ~x0: expected result from ~x1 must either be boolean or a triple"
2462
(defunk process-sieve (sieve. x r ls$ us$)
2463
(letk ((rslt. (process-fast-sieve sieve.)))
2464
(if (is-boolean rslt.) (mv rslt. () us$)
2465
(letk ((upds. us$ (process-slow-sieve sieve. x ls$ us$)))
2466
(if upds. (mv t (and (consp upds.) upds.) us$)
2467
(process-user-sieve sieve. r ls$ us$))))))
2469
(defunk process-each-sieve (sieves. x r ls$ us$)
2472
(letk ((ok. upds. us$ (process-sieve (first sieves.) x r ls$ us$))
2473
(ls$ (process-updates upds. ls$)))
2476
(process-each-sieve (rest sieves.) x r ls$ us$)))))
2478
(defunk process-sieves (x r) :inline
2479
(process-each-sieve (rule.sieves r) x r ls$ us$))
2482
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
2483
#| kernel unification and rewrite rule application functions |#
2484
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
2486
(defunk pop-var-chg-stk-fn (stk ls$)
2487
(if (=^ stk (opcd-btm))
2488
(set-var-chg-stk (opcd-btm) ls$)
2489
(letk ((nxt (oper.next-stk stk))
2490
(ls$ (oper.set-bound stk (node-btm))))
2491
(pop-var-chg-stk-fn nxt ls$))))
2493
(defunk pop-var-chg-stk () :inline
2494
(letk ((stk (get-var-chg-stk ls$)))
2495
(if (=^ stk (opcd-btm)) ls$
2496
(pop-var-chg-stk-fn stk ls$))))
2498
(defunk trace-rule-app (traced. rune. x) :inline
2499
(if (not traced.) ls$
2500
(prog2$ (cw ">>>~p0~%" rune.)
2501
(if (eq traced. t) ls$
2502
(prog2$ (cw "~p0~%" (prune-node-term x)) ls$)))))
2505
(defunk subst-node (y ls$)
2506
(assert (/=^ y (node-btm))
2507
(letk ((opcd-y (node.opcd y)))
2509
((=^ opcd-y (opcd-quote))
2511
((opcd.is-var opcd-y)
2512
(letk ((node (oper.bound (opcd.index opcd-y)))
2513
(node (if (=^ node (node-btm)) y node)))
2514
(assert (or (promoted node)
2515
(list y node (node-to-term y) (node-to-term node)))
2518
(letk ((x ls$ (allocate-node opcd-y (size-btm) nil ls$))
2519
(ls$ (subst-args (opcd.narg opcd-y) y 0 x ls$)))
2522
(defunk subst-args (narg y i x ls$)
2524
(letk ((a ls$ (subst-node (node.arg y i) ls$))
2525
(ls$ (node.set-arg x i a)))
2526
(subst-args (1-^ narg) y (1+^ i) x ls$))))
2529
(defunk 1way-unify-var (x opcd-y ls$)
2530
(letk ((op-y (opcd.index opcd-y))
2531
(bound (oper.bound op-y)))
2532
(if (=^ bound (node-btm))
2533
(letk ((ls$ (set-var-bound op-y x))) (mv t ls$))
2534
(mv (node= bound x) ls$))))
2536
(defunk 1way-unify-obj (x. opcd-y y ls$)
2538
((=^ opcd-y (opcd-cons))
2539
(if (atom x.) (mv nil ls$)
2540
(letk ((y0 (node.arg y 0))
2542
(op0 (node.opcd y0))
2543
(op1 (node.opcd y1))
2544
(match. ls$ (1way-unify-obj (car x.) op0 y0 ls$)))
2545
(if (not match.) (mv nil ls$)
2546
(1way-unify-obj (cdr x.) op1 y1 ls$)))))
2547
((opcd.is-var opcd-y)
2548
(letk ((x ls$ (create-quote x.)))
2549
(1way-unify-var x opcd-y ls$)))
2552
; The following function performs one-way unification of x with y (i.e. match x
2553
; with y where all variables in x are treated as ground).
2555
(defunk 1way-unify (x y n i args-p. ls$)
2557
(if (zp n) (mv t ls$)
2558
(letk ((match. ls$ (1way-unify (node.arg x i)
2561
(if (not match.) (mv nil ls$)
2562
(1way-unify x y (1-^ n) (1+^ i) t ls$))))
2563
(assert (and (/=^ x (node-btm)) (/=^ y (node-btm)))
2564
(letk ((opcd-y (node.opcd y))
2565
(opcd-x (node.opcd x)))
2567
((opcd.is-var opcd-y)
2568
(1way-unify-var x opcd-y ls$))
2569
((=^ opcd-y (opcd-quote))
2571
((=^ opcd-x (opcd-quote))
2572
(1way-unify-obj (qobj.obj (node.arg x 0)) opcd-y y ls$))
2573
((/=^ opcd-x opcd-y)
2576
(1way-unify x y (opcd.narg opcd-x) 0 t ls$)))))))
2578
(defunk unify-args (x y narg) :inline
2579
(1way-unify x y narg 0 t ls$))
2581
(defunk maximum-rule-ctr (- (expt 2 28) 2))
2583
(defunk incr-rule-ctr (r) :inline
2584
(letk ((ctr (rule.ctr r))
2585
(ctr (if (<^ ctr (maximum-rule-ctr)) (1+^ ctr) ctr)))
2586
(rule.set-ctr r ctr)))
2588
(defunk incr-rule-tryctr (r) :inline
2589
(letk ((ctr (rule.tryctr r))
2590
(ctr (if (<^ ctr (maximum-rule-ctr)) (1+^ ctr) ctr)))
2591
(rule.set-tryctr r ctr)))
2593
(defunk loop-stk-incr () (floor (static-param) 8))
2595
(defunk push-loop-stack (r x ls$)
2596
(letk ((l (get-loop-stk-top ls$))
2597
(ls$ (ensure-loop l (loop-stk-incr)))
2598
(ls$ (loop.set-rule l r))
2599
(ls$ (loop.set-node l x))
2600
(ls$ (set-loop-stk-top (1+^ l) ls$)))
2603
(defunk oper-rule-match (x r ls$ us$)
2604
(if (not (rule.enabled r))
2606
(letk ((match. ls$ us$ (process-sieves x r)))
2609
(letk ((ls$ (incr-rule-ctr r)))
2612
(defunk rule-matches (x r narg ls$ us$)
2613
(letk ((ls$ (incr-rule-tryctr r))
2614
(match. ls$ (unify-args x (rule.lhs r) narg)))
2617
(letk ((match. ls$ us$ (process-sieves x r)))
2620
(letk ((ls$ (incr-rule-ctr r)))
2621
(mv t ls$ us$)))))))
2623
(defunk args-are-quotes (n i x ls$)
2625
(and (=^ (node.opcd (node.arg x i)) (opcd-quote))
2626
(args-are-quotes (1-^ n) (1+^ i) x ls$))))
2628
(defunk args-quote-objs (n i x ls$)
2630
(cons (qobj.obj (node.arg (node.arg x i) 0))
2631
(args-quote-objs (1-^ n) (1+^ i) x ls$))))
2633
(defunk apply-exec (op x ls$)
2634
(letk ((args. (args-quote-objs (oper.narg op) 0 x ls$))
2635
(erp. val. (funcall (oper.name op) args.)))
2636
(if erp. (mv^ x ls$)
2637
(letk ((ls$ (incr-rule-ctr (oper.exec op)))
2638
(y ls$ (install-quote val. ls$)))
2641
(defunk exec-counterpart (opcd x ls$ us$)
2642
(letk ((op (opcd.index opcd))
2643
(narg (opcd.narg opcd))
2644
(exec (oper.exec op)))
2645
(if (not (args-are-quotes narg 0 x ls$))
2646
(mv^ x (dcv-empty) nil ls$ us$)
2647
(letk ((go. ls$ us$ (oper-rule-match x exec ls$ us$)))
2649
(mv^ x (dcv-empty) nil ls$ us$)
2650
(letk ((rslt ls$ (apply-exec op x ls$)))
2651
(mv^ rslt (dcv-empty) nil ls$ us$)))))))
2653
(defunk node/= (x y) :inline
2655
(or (and (=^ (node.opcd x) (opcd-quote))
2656
(=^ (node.opcd y) (opcd-quote)))
2657
(and (=^ x (node-nil)) (non-nilp y))
2658
(and (=^ y (node-nil)) (non-nilp x)))))
2660
(defunk built-in-rewrites (opcd x) :inline
2661
(cond ((opcd.is-equal opcd)
2662
(letk ((lhs (node.arg x 0))
2663
(rhs (node.arg x 1)))
2664
(cond ((node= lhs rhs) (node-t))
2665
((node/= lhs rhs) (node-nil))
2668
(letk ((tst (node.arg x 0))
2669
(tbr (node.arg x 1))
2670
(fbr (node.arg x 2)))
2671
(cond ((=^ tst (node-nil)) fbr)
2672
((non-nilp tst) tbr)
2673
((node= tbr fbr) tbr)
2677
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
2678
#| main kernel rewrite loop functions (rewrite-node is entry point) |#
2679
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
2681
(defunk depth-exceeded () :inline
2682
(zp (get-current-clock ls$)))
2684
(defunk space-exceeded () :inline
2685
(>^ (+^ (get-num-trans-nodes ls$) (get-num-of-nodes ls$))
2686
(get-node-limit ls$)))
2688
; compute-if-direction can return one of the following:
2689
; nil -- if-test has rewritten to nil, only rewrite false branch
2690
; t -- if-test has rewritten to non-nil, only rewrite true branch
2691
; :both -- assume context on both branches
2692
; :only-t -- assume context only on true branch
2693
; :only-nil -- assume context only on false branch
2694
; :neither -- do not assume context on either branch
2696
(defunk compute-if-direction (tst+) :inline
2697
(cond ((=^ tst+ (node-nil)) nil)
2699
(t (letk ((op (opcd.index (node.opcd tst+))))
2700
(if (oper.assume-tbr op)
2701
(if (oper.assume-fbr op) :both :only-t)
2702
(if (oper.assume-fbr op) :only-nil :neither))))))
2704
(defunk drop-dctx-dcv (dcx dcv) :inline
2705
(if (>=^ dcx (dctx-max-rep)) dcv (logand^ dcv (lognot^ (ash^ 1 dcx)))))
2708
(defunk promote-node (x ls$)
2709
(if (promoted x) (mv^ x ls$)
2710
(letk ((ls$ (promote-args (opcd.narg (node.opcd x)) 0 x ls$)))
2711
(install-node x t ls$))))
2713
(defunk promote-args (n i x ls$)
2715
(letk ((a ls$ (promote-node (node.arg x i) ls$))
2716
(ls$ (node.set-arg x i a)))
2717
(promote-args (1-^ n) (1+^ i) x ls$))))
2720
(defunk well-formed-context-equation (tst) :inline
2721
(and (opcd.is-equal (node.opcd tst))
2722
(not (=^ (node.opcd (node.arg tst 0)) (opcd-quote)))))
2724
(defunk create-equal-tst-for-case (tst cas. ls$)
2725
(letk ((opcd (node.opcd tst)))
2726
(assert (/=^ opcd (opcd-quote))
2727
(if (and cas. (or (opcd.is-equal opcd)
2728
(not (oper.boolp (opcd.index opcd)))))
2730
(letk ((x ls$ (allocate-node (opcd-equal) (size-btm) nil ls$))
2731
(ls$ (node.set-arg x 0 tst))
2732
(rhs (if cas. (node-t) (node-nil)))
2733
(ls$ (node.set-arg x 1 rhs)))
2734
(promote-node x ls$))))))
2736
(defunk push-new-context (tst ls$)
2737
(letk ((top (get-curr-ctx-top ls$)))
2738
(if (>=^ top (length-curr-ctx-stk ls$))
2739
(error "Maximum number of context stack nodes exceeded. ~
2740
The user may wish to adjust the maximum node bound for KAS."
2742
(letk ((ls$ (set-curr-ctx-stk top tst ls$))
2743
(ls$ (set-curr-ctx-top (1+^ top) ls$)))
2746
(defunk pop-new-context (ls$)
2747
(set-curr-ctx-top (1-^ (get-curr-ctx-top ls$)) ls$))
2750
(defunk is-subterm (x y ls$)
2752
(letk ((opcd (node.opcd y)))
2753
(and (/=^ opcd (opcd-quote))
2754
(not (opcd.is-var opcd))
2755
(is-subterm-args x y (opcd.narg opcd) 0 ls$)))))
2757
(defunk is-subterm-args (x y n i ls$)
2759
(or (is-subterm x (node.arg y i) ls$)
2760
(is-subterm-args x y (1-^ n) (1+^ i) ls$))))
2764
(defunk mark-node-in-ctx (x dcv ls$)
2765
(letk ((opcd (node.opcd x)))
2766
(if (=^ opcd (opcd-quote)) ls$
2767
(letk ((ls$ (if (node.in-ctx x) ls$
2768
(letk ((ls$ (create-new-undo (node-btm) dcv x (dcv-btm) ls$))
2769
(ls$ (node.set-in-ctx x t)))
2771
(mark-args-in-ctx (opcd.narg opcd) 0 x dcv ls$)))))
2773
(defunk mark-args-in-ctx (n i x dcv ls$)
2775
(letk ((ls$ (mark-node-in-ctx (node.arg x i) dcv ls$)))
2776
(mark-args-in-ctx (1-^ n) (1+^ i) x dcv ls$))))
2779
(defunk mark-subnodes-in-ctx (x dcv ls$)
2780
(letk ((opcd (node.opcd x)))
2781
(if (=^ opcd (opcd-quote)) ls$
2782
(mark-args-in-ctx (opcd.narg opcd) 0 x dcv ls$))))
2785
(defunk rewrite-hyps-args (n i h dcv ls$ us$)
2786
(if (zp n) (mv t dcv ls$ us$)
2787
(letk ((a dcv+ ls$ us$ (rewrite-node (node.arg h i) ls$ us$)))
2788
(if (not (non-nilp a)) (mv nil (dcv-empty) ls$ us$)
2789
(rewrite-hyps-args (1-^ n) (1+^ i) h (logior^ dcv dcv+) ls$ us$)))))
2791
(defunk rewrite-hyps (h ls$ us$)
2792
(if (=^ h (node-t)) (mv t (dcv-empty) ls$ us$)
2793
(letk ((bc (get-bchain-limit ls$)))
2794
(if (zp bc) (mv nil (dcv-empty) ls$ us$)
2795
(letk ((ls$ (set-bchain-limit (1-^ bc) ls$))
2797
(pass. dcv ls$ us$ (rewrite-hyps-args (opcd.narg op) 0 h (dcv-empty) ls$ us$))
2798
(ls$ (set-bchain-limit bc ls$)))
2799
(mv pass. dcv ls$ us$))))))
2801
(defunk apply-rule (r x narg ls$ us$)
2802
(if (not (rule.enabled r))
2803
(mv^ x (dcv-empty) nil ls$ us$)
2804
(letk ((match. ls$ us$ (rule-matches x r narg ls$ us$)))
2806
(letk ((ls$ (pop-var-chg-stk)))
2807
(mv^ x (dcv-empty) nil ls$ us$))
2808
(letk ((ls$ (push-loop-stack r x ls$))
2809
(h+ ls$ (subst-node (rule.hyps r) ls$))
2810
(y ls$ (subst-node (rule.rhs r) ls$))
2811
(ls$ (pop-var-chg-stk))
2812
(pass. dcv ls$ us$ (rewrite-hyps h+ ls$ us$)))
2814
(mv^ x (dcv-empty) t ls$ us$)
2815
(letk ((ls$ (trace-rule-app (rule.traced r) (rule.rune r) x)))
2816
(mv^ y dcv nil ls$ us$))))))))
2818
(defunk apply-rules (rules. x narg cond-failed. ls$ us$)
2820
(mv^ x (dcv-empty) cond-failed. ls$ us$)
2821
(letk ((y dcv c-f. ls$ us$ (apply-rule (first rules.) x narg ls$ us$))
2822
(cond-failed. (or c-f. cond-failed.)))
2824
(mv^ y dcv cond-failed. ls$ us$)
2825
(apply-rules (rest rules.) x narg cond-failed. ls$ us$)))))
2827
(defunk apply-rewrite (opcd x) :inline
2828
(apply-rules (oper.rules (opcd.index opcd)) x (opcd.narg opcd) nil ls$ us$))
2830
(defunk rewrite-step (opcd x ls$ us$)
2831
(letk ((y (built-in-rewrites opcd x)))
2832
(if (/=^ y x) (mv^ y (dcv-empty) nil ls$ us$)
2833
(letk ((y dcv c-f. ls$ us$ (apply-rewrite opcd x)))
2834
(if (/=^ y x) (mv^ y dcv c-f. ls$ us$)
2835
(exec-counterpart opcd x ls$ us$))))))
2837
(defunk decr-and-rewrite (x ls$ us$)
2838
(letk ((clk (get-current-clock ls$))
2839
(ls$ (set-current-clock (1-^ clk) ls$))
2840
(x+ dcv ls$ us$ (rewrite-node x ls$ us$))
2841
(ls$ (set-current-clock clk ls$)))
2842
(mv^ x+ dcv ls$ us$)))
2844
(defunk extend-context (tst dcv ndx ls$ us$)
2845
(if (not (well-formed-context-equation tst))
2847
(letk ((nxt (get-next-extend-age ls$))
2848
(ls$ (set-current-age nxt ls$))
2849
(ls$ (set-next-extend-age (1+^ nxt) ls$))
2850
(lhs (node.arg tst 0))
2851
(rhs (node.arg tst 1))
2852
(ls$ (update-rep lhs rhs dcv 1 ls$)))
2853
(if (not (get-allow-context-reduction ls$)) (mv t ls$ us$)
2854
(letk ((ls$ (mark-subnodes-in-ctx lhs dcv ls$))
2855
(ls$ (mark-node-in-ctx rhs dcv ls$)))
2856
(if (not (node.in-ctx lhs)) (mv t ls$ us$)
2857
(rewrite-context (get-curr-ctx-top ls$) lhs ndx ls$ us$)))))))
2859
(defunk rewrite-context (i lhs ndx ls$ us$)
2860
(if (=^ i 0) (mv t ls$ us$)
2862
(if (=^ i ndx) (rewrite-context i lhs ndx ls$ us$)
2863
(letk ((top (get-curr-ctx-stk i ls$)))
2864
(if (not (and (well-formed-context-equation top)
2865
(is-subterm lhs top ls$)))
2866
(rewrite-context i lhs ndx ls$ us$)
2867
(letk ((top-lhs (node.arg top 0))
2868
(tmp (node.rep top-lhs))
2869
(ls$ (node.set-rep top-lhs (node-btm)))
2870
(top+ dcv ls$ us$ (decr-and-rewrite top ls$ us$))
2871
(ls$ (node.set-rep top-lhs tmp)))
2872
(cond ((=^ top+ (node-nil))
2875
(rewrite-context i lhs ndx ls$ us$))
2877
(letk ((ls$ (set-curr-ctx-stk i top+ ls$))
2878
(ls$ (create-new-undo (node-btm) dcv top i ls$))
2879
(vald. ls$ us$ (extend-context top+ dcv i ls$ us$)))
2880
(if (not vald.) (mv nil ls$ us$)
2881
(rewrite-context i lhs ndx ls$ us$))))))))))))
2883
(defunk rewrite-case (cas. brn tst+ dir. ls$ us$)
2885
((and (not (eq dir. cas.))
2887
(mv^ brn (dcv-empty) ls$ us$)) ; DO NOT REWRITE branch
2890
(if cas. (eq dir. :only-nil) (eq dir. :only-t)))
2891
(rewrite-node brn ls$ us$)) ; REWRITE branch with no test assumption
2893
(letk ((dcx- (get-current-dctx ls$))
2894
(age (get-current-age ls$))
2895
(dcx+ ls$ (create-new-dctx ls$))
2896
(tst= ls$ (create-equal-tst-for-case tst+ cas. ls$))
2897
(ndx ls$ (push-new-context tst= ls$))
2898
(vald. ls$ us$ (extend-context tst= (ash^ 1 dcx+) ndx ls$ us$)))
2900
(letk ((ls$ (pop-new-context ls$))
2901
(ls$ (restore-previous-state dcx- dcx+ age ls$)))
2902
(mv^ (node-btm) (dcv-empty) ls$ us$))
2903
(letk ((node dcv ls$ us$ (rewrite-node brn ls$ us$))
2904
(ls$ (pop-new-context ls$))
2905
(ls$ (restore-previous-state dcx- dcx+ age ls$))
2906
(dcv (drop-dctx-dcv dcx+ dcv)))
2907
(assert (<=^ (max-in-dcv dcv) dcx-)
2908
(mv^ node dcv ls$ us$))))))))
2910
(defunk rewrite-args-if (x ls$ us$)
2911
(letk ((tst (node.arg x 0))
2912
(tbr (node.arg x 1))
2913
(fbr (node.arg x 2))
2914
(tst+ tst-dcv ls$ us$ (rewrite-node tst ls$ us$))
2915
(dir. (compute-if-direction tst+))
2916
(tbr+ tbr-dcv ls$ us$ (rewrite-case t tbr tst+ dir. ls$ us$))
2917
(fbr+ fbr-dcv ls$ us$ (rewrite-case nil fbr tst+ dir. ls$ us$))
2918
(no-tbr. (=^ tbr+ (node-btm)))
2919
(no-fbr. (=^ fbr+ (node-btm)))
2920
(tst+ (if no-tbr. (node-nil) (if no-fbr. (node-t) tst+)))
2921
(tbr+ (if no-tbr. tbr tbr+))
2922
(fbr+ (if no-fbr. fbr fbr+))
2923
(ls$ (node.set-arg x 0 tst+))
2924
(ls$ (node.set-arg x 1 tbr+))
2925
(ls$ (node.set-arg x 2 fbr+))
2926
(chgd. (or (/=^ tst+ tst) (/=^ tbr+ tbr) (/=^ fbr+ fbr))))
2927
(mv chgd. (logior^ tst-dcv tbr-dcv fbr-dcv) ls$ us$)))
2929
(defunk rewrite-args-op (n i x chgd. dcv ls$ us$)
2930
(if (zp n) (mv chgd. dcv ls$ us$)
2931
(letk ((a (node.arg x i))
2932
(a+ dcv+ ls$ us$ (rewrite-node a ls$ us$))
2933
(ls$ (node.set-arg x i a+))
2934
(chgd. (or (/=^ a+ a) chgd.))
2935
(dcv (logior^ dcv dcv+)))
2936
(rewrite-args-op (1-^ n) (1+^ i) x chgd. dcv ls$ us$))))
2938
(defunk rewrite-args-hide () :inline
2939
(mv nil (dcv-empty) ls$ us$))
2941
(defunk rewrite-args (opcd x ls$ us$)
2942
(assert (temp-node x)
2943
(cond ((opcd.is-if opcd) (rewrite-args-if x ls$ us$))
2944
((=^ opcd (opcd-hide)) (rewrite-args-hide))
2945
(t (rewrite-args-op (opcd.narg opcd) 0 x nil (dcv-empty) ls$ us$)))))
2947
(defunk rewrite-node+ (x- opcd rep age ls$ us$)
2949
(assert (and (promoted x-) (/=^ x- rep))
2950
(letk ((x+ dcv ls$ us$ (decr-and-rewrite rep ls$ us$))
2951
(dcv (logior^ (node.dcv x-) dcv))
2952
(ls$ (update-rep x- x+ dcv 2 ls$)))
2953
(mv^ x+ dcv ls$ us$)))
2954
;; /\ If we have a rep node, then rewrite the rep node and return the result, otherwise....
2955
(letk ((x ls$ (install-node x- nil ls$))
2956
(chgd. dcv1 ls$ us$ (rewrite-args opcd x ls$ us$)))
2957
(if (and (/=^ rep (node-btm)) (not chgd.))
2958
(assert (and (promoted x-) (/=^ x- rep))
2959
(letk ((ls$ (update-rep x- (-^ age) (dcv-btm) 3 ls$)))
2960
(mv^ x- (dcv-empty) ls$ us$)))
2961
;; /\ Rewrite the args and if the args have not changed and we were not marked to rewrite, then return original, otherwise...
2962
(letk ((x+ dcv2 cond-failed. ls$ us$ (rewrite-step opcd x ls$ us$)))
2964
(letk ((x+ dcv3 ls$ us$ (decr-and-rewrite x+ ls$ us$))
2965
(dcv (logior^ dcv1 dcv2 dcv3))
2966
(ls$ (update-rep x- x+ dcv 4 ls$))
2967
(ls$ (update-rep x x+ dcv 5 ls$)))
2968
(mv^ x+ dcv ls$ us$))
2969
;; /\ Apply rewrite rules and return rewrite of result if a rule fired, otherwise...
2970
(letk ((x ls$ (promote-node x ls$))
2974
(letk ((x+ dcv2 ls$ us$ (decr-and-rewrite rep ls$ us$))
2975
(dcv (logior^ dcv1 dcv2 (node.dcv x)))
2976
(ls$ (update-rep x- x+ dcv 6 ls$))
2977
(ls$ (update-rep x x+ dcv 7 ls$)))
2978
(mv^ x+ dcv ls$ us$)))
2979
;; /\ promote the node (it is in normal form) and then see if the node has a rep node which can then rewrite and return the result, otherwise...
2980
;; \/ look to see if we had a conditional rule fail due to hypothesis and mark rep accordingly and return promoted node.
2981
(letk ((ls$ (update-rep x- x dcv1 8 ls$))
2982
(x-rep (if cond-failed. (node-btm) (-^ age)))
2983
(ls$ (update-rep x x-rep (dcv-btm) 9 ls$)))
2984
(mv^ x dcv1 ls$ us$))))))))))
2986
(defunk rewrite-node (x ls$ us$)
2987
(letk ((x ls$ (check-memos x ls$))
2988
(opcd (node.opcd x))
2990
(age (get-current-age ls$)))
2993
(error "Maximum number of iterations in term rewriting was reached. ~
2994
The user may wish to adjust the rewrite depth for KAS."
2995
x (mv^ x (dcv-empty) ls$ us$)))
2997
(error "Maximum number of allocated nodes was reached during KAS rewriting. ~
2998
The user may wish to adjust the maximum node bound for KAS."
2999
x (mv^ x (dcv-empty) ls$ us$)))
3000
((or (=^ opcd (opcd-quote)) ;; quoted objects are always in normal-form
3001
(and (opcd.is-var opcd) ;; var.s which are not equated, are in normal-form
3003
(>=^ (-^ rep) age)) ;; node tagged in normal-form in current ctx
3004
(assert (promoted x)
3005
(mv^ x (dcv-empty) ls$ us$)))
3007
(assert (/=^ rep x) ;; this isn't critical, but we don't expect this to happen
3008
(letk ((save-depth (get-rew-call-depth ls$))
3009
(save-alloc (get-alloc-trans ls$))
3010
(save-num (get-num-trans-nodes ls$))
3011
(save-ltop (get-loop-stk-top ls$))
3012
(ls$ (set-rew-call-depth (1+^ save-depth) ls$))
3013
(x+ dcv ls$ us$ (rewrite-node+ x opcd rep age ls$ us$))
3014
(ls$ (set-num-trans-nodes save-num ls$))
3015
(ls$ (set-alloc-trans save-alloc ls$))
3016
(ls$ (set-rew-call-depth save-depth ls$))
3017
(ls$ (set-loop-stk-top save-ltop ls$)))
3018
(assert (promoted x+)
3019
(assert (=^ (get-current-age ls$) age)
3020
(mv x+ dcv ls$ us$)))))))))
3023
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
3024
#| stobj initialization and wrapper call for rewrite-node |#
3025
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
3027
(defabbrev rlrcd.sieves (rule) (first rule))
3028
(defabbrev rlrcd.lhs (rule) (second rule))
3029
(defabbrev rlrcd.rhs (rule) (third rule))
3030
(defabbrev rlrcd.rune (rule) (fourth rule))
3031
(defabbrev rlrcd.enabled (rule) (fifth rule))
3032
(defabbrev rlrcd.traced (rule) (sixth rule))
3033
(defabbrev rlrcd.hyps (rule) (seventh rule))
3035
(defabbrev make-rlrcd (sieves lhs rhs rune enabled traced hyps)
3036
(list sieves lhs rhs rune enabled traced hyps))
3038
(defabbrev oprcd.name (opr) (first (first opr)))
3039
(defabbrev oprcd.is-var (opr) (second (first opr)))
3040
(defabbrev oprcd.rules (opr) (third (first opr)))
3041
(defabbrev oprcd.narg (opr) (fourth (first opr)))
3042
(defabbrev oprcd.boolp (opr) (first (second opr)))
3043
(defabbrev oprcd.is-if (opr) (second (second opr)))
3044
(defabbrev oprcd.is-equal (opr) (third (second opr)))
3045
(defabbrev oprcd.non-nil (opr) (fourth (second opr)))
3046
(defabbrev oprcd.exec-enabled (opr) (fifth (second opr)))
3048
(defun make-oprcd (name is-var rules narg
3049
boolp is-if is-equal non-nil
3051
(list (list name is-var rules narg)
3052
(list boolp is-if is-equal non-nil
3055
(defun kern-chk-rule-traced (rune typ name descr)
3056
(if (atom descr) descr
3057
(let ((elem (first descr)))
3058
(cond ((atom elem) elem)
3059
((or (equal rune (first elem))
3060
(and (member-eq typ '(:rewrite :definition))
3061
(equal name (first elem))))
3063
(t (kern-chk-rule-traced rune typ name (rest descr)))))))
3065
(defun kern-is-rule-traced (rune ls$)
3066
(declare (xargs :stobjs ls$))
3068
(and (consp rune) (eql (len rune) 2))
3070
(kern-chk-rule-traced rune (first rune) (second rune)
3071
(get-initial-rule-trace-descriptor ls$))))
3072
(if (kern-is-trace-mark traced) traced
3073
(er hard 'kern-is-rule-traced "illegal trace mark: ~x0" traced)))))
3075
(defmacro defunf (fn args body)
3077
(declare (xargs :stobjs ls$)
3078
(type (signed-byte ,(kern-fixnum-size)) ,(first args)))
3081
(defunf kern-install-auto-rule (ndx opr typ ls$)
3082
(let* ((rune (list typ (oprcd.name opr)))
3084
(:executable-counterpart (oprcd.exec-enabled opr))))
3085
(traced (kern-is-rule-traced rune ls$)))
3086
(letk ((r ls$ (kern-alloc-rule-ndx ls$))
3088
(:executable-counterpart (oper.set-exec ndx r))
3090
(ls$ (rule.set-op r ndx))
3091
(ls$ (rule.set-sieves r ()))
3092
(ls$ (rule.set-rune r rune))
3093
(ls$ (rule.set-lhs r (kern-node-btm)))
3094
(ls$ (rule.set-rhs r (kern-node-btm)))
3095
(ls$ (rule.set-hyps r (kern-node-btm)))
3096
(ls$ (rule.set-ctr r 0))
3097
(ls$ (rule.set-tryctr r 0))
3098
(ls$ (rule.set-enabled r enabled))
3099
(ls$ (rule.set-traced r traced)))
3102
(defunf kern-install-oper-type (ndx opr typ ls$)
3103
(let* ((rune (case typ
3104
(:boolp (oprcd.boolp opr))
3105
(:is-if (oprcd.is-if opr))
3106
(:is-equal (oprcd.is-equal opr))
3107
(:non-nil (oprcd.non-nil opr))
3108
(t (er hard 'kern-install-oper-type "illegal typ"))))
3109
(flag (if rune t nil))
3111
(:boolp (oper.set-boolp ndx flag))
3112
(:is-if (oper.set-is-if ndx flag))
3113
(:is-equal (oper.set-is-equal ndx flag))
3114
(:non-nil (oper.set-non-nil ndx flag))
3116
(ls$ (if (not (eq typ :boolp)) ls$
3117
(letk ((ls$ (oper.set-assume-tbr ndx flag))
3118
(ls$ (oper.set-assume-fbr ndx flag)))
3120
(ls$ (if (consp rune)
3121
(letk ((r ls$ (kern-alloc-rule-ndx ls$))
3122
(ls$ (rule.set-op r ndx))
3123
(ls$ (rule.set-sieves r ()))
3124
(ls$ (rule.set-rune r rune))
3125
(ls$ (rule.set-lhs r (kern-node-btm)))
3126
(ls$ (rule.set-rhs r (kern-node-btm)))
3127
(ls$ (rule.set-hyps r (kern-node-btm)))
3128
(ls$ (rule.set-ctr r 1)))
3133
(defun kern-install-oper-base (name is-var opr ls$)
3134
(declare (xargs :stobjs ls$))
3135
(letk ((hash (kern-fn-hash-code name))
3136
(chain (get-op-hash hash ls$))
3137
(opcd (kern-lookup-opcd chain name is-var ls$))
3138
(ndx (if (/=^ opcd (kern-opcd-btm))
3140
(get-next-op-ndx ls$)))
3141
(ls$ (if (/=^ opcd (kern-opcd-btm))
3143
(letk ((ls$ (ensure-oper ndx (kern-oper-stor-incr)))
3144
(ls$ (oper.set-uniq ndx chain))
3145
(ls$ (set-op-hash hash ndx ls$))
3146
(ls$ (set-next-op-ndx (1+^ ndx) ls$)))
3148
(ls$ (oper.set-name ndx name))
3149
(ls$ (oper.set-is-var ndx is-var))
3150
(ls$ (oper.set-rules ndx ()))
3151
(ls$ (oper.set-num-nodes ndx 0))
3152
(ls$ (oper.set-num-trans ndx 0))
3153
(ls$ (oper.set-narg ndx (oprcd.narg opr)))
3154
(ls$ (oper.set-next-stk ndx (kern-opcd-btm)))
3155
(ls$ (oper.set-bound ndx (kern-node-btm)))
3156
(ls$ (oper.set-assume-tbr ndx nil))
3157
(ls$ (oper.set-assume-fbr ndx nil))
3158
(ls$ (if (eq name 'quote) ls$
3159
(kern-install-auto-rule ndx opr :executable-counterpart ls$)))
3160
(ls$ (kern-install-oper-type ndx opr :boolp ls$))
3161
(ls$ (kern-install-oper-type ndx opr :is-if ls$))
3162
(ls$ (kern-install-oper-type ndx opr :is-equal ls$))
3163
(ls$ (kern-install-oper-type ndx opr :non-nil ls$))
3164
(ls$ (if (member name (get-flip-t-fns ls$))
3165
(oper.set-assume-tbr ndx (not (oper.assume-tbr ndx)))
3167
(ls$ (if (member name (get-flip-nil-fns ls$))
3168
(oper.set-assume-fbr ndx (not (oper.assume-fbr ndx)))
3172
(defun kern-create-alist (vars vals)
3174
(acons (first vars) (first vals)
3175
(kern-create-alist (rest vars) (rest vals)))))
3178
(defun kern-expand-lambdas-fn (term alist)
3180
(if (assoc term alist)
3181
(cdr (assoc term alist))
3183
((eq (first term) 'quote)
3185
((atom (first term))
3187
(kern-expand-lambdas-args (rest term) alist)))
3189
(kern-expand-lambdas-fn
3190
(third (first term))
3192
(second (first term))
3193
(kern-expand-lambdas-args (rest term) alist))))))
3195
(defun kern-expand-lambdas-args (args alist)
3197
(cons (kern-expand-lambdas-fn (first args) alist)
3198
(kern-expand-lambdas-args (rest args) alist))))
3201
(defabbrev kern-expand-lambdas (term)
3202
(kern-expand-lambdas-fn term ()))
3204
(defun kern-expand-lambda-terms (terms)
3206
(cons (kern-expand-lambdas (first terms))
3207
(kern-expand-lambda-terms (rest terms)))))
3209
(defun kern-install-rules (rlrcds op ls$)
3210
(declare (xargs :stobjs ls$))
3212
(oper.set-rules op ())
3213
(letk ((r. (first rlrcds))
3214
(lhs. (kern-expand-lambdas (rlrcd.lhs r.)))
3215
(rhs. (kern-expand-lambdas (rlrcd.rhs r.)))
3216
(hyps. (kern-expand-lambdas (rlrcd.hyps r.)))
3217
(sieves. ls$ (kern-install-sieves (rlrcd.sieves r.) ls$))
3218
(ndx ls$ (kern-alloc-rule-ndx ls$))
3219
(lhs ls$ (kern-term-to-node lhs. ls$))
3220
(rhs ls$ (kern-term-to-node rhs. ls$))
3221
(hyps ls$ (kern-term-to-node hyps. ls$))
3222
(ls$ (rule.set-rune ndx (rlrcd.rune r.)))
3223
(ls$ (rule.set-sieves ndx sieves.))
3224
(ls$ (rule.set-ctr ndx 0))
3225
(ls$ (rule.set-lhs ndx lhs))
3226
(ls$ (rule.set-rhs ndx rhs))
3227
(ls$ (rule.set-hyps ndx hyps))
3228
(ls$ (rule.set-op ndx op))
3229
(ls$ (rule.set-enabled ndx (rlrcd.enabled r.)))
3230
(ls$ (rule.set-traced ndx (rlrcd.traced r.)))
3231
(ls$ (kern-install-rules (rest rlrcds) op ls$)))
3232
(oper.set-rules op (cons ndx (oper.rules op))))))
3234
(defun kern-install-base-opers (oprcds ls$)
3235
(declare (xargs :stobjs ls$))
3236
(if (endp oprcds) ls$
3237
(letk ((ls$ (kern-install-oper-base (oprcd.name (first oprcds))
3238
(oprcd.is-var (first oprcds))
3239
(first oprcds) ls$)))
3240
(kern-install-base-opers (rest oprcds) ls$))))
3242
(defun kern-install-rlrcds (oprcds ls$)
3243
(declare (xargs :stobjs ls$))
3244
(if (endp oprcds) ls$
3245
(letk ((opcd (kern-find-fn-opcd (oprcd.name (first oprcds))))
3246
(ndx (kern-assert (/=^ opcd (kern-opcd-btm))
3248
(ls$ (kern-install-rules (oprcd.rules (first oprcds)) ndx ls$)))
3249
(kern-install-rlrcds (rest oprcds) ls$))))
3251
(defun kern-install-oprcds (oprcds ls$)
3252
(declare (xargs :stobjs ls$))
3253
(letk ((ls$ (kern-install-base-opers oprcds ls$)))
3254
(kern-install-rlrcds oprcds ls$)))
3256
(defun kern-remove-equal-list (e x)
3258
((equal e (first x))
3259
(kern-remove-equal-list e (rest x)))
3261
(kern-remove-equal-list e (rest x))))))
3264
(defun kern-unfak-term (term)
3265
(cond ((atom term) term)
3266
((eq (first term) 'quote) term)
3267
((eq (first term) 'fak)
3268
(kern-unfak-term (second term)))
3269
(t (cons (first term)
3270
(kern-unfak-terms (rest term))))))
3272
(defun kern-unfak-terms (args)
3274
(cons (kern-unfak-term (first args))
3275
(kern-unfak-terms (rest args)))))
3278
(defun kern-translate-hyps (hyps)
3279
(cons (symbol-append 'hyps-and- (length hyps)) hyps))
3281
(defun kern-prune-sieves (hyps)
3282
(cond ((endp hyps) ())
3283
((and (consp (first hyps))
3284
(eq (caar hyps) 'siv))
3285
(kern-prune-sieves (rest hyps)))
3286
(t (cons (first hyps) (kern-prune-sieves (rest hyps))))))
3288
(defun kern-extract-sieves (hyps)
3289
(cond ((endp hyps) ())
3290
((and (consp (first hyps))
3291
(eq (caar hyps) 'siv))
3292
(cons (if (quotep (cadar hyps)) (cadr (cadar hyps)) (cadar hyps))
3293
(kern-extract-sieves (rest hyps))))
3294
(t (kern-extract-sieves (rest hyps)))))
3296
(defun kern-find-new-rules (lemmas recp ens all-fns rules new-fns ls$)
3297
(declare (xargs :stobjs ls$))
3299
(mv new-fns (reverse rules))
3300
(let* ((lemma (first lemmas))
3301
(rhs (kern-unfak-term (access rewrite-rule lemma :rhs)))
3302
(lhs (kern-unfak-term (access rewrite-rule lemma :lhs)))
3303
(rune (access rewrite-rule lemma :rune))
3304
(subclass (access rewrite-rule lemma :subclass))
3305
(hyps (and (not (eq subclass 'abbreviation))
3306
(kern-unfak-terms (access rewrite-rule lemma :hyps))))
3307
(heuristic-info (access rewrite-rule lemma :heuristic-info)))
3308
(if (and (eq (access rewrite-rule lemma :equiv) 'equal)
3309
(member-eq subclass '(definition abbreviation backchain))
3310
(implies (eq subclass 'backchain) (null heuristic-info)))
3311
(let* ((enabled (enabled-numep (access rewrite-rule lemma :nume) ens))
3312
(traced (kern-is-rule-traced rune ls$))
3313
(is-def (eq subclass 'definition))
3314
(enabled (and enabled (not (and is-def recp))))
3315
(sieves (kern-extract-sieves hyps))
3316
(hyps (kern-prune-sieves hyps))
3317
(hyps (kern-translate-hyps hyps))
3318
(new-rule (make-rlrcd sieves lhs rhs rune enabled traced hyps))
3319
(rule-fns (union-eq (all-fnnames lhs) (union-eq (all-fnnames rhs) (all-fnnames hyps)))))
3320
(kern-find-new-rules (rest lemmas) recp ens all-fns (cons new-rule rules)
3321
(union-eq (set-difference-eq rule-fns all-fns) new-fns) ls$))
3322
(kern-find-new-rules (rest lemmas) recp ens all-fns rules new-fns ls$)))))
3324
(defun kern-filter-fak-thms (lemmas fn)
3325
(cond ((endp lemmas) ())
3326
((eq (first (access rewrite-rule (first lemmas) :lhs)) fn)
3327
(cons (first lemmas)
3328
(kern-filter-fak-thms (rest lemmas) fn)))
3329
(t (kern-filter-fak-thms (rest lemmas) fn))))
3331
(defun kern-rules-alist-fn (fns all-fns rules-alist fak-thms ens wrld ls$)
3332
(declare (xargs :stobjs ls$))
3334
(reverse rules-alist)
3335
(let ((fn (first fns)))
3336
(mv-let (new-fns rules)
3337
(kern-find-new-rules (append (kern-getprop fn 'lemmas)
3338
(kern-filter-fak-thms fak-thms fn))
3339
(kern-getprop fn 'recursivep)
3340
ens (cons fn all-fns) () () ls$)
3341
(kern-rules-alist-fn (append (rest fns) new-fns)
3342
(append new-fns all-fns)
3343
(cons (cons fn rules) rules-alist)
3344
fak-thms ens wrld ls$)))))
3346
(defun kern-trans-fak-thms (lemmas)
3347
(if (endp lemmas) ()
3348
(let* ((lemma (first lemmas))
3349
(lhs (kern-unfak-term (access rewrite-rule lemma :lhs)))
3350
(equiv (access rewrite-rule lemma :equiv)))
3351
(if (not (and (eq equiv 'equal)
3353
(not (quotep lhs))))
3354
(kern-trans-fak-thms (rest lemmas))
3355
(cons (make rewrite-rule
3356
:rune (access rewrite-rule lemma :rune)
3357
:nume (access rewrite-rule lemma :nume)
3358
:hyps (access rewrite-rule lemma :hyps)
3361
:rhs (access rewrite-rule lemma :rhs)
3362
:subclass (access rewrite-rule lemma :subclass)
3363
:heuristic-info (access rewrite-rule lemma :heuristic-info)
3364
:backchain-limit-lst (access rewrite-rule lemma :backchain-limit-lst)
3365
:match-free (access rewrite-rule lemma :match-free))
3366
(kern-trans-fak-thms (rest lemmas)))))))
3368
(defun kern-rules-alist (fns ens wrld ls$)
3369
(declare (xargs :stobjs ls$))
3370
(kern-rules-alist-fn fns fns () (kern-trans-fak-thms (kern-getprop 'fak 'lemmas)) ens wrld ls$))
3372
(defun kern-find-nume (pairs rune)
3373
(cond ((endp pairs) nil)
3374
((equal rune (cdar pairs))
3376
(t (kern-find-nume (cdr pairs) rune))))
3378
(defun kern-type-pre-subsetp (tp ens ts)
3379
(and (enabled-numep (access type-prescription tp :nume) ens)
3380
(ts-subsetp (access type-prescription tp :basic-ts) ts)
3381
(null (access type-prescription tp :hyps))
3382
(null (access type-prescription tp :vars))))
3384
;; NOTE: In the following function, we have decided to ignore the enabled
3385
;; status of the definition rule we use to determine the match. The problem is
3386
;; that the user may want a function to be matched to equal or if, but disable
3387
;; the definition rule. One level of indirection in the function definition
3388
;; will fail this check and allow the user to define functions which are equal,
3389
;; if, but are not understood by the simplifier as such.
3391
;; (enabled-numep (access rewrite-rule lemma :nume) ens)
3393
(defun kern-match-defn-body (lemma ens lhs fn num-formals)
3394
(declare (ignore ens))
3395
(and (equal (length lhs) (1+ num-formals))
3396
(member (access rewrite-rule lemma :subclass)
3397
'(abbreviation definition))
3398
(null (access rewrite-rule lemma :hyps))
3399
(let ((rune (access rewrite-rule lemma :rune)))
3400
(and (consp rune) (eq (first rune) :definition)))
3401
(eq (access rewrite-rule lemma :equiv) 'equal)
3402
(equal (access rewrite-rule lemma :lhs) lhs)
3403
(equal (access rewrite-rule lemma :rhs)
3404
(cons fn (rest lhs)))))
3406
(defun kern-find-boolp (lst ens)
3408
(let ((tp (first lst)))
3409
(if (kern-type-pre-subsetp tp ens *ts-boolean*)
3410
(access type-prescription tp :rune)
3411
(kern-find-boolp (rest lst) ens)))))
3413
(defun kern-find-non-nil (lst ens)
3415
(let ((tp (first lst)))
3416
(if (kern-type-pre-subsetp tp ens *ts-non-nil*)
3417
(access type-prescription tp :rune)
3418
(kern-find-non-nil (rest lst) ens)))))
3420
(defun kern-find-is-if (lst ens lhs)
3422
(let ((r (first lst)))
3423
(if (kern-match-defn-body r ens lhs 'if 3)
3424
(access rewrite-rule r :rune)
3425
(kern-find-is-if (rest lst) ens lhs)))))
3427
(defun kern-find-is-equal (lst ens lhs)
3429
(let ((r (first lst)))
3430
(if (kern-match-defn-body r ens lhs 'equal 2)
3431
(access rewrite-rule r :rune)
3432
(kern-find-is-equal (rest lst) ens lhs)))))
3434
(defun kern-create-oprcds (alist ens wrld)
3436
(let* ((fn (caar alist))
3437
(rules (cdar alist))
3438
(exec (list :executale-counterpart fn))
3439
(formals (kern-getprop fn 'formals))
3440
(lhs (cons fn formals))
3441
(nume (kern-find-nume (kern-getprop fn 'runic-mapping-pairs) exec))
3442
(enabled-exec (if nume (enabled-numep nume ens) t))
3443
(num-formals (if (eq fn 'quote) 1 (length formals)))
3444
(type-pres (kern-getprop fn 'type-prescriptions))
3445
(lemmas (kern-getprop fn 'lemmas))
3446
(boolp (or (eq fn 'equal) (kern-find-boolp type-pres ens)))
3447
(non-nil (or (eq fn 'cons) (kern-find-non-nil type-pres ens)))
3448
(is-if (or (eq fn 'if) (kern-find-is-if lemmas ens lhs)))
3449
(is-equal (or (eq fn 'equal) (kern-find-is-equal lemmas ens lhs)))
3450
(exec-enabled (if enabled-exec t nil)))
3451
(cons (make-oprcd fn nil rules num-formals
3452
boolp is-if is-equal non-nil exec-enabled)
3453
(kern-create-oprcds (cdr alist) ens wrld)))))
3455
(defunf kern-init-node-hash (n ls$)
3458
(ls$ (set-node-hash n (kern-node-btm) ls$)))
3459
(kern-init-node-hash n ls$))))
3461
(defunf kern-init-quote-hash (n ls$)
3464
(ls$ (set-quote-hash n (kern-node-btm) ls$)))
3465
(kern-init-quote-hash n ls$))))
3467
(defunf kern-init-op-hash (n ls$)
3470
(ls$ (set-op-hash n (kern-opcd-btm) ls$)))
3471
(kern-init-op-hash n ls$))))
3473
(defunf kern-init-memo-tbl (m ls$)
3476
(ls$ (memo.set-opcd m (kern-opcd-btm))))
3477
(kern-init-memo-tbl m ls$))))
3479
(defun kern-install-and-check-quotes (alst ls$)
3480
(declare (xargs :stobjs ls$))
3482
(letk ((node ls$ (kern-create-quote (caar alst))))
3483
(kern-force-assert (equal node (cdar alst))
3484
(kern-install-and-check-quotes (cdr alst) ls$)))))
3486
(defun kern-base-quote-alist ()
3487
(list (cons nil (kern-node-nil))
3488
(cons t (kern-node-t))))
3490
(defun kern-install-base-quotes (ls$)
3491
(declare (xargs :stobjs ls$))
3492
(kern-install-and-check-quotes (kern-base-quote-alist) ls$))
3494
(defun kern-find-max-narg1 (oprcds max)
3495
(cond ((endp oprcds)
3496
(or max (er hard 'kern-logic-init "illegal empty list of oprcds")))
3498
(> (oprcd.narg (first oprcds))
3500
(kern-find-max-narg1 (rest oprcds) (first oprcds)))
3501
(t (kern-find-max-narg1 (rest oprcds) max))))
3503
(defun kern-find-max-narg (oprcds)
3504
(kern-find-max-narg1 oprcds nil))
3506
(defun kern-check-opcode-alist (alst ls$)
3507
(declare (xargs :stobjs ls$))
3509
(letk ((opcd (kern-find-fn-opcd (caar alst))))
3510
(if (not (equal opcd (cdar alst)))
3511
(prog2$ (er hard 'kern-check-opcode-alist
3512
"built-in opcd failure: ~x0"
3513
(list opcd (caar alst) (cdar alst)))
3515
(kern-check-opcode-alist (cdr alst) ls$)))))
3517
(defun kern-initial-fns () '(quote if equal cons hide fail))
3519
(defun kern-base-opcd-alist ()
3520
(list (cons 'quote (kern-opcd-quote))
3521
(cons 'if (kern-opcd-if))
3522
(cons 'equal (kern-opcd-equal))
3523
(cons 'cons (kern-opcd-cons))
3524
(cons 'hide (kern-opcd-hide))
3525
(cons 'fail (kern-opcd-fail))))
3527
(defun kern-check-base-opcodes (ls$)
3528
(declare (xargs :stobjs ls$))
3529
(kern-check-opcode-alist (kern-base-opcd-alist) ls$))
3531
(defunf kern-clear-node-counts (n ls$)
3534
(ls$ (oper.set-num-nodes n 0))
3535
(ls$ (oper.set-num-trans n 0)))
3536
(kern-clear-node-counts n ls$))))
3538
(defun user-node-limit (sp) (expt 2 sp))
3539
(defun user-node-alloc (sp) (floor (user-node-limit sp) 8))
3540
(defun user-node-step (sp) (user-node-alloc sp))
3541
(defun qobj-tbl-initial (sp) (floor (user-node-alloc sp) 4))
3542
(defun oper-tbl-initial (sp) (floor (user-node-alloc sp) 8))
3543
(defun rule-tbl-initial (sp) (* 2 (oper-tbl-initial sp)))
3544
(defun undo-stk-initial (sp) (* 2 (oper-tbl-initial sp)))
3545
(defun node-hash-size (sp) (* (user-node-alloc sp) 2))
3546
(defun node-hash-mask (sp) (1- (node-hash-size sp)))
3547
;; The 1+ in the next definition is needed because an entry may take two slots
3548
;; and we need an extra slot for padding the last entry in the memo-table.
3549
(defun node-memo-size (sp) (1+ (floor (node-hash-size sp)
3550
(kern-hash-memo-divisor))))
3551
(defun node-memo-hash (sp) (- (node-memo-size sp) 2))
3552
(defun start-clock-value (sp) (floor (user-node-alloc sp) 2))
3553
(defun node-trans-size (sp) (* (floor (user-node-alloc sp) 2)
3554
(+ (kern-base-trans-alloc)
3555
(kern-avg-num-args))))
3556
(defun node-stor-size (sp) (* (user-node-alloc sp)
3557
(+ (kern-base-node-alloc)
3558
(kern-avg-num-args))))
3559
(defun initial-loop-size (sp) (floor (user-node-alloc sp) 8))
3560
(defun curr-ctx-stk-size (sp) (* sp sp 10))
3561
(defun first-quote-ndx () (1+ (kern-qobj-btm)))
3562
(defun first-oper-ndx () (1+ (kern-opcd-btm)))
3563
(defun first-node-ndx () (1+ (kern-node-btm)))
3564
(defun first-trans-ndx () (1+ (kern-node-btm)))
3566
(defun kern-logic-init (term wrld ens ls$)
3567
(declare (xargs :stobjs ls$))
3568
(let* ((fns (all-fnnames term))
3569
(fns (set-difference-eq fns (kern-initial-fns)))
3570
(fns (append (kern-initial-fns) fns))
3571
(alist (kern-rules-alist fns ens wrld ls$))
3572
(oprcds (kern-create-oprcds alist ens wrld)))
3573
(cond ((>= (length oprcds) (kern-max-num-fns))
3574
(prog2$ (er0 hard 'kern-logic-init
3575
"The kernel simplifier has a hard limit of ~x0 for the number of ~
3576
functions which can be installed for a given term. The number of ~
3577
functions required for this call is ~x1 which exceeds th limit."
3581
((>= (oprcd.narg (kern-find-max-narg oprcds)) (kern-max-num-args))
3582
(prog2$ (er0 hard 'kern-logic-init
3583
"The kernel simplifier has a hard limit of ~x0 for the number of ~
3584
arguments for any given function. The number of arguments for the ~
3585
function ~x1 is ~x2 which exceeds the limit."
3587
(oprcd.name (kern-find-max-narg oprcds))
3588
(oprcd.narg (kern-find-max-narg oprcds)))
3591
(letk ((sp (get-kern-size-param ls$))
3592
(ls$ (resize-node-stor (node-stor-size sp) ls$))
3593
(ls$ (resize-node-hash (node-hash-size sp) ls$))
3594
(ls$ (kern-init-node-hash (node-hash-size sp) ls$))
3595
(ls$ (set-alloc-nodes (first-node-ndx) ls$))
3596
(ls$ (set-num-of-nodes 0 ls$))
3597
(ls$ (ensure-qobj (qobj-tbl-initial sp) 0))
3598
(ls$ (resize-quote-hash (kern-quote-hash-size) ls$))
3599
(ls$ (kern-init-quote-hash (kern-quote-hash-size) ls$))
3600
(ls$ (set-next-quote (first-quote-ndx) ls$))
3601
(ls$ (set-node-step (user-node-step sp) ls$))
3602
(ls$ (set-node-limit (user-node-limit sp) ls$))
3603
(ls$ (set-hash-mask (node-hash-mask sp) ls$))
3604
(ls$ (resize-trans-stor (node-trans-size sp) ls$))
3605
(ls$ (set-alloc-trans (first-trans-ndx) ls$))
3606
(ls$ (set-num-trans-nodes 0 ls$))
3607
(ls$ (ensure-memo (node-memo-size sp) 0))
3608
(ls$ (kern-init-memo-tbl (node-memo-size sp) ls$))
3609
(ls$ (ensure-loop (initial-loop-size sp) 0))
3610
(ls$ (set-loop-stk-top (1+ (kern-loop-btm)) ls$))
3611
(ls$ (ensure-oper (oper-tbl-initial sp) 0))
3612
(ls$ (set-next-op-ndx (first-oper-ndx) ls$))
3613
(ls$ (resize-op-hash (kern-op-hash-tbl-size) ls$))
3614
(ls$ (kern-init-op-hash (kern-op-hash-tbl-size) ls$))
3615
(ls$ (ensure-undo (undo-stk-initial sp) 0))
3616
(ls$ (set-undo-top 1 ls$))
3617
(ls$ (set-undo-free-list (kern-undo-btm) ls$))
3618
(ls$ (ensure-rule (rule-tbl-initial sp) 0))
3619
(ls$ (set-next-rule-ndx (kern-first-rule-ndx) ls$))
3620
(ls$ (set-current-world wrld ls$))
3621
(ls$ (set-current-ens ens ls$))
3622
(ls$ (set-var-chg-stk (kern-node-btm) ls$))
3623
(ls$ (set-current-age 1 ls$))
3624
(ls$ (set-bchain-limit 2 ls$))
3625
(ls$ (set-next-extend-age 2 ls$))
3626
(ls$ (set-current-dctx (kern-dctx-0) ls$))
3627
(ls$ (set-current-clock (start-clock-value sp) ls$))
3628
(ls$ (set-warned-ctx-depth nil ls$))
3629
(ls$ (kern-install-base-quotes ls$))
3630
(ls$ (kern-install-oprcds oprcds ls$))
3631
(ls$ (kern-check-base-opcodes ls$))
3632
(ls$ (set-rew-call-depth 0 ls$))
3633
(ls$ (set-curr-ctx-top 0 ls$))
3634
(ls$ (resize-curr-ctx-stk (curr-ctx-stk-size sp) ls$))
3635
(ls$ (kern-clear-node-counts (num-of-oper) ls$)))
3639
(defunk has-fail-subterm (x ls$)
3640
(letk ((opcd (node.opcd x)))
3641
(or (=^ opcd (opcd-fail))
3642
(and (/=^ opcd (opcd-quote))
3643
(not (opcd.is-var opcd))
3644
(args-has-fail-subterm x (opcd.narg opcd) 0 ls$)))))
3646
(defunk args-has-fail-subterm (x n i ls$)
3648
(or (has-fail-subterm (node.arg x i) ls$)
3649
(args-has-fail-subterm x (1-^ n) (1+^ i) ls$))))
3652
(defun kern-create-result (node term ls$ state)
3653
(declare (xargs :stobjs (ls$ state)))
3654
(if (=^ node (kern-node-btm))
3655
(let ((state (fms "An internal error in kernel-simplify: returned (node-btm). ~
3656
Please notify current maintainer of kern-simp."
3657
() (standard-co state) state nil)))
3658
(mv t term () state))
3659
(let ((ttree (kern-print-stats ls$)))
3660
(if (kern-has-fail-subterm node ls$)
3661
(mv nil term ttree state)
3662
(mv nil (kern-node-to-term node) ttree state)))))
3664
(defun kern-simplify-term (term wrld ens ls$ us$)
3665
(declare (xargs :stobjs (ls$ us$)))
3666
(letk ((term. (kern-unfak-term term))
3667
(ls$ (kern-logic-init term. wrld ens ls$))
3668
(us$ (kern-user-init ls$ us$))
3669
(node ls$ (kern-term-to-node term. ls$))
3670
(node+ dcv ls$ us$ (kern-rewrite-node node ls$ us$)))
3671
(kern-force-assert (or (=^ dcv (kern-dcv-empty)) (list dcv))
3672
(mv node+ ls$ us$))))
3674
(defun parse-kernel-simplify-hint (hint)
3675
(if (and (consp hint)
3676
(eq (first hint) 'k-s-hint)
3677
(quote-listp (rest hint)))
3678
(mv (second (second hint))
3679
(second (third hint))
3680
(second (fourth hint))
3681
(second (fifth hint))
3682
(second (sixth hint))
3683
(second (seventh hint))
3684
(second (eighth hint))
3685
(second (ninth hint)))
3686
(mv nil nil nil nil nil nil 4 t)))
3688
(defun min-size-param () 13) ;; this one ensures lower-bound for several parameters
3689
(defun max-size-param () 36) ;; this one is limited by the number of bits in a node
3691
(defun kern-init-top-params (hint ls$)
3692
(declare (xargs :stobjs ls$))
3693
(mv-let (size-param quiet alloc-display flip-t flip-nil rule-trace prune-depth context-reduce)
3694
(parse-kernel-simplify-hint hint)
3695
(let* ((size-param (min (max (nfix size-param) (min-size-param)) (max-size-param)))
3696
(ls$ (set-kern-size-param size-param ls$))
3697
(ls$ (set-output-verbose (not quiet) ls$))
3698
(ls$ (set-ls$-resize-array-display alloc-display ls$))
3699
(ls$ (set-initial-rule-trace-descriptor rule-trace ls$))
3700
(ls$ (set-initial-node-prune-depth prune-depth ls$))
3701
(ls$ (set-allow-context-reduction context-reduce ls$))
3702
(ls$ (set-flip-t-fns (and (true-listp flip-t) flip-t) ls$))
3703
(ls$ (set-flip-nil-fns (and (true-listp flip-nil) flip-nil) ls$)))
3706
(defun kern-clause-to-term (cl)
3707
(cond ((endp cl) *T*)
3708
((endp (rest cl)) (first cl))
3709
(t (list 'if (first cl) *T* (kern-clause-to-term (rest cl))))))
3711
(defun kern-simplify-main (cl hint ls$ us$ state)
3712
(declare (xargs :stobjs (ls$ us$ state)))
3713
(let* ((ls$ (kern-init-top-params hint ls$))
3714
(cl (kern-expand-lambda-terms cl))
3715
(term (kern-clause-to-term cl)))
3716
(mv-let (node ls$ us$)
3717
(kern-simplify-term term (w state) (ens state) ls$ us$)
3718
(mv-let (erp term ttree state)
3719
(kern-create-result node term ls$ state)
3720
(mv erp term ttree state ls$ us$)))))
3722
(defun kernel-simplify (cl hint state)
3723
(declare (xargs :stobjs state))
3724
(with-local-stobj ls$
3725
(mv-let (erp term ttree state ls$)
3726
(with-local-stobj us$
3727
(mv-let (erp term ttree state ls$ us$)
3728
(kern-simplify-main cl hint ls$ us$ state)
3729
(mv erp term ttree state ls$)))
3730
(declare (ignore ttree))
3731
(let ((cl-list (list (list term))))
3732
(mv erp cl-list state)))))
3738
;; the "hint" for the kernel-simplify processor is expected to be a call of the following
3739
;; function where the arguments to the call should be quoted constants which are used to
3740
;; provide optional parameters to simplifier:
3742
(defun k-s-hint (size-param quiet alloc-display flip-t flip-nil rule-trace prune-depth context-reduce)
3744
(list 'quote size-param)
3746
(list 'quote alloc-display)
3747
(list 'quote flip-t)
3748
(list 'quote flip-nil)
3749
(list 'quote rule-trace)
3750
(list 'quote prune-depth)
3751
(list 'quote context-reduce)))
3753
(defmacro defthmk-generic (name form &rest aux)
3754
`(defthm ,name ,form
3757
:do-not '(preprocess simplify eliminate-destructors fertilize generalize eliminate-irrelevance)
3758
:clause-processor (:function kernel-simplify :hint (k-s-hint 20 nil nil nil nil nil 4 nil))))
3761
(define-trusted-clause-processor kernel-simplify nil :ttag kernel-simplify-ttag)
added
removed
books/workshops/2009/sumners/support/kas.lisp
