;;;  EFFECTIVE-HOMOLOGY  EFFECTIVE-HOMOLOGY  EFFECTIVE-HOMOLOGY
;;;  EFFECTIVE-HOMOLOGY  EFFECTIVE-HOMOLOGY  EFFECTIVE-HOMOLOGY
;;;  EFFECTIVE-HOMOLOGY  EFFECTIVE-HOMOLOGY  EFFECTIVE-HOMOLOGY

(IN-PACKAGE #:cat)

(PROVIDE "effective-homology")

;;;
;;;  REDUCTIONS
;;;


#+clisp(eval-when (:compile-toplevel :load-toplevel :execute)
         (setf (ext:package-lock :clos) nil))
(DEFMETHOD PRINT-OBJECT ((rdct reduction) stream)
  (the reduction
       (progn
	 (format stream "[K~D Reduction K~D => K~D]"
		 (idnm rdct) (idnm (tcc rdct)) (idnm (bcc rdct)))
	 rdct)))
#+clisp(eval-when (:compile-toplevel :load-toplevel :execute)
         (setf (ext:package-lock :clos) t))


(DEFUN RDCT (n)
  (declare (fixnum n))
  "--------------------------------------------------------------[function-doc]
RDCT
Args: (n)
Returns the N-th user-created reduction from the list *RDCT-LIST*. Returns NIL
if it doesn't exist.
------------------------------------------------------------------------------"
  (the (or null reduction)
       (find n *rdct-list* :key #'idnm)))


(DEFUN BUILD-RDCT (&key f g h orgn)
  (declare
   (type morphism f g h)
   (list orgn))
  "--------------------------------------------------------------[function-doc]
BUILD-RDCT
Args: (&key f g h orgn)
Returns an instance of the class REDUCTION. The keyword arguments are as
follows:

:F F, an object of type morphism representing the morphism f of a reduction

:G G, an object of type morphism representing the morphism g of a reduction

:H H, an object of type morphism representing the morphism h of a reduction

:ORGN ORGN, a list containing a relevant and carefully chosen comment about
            the origin of the chain complex. This comment should be unique
            for a Kenzo session (between calls of CAT-INIT), as it is used
            for caching purposes.

Use this function instead of creating instances via the standard constructor
MAKE-INSTANCE.
------------------------------------------------------------------------------"
  (the reduction
       (progn
         (unless orgn
	   (setf orgn `(build-rdct ,f ,g ,h)))
         (let ((already (find orgn *rdct-list* :test #'equal :key #'orgn)))
	   (declare (type (or reduction null) already))
	   (when already
	     (return-from build-rdct already)))
         (with-slots ((fsorc sorc) (ftrgt trgt) (fdegr degr)) f
	   (declare
	    (type chain-complex fsorc ftrgt)
	    (fixnum fdegr))
	   (with-slots ((gsorc sorc) (gtrgt trgt) (gdegr degr)) g
	     (declare
	      (type chain-complex gsorc gtrgt)
	      (fixnum gdegr))
	     (with-slots ((hsorc sorc) (htrgt trgt) (hdegr degr)) h
	       (declare
		(type chain-complex hsorc htrgt)
		(fixnum hdegr))
	       (unless (and (eq gsorc ftrgt)
			    (eq fsorc gtrgt)
			    (eq hsorc fsorc)
			    (eq htrgt fsorc)
			    (zerop fdegr)
			    (zerop gdegr)
			    (= +1 hdegr))
		 (error "In BUILD-RDCT, the data are non coherent."))
	       (let ((rdct (make-instance 'reduction
					  :tcc fsorc :bcc ftrgt
					  :f f :g g :h h
					  :orgn orgn)))
		 (declare (type reduction rdct))
		 (push rdct *rdct-list*)
		 rdct)))))))


(DEFUN TRIVIAL-RDCT (chcm)
  (declare (type chain-complex chcm))
  "--------------------------------------------------------------[function-doc]
TRIVIAL-RDCT
Args: (chcm)
Builds the trivial reduction according to the following diagram, which
involves the chain complex CHCM only:

          Zero    s
     C  ------->   C
      ^
    | |
 Id | | Id
    | |
    v
     C

Zero is the zero morphism of degree 1 of C and Id is its identity morphism.

See also: ZERO-MRPH, IDNT-MRPH.
------------------------------------------------------------------------------"
  (build-rdct
   :f (idnt-mrph chcm)
   :g (idnt-mrph chcm)
   :h (zero-mrph chcm chcm +1)
   :orgn `(trivial-rdct ,chcm)))


;;;
;;;  HOMOTOPY-EQUIVALENCES
;;;

;;(defgeneric build-hmeq (keyword lrdct &key &allow-other-keys)
(DEFGENERIC BUILD-HMEQ (keyword lrdct &key))


(DEFMETHOD BUILD-HMEQ ((keyword1 (eql :lrdct)) lrdct &key rrdct orgn)
  (declare
   (type reduction lrdct rrdct)
   (list orgn))
  (the homotopy-equivalence
       (progn
         (with-slots ((lf f) (lg g) (lh h) (ltcc tcc) (lbcc bcc)) lrdct
	   (declare
	    (type morphism lf lg lh)
	    (type chain-complex ltcc lbcc))
	   (with-slots ((rf f) (rg g) (rh h) (rtcc tcc) (rbcc bcc)) rrdct
	     (declare
	      (type morphism rf rg rh)
	      (type chain-complex rtcc rbcc))
	     (unless (eq ltcc rtcc)
               (error "In BUILD-HMEQ (version from rdct), the tcc's are not the same."))
	     (unless orgn
               (setf orgn `(build-hmeq ,lrdct ,rrdct)))
	     (let ((already (find orgn *hmeq-list* :test #'equal :key #'orgn)))
               (declare (type (or homotopy-equivalence null) already))
               (when already
		 (return-from build-hmeq already)))
	     (let ((hmeq (make-instance 'homotopy-equivalence
					:lbcc lbcc :tcc ltcc :rbcc rbcc
					:lf lf :lg lg :lh lh
					:rf rf :rg rg :rh rh
					:lrdct lrdct :rrdct rrdct
					:orgn orgn)))
               (declare (type homotopy-equivalence hmeq))
               (push hmeq *hmeq-list*)
               hmeq))))))


#+clisp(eval-when (:compile-toplevel :load-toplevel :execute)
         (setf (ext:package-lock :clos) nil))
(DEFMETHOD PRINT-OBJECT ((hmeq homotopy-equivalence) stream)
  (the homotopy-equivalence
       (progn
	 (format stream "[K~D Homotopy-Equivalence K~D <= K~D => K~D]"
		 (idnm hmeq)
		 (idnm (lbcc hmeq)) (idnm (tcc hmeq)) (idnm (rbcc hmeq)))
	 hmeq)))
#+clisp(eval-when (:compile-toplevel :load-toplevel :execute)
         (setf (ext:package-lock :clos) t))

(DEFGENERIC HMEQ (integer))

(DEFMETHOD HMEQ ((n integer))
  (declare (fixnum n))
  (the (or homotopy-equivalence null)
       (find n *hmeq-list* :key #'idnm)))

(DEFMETHOD BUILD-HMEQ ((keyword1 (eql :lf)) lf &key lg lh rf rg rh orgn)
  (declare
   (type morphism lf lg lh rf rg rh)
   (list orgn))
  (the homotopy-equivalence
       (progn
         (unless orgn
	   (setf orgn `(build-hmeq ,lf ,lg ,lh ,rf ,rg ,rh)))
         (let ((already (find orgn *hmeq-list* :test #'equal :key #'orgn)))
	   (declare (type (or null homotopy-equivalence) already))
	   (when already
	     (return-from build-hmeq already)))
         (build-hmeq
          :lrdct (build-rdct :f lf :g lg :h lh
			     :orgn `(build-hmeq ,lf ,lg ,lh ,rf ,rg ,rh lrdct))
          :rrdct (build-rdct :f rf :g rg :h rh
			     :orgn `(build-hmeq ,lf ,lg ,lh ,rf ,rg ,rh rrdct))
          :orgn orgn))))

(DEFUN TRIVIAL-HMEQ (chcm)
  (declare (type chain-complex chcm))
  (build-hmeq
   :lrdct (trivial-rdct chcm)
   :rrdct (trivial-rdct chcm)
   :orgn `(trivial-hmeq ,chcm)))

;; Functions.

(DEFUN PRE-CHECK-RDCT (rdct)
  "--------------------------------------------------------------[function-doc]
PRE-CHECK-RDCT
Args: (rdct)
Assigns the following Lisp global variables, using morphisms from RDCT and the
differentials and identity morphisms of the underlying chain complexes,
according to these formulas:

*TDD*         = d  ° d
                 ^    ^
                 C    C

*BDD*         = d  ° d
                 C    C

*ID-FG*       = Id  - f ° g
                  C

*ID-GF-DH-HD* = Id  - g ° f - (d ° h + h ° d )
                  ^             ^           ^
                  C             C           C

*HH*          = h ° h
*FH*          = f ° h
*HG*          = h ° g

*DF-FD*       = d  ° f - f ° d
                 C            ^
                              C

*DG-GD*       = d  ° g - g ° d
                 ^            C
                 C

------------------------------------------------------------------------------"
  (declare (type reduction rdct))
  (with-slots (bcc tcc f g h) rdct
    (declare
     (type chain-complex bcc tcc)
     (type morphism f g h))
    (setf *tdd* (cmps tcc tcc)
	  *bdd* (cmps bcc bcc)
	  *df-fd* (sbtr
		   (cmps bcc f)
		   (cmps f tcc))
	  *dg-gd* (sbtr
		   (cmps tcc g)
		   (cmps g bcc))
	  *id-fg* (sbtr (idnt-mrph bcc) (cmps f g))
	  *id-gf-dh-hd* (i-sbtr (idnt-mrph tcc)
				(cmps g f)
				(cmps tcc h)
				(cmps h tcc))
	  *hh* (cmps h h)
	  *fh* (cmps f h)
	  *hg* (cmps h g)))
  (done))


(DEFUN CHECK-RDCT ()
  "--------------------------------------------------------------[function-doc]
CHECK-RDCT
Args: ()
Maps combinations of the top and bottom chain complexes of a reduction using
the morphisms created by PRE-CHECK-RDCT. Having no parameters, the
combinations must be provided via the Lisp global variables *TC* and *BC*,
for the top and bottom chain complex, respectively. If the morphisms are
coherent, the result of each mapping is a null combination.

Note: This function is intended for interactive use. It pauses after each
evaluation for the user to inspect the result. Resume execution, by pressing
the <Enter> key.
------------------------------------------------------------------------------"
  (dolist (cmbn '(*tc* *bc*))
    (declare (type symbol cmbn))
    (format t "~%~A => ~A" cmbn (eval cmbn)))
  (dolist (phi '(*tdd* *bdd* *df-fd* *dg-gd* *id-fg* *id-gf-dh-hd*
		 *hh* *fh* *hg*))
    (declare (type symbol phi))
    (format t "~%Checking ~A = 0" phi)
    (format t "~%Result: ")
    (princ (cmbn-? (eval phi)
		   (if (member phi '(*bdd* *dg-gd* *id-fg* *dg-gd* *hg*))
		       *bc* *tc*)))
    (read-line))
  (done))


(DEFUN CHECK-RDCT-NO-WAIT ()
  "--------------------------------------------------------------[function-doc]
CHECK-RDCT-NO-WAIT
Args: ()
Maps combinations of the top and bottom chain complexes of a reduction using
the morphisms created by PRE-CHECK-RDCT. Having no parameters, the
combinations must be provided via the Lisp global variables *TC* and *BC*,
for the top and bottom chain complex, respectively. If the morphisms are
coherent, the result of each mapping is a null combination.
------------------------------------------------------------------------------"
  (dolist (cmbn '(*tc* *bc*))
    (declare (type symbol cmbn))
    (format t "~%~A => ~A" cmbn (eval cmbn)))
  (dolist (phi '(*tdd* *bdd* *df-fd* *dg-gd* *id-fg* *id-gf-dh-hd*
		 *hh* *fh* *hg*))
    (declare (type symbol phi))
    (format t "~%Checking ~A = 0" phi)
    (format t "~%Result: ")
    (princ (cmbn-? (eval phi)
		   (if (member phi '(*bdd* *dg-gd* *id-fg* *dg-gd* *hg*))
		       *bc* *tc*))))
  (done))


(DEFMETHOD CMPS ((brdct reduction) (trdct reduction) &optional dummy)
  (declare (ignore dummy))
  (when (eq (first (orgn brdct)) 'trivial-rdct)
    (return-from cmps trdct))
  (when (eq (first (orgn trdct)) 'trivial-rdct)
    (return-from cmps brdct))
  (with-slots ((tf f) (tg g) (th h)) trdct
    (declare (type morphism tf tg th))
    (with-slots ((bf f) (bg g) (bh h)) brdct
      (declare (type morphism bf bg bh))
      (build-rdct
       :f (cmps bf tf)
       :g (cmps tg bg)
       :h (add th (i-cmps tg bh tf))
       :orgn `(cmps ,brdct ,trdct)))))

;;
;; BASIC PERTURBATION LEMMA.
;;

(DEFMETHOD ADD ((rdct reduction) (perturbation morphism) &optional dummy)
  (declare (type null dummy))
  (when dummy
    (error "Why a third argument in (ADD REDUCTION MORPHISM)?"))
  (when (eq (grmd (tcc rdct)) (grmd (sorc perturbation)))
    (return-from add
      (basic-perturbation-lemma rdct perturbation)))
  (when (eq (grmd (bcc rdct)) (grmd (sorc perturbation)))
    (return-from add
      (easy-perturbation-lemma rdct perturbation)))
  (error "In (METHOD ADD REDUCTION MORPHISM),~@
           the data do not sound like coherent."))

(DEFUN BASIC-PERTURBATION-LEMMA (reduction top-perturbation)
  (declare
   (type reduction reduction)
   (type morphism top-perturbation))
  (the (values reduction morphism)
       (with-slots ((old-tcc tcc) (old-bcc bcc)
		    (old-f f) (old-g g) (old-h h)) reduction
         (declare
	  (type chain-complex old-tcc old-bcc)
	  (type morphism old-f old-g old-h))
         (when (eq (first (orgn top-perturbation)) 'zero-mrph)
	   (return-from basic-perturbation-lemma
	     (values reduction (zero-mrph old-bcc))))
         (when (eq (first (orgn (h reduction))) 'zero-mrph)
	   (return-from basic-perturbation-lemma
	     (values
	      (trivial-rdct (add old-tcc top-perturbation))
	      (i-cmps old-f top-perturbation old-g))))
         (let* ((sigma (bpl-*-sigma old-h top-perturbation))
                (new-f (cmps old-f
			     (sbtr (idnt-mrph old-tcc)
				   (i-cmps
				    top-perturbation
				    sigma
				    old-h))))
                (new-g (cmps sigma old-g))
                (new-h (cmps sigma old-h))
                (bottom-perturbation (i-cmps
				      old-f
				      top-perturbation
				      new-g))
                (new-tcc (add old-tcc top-perturbation))
                (new-bcc (add old-bcc bottom-perturbation)))
	   (declare
	    (type chain-complex new-tcc new-bcc)
	    (type morphism sigma new-f new-g new-h bottom-perturbation))
	   (setf new-f (dstr-change-sorc-trgt new-f :new-sorc new-tcc
					      :new-trgt new-bcc)
		 new-g (dstr-change-sorc-trgt new-g :new-sorc new-bcc
					      :new-trgt new-tcc)
		 new-h (dstr-change-sorc-trgt new-h :new-sorc new-tcc
					      :new-trgt new-tcc))
	   (values
	    (build-rdct :f new-f :g new-g :h new-h
			:orgn `(basic-perturbation-lemma ,reduction
							 ,top-perturbation))
	    bottom-perturbation)))))

(DEFUN EASY-PERTURBATION-LEMMA (reduction bottom-perturbation)
  (declare
   (type reduction reduction)
   (type morphism bottom-perturbation))
  (the (values reduction morphism)
       (with-slots ((old-tcc tcc) (old-bcc bcc)
		    (old-f f) (old-g g) (old-h h)) reduction
         (declare
	  (type chain-complex old-tcc old-bcc)
	  (type morphism old-f old-g old-h))
         (when (eq 'zero-mrph (first (orgn bottom-perturbation)))
	   (return-from easy-perturbation-lemma
	     (values reduction (zero-mrph old-tcc))))
	 (when (eq 'trivial-rdct (first (orgn reduction)))
	   (return-from easy-perturbation-lemma
	     (trivial-rdct (add (bcc reduction) bottom-perturbation))))
         (let ((top-perturbation (i-cmps old-g bottom-perturbation old-f)))
	   (declare (type morphism top-perturbation))
	   (let ((new-bcc (add old-bcc bottom-perturbation))
		 (new-tcc (add old-tcc top-perturbation)))
	     (declare (type chain-complex new-bcc new-tcc))
	     (values
	      (build-rdct
	       :f (dstr-change-sorc-trgt old-f :new-sorc new-tcc
					 :new-trgt new-bcc)
	       :g (dstr-change-sorc-trgt old-g :new-sorc new-bcc
					 :new-trgt new-tcc)
	       :h (dstr-change-sorc-trgt old-h :new-sorc new-tcc
					 :new-trgt new-tcc)
	       :orgn `(easy-perturbation-lemma ,reduction
					       ,bottom-perturbation))
	      top-perturbation))))))

(DEFUN SPECIAL-BPL (reduction top-perturbation)
  (declare
   (type reduction reduction)
   (type morphism top-perturbation))
  (when (eq (first (orgn top-perturbation)) 'zero-mrph)
    (return-from special-bpl reduction))
  (the reduction
       (with-slots ((old-tcc tcc) (old-bcc bcc)
		    (old-f f) (old-g g) (old-h h)) reduction
         (declare
	  (type chain-complex old-tcc old-bcc)
	  (type morphism old-f old-g old-h))
         (let* ((sigma (bpl-*-sigma old-h top-perturbation))
                (new-f (cmps old-f
			     (sbtr (idnt-mrph old-tcc)
				   (i-cmps
				    top-perturbation
				    sigma
				    old-h))))
                (new-h (cmps sigma old-h))
                (new-tcc (add old-tcc top-perturbation)))
	   (declare
	    (type chain-complex new-tcc)
	    (type morphism sigma new-f new-h))
	   (setf new-f (dstr-change-sorc-trgt new-f :new-sorc new-tcc)
		 old-g (dstr-change-sorc-trgt old-g :new-trgt new-tcc)
		 new-h (dstr-change-sorc-trgt new-h :new-sorc new-tcc
					      :new-trgt new-tcc))
	   (build-rdct :f new-f :g old-g :h new-h
		       :orgn `(special-bpl ,reduction ,top-perturbation))))))

(DEFUN SPECIAL-BPL-2 (reduction top-perturbation)
  (declare
   (type reduction reduction)
   (type morphism top-perturbation))
  (the reduction
       (with-slots ((old-tcc tcc) (old-bcc bcc)
		    (old-f f) (old-g g) (old-h h)) reduction
         (declare
	  (type chain-complex old-tcc old-bcc)
	  (type morphism old-f old-g old-h))
         (when (eq (first (orgn top-perturbation)) 'zero-mrph)
	   (return-from special-bpl-2
	     (values reduction (zero-mrph old-bcc))))
         (when (eq (first (orgn (h reduction))) 'zero-mrph)
	   (return-from special-bpl-2
	     (values
	      (trivial-rdct (add old-tcc top-perturbation))
	      (i-cmps old-f top-perturbation old-g))))
         (let* ((sigma (bpl-*-sigma old-h top-perturbation))
                (new-g (cmps sigma old-g))
                (new-h (cmps sigma old-h))
                (new-tcc (add old-tcc top-perturbation)))
	   (declare
	    (type chain-complex new-tcc)
	    (type morphism sigma new-g new-h))
	   (setf old-f (dstr-change-sorc-trgt old-f :new-sorc new-tcc)
		 new-g (dstr-change-sorc-trgt new-g :new-trgt new-tcc)
		 new-h (dstr-change-sorc-trgt new-h :new-sorc new-tcc
					      :new-trgt new-tcc))
	   (values
	    (build-rdct :f old-f :g new-g :h new-h
			:orgn `(special-bpl-2 ,reduction ,top-perturbation)))))))

(DEFUN BPL-*-sigma (homotopy perturbation)
  (declare (type morphism homotopy perturbation))
  (the morphism
       (let ((cmpr (cmpr (sorc perturbation)))
	     (h-delta (cmps homotopy perturbation)))
         (declare
	  (type cmprf cmpr)
	  (type morphism h-delta))
         (flet
	     ((sigma-* (degr gnrt)
                (declare
		 (fixnum degr)
		 (type gnrt gnrt))
                (do ((rslt (zero-cmbn degr) (2cmbn-add cmpr rslt iterated))
                     (iterated (term-cmbn degr 1 gnrt)
			       (cmbn-opps (cmbn-? h-delta iterated))))
                    ((cmbn-zero-p iterated) rslt)
		  (declare (type cmbn rslt iterated)))))
	   (build-mrph
	    :sorc (sorc homotopy) :trgt (sorc homotopy) :degr 0
	    :intr #'sigma-*
	    :strt :gnrt
	    :orgn `(bpl-*-sigma ,homotopy ,perturbation))))))

(DEFMETHOD ADD ((hmeq homotopy-equivalence) (lb-perturbation morphism)
		&optional dummy)
  (declare (ignore dummy))
  (the homotopy-equivalence
       (with-slots (lrdct rrdct) hmeq
         (declare (type reduction lrdct rrdct))
         (multiple-value-bind (new-lrdct top-perturbation)
	     (add lrdct lb-perturbation)
	   (declare
	    (type reduction new-lrdct)
	    (type morphism lb-perturbation))
	   (build-hmeq
	    :lrdct new-lrdct
	    :rrdct (add rrdct top-perturbation)
	    :orgn `(add ,hmeq ,lb-perturbation))))))