gheber / kenzo

A repackaged version of the Kenzo program by Francis Sergeraert and collaborators.
https://sur-l-analysis-sit.us/
Other
50 stars 8 forks source link

smith.lisp #104

Closed gheber closed 8 years ago

gheber commented 8 years ago

; in: DEFUN LIST-SMITH ; (PROGN ; (LET ((CAT::MATRIX (THIRD CAT::MTRX-LIST)) (CAT::BEGIN 0)) ; (DECLARE (TYPE CAT::MATRIX CAT::MATRIX) ; (FIXNUM CAT::BEGIN)) ; (LOOP ; (MULTIPLE-VALUE-BIND (CAT::TERM CAT::IL CAT::IC) ; (CAT::MINIMAL-TERM CAT::MATRIX CAT::BEGIN) ; (DECLARE #) ; (WHEN # #) ; (CAT::MINIMAL-TERM-TOP-LEFT CAT::MTRX-LIST CAT::BEGIN CAT::IL CAT::IC)) ; (LOOP (MULTIPLE-VALUE-BIND # # # #)) ; (INCF CAT::BEGIN))) ; CAT::MTRX-LIST) ; ==> ; CAT::MTRX-LIST ; ; note: deleting unreachable code

; in: DEFUN ECHCM-WITHOUT-EPI ; (THE CAT::CHAIN-COMPLEX ; (WITH-SLOTS (CAT::CMPR CAT::BASIS CAT::DFFR CAT::ORGN) ; CAT::ECHCM ; (DECLARE (TYPE CAT::CMPRF CAT::CMPR) ; (TYPE CAT::BASIS CAT::BASIS) ; (TYPE CAT::MORPHISM CAT::DFFR) ; (LIST CAT::ORGN)) ; (CAT::BUILD-CHCM :CMPR ; #'(LAMBDA (CAT::GNRT1 CAT::GNRT2) ; (IF # ; # ; #)) ; :BASIS ; #'(LAMBDA (CAT::DEGR) (DECLARE #) (COND # # #)) ; :INTR-DFFR ; #'(LAMBDA (CAT::CMBN) (DECLARE #) (CASE # # # #)) ; :STRT :CMBN :ORGN ; `(CAT::ECHCM-WITHOUT-EPI ,CAT::ECHCM)))) ; ; note: type assertion too complex to check: ; (VALUES CHAIN-COMPLEX &REST T).

; in: DEFUN ECHCM-KILL-EPI ; (THE CAT::REDUCTION ; (WITH-SLOTS (CAT::CMPR CAT::BASIS) ; CAT::ECHCM ; (DECLARE (TYPE CAT::CMPRF CAT::CMPR) ; (TYPE CAT::BASIS CAT::BASIS)) ; (ASSERT (NOT (EQ CAT::BASIS :LOCALLY-EFFECTIVE))) ; (LET* ((CAT::F-BASIS #) ; (CAT::F+1-BASIS #) ; (CAT::MTRX-LIST #) ; (CAT::SMITH #) ; (CAT::M #) ; (CAT::N #) ; (CAT::INTR-F #) ; (CAT::INTR-G #) ; (CAT::INTR-H #) ; (CAT::ECHCM2 #)) ; (DECLARE (LIST CAT::MTRX-LIST) ; (TYPE CAT::MATRIX CAT::SMITH) ; (FIXNUM CAT::M CAT::N) ; (TYPE CAT::INTR-MRPH CAT::INTR-F CAT::INTR-G CAT::INTR-H) ; (TYPE CAT::CHAIN-COMPLEX CAT::ECHCM2)) ; (ASSERT (DOTIMES # #)) ; (CAT::BUILD-RDCT :F ; (CAT::BUILD-MRPH :SORC CAT::ECHCM :TRGT CAT::ECHCM2 ; :DEGR 0 :INTR CAT::INTR-F :STRT ; :CMBN :ORGN ...) ; :G ; (CAT::BUILD-MRPH :SORC CAT::ECHCM2 :TRGT CAT::ECHCM ; :DEGR 0 :INTR CAT::INTR-G :STRT ; :CMBN :ORGN ...) ; :H ; (CAT::BUILD-MRPH :SORC CAT::ECHCM :TRGT CAT::ECHCM ; :DEGR 1 :INTR CAT::INTR-H :STRT ; :CMBN :ORGN ...) ; :ORGN `(CAT::ECHCM-KILL-EPI ,CAT::ECHCM))))) ; ; note: type assertion too complex to check: ; (VALUES REDUCTION &REST T).

; in: DEFUN KILL-EPIS ; (THE CAT::HOMOTOPY-EQUIVALENCE ; (PROGN ; (DO ((CAT::INDX FIRST #)) ; ((= CAT::INDX CAT::END)) ; (DECLARE (FIXNUM CAT::INDX)) ; (CAT::KILL-EPI CAT::CHCM CAT::INDX)) ; (CAT::EFHM CAT::CHCM))) ; ; note: type assertion too complex to check: ; (VALUES HOMOTOPY-EQUIVALENCE &REST T).

; in: DEFUN CHML-CLSS ; (THE CAT::MORPHISM ; (CAT::BUILD-MRPH :SORC (CAT::ECHCM CAT::CHCM) :TRGT (CAT::Z-CHCM) :DEGR ; (- FIRST) :INTR (CAT::CHML-CLSS-INTR CAT::CHCM FIRST) ; :STRT :CMBN :ORGN ...)) ; ; note: type assertion too complex to check: ; (VALUES MORPHISM &REST T).