mmarco/kenzo
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Resolved #40 #41 #43 #45 as per Francis' comment. The (unless (>= abar-degr *))

Browse Source 
check prevents "degree overflow."
This commit is contained in:
Gerd Heber 2015-11-18 19:49:09 -06:00
parent 86306c9c42
commit d061360c93
3 changed files with 752 additions and 826 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

102
test/cl-space-efhm-test.lisp
View File

@ -1,19 +1,12 @@
(in-package :kenzo-test) (in-package :kenzo-test)
(in-suite :kenzo) (in-suite :kenzo)
#|
(test cs-hat-u-t (test cs-hat-u-t
(cat:cat-init) (cat:cat-init)
(let* ((c (cat:cs-hat-u-t (cat:k-z-1))) (let ((c (cat:cs-hat-u-t (cat:k-z-1)))
(abar (random-abar 8 4)) abar-degr
(abar-degr (apply #'+ (mapcar #'car (cat:abar-list abar)))) gnrt)
(gnrt (cat:tnpr 5 (cat:tnpr 3 (cat:gbar 3 0 '(1 2) 0 '(3) 0 '())
2 '(4 5))
abar-degr abar)))
(cat:? c (+ 5 abar-degr) gnrt)
(is (cat:cmbn-zero-p (cat:? c (cat:? c (+ 5 abar-degr) gnrt))))
(dotimes (i 10) (dotimes (i 10)
(let ((abar (random-abar 8 4))) (let ((abar (random-abar 8 4)))
(setf abar-degr (apply #'+ (mapcar #'car (cat:abar-list abar)))) (setf abar-degr (apply #'+ (mapcar #'car (cat:abar-list abar))))
@ -53,20 +46,14 @@
(print (cat:? c (+ 4 abar-degr) gnrt)) (print (cat:? c (+ 4 abar-degr) gnrt))
(is (cat:cmbn-zero-p (cat:? c (cat:? c (+ 4 abar-degr) (is (cat:cmbn-zero-p (cat:? c (cat:? c (+ 4 abar-degr)
gnrt))))))))) gnrt)))))))))
|#
#|
(test cs-hat-t-u (test cs-hat-t-u
(cat:cat-init) (cat:cat-init)
(dotimes (i 5) (print (random-abar 8 4))) (dotimes (i 5) (print (random-abar 8 4)))
(let* ((c (cat:cs-hat-t-u (cat:k-z-1))) (let ((c (cat:cs-hat-t-u (cat:k-z-1)))
(abar (random-abar 8 4)) abar-degr
(abar-degr (apply #'+ (mapcar #'car (cat:abar-list abar)))) gnrt)
(gnrt (cat:tnpr 5 (cat:tnpr 3 (cat:gbar 3 0 '(1 2) 0 '(3) 0 '())
2 '(4 5))
abar-degr abar)))
(cat:? c (+ 5 abar-degr) gnrt)
(is (cat:cmbn-zero-p (cat:? c (cat:? c (+ 5 abar-degr) gnrt))))
(dotimes (i 10) (dotimes (i 10)
(let ((abar (random-abar 8 4))) (let ((abar (random-abar 8 4)))
(setf abar-degr (apply #'+ (mapcar #'car (cat:abar-list abar)))) (setf abar-degr (apply #'+ (mapcar #'car (cat:abar-list abar))))
@ -107,9 +94,8 @@
(print (cat:? c (+ 4 abar-degr) gnrt)) (print (cat:? c (+ 4 abar-degr) gnrt))
(is (cat:cmbn-zero-p (cat:? c (cat:? c (+ 4 abar-degr) (is (cat:cmbn-zero-p (cat:? c (cat:? c (+ 4 abar-degr)
gnrt))))))))) gnrt)))))))))
|#
#|
(test cs-left-hmeq-hat (test cs-left-hmeq-hat
(cat:cat-init) (cat:cat-init)
(let ((c (cat:cs-left-hmeq-hat (cat:k-z-1))) (let ((c (cat:cs-left-hmeq-hat (cat:k-z-1)))
@ -155,23 +141,8 @@
(print (cat:? c (+ 4 abar-degr) gnrt)) (print (cat:? c (+ 4 abar-degr) gnrt))
(is (cat:cmbn-zero-p (cat:? c (cat:? c (+ 4 abar-degr) (is (cat:cmbn-zero-p (cat:? c (cat:? c (+ 4 abar-degr)
gnrt))))))))) gnrt)))))))))
|#
(test cs-pre-left-hmeq-left-reduction-intr-f
(cat:cs-pre-left-hmeq-left-reduction-intr-f
(cat:cmbn 6 100 (cat:tnpr 4 (cat:tnpr 2 'a 2 'b) 2 'c)
10 (cat:tnpr 6 (cat:tnpr 2 'a 4 'b) 0 'c)
50 (cat:tnpr 6 (cat:tnpr 6 'a 0 'b) 0 'c)
1 (cat:tnpr 6 (cat:tnpr 6 'aa 0 'b) 0 'c))))
(test cs-pre-left-hmeq-left-reduction-intr-g
(let ((g (cat:cs-pre-left-hmeq-left-reduction-intr-g '())))
(funcall g (cat:cmbn 3 14 (cat:gbar 3 0 'a 1 'b 0 '())))))
#|
(test cs-pre-left-hmeq-left-reduction (test cs-pre-left-hmeq-left-reduction
(cat:cat-init) (cat:cat-init)
(let ((rdct (cat:cs-pre-left-hmeq-left-reduction (cat:k-z-1))) (let ((rdct (cat:cs-pre-left-hmeq-left-reduction (cat:k-z-1)))
@ -179,17 +150,6 @@
gnrt gnrt
gbar) gbar)
(cat:pre-check-rdct rdct) (cat:pre-check-rdct rdct)
(setf cat:*tc* (cat:cmbn 0 1
(cat:tnpr 0 (cat:tnpr 0
cat:+null-gbar+ 0 '())
0 cat:+null-abar+))
cat:*bc* (cat:cmbn 0 1 cat:+null-gbar+))
(check-rdct)
(setf cat:*tc* (cat:cmbn 1 1
(cat:tnpr 1 (cat:tnpr 0
cat:+null-gbar+ 1 '(13))
0 cat:+null-abar+)))
(check-rdct)
(dotimes (i 10) (dotimes (i 10)
(let ((abar (random-abar 8 4))) (let ((abar (random-abar 8 4)))
(setf abar-degr (apply #'+ (mapcar #'car (cat:abar-list abar)))) (setf abar-degr (apply #'+ (mapcar #'car (cat:abar-list abar))))
@ -235,25 +195,15 @@
(setf cat:*tc* (cat:cmbn (+ 4 abar-degr) 1 gnrt)) (setf cat:*tc* (cat:cmbn (+ 4 abar-degr) 1 gnrt))
(setf cat:*bc* (cat:cmbn 5 1 gbar)) (setf cat:*bc* (cat:cmbn 5 1 gbar))
(check-rdct)))))) (check-rdct))))))
|#
#|
(test cs-left-hmeq-left-reduction (test cs-left-hmeq-left-reduction
(cat:cat-init) (cat:cat-init)
(let ((rdct (cat:cs-left-hmeq-left-reduction (cat:k-z-1))) (let ((rdct (cat:cs-left-hmeq-left-reduction (cat:k-z-1)))
abar-degr gnrt gbar) abar-degr
gnrt
gbar)
(cat:pre-check-rdct rdct) (cat:pre-check-rdct rdct)
(setf cat:*tc* (cat:cmbn 0 1 (cat:tnpr 0
(cat:tnpr 0 cat:+null-gbar+
0 '()) 0
cat:+null-abar+))
cat:*bc* (cat:cmbn 0 1 cat:+null-gbar+))
(check-rdct)
(setf cat:*tc* (cat:cmbn 1 1 (cat:tnpr 1
(cat:tnpr 0 cat:+null-gbar+
1 '(13)) 0
cat:+null-abar+)))
(check-rdct)
(dotimes (i 10) (dotimes (i 10)
(let ((abar (random-abar 8 4))) (let ((abar (random-abar 8 4)))
(setf abar-degr (apply #'+ (mapcar #'car (cat:abar-list abar)))) (setf abar-degr (apply #'+ (mapcar #'car (cat:abar-list abar))))
@ -299,7 +249,7 @@
(setf cat:*tc* (cat:cmbn (+ 4 abar-degr) 1 gnrt)) (setf cat:*tc* (cat:cmbn (+ 4 abar-degr) 1 gnrt))
(setf cat:*bc* (cat:cmbn 5 1 gbar)) (setf cat:*bc* (cat:cmbn 5 1 gbar))
(check-rdct)))))) (check-rdct))))))
|#
(test cs-pre-left-hmeq-right-reduction-intr-f (test cs-pre-left-hmeq-right-reduction-intr-f
(cat:cs-pre-left-hmeq-right-reduction-intr-f (cat:cs-pre-left-hmeq-right-reduction-intr-f
@ -315,24 +265,13 @@
(let ((g (cat:cs-pre-left-hmeq-right-reduction-intr-g 'i))) (let ((g (cat:cs-pre-left-hmeq-right-reduction-intr-g 'i)))
(funcall g (cat:cmbn 3 2 (cat:abar 1 'a 2 'b))))) (funcall g (cat:cmbn 3 2 (cat:abar 1 'a 2 'b)))))
#|
(test cs-pre-left-hmeq-right-reduction (test cs-pre-left-hmeq-right-reduction
(cat:cat-init) (cat:cat-init)
(let ((rdct (cat:cs-pre-left-hmeq-right-reduction (cat:k-z-1))) (let ((rdct (cat:cs-pre-left-hmeq-right-reduction (cat:k-z-1)))
abar-degr abar-degr
gnrt) gnrt)
(cat:pre-check-rdct rdct) (cat:pre-check-rdct rdct)
(setf cat:*tc* (cat:cmbn 0 1 (cat:tnpr 0
(cat:tnpr 0 cat:+null-gbar+
0 '())
0 cat:+null-abar+))
cat:*bc* (cat:cmbn 0 1 cat:+null-abar+))
(check-rdct)
(setf cat:*tc* (cat:cmbn 1 1 (cat:tnpr 1
(cat:tnpr 0 cat:+null-gbar+
1 '(13))
0 cat:+null-abar+)))
(check-rdct)
(dotimes (i 10) (dotimes (i 10)
(let ((abar (random-abar 8 4))) (let ((abar (random-abar 8 4)))
(setf abar-degr (apply #'+ (mapcar #'car (cat:abar-list abar)))) (setf abar-degr (apply #'+ (mapcar #'car (cat:abar-list abar))))
@ -373,27 +312,14 @@
(setf cat:*tc* (cat:cmbn (+ 4 abar-degr) 1 gnrt)) (setf cat:*tc* (cat:cmbn (+ 4 abar-degr) 1 gnrt))
(setf cat:*bc* (cat:cmbn abar-degr 1 abar)) (setf cat:*bc* (cat:cmbn abar-degr 1 abar))
(check-rdct)))))) (check-rdct))))))
|#
#| #|
(test cs-left-hmeq-right-reduction (test cs-left-hmeq-right-reduction
(cat:cat-init) (cat:cat-init)
(let ((rdct (cat:cs-left-hmeq-right-reduction (cat:k-z-1))) (let ((rdct (cat:cs-left-hmeq-right-reduction (cat:k-z-1)))
abar-degr abar-degr
gnrt) gnrt)
(cat:pre-check-rdct rdct) (cat:pre-check-rdct rdct)
(setf cat:*tc* (cat:cmbn 0 1
(cat:tnpr 0 (cat:tnpr 0 cat:+null-gbar+
0 '())
0 cat:+null-abar+))
cat:*bc* (cat:cmbn 0 1 cat:+null-abar+))
(check-rdct)
(setf cat:*tc* (cat:cmbn 1 1
(cat:tnpr 1 (cat:tnpr 0 cat:+null-gbar+
1 '(13))
0 cat:+null-abar+)))
(check-rdct)
(dotimes (i 10) (dotimes (i 10)
(let ((abar (random-abar 4 2))) (let ((abar (random-abar 4 2)))
(setf abar-degr (apply #'+ (mapcar #'car (cat:abar-list abar)))) (setf abar-degr (apply #'+ (mapcar #'car (cat:abar-list abar))))