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

KindCoveredAll%
expression335924 36.3
branch1046 21.7
Key
Not instrumented
Conditionalized out
Executed
Not executed
 
Both branches taken
One branch taken
Neither branch taken
1
 ;; General Functions about geb
2
 
3
 (in-package :geb.main)
4
 
5
 (defmethod curry-prod (fun fst (snd <substobj>))
6
   (match-of substobj snd
7
     (so0          (terminal fst))
8
     (so1          (comp fun (pair fst
9
                                   (terminal fst))))
10
     ((coprod x y) (pair (curry (left-morph  (comp fun (gather fst x y))))
11
                         (curry (right-morph (comp fun (gather fst x y))))))
12
     (prod         (curry (curry (prod-left-assoc fun))))))
13
 
14
 (defmethod curry-prod (fun fst (snd <natobj>))
15
   (let ((num (num snd)))
16
     (if (= num 1)
17
         (pair
18
          ;; On the left, see what the morphism does at 0
19
          (curry (comp fun
20
                       (prod-mor fst
21
                                 (nat-const 1 0))))
22
          ;; On the left, see what the morphism does at 0
23
          (curry (comp fun
24
                       (prod-mor fst
25
                                 (nat-const 1 1)))))
26
         (curry (comp fun
27
                      (prod-mor fst
28
                                (nat-concat 1 (1- num))))))))
29
 
30
 (defmethod dom ((x <substmorph>))
31
   (assure cat-obj
32
     (typecase-of substmorph x
33
       (init         so0)
34
       (terminal     (obj x))
35
       (substobj     x)
36
       (inject-left  (mcar x))
37
       (inject-right (mcadr x))
38
       (comp         (dom (mcadr x)))
39
       (pair         (dom (mcar x)))
40
       (distribute   (prod (mcar x) (coprod (mcadr x) (mcaddr x))))
41
       (case         (coprod (dom (mcar x)) (dom (mcadr x))))
42
       ((or project-right
43
            project-left)
44
        (prod (mcar x) (mcadr x)))
45
       (otherwise
46
        (subclass-responsibility x)))))
47
 
48
 (defmethod dom ((x <natmorph>))
49
   (cond ((typep x 'nat-concat)      (prod (nat-width (num-left x))
50
                                           (nat-width (num-right x))))
51
         ((typep x 'nat-const)       so1)
52
         ((typep x 'nat-inj)         (nat-width (num x)))
53
         ((typep x 'one-bit-to-bool) (nat-width 1))
54
         ((typep x 'nat-decompose)   (nat-width (num x)))
55
         (t                          (let ((bit (nat-width (num x))))
56
                                      (prod bit bit)))))
57
 
58
 (defmethod dom ((x <natobj>))
59
   x)
60
 
61
 (defmethod dom ((ref reference))
62
   ref)
63
 
64
 (defmethod codom ((ref reference))
65
   ref)
66
 
67
 (defmethod codom ((x <substmorph>))
68
   (assure cat-obj
69
     (typecase-of substmorph x
70
       (terminal      so1)
71
       (init          (obj x))
72
       (substobj      x)
73
       (project-left  (mcar x))
74
       (project-right (mcadr x))
75
       (comp          (codom (mcar x)))
76
       (case          (codom (mcar x)))
77
       (pair          (prod (codom (mcar x))
78
                            (codom (mcdr x))))
79
       (distribute    (coprod (prod (mcar x) (mcadr x))
80
                              (prod (mcar x) (mcaddr x))))
81
       ((or inject-left
82
            inject-right)
83
        (coprod (mcar x) (mcadr x)))
84
       (otherwise
85
        (subclass-responsibility x)))))
86
 
87
 (defmethod codom ((x <natmorph>))
88
   (typecase-of natmorph x
89
     (nat-inj         (nat-width (1+ (num x))))
90
     (nat-concat      (nat-width (+ (num-left x) (num-right x))))
91
     (one-bit-to-bool (coprod so1 so1))
92
     (nat-decompose   (prod (nat-width 1) (nat-width (1- (num x)))))
93
     ((or nat-eq
94
          nat-lt)
95
      (coprod so1 so1))
96
     ((or nat-add
97
          nat-sub
98
          nat-mult
99
          nat-div
100
          nat-const
101
          nat-mod)
102
      (nat-width (num x)))
103
     (otherwise
104
      (subclass-responsibility x))))
105
 
106
 (defmethod codom ((x <natobj>))
107
   x)
108
 
109
 
110
 (-> const (cat-morph cat-obj) (or t comp))
111
 (defun const (f x)
112
   "The constant morphism.
113
 
114
 Takes a morphism from [SO1][class] to a desired value of type $B$,
115
 along with a [\\<SUBSTOBJ\\>] that represents the input type say of
116
 type $A$, giving us a morphism from $A$ to $B$.
117
 
118
 Thus if:
119
 F : [SO1][class] → a,
120
 X : b
121
 
122
 then: (const f x) : a → b
123
 
124
 ```
125
 Γ, f : so1 → b, x : a
126
 ----------------------
127
 (const f x) : a → b
128
 ```
129
 
130
 Further, If the input `F` has an ALIAS, then we wrap the output
131
 in a new alias to denote it's a constant version of that value.
132
 
133
 
134
 Example:
135
 
136
 ```lisp
137
 (const true bool) ; bool -> bool
138
 ```"
139
   (let ((obj (comp f (terminal x)))
140
         (alias (meta-lookup f :alias)))
141
     (if alias
142
         (make-alias :name (intern (format nil "CONST-~A" alias))
143
                     :obj obj)
144
         obj)))
145
 
146
 (-> cleave (cat-morph &rest cat-morph) pair)
147
 (defun cleave (v1 &rest values)
148
   "Applies each morphism to the object in turn."
149
   (if (null values)
150
       v1
151
       (mvfoldr #'pair (cons v1 (butlast values)) (car (last values)))))
152
 
153
 ;; Should this be in a geb.utils: package or does it deserve to be in
154
 ;; the main geb package?
155
 
156
 (-> commutes (cat-obj cat-obj) pair)
157
 (defun commutes (x y)
158
   (pair (<-right x y) (<-left x y)))
159
 
160
 
161
 ;; TODO easy tests to make for it, just do it!
162
 (-> commutes-left (cat-morph) comp)
163
 (defun commutes-left (morph)
164
   "swap the input [domain][DOM] of the given [cat-morph]
165
 
166
 In order to swap the [domain][DOM] we expect the [cat-morph] to
167
 be a [PROD][class]
168
 
169
 Thus if: `(dom morph) ≡ (prod x y)`, for any `x`, `y` [CAT-OBJ]
170
 
171
 then: `(commutes-left (dom morph)) ≡ (prod y x)`
172
 u
173
 ```
174
 Γ, f : x × y → a
175
 ------------------------------
176
 (commutes-left f) : y × x → a
177
 ```
178
 "
179
   (let ((dom (dom morph)))
180
     (if (not (typep dom 'prod))
181
         (error "object ~A need to be of a product type, however it is of ~A"
182
                morph dom)
183
         (comp morph (commutes (mcadr dom) (mcar dom))))))
184
 
185
 (-> !-> (substobj substobj) substobj)
186
 (defun !-> (a b)
187
   (etypecase-of substobj a
188
     (so0    so1)
189
     (so1    b)
190
     (coprod (prod (!-> (mcar a)  b)
191
                   (!-> (mcadr a) b)))
192
     (prod   (!-> (mcar a)
193
                  (!-> (mcadr a) b)))))
194
 
195
 (defgeneric so-card-alg (obj)
196
   (:documentation "Gets the cardinality of the given object, returns a FIXNUM"))
197
 
198
 ;; (-> so-card-alg (<substobj>) fixnum)
199
 (defmethod so-card-alg ((obj <substobj>))
200
   ;; we don't use the cata morphism so here we are. Doesn't give me
201
   ;; much extra
202
   (match-of geb:substobj obj
203
     ((geb:prod a b)   (* (so-card-alg a)
204
                          (so-card-alg b)))
205
     ((geb:coprod a b) (+ (so-card-alg a)
206
                          (so-card-alg b)))
207
     (geb:so0          1)
208
     (geb:so1          1)))
209
 
210
 (defmethod so-eval ((x <substobj>) y)
211
   (match-of substobj x
212
     (so0          (comp (init y) (<-right so1 so0)))
213
     (so1          (<-left y so1))
214
     ((coprod a b) (comp (mcase (comp (so-eval a y)
215
                                      (so-forget-middle (so-hom-obj a y) (so-hom-obj b y) a))
216
                                (comp (so-eval b y)
217
                                      (so-forget-first (so-hom-obj a y) (so-hom-obj b y) b)))
218
                         (distribute (prod (so-hom-obj a y) (so-hom-obj b y)) a b)))
219
     ((prod a b)   (let ((eyz   (so-eval b y))
220
                         (exhyz (so-eval a (so-hom-obj b y)))
221
                         (hom   (so-hom-obj a (so-hom-obj b y))))
222
                     (comp eyz
223
                           (pair (comp exhyz (so-forget-right hom a b))
224
                                 (comp (<-right a b)
225
                                       (<-right hom (prod a b)))))))))
226
 
227
 (defmethod so-eval ((x <natobj>) y)
228
   (let ((num (num x)))
229
     (if (= num 1)
230
         (comp (so-eval (coprod so1 so1)
231
                        y)
232
               (prod-mor (so-hom-obj x y)
233
                         one-bit-to-bool))
234
         (comp (so-eval (prod (nat-width 1)
235
                              (nat-width (1- num)))
236
                        y)
237
               (prod-mor (so-hom-obj x y)
238
                         (nat-decompose num))))))
239
 
240
 (defmethod so-hom-obj ((x <substobj>) z)
241
   (match-of substobj x
242
     (so0          so1)
243
     (so1          z)
244
     ((coprod x y) (prod (so-hom-obj x z)
245
                         (so-hom-obj y z)))
246
     ((prod x y)   (so-hom-obj x (so-hom-obj y z)))))
247
 
248
 (defmethod so-hom-obj ((x <natobj>) z)
249
   (let ((num (num x))
250
         (bool (coprod so1 so1)))
251
     (if (= num 1)
252
         (so-hom-obj bool
253
                     z)
254
         ;; The left part of the product is associated with what the
255
         ;; function does on 0, right part of what it does on 1
256
         ;; using the choice of interpreting false as left and
257
         ;; true as right in bool
258
         (so-hom-obj  (prod  (nat-width 1)
259
                             (nat-width (1- num)))
260
                      z))))
261
 
262
 (-> so-forget-right (cat-obj cat-obj cat-obj) substmorph)
263
 (defun so-forget-right (x y z)
264
   (pair (<-left x (prod y z))
265
         (comp (<-left y z)
266
               (<-right x (prod y z)))))
267
 
268
 (-> so-forget-middle (cat-obj cat-obj cat-obj) substmorph)
269
 (defun so-forget-middle (x y z)
270
   (pair (comp (<-left x y) (<-left (prod x y) z))
271
         (<-right (prod x y) z)))
272
 
273
 (-> so-forget-first (cat-obj cat-obj cat-obj) substmorph)
274
 (defun so-forget-first (x y z)
275
   (pair (comp (<-right x y) (<-left (prod x y) z))
276
         (<-right (prod x y) z)))
277
 
278
 (defun gather (x y z)
279
   (pair (mcase (<-left x y) (<-left x z))
280
         (mcase (comp (->left y z) (<-right x y))
281
                (comp (->right y z) (<-right x z)))))
282
 
283
 (defun prod-left-assoc (f)
284
   (trivia:match (dom f)
285
     ((prod w (prod x y))
286
      (comp f (pair (comp (<-left w x) (<-left (prod w x) y))
287
                    (pair (comp (<-right w x) (<-left (prod w x) y))
288
                          (<-right (prod w x) y)))))
289
     (_ (error "object ~A need to be of a double product type, however it is of ~A" f (dom f)))))
290
 
291
 (defun right-morph (f)
292
   (trivia:match (dom f)
293
     ((coprod x y)
294
      (comp f (->right x y)))
295
     (_ (error "object ~A need to be of a coproduct type, however it is of ~A"
296
               f (dom f)))))
297
 
298
 (defun left-morph (f)
299
   (trivia:match (dom f)
300
     ((coprod x y)
301
      (comp f (->left x y)))
302
     (_ (error "object ~A need to be of a coproduct type, however it is of ~A"
303
               f (dom f)))))
304
 
305
 (defun coprod-mor (f g)
306
   "Given f : A  → B and g : C  → D gives appropriate morphism between
307
 [COPROD][class] objects f x g : A + B  → C + D via the unversal property.
308
 That is, the morphism part of the coproduct functor Geb x Geb → Geb"
309
   (mcase (comp (->left (codom f) (codom g))
310
                f)
311
          (comp (->right (codom f) (codom g))
312
                g)))
313
 
314
 (defun prod-mor (f g)
315
    "Given f : A  → B and g : C  → D gives appropriate morphism between
316
 [PROD][class] objects f x g : A x B  → C x D via the unversal property.
317
 This is the morphism part of the product functor Geb x Geb → Geb"
318
   (pair (comp f
319
               (<-left (dom f) (dom g)))
320
         (comp g
321
               (<-right (dom f) (dom g)))))
322
 
323
 (defgeneric text-name (morph)
324
   (:documentation
325
    "Gets the name of the moprhism"))
326
 
327
 (defmethod text-name ((morph <substmorph>))
328
   (typecase-of substmorph morph
329
     (project-left  "π₁")
330
     (project-right "π₂")
331
     (inject-left   "ι₁")
332
     (inject-right  "ι₂")
333
     (terminal       "τ")
334
     (init           "Init")
335
     (distribute     "Dist")
336
     ((or case pair) "")
337
     (comp           "")
338
     (substobj       "Id")
339
     (otherwise (subclass-responsibility morph))))
340
 
341
 (defmethod text-name ((morph opaque-morph))
342
   "")
343
 (defmethod text-name ((morph cat-obj))
344
   "Id")
345
 
346
 (defmethod maybe ((obj <substobj>))
347
   "I recursively add maybe terms to all [\\<SBUSTOBJ\\>][class] terms,
348
 for what maybe means checkout [my generic function documentation][maybe].
349
 
350
 turning [products][prod] of A x B into Maybe (Maybe A x Maybe B),
351
 
352
 turning [coproducts][coprod] of A | B into Maybe (Maybe A | Maybe B),
353
 
354
 turning [SO1] into Maybe [SO1]
355
 
356
 and [SO0] into Maybe [SO0]"
357
   (coprod so1 obj))
358
 
359
 (defmethod maybe ((obj <natobj>))
360
   (coprod so1 obj))
361
 
362
 (defun curry (f)
363
   "Curries the given object, returns a [cat-morph]
364
 
365
 The [cat-morph] given must have its DOM be of a PROD type, as [CURRY][function]
366
 invokes the idea of
367
 
368
 if f : ([PROD][class] a b) → c
369
 
370
 for all `a`, `b`, and `c` being an element of [cat-morph]
371
 
372
 then: (curry f): a → c^b
373
 
374
 where c^b means c to the exponent of b (EXPT c b)
375
 
376
 
377
 ```
378
 Γ, f : a × b → c,
379
 --------------------
380
 (curry f) : a → c^b
381
 ```
382
 
383
 In category terms, `a → c^b` is isomorphic to `a → b → c`
384
 
385
 "
386
   (if (not (typep (dom f) 'prod))
387
       (error "object ~A need to be of a product type, however it is of ~A" f (dom f))
388
       (let ((dom (dom f)))
389
         (curry-prod f (mcar dom) (mcadr dom)))))
390
 
391
 (defun uncurry (y z f)
392
   "Given a morphism f : x → z^y and explicitly given y and z variables
393
 produces an uncurried version f' : x × y → z of said morphism"
394
   (comp (so-eval y z)
395
         (pair (comp f (<-left (dom f) y)) (<-right (dom f) y))))
396
 
397
 (defun morph-type (f)
398
   "Given a moprhism f : a → b gives a list (a, b) of the domain and
399
 codomain respectively"
400
   (list (dom f) (codom f)))
401
 
402
 (defmethod gapply ((morph <substmorph>) object)
403
   "My main documentation can be found on [GAPPLY][generic-function]
404
 
405
 I am the [GAPPLY][generic-function] for [\\<SBUSTMORPH\\>][class], the
406
 OBJECT that I expect is of type [REALIZED-OBJECT][type]. See the
407
 documentation for [REALIZED-OBJECT][type] for the forms it can take.
408
 
409
 Some examples of me are
410
 
411
 ```lisp
412
 GEB> (gapply (comp
413
               (mcase geb-bool:true
414
                      geb-bool:not)
415
               (->right so1 geb-bool:bool))
416
              (left so1))
417
 (right s-1)
418
 GEB> (gapply (comp
419
               (mcase geb-bool:true
420
                      geb-bool:not)
421
               (->right so1 geb-bool:bool))
422
              (right so1))
423
 (left s-1)
424
 GEB> (gapply geb-bool:and
425
              (list (right so1)
426
                    (right so1)))
427
 (right s-1)
428
 GEB> (gapply geb-bool:and
429
              (list (left so1)
430
                    (right so1)))
431
 (left s-1)
432
 GEB> (gapply geb-bool:and
433
              (list (right so1)
434
                    (left so1)))
435
 (left s-1)
436
 GEB> (gapply geb-bool:and
437
              (list (left so1)
438
                    (left so1)))
439
 (left s-1)
440
 ```
441
 "
442
   (typecase-of substmorph morph
443
     ;; object should be a list here
444
     (project-left (car object))
445
     ;; object should be a list here
446
     (project-right (cadr object))
447
     ;; inject the left and rights
448
     (inject-left   (left object))
449
     (inject-right  (right object))
450
     (terminal      so1)
451
     ;; we could generate an arbitrary type for some subest of types,
452
     ;; and use this as a fuzzer, but alas
453
     (init          (error "Can't generate a type from void"))
454
     (case (etypecase-of realized-object object
455
             (left
456
              (gapply (mcar morph) (obj object)))
457
             (right
458
              (gapply (mcadr morph) (obj object)))
459
             ((or so0 so1 list)
460
              (error "invalid type application, trying to apply a
461
              function with a dom of type ~A to an object with value ~A"
462
                     (dom morph)
463
                     object))))
464
     (pair (list (gapply (mcar morph) object)
465
                 (gapply (mcdr morph) object)))
466
     (comp (gapply (mcar morph)
467
                   (gapply (mcadr morph) object)))
468
     (distribute
469
      (etypecase-of realized-object (cadr object)
470
        (left
471
         (left (list (car object) (obj (cadr object)))))
472
        (right
473
         (right (list (car object) (obj (cadr object)))))
474
        ((or so1 so0 list)
475
         (error "invalid type application, trying to apply a
476
              function with a dom of type ~A to an object with value ~A"
477
                (dom morph)
478
                (cadr object)))))
479
     (substobj object)
480
     (otherwise (subclass-responsibility morph))))
481
 
482
 (defmethod gapply ((morph <natmorph>) object)
483
   (typecase-of natmorph morph
484
     (nat-add   (+ (car object) (cadr object)))
485
     (nat-mult  (* (car object) (cadr object)))
486
     (nat-sub   (- (car object) (cadr object)))
487
     (nat-div   (multiple-value-bind (q)
488
                    (floor (car object) (cadr object)) q))
489
     (nat-mod   (mod (car object) (cadr object)))
490
     (nat-const  (pos morph))
491
     (nat-inj    object)
492
     (nat-concat  (+ (* (expt 2 (num-right morph)) (car object)) (cadr object)))
493
     (one-bit-to-bool (if (= object 0)
494
                          (left so1)
495
                          (right so1)))
496
     (nat-decompose (if (>= object  (expt 2 (1- (num morph))))
497
                        (list 1 (- object (expt 2 (1- (num morph)))))
498
                        (list 0 object)))
499
     (nat-eq        (if (= (car object) (cadr object))
500
                        (left so1)
501
                        (right so1)))
502
     (nat-lt        (if (< (car object) (cadr object))
503
                        (left so1)
504
                        (right so1)))
505
     (otherwise (subclass-responsibility morph))))
506
 
507
 ;; I believe this is the correct way to use gapply for cat-obj
508
 (defmethod gapply ((morph cat-obj) object)
509
   "My main documentation can be found on [GAPPLY][generic-function]
510
 
511
 I am the [GAPPLY][generic-function] for a generic [CAT-OBJ][class]. I
512
 simply return the object given to me"
513
   object)
514
 
515
 (defmethod gapply ((morph opaque-morph) object)
516
   "My main documentation can be found on [GAPPLY][generic-function]
517
 
518
 I am the [GAPPLY][generic-function] for a generic [OPAQUE-MOPRH][class]
519
 I simply dispatch [GAPPLY][generic-function] on my interior code
520
 ```lisp
521
 GEB> (gapply (comp geb-list:*car* geb-list:*cons*)
522
              (list (right geb-bool:true-obj) (left geb-list:*nil*)))
523
 (right GEB-BOOL:TRUE)
524
 ```"
525
   (gapply (code morph) object))
526
 
527
 (defmethod gapply ((morph opaque) object)
528
   "My main documentation can be found on [GAPPLY][generic-function]
529
 
530
 I am the [GAPPLY][generic-function] for a generic [OPAQUE][class] I
531
 simply dispatch [GAPPLY][generic-function] on my interior code, which
532
 is likely just an object"
533
   (gapply (code morph) object))
534
 
535
 (defmethod well-defp-cat ((morph <substmorph>))
536
   (etypecase-of substmorph morph
537
     (comp
538
      (let ((mcar (mcar morph))
539
            (mcadr (mcadr morph)))
540
        (if (and (well-defp-cat mcar)
541
                 (well-defp-cat mcadr)
542
                 (obj-equalp (dom mcar)
543
                             (codom mcadr)))
544
            t
545
            (error "(Co)Domains do not match for ~A" morph))))
546
     (case
547
         (let ((mcar (mcar morph))
548
               (mcadr (mcadr morph)))
549
           (if (and (well-defp-cat mcar)
550
                    (well-defp-cat mcadr)
551
                    (obj-equalp (codom mcar)
552
                                (codom mcadr)))
553
               t
554
               (error "Casing ill-defined for ~A" morph))))
555
     (pair
556
      (let ((mcar (mcar morph))
557
            (mcdr (mcdr morph)))
558
        (if (and (well-defp-cat mcar)
559
                 (well-defp-cat mcdr)
560
                 (obj-equalp (dom mcar)
561
                             (dom mcdr)))
562
            t
563
            (error "Pairing ill-defined for ~A" morph))))
564
     ((or substobj
565
          init
566
          terminal
567
          project-left
568
          project-right
569
          inject-left
570
          inject-right
571
          distribute)
572
      t)))
573
 
574
 (defmethod well-defp-cat ((morph <natmorph>))
575
   t)
576
 
577
 (defmethod well-defp-cat ((morph <natobj>))
578
   t)
579
 ������������������������������������������������������������������������