Merge branches 'mariari/ccl-coverage-fixes' and 'artem/uncurry-case'

geb.asd

@@ -147,9 +147,10 @@
   ((:file package)
    (:file meta)
    (:file geb)
+   (:file geb-trans)
    (:file lambda)
    (:file lambda-experimental)
-   (:file lambda-conversion)
+   (:file lambda-trans)
    (:file poly)
    (:file bitc)
    (:file pipeline)

src/geb/trans.lisp

@@ -120,7 +120,7 @@
        (apply #'bitc:parallel
               (append (list bitc:zero (bitc:ident car-width))
                       (zero-list (padding-bits cadr-width
-                                          car-width))))))
+                                               car-width))))))
     ;; Inject-right y -> x + y tags the y with a 1, indicating right,
     ;;   and pads the encoded y with as many zeros as would be needed
     ;;   to store either an x or a y.
@@ -130,7 +130,7 @@
        (apply #'bitc:parallel
               (append (list bitc:one (bitc:ident cadr-width))
                       (zero-list (padding-bits car-width
-                                          cadr-width))))))
+                                               cadr-width))))))
 
     ;; Case translates directly into a branch. The sub-morphisms of
     ;; case are padded with drop so they have the same input lengths.

src/lambda/trans.lisp

@@ -101,12 +101,18 @@ the context on the left as well. For more info check [LAMB][class]"
                   (comp (->right (mcar tott) (mcadr tott))
                         (rec context term))))
                ((case-on on ltm rtm)
-                (let ((toon (ttype on)))
-                  (comp (mcase (curry (rec
-                                       (cons (mcar toon) context) ltm))
-                               (curry (rec
-                                       (cons (mcadr toon) context) rtm)))
-                        (rec context on))))
+                (let ((ctx  (stlc-ctx-to-mu context))
+                      (mcr  (mcar (ttype on)))
+                      (mcdr (mcadr (ttype on))))
+                  (comp (comp (mcase (commutes-left (rec
+                                                     (cons mcr context) ltm))
+                                     (commutes-left (rec
+                                                     (cons mcdr context) rtm)))
+                              (commutes-left (distribute ctx
+                                                         (fun-to-hom mcr)
+                                                         (fun-to-hom mcdr))))
+                        (geb:pair (rec context on)
+                                  ctx))))
                ((pair ltm rtm)
                 (geb:pair (rec context ltm)
                           (rec context rtm)))
@@ -129,10 +135,10 @@ the context on the left as well. For more info check [LAMB][class]"
                               :from-end t)))
                ((index pos)
                 (stlc-ctx-proj context pos)))))
-    (let ((ann-term (ann-term1 context tterm)))
-      (if (well-defp context ann-term)
-          (rec context ann-term)
-          (error "not a well-defined ~A in said ~A" tterm context)))))
+    (if (well-defp context tterm)
+        (rec context (ann-term1 context tterm))
+        (error "not a well-defined ~A in said ~A" tterm context))))
+
 
 
 (-> stlc-ctx-to-mu (stlc-context) substobj)
@@ -159,6 +165,7 @@ LAMBDA> (stlc-ctx-to-mu (list so1 (fun-to-hom (fun-type geb-bool:bool geb-bool:b
 ;; Utility Functions
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
+
 (defun stlc-ctx-proj (context depth)
   "Given a context, we interpret it as a [PROD][class] object of appropriate
 length with fibrations given by [PROD][class] projections."

test/bitc.lisp

@@ -21,7 +21,6 @@
   :parent geb-bitc
   (of-type list test-circuit-1))
 
-
 (define-test bitc-evaluates-and-correctly
   :parent geb-bitc
   (is equalp #*1 (gapply (to-bitc geb-bool:and) #*11))

test/geb-trans.lisp

@@ -0,0 +1,20 @@
+(in-package :geb-test)
+
+(define-test geb.trans :parent geb-test-suite)
+
+(def geb.pair-of-size-4
+  (to-bitc
+   (pair (->right so1 bool)
+         (->left so1 bool))))
+
+(define-test geb.trans-pair :parent geb.trans
+  (is = 4 (codom geb.pair-of-size-4)
+      "both objects have max size of 2, pair them size 4")
+  (is = 1 (dom   geb.pair-of-size-4)
+      "Our input is bool, thus 1 bit")
+  (is obj-equalp #*1100 (gapply geb.pair-of-size-4 #*1)
+      "Right should tag it with 1, with our 1 injected and our left should
+       always be 00")
+  (is obj-equalp #*1000 (gapply geb.pair-of-size-4 #*0)
+      "Right should tag it with 1, with our 0 injected and our left should
+       always be 00"))

test/geb.lisp

@@ -66,39 +66,37 @@
                                 (->left so1 so1)))
       "Checking the dom of pair")
   (is obj-equalp
-      (prod geb-bool:bool
-            geb-bool:bool)
+      (prod bool
+            bool)
       (codom (pair (->left geb-bool:false-obj geb-bool:true-obj)
                    (->left geb-bool:false-obj geb-bool:true-obj)))
       "Checking the codom of pair")
   (is obj-equalp
-      (dom (<-left so1 geb-bool:bool))
-      (prod so1 geb-bool:bool)
+      (dom (<-left so1 bool))
+      (prod so1 bool)
       "checking dom of projection")
   (is obj-equalp
-      (dom (distribute geb-bool:bool so1 so1))
-      (prod geb-bool:bool (coprod so1 so1))
+      (dom (distribute bool so1 so1))
+      (prod bool (coprod so1 so1))
       "checking dom of distribution")
   (is obj-equalp
-      (codom (distribute geb-bool:bool so1 so1))
-      (coprod (prod geb-bool:bool so1)
-              (prod geb-bool:bool so1))
+      (codom (distribute bool so1 so1))
+      (coprod (prod bool so1)
+              (prod bool so1))
       "checking codom of distribution"))
 
 
 (define-test curry
   :parent geb
-  (of-type substmorph (curry (<-left geb-bool:bool geb-bool:bool)))
+  (of-type substmorph (curry (<-left bool bool)))
   ;; may be typing this a bit too strictly
-  (of-type comp (curry (<-left geb-bool:bool so1)))
-  (is obj-equalp
-      (dom (geb:curry geb-bool:and))
-      geb-bool:bool))
+  (of-type comp (curry (<-left bool so1)))
+  (is obj-equalp (dom (geb:curry bool:and)) bool))
 
 
 (define-test geb-trans :parent geb)
 
-(def test-morph-2 (<-left so1 geb-bool:bool))
+(def test-morph-2 (<-left so1 bool))
 
 (def test-poly-2 (to-poly test-morph-2))
 
@@ -115,48 +113,18 @@
 
 ;; PLEASE FUZZ THIS!
 (define-test interpret-bool :parent geb-interpreter
-  (is
-   obj-equalp
-   (gapply geb-bool:and
-           (list (left so1)
-                 (left so1)))
-   (left so1))
-
-  (is
-   obj-equalp
-   (gapply geb-bool:and
-           (list (left so1)
-                 (right so1)))
-   (left so1))
-
-  (is
-   obj-equalp
-   (gapply geb-bool:and
-           (list (right so1)
-                 (right so1)))
-   (right so1))
-
-  (is
-   obj-equalp
-   (gapply geb-bool:not
-           (left so1))
-   (right so1))
-
-  (is
-   obj-equalp
-   (gapply geb-bool:not
-           (right so1))
-   (left so1)))
-
-(define-test gapply-bool-id
-  :parent geb-trans
   (is obj-equalp
-      (right so1)
-      (gapply
-       (to-cat nil (lambda:lamb (list (coprod so1 so1)) (geb.lambda:index 0)))
-       (list (right so1) so1)))
+      (gapply bool:and (list (left so1) (left so1)))
+      (left so1))
+
   (is obj-equalp
-      (left so1)
-      (gapply
-       (to-cat nil (lambda:lamb (list (coprod so1 so1)) (geb.lambda:index 0)))
-       (list (left so1) so1))))
+      (gapply bool:and (list (left so1) (right so1)))
+      (left so1))
+
+  (is obj-equalp
+      (gapply bool:and (list (right so1) (right so1)))
+      (right so1))
+
+  (is obj-equalp (gapply bool:not (left so1)) (right so1))
+
+  (is obj-equalp (gapply bool:not (right so1)) (left so1)))