Another batch of CL-SPACE-EFHM tests extracted.

This commit is contained in:
Gerd Heber 2015-07-20 20:13:04 -05:00
parent ed51e2b993
commit 3d6c2812b9
5 changed files with 322 additions and 346 deletions

View File

@ -1,6 +1,6 @@
(defsystem :kenzo-test (defsystem :kenzo-test
:description "A simple test suite for Kenzo" :description "A simple regression test suite for Kenzo"
:serial t :serial t
:version "0.1.0" :version "0.1.0"
:author "Francis Sergeraert <Francis.Sergeraert@ujf-grenoble.fr>" :author "Francis Sergeraert <Francis.Sergeraert@ujf-grenoble.fr>"
@ -17,9 +17,9 @@
(:file "chain-complexes-test") (:file "chain-complexes-test")
(:file "chcm-elementary-op-test") (:file "chcm-elementary-op-test")
(:file "circle") (:file "circle")
(:file "cl-space-efhm-test")
(:file "combinations-test") (:file "combinations-test")
(:file "cones-test") (:file "cones-test")
(:file "cl-space-efhm-test")
(:file "delta-test") (:file "delta-test")
(:file "diabolo") (:file "diabolo")
(:file "effective-homology-test") (:file "effective-homology-test")

View File

@ -29,6 +29,7 @@
;; bar.lisp ;; bar.lisp
+NULL-ABAR+
ABAR ABAR
BAR BAR
BAR-BASIS-LENGTH BAR-BASIS-LENGTH
@ -97,6 +98,13 @@
CS-HAT-T-U CS-HAT-T-U
CS-HAT-U-T 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 ;; classes.lisp
@ -136,6 +144,7 @@
;; classifying-space.lisp ;; classifying-space.lisp
+NULL-GBAR+
CLASSIFYING-SPACE CLASSIFYING-SPACE
;; combinations.lisp ;; combinations.lisp

View File

@ -1,10 +1,10 @@
(DECLAIM (OPTIMIZE (speed 0) (space 0) (debug 3))) (DECLAIM (OPTIMIZE (speed 3) (space 0) (debug 3)))
(require 'asdf) (require 'asdf)
(asdf:operate 'asdf:load-op 'kenzo-test) (asdf:operate 'asdf:load-op 'kenzo-test)
(fiveam:run!) (fiveam:run!)
#+ccl(quit) #+(or ecl ccl) (quit)
#+sbcl(sb-ext:exit) #+sbcl(sb-ext:exit)

View File

@ -135,63 +135,6 @@
(setf (slot-value rslt 'grmd) hat-u-u) (setf (slot-value rslt 'grmd) hat-u-u)
rslt))) 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 (DEFUN CS-LEFT-HMEQ-HAT (smgr
&aux (hat-t-u (cs-hat-t-u smgr)) &aux (hat-t-u (cs-hat-t-u smgr))
@ -204,85 +147,32 @@
(the chain-complex (the chain-complex
(add hat-t-u hat-right-perturbation))) (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) (DEFUN CS-PRE-LEFT-HMEQ-LEFT-REDUCTION-INTR-F (cmbn)
(declare (type cmbn cmbn)) (declare (type cmbn cmbn))
(the cmbn (the cmbn
(with-cmbn (degr list) cmbn (with-cmbn
(make-cmbn (degr list) cmbn
:degr degr (make-cmbn
:list (mapcar :degr degr
#'(lambda (term) :list (mapcar
(declare (type term term)) #'(lambda (term)
(with-term (cffc tnpr) term (declare (type term term))
(term cffc (gnrt1 (gnrt1 tnpr))))) (with-term
(member-if (cffc tnpr) term
#'(lambda (term) (term cffc (gnrt1 (gnrt1 tnpr)))))
(declare (type term term)) (member-if
(with-term (cffc tnpr) term #'(lambda (term)
(declare (ignore cffc)) (declare (type term term))
(with-tnpr (degr1 tnpr1 degr2 abar2) tnpr (with-term
(declare (ignore degr1 abar2)) (cffc tnpr) term
(and (zerop degr2) (zerop (degr2 tnpr1)))))) (declare (ignore cffc))
list)))))) (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 (DEFUN CS-PRE-LEFT-HMEQ-LEFT-REDUCTION-F (smgr
&aux (hat-u-t (cs-hat-u-t smgr)) &aux (hat-u-t (cs-hat-u-t smgr))
@ -305,28 +195,27 @@
(flet ((rslt (cmbn) (flet ((rslt (cmbn)
(declare (type cmbn cmbn)) (declare (type cmbn cmbn))
(the cmbn (the cmbn
(with-cmbn (degr list) cmbn (with-cmbn
(make-cmbn (degr list) cmbn
:degr degr (make-cmbn
:list (mapcar :degr degr
#'(lambda (term) :list (mapcar
(declare (type term term)) #'(lambda (term)
(with-term (cffc gbar) term (declare (type term term))
(term cffc (with-term
(tnpr degr (cffc gbar) term
(tnpr degr gbar 0 idnt) (term cffc
0 +null-abar+)))) (tnpr degr
list)))))) (tnpr degr gbar 0 idnt)
0 +null-abar+))))
list))))))
(the intr-mrph #'rslt))) (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 (DEFUN CS-PRE-LEFT-HMEQ-LEFT-REDUCTION-G (smgr
&aux (hat-u-t (cs-hat-u-t smgr)) &aux (hat-u-t (cs-hat-u-t smgr))
(classifying-space (classifying-space smgr))) (classifying-space
(classifying-space smgr)))
(declare (declare
(type simplicial-group smgr) (type simplicial-group smgr)
(type chain-complex hat-u-t) (type chain-complex hat-u-t)
@ -340,39 +229,45 @@
:strt :cmbn :strt :cmbn
:orgn `(cs-pre-left-hmeq-left-reduction-g ,smgr)))) :orgn `(cs-pre-left-hmeq-left-reduction-g ,smgr))))
(DEFUN CS-PRE-LEFT-HMEQ-LEFT-REDUCTION-INTR-H (cmpr idnt) (DEFUN CS-PRE-LEFT-HMEQ-LEFT-REDUCTION-INTR-H (cmpr idnt)
(declare (type gmsm idnt)) (declare (type gmsm idnt))
(flet ((rslt (cmbn) (flet ((rslt (cmbn)
(declare (type cmbn cmbn)) (declare (type cmbn cmbn))
(the cmbn (the cmbn
(with-cmbn (degr list) cmbn (with-cmbn
(do ((rslt (zero-cmbn (1+ degr))) (degr list) cmbn
(mark list (cdr mark))) (do ((rslt (zero-cmbn (1+ degr)))
((endp mark) rslt) (mark list (cdr mark)))
(declare ((endp mark) rslt)
(type cmbn rslt) (declare
(list mark)) (type cmbn rslt)
(let ((term (car mark))) (list mark))
(declare (type term term)) (let ((term (car mark)))
(with-term (cffc tnpr) term (declare (type term term))
(with-tnpr (degr1 tnpr1 degr2 abar2) tnpr (with-term
(declare (ignore degr1)) (cffc tnpr) term
(with-tnpr (degr11 gbar11 degr12 gmsm12) tnpr1 (with-tnpr
(unless (zerop degr12) (degr1 tnpr1 degr2 abar2) tnpr
(dstr-add-term-to-cmbn (declare (ignore degr1))
cmpr (with-tnpr
(if (evenp degr11) cffc (- cffc)) (degr11 gbar11 degr12 gmsm12) tnpr1
(tnpr degr11 (unless (zerop degr12)
(tnpr degr11 gbar11 0 idnt) (dstr-add-term-to-cmbn
(+ 1 degr12 degr2) cmpr
(make-abar (if (evenp degr11) cffc (- cffc))
:list (tnpr degr11
(cons (brgn (1+ degr12) (tnpr degr11 gbar11 0 idnt)
gmsm12) (+ 1 degr12 degr2)
(abar-list abar2)))) (make-abar
rslt))))))))))) :list
(cons (brgn (1+ degr12)
gmsm12)
(abar-list abar2))))
rslt)))))))))))
(the intr-mrph #'rslt))) (the intr-mrph #'rslt)))
(DEFUN CS-PRE-LEFT-HMEQ-LEFT-REDUCTION-H (smgr (DEFUN CS-PRE-LEFT-HMEQ-LEFT-REDUCTION-H (smgr
&aux (hat-u-t (cs-hat-u-t smgr))) &aux (hat-u-t (cs-hat-u-t smgr)))
(declare (declare
@ -383,12 +278,12 @@
:sorc hat-u-t :sorc hat-u-t
:trgt hat-u-t :trgt hat-u-t
:degr +1 :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 :strt :cmbn
:orgn `(cs-pre-left-hmeq-left-reduction-h ,smgr)))) :orgn `(cs-pre-left-hmeq-left-reduction-h ,smgr))))
(DEFUN CS-PRE-LEFT-HMEQ-LEFT-REDUCTION (smgr) (DEFUN CS-PRE-LEFT-HMEQ-LEFT-REDUCTION (smgr)
(declare (type simplicial-group smgr)) (declare (type simplicial-group smgr))
(the reduction (the reduction
@ -398,74 +293,11 @@
:h (cs-pre-left-hmeq-left-reduction-h smgr) :h (cs-pre-left-hmeq-left-reduction-h smgr)
:orgn `(cs-pre-left-hmeq-left-reduction ,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 (DEFUN CS-LEFT-HMEQ-LEFT-REDUCTION (smgr
&aux (pre-left-hmeq-left-reduction &aux (pre-left-hmeq-left-reduction
(cs-pre-left-hmeq-left-reduction smgr)) (cs-pre-left-hmeq-left-reduction
smgr))
(hat-left-perturbation (hat-left-perturbation
(cs-hat-left-perturbation smgr))) (cs-hat-left-perturbation smgr)))
(declare (declare
@ -489,71 +321,6 @@
rslt)))) 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) (DEFUN CS-PRE-LEFT-HMEQ-RIGHT-REDUCTION-INTR-F (cmbn)
(declare (type cmbn cmbn)) (declare (type cmbn cmbn))
(the cmbn (the cmbn
@ -571,15 +338,6 @@
(make-cmbn :degr degr (make-cmbn :degr degr
:list (nreverse rslt)))))) :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 (DEFUN CS-PRE-LEFT-HMEQ-RIGHT-REDUCTION-F (smgr
&aux (hat-t-u (cs-hat-t-u smgr)) &aux (hat-t-u (cs-hat-t-u smgr))
@ -594,29 +352,28 @@
:strt :cmbn :strt :cmbn
:orgn `(cs-pre-left-hmeq-right-reduction-f ,smgr)))) :orgn `(cs-pre-left-hmeq-right-reduction-f ,smgr))))
(DEFUN CS-PRE-LEFT-HMEQ-RIGHT-REDUCTION-INTR-G (idnt) (DEFUN CS-PRE-LEFT-HMEQ-RIGHT-REDUCTION-INTR-G (idnt)
(declare (type gmsm idnt)) (declare (type gmsm idnt))
(flet ((rslt (cmbn) (flet ((rslt (cmbn)
(declare (type cmbn cmbn)) (declare (type cmbn cmbn))
(the cmbn (the cmbn
(with-cmbn (degr list) cmbn (with-cmbn
(let ((bsgn (tnpr 0 +null-gbar+ 0 idnt))) (degr list) cmbn
(declare (type tnpr bsgn)) (let ((bsgn (tnpr 0 +null-gbar+ 0 idnt)))
(make-cmbn :degr degr (declare (type tnpr bsgn))
:list (mapcar (make-cmbn :degr degr
#'(lambda (term) :list (mapcar
(declare (type term term)) #'(lambda (term)
(with-term (cffc abar) term (declare (type term term))
(term cffc (with-term
(tnpr 0 bsgn (cffc abar) term
degr abar)))) (term cffc
list))))))) (tnpr 0 bsgn
degr abar))))
list)))))))
(the intr-mrph #'rslt))) (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 (DEFUN CS-PRE-LEFT-HMEQ-RIGHT-REDUCTION-G (smgr
&aux (hat-t-u (cs-hat-t-u smgr)) &aux (hat-t-u (cs-hat-t-u smgr))

View File

@ -3,7 +3,6 @@
(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)))
@ -13,7 +12,7 @@
2 '(4 5)) 2 '(4 5))
abar-degr abar))) abar-degr abar)))
(cat:? c (+ 5 abar-degr) gnrt) (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) (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))))
@ -22,7 +21,8 @@
abar-degr abar)) abar-degr abar))
(unless (>= abar-degr 10) (unless (>= abar-degr 10)
(print (cat:? c (+ 5 abar-degr) gnrt)) (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) (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))))
@ -31,7 +31,8 @@
abar-degr abar)) abar-degr abar))
(unless (>= abar-degr 9) (unless (>= abar-degr 9)
(print (cat:? c (+ 6 abar-degr) gnrt)) (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) (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))))
@ -39,7 +40,8 @@
3 '(4 5 6)) abar-degr abar)) 3 '(4 5 6)) abar-degr abar))
(unless (>= abar-degr 10) (unless (>= abar-degr 10)
(print (cat:? c (+ 5 abar-degr) gnrt)) (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) (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))))
@ -48,7 +50,8 @@
abar-degr abar)) abar-degr abar))
(unless (>= abar-degr 11) (unless (>= abar-degr 11)
(print (cat:? c (+ 4 abar-degr) gnrt)) (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 (test cs-hat-t-u
@ -61,7 +64,7 @@
2 '(4 5)) 2 '(4 5))
abar-degr abar))) abar-degr abar)))
(cat:? c (+ 5 abar-degr) gnrt) (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) (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))))
@ -70,7 +73,8 @@
abar-degr abar)) abar-degr abar))
(unless (>= abar-degr 10) (unless (>= abar-degr 10)
(print (cat:? c (+ 5 abar-degr) gnrt)) (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) (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))))
@ -79,7 +83,8 @@
abar-degr abar)) abar-degr abar))
(unless (>= abar-degr 9) (unless (>= abar-degr 9)
(print (cat:? c (+ 6 abar-degr) gnrt)) (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) (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))))
@ -88,7 +93,8 @@
abar-degr abar)) abar-degr abar))
(unless (>= abar-degr 10) (unless (>= abar-degr 10)
(print (cat:? c (+ 5 abar-degr) gnrt)) (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) (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))))
@ -97,4 +103,208 @@
abar-degr abar)) abar-degr abar))
(unless (>= abar-degr 11) (unless (>= abar-degr 11)
(print (cat:? c (+ 4 abar-degr) gnrt)) (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)))))