diff --git a/docs/documentation.lisp b/docs/documentation.lisp index 22f157d1b..841c65808 100644 --- a/docs/documentation.lisp +++ b/docs/documentation.lisp @@ -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) diff --git a/docs/package.lisp b/docs/package.lisp index b2d75921b..c78e43f33 100644 --- a/docs/package.lisp +++ b/docs/package.lisp @@ -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) diff --git a/geb.asd b/geb.asd index f77c410c6..b3ac2fde3 100644 --- a/geb.asd +++ b/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" @@ -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) @@ -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))) @@ -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)))) @@ -131,6 +144,7 @@ (:file lambda) (:file lambda-conversion) (:file poly) + (:file bitc) (:file pipeline) (:module gui :serial t diff --git a/src/bitc/bitc.lisp b/src/bitc/bitc.lisp new file mode 100644 index 000000000..5645edde9 --- /dev/null +++ b/src/bitc/bitc.lisp @@ -0,0 +1,103 @@ +(in-package :geb.bitc.main) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Domain and codomain definitions +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defmethod dom ((x )) + "Gives the length of the bit vector the [\\] moprhism takes" + (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 )) + "Gives the length of the bit vector the [\\] morphism returns" + (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)))) + + +(defmethod gapply ((morphism ) (object bit-vector)) + "My My main documentation can be found on [GAPPLY][generic-function] + +I am the [GAPPLY][generic-function] for [\\][class], the +OBJECT that I expect is of type NUMBER. [GAPPLY][generic-function] +reduces down to ordinary common lisp expressions rather straight +forwardly + +```lisp +;; figure out the number of bits the function takes +GEB-TEST> (dom (to-bitc geb-bool:and)) +2 (2 bits, #x2, #o2, #b10) +GEB-TEST> (gapply (to-bitc geb-bool:and) #*11) +#*1 +GEB-TEST> (gapply (to-bitc geb-bool:and) #*10) +#*0 +GEB-TEST> (gapply (to-bitc geb-bool:and) #*01) +#*0 +GEB-TEST> (gapply (to-bitc geb-bool:and) #*00) +#*0 +```" + ;; use a non copying version of subseq some time + (etypecase-of bitc morphism + (compose (gapply (mcar morphism) + (gapply (mcadr morphism) object))) + (fork (concatenate 'bit-vector object object)) + (ident object) + (one #*1) + (zero #*0) + (drop #*) + (swap + (let ((n (mcar morphism))) + (concatenate 'bit-vector (subseq object 0) (subseq object 0 n)))) + (parallel + (let* ((cx (dom (mcar morphism))) + (inp1 (subseq object 0 cx)) + (inp2 (subseq object cx))) + (concatenate 'bit-vector + (gapply (mcar morphism) inp1) + (gapply (mcadr morphism) inp2)))) + (branch + (let ((without-first-bit (subseq object 1))) + (if (zerop (bit object 0)) + (gapply (mcar morphism) without-first-bit) + (gapply (mcadr morphism) without-first-bit)))))) + +(defmethod gapply ((morphism ) (object list)) + "I am a helper gapply function, where the second argument for +[\\] is a list. See the docs for the BIT-VECTOR version for +the proper one. We do allow sending in a list like so + +```lisp +;; figure out the number of bits the function takes +GEB-TEST> (dom (to-bitc geb-bool:and)) +2 (2 bits, #x2, #o2, #b10) +GEB-TEST> (gapply (to-bitc geb-bool:and) (list 1 1)) +#*1 +GEB-TEST> (gapply (to-bitc geb-bool:and) (list 1 0)) +#*0 +GEB-TEST> (gapply (to-bitc geb-bool:and) (list 0 1)) +#*0 +GEB-TEST> (gapply (to-bitc geb-bool:and) (list 0 0)) +#*0 +``` +" + (gapply morphism (coerce object 'bit-vector))) diff --git a/src/bitc/package.lisp b/src/bitc/package.lisp new file mode 100644 index 000000000..9386522b5 --- /dev/null +++ b/src/bitc/package.lisp @@ -0,0 +1,61 @@ +(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 () ( 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) + +(pax:defsection @bitc-api (:title "Bits (Boolean Circuit) API") + "This covers the Bits (Boolean Circuit) API" + (gapply (pax:method () ( bit-vector))) + (gapply (pax:method () ( list))) + (dom (pax:method () ())) + (codom (pax:method () ()))) + +(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-api pax:section) + (@bitc-trans pax:section)) diff --git a/src/bitc/trans.lisp b/src/bitc/trans.lisp new file mode 100644 index 000000000..0d49a9d46 --- /dev/null +++ b/src/bitc/trans.lisp @@ -0,0 +1,86 @@ +(in-package :geb.bitc.trans) + +(defmethod 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) + :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 ) 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 0, run f on the remaining bits. + + If its 1, 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)))) diff --git a/src/entry/entry.lisp b/src/entry/entry.lisp index 111416fe5..b1eb1d7b6 100644 --- a/src/entry/entry.lisp +++ b/src/entry/entry.lisp @@ -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))))) diff --git a/src/entry/package.lisp b/src/entry/package.lisp index 4999f304d..375ddf34c 100644 --- a/src/entry/package.lisp +++ b/src/entry/package.lisp @@ -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) diff --git a/src/geb/package.lisp b/src/geb/package.lisp index 6b40ad28f..f27be78d1 100644 --- a/src/geb/package.lisp +++ b/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))) @@ -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))) @@ -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 () ())) + (to-poly (pax:method () ())) + (to-circuit (pax:method () ( t))) + (to-bitc (pax:method () ()))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; bool module diff --git a/src/geb/trans.lisp b/src/geb/trans.lisp index 2abfe4e83..9673b1b20 100644 --- a/src/geb/trans.lisp +++ b/src/geb/trans.lisp @@ -2,9 +2,6 @@ (in-package :geb.trans) -(defgeneric to-poly (morphism) - (:documentation "Turns a @GEB-SUBSTMORPH into a POLY:POLY")) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Morph to Poly Implementation ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -73,8 +70,117 @@ (defun obj-to-nat (obj) (so-card-alg obj)) -(-> to-circuit ( keyword) geb.vampir.spec:statement) -(defun to-circuit (obj name) +(defmethod to-circuit ((obj ) name) "Turns a @GEB-SUBSTMORPH to a Vamp-IR Term" (assure geb.vampir.spec:statement - (geb.poly:to-circuit (to-poly obj) name))) + (to-circuit (to-bitc obj) name))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Morph to Bitc Implementation +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defmethod bitwidth ((obj )) + (typecase-of substobj obj + (so0 0) + (so1 0) + (coprod (+ 1 (max (bitwidth (mcar obj)) (bitwidth (mcadr obj))))) + (prod (+ (bitwidth (mcar obj)) (bitwidth (mcadr obj)))) + (otherwise (subclass-responsibility obj)))) + +(defmethod to-bitc ((obj )) + (typecase-of substmorph obj + (substobj + (bitc:ident (bitwidth obj))) + (comp + (bitc:compose (to-bitc (mcar obj)) + (to-bitc (mcadr obj)))) + ;; This should never occure, but if it does, it produces a + ;; constant morphism onto an all 0s list + (init + (let* ((list (zero-list (bitwidth (mcar obj)))) + (len (length list))) + (cond ((= 0 len) (bitc:drop 0)) + ((= 1 len) bitc:zero) + (t (apply #'bitc:parallel list))))) + ;; Terminal maps any bit-list onto the empty bit-list + (terminal + (bitc:drop (bitwidth (mcar obj)))) + + ;; 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 + (let ((car-width (bitwidth (mcar obj))) + (cadr-width (bitwidth (mcadr obj)))) + (apply #'bitc:parallel + (append (list bitc:zero (bitc:ident car-width)) + (zero-list (padding-bits cadr-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. + (inject-right + (let ((car-width (bitwidth (mcar obj))) + (cadr-width (bitwidth (mcadr obj)))) + (apply #'bitc:parallel + (append (list bitc:one (bitc:ident cadr-width)) + (zero-list (padding-bits car-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. + (case + (let ((car-width (bitwidth (dom (mcar obj)))) + (cadr-width (bitwidth (dom (mcadr obj))))) + (bitc:branch (bitc:parallel (to-bitc (mcar obj)) + (bitc:drop + (padding-bits cadr-width car-width))) + (bitc:parallel (to-bitc (mcadr obj)) + (bitc:drop + (padding-bits car-width cadr-width)))))) + ;; project-left just drops any bits not being used to encode the + ;; first component. + (project-left + (bitc:parallel (bitc:ident (bitwidth (mcar obj))) + (bitc:drop (bitwidth (mcadr obj))))) + + ;; project-right just drops any bits not being used to encode the + ;; second component. + (project-right + (bitc:parallel (bitc:drop (bitwidth (mcar obj))) + (bitc:ident (bitwidth (mcadr obj))))) + + ;; 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 (bitwidth (dom (mcar obj)))))) + ;; 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 (bitwidth (mcar obj)) 1) + (bitc:ident (max (bitwidth (mcadr obj)) + (bitwidth (mcaddr obj)))))) + (otherwise (subclass-responsibility obj)))) + +(defun zero-list (length) + (make-list length :initial-element bitc:zero)) + +(-> padding-bits ((integer 0) (integer 0)) (integer 0)) +(defun padding-bits (number number2) + " +```lisp +(max number number2) +``` +is the bits needed to store NUMBER or NUMBER2 + +Thus if we want to calculate the number of padding bits needed then we +should calculate + +```lisp +(- (max number number2) number2) +``` + +We use an optimized version in actual code, which happens to compute the same result" + (max (- number number2) 0)) diff --git a/src/generics/generics.lisp b/src/generics/generics.lisp index ff075ae93..02d72e50c 100644 --- a/src/generics/generics.lisp +++ b/src/generics/generics.lisp @@ -1,6 +1,5 @@ (in-package :geb.generics) - (defgeneric gapply (morphism object) (:documentation "Applies a given Moprhism to a given object. @@ -23,3 +22,30 @@ GEB> (gapply (comp (right so1)) (left s-1) ```")) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Conversion functions +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defgeneric to-bitc (morphism) + (:documentation + "Turns a given MORPHISM into a [GEB.BITC.SPEC:BITC]")) + +(defgeneric to-poly (morphism) + (:documentation + "Turns a given MORPHISM into a [GEB.POLY.SPEC:POLY]")) + +(defgeneric to-circuit (morphism name) + (:documentation + "Turns a MORPHISM into a Vampir circuit. the NAME is the given name of +the output circuit.")) + +(defgeneric to-vampir (morphism values) + (:documentation + "Turns a MORPHISM into a Vampir circuit, with concrete values. + +The more natural interface is [TO-CIRCUIT], however this is a more low +level interface into what the polynomial categories actually +implement, and thus can be extended or changed. + +The VALUES are likely vampir values in a list.")) diff --git a/src/generics/package.lisp b/src/generics/package.lisp index 7e20aa660..f53b2628b 100644 --- a/src/generics/package.lisp +++ b/src/generics/package.lisp @@ -12,4 +12,8 @@ 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)) + (gapply pax:generic-function) + (to-circuit pax:generic-function) + (to-bitc pax:generic-function) + (to-poly pax:generic-function) + (to-vampir pax:generic-function)) diff --git a/src/lambda/package.lisp b/src/lambda/package.lisp index 033c62cdd..b074438b5 100644 --- a/src/lambda/package.lisp +++ b/src/lambda/package.lisp @@ -24,7 +24,7 @@ (geb.utils:muffle-package-variance (uiop:define-package #:geb.lambda.trans (:documentation "A basic lambda translator into other parts of geb") - (:shadow #:to-poly #:to-circuit) + (:shadow #:to-poly #:to-circuit #:to-bitc) (:mix #:geb.lambda.spec #:geb.common #:common-lisp :geb.lambda.main))) (in-package #:geb.lambda.trans) @@ -39,6 +39,7 @@ data types" (compile-checked-term pax:generic-function) (to-poly pax:function) + (to-bitc pax:function) (to-circuit pax:function) (@utility pax:section)) diff --git a/src/lambda/trans.lisp b/src/lambda/trans.lisp index cd7aff7a9..40de285a6 100644 --- a/src/lambda/trans.lisp +++ b/src/lambda/trans.lisp @@ -11,18 +11,22 @@ (defgeneric compile-checked-term (context type term) (:documentation "Compiles a checked term into SubstMorph category")) -(-> to-poly (list t ) (or geb.poly: geb.poly:poly)) +(-> to-poly (list t ) t) +(defun to-bitc (context type obj) + (~>> obj + (compile-checked-term context type) + geb.common:to-bitc)) + (defun to-poly (context type obj) - (assure (or geb.poly: geb.poly:poly) - (~>> obj - (compile-checked-term context type) - geb:to-poly))) + (~>> obj + (compile-checked-term context type) + geb.common:to-poly)) (-> to-circuit (list t keyword) geb.vampir.spec:statement) (defun to-circuit (context type obj name) (assure geb.vampir.spec:statement - (~> (to-poly context type obj) - (geb.poly:to-circuit name)))) + (~> (to-bitc context type obj) + (geb.common:to-circuit name)))) (defmethod empty ((class (eql (find-class 'list)))) nil) diff --git a/src/poly/package.lisp b/src/poly/package.lisp index d862c6a54..84dcd21d3 100644 --- a/src/poly/package.lisp +++ b/src/poly/package.lisp @@ -14,8 +14,17 @@ (pax:defsection @poly-trans (:title "Polynomial Transformations") "This covers transformation functions from" - (to-vampir pax:generic-function) - (to-circuit pax:function)) + (to-circuit (pax:method () ( t))) + (to-vampir (pax:method () (integer t))) + (to-vampir (pax:method () (ident t))) + (to-vampir (pax:method () (+ t))) + (to-vampir (pax:method () (* t))) + (to-vampir (pax:method () (- t))) + (to-vampir (pax:method () (/ t))) + (to-vampir (pax:method () (compose t))) + (to-vampir (pax:method () (if-zero t))) + (to-vampir (pax:method () (if-lt t))) + (to-vampir (pax:method () (mod t)))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; poly module diff --git a/src/poly/trans.lisp b/src/poly/trans.lisp index d19a7b83b..e39288a8b 100644 --- a/src/poly/trans.lisp +++ b/src/poly/trans.lisp @@ -1,10 +1,15 @@ (in-package :geb.poly.trans) -(defgeneric to-vampir (morphism value) - (:documentation "Turns a POLY term into a Vamp-IR term with a given value")) - -(defun to-circuit (morphism name) +(defmethod to-circuit ((morphism ) name) "Turns a POLY term into a Vamp-IR Gate with the given name" + (circuit-gen morphism name)) + +(defmethod to-circuit ((morphism integer) name) + "Turns a POLY term into a Vamp-IR Gate with the given name, by just +returning the value" + (circuit-gen morphism name)) + +(defun circuit-gen (morphism name) (let ((wire (vamp:make-wire :var :x))) (vamp:make-alias :name name :inputs (list wire) diff --git a/src/specs/bitc-printer.lisp b/src/specs/bitc-printer.lisp new file mode 100644 index 000000000..186671ba8 --- /dev/null +++ b/src/specs/bitc-printer.lisp @@ -0,0 +1,26 @@ +(in-package #:geb.bitc.spec) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Subst Constructor Printer +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; we are going to be super lazy about this, just make a format +(defmacro easy-printer (class-name) + `(defmethod print-object ((obj ,class-name) stream) + (format stream "~A" + (cons ',class-name + (mapcar #'cdr (geb.mixins:to-pointwise-list obj)))))) + +(easy-printer compose) +(easy-printer fork) +(easy-printer parallel) +(easy-printer swap) +(easy-printer one) +(easy-printer zero) +(easy-printer ident) +(easy-printer drop) +(easy-printer branch) + +(defmethod print-object ((obj ident) stream) + (print-unreadable-object (obj stream :type nil :identity nil) + (format stream "IDENT"))) diff --git a/src/specs/bitc.lisp b/src/specs/bitc.lisp new file mode 100644 index 000000000..da5aa84b0 --- /dev/null +++ b/src/specs/bitc.lisp @@ -0,0 +1,184 @@ +(in-package #:geb.bitc.spec) + +(deftype bitc () + `(or compose fork parallel swap one zero ident drop branch)) + +(defclass (geb.mixins:direct-pointwise-mixin cat-morph) ()) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Constructor Morphisms for Bits (Objects are just natural numbers) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defclass compose () + ((mcar :initarg :mcar + :accessor mcar + :documentation "") + (mcadr :initarg :mcadr + :accessor mcadr + :documentation "")) + (:documentation "composes the MCAR and the MCADR")) + +(defclass fork () + ((mcar :initarg :mcar + :accessor mcar + :documentation "")) + (:documentation "Copies the MCAR of length n onto length 2*n by copying its +inputs (MCAR).")) + +(defclass parallel () + ((mcar :initarg :mcar + :accessor mcar + :documentation "") + (mcadr :initarg :mcadr + :accessor mcadr + :documentation "")) + (:documentation + " +```lisp +(parallel x y) +``` + +constructs a [PARALLEL][class] term where the [MCAR] is `x` and the +[MCADR] is `y`, + +where if + +``` +x : a → b, y : c → d +------------------------------- +(parallel x y) : a + c → b + d +``` + +then the [PARALLEL][class] will return a function from a and c to b +and d where the [MCAR] and [MCADR] run on subvectors of the input.")) + +(defclass swap () + ((mcar :initarg :mcar + :accessor mcar + :documentation "") + (mcadr :initarg :mcadr + :accessor mcadr + :documentation "")) + (:documentation + " +```lisp +(swap n m) +``` + +binds the [MCAR] to n and [MCADR] to m, where if the input +vector is of length `n + m`, then it swaps the bits, algebraically we +view it as + +```lisp +(swap n m) : #*b₁...bₙbₙ₊₁...bₙ₊ₘ → #*bₙ₊₁...bₘ₊ₙb₁...bₙ +```")) + +(defclass one () + () + (:documentation + "[ONE][class] represents the map from 0 onto 1 producing a vector + with only 1 in it.")) + +(defclass zero () + () + (:documentation + "[ZERO] map from 0 onto 1 producing a vector with only 0 in + it.")) + +(defclass ident () + ((mcar :initarg :mcar + :accessor mcar + :documentation "")) + (:documentation + "[IDENT] represents the identity")) + +(defclass drop () + ((mcar :initarg :mcar + :accessor mcar + :documentation "")) + (:documentation + "[DROP] represents the unique morphism from n to 0.")) + +(defclass branch () + ((mcar :initarg :mcar + :accessor mcar + :documentation "") + (mcadr :initarg :mcadr + :accessor mcadr + :documentation "")) + (:documentation + " +```lisp +(branch x y) +``` + +constructs a [BRANCH][class] term where the [MCAR] is `x` and the +[MCADR] is `y`, + +where if + +``` +x : a → b, y : a → b +------------------------------- +(branch x y) : 1+a → b +``` + +then the [BRANCH] will return a function on the type `1 + a`, where the +1 represents a bit to branch on. If the first bit is `0`, then the +[MCAR] is ran, however if the bit is `1`, then the [MCADR] is ran.")) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Constructors +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defmacro make-multi (constructor) + `(defun ,constructor (mcar mcadr &rest args) + ,(format nil "Creates a multiway constructor for [~A]" constructor) + (reduce (lambda (x y) + (make-instance ',constructor :mcar x :mcadr y)) + (list* mcar mcadr args) + :from-end t))) + +(make-multi parallel) +(make-multi compose) + +(defun fork (mcar) + "FORK ARG1" + (make-instance 'fork :mcar mcar)) + +(defun swap (mcar mcadr) + "swap ARG1 and ARG2" + (make-instance 'swap :mcar mcar :mcadr mcadr)) + +(serapeum:def one + (make-instance 'one)) + +(serapeum:def zero + (make-instance 'zero)) + +(defun ident (mcar) + "ident ARG1" + (make-instance 'ident :mcar mcar)) + +(defun drop (mcar) + "drop ARG1" + (make-instance 'drop :mcar mcar)) + +(defun branch (mcar mcadr) + "branch with ARG1 or ARG2" + (make-instance 'branch :mcar mcar :mcadr mcadr)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Pattern Matching +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; Ι don't do multi way pattern matching yet :( +(make-pattern compose mcar mcadr) +(make-pattern fork mcar) +(make-pattern parallel mcar mcadr) +(make-pattern swap mcar mcadr) +(make-pattern ident mcar) +(make-pattern drop mcar) +(make-pattern branch mcar mcadr) +(make-pattern one) +(make-pattern zero) diff --git a/src/specs/package.lisp b/src/specs/package.lisp index 45c654d0e..2d868dcac 100644 --- a/src/specs/package.lisp +++ b/src/specs/package.lisp @@ -9,6 +9,12 @@ (:shadow :+ :* :/ :- :mod) (:use #:geb.utils #:cl))) +(muffle-package-variance + (defpackage #:geb.bitc.spec + (:export :dom :codom) + (:shadow :drop :fork) + (:use #:geb.utils #:cl #:geb.mixins))) + ;; please document this later. (muffle-package-variance (uiop:define-package #:geb.lambda.spec @@ -90,6 +96,39 @@ constructors" (if-zero pax:function) (if-lt pax:function)) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Geb Bits Package Documentation +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(in-package :geb.bitc.spec) + +(pax:defsection @bitc (:title "Bits Types") + "This section covers the types of things one can find in the [BITS] +constructors" + (bitc pax:type) + ( pax:class) + (compose pax:class) + (fork pax:class) + (parallel pax:class) + (swap pax:class) + (one pax:class) + (zero pax:class) + (ident pax:class) + (drop pax:class) + (branch pax:class)) + +(pax:defsection @bitc-constructors (:title "Bits (Boolean Circuit) Constructors") + "Every accessor for each of the CLASS's found here are from @GEB-ACCESSORS" + (compose pax:function) + (fork pax:function) + (parallel pax:function) + (swap pax:function) + (one pax:symbol-macro) + (zero pax:symbol-macro) + (ident pax:function) + (drop pax:function) + (branch pax:function)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Geb lambda Package Documentation ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/src/specs/poly-printer.lisp b/src/specs/poly-printer.lisp index 345e1f81c..5cacdd524 100644 --- a/src/specs/poly-printer.lisp +++ b/src/specs/poly-printer.lisp @@ -40,9 +40,9 @@ ;; we are going to be super lazy about this, just make a format (defmacro easy-printer (class-name) `(defmethod print-object ((obj ,class-name) stream) - (print-object (cons ',class-name - (mapcar #'cdr (geb.mixins:to-pointwise-list obj))) - stream))) + (format stream "~A" + (cons ',class-name + (mapcar #'cdr (geb.mixins:to-pointwise-list obj)))))) (easy-printer +) (easy-printer -) diff --git a/test/bitc.lisp b/test/bitc.lisp new file mode 100644 index 000000000..d1a9a4077 --- /dev/null +++ b/test/bitc.lisp @@ -0,0 +1,30 @@ +(in-package :geb-test) + +(define-test geb-bitc :parent geb-test-suite) + +(def bitc-circuit-1 + (bitc:compose (bitc:branch + (bitc:parallel (bitc:compose (bitc:parallel bitc:zero + (bitc:ident 0)) + (bitc:drop 1)) + (bitc:ident 0)) + (bitc:parallel (bitc:parallel (bitc:ident 1) + (bitc:drop 0)) + (bitc:ident 0))) + (bitc:parallel (bitc:swap 1 1) + (bitc:ident 0)))) + +(def test-circuit-1 + (to-circuit bitc-circuit-1 :tc_1)) + +(define-test vampir-converter + :parent geb-bitc + (of-type geb.vampir.spec:alias test-circuit-1)) + + +(define-test bitc-evaluates-and-correctly + :parent geb-bitc + (is equalp #*1 (gapply (to-bitc geb-bool:and) #*11)) + (is equalp #*0 (gapply (to-bitc geb-bool:and) #*10)) + (is equalp #*0 (gapply (to-bitc geb-bool:and) #*01)) + (is equalp #*0 (gapply (to-bitc geb-bool:and) #*00))) diff --git a/test/geb.lisp b/test/geb.lisp index 58aa976e6..a6bf6e9f8 100644 --- a/test/geb.lisp +++ b/test/geb.lisp @@ -100,9 +100,11 @@ (def test-morph-2 (<-left so1 geb-bool:bool)) -(def test-poly-2 (geb:to-poly test-morph-2)) +(def test-poly-2 (to-poly test-morph-2)) -(def test-circuit-2 (geb:to-circuit test-morph-2 :tc_2)) +(def test-bitc-2 (to-bitc test-morph-2)) + +(def test-circuit-2 (to-circuit test-morph-2 :tc_2)) (define-test vampir-test-2 :parent geb-trans diff --git a/test/package.lisp b/test/package.lisp index 60885f89d..229c7a564 100644 --- a/test/package.lisp +++ b/test/package.lisp @@ -4,6 +4,7 @@ (:shadowing-import-from :serapeum :true) (:shadow :value :children) (:local-nicknames (#:poly #:geb.poly) + (#:bitc #:geb.bitc) (#:lambda #:geb.lambda)) (:use #:geb.common #:parachute)) diff --git a/test/poly.lisp b/test/poly.lisp index 65830041d..63d3f7489 100644 --- a/test/poly.lisp +++ b/test/poly.lisp @@ -3,17 +3,17 @@ (define-test geb-poly :parent geb-test-suite) (def test-circuit-1 - (poly:to-circuit (poly:+ 1 (poly:+ poly:ident (poly:* 3 poly:ident))) + (to-circuit (poly:+ 1 (poly:+ poly:ident (poly:* 3 poly:ident))) :tc_1)) (def test-circuit-2 - (poly:to-circuit (poly:if-lt (poly:+ 2 (poly:+ poly:ident (poly:* 3 poly:ident))) - (poly:+ 1 (poly:+ poly:ident (poly:* 3 poly:ident))) - 5 - 8) - :foo)) + (to-circuit (poly:if-lt (poly:+ 2 (poly:+ poly:ident (poly:* 3 poly:ident))) + (poly:+ 1 (poly:+ poly:ident (poly:* 3 poly:ident))) + 5 + 8) + :foo)) -(define-test vampir-converter +(define-test poly-vampir-converter :parent geb-poly (of-type geb.vampir.spec:alias test-circuit-1) (of-type geb.vampir.spec:alias test-circuit-2))