From 6cfb13c22dccc9a0a07cd8d0faf225b4afd4f085 Mon Sep 17 00:00:00 2001 From: Anthony Hart Date: Tue, 25 Apr 2023 00:55:06 -0700 Subject: [PATCH 1/4] Added Bitc polynomial backend and transformation to vampir Adds category of boolean circuits (BITC). The objects in this category are just natural numbers representing the type of bit vectors of a certain length. There are nine methods for constructing morphisms; - (compose x y), which composes morphisms x and y. - (ident n), which is the identity on n. - (fork n), which maps n onto 2*n by copying its inputs. - (parallel x y), which (if x : a -> b and y : c -> d) will be a morphism from a + c -> b + d, running x and y on subvectors. - (swap n m), which maps n + m onto m + n by swapping. - ONE, which represents the map from 0 onto 1 producing a vector with only 1 in it. - ZERO, which represents the map from 0 onto 1 producing a vector with only 0 in it. - (drop n), which represents the unique morphism from n to 0. - (branch x y), which (if x : a -> b and y : a -> b) maps 1+a to b by splitting on the first bit to decide which morphism to apply to the remaining bits. There are other ways to formulate this category, but I think this particular formulation is quite convenient. I've implemented a `to-bitc` function in geb.trans which translates geb objects and morphisms into bitc objects and morphisms. Additionally, I've implemented a `to-vampir` function in bitc.trans which translates a bit morphism into a vampire morphism. I'm not sure what else is needed, but the core implementation is done for now. In the future, this should be extended to a category whose objects represent vectors over some finite set other than the booleans. The reason I didn't do that hear is because coproducts are only binary and there aren't finite sets beyond so0 and so1, so bitvectors are quite natural and using anything else would require post-hoc optimization, but future versions of geb may want more. Also, I'd like to know what, if any, performance benefits this gives over the univariate polynomial formulation. I didn't test that. --- docs/documentation.lisp | 1 + docs/package.lisp | 1 + geb.asd | 18 +++- src/bitc/bitc.lisp | 33 +++++++ src/bitc/package.lisp | 54 +++++++++++ src/bitc/trans.lisp | 89 +++++++++++++++++ src/entry/package.lisp | 1 + src/geb/package.lisp | 7 +- src/geb/trans.lisp | 110 +++++++++++++++++++++ src/specs/bitc-printer.lisp | 26 +++++ src/specs/bitc.lisp | 184 ++++++++++++++++++++++++++++++++++++ src/specs/package.lisp | 39 ++++++++ src/specs/poly-printer.lisp | 6 +- test/bitc.lisp | 21 ++++ test/geb.lisp | 2 + test/package.lisp | 1 + 16 files changed, 585 insertions(+), 8 deletions(-) create mode 100644 src/bitc/bitc.lisp create mode 100644 src/bitc/package.lisp create mode 100644 src/bitc/trans.lisp create mode 100644 src/specs/bitc-printer.lisp create mode 100644 src/specs/bitc.lisp create mode 100644 test/bitc.lisp 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 fd0baef65..d1495eb04 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" @@ -46,6 +50,12 @@ :description "Polynomial" :depends-on (util geb vampir specs) :components ((:file package))) + (: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) @@ -68,6 +78,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))) @@ -81,11 +93,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)))) @@ -124,6 +137,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..158abe4cf --- /dev/null +++ b/src/bitc/bitc.lisp @@ -0,0 +1,33 @@ +(in-package :geb.bitc.main) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Domain and codomain definitions +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defmethod dom ((x )) + (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 )) + (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)))) diff --git a/src/bitc/package.lisp b/src/bitc/package.lisp new file mode 100644 index 000000000..c747e4045 --- /dev/null +++ b/src/bitc/package.lisp @@ -0,0 +1,54 @@ +(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:function) + (to-vampir pax:generic-function) + (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)) diff --git a/src/bitc/trans.lisp b/src/bitc/trans.lisp new file mode 100644 index 000000000..c2b52874e --- /dev/null +++ b/src/bitc/trans.lisp @@ -0,0 +1,89 @@ +(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) + :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 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)))) diff --git a/src/entry/package.lisp b/src/entry/package.lisp index 4999f304d..787ae3b58 100644 --- a/src/entry/package.lisp +++ b/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))) diff --git a/src/geb/package.lisp b/src/geb/package.lisp index 0d68f27e4..3d76001f9 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 #: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 diff --git a/src/geb/trans.lisp b/src/geb/trans.lisp index 2abfe4e83..73fe38787 100644 --- a/src/geb/trans.lisp +++ b/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,110 @@ "Turns a @GEB-SUBSTMORPH to a Vamp-IR Term" (assure geb.vampir.spec:statement (geb.poly:to-circuit (to-poly 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 + (apply #'bitc:parallel (zero-list (bitwidth (mcar obj))))) + ;; 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/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..849b2f98d --- /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 `1`, then the +[MCAR] is ran, however if the bit is `0`, 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 7c7105964..ccb8c630c 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..a55c2a110 --- /dev/null +++ b/test/bitc.lisp @@ -0,0 +1,21 @@ +(in-package :geb-test) + +(define-test geb-bitc :parent geb-test-suite) + +(def test-circuit-1 + (bitc:to-circuit + (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))) + :tc_1)) + +(define-test vampir-converter + :parent geb-bitc + (of-type geb.vampir.spec:alias test-circuit-1)) diff --git a/test/geb.lisp b/test/geb.lisp index 453c87257..dc7757658 100644 --- a/test/geb.lisp +++ b/test/geb.lisp @@ -102,6 +102,8 @@ (def test-poly-2 (geb:to-poly test-morph-2)) +(def test-bitc-2 (geb:to-bitc test-morph-2)) + (def test-circuit-2 (geb:to-circuit test-morph-2 :tc_2)) (define-test vampir-test-2 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)) From 10e3c1b669b17c13ffb45363cd65bb9712c80915 Mon Sep 17 00:00:00 2001 From: mariari Date: Tue, 2 May 2023 15:11:51 +0800 Subject: [PATCH 2/4] Move transition functions to the generics package This fixes the trans loading order issues, and allows the bitc and poly backends to share the same method name along with other parts of the codebase being more properly abstracted --- src/bitc/package.lisp | 3 +-- src/bitc/trans.lisp | 5 +---- src/entry/entry.lisp | 2 +- src/entry/package.lisp | 2 +- src/geb/package.lisp | 10 ++++++---- src/geb/trans.lisp | 12 ++---------- src/generics/generics.lisp | 28 +++++++++++++++++++++++++++- src/generics/package.lisp | 6 +++++- src/lambda/trans.lisp | 4 ++-- src/poly/package.lisp | 13 +++++++++++-- src/poly/trans.lisp | 13 +++++++++---- test/bitc.lisp | 2 +- test/geb.lisp | 6 +++--- test/poly.lisp | 12 ++++++------ 14 files changed, 76 insertions(+), 42 deletions(-) diff --git a/src/bitc/package.lisp b/src/bitc/package.lisp index c747e4045..59b76f897 100644 --- a/src/bitc/package.lisp +++ b/src/bitc/package.lisp @@ -14,8 +14,7 @@ (pax:defsection @bitc-trans (:title "Bits (Boolean Circuit) Transformations") "This covers transformation functions from" - (to-circuit pax:function) - (to-vampir pax:generic-function) + (to-circuit (pax:method () ( t))) (to-vampir (pax:method () (compose t))) (to-vampir (pax:method () (fork t))) (to-vampir (pax:method () (parallel t))) diff --git a/src/bitc/trans.lisp b/src/bitc/trans.lisp index c2b52874e..998ea16f5 100644 --- a/src/bitc/trans.lisp +++ b/src/bitc/trans.lisp @@ -1,9 +1,6 @@ (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) +(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 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 787ae3b58..375ddf34c 100644 --- a/src/entry/package.lisp +++ b/src/entry/package.lisp @@ -6,7 +6,7 @@ (: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 12ca1f9fa..f27be78d1 100644 --- a/src/geb/package.lisp +++ b/src/geb/package.lisp @@ -47,7 +47,8 @@ (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) + (: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,9 +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-bitc pax:generic-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 73fe38787..db1a4e3fd 100644 --- a/src/geb/trans.lisp +++ b/src/geb/trans.lisp @@ -2,12 +2,6 @@ (in-package :geb.trans) -(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 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -76,12 +70,10 @@ (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-poly obj) name))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Morph to Bitc Implementation 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/trans.lisp b/src/lambda/trans.lisp index cd7aff7a9..f97c793de 100644 --- a/src/lambda/trans.lisp +++ b/src/lambda/trans.lisp @@ -16,13 +16,13 @@ (assure (or geb.poly: geb.poly:poly) (~>> obj (compile-checked-term context type) - geb:to-poly))) + 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)))) + (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/test/bitc.lisp b/test/bitc.lisp index a55c2a110..4fa46c461 100644 --- a/test/bitc.lisp +++ b/test/bitc.lisp @@ -3,7 +3,7 @@ (define-test geb-bitc :parent geb-test-suite) (def test-circuit-1 - (bitc:to-circuit + (to-circuit (bitc:compose (bitc:branch (bitc:parallel (bitc:compose (bitc:parallel bitc:zero (bitc:ident 0)) diff --git a/test/geb.lisp b/test/geb.lisp index 6d4fc939c..a6bf6e9f8 100644 --- a/test/geb.lisp +++ b/test/geb.lisp @@ -100,11 +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-bitc-2 (geb:to-bitc test-morph-2)) +(def test-bitc-2 (to-bitc test-morph-2)) -(def test-circuit-2 (geb:to-circuit test-morph-2 :tc_2)) +(def test-circuit-2 (to-circuit test-morph-2 :tc_2)) (define-test vampir-test-2 :parent geb-trans diff --git a/test/poly.lisp b/test/poly.lisp index 65830041d..77377b003 100644 --- a/test/poly.lisp +++ b/test/poly.lisp @@ -3,15 +3,15 @@ (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 :parent geb-poly From 54d6f7563bcfef1b9edee71bdcc1a14e682dd30c Mon Sep 17 00:00:00 2001 From: mariari Date: Tue, 2 May 2023 16:08:32 +0800 Subject: [PATCH 3/4] Implement an interpreter for bitc we implement gapply for , and add tests to make sure it properly interpretets the backend. Further, we fix the documentation string that properly explains how branch works --- src/bitc/bitc.lisp | 70 +++++++++++++++++++++++++++++++++++++++++++ src/bitc/package.lisp | 8 +++++ src/bitc/trans.lisp | 4 +-- src/specs/bitc.lisp | 4 +-- test/bitc.lisp | 33 ++++++++++++-------- test/poly.lisp | 2 +- 6 files changed, 104 insertions(+), 17 deletions(-) diff --git a/src/bitc/bitc.lisp b/src/bitc/bitc.lisp index 158abe4cf..5645edde9 100644 --- a/src/bitc/bitc.lisp +++ b/src/bitc/bitc.lisp @@ -5,6 +5,7 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (defmethod dom ((x )) + "Gives the length of the bit vector the [\\] moprhism takes" (typecase-of bitc x (compose (dom (mcadr x))) (fork (mcar x)) @@ -19,6 +20,7 @@ (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))) @@ -31,3 +33,71 @@ (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 index 59b76f897..9386522b5 100644 --- a/src/bitc/package.lisp +++ b/src/bitc/package.lisp @@ -43,6 +43,13 @@ (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") @@ -50,4 +57,5 @@ 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 index 998ea16f5..0d49a9d46 100644 --- a/src/bitc/trans.lisp +++ b/src/bitc/trans.lisp @@ -70,9 +70,9 @@ (defmethod to-vampir ((obj branch) values) "Look at the first bit. - If its 1, run f on the remaining bits. + If its 0, run f on the remaining bits. - If its 0, run g on the remaining bits." + If its 1, run g on the remaining bits." (let ((x (car values)) (xs (cdr values)) (f (mcar obj)) diff --git a/src/specs/bitc.lisp b/src/specs/bitc.lisp index 849b2f98d..da5aa84b0 100644 --- a/src/specs/bitc.lisp +++ b/src/specs/bitc.lisp @@ -124,8 +124,8 @@ x : a → b, y : 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 `1`, then the -[MCAR] is ran, however if the bit is `0`, then the [MCADR] is ran.")) +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 diff --git a/test/bitc.lisp b/test/bitc.lisp index 4fa46c461..d1a9a4077 100644 --- a/test/bitc.lisp +++ b/test/bitc.lisp @@ -2,20 +2,29 @@ (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: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))) - :tc_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/poly.lisp b/test/poly.lisp index 77377b003..63d3f7489 100644 --- a/test/poly.lisp +++ b/test/poly.lisp @@ -13,7 +13,7 @@ 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)) From 04dafdaaa3e30e06534420ab15a6fde1b21c6a6f Mon Sep 17 00:00:00 2001 From: mariari Date: Tue, 2 May 2023 16:25:19 +0800 Subject: [PATCH 4/4] Fix geb->bitc with init and move over the default backend to bitc This commit fixes a bug with init where init a domain with less than 2 bits would cause init to crash Further we move the default compilation pipeline to use the bitc backend --- src/geb/trans.lisp | 8 ++++++-- src/lambda/package.lisp | 3 ++- src/lambda/trans.lisp | 16 ++++++++++------ 3 files changed, 18 insertions(+), 9 deletions(-) diff --git a/src/geb/trans.lisp b/src/geb/trans.lisp index db1a4e3fd..9673b1b20 100644 --- a/src/geb/trans.lisp +++ b/src/geb/trans.lisp @@ -73,7 +73,7 @@ (defmethod to-circuit ((obj ) name) "Turns a @GEB-SUBSTMORPH to a Vamp-IR Term" (assure geb.vampir.spec:statement - (to-circuit (to-poly obj) name))) + (to-circuit (to-bitc obj) name))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Morph to Bitc Implementation @@ -97,7 +97,11 @@ ;; This should never occure, but if it does, it produces a ;; constant morphism onto an all 0s list (init - (apply #'bitc:parallel (zero-list (bitwidth (mcar obj))))) + (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)))) 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 f97c793de..40de285a6 100644 --- a/src/lambda/trans.lisp +++ b/src/lambda/trans.lisp @@ -11,17 +11,21 @@ (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.common: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) + (~> (to-bitc context type obj) (geb.common:to-circuit name)))) (defmethod empty ((class (eql (find-class 'list)))) nil)