Coverage report: /home/runner/work/geb/geb/src/specs/geb.lisp
Kind | Covered | All | % |
expression | 76 | 139 | 54.7 |
branch | 0 | 0 | nil |
Key
Not instrumented
Conditionalized out
Executed
Not executed
Both branches taken
One branch taken
Neither branch taken
3
(defclass <substobj> (<substmorph> direct-pointwise-mixin meta-mixin cat-obj) ()
5
"the class corresponding to SUBSTOBJ. See GEB-DOCS/DOCS:@OPEN-CLOSED"))
7
`(or prod coprod so0 so1))
9
(deftype realized-object ()
10
"A realized object that can be sent into.
12
Lists represent [PROD][class] in the [\\<SUBSTOBJ\\>][class] category
14
[LEFT][class] and [RIGHT][class] represents realized values for [COPROD][class]
16
Lastly [SO1][class] and [SO0][class] represent the proper class"
23
;; we say that id doesn't exist, as we don't need the tag. If we find
24
;; that to ill typed (substobj is a substmorph as far as type checking
25
;; is concerned without an explicit id constrcutor), then we can
26
;; include it and remove it from the or type here.
28
(defclass <substmorph> (direct-pointwise-mixin meta-mixin cat-morph) ()
30
"the class type corresponding to SUBSTMORPH. See GEB-DOCS/DOCS:@OPEN-CLOSED"))
31
(deftype substmorph ()
32
"The morphisms of the [SUBSTMORPH][type] category"
34
comp init terminal case pair distribute
35
inject-left inject-right
36
project-left project-right))
38
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
39
;; Subst Constructor Objects
40
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
42
;; these could be keywords, but maybe in the future not?
43
(defclass so0 (<substobj>)
46
"The Initial Object. This is sometimes known as the
47
[VOID](https://en.wikipedia.org/wiki/Void_type) type.
49
the formal grammar of [SO0][class] is
55
where [SO0][class] is `THE` initial object.
62
"The Initial/Void Object"))
64
(defclass so1 (<substobj>)
67
"The Terminal Object. This is sometimes referred to as the
68
[Unit](https://en.wikipedia.org/wiki/Unit_type) type.
70
the formal grammar or [SO1][class] is
76
where [SO1][class] is `THE` terminal object
84
Here we construct [GEB-BOOL:BOOL] by simply stating that we have the
85
terminal object on either side, giving us two possible ways to fill
94
where applying [->LEFT] gives us the left unit, while [->RIGHT] gives
97
;; please make better names and documentation strings!
99
(defclass prod (<substobj>)
100
((mcar :initarg :mcar
103
(mcadr :initarg :mcadr
107
"The [PRODUCT][PROD class] object. Takes two CAT-OBJ values that
110
The formal grammar of [PRODUCT][PROD class] is
116
where [PROD][class] is the constructor, [MCAR] is the left value of the
117
product, and [MCADR] is the right value of the product.
122
(geb-gui::visualize (prod geb-bool:bool geb-bool:bool))
125
Here we create a product of two [GEB-BOOL:BOOL] types."))
127
(defclass coprod (<substobj>)
128
((mcar :initarg :mcar
131
(mcadr :initarg :mcadr
135
"the [CO-PRODUCT][COPROD class] object. Takes CAT-OBJ values that
136
get put into a choice of either value.
138
The formal grammar of [PRODUCT][PROD class] is
144
Where [CORPOD][class] is the constructor, [MCAR] is the left choice of
145
the sum, and [MCADR] is the right choice of the sum.
150
(geb-gui::visualize (coprod so1 so1))
153
Here we create the boolean type, having a choice between two unit
156
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
157
;; Subst Morphism Objects
158
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
160
(defclass functor (<substmorph>)
166
(defclass comp (<substmorph>)
167
((mcar :initarg :mcar
170
:documentation "The first composed morphism")
171
(mcadr :initarg :mcadr
174
:documentation "the second morphism"))
176
"The composition morphism. Takes two CAT-MORPH values that get
177
applied in standard composition order.
179
The formal grammar of [COMP][class] is
185
which may be more familiar as
191
Where [COMP][class]\\( 。\\) is the constructor, [MCAR]\\(g\\) is the second morphism
192
that gets applied, and [MCADR]\\(f\\) is the first morphism that gets
200
(<-right so1 geb-bool:bool)
201
(pair (<-left so1 geb-bool:bool)
202
(<-right so1 geb-bool:bool))))
205
In this example we are composing two morphisms. the first morphism
206
that gets applied ([PAIR] ...) is the identity function on the
207
type ([PROD][class] [SO1][class] [GEB-BOOL:BOOL]), where we pair the
208
[left projection](PROJECT-LEFT) and the [right
209
projection](PROJECT-RIGHT), followed by taking the [right
210
projection](PROJECT-RIGHT) of the type.
212
Since we know ([COMP][class] f id) is just f per the laws of category
213
theory, this expression just reduces to
216
(<-right so1 geb-bool:bool)
219
(defclass init (<substmorph>)
225
"The [INITIAL][INIT class] Morphism, takes any [CAT-OBJ] and
226
creates a moprhism from [SO0][class] (also known as void) to the object given.
228
The formal grammar of [INITIAL][INIT class] is
234
where [INIT][class] is the constructor. [OBJ] is the type of object
235
that will be conjured up from [SO0][class], when the morphism is
236
applied onto an object.
244
In this example we are creating a unit value out of void."))
246
(defclass terminal (<substmorph>)
252
"The [TERMINAL][class] morphism, Takes any [CAT-OBJ] and creates a
253
morphism from that object to [SO1][class] (also known as unit).
255
The formal grammar of [TERMINAL][class] is
261
where [TERMINAL][class] is the constructor. [OBJ] is the type of object that
262
will be mapped to [SO1][class], when the morphism is applied onto an
268
(terminal (coprod so1 so1))
270
(geb-gui::visualize (terminal (coprod so1 so1)))
272
(comp value (terminal (codomain value)))
274
(comp true (terminal bool))
277
In the first example, we make a morphism from the corpoduct of
278
[SO1][class] and [SO1][class] (essentially [GEB-BOOL:BOOL]) to
281
In the third example we can proclaim a constant function by ignoring
282
the input value and returning a morphism from unit to the desired type.
284
The fourth example is taking a [GEB-BOOL:BOOL] and returning [GEB-BOOL:TRUE]."))
286
;; Please name all of these better plz
288
(defclass inject-left (<substmorph>)
289
((mcar :initarg :mcar
293
(mcadr :initarg :mcadr
298
"The left injection morphism. Takes two CAT-OBJ values. It is
299
the dual of INJECT-RIGHT
301
The formal grammar is
307
Where [->LEFT] is the constructor, [MCAR] is the value being injected into
308
the coproduct of [MCAR] + [MCADR], and the [MCADR] is just the type for
309
the unused right constructor.
314
(geb-gui::visualize (->left so1 geb-bool:bool))
319
(->left so1 geb-bool:bool))
323
In the second example, we inject a term with the shape SO1 into a pair
324
with the shape ([SO1][class] × [GEB-BOOL:BOOL]), then we use MCASE to denote a
325
morphism saying. `IF` the input is of the shape [SO1], then give us True,
326
otherwise flip the value of the boolean coming in."))
328
(defclass inject-right (<substmorph>)
329
((mcar :initarg :mcar
333
(mcadr :initarg :mcadr
338
"The right injection morphism. Takes two CAT-OBJ values. It is
339
the dual of INJECT-LEFT
341
The formal grammar is
347
Where ->RIGHT is the constructor, [MCADR] is the value being injected into
348
the coproduct of [MCAR] + [MCADR], and the [MCAR] is just the type for
349
the unused left constructor.
354
(geb-gui::visualize (->right so1 geb-bool:bool))
359
(->right so1 geb-bool:bool))
363
In the second example, we inject a term with the shape [GEB-BOOL:BOOL]
364
into a pair with the shape ([SO1][class] × [GEB-BOOL:BOOL]), then we use
365
[MCASE] to denote a morphism saying. IF the input is of the shape [SO1],
366
then give us True, otherwise flip the value of the boolean coming in."))
368
(defclass case (<substmorph>)
369
((mcar :initarg :mcar
372
:documentation "The morphism that gets applied on the left coproduct")
373
(mcadr :initarg :mcadr
376
:documentation "The morphism that gets applied on the right coproduct"))
378
"Eliminates coproducts. Namely Takes two CAT-MORPH values, one
379
gets applied on the left coproduct while the other gets applied on the
380
right coproduct. The result of each CAT-MORPH values must be
383
The formal grammar of [CASE][class] is:
389
Where [MCASE] is the constructor, [MCAR] is the morphism that gets
390
applied to the left coproduct, and [MCADR] is the morphism that gets
391
applied to the right coproduct.
399
(->right so1 geb-bool:bool))
402
In the second example, we inject a term with the shape [GEB-BOOL:BOOL]
403
into a pair with the shape ([SO1][class] × [GEB-BOOL:BOOL]), then we use
404
[MCASE] to denote a morphism saying. IF the input is of the shape [SO1],
405
then give us True, otherwise flip the value of the boolean coming in."))
407
(defclass pair (<substmorph>)
408
((mcar :initarg :mcar
411
:documentation "The left morphism")
415
:documentation "The right morphism"))
417
"Introduces products. Namely Takes two CAT-MORPH values. When
418
the PAIR morphism is applied on data, these two [CAT-MORPH]'s are
419
applied to the object, returning a pair of the results
421
The formal grammar of constructing an instance of pair is:
427
where PAIR is the constructor, MCAR is the left morphism, and MCDR is
433
(pair (<-left so1 geb-bool:bool)
434
(<-right so1 geb-bool:bool))
436
(geb-gui::visualize (pair (<-left so1 geb-bool:bool)
437
(<-right so1 geb-bool:bool)))
440
Here this pair morphism takes the pair SO1 × GEB-BOOL:BOOL, and
441
projects back the left field [SO1][class] as the first value of the pair and
442
projects back the GEB-BOOL:BOOL field as the second values."))
444
(defclass project-left (<substmorph>)
445
((mcar :initarg :mcar
449
(mcadr :initarg :mcadr
454
"The [LEFT PROJECTION][PROJECT-LEFT class]. Takes two
455
[CAT-MORPH] values. When the [LEFT PROJECTION][PROJECT-LEFT
456
class] morphism is then applied, it grabs the left value of a product,
457
with the type of the product being determined by the two
458
[CAT-MORPH] values given.
460
the formal grammar of a [PROJECT-LEFT][class] is:
466
Where [<-LEFT] is the constructor, [MCAR] is the left type of the
467
[PRODUCT][class] and [MCADR] is the right type of the [PRODUCT][class].
473
(<-left geb-bool:bool (prod so1 geb-bool:bool)))
476
In this example, we are getting the left [GEB-BOOL:BOOL] from a
477
product with the shape
479
([GEB-BOOL:BOOL][] [×][PROD class] [SO1][class] [×][PROD class] [GEB-BOOL:BOOL])"))
481
(defclass project-right (<substmorph>)
482
((mcar :initarg :mcar
486
(mcadr :initarg :mcadr
489
:documentation "Right projection (product elimination)"))
490
(:documentation "The [RIGHT PROJECTION][PROJECT-RIGHT class]. Takes two
491
[CAT-MORPH] values. When the [RIGHT PROJECTION][PROJECT-RIGHT
492
class] morphism is then applied, it grabs the right value of a product,
493
with the type of the product being determined by the two
494
[CAT-MORPH] values given.
497
the formal grammar of a [PROJECT-RIGHT][class] is:
503
Where [<-RIGHT] is the constructor, [MCAR] is the right type of the
504
[PRODUCT][class] and [MCADR] is the right type of the [PRODUCT][class].
510
(comp (<-right so1 geb-bool:bool)
511
(<-right geb-bool:bool (prod so1 geb-bool:bool))))
514
In this example, we are getting the right [GEB-BOOL:BOOL] from a
515
product with the shape
517
([GEB-BOOL:BOOL][] [×][PROD class] [SO1][class] [×][PROD class] [GEB-BOOL:BOOL])"))
519
(defclass distribute (<substmorph>)
520
((mcar :initarg :mcar
524
(mcadr :initarg :mcadr
528
(mcaddr :initarg :mcaddr
532
(:documentation "The distributive law"))
534
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
536
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
538
(defclass left (direct-pointwise-mixin)
541
:documentation "The object that is being injected left")))
543
(defclass right (direct-pointwise-mixin)
546
:documentation "The object that is being injected left")))
548
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
549
;; Constructors for the base types
550
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
552
;; this is considered bad style, one should call their constructors
553
;; make, but it does not matter
556
"Creates a fresh so1. Useful for aliases"
557
(make-instance 'so1))
560
"Creates a fresh so0. Useful for aliases"
561
(make-instance 'so0))
563
(defparameter *so0* (make-instance 'so0)
564
"The Initial Object")
566
"The Initial Object")
567
(defparameter *so1* (make-instance 'so1)
568
"The Terminal Object")
570
"The Terminal Object")
575
(make-instance 'left :obj obj)))
580
(make-instance 'right :obj obj)))
584
(defun prod (car cadr)
586
(make-instance 'prod :mcar car :mcadr cadr)))
588
(-> coprod (t t) coprod)
589
(defun coprod (car cadr)
591
(make-instance 'coprod :mcar car :mcadr cadr)))
593
(defmacro alias (name obj)
594
`(make-alias :name ',name :obj ,obj))
596
(-> make-alias (&key (:name symbol) (:obj t)) t)
597
(defun make-alias (&key name obj)
598
(geb.mixins:meta-insert obj :alias name)
601
(defun has-aliasp (obj)
602
(multiple-value-bind (val in-there) (geb.mixins:meta-lookup obj :alias)
603
(declare (ignore val))
606
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
607
;; Constructors for the morphism constructors
608
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
609
;; we could type the objects more if wanted
611
(-> comp (cat-morph cat-morph &rest cat-morph) comp)
612
(defun comp (car cadr &rest comps)
613
(let ((list (list* car cadr comps)))
614
(mvfoldr (lambda (x acc)
615
(make-instance 'comp :mcar x :mcadr acc))
619
(-> init (cat-obj) init)
622
(make-instance 'init :obj obj)))
624
(-> terminal (cat-obj) terminal)
625
(defun terminal (obj)
627
(make-instance 'terminal :obj obj)))
629
(-> ->left (cat-obj cat-obj) inject-left)
630
(defun ->left (mcar mcadr)
631
"injects left constructor"
633
(make-instance 'inject-left :mcar mcar :mcadr mcadr)))
635
(-> ->right (cat-obj cat-obj) inject-right)
636
(defun ->right (mcar mcadr)
637
"injects right constructor"
639
(make-instance 'inject-right :mcar mcar :mcadr mcadr)))
641
(-> <-left (cat-obj cat-obj) project-left)
642
(defun <-left (mcar mcadr)
643
"projects left constructor"
645
(make-instance 'project-left :mcar mcar :mcadr mcadr)))
647
(-> <-right (cat-obj cat-obj) project-right)
648
(defun <-right (mcar mcadr)
649
"projects right constructor"
651
(make-instance 'project-right :mcar mcar :mcadr mcadr)))
653
(-> mcase (cat-morph cat-morph) case)
654
(defun mcase (mcar mcadr)
656
(make-instance 'case :mcar mcar :mcadr mcadr)))
658
(-> pair (cat-morph cat-morph) pair)
659
(defun pair (mcar mcdr)
661
(make-instance 'pair :mcar mcar :mcdr mcdr)))
663
(-> distribute (cat-obj cat-obj cat-obj) distribute)
664
(defun distribute (mcar mcadr mcaddr)
666
(make-instance 'distribute :mcar mcar :mcadr mcadr :mcaddr mcaddr)))
668
(defun make-functor (&key obj func)
669
(make-instance 'functor :func func :obj obj))
671
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
673
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
675
(defmethod mcar ((obj terminal))
678
(defmethod mcar ((obj init))
681
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
682
;; Pattern Matching conveniences
683
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
685
;; less safe than I wanted due to the names can be out of sync, but
686
;; w/e I can fix it with a better defclass macro
687
(make-pattern prod mcar mcadr)
688
(make-pattern so1 mcar mcadr)
689
(make-pattern so0 mcar mcadr)
690
(make-pattern coprod mcar mcadr)
691
(make-pattern init obj)
692
(make-pattern terminal obj)
693
(make-pattern comp mcar mcadr)
694
(make-pattern inject-left mcar mcadr)
695
(make-pattern inject-right mcar mcadr)
696
(make-pattern case mcar mcadr)
697
(make-pattern pair mcar mcdr)
698
(make-pattern project-left mcar mcadr)
699
(make-pattern project-right mcar mcadr)
700
(make-pattern distribute mcar mcadr mcaddr)