Add method to compile geb to boolean circuits.

geb.asd

@@ -9,11 +9,15 @@
   :description "Gödel, Escher, Bach, a categorical view of computation"
   :build-pathname "../build/geb.image"
   :entry-point "geb.entry::entry"
+
   :build-operation "program-op"
   :author "Mariari"
+
   :license "MIT"
+
   :pathname "src/"
   :components
+
   ((:module util
     :serial t
     :description "Internal utility functions"
@@ -60,6 +64,12 @@
     :depends-on (util geb vampir specs)
     :components ((:file package)
                  (:file poly)))
+   (:module bitc
+    :serial t
+    :description "bitc (Boolean Circuits)"
+    :depends-on (util vampir mixins specs)
+    :components ((:file package)
+                 (:file bitc)))
    (:module lambda
     :serial t
     :depends-on (geb specs)
@@ -84,6 +94,8 @@
                  (:file poly-printer)
                  (:file extension)
                  (:file extension-printer)
+                 (:file bitc)
+                 (:file bitc-printer)
                  ;; HACK: to make the package properly refer to the
                  ;; right symbols
                  (:file ../util/package)))
@@ -97,11 +109,12 @@
     :pathname "../src/"
     :components ((:file lambda/trans)
                  (:file geb/trans)
-                 (:file poly/trans)))
+                 (:file poly/trans)
+                 (:file bitc/trans)))
    (:module entry
     :serial t
     :description "Entry point for the geb codebase"
-    :depends-on (util geb vampir specs poly lambda)
+    :depends-on (util geb vampir specs poly bitc lambda)
     :components ((:file package)
                  (:file entry))))
   :in-order-to ((asdf:test-op (asdf:test-op :geb/test))))
@@ -141,6 +154,7 @@
    (:file lambda-experimental)
    (:file lambda-conversion)
    (:file poly)
+   (:file bitc)
    (:file pipeline)
    (:module gui
     :serial t

src/bitc/bitc.lisp

@@ -0,0 +1,33 @@
+(in-package :geb.bitc.main)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Domain and codomain definitions
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(defmethod dom ((x <bitc>))
+  (typecase-of bitc x
+    (compose          (dom (mcadr x)))
+    (fork             (dom (mcar x)))
+    (parallel         (+ (dom (mcar x)) (dom (mcadr x))))
+    (swap             (+ (mcar x) (mcadr x)))
+    (one              0)
+    (zero             0)
+    (ident            (mcar x))
+    (drop             (mcar x))
+    (branch           (+ 1 (dom (mcar x))))
+    (otherwise
+      (subclass-responsibility x))))
+
+(defmethod codom ((x <bitc>))
+  (typecase-of bitc x
+    (compose          (codom (mcar x)))
+    (fork             (* 2 (codom (mcar x))))
+    (parallel         (+ (codom (mcar x)) (codom (mcadr x))))
+    (swap             (+ (mcar x) (mcadr x)))
+    (one              1)
+    (zero             1)
+    (ident            (mcar x))
+    (drop             0)
+    (branch           (codom (mcar x)))
+    (otherwise
+      (subclass-responsibility x))))

src/bitc/package.lisp

@@ -0,0 +1,46 @@
+(in-package :geb.utils)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;; trans module
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(muffle-package-variance
+ (defpackage #:geb.bitc.trans
+   (:local-nicknames (:vamp :geb.vampir.spec))
+   (:use #:geb.common #:geb.bitc.spec)
+   (:shadowing-import-from #:geb.bitc.spec #:drop #:fork)
+   ))
+
+(in-package :geb.bitc.trans)
+
+(pax:defsection @bitc-trans (:title "Bits (Boolean Circuit) Transformations")
+  "This covers transformation functions from"
+  (to-vampir  pax:generic-function)
+  (to-circuit pax:function))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;; bitc module
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(geb.utils:muffle-package-variance
+ (uiop:define-package #:geb.bitc.main
+   (:use #:geb.common #:geb.mixins)
+   (:shadowing-import-from #:geb.bitc.spec #:drop #:fork)
+   (:use-reexport #:geb.bitc.trans #:geb.bitc.spec)))
+
+(geb.utils:muffle-package-variance
+ (uiop:define-package #:geb.bitc
+   (:use #:geb.common)
+   (:shadowing-import-from #:geb.bitc.spec :fork :drop)
+   (:use-reexport #:geb.bitc.trans #:geb.bitc.spec #:geb.bitc.main)))
+
+(in-package :geb.bitc.main)
+
+(in-package :geb.bitc)
+
+(pax:defsection @bitc-manual (:title "Bits (Boolean Circuit) Specification")
+  "This covers a GEB view of Boolean Circuits. In particular this type will
+be used in translating GEB's view of Boolean Circuits into Vampir"
+  (@bitc              pax:section)
+  (@bitc-constructors pax:section)
+  (@bitc-trans        pax:section))

src/bitc/trans.lisp

@@ -0,0 +1,110 @@
+(in-package :geb.bitc.trans)
+
+(defgeneric to-vampir (morphism values)
+  (:documentation "Turns a BITC term into a Vamp-IR term with a given value"))
+
+(defun to-circuit (morphism name)
+  "Turns a BITC term into a Vamp-IR Gate with the given name"
+  (let* ((wire-count (dom morphism))
+         (wires (loop for i from 1 to wire-count
+                      collect (vamp:make-wire :var (intern (format nil "x~a" i))))))
+    (vamp:make-alias :name name
+                     :inputs wires
+                     :body (to-vampir morphism wires))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Bits to Vampir Implementation
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(defmethod to-vampir ((obj <bitc>) values)
+  (declare (ignore values))
+  (subclass-responsibility obj))
+
+(-> direct-fields-to-list-vampir (geb.mixins:direct-pointwise-mixin) list)
+(defun direct-fields-to-list (obj)
+  (mapcar #'cdr (geb.mixins:to-pointwise-list obj)))
+
+(defun infix-creation (symbol value1 value2)
+  (vamp:make-infix :op symbol
+                   :lhs value1
+                   :rhs value2))
+
+
+(defmethod to-vampir ((obj compose) values)
+  (to-vampir (mcar obj)
+             (to-vampir (mcadr obj) values)))
+
+(defmethod to-vampir ((obj fork) values)
+  ; Copy input n intput bits into 2*n output bits
+  (append values values))
+
+(defmethod to-vampir ((obj parallel) values)
+  ; toElem[par[car_, cadr_]] :=
+  ;   Function[{inp},
+  ;     Module[{cx, inp1, inp2},
+  ;       cx = dom[car];
+  ;       inp1 = inp[[1 ;; cx]];
+  ;       inp2 = inp[[cx + 1 ;; All]];
+  ;       Flatten[{toElem[car][inp1], toElem[cadr][inp2]}, 1]
+  ;   ]]
+
+
+  ; Take n + m bits, execute car the n bits and cadr on the m bits and 
+  ; concat the results from car and cadr
+  (let* ((car (mcar obj))
+         (cadr (mcadr obj))
+         (cx (dom car))
+         (inp1 (subseq values 0 cx))
+         (inp2 (subseq values cx)))
+    (concatenate 'list (to-vampir car inp1) (to-vampir cadr inp2))))
+
+(defmethod to-vampir ((obj swap) values)
+  ; toElem[swap[n_, m_]] := Flatten[{#[[n + 1 ;; All]], #[[1 ;; n]]}, 1] &
+  ; Turn n + m bits into m + n bits by swapping
+  (let ((n (mcar obj)))
+       (append (subseq values (+ 1 n)) (subseq values 0 (+ 1 n)))))
+
+(defmethod to-vampir ((obj one) values)
+  ; toElem[True] := {1} &
+  ; Produce a bitvector of length 1 containing 1
+  (declare (ignore values))
+  (list (vamp:make-constant :const 1)))
+
+(defmethod to-vampir ((obj zero) values)
+  ; toElem[False] := {0} &
+  ; Produce a bitvector of length 1 containing 0
+  (declare (ignore values))
+  (list (vamp:make-constant :const 0)))
+
+(defmethod to-vampir ((obj ident) values)
+  ; toElem[id[_]] := # &
+  ; turn n bits into n bits by doing nothing
+  values)
+
+(defmethod to-vampir ((obj drop) values)
+  ; toElem[drop[_]] := {} &
+  ; turn n bits into an empty bitvector
+  (declare (ignore values))
+  nil)
+
+(defmethod to-vampir ((obj branch) values)
+  ; toElem[branch[f_, g_]][{x_, values__}] :=
+  ;   Thread@Plus[
+  ;     Times[1 - x, #] & /@ toElem[f][{values}],
+  ;     Times[x, #] & /@ toElem[g][{values}]
+  ;   ]
+
+  ; Look at the first bit.
+  ; If its 1, run f on the remaining bits.
+  ; If its 0, run g on the remaining bits.
+  (let* ((x (car values))
+         (xs (cdr values))
+         (f (mcar obj))
+         (g (mcadr obj))
+         (f-elems (to-vampir f xs))
+         (g-elems (to-vampir g xs)))
+    (mapcar #'(lambda (f-elem g-elem)
+                (infix-creation :+
+                  (infix-creation :* (infix-creation :- (vamp:make-constant :const 1) x) f-elem)
+                  (infix-creation :* x g-elem)))
+            f-elems g-elems)))

src/entry/package.lisp

@@ -4,6 +4,7 @@
  (defpackage #:geb.entry
    (:documentation "Entry point for the geb codebase")
    (:local-nicknames  (#:poly #:geb.poly)
+                      (#:bitc #:geb.bitc)
                       (:lambda     :geb.lambda))
    (:use #:serapeum #:common-lisp)))
 

src/geb/package.lisp

@@ -6,7 +6,7 @@
  (defpackage #:geb.main
    (:documentation "Gödel, Escher, Bach categorical model")
    (:use #:common-lisp #:geb.generics #:serapeum #:geb.mixins #:geb.utils #:geb.spec)
-   (:local-nicknames (#:poly #:geb.poly.spec))
+   (:local-nicknames (#:poly #:geb.poly.spec) (#:bitc #:geb.bitc.spec))
    (:shadowing-import-from #:geb.spec :left :right :prod :case)
    (:export :prod :case :mcar :mcadr :mcaddr :mcdr :name :func :obj :dom :codom)))
 
@@ -48,7 +48,7 @@
  (defpackage #:geb.trans
    (:documentation "Gödel, Escher, Bach categorical model")
    (:use #:common-lisp #:serapeum #:geb.mixins #:geb.utils #:geb.spec #:geb.main)
-   (:local-nicknames (#:poly #:geb.poly.spec))
+   (:local-nicknames (#:poly #:geb.poly.spec) (#:bitc #:geb.bitc.spec))
    (:shadowing-import-from #:geb.spec :left :right :prod :case)
    (:export :prod :case :mcar :mcadr :mcaddr :mcdr :name :func :obj)))
 
@@ -58,7 +58,8 @@
   "These cover various conversions from @GEB-SUBSTMORPH and @GEB-SUBSTMU
 into other categorical data structures."
   (to-poly    pax:generic-function)
-  (to-circuit pax:function))
+  (to-circuit pax:function)
+  (to-bitc    pax:generic-function))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;; bool module

src/geb/trans.lisp

@@ -5,6 +5,9 @@
 (defgeneric to-poly (morphism)
   (:documentation "Turns a @GEB-SUBSTMORPH into a POLY:POLY"))
 
+(defgeneric to-bitc (morphism)
+  (:documentation "Turns a @GEB-SUBSTMORPH into a bitc:BITC"))
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Morph to Poly Implementation
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -78,3 +81,77 @@
   "Turns a @GEB-SUBSTMORPH to a Vamp-IR Term"
   (assure list
     (geb.poly:to-circuit (to-poly obj) name)))
+
+
+
+
+
+
+(defmethod to-bitc ((obj <substobj>))
+  (typecase-of substobj obj
+    (so0     0)
+    (so1     0)
+    (coprod  (+ 1 (max (to-bitc (mcar obj)) (to-bitc (mcadr obj)))))
+    (prod    (+ (to-bitc (mcar obj)) (to-bitc (mcadr obj))))
+    (otherwise (subclass-responsibility obj))))
+
+(defmethod to-bitc ((obj <substmorph>))
+  (typecase-of substmorph obj
+    (substobj     (error "impossible"))
+    ;toBits[comp[f__]] := toBits /@ comp[f]
+    (comp          (bitc:compose (to-bitc (mcar obj))
+                                 (to-bitc (mcadr obj))))
+    ; toBits[init[x_]] := par @@ Table[False, bitWidth@x]
+
+    ; This should never occure, but if it does, it produces a constant morphism onto an all 0s vector
+    (init          (apply #'bitc:parallel (make-list (to-bitc (mcar obj)) :initial-element bitc:zero)))
+    ; toBits[terminal[x_]] := drop[bitWidth@x]
+
+    ; Terminal maps any bitvector onto the empty bitvector
+    (terminal      (bitc:drop (to-bitc (mcar obj))))
+    ;toBits[injectLeft[mcar_, mcadr_]] :=
+    ; par @@ Join[{False, id[bitWidth@mcar]}, Table[False, Max[bitWidth@mcar, bitWidth@mcadr] - bitWidth@mcar]]
+
+    ; Inject-left x -> x + y tags the x with a 0, indicating left, and pads the encoded x with as many zeros
+    ;   as would be needed to store either an x or a y.
+    (inject-left   (apply #'bitc:parallel (append (list bitc:zero (bitc:ident (to-bitc (mcar obj))))
+                                                  (make-list (- (max (to-bitc (mcar obj)) (to-bitc (mcadr obj))) (to-bitc (mcar obj))) :initial-element bitc:zero)
+                                          )))
+    ;toBits[injectRight[mcar_,mcadr_]]:=
+    ;  par@@Join[{True,id[bitWidth@mcadr]},Table[False, Max[bitWidth@mcar, bitWidth@mcadr] - bitWidth@mcadr]]
+
+    ; 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.
+    (inject-right  (apply #'bitc:parallel (append (list bitc:one (bitc:ident (to-bitc (mcadr obj)))) 
+                                                  (make-list (- (max (to-bitc (mcar obj)) (to-bitc (mcadr obj))) (to-bitc (mcadr obj))) :initial-element bitc:zero)
+                                          )))
+    ;toBits[case[mcar_,mcadr_]]:=
+    ;  branch[
+    ;    par[toBits@mcar,id[Max[dom@mcar,dom@mcadr]-dom@mcar]],
+    ;    par[toBits@mcadr,id[Max[dom@mcar,dom@mcadr]-dom@mcadr]]
+    ;  ]
+
+    ; Case translates directly into a branch.
+    ; The sub-morphisms of case are padded with drop so they have the same input lengths.
+    (case          (bitc:branch (bitc:parallel (to-bitc (mcar obj))  (bitc:drop (- (max (to-bitc (dom (mcar obj))) (to-bitc (dom (mcadr obj)))) (to-bitc (dom (mcar obj))))))
+                                (bitc:parallel (to-bitc (mcadr obj)) (bitc:drop (- (max (to-bitc (dom (mcar obj))) (to-bitc (dom (mcadr obj)))) (to-bitc (dom (mcadr obj))))))))
+    ; toBits[projectRight[mcar_, mcadr_]] := par[drop[bitWidth@mcar], id[bitWidth@mcadr]]
+
+    ; project-left just drops any bits not being used to encode the first component. 
+    (project-left  (bitc:parallel (bitc:ident (to-bitc (mcar obj))) (bitc:drop (to-bitc (mcadr obj)))))
+    ; toBits[projectLeft[mcar_, mcadr_]] := par[id[bitWidth@mcar], drop[bitWidth@mcadr]]
+
+    ; project-right just drops any bits not being used to encode the second component.
+    (project-right (bitc:parallel (bitc:drop (to-bitc (mcar obj))) (bitc:ident (to-bitc (mcadr obj)))))
+    ; toBits[pair[mcar_, mcdr_]] := comp[par[toBits[mcar], toBits[mcdr]], fork[dom[mcar]]]
+
+    ; Pair will copy the input and run the encoded morphisms in pair on the two copied subvetors.
+    (pair          (bitc:compose (bitc:parallel (to-bitc (mcar obj)) (to-bitc (mcdr obj))) (bitc:fork (to-bitc (dom (mcar obj))))))
+    ;toBits[distribute[mcar_, mcadr_, mcaddr_]] :=
+    ;  par[swap[bitWidth[mcar], 1], id[Max[bitWidth@mcadr, bitWidth@mcaddr]]]
+
+    ; a * (b + c) will be encoded as [a] [0 or 1] [b or c]. By swapping the [0 or 1] with [a], we get an encoding for
+    ; (a * b) + (a * c).
+    (distribute    (bitc:parallel (bitc:swap (to-bitc (mcar obj)) 1) (bitc:ident (max (to-bitc (mcadr obj)) (to-bitc (mcaddr obj))))))
+    (otherwise (subclass-responsibility obj))))
+