From c7394b825faf2cead52e003aae3dae6f80152ec3 Mon Sep 17 00:00:00 2001 From: Anthony Hart Date: Tue, 25 Apr 2023 00:55:06 -0700 Subject: [PATCH 01/13] boolean circuit compliation port (not tested) --- src/bits/bits.lisp | 33 +++++++++++ src/bits/package.lisp | 37 ++++++++++++ src/bits/trans.lisp | 103 ++++++++++++++++++++++++++++++++++ src/geb/trans.lisp | 52 +++++++++++++++++ src/specs/bits-printer.lisp | 31 +++++++++++ src/specs/bits.lisp | 108 ++++++++++++++++++++++++++++++++++++ 6 files changed, 364 insertions(+) create mode 100644 src/bits/bits.lisp create mode 100644 src/bits/package.lisp create mode 100644 src/bits/trans.lisp create mode 100644 src/specs/bits-printer.lisp create mode 100644 src/specs/bits.lisp diff --git a/src/bits/bits.lisp b/src/bits/bits.lisp new file mode 100644 index 000000000..67d44ba7f --- /dev/null +++ b/src/bits/bits.lisp @@ -0,0 +1,33 @@ +(defmethod dom ((x )) + (assure substobj + (typecase-of bits x + (compose (dom (mcadr x))) + (fork (dom (mcar x))) + (parallel (+ (dom (mcar x)) (dom (mcadr x)))) + (negation 1) + (conjunction 2) + (swap (+ (mcar x) (mcadr x))) + (true 0) + (false 0) + (identity (mcar x)) + (drop (mcar x)) + (branch (+ 1 (dom (mcar x)))) + (otherwise + (subclass-responsibility x))))) + +(defmethod codom ((x )) + (assure substobj + (typecase-of bits x + (compose (codom (mcar x))) + (fork (* 2 (codom (mcar x)))) + (parallel (+ (codom (mcar x)) (codom (mcadr x)))) + (negation 1) + (conjunction 1) + (swap (+ (mcar x) (mcadr x))) + (true 1) + (false 1) + (identity (mcar x)) + (drop 0) + (branch (codom (mcar x))) + (otherwise + (subclass-responsibility x))))) diff --git a/src/bits/package.lisp b/src/bits/package.lisp new file mode 100644 index 000000000..9746ffd80 --- /dev/null +++ b/src/bits/package.lisp @@ -0,0 +1,37 @@ +(in-package :geb.utils) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;; trans module +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(muffle-package-variance + (defpackage #:geb.bits.trans + (:local-nicknames (:vamp :geb.vampir.spec)) + (:use #:geb.common #:geb.bits.spec) + (:shadowing-import-from #:geb.bits.spec :+ :* :/ :- :mod))) + +(in-package :geb.bits.trans) + +(pax:defsection @bits-trans (:title "Bits (Boolean Circuit) Transformations") + "This covers transformation functions from" + (to-vampir pax:generic-function) + (to-circuit pax:function)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;; bits module +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(geb.utils:muffle-package-variance + (uiop:define-package #:geb.bits + (:use #:geb.common) + ;(:shadowing-import-from #:geb.bits.spec ) + (:use-reexport #:geb.bits.trans #:geb.bits.spec))) + +(in-package :geb.bits) + +(pax:defsection @bits-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" + (@bits pax:section) + (@bits-constructors pax:section) + (@bits-trans pax:section)) diff --git a/src/bits/trans.lisp b/src/bits/trans.lisp new file mode 100644 index 000000000..e22b7e8a9 --- /dev/null +++ b/src/bits/trans.lisp @@ -0,0 +1,103 @@ +(in-package :geb.bits.trans) + +(defgeneric to-vampir (morphism values) + (:documentation "Turns a BITS term into a Vamp-IR term with a given value")) + +(defun to-circuit (morphism name) + "Turns a BITS term into a Vamp-IR Gate with the given name" + (let ((wire (vamp:make-wire :var :x))) + (vamp:make-alias :name name + :inputs (list wire) + :body (list (to-vampir morphism wire))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Bits to Vampir Implementation +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defmethod to-vampir ((obj ) 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 obj value1 value2) + (vamp:make-infix :op symbol + :lhs value + :rhs value2)) + + +(defmethod to-vampir ((obj compose) values) + (to-vampir (mcar obj) + (to-vampir (mcadr obj) values))) + +(defmethod to-vampir ((obj fork) values) + ; toElem[fork[n_]] := Function[{inp}, Flatten[{inp, inp}, 1]] + (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] + ; ]] + (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 negation) values) + ; toElem[neg] := {1 - #[[1]]} & + (list (infix-creation :- (make-constant :const 1) (car values)))) + +(defmethod to-vampir ((obj conjunction) values) + ; toElem[conj] := {#[[1]] * #[[2]]} & + (list (infix-creation :* (car values) (car (cdr values))))) + +(defmethod to-vampir ((obj swap) values) + ; toElem[swap[n_, m_]] := Flatten[{#[[n + 1 ;; All]], #[[1 ;; n]]}, 1] & + (let ((n (mcar obj))) + (append (subseq values (1 + n)) (subseq values 0 (1 + n))))) + +(defmethod to-vampir ((obj true) values) + ; toElem[True] := {1} & + (declare (ignore values)) + (list (vamp:make-constant :const 1))) + +(defmethod to-vampir ((obj false) values) + ; toElem[False] := {0} & + (declare (ignore values)) + (list (vamp:make-constant :const 0))) + +(defmethod to-vampir ((obj identity) values) + ; toElem[id[_]] := # & + values) + +(defmethod to-vampir ((obj drop) values) + ; toElem[drop[_]] := {} & + (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}] + ; ] + (let* ((x (car values)) + (rest-values (cdr values)) + (f (mcar obj)) + (g (mcadr obj)) + (f-elems (to-vampir f rest-values)) + (g-elems (to-vampir g rest-values))) + (mapcar #'(lambda (f-elem g-elem) + (infix-creation :+ + (infix-creation :* (infix-creation :- 1 x) f-elem) + (infix-creation :* x g-elem))) + f-elems g-elems))) diff --git a/src/geb/trans.lisp b/src/geb/trans.lisp index 2abfe4e83..211333bdd 100644 --- a/src/geb/trans.lisp +++ b/src/geb/trans.lisp @@ -78,3 +78,55 @@ "Turns a @GEB-SUBSTMORPH to a Vamp-IR Term" (assure geb.vampir.spec:statement (geb.poly:to-circuit (to-poly obj) name))) + + + + + + +(defmethod to-bits ((obj )) + (typecase-of substobj obj + (so0 0) + (so1 0) + (coprod (+ 1 (max (to-bits (mcar obj)) (to-bits (mcadr obj))))) + (prod (+ (to-bits (mcar obj)) (to-bits (mcadr obj)))) + (otherwise (subclass-responsibility obj)))) + +(defmethod to-bits ((obj )) + (typecase-of substmorph obj + (substobj (error "impossible")) + ;toBits[comp[f__]] := toBits /@ comp[f] + (comp (bits:compose (to-bits (mcar obj)) + (to-bits (mcadr obj)))) + ; toBits[init[x_]] := par @@ Table[False, bitWidth@x] + (init (apply #'bits:parallel (make-list (to-bits (mcar obj)) :initial-element bits:false))) + ; toBits[terminal[x_]] := drop[bitWidth@x] + (terminal (bits:drop (to-bits (mcar obj)))) + ;toBits[injectLeft[mcar_, mcadr_]] := + ; par @@ Join[{False, id[bitWidth@mcar]}, Table[False, Max[bitWidth@mcar, bitWidth@mcadr] - bitWidth@mcar]] + (inject-left (apply #'bits:parallel (append (list bits:false (bits:identity (to-bits (mcar obj)))) + (make-list (- (max (to-bits (mcar obj)) (to-bits (mcadr obj))) (to-bits (mcar obj))) :initial-element bits:false) + ))) + ;toBits[injectRight[mcar_,mcadr_]]:= + ; par@@Join[{True,id[bitWidth@mcadr]},Table[False, Max[bitWidth@mcar, bitWidth@mcadr] - bitWidth@mcadr]] + (inject-right (apply #'bits:parallel (append (list bits:true (bits:identity (to-bits (mcadr obj)))) + (make-list (- (max (to-bits (mcar obj)) (to-bits (mcadr obj))) (to-bits (mcadr obj))) :initial-element bits:false) + ))) + ;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 (bits:branch (bits:parallel (to-bits (mcar obj)) (bits:identity (- (max (dom (mcar obj)) (dom (mcadr obj))) (dom (mcar obj))))) + (bits:parallel (to-bits (mcadr obj)) (bits:identity (- (max (dom (mcar obj)) (dom (mcadr obj))) (dom (mcadr obj))))))) + ; toBits[projectRight[mcar_, mcadr_]] := par[drop[bitWidth@mcar], id[bitWidth@mcadr]] + (project-left (bits:parallel (bits:identity (to-bits (mcar obj))) (bits:drop (to-bits (mcadr obj))))) + ; toBits[projectLeft[mcar_, mcadr_]] := par[id[bitWidth@mcar], drop[bitWidth@mcadr]] + (project-right (bits:parallel (bits:drop (to-bits (mcar obj))) (bits:identity (to-bits (mcadr obj))))) + ; toBits[pair[mcar_, mcdr_]] := comp[par[toBits[mcar], toBits[mcdr]], fork[dom[mcar]]] + (pair (bits:compose (bits:parallel (to-bits (mcar obj)) (to-bits (mcdr obj))) (bits:fork (dom (mcar obj))))) + ;toBits[distribute[mcar_, mcadr_, mcaddr_]] := + ; par[swap[bitWidth[mcar], 1], id[Max[bitWidth@mcadr, bitWidth@mcaddr]]] + (distribute (bits:parallel (bits:swap (to-bits (mcar obj)) 1) (bits:identity (max (to-bits (mcadr obj)) (to-bits (mcaddr obj)))))) + (otherwise (subclass-responsibility obj)))) + diff --git a/src/specs/bits-printer.lisp b/src/specs/bits-printer.lisp new file mode 100644 index 000000000..6eea2ea35 --- /dev/null +++ b/src/specs/bits-printer.lisp @@ -0,0 +1,31 @@ +;; TO DO: + + +(in-package #:geb.bits.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) + (print-object (cons ',class-name + (mapcar #'cdr (geb.mixins:to-pointwise-list obj))) + stream))) + +(easy-printer compose) +(easy-printer fork) +(easy-printer parallel) +(easy-printer negation) +(easy-printer conjunction) +(easy-printer swap) +(easy-printer true) +(easy-printer false) +(easy-printer identity) +(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/bits.lisp b/src/specs/bits.lisp new file mode 100644 index 000000000..39dea50d4 --- /dev/null +++ b/src/specs/bits.lisp @@ -0,0 +1,108 @@ +(in-package #:geb.bits.spec) + +(deftype bits () + `(or compose fork parallel negation conjunction swap true false identity drop branch)) + +(defclass (geb.mixins:direct-pointwise-mixin) ()) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Constructor Morphisms for Bits (Objects are just natural numbers) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defclass compose () + ((mcar :initarg :mcar + :accessor mcar + :documentation "") + (mcadr :initarg :mcadr + :accessor mcadr + :documentation ""))) + +(defclass fork () + ((mcar :initarg :mcar + :accessor mcar + :documentation ""))) + +(defclass parallel () + ((mcar :initarg :mcar + :accessor mcar + :documentation "") + (mcadr :initarg :mcadr + :accessor mcadr + :documentation ""))) + +(defclass negation () + ((mcar :initarg :mcar + :accessor mcar + :documentation ""))) + +(defclass conjunction () + ((mcar :initarg :mcar + :accessor mcar + :documentation "") + (mcadr :initarg :mcadr + :accessor mcadr + :documentation ""))) + +(defclass swap () + ((mcar :initarg :mcar + :accessor mcar + :documentation "") + (mcadr :initarg :mcadr + :accessor mcadr + :documentation ""))) + +(defclass true () + ()) + +(defclass false () + ()) + +(defclass identity () + ((mcar :initarg :mcar + :accessor mcar + :documentation ""))) + +(defclass drop () + ((mcar :initarg :mcar + :accessor mcar + :documentation ""))) + +(defclass branch () + ((mcar :initarg :mcar + :accessor mcar + :documentation "") + (mcadr :initarg :mcadr + :accessor mcadr + :documentation ""))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; 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) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; 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 negation mcar) +(make-pattern conjunction mcar mcadr) +(make-pattern swap mcar mcadr) +(make-pattern true ) +(make-pattern false ) +(make-pattern identity mcar) +(make-pattern drop mcar) +(make-pattern branch mcar mcadr) From 9b4cab9cb251588201f6fa15a4da3ccf25d86ab0 Mon Sep 17 00:00:00 2001 From: Anthony Hart Date: Wed, 26 Apr 2023 02:28:38 -0700 Subject: [PATCH 02/13] Save progress on bug fixing --- geb.asd | 18 ++++++- src/{bits/bits.lisp => bitc/bitc.lisp} | 24 ++++------ src/{bits => bitc}/package.lisp | 29 ++++++------ src/{bits => bitc}/trans.lisp | 32 +++++-------- src/entry/package.lisp | 1 + src/geb/trans.lisp | 39 ++++++++------- .../{bits-printer.lisp => bitc-printer.lisp} | 10 ++-- src/specs/{bits.lisp => bitc.lisp} | 47 +++++++------------ src/specs/package.lisp | 37 +++++++++++++++ test/bitc.lisp | 16 +++++++ test/geb.lisp | 2 + 11 files changed, 150 insertions(+), 105 deletions(-) rename src/{bits/bits.lisp => bitc/bitc.lisp} (63%) rename src/{bits => bitc}/package.lisp (57%) rename src/{bits => bitc}/trans.lisp (75%) rename src/specs/{bits-printer.lisp => bitc-printer.lisp} (83%) rename src/specs/{bits.lisp => bitc.lisp} (69%) create mode 100644 test/bitc.lisp diff --git a/geb.asd b/geb.asd index 2c3c73685..7e5caca52 100644 --- a/geb.asd +++ b/geb.asd @@ -1,3 +1,4 @@ + (asdf:defsystem :geb :depends-on (:trivia :alexandria :serapeum :fset :fare-quasiquote-extras ;; wed are only importing this for now until I @@ -9,11 +10,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 +51,11 @@ :description "Polynomial" :depends-on (util geb vampir specs) :components ((:file package))) + (:module bits + :serial t + :description "Bits (Boolean Circuits)" + :depends-on (util geb vampir specs) + :components ((:file package))) (:module lambda :serial t :depends-on (geb specs) @@ -68,6 +78,8 @@ (:file lambda) (:file poly) (:file poly-printer) + (:file bits) + (:file bits-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 bits/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 bits lambda) :components ((:file package) (:file entry)))) :in-order-to ((asdf:test-op (asdf:test-op :geb/test)))) @@ -125,6 +138,7 @@ (:file lambda-experimental) (:file lambda-conversion) (:file poly) + (:file bits) (:file pipeline) (:module gui :serial t diff --git a/src/bits/bits.lisp b/src/bitc/bitc.lisp similarity index 63% rename from src/bits/bits.lisp rename to src/bitc/bitc.lisp index 67d44ba7f..cd635233c 100644 --- a/src/bits/bits.lisp +++ b/src/bitc/bitc.lisp @@ -1,32 +1,28 @@ -(defmethod dom ((x )) +(defmethod dom ((x )) (assure substobj - (typecase-of bits x + (typecase-of bitc x (compose (dom (mcadr x))) (fork (dom (mcar x))) (parallel (+ (dom (mcar x)) (dom (mcadr x)))) - (negation 1) - (conjunction 2) (swap (+ (mcar x) (mcadr x))) - (true 0) - (false 0) - (identity (mcar x)) + (one 0) + (zero 0) + (ident (mcar x)) (drop (mcar x)) (branch (+ 1 (dom (mcar x)))) (otherwise (subclass-responsibility x))))) -(defmethod codom ((x )) +(defmethod codom ((x )) (assure substobj - (typecase-of bits x + (typecase-of bitc x (compose (codom (mcar x))) (fork (* 2 (codom (mcar x)))) (parallel (+ (codom (mcar x)) (codom (mcadr x)))) - (negation 1) - (conjunction 1) (swap (+ (mcar x) (mcadr x))) - (true 1) - (false 1) - (identity (mcar x)) + (one 1) + (zero 1) + (ident (mcar x)) (drop 0) (branch (codom (mcar x))) (otherwise diff --git a/src/bits/package.lisp b/src/bitc/package.lisp similarity index 57% rename from src/bits/package.lisp rename to src/bitc/package.lisp index 9746ffd80..175e138a3 100644 --- a/src/bits/package.lisp +++ b/src/bitc/package.lisp @@ -5,33 +5,34 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (muffle-package-variance - (defpackage #:geb.bits.trans + (defpackage #:geb.bitc.trans (:local-nicknames (:vamp :geb.vampir.spec)) - (:use #:geb.common #:geb.bits.spec) - (:shadowing-import-from #:geb.bits.spec :+ :* :/ :- :mod))) + (:use #:geb.common #:geb.bitc.spec) + (:shadowing-import-from #:geb.bitc.spec #:drop #:fork) + )) -(in-package :geb.bits.trans) +(in-package :geb.bitc.trans) -(pax:defsection @bits-trans (:title "Bits (Boolean Circuit) Transformations") +(pax:defsection @bitc-trans (:title "Bits (Boolean Circuit) Transformations") "This covers transformation functions from" (to-vampir pax:generic-function) (to-circuit pax:function)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;; bits module +;;; bitc module ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (geb.utils:muffle-package-variance - (uiop:define-package #:geb.bits + (uiop:define-package #:geb.bitc (:use #:geb.common) - ;(:shadowing-import-from #:geb.bits.spec ) - (:use-reexport #:geb.bits.trans #:geb.bits.spec))) + (:shadowing-import-from #:geb.bitc.spec #:drop #:fork) + (:use-reexport #:geb.bitc.trans #:geb.bitc.spec))) -(in-package :geb.bits) +(in-package :geb.bitc) -(pax:defsection @bits-manual (:title "Bits (Boolean Circuit) Specification") +(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" - (@bits pax:section) - (@bits-constructors pax:section) - (@bits-trans pax:section)) + (@bitc pax:section) + (@bitc-constructors pax:section) + (@bitc-trans pax:section)) diff --git a/src/bits/trans.lisp b/src/bitc/trans.lisp similarity index 75% rename from src/bits/trans.lisp rename to src/bitc/trans.lisp index e22b7e8a9..ec3204e83 100644 --- a/src/bits/trans.lisp +++ b/src/bitc/trans.lisp @@ -1,10 +1,10 @@ -(in-package :geb.bits.trans) +(in-package :geb.bitc.trans) (defgeneric to-vampir (morphism values) - (:documentation "Turns a BITS term into a Vamp-IR term with a given value")) + (:documentation "Turns a BITC term into a Vamp-IR term with a given value")) (defun to-circuit (morphism name) - "Turns a BITS term into a Vamp-IR Gate with the given name" + "Turns a BITC term into a Vamp-IR Gate with the given name" (let ((wire (vamp:make-wire :var :x))) (vamp:make-alias :name name :inputs (list wire) @@ -14,7 +14,7 @@ ;; Bits to Vampir Implementation ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defmethod to-vampir ((obj ) values) +(defmethod to-vampir ((obj ) values) (declare (ignore values)) (subclass-responsibility obj)) @@ -22,7 +22,7 @@ (defun direct-fields-to-list (obj) (mapcar #'cdr (geb.mixins:to-pointwise-list obj))) -(defun infix-creation (symbol obj value1 value2) +(defun infix-creation (symbol value1 value2) (vamp:make-infix :op symbol :lhs value :rhs value2)) @@ -40,10 +40,10 @@ ; 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] + ; cx = dom[car]; + ; inp1 = inp[[1 ;; cx]]; + ; inp2 = inp[[cx + 1 ;; All]]; + ; Flatten[{toElem[car][inp1], toElem[cadr][inp2]}, 1] ; ]] (let* ((car (mcar obj)) (cadr (mcadr obj)) @@ -52,30 +52,22 @@ (inp2 (subseq values cx))) (concatenate 'list (to-vampir car inp1) (to-vampir cadr inp2)))) -(defmethod to-vampir ((obj negation) values) - ; toElem[neg] := {1 - #[[1]]} & - (list (infix-creation :- (make-constant :const 1) (car values)))) - -(defmethod to-vampir ((obj conjunction) values) - ; toElem[conj] := {#[[1]] * #[[2]]} & - (list (infix-creation :* (car values) (car (cdr values))))) - (defmethod to-vampir ((obj swap) values) ; toElem[swap[n_, m_]] := Flatten[{#[[n + 1 ;; All]], #[[1 ;; n]]}, 1] & (let ((n (mcar obj))) (append (subseq values (1 + n)) (subseq values 0 (1 + n))))) -(defmethod to-vampir ((obj true) values) +(defmethod to-vampir ((obj one) values) ; toElem[True] := {1} & (declare (ignore values)) (list (vamp:make-constant :const 1))) -(defmethod to-vampir ((obj false) values) +(defmethod to-vampir ((obj zero) values) ; toElem[False] := {0} & (declare (ignore values)) (list (vamp:make-constant :const 0))) -(defmethod to-vampir ((obj identity) values) +(defmethod to-vampir ((obj ident) values) ; toElem[id[_]] := # & values) 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/trans.lisp b/src/geb/trans.lisp index 419ce31cf..a68325c81 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 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -84,49 +87,49 @@ -(defmethod to-bits ((obj )) +(defmethod to-bitc ((obj )) (typecase-of substobj obj (so0 0) (so1 0) - (coprod (+ 1 (max (to-bits (mcar obj)) (to-bits (mcadr obj))))) - (prod (+ (to-bits (mcar obj)) (to-bits (mcadr obj)))) + (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-bits ((obj )) +(defmethod to-bitc ((obj )) (typecase-of substmorph obj (substobj (error "impossible")) ;toBits[comp[f__]] := toBits /@ comp[f] - (comp (bits:compose (to-bits (mcar obj)) - (to-bits (mcadr obj)))) + (comp (bitc:compose (to-bitc (mcar obj)) + (to-bitc (mcadr obj)))) ; toBits[init[x_]] := par @@ Table[False, bitWidth@x] - (init (apply #'bits:parallel (make-list (to-bits (mcar obj)) :initial-element bits:false))) + (init (apply #'bitc:parallel (make-list (to-bitc (mcar obj)) :initial-element bitc:zero))) ; toBits[terminal[x_]] := drop[bitWidth@x] - (terminal (bits:drop (to-bits (mcar obj)))) + (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 (apply #'bits:parallel (append (list bits:false (bits:identity (to-bits (mcar obj)))) - (make-list (- (max (to-bits (mcar obj)) (to-bits (mcadr obj))) (to-bits (mcar obj))) :initial-element bits:false) + (inject-left (apply #'bitc:parallel (append (list bitc:zero (bitc:identity (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 (apply #'bits:parallel (append (list bits:true (bits:identity (to-bits (mcadr obj)))) - (make-list (- (max (to-bits (mcar obj)) (to-bits (mcadr obj))) (to-bits (mcadr obj))) :initial-element bits:false) + (inject-right (apply #'bitc:parallel (append (list bitc:one (bitc:identity (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 (bits:branch (bits:parallel (to-bits (mcar obj)) (bits:identity (- (max (dom (mcar obj)) (dom (mcadr obj))) (dom (mcar obj))))) - (bits:parallel (to-bits (mcadr obj)) (bits:identity (- (max (dom (mcar obj)) (dom (mcadr obj))) (dom (mcadr obj))))))) + (case (bitc:branch (bitc:parallel (to-bitc (mcar obj)) (bitc:identity (- (max (dom (mcar obj)) (dom (mcadr obj))) (dom (mcar obj))))) + (bitc:parallel (to-bitc (mcadr obj)) (bitc:identity (- (max (dom (mcar obj)) (dom (mcadr obj))) (dom (mcadr obj))))))) ; toBits[projectRight[mcar_, mcadr_]] := par[drop[bitWidth@mcar], id[bitWidth@mcadr]] - (project-left (bits:parallel (bits:identity (to-bits (mcar obj))) (bits:drop (to-bits (mcadr obj))))) + (project-left (bitc:parallel (bitc:identity (to-bitc (mcar obj))) (bitc:drop (to-bitc (mcadr obj))))) ; toBits[projectLeft[mcar_, mcadr_]] := par[id[bitWidth@mcar], drop[bitWidth@mcadr]] - (project-right (bits:parallel (bits:drop (to-bits (mcar obj))) (bits:identity (to-bits (mcadr obj))))) + (project-right (bitc:parallel (bitc:drop (to-bitc (mcar obj))) (bitc:identity (to-bitc (mcadr obj))))) ; toBits[pair[mcar_, mcdr_]] := comp[par[toBits[mcar], toBits[mcdr]], fork[dom[mcar]]] - (pair (bits:compose (bits:parallel (to-bits (mcar obj)) (to-bits (mcdr obj))) (bits:fork (dom (mcar obj))))) + (pair (bitc:compose (bitc:parallel (to-bitc (mcar obj)) (to-bitc (mcdr obj))) (bitc:fork (dom (mcar obj))))) ;toBits[distribute[mcar_, mcadr_, mcaddr_]] := ; par[swap[bitWidth[mcar], 1], id[Max[bitWidth@mcadr, bitWidth@mcaddr]]] - (distribute (bits:parallel (bits:swap (to-bits (mcar obj)) 1) (bits:identity (max (to-bits (mcadr obj)) (to-bits (mcaddr obj)))))) + (distribute (bitc:parallel (bitc:swap (to-bitc (mcar obj)) 1) (bitc:identity (max (to-bitc (mcadr obj)) (to-bitc (mcaddr obj)))))) (otherwise (subclass-responsibility obj)))) diff --git a/src/specs/bits-printer.lisp b/src/specs/bitc-printer.lisp similarity index 83% rename from src/specs/bits-printer.lisp rename to src/specs/bitc-printer.lisp index 6eea2ea35..a2a936fbe 100644 --- a/src/specs/bits-printer.lisp +++ b/src/specs/bitc-printer.lisp @@ -1,7 +1,7 @@ ;; TO DO: -(in-package #:geb.bits.spec) +(in-package #:geb.bitc.spec) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Subst Constructor Printer @@ -17,12 +17,10 @@ (easy-printer compose) (easy-printer fork) (easy-printer parallel) -(easy-printer negation) -(easy-printer conjunction) (easy-printer swap) -(easy-printer true) -(easy-printer false) -(easy-printer identity) +(easy-printer one) +(easy-printer zero) +(easy-printer ident) (easy-printer drop) (easy-printer branch) diff --git a/src/specs/bits.lisp b/src/specs/bitc.lisp similarity index 69% rename from src/specs/bits.lisp rename to src/specs/bitc.lisp index 39dea50d4..d19ffa4d4 100644 --- a/src/specs/bits.lisp +++ b/src/specs/bitc.lisp @@ -1,15 +1,15 @@ -(in-package #:geb.bits.spec) +(in-package #:geb.bitc.spec) -(deftype bits () - `(or compose fork parallel negation conjunction swap true false identity drop branch)) +(deftype bitc () + `(or compose fork parallel swap one zero ident drop branch)) -(defclass (geb.mixins:direct-pointwise-mixin) ()) +(defclass (geb.mixins:direct-pointwise-mixin) ()) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Constructor Morphisms for Bits (Objects are just natural numbers) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defclass compose () +(defclass compose () ((mcar :initarg :mcar :accessor mcar :documentation "") @@ -17,12 +17,12 @@ :accessor mcadr :documentation ""))) -(defclass fork () +(defclass fork () ((mcar :initarg :mcar :accessor mcar :documentation ""))) -(defclass parallel () +(defclass parallel () ((mcar :initarg :mcar :accessor mcar :documentation "") @@ -30,20 +30,7 @@ :accessor mcadr :documentation ""))) -(defclass negation () - ((mcar :initarg :mcar - :accessor mcar - :documentation ""))) - -(defclass conjunction () - ((mcar :initarg :mcar - :accessor mcar - :documentation "") - (mcadr :initarg :mcadr - :accessor mcadr - :documentation ""))) - -(defclass swap () +(defclass swap () ((mcar :initarg :mcar :accessor mcar :documentation "") @@ -51,23 +38,23 @@ :accessor mcadr :documentation ""))) -(defclass true () +(defclass one () ()) -(defclass false () +(defclass zero () ()) -(defclass identity () +(defclass ident () ((mcar :initarg :mcar :accessor mcar :documentation ""))) -(defclass drop () +(defclass drop () ((mcar :initarg :mcar :accessor mcar :documentation ""))) -(defclass branch () +(defclass branch () ((mcar :initarg :mcar :accessor mcar :documentation "") @@ -98,11 +85,9 @@ (make-pattern compose mcar mcadr) (make-pattern fork mcar) (make-pattern parallel mcar mcadr) -(make-pattern negation mcar) -(make-pattern conjunction mcar mcadr) (make-pattern swap mcar mcadr) -(make-pattern true ) -(make-pattern false ) -(make-pattern identity mcar) +(make-pattern one ) +(make-pattern zero ) +(make-pattern ident mcar) (make-pattern drop mcar) (make-pattern branch mcar mcadr) diff --git a/src/specs/package.lisp b/src/specs/package.lisp index 068e9a452..d1a62e612 100644 --- a/src/specs/package.lisp +++ b/src/specs/package.lisp @@ -9,6 +9,10 @@ (:shadow :+ :* :/ :- :mod) (:use #:geb.utils #:cl))) +(muffle-package-variance + (defpackage #:geb.bitc.spec + (:use #:geb.utils #:cl))) + ;; please document this later. (muffle-package-variance (uiop:define-package #:geb.lambda.spec @@ -90,6 +94,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:type) + (compose pax:type) + (fork pax:type) + (parallel pax:type) + (swap pax:type) + (one pax:type) + (zero pax:type) + (ident pax:type) + (drop pax:type) + (branch pax:type)) + +(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:type) + (fork pax:type) + (parallel pax:type) + (swap pax:type) + (one pax:type) + (zero pax:type) + (ident pax:type) + (drop pax:type) + (branch pax:type)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Geb lambda Package Documentation ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/test/bitc.lisp b/test/bitc.lisp new file mode 100644 index 000000000..49cbf12fc --- /dev/null +++ b/test/bitc.lisp @@ -0,0 +1,16 @@ +(in-package :geb-test) + +(define-test geb-bitc :parent geb-test-suite) + +(def test-circuit-1 + (bitc:to-circuit + (bitc:comp + (bitc:branch + (bitc:parallel (bitc:comp (bitc:parallel bitc:zero (bitc:identity 0)) (bitc:drop 1)) (bitc:identity 0)) + (bitc:parallel (bitc:parallel (bitc:identity 1) (bitc:drop 0)) (bitc:identity 0))) + (bitc:parallel (bitc:swap 1 1) (bitc:identity 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..8e89ad1da 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-bits-2 (geb:to-bits test-morph-2)) + (def test-circuit-2 (geb:to-circuit test-morph-2 :tc_2)) (define-test vampir-test-2 From c8609493c8ddfbffe8615e036c201b305726529a Mon Sep 17 00:00:00 2001 From: Anthony Hart Date: Wed, 26 Apr 2023 04:17:44 -0700 Subject: [PATCH 03/13] Further bug fixing (imports broken?) --- geb.asd | 14 +++++++------- src/bitc/bitc.lisp | 29 ----------------------------- src/bitc/trans.lisp | 36 +++++++++++++++++++++++++++++++++++- src/geb/package.lisp | 7 ++++--- src/geb/trans.lisp | 16 ++++++++-------- test/bitc.lisp | 8 ++++---- test/geb.lisp | 2 +- test/package.lisp | 1 + 8 files changed, 60 insertions(+), 53 deletions(-) delete mode 100644 src/bitc/bitc.lisp diff --git a/geb.asd b/geb.asd index 7e5caca52..13902a15d 100644 --- a/geb.asd +++ b/geb.asd @@ -51,9 +51,9 @@ :description "Polynomial" :depends-on (util geb vampir specs) :components ((:file package))) - (:module bits + (:module bitc :serial t - :description "Bits (Boolean Circuits)" + :description "bitc (Boolean Circuits)" :depends-on (util geb vampir specs) :components ((:file package))) (:module lambda @@ -78,8 +78,8 @@ (:file lambda) (:file poly) (:file poly-printer) - (:file bits) - (:file bits-printer) + (:file bitc) + (:file bitc-printer) ;; HACK: to make the package properly refer to the ;; right symbols (:file ../util/package))) @@ -94,11 +94,11 @@ :components ((:file lambda/trans) (:file geb/trans) (:file poly/trans) - (:file bits/trans))) + (:file bitc/trans))) (:module entry :serial t :description "Entry point for the geb codebase" - :depends-on (util geb vampir specs poly bits 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)))) @@ -138,7 +138,7 @@ (:file lambda-experimental) (:file lambda-conversion) (:file poly) - (:file bits) + (:file bitc) (:file pipeline) (:module gui :serial t diff --git a/src/bitc/bitc.lisp b/src/bitc/bitc.lisp deleted file mode 100644 index cd635233c..000000000 --- a/src/bitc/bitc.lisp +++ /dev/null @@ -1,29 +0,0 @@ -(defmethod dom ((x )) - (assure substobj - (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 )) - (assure substobj - (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))))) diff --git a/src/bitc/trans.lisp b/src/bitc/trans.lisp index ec3204e83..e02797166 100644 --- a/src/bitc/trans.lisp +++ b/src/bitc/trans.lisp @@ -10,6 +10,40 @@ :inputs (list wire) :body (list (to-vampir morphism wire))))) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Domain and codomain definitions +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defmethod dom ((x )) + (assure substobj + (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 )) + (assure substobj + (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))))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Bits to Vampir Implementation ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -55,7 +89,7 @@ (defmethod to-vampir ((obj swap) values) ; toElem[swap[n_, m_]] := Flatten[{#[[n + 1 ;; All]], #[[1 ;; n]]}, 1] & (let ((n (mcar obj))) - (append (subseq values (1 + n)) (subseq values 0 (1 + n))))) + (append (subseq values (+ 1 n)) (subseq values 0 (+ 1 n))))) (defmethod to-vampir ((obj one) values) ; toElem[True] := {1} & diff --git a/src/geb/package.lisp b/src/geb/package.lisp index 3e57ea992..8faed3998 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 a68325c81..bf0b7241f 100644 --- a/src/geb/trans.lisp +++ b/src/geb/trans.lisp @@ -6,7 +6,7 @@ (:documentation "Turns a @GEB-SUBSTMORPH into a POLY:POLY")) (defgeneric to-bitc (morphism) - (:documentation "Turns a @GEB-SUBSTMORPH into a BITC:BITC")) + (:documentation "Turns a @GEB-SUBSTMORPH into a bitc:BITC")) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Morph to Poly Implementation @@ -107,12 +107,12 @@ (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 (apply #'bitc:parallel (append (list bitc:zero (bitc:identity (to-bitc (mcar obj)))) + (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 (apply #'bitc:parallel (append (list bitc:one (bitc:identity (to-bitc (mcadr obj)))) + (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_]]:= @@ -120,16 +120,16 @@ ; par[toBits@mcar,id[Max[dom@mcar,dom@mcadr]-dom@mcar]], ; par[toBits@mcadr,id[Max[dom@mcar,dom@mcadr]-dom@mcadr]] ; ] - (case (bitc:branch (bitc:parallel (to-bitc (mcar obj)) (bitc:identity (- (max (dom (mcar obj)) (dom (mcadr obj))) (dom (mcar obj))))) - (bitc:parallel (to-bitc (mcadr obj)) (bitc:identity (- (max (dom (mcar obj)) (dom (mcadr obj))) (dom (mcadr obj))))))) + (case (bitc:branch (bitc:parallel (to-bitc (mcar obj)) (bitc:ident (- (max (dom (mcar obj)) (dom (mcadr obj))) (dom (mcar obj))))) + (bitc:parallel (to-bitc (mcadr obj)) (bitc:ident (- (max (dom (mcar obj)) (dom (mcadr obj))) (dom (mcadr obj))))))) ; toBits[projectRight[mcar_, mcadr_]] := par[drop[bitWidth@mcar], id[bitWidth@mcadr]] - (project-left (bitc:parallel (bitc:identity (to-bitc (mcar obj))) (bitc:drop (to-bitc (mcadr obj))))) + (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 (bitc:parallel (bitc:drop (to-bitc (mcar obj))) (bitc:identity (to-bitc (mcadr obj))))) + (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 (bitc:compose (bitc:parallel (to-bitc (mcar obj)) (to-bitc (mcdr obj))) (bitc:fork (dom (mcar obj))))) ;toBits[distribute[mcar_, mcadr_, mcaddr_]] := ; par[swap[bitWidth[mcar], 1], id[Max[bitWidth@mcadr, bitWidth@mcaddr]]] - (distribute (bitc:parallel (bitc:swap (to-bitc (mcar obj)) 1) (bitc:identity (max (to-bitc (mcadr obj)) (to-bitc (mcaddr obj)))))) + (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)))) diff --git a/test/bitc.lisp b/test/bitc.lisp index 49cbf12fc..b992f0280 100644 --- a/test/bitc.lisp +++ b/test/bitc.lisp @@ -4,11 +4,11 @@ (def test-circuit-1 (bitc:to-circuit - (bitc:comp + (bitc:compose (bitc:branch - (bitc:parallel (bitc:comp (bitc:parallel bitc:zero (bitc:identity 0)) (bitc:drop 1)) (bitc:identity 0)) - (bitc:parallel (bitc:parallel (bitc:identity 1) (bitc:drop 0)) (bitc:identity 0))) - (bitc:parallel (bitc:swap 1 1) (bitc:identity 0))) + (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 diff --git a/test/geb.lisp b/test/geb.lisp index 8e89ad1da..6d37fe72b 100644 --- a/test/geb.lisp +++ b/test/geb.lisp @@ -102,7 +102,7 @@ (def test-poly-2 (geb:to-poly test-morph-2)) -(def test-bits-2 (geb:to-bits 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)) 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 386aec509475b6131d22921e50cb63ab4d3114b3 Mon Sep 17 00:00:00 2001 From: Anthony Hart Date: Wed, 26 Apr 2023 06:26:13 -0700 Subject: [PATCH 04/13] Fix more bugs, but still not working --- src/bitc/trans.lisp | 34 ------------------------ src/geb/trans.lisp | 6 ++--- src/specs/bitc.lisp | 60 +++++++++++++++++++++++++++++++++++++++++- src/specs/package.lisp | 4 ++- test/geb.lisp | 2 +- 5 files changed, 66 insertions(+), 40 deletions(-) diff --git a/src/bitc/trans.lisp b/src/bitc/trans.lisp index e02797166..16f56dcf9 100644 --- a/src/bitc/trans.lisp +++ b/src/bitc/trans.lisp @@ -10,40 +10,6 @@ :inputs (list wire) :body (list (to-vampir morphism wire))))) -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Domain and codomain definitions -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defmethod dom ((x )) - (assure substobj - (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 )) - (assure substobj - (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))))) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Bits to Vampir Implementation ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/src/geb/trans.lisp b/src/geb/trans.lisp index bf0b7241f..96c016fe4 100644 --- a/src/geb/trans.lisp +++ b/src/geb/trans.lisp @@ -120,14 +120,14 @@ ; par[toBits@mcar,id[Max[dom@mcar,dom@mcadr]-dom@mcar]], ; par[toBits@mcadr,id[Max[dom@mcar,dom@mcadr]-dom@mcadr]] ; ] - (case (bitc:branch (bitc:parallel (to-bitc (mcar obj)) (bitc:ident (- (max (dom (mcar obj)) (dom (mcadr obj))) (dom (mcar obj))))) - (bitc:parallel (to-bitc (mcadr obj)) (bitc:ident (- (max (dom (mcar obj)) (dom (mcadr obj))) (dom (mcadr obj))))))) + (case (bitc:branch (bitc:parallel (to-bitc (mcar obj)) (bitc:ident (- (max (bitc:dom (mcar obj)) (bitc:dom (mcadr obj))) (bitc:dom (mcar obj))))) + (bitc:parallel (to-bitc (mcadr obj)) (bitc:ident (- (max (bitc:dom (mcar obj)) (bitc:dom (mcadr obj))) (bitc:dom (mcadr obj))))))) ; toBits[projectRight[mcar_, mcadr_]] := par[drop[bitWidth@mcar], id[bitWidth@mcadr]] (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 (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 (bitc:compose (bitc:parallel (to-bitc (mcar obj)) (to-bitc (mcdr obj))) (bitc:fork (dom (mcar obj))))) + (pair (bitc:compose (bitc:parallel (to-bitc (mcar obj)) (to-bitc (mcdr obj))) (bitc:fork (bitc:dom (mcar obj))))) ;toBits[distribute[mcar_, mcadr_, mcaddr_]] := ; par[swap[bitWidth[mcar], 1], id[Max[bitWidth@mcadr, bitWidth@mcaddr]]] (distribute (bitc:parallel (bitc:swap (to-bitc (mcar obj)) 1) (bitc:ident (max (to-bitc (mcadr obj)) (to-bitc (mcaddr obj)))))) diff --git a/src/specs/bitc.lisp b/src/specs/bitc.lisp index d19ffa4d4..d79ec13de 100644 --- a/src/specs/bitc.lisp +++ b/src/specs/bitc.lisp @@ -3,7 +3,7 @@ (deftype bitc () `(or compose fork parallel swap one zero ident drop branch)) -(defclass (geb.mixins:direct-pointwise-mixin) ()) +(defclass (geb.mixins:direct-pointwise-mixin cat-morph) ()) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Constructor Morphisms for Bits (Objects are just natural numbers) @@ -77,6 +77,32 @@ (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)) + +(defvar one + (make-instance 'one)) + +(defvar 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 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -91,3 +117,35 @@ (make-pattern ident mcar) (make-pattern drop mcar) (make-pattern branch mcar mcadr) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Domain and codomain definitions +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defmethod dom ((x )) + (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 )) + (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)))) diff --git a/src/specs/package.lisp b/src/specs/package.lisp index d1a62e612..fdc071910 100644 --- a/src/specs/package.lisp +++ b/src/specs/package.lisp @@ -11,7 +11,9 @@ (muffle-package-variance (defpackage #:geb.bitc.spec - (:use #:geb.utils #:cl))) + (:export :dom :codom) + (:shadow :drop :fork) + (:use #:geb.utils #:cl #:geb.mixins))) ;; please document this later. (muffle-package-variance diff --git a/test/geb.lisp b/test/geb.lisp index 6d37fe72b..dc7757658 100644 --- a/test/geb.lisp +++ b/test/geb.lisp @@ -102,7 +102,7 @@ (def test-poly-2 (geb:to-poly test-morph-2)) -;(def test-bitc-2 (geb:to-bitc 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)) From f90cc4b798e40cba0e786f42ceb59a8385d687a8 Mon Sep 17 00:00:00 2001 From: Anthony Hart Date: Wed, 26 Apr 2023 07:28:11 -0700 Subject: [PATCH 05/13] Move dom and codom --- geb.asd | 7 +++---- src/bitc/bits.lisp | 33 +++++++++++++++++++++++++++++++++ src/bitc/package.lisp | 12 ++++++++++-- src/specs/bitc.lisp | 32 -------------------------------- 4 files changed, 46 insertions(+), 38 deletions(-) create mode 100644 src/bitc/bits.lisp diff --git a/geb.asd b/geb.asd index 5ac70cbce..45d933406 100644 --- a/geb.asd +++ b/geb.asd @@ -1,4 +1,3 @@ - (asdf:defsystem :geb :depends-on (:trivia :alexandria :serapeum :fset :fare-quasiquote-extras ;; wed are only importing this for now until I @@ -65,12 +64,12 @@ :depends-on (util geb vampir specs) :components ((:file package) (:file poly))) - :components ((:file package))) (:module bitc :serial t :description "bitc (Boolean Circuits)" - :depends-on (util geb vampir specs) - :components ((:file package))) + :depends-on (util vampir mixins specs) + :components ((:file package) + (:file bits))) (:module lambda :serial t :depends-on (geb specs) diff --git a/src/bitc/bits.lisp b/src/bitc/bits.lisp new file mode 100644 index 000000000..9ef33ee93 --- /dev/null +++ b/src/bitc/bits.lisp @@ -0,0 +1,33 @@ +(in-package :geb.bits.main) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Domain and codomain definitions +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defmethod dom ((x )) + (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 )) + (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)))) diff --git a/src/bitc/package.lisp b/src/bitc/package.lisp index 175e138a3..7489c047b 100644 --- a/src/bitc/package.lisp +++ b/src/bitc/package.lisp @@ -24,9 +24,17 @@ (geb.utils:muffle-package-variance (uiop:define-package #:geb.bitc - (:use #:geb.common) + (:use #:geb.common #:geb.mixins) (:shadowing-import-from #:geb.bitc.spec #:drop #:fork) - (:use-reexport #:geb.bitc.trans #:geb.bitc.spec))) + (:use-reexport #:geb.bitc.trans #:geb.bitc.spec #:geb.bitc.main))) + +(in-package :geb.bitc.main) + +(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) diff --git a/src/specs/bitc.lisp b/src/specs/bitc.lisp index d79ec13de..de285944d 100644 --- a/src/specs/bitc.lisp +++ b/src/specs/bitc.lisp @@ -117,35 +117,3 @@ (make-pattern ident mcar) (make-pattern drop mcar) (make-pattern branch mcar mcadr) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Domain and codomain definitions -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defmethod dom ((x )) - (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 )) - (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)))) From e70c3134d1d8983a3b5aff0024bd87354600443f Mon Sep 17 00:00:00 2001 From: Anthony Hart Date: Wed, 26 Apr 2023 08:23:38 -0700 Subject: [PATCH 06/13] Bug fixing (It works now) --- src/bitc/bits.lisp | 2 +- src/bitc/package.lisp | 8 ++++---- src/bitc/trans.lisp | 16 +++++++++------- 3 files changed, 14 insertions(+), 12 deletions(-) diff --git a/src/bitc/bits.lisp b/src/bitc/bits.lisp index 9ef33ee93..661fed728 100644 --- a/src/bitc/bits.lisp +++ b/src/bitc/bits.lisp @@ -1,4 +1,4 @@ -(in-package :geb.bits.main) +(in-package :geb.bitc.main) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Domain and codomain definitions diff --git a/src/bitc/package.lisp b/src/bitc/package.lisp index 7489c047b..3fbc981c4 100644 --- a/src/bitc/package.lisp +++ b/src/bitc/package.lisp @@ -23,12 +23,10 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (geb.utils:muffle-package-variance - (uiop:define-package #:geb.bitc + (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.bitc.main))) - -(in-package :geb.bitc.main) + (:use-reexport #:geb.bitc.trans #:geb.bitc.spec))) (geb.utils:muffle-package-variance (uiop:define-package #:geb.bitc @@ -36,6 +34,8 @@ (: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") diff --git a/src/bitc/trans.lisp b/src/bitc/trans.lisp index 16f56dcf9..baece0cc2 100644 --- a/src/bitc/trans.lisp +++ b/src/bitc/trans.lisp @@ -5,10 +5,12 @@ (defun to-circuit (morphism name) "Turns a BITC term into a Vamp-IR Gate with the given name" - (let ((wire (vamp:make-wire :var :x))) + (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 (list wire) - :body (list (to-vampir morphism wire))))) + :inputs wires + :body (to-vampir morphism wires)))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Bits to Vampir Implementation @@ -24,7 +26,7 @@ (defun infix-creation (symbol value1 value2) (vamp:make-infix :op symbol - :lhs value + :lhs value1 :rhs value2)) @@ -83,11 +85,11 @@ ; Times[x, #] & /@ toElem[g][{values}] ; ] (let* ((x (car values)) - (rest-values (cdr values)) + (xs (cdr values)) (f (mcar obj)) (g (mcadr obj)) - (f-elems (to-vampir f rest-values)) - (g-elems (to-vampir g rest-values))) + (f-elems (to-vampir f xs)) + (g-elems (to-vampir g xs))) (mapcar #'(lambda (f-elem g-elem) (infix-creation :+ (infix-creation :* (infix-creation :- 1 x) f-elem) From 55bdd6b93038a9e48d87d7ecc384c112bc236b24 Mon Sep 17 00:00:00 2001 From: Anthony Hart Date: Wed, 26 Apr 2023 08:32:21 -0700 Subject: [PATCH 07/13] Add comments for future generations --- src/bitc/trans.lisp | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/src/bitc/trans.lisp b/src/bitc/trans.lisp index baece0cc2..131d53465 100644 --- a/src/bitc/trans.lisp +++ b/src/bitc/trans.lisp @@ -35,7 +35,7 @@ (to-vampir (mcadr obj) values))) (defmethod to-vampir ((obj fork) values) - ; toElem[fork[n_]] := Function[{inp}, Flatten[{inp, inp}, 1]] + ; Copy input n intput bits into 2*n output bits (append values values)) (defmethod to-vampir ((obj parallel) values) @@ -47,6 +47,10 @@ ; 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)) @@ -56,25 +60,30 @@ (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) @@ -84,6 +93,10 @@ ; 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)) From 621c535a56613407cbc4bc570a916bd20bc9cd33 Mon Sep 17 00:00:00 2001 From: Anthony Hart Date: Wed, 26 Apr 2023 22:11:05 -0700 Subject: [PATCH 08/13] Make 1 make constant --- src/bitc/trans.lisp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/bitc/trans.lisp b/src/bitc/trans.lisp index 131d53465..a46fa67c3 100644 --- a/src/bitc/trans.lisp +++ b/src/bitc/trans.lisp @@ -105,6 +105,6 @@ (g-elems (to-vampir g xs))) (mapcar #'(lambda (f-elem g-elem) (infix-creation :+ - (infix-creation :* (infix-creation :- 1 x) f-elem) + (infix-creation :* (infix-creation :- (vamp:make-constant :const 1) x) f-elem) (infix-creation :* x g-elem))) f-elems g-elems))) From 5f570fd2490c5c3584bf1994b8a88e4f0aef8a93 Mon Sep 17 00:00:00 2001 From: Anthony Hart Date: Wed, 26 Apr 2023 22:11:27 -0700 Subject: [PATCH 09/13] Rename bits.lisp to bitc.lisp --- geb.asd | 2 +- src/bitc/{bits.lisp => bitc.lisp} | 0 2 files changed, 1 insertion(+), 1 deletion(-) rename src/bitc/{bits.lisp => bitc.lisp} (100%) diff --git a/geb.asd b/geb.asd index 45d933406..e113aa4cd 100644 --- a/geb.asd +++ b/geb.asd @@ -69,7 +69,7 @@ :description "bitc (Boolean Circuits)" :depends-on (util vampir mixins specs) :components ((:file package) - (:file bits))) + (:file bitc))) (:module lambda :serial t :depends-on (geb specs) diff --git a/src/bitc/bits.lisp b/src/bitc/bitc.lisp similarity index 100% rename from src/bitc/bits.lisp rename to src/bitc/bitc.lisp From ee2b783b8553f5cc584f30e012d8b729208632e0 Mon Sep 17 00:00:00 2001 From: Anthony Hart Date: Wed, 26 Apr 2023 22:52:48 -0700 Subject: [PATCH 10/13] Fix bugs when translating from pairs and cases to bitc --- src/geb/trans.lisp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/geb/trans.lisp b/src/geb/trans.lisp index ebf619969..b9d11ec8b 100644 --- a/src/geb/trans.lisp +++ b/src/geb/trans.lisp @@ -120,14 +120,14 @@ ; par[toBits@mcar,id[Max[dom@mcar,dom@mcadr]-dom@mcar]], ; par[toBits@mcadr,id[Max[dom@mcar,dom@mcadr]-dom@mcadr]] ; ] - (case (bitc:branch (bitc:parallel (to-bitc (mcar obj)) (bitc:ident (- (max (bitc:dom (mcar obj)) (bitc:dom (mcadr obj))) (bitc:dom (mcar obj))))) - (bitc:parallel (to-bitc (mcadr obj)) (bitc:ident (- (max (bitc:dom (mcar obj)) (bitc:dom (mcadr obj))) (bitc:dom (mcadr obj))))))) + (case (bitc:branch (bitc:parallel (to-bitc (mcar obj)) (bitc:ident (- (max (dom (to-bitc (mcar obj))) (dom (to-bitc (mcadr obj)))) (dom (to-bitc (mcar obj)))))) + (bitc:parallel (to-bitc (mcadr obj)) (bitc:ident (- (max (dom (to-bitc (mcar obj))) (dom (to-bitc (mcadr obj)))) (dom (to-bitc (mcadr obj)))))))) ; toBits[projectRight[mcar_, mcadr_]] := par[drop[bitWidth@mcar], id[bitWidth@mcadr]] (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 (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 (bitc:compose (bitc:parallel (to-bitc (mcar obj)) (to-bitc (mcdr obj))) (bitc:fork (bitc:dom (mcar obj))))) + (pair (bitc:compose (bitc:parallel (to-bitc (mcar obj)) (to-bitc (mcdr obj))) (bitc:fork (dom (to-bitc (mcar obj)))))) ;toBits[distribute[mcar_, mcadr_, mcaddr_]] := ; par[swap[bitWidth[mcar], 1], id[Max[bitWidth@mcadr, bitWidth@mcaddr]]] (distribute (bitc:parallel (bitc:swap (to-bitc (mcar obj)) 1) (bitc:ident (max (to-bitc (mcadr obj)) (to-bitc (mcaddr obj)))))) From e897481a8ddbeffe41856e1e49f79af7663ffe85 Mon Sep 17 00:00:00 2001 From: Anthony Hart Date: Wed, 26 Apr 2023 22:54:57 -0700 Subject: [PATCH 11/13] Make implementation slightly closer to original --- src/geb/trans.lisp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/geb/trans.lisp b/src/geb/trans.lisp index b9d11ec8b..9b2bcd086 100644 --- a/src/geb/trans.lisp +++ b/src/geb/trans.lisp @@ -120,14 +120,14 @@ ; par[toBits@mcar,id[Max[dom@mcar,dom@mcadr]-dom@mcar]], ; par[toBits@mcadr,id[Max[dom@mcar,dom@mcadr]-dom@mcadr]] ; ] - (case (bitc:branch (bitc:parallel (to-bitc (mcar obj)) (bitc:ident (- (max (dom (to-bitc (mcar obj))) (dom (to-bitc (mcadr obj)))) (dom (to-bitc (mcar obj)))))) - (bitc:parallel (to-bitc (mcadr obj)) (bitc:ident (- (max (dom (to-bitc (mcar obj))) (dom (to-bitc (mcadr obj)))) (dom (to-bitc (mcadr obj)))))))) + (case (bitc:branch (bitc:parallel (to-bitc (mcar obj)) (bitc:ident (- (max (to-bitc (dom (mcar obj))) (to-bitc (dom (mcadr obj)))) (to-bitc (dom (mcar obj)))))) + (bitc:parallel (to-bitc (mcadr obj)) (bitc:ident (- (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 (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 (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 (bitc:compose (bitc:parallel (to-bitc (mcar obj)) (to-bitc (mcdr obj))) (bitc:fork (dom (to-bitc (mcar obj)))))) + (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]]] (distribute (bitc:parallel (bitc:swap (to-bitc (mcar obj)) 1) (bitc:ident (max (to-bitc (mcadr obj)) (to-bitc (mcaddr obj)))))) From 9ebdc89bc57023daf6e3dbadf98fa74b6719daac Mon Sep 17 00:00:00 2001 From: Anthony Hart Date: Thu, 27 Apr 2023 02:01:09 -0700 Subject: [PATCH 12/13] Add comments to to-bitc --- src/geb/trans.lisp | 26 ++++++++++++++++++++++++-- 1 file changed, 24 insertions(+), 2 deletions(-) diff --git a/src/geb/trans.lisp b/src/geb/trans.lisp index 9b2bcd086..3bb4221cb 100644 --- a/src/geb/trans.lisp +++ b/src/geb/trans.lisp @@ -102,16 +102,26 @@ (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) ))) @@ -120,16 +130,28 @@ ; par[toBits@mcar,id[Max[dom@mcar,dom@mcadr]-dom@mcar]], ; par[toBits@mcadr,id[Max[dom@mcar,dom@mcadr]-dom@mcadr]] ; ] - (case (bitc:branch (bitc:parallel (to-bitc (mcar obj)) (bitc:ident (- (max (to-bitc (dom (mcar obj))) (to-bitc (dom (mcadr obj)))) (to-bitc (dom (mcar obj)))))) - (bitc:parallel (to-bitc (mcadr obj)) (bitc:ident (- (max (to-bitc (dom (mcar obj))) (to-bitc (dom (mcadr obj)))) (to-bitc (dom (mcadr obj)))))))) + + ; 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)))) From f23043d7104ff50fd8b3ecdcef4100d50e705adf Mon Sep 17 00:00:00 2001 From: Anthony Hart Date: Thu, 27 Apr 2023 09:46:57 -0700 Subject: [PATCH 13/13] Allow substobj within substmorph to be handled by to-bitc --- src/geb/trans.lisp | 32 ++++++++++++++++---------------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/src/geb/trans.lisp b/src/geb/trans.lisp index 3bb4221cb..c6289f313 100644 --- a/src/geb/trans.lisp +++ b/src/geb/trans.lisp @@ -87,43 +87,43 @@ -(defmethod to-bitc ((obj )) +(defmethod bitwidth ((obj )) (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)))) + (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 (error "impossible")) + (substobj (bitc:ident (bitwidth obj))) ;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))) + (init (apply #'bitc:parallel (make-list (bitwidth (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)))) + (terminal (bitc:drop (bitwidth (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) + (inject-left (apply #'bitc:parallel (append (list bitc:zero (bitc:ident (bitwidth (mcar obj)))) + (make-list (- (max (bitwidth (mcar obj)) (bitwidth (mcadr obj))) (bitwidth (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) + (inject-right (apply #'bitc:parallel (append (list bitc:one (bitc:ident (bitwidth (mcadr obj)))) + (make-list (- (max (bitwidth (mcar obj)) (bitwidth (mcadr obj))) (bitwidth (mcadr obj))) :initial-element bitc:zero) ))) ;toBits[case[mcar_,mcadr_]]:= ; branch[ @@ -133,25 +133,25 @@ ; 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)))))))) + (case (bitc:branch (bitc:parallel (to-bitc (mcar obj)) (bitc:drop (- (max (bitwidth (dom (mcar obj))) (bitwidth (dom (mcadr obj)))) (bitwidth (dom (mcar obj)))))) + (bitc:parallel (to-bitc (mcadr obj)) (bitc:drop (- (max (bitwidth (dom (mcar obj))) (bitwidth (dom (mcadr obj)))) (bitwidth (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))))) + (project-left (bitc:parallel (bitc:ident (bitwidth (mcar obj))) (bitc:drop (bitwidth (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))))) + (project-right (bitc:parallel (bitc:drop (bitwidth (mcar obj))) (bitc:ident (bitwidth (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)))))) + (pair (bitc:compose (bitc:parallel (to-bitc (mcar obj)) (to-bitc (mcdr obj))) (bitc:fork (bitwidth (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)))))) + (distribute (bitc:parallel (bitc:swap (bitwidth (mcar obj)) 1) (bitc:ident (max (bitwidth (mcadr obj)) (bitwidth (mcaddr obj)))))) (otherwise (subclass-responsibility obj))))