From 3d6c2812b9da04779d43f0403f19b59c528f7400 Mon Sep 17 00:00:00 2001 From: Gerd Heber Date: Mon, 20 Jul 2015 20:13:04 -0500 Subject: [PATCH] Another batch of CL-SPACE-EFHM tests extracted. --- kenzo-test.asd | 4 +- package.lisp | 9 + run-kenzo-test.lisp | 4 +- src/cl-space-efhm.lisp | 419 ++++++++--------------------------- test/cl-space-efhm-test.lisp | 232 ++++++++++++++++++- 5 files changed, 322 insertions(+), 346 deletions(-) diff --git a/kenzo-test.asd b/kenzo-test.asd index a9f2c28..b51c07e 100644 --- a/kenzo-test.asd +++ b/kenzo-test.asd @@ -1,6 +1,6 @@ (defsystem :kenzo-test - :description "A simple test suite for Kenzo" + :description "A simple regression test suite for Kenzo" :serial t :version "0.1.0" :author "Francis Sergeraert " @@ -17,9 +17,9 @@ (:file "chain-complexes-test") (:file "chcm-elementary-op-test") (:file "circle") + (:file "cl-space-efhm-test") (:file "combinations-test") (:file "cones-test") - (:file "cl-space-efhm-test") (:file "delta-test") (:file "diabolo") (:file "effective-homology-test") diff --git a/package.lisp b/package.lisp index cad06ed..63a12cd 100644 --- a/package.lisp +++ b/package.lisp @@ -29,6 +29,7 @@ ;; bar.lisp + +NULL-ABAR+ ABAR BAR BAR-BASIS-LENGTH @@ -97,6 +98,13 @@ CS-HAT-T-U CS-HAT-U-T + CS-LEFT-HMEQ-HAT + CS-LEFT-HMEQ-LEFT-REDUCTION + CS-PRE-LEFT-HMEQ-LEFT-REDUCTION + CS-PRE-LEFT-HMEQ-LEFT-REDUCTION-INTR-F + CS-PRE-LEFT-HMEQ-LEFT-REDUCTION-INTR-G + CS-PRE-LEFT-HMEQ-RIGHT-REDUCTION-INTR-F + CS-PRE-LEFT-HMEQ-RIGHT-REDUCTION-INTR-G ;; classes.lisp @@ -136,6 +144,7 @@ ;; classifying-space.lisp + +NULL-GBAR+ CLASSIFYING-SPACE ;; combinations.lisp diff --git a/run-kenzo-test.lisp b/run-kenzo-test.lisp index af1dcd3..7c086da 100644 --- a/run-kenzo-test.lisp +++ b/run-kenzo-test.lisp @@ -1,10 +1,10 @@ -(DECLAIM (OPTIMIZE (speed 0) (space 0) (debug 3))) +(DECLAIM (OPTIMIZE (speed 3) (space 0) (debug 3))) (require 'asdf) (asdf:operate 'asdf:load-op 'kenzo-test) (fiveam:run!) -#+ccl(quit) +#+(or ecl ccl) (quit) #+sbcl(sb-ext:exit) diff --git a/src/cl-space-efhm.lisp b/src/cl-space-efhm.lisp index f158e51..bb9463d 100644 --- a/src/cl-space-efhm.lisp +++ b/src/cl-space-efhm.lisp @@ -135,63 +135,6 @@ (setf (slot-value rslt 'grmd) hat-u-u) rslt))) -#| -(cat-init) -(setf c (cs-hat-t-u (k-z-1))) -(defun random-abar (tot-degr~ max-degr) - (do ((rslt nil) - (cum-degr 0 (+ cum-degr degr 1)) - (degr)) - ((>= cum-degr tot-degr~) (make-abar :list rslt)) - (setf degr (1+ (random max-degr))) - (push (brgn (1+ degr) - (let ((list (make-list degr))) - (mapl - #'(lambda (sublist) - (setf (car sublist) (- (random 21) 10))) - list) - list)) - rslt))) -(dotimes (i 5) (print (random-abar 8 4))) -(setf abar (random-abar 8 4)) -(setf abar-degr (apply #'+ (mapcar #'car (abar-list abar)))) -(setf gnrt (tnpr 5 (tnpr 3 (gbar 3 0 '(1 2) 0 '(3) 0 '()) 2 '(4 5)) - abar-degr abar)) -(? c (+ 5 abar-degr) gnrt) -(? c *) -(dotimes (i 10) - (let ((abar (random-abar 8 4))) - (setf abar-degr (apply #'+ (mapcar #'car (abar-list abar)))) - (setf gnrt (tnpr 5 (tnpr 3 (gbar 3 0 '(1 2) 0 '(3) 0 '()) 2 '(4 5)) - abar-degr abar)) - (unless (>= abar-degr 10) - (print (? c (+ 5 abar-degr) gnrt)) - (print (? c (? c (+ 5 abar-degr) gnrt)))))) -(dotimes (i 10) - (let ((abar (random-abar 8 4))) - (setf abar-degr (apply #'+ (mapcar #'car (abar-list abar)))) - (setf gnrt (tnpr 6 (tnpr 3 (gbar 3 0 '(1 2) 0 '(3) 0 '()) 3 '(4 5 6)) - abar-degr abar)) - (unless (>= abar-degr 9) - (print (? c (+ 6 abar-degr) gnrt)) - (print (? c (? c (+ 6 abar-degr) gnrt)))))) -(dotimes (i 10) - (let ((abar (random-abar 8 4))) - (setf abar-degr (apply #'+ (mapcar #'car (abar-list abar)))) - (setf gnrt (tnpr 5 (tnpr 2 (gbar 2 0 '(3) 0 '()) 3 '(4 5 6)) - abar-degr abar)) - (unless (>= abar-degr 10) - (print (? c (+ 5 abar-degr) gnrt)) - (print (? c (? c (+ 5 abar-degr) gnrt)))))) -(dotimes (i 10) - (let ((abar (random-abar 8 4))) - (setf abar-degr (apply #'+ (mapcar #'car (abar-list abar)))) - (setf gnrt (tnpr 4 (tnpr 2 (gbar 2 0 '(3) 0 '()) 2 '(4 5)) - abar-degr abar)) - (unless (>= abar-degr 11) - (print (? c (+ 4 abar-degr) gnrt)) - (print (? c (? c (+ 4 abar-degr) gnrt)))))) -|# (DEFUN CS-LEFT-HMEQ-HAT (smgr &aux (hat-t-u (cs-hat-t-u smgr)) @@ -204,85 +147,32 @@ (the chain-complex (add hat-t-u hat-right-perturbation))) -#| -(cat-init) -(setf c (cs-left-hmeq-hat (k-z-1))) -(defun random-abar (tot-degr~ max-degr) - (do ((rslt nil) - (cum-degr 0 (+ cum-degr degr 1)) - (degr)) - ((>= cum-degr tot-degr~) (make-abar :list rslt)) - (setf degr (1+ (random max-degr))) - (push (brgn (1+ degr) - (let ((list (make-list degr))) - (mapl - #'(lambda (sublist) - (setf (car sublist) (- (random 21) 10))) - list) - list)) - rslt))) -(dotimes (i 10) - (let ((abar (random-abar 8 4))) - (setf abar-degr (apply #'+ (mapcar #'car (abar-list abar)))) - (setf gnrt (tnpr 5 (tnpr 3 (gbar 3 0 '(1 2) 0 '(3) 0 '()) 2 '(4 5)) - abar-degr abar)) - (unless (>= abar-degr 10) - (print (? c (+ 5 abar-degr) gnrt)) - (print (? c (? c (+ 5 abar-degr) gnrt)))))) -(dotimes (i 10) - (let ((abar (random-abar 8 4))) - (setf abar-degr (apply #'+ (mapcar #'car (abar-list abar)))) - (setf gnrt (tnpr 6 (tnpr 3 (gbar 3 0 '(1 2) 0 '(3) 0 '()) 3 '(4 5 6)) - abar-degr abar)) - (unless (>= abar-degr 9) - (print (? c (+ 6 abar-degr) gnrt)) - (print (? c (? c (+ 6 abar-degr) gnrt)))))) -(dotimes (i 10) - (let ((abar (random-abar 8 4))) - (setf abar-degr (apply #'+ (mapcar #'car (abar-list abar)))) - (setf gnrt (tnpr 5 (tnpr 2 (gbar 2 0 '(3) 0 '()) 3 '(4 5 6)) - abar-degr abar)) - (unless (>= abar-degr 10) - (print (? c (+ 5 abar-degr) gnrt)) - (print (? c (? c (+ 5 abar-degr) gnrt)))))) -(dotimes (i 10) - (let ((abar (random-abar 8 4))) - (setf abar-degr (apply #'+ (mapcar #'car (abar-list abar)))) - (setf gnrt (tnpr 4 (tnpr 2 (gbar 2 0 '(3) 0 '()) 2 '(4 5)) - abar-degr abar)) - (unless (>= abar-degr 11) - (print (? c (+ 4 abar-degr) gnrt)) - (print (? c (? c (+ 4 abar-degr) gnrt)))))) -|# (DEFUN CS-PRE-LEFT-HMEQ-LEFT-REDUCTION-INTR-F (cmbn) (declare (type cmbn cmbn)) (the cmbn - (with-cmbn (degr list) cmbn - (make-cmbn - :degr degr - :list (mapcar - #'(lambda (term) - (declare (type term term)) - (with-term (cffc tnpr) term - (term cffc (gnrt1 (gnrt1 tnpr))))) - (member-if - #'(lambda (term) - (declare (type term term)) - (with-term (cffc tnpr) term - (declare (ignore cffc)) - (with-tnpr (degr1 tnpr1 degr2 abar2) tnpr - (declare (ignore degr1 abar2)) - (and (zerop degr2) (zerop (degr2 tnpr1)))))) - list)))))) + (with-cmbn + (degr list) cmbn + (make-cmbn + :degr degr + :list (mapcar + #'(lambda (term) + (declare (type term term)) + (with-term + (cffc tnpr) term + (term cffc (gnrt1 (gnrt1 tnpr))))) + (member-if + #'(lambda (term) + (declare (type term term)) + (with-term + (cffc tnpr) term + (declare (ignore cffc)) + (with-tnpr + (degr1 tnpr1 degr2 abar2) tnpr + (declare (ignore degr1 abar2)) + (and (zerop degr2) (zerop (degr2 tnpr1)))))) + list)))))) -#| -(cs-pre-left-hmeq-left-reduction-intr-f - (cmbn 6 100 (tnpr 4 (tnpr 2 'a 2 'b) 2 'c) - 10 (tnpr 6 (tnpr 2 'a 4 'b) 0 'c) - 50 (tnpr 6 (tnpr 6 'a 0 'b) 0 'c) - 1 (tnpr 6 (tnpr 6 'aa 0 'b) 0 'c))) -|# (DEFUN CS-PRE-LEFT-HMEQ-LEFT-REDUCTION-F (smgr &aux (hat-u-t (cs-hat-u-t smgr)) @@ -305,28 +195,27 @@ (flet ((rslt (cmbn) (declare (type cmbn cmbn)) (the cmbn - (with-cmbn (degr list) cmbn - (make-cmbn - :degr degr - :list (mapcar - #'(lambda (term) - (declare (type term term)) - (with-term (cffc gbar) term - (term cffc - (tnpr degr - (tnpr degr gbar 0 idnt) - 0 +null-abar+)))) - list)))))) + (with-cmbn + (degr list) cmbn + (make-cmbn + :degr degr + :list (mapcar + #'(lambda (term) + (declare (type term term)) + (with-term + (cffc gbar) term + (term cffc + (tnpr degr + (tnpr degr gbar 0 idnt) + 0 +null-abar+)))) + list)))))) (the intr-mrph #'rslt))) -#| -(setf g (cs-pre-left-hmeq-left-reduction-intr-g '())) -(funcall g (cmbn 3 14 (gbar 3 0 'a 1 'b 0 '()))) -|# (DEFUN CS-PRE-LEFT-HMEQ-LEFT-REDUCTION-G (smgr &aux (hat-u-t (cs-hat-u-t smgr)) - (classifying-space (classifying-space smgr))) + (classifying-space + (classifying-space smgr))) (declare (type simplicial-group smgr) (type chain-complex hat-u-t) @@ -340,39 +229,45 @@ :strt :cmbn :orgn `(cs-pre-left-hmeq-left-reduction-g ,smgr)))) + (DEFUN CS-PRE-LEFT-HMEQ-LEFT-REDUCTION-INTR-H (cmpr idnt) (declare (type gmsm idnt)) (flet ((rslt (cmbn) (declare (type cmbn cmbn)) (the cmbn - (with-cmbn (degr list) cmbn - (do ((rslt (zero-cmbn (1+ degr))) - (mark list (cdr mark))) - ((endp mark) rslt) - (declare - (type cmbn rslt) - (list mark)) - (let ((term (car mark))) - (declare (type term term)) - (with-term (cffc tnpr) term - (with-tnpr (degr1 tnpr1 degr2 abar2) tnpr - (declare (ignore degr1)) - (with-tnpr (degr11 gbar11 degr12 gmsm12) tnpr1 - (unless (zerop degr12) - (dstr-add-term-to-cmbn - cmpr - (if (evenp degr11) cffc (- cffc)) - (tnpr degr11 - (tnpr degr11 gbar11 0 idnt) - (+ 1 degr12 degr2) - (make-abar - :list - (cons (brgn (1+ degr12) - gmsm12) - (abar-list abar2)))) - rslt))))))))))) + (with-cmbn + (degr list) cmbn + (do ((rslt (zero-cmbn (1+ degr))) + (mark list (cdr mark))) + ((endp mark) rslt) + (declare + (type cmbn rslt) + (list mark)) + (let ((term (car mark))) + (declare (type term term)) + (with-term + (cffc tnpr) term + (with-tnpr + (degr1 tnpr1 degr2 abar2) tnpr + (declare (ignore degr1)) + (with-tnpr + (degr11 gbar11 degr12 gmsm12) tnpr1 + (unless (zerop degr12) + (dstr-add-term-to-cmbn + cmpr + (if (evenp degr11) cffc (- cffc)) + (tnpr degr11 + (tnpr degr11 gbar11 0 idnt) + (+ 1 degr12 degr2) + (make-abar + :list + (cons (brgn (1+ degr12) + gmsm12) + (abar-list abar2)))) + rslt))))))))))) (the intr-mrph #'rslt))) + (DEFUN CS-PRE-LEFT-HMEQ-LEFT-REDUCTION-H (smgr &aux (hat-u-t (cs-hat-u-t smgr))) (declare @@ -383,12 +278,12 @@ :sorc hat-u-t :trgt hat-u-t :degr +1 - :intr (cs-pre-left-hmeq-left-reduction-intr-h (cmpr hat-u-t) (bspn smgr)) + :intr (cs-pre-left-hmeq-left-reduction-intr-h (cmpr hat-u-t) + (bspn smgr)) :strt :cmbn :orgn `(cs-pre-left-hmeq-left-reduction-h ,smgr)))) - (DEFUN CS-PRE-LEFT-HMEQ-LEFT-REDUCTION (smgr) (declare (type simplicial-group smgr)) (the reduction @@ -398,74 +293,11 @@ :h (cs-pre-left-hmeq-left-reduction-h smgr) :orgn `(cs-pre-left-hmeq-left-reduction ,smgr)))) -#| -(cat-init) -(defun random-abar (tot-degr~ max-degr) - (do ((rslt nil) - (cum-degr 0 (+ cum-degr degr 1)) - (degr)) - ((>= cum-degr tot-degr~) (make-abar :list rslt)) - (setf degr (1+ (random max-degr))) - (push (brgn (1+ degr) - (let ((list (make-list degr))) - (mapl - #'(lambda (sublist) - (setf (car sublist) (- (random 21) 10))) - list) - list)) - rslt))) -(setf rdct (cs-pre-left-hmeq-left-reduction (k-z-1))) -(pre-check-rdct rdct) -(setf *tc* (cmbn 0 1 (tnpr 0 (tnpr 0 +null-gbar+ 0 '()) 0 +null-abar+)) - *bc* (cmbn 0 1 +null-gbar+)) -(check-rdct) -(setf *tc* (cmbn 1 1 (tnpr 1 (tnpr 0 +null-gbar+ 1 '(13)) 0 +null-abar+))) -(check-rdct) -(dotimes (i 10) - (let ((abar (random-abar 8 4))) - (setf abar-degr (apply #'+ (mapcar #'car (abar-list abar)))) - (setf gnrt (tnpr 5 (tnpr 3 (gbar 3 0 '(1 2) 0 '(3) 0 '()) 2 '(4 5)) - abar-degr abar)) - (setf gbar (gbar 2 0 '(1) 0 '())) - (unless (>= abar-degr 9) - (setf *tc* (cmbn (+ 5 abar-degr) 1 gnrt) - *bc* (cmbn 2 1 gbar)) - (check-rdct)))) -(dotimes (i 10) - (let ((abar (random-abar 6 4))) - (setf abar-degr (apply #'+ (mapcar #'car (abar-list abar)))) - (setf gnrt (tnpr 6 (tnpr 3 (gbar 3 0 '(1 2) 0 '(3) 0 '()) 3 '(4 5 6)) - abar-degr abar)) - (setf gbar (gbar 3 0 '(1 2) 1 '() 0 '())) - (unless (>= abar-degr 8) - (setf *tc* (cmbn (+ 6 abar-degr) 1 gnrt) - *bc* (cmbn 3 1 gbar)) - (check-rdct)))) -(dotimes (i 10) - (let ((abar (random-abar 6 4))) - (setf abar-degr (apply #'+ (mapcar #'car (abar-list abar)))) - (setf gnrt (tnpr 5 (tnpr 2 (gbar 2 0 '(3) 0 '()) 3 '(4 5 6)) - abar-degr abar)) - (setf gbar (gbar 4 0 '(1 2 3) 0 '(4 5) 0 '(6) 0 '())) - (unless (>= abar-degr 9) - (setf *tc* (cmbn (+ 5 abar-degr) 1 gnrt)) - (setf *bc* (cmbn 4 1 gbar)) - (check-rdct)))) -(dotimes (i 10) - (let ((abar (random-abar 6 4))) - (setf abar-degr (apply #'+ (mapcar #'car (abar-list abar)))) - (setf gnrt (tnpr 4 (tnpr 2 (gbar 2 0 '(3) 0 '()) 2 '(4 5)) - abar-degr abar)) - (setf gbar (gbar 5 8 '(1 2 3) 0 '(4 5 6) 0 '(7 8) 0 '(9) 0 '())) - (unless (>= abar-degr 10) - (setf *tc* (cmbn (+ 4 abar-degr) 1 gnrt)) - (setf *bc* (cmbn 5 1 gbar)) - (check-rdct)))) -|# (DEFUN CS-LEFT-HMEQ-LEFT-REDUCTION (smgr &aux (pre-left-hmeq-left-reduction - (cs-pre-left-hmeq-left-reduction smgr)) + (cs-pre-left-hmeq-left-reduction + smgr)) (hat-left-perturbation (cs-hat-left-perturbation smgr))) (declare @@ -489,71 +321,6 @@ rslt)))) -#| -(cat-init) -(defun random-abar (tot-degr~ max-degr) - (do ((rslt nil) - (cum-degr 0 (+ cum-degr degr 1)) - (degr)) - ((>= cum-degr tot-degr~) (make-abar :list rslt)) - (setf degr (1+ (random max-degr))) - (push (brgn (1+ degr) - (let ((list (make-list degr))) - (mapl - #'(lambda (sublist) - (setf (car sublist) (- (random 21) 10))) - list) - list)) - rslt))) -(setf rdct (cs-left-hmeq-left-reduction (k-z-1))) -(pre-check-rdct rdct) -(setf *tc* (cmbn 0 1 (tnpr 0 (tnpr 0 +null-gbar+ 0 '()) 0 +null-abar+)) - *bc* (cmbn 0 1 +null-gbar+)) -(check-rdct) -(setf *tc* (cmbn 1 1 (tnpr 1 (tnpr 0 +null-gbar+ 1 '(13)) 0 +null-abar+))) -(check-rdct) -(dotimes (i 10) - (let ((abar (random-abar 8 4))) - (setf abar-degr (apply #'+ (mapcar #'car (abar-list abar)))) - (setf gnrt (tnpr 5 (tnpr 3 (gbar 3 0 '(1 2) 0 '(3) 0 '()) 2 '(4 5)) - abar-degr abar)) - (setf gbar (gbar 2 0 '(1) 0 '())) - (unless (>= abar-degr 9) - (setf *tc* (cmbn (+ 5 abar-degr) 1 gnrt) - *bc* (cmbn 2 1 gbar)) - (check-rdct)))) -(dotimes (i 10) - (let ((abar (random-abar 6 4))) - (setf abar-degr (apply #'+ (mapcar #'car (abar-list abar)))) - (setf gnrt (tnpr 6 (tnpr 3 (gbar 3 0 '(1 2) 0 '(3) 0 '()) 3 '(4 5 6)) - abar-degr abar)) - (setf gbar (gbar 3 0 '(1 2) 1 '() 0 '())) - (unless (>= abar-degr 8) - (setf *tc* (cmbn (+ 6 abar-degr) 1 gnrt) - *bc* (cmbn 3 1 gbar)) - (check-rdct)))) -(dotimes (i 10) - (let ((abar (random-abar 6 4))) - (setf abar-degr (apply #'+ (mapcar #'car (abar-list abar)))) - (setf gnrt (tnpr 5 (tnpr 2 (gbar 2 0 '(3) 0 '()) 3 '(4 5 6)) - abar-degr abar)) - (setf gbar (gbar 4 0 '(1 2 3) 0 '(4 5) 0 '(6) 0 '())) - (unless (>= abar-degr 9) - (setf *tc* (cmbn (+ 5 abar-degr) 1 gnrt)) - (setf *bc* (cmbn 4 1 gbar)) - (check-rdct)))) -(dotimes (i 10) - (let ((abar (random-abar 6 4))) - (setf abar-degr (apply #'+ (mapcar #'car (abar-list abar)))) - (setf gnrt (tnpr 4 (tnpr 2 (gbar 2 0 '(3) 0 '()) 2 '(4 5)) - abar-degr abar)) - (setf gbar (gbar 5 8 '(1 2 3) 0 '(4 5 6) 0 '(7 8) 0 '(9) 0 '())) - (unless (>= abar-degr 10) - (setf *tc* (cmbn (+ 4 abar-degr) 1 gnrt)) - (setf *bc* (cmbn 5 1 gbar)) - (check-rdct)))) -|# - (DEFUN CS-PRE-LEFT-HMEQ-RIGHT-REDUCTION-INTR-F (cmbn) (declare (type cmbn cmbn)) (the cmbn @@ -571,15 +338,6 @@ (make-cmbn :degr degr :list (nreverse rslt)))))) -#| -(cs-pre-left-hmeq-right-reduction-intr-f - (cmbn 4 2 (tnpr 0 (tnpr 0 +null-gbar+ 0 'i) - 4 (abar 2 'a 2 'b)) - 3 (tnpr 0 (tnpr 0 +null-gbar+ 0 'i) - 4 (abar 2 'a 2 'c)) - 5 (tnpr 1 (tnpr 0 +null-gbar+ 1 'a) - 3 (abar 1 'a 2 'b)))) -|# (DEFUN CS-PRE-LEFT-HMEQ-RIGHT-REDUCTION-F (smgr &aux (hat-t-u (cs-hat-t-u smgr)) @@ -594,29 +352,28 @@ :strt :cmbn :orgn `(cs-pre-left-hmeq-right-reduction-f ,smgr)))) + (DEFUN CS-PRE-LEFT-HMEQ-RIGHT-REDUCTION-INTR-G (idnt) (declare (type gmsm idnt)) (flet ((rslt (cmbn) (declare (type cmbn cmbn)) (the cmbn - (with-cmbn (degr list) cmbn - (let ((bsgn (tnpr 0 +null-gbar+ 0 idnt))) - (declare (type tnpr bsgn)) - (make-cmbn :degr degr - :list (mapcar - #'(lambda (term) - (declare (type term term)) - (with-term (cffc abar) term - (term cffc - (tnpr 0 bsgn - degr abar)))) - list))))))) + (with-cmbn + (degr list) cmbn + (let ((bsgn (tnpr 0 +null-gbar+ 0 idnt))) + (declare (type tnpr bsgn)) + (make-cmbn :degr degr + :list (mapcar + #'(lambda (term) + (declare (type term term)) + (with-term + (cffc abar) term + (term cffc + (tnpr 0 bsgn + degr abar)))) + list))))))) (the intr-mrph #'rslt))) -#| -(setf g (cs-pre-left-hmeq-right-reduction-intr-g 'i)) -(funcall g (cmbn 3 2 (abar 1 'a 2 'b))) -|# (DEFUN CS-PRE-LEFT-HMEQ-RIGHT-REDUCTION-G (smgr &aux (hat-t-u (cs-hat-t-u smgr)) diff --git a/test/cl-space-efhm-test.lisp b/test/cl-space-efhm-test.lisp index 857e782..33f58d2 100644 --- a/test/cl-space-efhm-test.lisp +++ b/test/cl-space-efhm-test.lisp @@ -3,7 +3,6 @@ (in-suite :kenzo) - (test cs-hat-u-t (cat:cat-init) (let* ((c (cat:cs-hat-u-t (cat:k-z-1))) @@ -13,7 +12,7 @@ 2 '(4 5)) abar-degr abar))) (cat:? c (+ 5 abar-degr) gnrt) - (cat:? c (cat:? c (+ 5 abar-degr) gnrt)) + (is (cat:cmbn-zero-p (cat:? c (cat:? c (+ 5 abar-degr) gnrt)))) (dotimes (i 10) (let ((abar (random-abar 8 4))) (setf abar-degr (apply #'+ (mapcar #'car (cat:abar-list abar)))) @@ -22,7 +21,8 @@ abar-degr abar)) (unless (>= abar-degr 10) (print (cat:? c (+ 5 abar-degr) gnrt)) - (print (cat:? c (cat:? c (+ 5 abar-degr) gnrt)))))) + (is (cat:cmbn-zero-p (cat:? c (cat:? c (+ 5 abar-degr) + gnrt))))))) (dotimes (i 10) (let ((abar (random-abar 8 4))) (setf abar-degr (apply #'+ (mapcar #'car (cat:abar-list abar)))) @@ -31,7 +31,8 @@ abar-degr abar)) (unless (>= abar-degr 9) (print (cat:? c (+ 6 abar-degr) gnrt)) - (print (cat:? c (cat:? c (+ 6 abar-degr) gnrt)))))) + (is (cat:cmbn-zero-p (cat:? c (cat:? c (+ 6 abar-degr) + gnrt))))))) (dotimes (i 10) (let ((abar (random-abar 8 4))) (setf abar-degr (apply #'+ (mapcar #'car (cat:abar-list abar)))) @@ -39,7 +40,8 @@ 3 '(4 5 6)) abar-degr abar)) (unless (>= abar-degr 10) (print (cat:? c (+ 5 abar-degr) gnrt)) - (print (cat:? c (cat:? c (+ 5 abar-degr) gnrt)))))) + (is (cat:cmbn-zero-p (cat:? c (cat:? c (+ 5 abar-degr) + gnrt))))))) (dotimes (i 10) (let ((abar (random-abar 8 4))) (setf abar-degr (apply #'+ (mapcar #'car (cat:abar-list abar)))) @@ -48,7 +50,8 @@ abar-degr abar)) (unless (>= abar-degr 11) (print (cat:? c (+ 4 abar-degr) gnrt)) - (print (cat:? c (cat:? c (+ 4 abar-degr) gnrt)))))))) + (is (cat:cmbn-zero-p (cat:? c (cat:? c (+ 4 abar-degr) + gnrt))))))))) (test cs-hat-t-u @@ -61,7 +64,7 @@ 2 '(4 5)) abar-degr abar))) (cat:? c (+ 5 abar-degr) gnrt) - (cat:? c (cat:? c (+ 5 abar-degr) gnrt)) + (is (cat:cmbn-zero-p (cat:? c (cat:? c (+ 5 abar-degr) gnrt)))) (dotimes (i 10) (let ((abar (random-abar 8 4))) (setf abar-degr (apply #'+ (mapcar #'car (cat:abar-list abar)))) @@ -70,7 +73,8 @@ abar-degr abar)) (unless (>= abar-degr 10) (print (cat:? c (+ 5 abar-degr) gnrt)) - (print (cat:? c (cat:? c (+ 5 abar-degr) gnrt)))))) + (is (cat:cmbn-zero-p (cat:? c (cat:? c (+ 5 abar-degr) + gnrt))))))) (dotimes (i 10) (let ((abar (random-abar 8 4))) (setf abar-degr (apply #'+ (mapcar #'car (cat:abar-list abar)))) @@ -79,7 +83,8 @@ abar-degr abar)) (unless (>= abar-degr 9) (print (cat:? c (+ 6 abar-degr) gnrt)) - (print (cat:? c (cat:? c (+ 6 abar-degr) gnrt)))))) + (is (cat:cmbn-zero-p (cat:? c (cat:? c (+ 6 abar-degr) + gnrt))))))) (dotimes (i 10) (let ((abar (random-abar 8 4))) (setf abar-degr (apply #'+ (mapcar #'car (cat:abar-list abar)))) @@ -88,7 +93,8 @@ abar-degr abar)) (unless (>= abar-degr 10) (print (cat:? c (+ 5 abar-degr) gnrt)) - (print (cat:? c (cat:? c (+ 5 abar-degr) gnrt)))))) + (is (cat:cmbn-zero-p (cat:? c (cat:? c (+ 5 abar-degr) + gnrt))))))) (dotimes (i 10) (let ((abar (random-abar 8 4))) (setf abar-degr (apply #'+ (mapcar #'car (cat:abar-list abar)))) @@ -97,4 +103,208 @@ abar-degr abar)) (unless (>= abar-degr 11) (print (cat:? c (+ 4 abar-degr) gnrt)) - (print (cat:? c (cat:? c (+ 4 abar-degr) gnrt)))))))) + (is (cat:cmbn-zero-p (cat:? c (cat:? c (+ 4 abar-degr) + gnrt))))))))) + + +(test cs-left-hmeq-hat + (cat:cat-init) + (let ((c (cat:cs-left-hmeq-hat (cat:k-z-1))) + abar-degr + gnrt) + (dotimes (i 10) + (let ((abar (random-abar 8 4))) + (setf abar-degr (apply #'+ (mapcar #'car (cat:abar-list abar)))) + (setf gnrt (cat:tnpr 5 (cat:tnpr 3 (cat:gbar 3 0 '(1 2) 0 '(3) + 0 '()) 2 '(4 5)) + abar-degr abar)) + (unless (>= abar-degr 10) + (print (cat:? c (+ 5 abar-degr) gnrt)) + (is (cat:cmbn-zero-p (cat:? c (cat:? c (+ 5 abar-degr) + gnrt))))))) + (dotimes (i 10) + (let ((abar (random-abar 8 4))) + (setf abar-degr (apply #'+ (mapcar #'car (cat:abar-list abar)))) + (setf gnrt (cat:tnpr 6 (cat:tnpr 3 (cat:gbar 3 0 '(1 2) 0 '(3) + 0 '()) 3 '(4 5 6)) + abar-degr abar)) + (unless (>= abar-degr 9) + (print (cat:? c (+ 6 abar-degr) gnrt)) + (is (cat:cmbn-zero-p (cat:? c (cat:? c (+ 6 abar-degr) + gnrt))))))) + (dotimes (i 10) + (let ((abar (random-abar 8 4))) + (setf abar-degr (apply #'+ (mapcar #'car (cat:abar-list abar)))) + (setf gnrt (cat:tnpr 5 (cat:tnpr 2 (cat:gbar 2 0 '(3) 0 '()) + 3 '(4 5 6)) + abar-degr abar)) + (unless (>= abar-degr 10) + (print (cat:? c (+ 5 abar-degr) gnrt)) + (is (cat:cmbn-zero-p (cat:? c (cat:? c (+ 5 abar-degr) + gnrt))))))) + (dotimes (i 10) + (let ((abar (random-abar 8 4))) + (setf abar-degr (apply #'+ (mapcar #'car (cat:abar-list abar)))) + (setf gnrt (cat:tnpr 4 (cat:tnpr 2 (cat:gbar 2 0 '(3) 0 '()) + 2 '(4 5)) + abar-degr abar)) + (unless (>= abar-degr 11) + (print (cat:? c (+ 4 abar-degr) gnrt)) + (is (cat:cmbn-zero-p (cat:? c (cat:? c (+ 4 abar-degr) + 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 + (cat:cat-init) + (let ((rdct (cat:cs-pre-left-hmeq-left-reduction (cat:k-z-1))) + abar-degr + gnrt + gbar) + (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) + (let ((abar (random-abar 8 4))) + (setf abar-degr (apply #'+ (mapcar #'car (cat:abar-list abar)))) + (setf gnrt (cat:tnpr 5 (cat:tnpr 3 (cat:gbar 3 0 '(1 2) 0 '(3) + 0 '()) 2 '(4 5)) + abar-degr abar)) + (setf gbar (cat:gbar 2 0 '(1) 0 '())) + (unless (>= abar-degr 9) + (setf cat:*tc* (cat:cmbn (+ 5 abar-degr) 1 gnrt) + cat:*bc* (cat:cmbn 2 1 gbar)) + (check-rdct)))) + (dotimes (i 10) + (let ((abar (random-abar 6 4))) + (setf abar-degr (apply #'+ (mapcar #'car (cat:abar-list abar)))) + (setf gnrt (cat:tnpr 6 (cat:tnpr 3 (cat:gbar 3 0 '(1 2) 0 '(3) + 0 '()) 3 '(4 5 6)) + abar-degr abar)) + (setf gbar (cat:gbar 3 0 '(1 2) 1 '() 0 '())) + (unless (>= abar-degr 8) + (setf cat:*tc* (cat:cmbn (+ 6 abar-degr) 1 gnrt) + cat:*bc* (cat:cmbn 3 1 gbar)) + (check-rdct)))) + (dotimes (i 10) + (let ((abar (random-abar 6 4))) + (setf abar-degr (apply #'+ (mapcar #'car (cat:abar-list abar)))) + (setf gnrt (cat:tnpr 5 (cat:tnpr 2 (cat:gbar 2 0 '(3) 0 '()) + 3 '(4 5 6)) + abar-degr abar)) + (setf gbar (cat:gbar 4 0 '(1 2 3) 0 '(4 5) 0 '(6) 0 '())) + (unless (>= abar-degr 9) + (setf cat:*tc* (cat:cmbn (+ 5 abar-degr) 1 gnrt)) + (setf cat:*bc* (cat:cmbn 4 1 gbar)) + (check-rdct)))) + (dotimes (i 10) + (let ((abar (random-abar 6 4))) + (setf abar-degr (apply #'+ (mapcar #'car (cat:abar-list abar)))) + (setf gnrt (cat:tnpr 4 (cat:tnpr 2 (cat:gbar 2 0 '(3) 0 '()) + 2 '(4 5)) + abar-degr abar)) + (setf gbar (cat:gbar 5 8 '(1 2 3) 0 '(4 5 6) 0 '(7 8) 0 '(9) + 0 '())) + (unless (>= abar-degr 10) + (setf cat:*tc* (cat:cmbn (+ 4 abar-degr) 1 gnrt)) + (setf cat:*bc* (cat:cmbn 5 1 gbar)) + (check-rdct)))))) + + +(test cs-left-hmeq-left-reduction + (cat:cat-init) + (let ((rdct (cat:cs-left-hmeq-left-reduction (cat:k-z-1))) + abar-degr gnrt gbar) + (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) + (let ((abar (random-abar 8 4))) + (setf abar-degr (apply #'+ (mapcar #'car (cat:abar-list abar)))) + (setf gnrt (cat:tnpr 5 (cat:tnpr 3 (cat:gbar 3 0 '(1 2) 0 '(3) + 0 '()) 2 '(4 5)) + abar-degr abar)) + (setf gbar (cat:gbar 2 0 '(1) 0 '())) + (unless (>= abar-degr 9) + (setf cat:*tc* (cat:cmbn (+ 5 abar-degr) 1 gnrt) + cat:*bc* (cat:cmbn 2 1 gbar)) + (check-rdct)))) + (dotimes (i 10) + (let ((abar (random-abar 6 4))) + (setf abar-degr (apply #'+ (mapcar #'car (cat:abar-list abar)))) + (setf gnrt (cat:tnpr 6 (cat:tnpr 3 (cat:gbar 3 0 '(1 2) 0 '(3) + 0 '()) 3 '(4 5 6)) + abar-degr abar)) + (setf gbar (cat:gbar 3 0 '(1 2) 1 '() 0 '())) + (unless (>= abar-degr 8) + (setf cat:*tc* (cat:cmbn (+ 6 abar-degr) 1 gnrt) + cat:*bc* (cat:cmbn 3 1 gbar)) + (check-rdct)))) + (dotimes (i 10) + (let ((abar (random-abar 6 4))) + (setf abar-degr (apply #'+ (mapcar #'car (cat:abar-list abar)))) + (setf gnrt (cat:tnpr 5 (cat:tnpr 2 (cat:gbar 2 0 '(3) 0 '()) + 3 '(4 5 6)) + abar-degr abar)) + (setf gbar (cat:gbar 4 0 '(1 2 3) 0 '(4 5) 0 '(6) 0 '())) + (unless (>= abar-degr 9) + (setf cat:*tc* (cat:cmbn (+ 5 abar-degr) 1 gnrt)) + (setf cat:*bc* (cat:cmbn 4 1 gbar)) + (check-rdct)))) + (dotimes (i 10) + (let ((abar (random-abar 6 4))) + (setf abar-degr (apply #'+ (mapcar #'car (cat:abar-list abar)))) + (setf gnrt (cat:tnpr 4 (cat:tnpr 2 (cat:gbar 2 0 '(3) 0 '()) + 2 '(4 5)) + abar-degr abar)) + (setf gbar (cat:gbar 5 8 '(1 2 3) 0 '(4 5 6) 0 '(7 8) 0 '(9) + 0 '())) + (unless (>= abar-degr 10) + (setf cat:*tc* (cat:cmbn (+ 4 abar-degr) 1 gnrt)) + (setf cat:*bc* (cat:cmbn 5 1 gbar)) + (check-rdct)))))) + + +(test cs-pre-left-hmeq-right-reduction-intr-f + (cat:cs-pre-left-hmeq-right-reduction-intr-f + (cat:cmbn 4 2 (cat:tnpr 0 (cat:tnpr 0 cat:+null-gbar+ 0 'i) + 4 (cat:abar 2 'a 2 'b)) + 3 (cat:tnpr 0 (cat:tnpr 0 cat:+null-gbar+ 0 'i) + 4 (cat:abar 2 'a 2 'c)) + 5 (cat:tnpr 1 (cat:tnpr 0 cat:+null-gbar+ 1 'a) + 3 (cat:abar 1 'a 2 'b))))) + + +(test cs-pre-left-hmeq-right-reduction-g + (let ((g (cat:cs-pre-left-hmeq-right-reduction-intr-g 'i))) + (funcall g (cat:cmbn 3 2 (cat:abar 1 'a 2 'b)))))