Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add method to compile geb to boolean circuits #108

Merged
merged 5 commits into from
May 3, 2023
Merged
Show file tree
Hide file tree
Changes from 3 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions docs/documentation.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@
(@idioms pax:section)
(@geb pax:section)
(@geb-gui-manual pax:section)
(@bitc-manual pax:section)
(@poly-manual pax:section)
(@stlc pax:section)
(@mixins pax:section)
Expand Down
1 change: 1 addition & 0 deletions docs/package.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@
(:import-from #:geb.utils #:@geb-utils-manual)
(:import-from #:geb-test #:@geb-test-manual)
(:import-from #:geb.poly #:@poly-manual)
(:import-from #:geb.bitc #:@bitc-manual)
(:import-from #:geb.specs #:@geb-specs)
(:import-from #:geb.entry #:@geb-entry)
(:import-from #:geb.lambda #:@stlc)
Expand Down
18 changes: 16 additions & 2 deletions geb.asd
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down Expand Up @@ -53,6 +57,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)
Expand All @@ -75,6 +85,8 @@
(:file lambda)
(:file poly)
(:file poly-printer)
(:file bitc)
(:file bitc-printer)
;; HACK: to make the package properly refer to the
;; right symbols
(:file ../util/package)))
Expand All @@ -88,11 +100,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))))
Expand Down Expand Up @@ -131,6 +144,7 @@
(:file lambda)
(:file lambda-conversion)
(:file poly)
(:file bitc)
(:file pipeline)
(:module gui
:serial t
Expand Down
33 changes: 33 additions & 0 deletions src/bitc/bitc.lisp
Original file line number Diff line number Diff line change
@@ -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 (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 (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))))
53 changes: 53 additions & 0 deletions src/bitc/package.lisp
Original file line number Diff line number Diff line change
@@ -0,0 +1,53 @@
(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-circuit (pax:method () (<bitc> t)))
(to-vampir (pax:method () (compose t)))
(to-vampir (pax:method () (fork t)))
(to-vampir (pax:method () (parallel t)))
(to-vampir (pax:method () (swap t)))
(to-vampir (pax:method () (one t)))
(to-vampir (pax:method () (zero t)))
(to-vampir (pax:method () (ident t)))
(to-vampir (pax:method () (drop t)))
(to-vampir (pax:method () (branch t))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; 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))
86 changes: 86 additions & 0 deletions src/bitc/trans.lisp
Original file line number Diff line number Diff line change
@@ -0,0 +1,86 @@
(in-package :geb.bitc.trans)

(defmethod to-circuit ((morphism <bitc>) 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)
:keyword)))))
(vamp:make-alias :name name
:inputs wires
:body (list (vamp:make-tuples :wires (to-vampir morphism wires))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Bits to Vampir Implementation
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defmethod to-vampir ((obj <bitc>) values)
(declare (ignore values))
(subclass-responsibility 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)
"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)))
(append (to-vampir car inp1)
(to-vampir cadr inp2))))

(defmethod to-vampir ((obj swap) values)
"Turn n + m bits into m + n bits by swapping"
(let ((n (mcar obj)))
(append (subseq values n)
(subseq values 0 n))))

(defmethod to-vampir ((obj one) values)
"Produce a bitvector of length 1 containing 1"
(declare (ignore values))
(list (vamp:make-constant :const 1)))

(defmethod to-vampir ((obj zero) values)
"Produce a bitvector of length 1 containing 0"
(declare (ignore values))
(list (vamp:make-constant :const 0)))

(defmethod to-vampir ((obj ident) values)
"turn n bits into n bits by doing nothing"
values)

(defmethod to-vampir ((obj drop) values)
"turn n bits into an empty bitvector"
(declare (ignore values))
nil)

(defmethod to-vampir ((obj branch) 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))
(one (vamp:make-constant :const 1)))
(mapcar (lambda (f-elem g-elem)
(infix-creation :+
(infix-creation :* (infix-creation :- one x) f-elem)
(infix-creation :* x g-elem)))
(to-vampir f xs)
(to-vampir g xs))))
2 changes: 1 addition & 1 deletion src/entry/entry.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,7 @@
(lambda:typed-stlc-type eval)
(lambda:typed-stlc-value eval))))
(vampir
(geb.vampir:extract (list (geb:to-circuit eval vampir-name))))
(geb.vampir:extract (list (to-circuit eval vampir-name))))
(t
(format stream eval)))))

Expand Down
3 changes: 2 additions & 1 deletion src/entry/package.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,9 @@
(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)))
(:use #:geb.common)))


(in-package :geb.entry)
Expand Down
13 changes: 8 additions & 5 deletions src/geb/package.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -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)))

Expand Down Expand Up @@ -47,8 +47,9 @@
(geb.utils:muffle-package-variance
(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))
(:use #:common-lisp #:serapeum #:geb.mixins #:geb.utils #:geb.spec #:geb.main
#:geb.generics)
(: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)))

Expand All @@ -57,8 +58,10 @@
(pax:defsection @geb-translation (:title "Translation Functions")
"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-poly (pax:method () (<substobj>)))
(to-poly (pax:method () (<substmorph>)))
(to-circuit (pax:method () (<substmorph> t)))
(to-bitc (pax:method () (<substmorph>))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; bool module
Expand Down
Loading