Coverage report: /home/runner/work/geb/geb/src/geb/trans.lisp

KindCoveredAll%
expression370581 63.7
branch520 25.0
Key
Not instrumented
Conditionalized out
Executed
Not executed
 
Both branches taken
One branch taken
Neither branch taken
1
 ;; Transition or Translation functions about geb
2
 
3
 (in-package :geb.trans)
4
 
5
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
6
 ;; Morph to Poly Implementation
7
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
8
 
9
 ;; This maintains exhaustion while leaving it open to extension. you
10
 ;; can subclass <substmorph>, without having to update the exhaustion
11
 ;; set, however you'll need to properly implement the interface
12
 ;; methods on it.
13
 
14
 ;; Hopefully I can form a complete list somewhere, so one can see the
15
 ;; interface functions intended.
16
 
17
 ;; We could have also derived this from methods, these are equivalent,
18
 ;; so both styles are acceptable
19
 (defmethod to-poly ((obj <substmorph>))
20
   (typecase-of substmorph obj
21
     (substobj     (error "impossible"))
22
     (init          0)
23
     (terminal      0)
24
     (inject-left   poly:ident)
25
     (inject-right  (poly:+ (obj-to-nat (mcar obj)) poly:ident))
26
     (comp          (poly:compose (to-poly (mcar obj))
27
                                  (to-poly (mcadr obj))))
28
     (project-right (let ((nat (obj-to-nat (mcadr obj))))
29
                      (if (zerop nat)
30
                          nat
31
                          (poly:mod poly:ident nat))))
32
     (project-left  (let ((nat (obj-to-nat (mcar obj))))
33
                      (if (zerop nat)
34
                          nat
35
                          ;; we want to bitshift it by the size
36
                          (poly:/
37
                           (poly:- poly:ident
38
                                   ;; we need to remove the right value
39
                                   ;; we are doing project-right
40
                                   (to-poly (<-right (mcar obj) (mcadr obj))))
41
                           nat))))
42
     (distribute    (let ((cx (obj-to-nat (mcar obj)))
43
                          (cy (obj-to-nat (mcadr obj)))
44
                          (cz (obj-to-nat (mcaddr obj))))
45
                      (if (and (zerop cy) (zerop cz))
46
                          0
47
                          (let* ((yz   (poly:+ cy cz))
48
                                 (xin  (poly:/ poly:ident yz))
49
                                 (yzin (poly:mod poly:ident yz)))
50
                            (poly:if-lt yzin cy
51
                                        (poly:+ (poly:* cy xin) yzin)
52
                                        (poly:+ (poly:* cz xin)
53
                                                (poly:- yzin cy)
54
                                                (poly:* cx cy)))))))
55
     (pair          (let* ((z  (codom (mcdr obj)))
56
                           (cz (obj-to-nat z)))
57
                      (poly:+ (poly:* cz (to-poly (mcar obj)))
58
                              (to-poly (mcdr obj)))))
59
     (case          (let* ((f      (mcar obj))
60
                           (x      (dom f))
61
                           (cx     (obj-to-nat x))
62
                           (poly-g (to-poly (mcadr obj))))
63
                      (if (zerop cx)
64
                          poly-g
65
                          (poly:if-lt poly:ident cx
66
                                      (to-poly f)
67
                                      (poly:compose poly-g
68
                                                    (poly:- poly:ident cx))))))
69
     (otherwise (subclass-responsibility obj))))
70
 
71
 ;; put here just to avoid confusion
72
 (defmethod to-poly ((obj <substobj>))
73
   (declare (ignore obj))
74
   poly:ident)
75
 
76
 (defun obj-to-nat (obj)
77
   (so-card-alg obj))
78
 
79
 (defmethod to-circuit ((obj <substmorph>) name)
80
   "Turns a @GEB-SUBSTMORPH to a Vamp-IR Term"
81
   (to-circuit (to-seqn obj) name))
82
 
83
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
84
 ;; Morph to Bitc Implementation
85
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
86
 
87
 (defmethod bitwidth ((obj <substobj>))
88
   (typecase-of substobj obj
89
     (so0     0)
90
     (so1     0)
91
     (coprod  (+ 1 (max (bitwidth (mcar obj)) (bitwidth (mcadr obj)))))
92
     (prod    (+ (bitwidth (mcar obj)) (bitwidth (mcadr obj))))
93
     (otherwise (subclass-responsibility obj))))
94
 
95
 (defmethod to-bitc ((obj <substmorph>))
96
   (typecase-of substmorph obj
97
     (substobj
98
      (bitc:ident (bitwidth obj)))
99
     (comp
100
      (bitc:compose (to-bitc (mcar obj))
101
                    (to-bitc (mcadr obj))))
102
     ;; This should never occure, but if it does, it produces a
103
     ;; constant morphism onto an all 0s list
104
     (init
105
      (let* ((list (zero-list (bitwidth (mcar obj))))
106
             (len  (length list)))
107
        (cond ((= 0 len) (bitc:drop 0))
108
              ((= 1 len) bitc:zero)
109
              (t         (apply #'bitc:parallel list)))))
110
     ;; Terminal maps any bit-list onto the empty bit-list
111
     (terminal
112
      (bitc:drop (bitwidth (mcar obj))))
113
 
114
     ;; Inject-left x -> x + y tags the x with a 0, indicating left,
115
     ;;   and pads the encoded x with as many zeros as would be needed
116
     ;;   to store either an x or a y.
117
     (inject-left
118
      (let ((car-width  (bitwidth (mcar obj)))
119
            (cadr-width (bitwidth (mcadr obj))))
120
        (apply #'bitc:parallel
121
               (append (list bitc:zero (bitc:ident car-width))
122
                       (zero-list (padding-bits cadr-width
123
                                                car-width))))))
124
     ;; Inject-right y -> x + y tags the y with a 1, indicating right,
125
     ;;   and pads the encoded y with as many zeros as would be needed
126
     ;;   to store either an x or a y.
127
     (inject-right
128
      (let ((car-width  (bitwidth (mcar obj)))
129
            (cadr-width (bitwidth (mcadr obj))))
130
        (apply #'bitc:parallel
131
               (append (list bitc:one (bitc:ident cadr-width))
132
                       (zero-list (padding-bits car-width
133
                                                cadr-width))))))
134
 
135
     ;; Case translates directly into a branch. The sub-morphisms of
136
     ;; case are padded with drop so they have the same input lengths.
137
     (case
138
       (let ((car-width  (bitwidth (dom (mcar obj))))
139
             (cadr-width (bitwidth (dom (mcadr obj)))))
140
         (bitc:branch (bitc:parallel (to-bitc (mcar obj))
141
                                     (bitc:drop
142
                                      (padding-bits cadr-width car-width)))
143
                      (bitc:parallel (to-bitc (mcadr obj))
144
                                     (bitc:drop
145
                                      (padding-bits car-width cadr-width))))))
146
     ;; project-left just drops any bits not being used to encode the
147
     ;; first component.
148
     (project-left
149
      (bitc:parallel (bitc:ident (bitwidth (mcar obj)))
150
                     (bitc:drop (bitwidth (mcadr obj)))))
151
 
152
     ;; project-right just drops any bits not being used to encode the
153
     ;; second component.
154
     (project-right
155
      (bitc:parallel (bitc:drop (bitwidth (mcar obj)))
156
                     (bitc:ident (bitwidth (mcadr obj)))))
157
 
158
     ;; Pair will copy the input and run the encoded morphisms in pair
159
     ;; on the two copied subvetors.
160
     (pair
161
      (bitc:compose (bitc:parallel (to-bitc (mcar obj)) (to-bitc (mcdr obj)))
162
                    (bitc:fork (bitwidth (dom (mcar obj))))))
163
     ;; a * (b + c) will be encoded as [a] [0 or 1] [b or c]. By
164
     ;; swapping the [0 or 1] with [a], we get an encoding for (a * b)
165
     ;; + (a * c).
166
     (distribute
167
      (bitc:parallel (bitc:swap (bitwidth (mcar obj)) 1)
168
                     (bitc:ident (max (bitwidth (mcadr obj))
169
                                      (bitwidth (mcaddr obj))))))
170
     (otherwise (subclass-responsibility obj))))
171
 
172
 (defun zero-list (length)
173
   (make-list length :initial-element bitc:zero))
174
 
175
 (-> padding-bits ((integer 0) (integer 0)) (integer 0))
176
 (defun padding-bits (number number2)
177
   "
178
 ```lisp
179
 (max number number2)
180
 ```
181
 is the bits needed to store NUMBER or NUMBER2
182
 
183
 Thus if we want to calculate the number of padding bits needed then we
184
 should calculate
185
 
186
 ```lisp
187
 (- (max number number2) number2)
188
 ```
189
 
190
 We use an optimized version in actual code, which happens to compute the same result"
191
   (max (- number number2) 0))
192
 
193
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
194
 ;; Geb to Seqn Implementation
195
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
196
 
197
 (defmethod to-seqn ((obj <substobj>))
198
   "Preserves identity morphims"
199
   (seqn:id (geb.common:width obj)))
200
 
201
 (defmethod to-seqn ((obj geb.extension.spec:<natobj>))
202
   (seqn:id (geb.common:width obj)))
203
 
204
 (defmethod to-seqn ((obj comp))
205
   "Preserves composition"
206
   (seqn:composition (to-seqn (mcar obj))
207
                     (to-seqn (mcadr obj))))
208
 
209
 (defmethod to-seqn ((obj init))
210
   "Produces a list of zeroes
211
 Currently not aligning with semantics of drop-width
212
 as domain and codomain can be of differing lengths"
213
   (seqn:drop-width (list 0)
214
                    (width (mcar obj))))
215
 
216
 (defmethod to-seqn ((obj terminal))
217
   "Drops everything to the terminal object,
218
 i.e. to nothing"
219
   (drop-nil (width (mcar obj))))
220
 
221
 (defmethod to-seqn ((obj inject-left))
222
   "Injects an x by marking its entries with 0
223
 and then inserting as padded bits if necessary"
224
   (let ((l1 (width (mcar obj)))
225
         (l3 (width (coprod (mcar obj)
226
                               (mcadr obj)))))
227
     ;; (a1,...,an) -> (0, a1,...,an) -> (1, max(a1, b1),..., max(an, 0) or max(an, bn))
228
     ;; if lengths match
229
     (composition (parallel-seq zero-bit
230
                                (inj-coprod-parallel l1 l3))
231
                  (inj-length-right (list 0)
232
                                    l1))))
233
 
234
 (defmethod to-seqn ((obj inject-right))
235
   "Injects an x by marking its entries with 1
236
 and then inserting as padded bits if necessary"
237
   (let ((l2 (width (mcadr obj)))
238
         (l3 (width (coprod (mcar obj)
239
                               (mcadr obj)))))
240
     (composition (parallel-seq one-bit
241
                                (inj-coprod-parallel l2
242
                                                     l3))
243
                  (inj-length-right (list 0)
244
                                    l2))))
245
 
246
 (defmethod to-seqn ((obj case))
247
   "Cases by forgetting the padding and if necessary dropping
248
 the extra entries if one of the inputs had more of them to start
249
 with"
250
   (let* ((lft (dom (mcar obj)))
251
          (rt  (dom (mcadr obj)))
252
          (cpr (dom obj))
253
          (wlft (width lft))
254
          (wrt  (width rt))
255
          (mcar (mcar obj))
256
          (mcadr (mcadr obj))
257
          (lengthleft (length wlft))
258
          (lengthright (length wrt)))
259
     (labels
260
         ((funor (x y z)
261
            (composition (to-seqn z)
262
                         (composition (remove-right x)
263
                                      (parallel-seq
264
                                       (drop-width (butlast
265
                                                    (cdr (width cpr))
266
                                                    (- (length y)
267
                                                       (length x)))
268
                                                   x)
269
                                       (drop-nil (nthcdr (1+ (length x))
270
                                                         (width cpr)))))))
271
          (funinj (x y)
272
            (composition (to-seqn x)
273
                         (drop-width (cdr (width cpr)) y))))
274
       (cond ((< lengthleft lengthright)
275
              ;; branch on the left counts the first entries of an occuring and drops the rest
276
              ;; then injects it into the smaller bit sizes if necessary
277
              ;; (max(a1, b1),,,.,(max (an, bn),..., max(0, bm))) -> (a1,...,an,0)
278
              ;; -> (a1,....,an)
279
              ;; branch on the right is just injecting
280
              ;; (max(a1, b1),..., max(0, bn)) -> (b1, ...., bn) -> codom))
281
              (branch-seq (funor wlft wrt mcar) (funinj mcadr wrt)))
282
             ((< lengthright lengthleft)
283
              (branch-seq (funinj mcar wlft) (funor wrt wlft mcadr)))
284
             ((= lengthright lengthleft)
285
              (branch-seq (funinj mcar wlft) (funinj mcadr wrt)))))))
286
 
287
 (defmethod to-seqn ((obj project-left))
288
   "Takes a list of an even length and cuts the right half"
289
   (let ((sw (width (mcar obj))))
290
     (composition (remove-right sw)
291
                  (parallel-seq (id sw)
292
                                (drop-nil (width (mcadr obj)))))))
293
 
294
 (defmethod to-seqn  ((obj project-right))
295
   "Takes a list of an even length and cuts the left half"
296
   (let ((sw (width (mcadr obj))))
297
     (composition (remove-left sw)
298
                  (parallel-seq (drop-nil (width (mcar obj)))
299
                                (id sw)))))
300
 
301
 (defmethod to-seqn ((obj pair))
302
   "Forks entries and then applies both morphism
303
 on corresponding entries"
304
   (composition (parallel-seq (to-seqn (mcar obj))
305
                              (to-seqn (mcdr obj)))
306
                (fork-seq (width (dom obj)))))
307
 
308
 (defmethod to-seqn ((obj distribute))
309
   "Given A x (B + C) simply moves the 1-bit entry
310
 to the front and keep the same padding relations to
311
 get ((A x B) + (A x C)) as times appends sequences"
312
   (shift-front (width (dom obj))
313
                (1+ (length (width (mcar obj))))))
314
 
315
 (defmethod to-seqn ((obj geb.extension.spec:nat-add))
316
   "Addition is interpreted as addition"
317
   (seqn-add (geb.extension.spec:num obj)))
318
 
319
 (defmethod to-seqn ((obj geb.extension.spec:nat-mult))
320
   "Multiplication is interpreted as multiplication"
321
   (seqn-multiply (geb.extension.spec:num obj)))
322
 
323
 (defmethod to-seqn ((obj geb.extension.spec:nat-sub))
324
   "Subtraction is interpreted as subtraction"
325
   (seqn-subtract (geb.extension.spec:num obj)))
326
 
327
 (defmethod to-seqn ((obj geb.extension.spec:nat-div))
328
   "Division is interpreted as divition"
329
   (seqn-divide (geb.extension.spec:num obj)))
330
 
331
 (defmethod to-seqn ((obj geb.extension.spec:nat-mod))
332
   "Modulo is interpreted as modulo"
333
   (seqn-mod (geb.extension.spec:num obj)))
334
 
335
 (defmethod to-seqn ((obj geb.extension.spec:nat-const))
336
   "A choice of a natural number is the same exact choice in SeqN"
337
   (seqn-nat (geb.extension.spec:num obj) (geb.extension.spec:pos obj)))
338
 
339
 (defmethod to-seqn ((obj geb.extension.spec:nat-inj))
340
   "Injection of bit-sizes is interpreted in the same maner in SeqN"
341
   (let ((num (geb.extension.spec:num obj)))
342
     (inj-size num (1+ num))))
343
 
344
 (defmethod to-seqn ((obj geb.extension.spec:nat-concat))
345
   "Concatenation is interpreted as concatenation"
346
   (seqn-concat (geb.extension.spec:num-left obj)
347
                (geb.extension.spec:num-right obj )))
348
 
349
 (defmethod to-seqn ((obj geb.extension.spec:one-bit-to-bool))
350
   "Iso interpreted in an evident manner"
351
   (inj-length-left (list 1) (list 0)))
352
 
353
 (defmethod to-seqn ((obj geb.extension.spec:nat-decompose))
354
   "Decomposition is interpreted on the nose"
355
   (seqn-decompose (geb.extension.spec:num obj)))
356
 
357
 (defmethod to-seqn ((obj geb.extension.spec:nat-eq))
358
   "Equality predicate is interpreted on the nose"
359
   (seqn-eq (geb.extension.spec:num obj)))
360
 
361
 (defmethod to-seqn ((obj geb.extension.spec:nat-lt))
362
   "Equality predicate is interpreted on the nose"
363
   (seqn-lt (geb.extension.spec:num obj)))