Merge branch 'artem/well-defp'

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 <substmorph>))
+  (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 <natmorph>))
+  t)
+
+(defmethod well-defp-cat ((morph <natobj>))
+  t)

src/geb/package.lisp

@@ -244,6 +244,9 @@ We also define out API functions to operate on this"
   (gapply                     (pax:method () (<substmorph> t)))
   (gapply                     (pax:method () (opaque-morph t)))
   (gapply                     (pax:method () (opaque t)))
+  (well-defp-cat              (pax:method () (<substmorph>)))
+  (well-defp-cat              (pax:method () (<natmorph>)))
+  (well-defp-cat              (pax:method () (<natobj>)))
   (geb-bool:@geb-bool        pax:section)
   (geb-list:@geb-list        pax:section)
   (geb.trans:@geb-translation pax:section)

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
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

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)

src/seqn/package.lisp

@@ -18,12 +18,13 @@
   (width              (pax:method () (<natobj>)))
   (width               pax:generic-function)
   (inj-coprod-parallel pax:function)
-  (zero-list           pax:function)
-  (dom    (pax:method () (<seqn>)))
-  (dom    (pax:generic-function))
-  (cod    (pax:method () (<seqn>)))
-  (cod    (pax:generic-function))
-  (gapply (pax:method () (<seqn> t))))
+  (zero-list              pax:function)
+  (dom                 (pax:method () (<seqn>)))
+  (dom                 (pax:generic-function))
+  (cod                 (pax:method () (<seqn>)))
+  (cod                 (pax:generic-function))
+  (well-defp-cat       (pax:method () (<seqn>)))
+  (gapply              (pax:method () (<seqn> t))))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;; trans module

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 <seqn>))
+  (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)))