diff --git a/src/geb/geb.lisp b/src/geb/geb.lisp index f1ed075ff..a33a9b71c 100644 --- a/src/geb/geb.lisp +++ b/src/geb/geb.lisp @@ -536,3 +536,48 @@ I am the [GAPPLY][generic-function] for a generic [OPAQUE][class] I simply dispatch [GAPPLY][generic-function] on my interior code, which is likely just an object" (gapply (code morph) object)) + +(defmethod well-defp-cat ((morph )) + (etypecase-of substmorph morph + (comp + (let ((mcar (mcar morph)) + (mcadr (mcadr morph))) + (if (and (well-defp-cat mcar) + (well-defp-cat mcadr) + (obj-equalp (dom mcar) + (codom mcadr))) + t + (error "(Co)Domains do not match for ~A" morph)))) + (case + (let ((mcar (mcar morph)) + (mcadr (mcadr morph))) + (if (and (well-defp-cat mcar) + (well-defp-cat mcadr) + (obj-equalp (codom mcar) + (codom mcadr))) + t + (error "Casing ill-defined for ~A" morph)))) + (pair + (let ((mcar (mcar morph)) + (mcdr (mcdr morph))) + (if (and (well-defp-cat mcar) + (well-defp-cat mcdr) + (obj-equalp (dom mcar) + (dom mcdr))) + t + (error "Pairing ill-defined for ~A" morph)))) + ((or substobj + init + terminal + project-left + project-right + inject-left + inject-right + distribute) + t))) + +(defmethod well-defp-cat ((morph )) + t) + +(defmethod well-defp-cat ((morph )) + t) diff --git a/src/geb/package.lisp b/src/geb/package.lisp index 3e389aca0..393b3f63e 100644 --- a/src/geb/package.lisp +++ b/src/geb/package.lisp @@ -244,6 +244,9 @@ We also define out API functions to operate on this" (gapply (pax:method () ( t))) (gapply (pax:method () (opaque-morph t))) (gapply (pax:method () (opaque t))) + (well-defp-cat (pax:method () ())) + (well-defp-cat (pax:method () ())) + (well-defp-cat (pax:method () ())) (geb-bool:@geb-bool pax:section) (geb-list:@geb-list pax:section) (geb.trans:@geb-translation pax:section) diff --git a/src/generics/generics.lisp b/src/generics/generics.lisp index 5ff121c97..906584b63 100644 --- a/src/generics/generics.lisp +++ b/src/generics/generics.lisp @@ -23,6 +23,12 @@ GEB> (gapply (comp (left s-1) ```")) +(defgeneric well-defp-cat (morphism) + (:documentation "Given a moprhism of a category, checks that +it is well-defined. E.g. that composition of morphism is +well-defined by checking that the domain of MCAR corresponds +to the codomain of MCADR")) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Object Functions ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/src/generics/package.lisp b/src/generics/package.lisp index 464ec7eec..79721833d 100644 --- a/src/generics/package.lisp +++ b/src/generics/package.lisp @@ -14,6 +14,7 @@ You can view their documentation in their respective API sections. The main documentation for the functionality is given here, with examples often given in the specific methods" (gapply pax:generic-function) + (well-defp-cat pax:generic-function) (maybe pax:generic-function) (so-eval pax:generic-function) (to-circuit pax:generic-function) diff --git a/src/seqn/package.lisp b/src/seqn/package.lisp index 2864ce0a5..96e1eb3f2 100644 --- a/src/seqn/package.lisp +++ b/src/seqn/package.lisp @@ -18,12 +18,13 @@ (width (pax:method () ())) (width pax:generic-function) (inj-coprod-parallel pax:function) - (zero-list pax:function) - (dom (pax:method () ())) - (dom (pax:generic-function)) - (cod (pax:method () ())) - (cod (pax:generic-function)) - (gapply (pax:method () ( t)))) + (zero-list pax:function) + (dom (pax:method () ())) + (dom (pax:generic-function)) + (cod (pax:method () ())) + (cod (pax:generic-function)) + (well-defp-cat (pax:method () ())) + (gapply (pax:method () ( t)))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; trans module diff --git a/src/seqn/seqn.lisp b/src/seqn/seqn.lisp index b2824fefe..d034039d1 100644 --- a/src/seqn/seqn.lisp +++ b/src/seqn/seqn.lisp @@ -179,3 +179,66 @@ is capable of succesfully evaluating all compiled terms" (seqn-lt (if (< (car vector) (cadr vector)) (list 0 0) (list 1 0))))) + +(defmethod well-defp-cat ((morph )) + (etypecase-of seqn morph + (composition + (let* ((mcar (mcar morph)) + (mcadr (mcadr morph)) + (dom (dom mcar)) + (cod (cod mcadr))) + (if (and (well-defp-cat mcar) + (well-defp-cat mcadr) + (obj-equalp dom + cod)) + t + (error "Co(Domains) do not match for ~A with domain + of MCAR ~A1 and codomain of MCADR ~A2." + morph cod dom)))) + (parallel-seq + (if (and (well-defp-cat (mcar morph)) + (well-defp-cat (mcadr morph))) + t + (error "Not well-defined parallel composition ~A" morph))) + (branch-seq + (let* ((mcar (mcar morph)) + (mcadr (mcadr morph)) + (dom1 (dom mcar)) + (dom2 (dom mcadr)) + (cod1 (cod mcar)) + (cod2 (cod mcadr))) + (if (and (well-defp-cat mcar) + (well-defp-cat mcadr) + (obj-equalp dom1 dom2) + (obj-equalp cod1 cod2)) + t + (error "Not a well-defined branching ~A. + ~A1 has dom ~a1 and cod ~a2. + ~A2 has dom ~a3 and cod ~a4" + morph mcar dom1 cod1 mcadr dom2 cod2)))) + (shift-front + (if (>= (length (mcar morph)) + (mcadr morph)) + t + (error "Wrong shift-length for ~A" morph))) + ((or id + fork-seq + drop-nil + drop-width + remove-right + remove-left + inj-length-left + inj-length-right + inj-size + zero-bit + one-bit + seqn-add + seqn-multiply + seqn-divide + seqn-subtract + seqn-nat + seqn-concat + seqn-decompose + seqn-eq + seqn-lt) + t)))