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

KindCoveredAll%
expression3078 38.5
branch00nil
Key
Not instrumented
Conditionalized out
Executed
Not executed
 
Both branches taken
One branch taken
Neither branch taken
1
 (in-package :geb.extension.spec)
2
 
3
 ;; Sadly no polynomial category to extend ☹
4
 (defclass common-sub-expression (direct-pointwise-mixin meta-mixin cat-morph)
5
   ((obj :initarg :obj
6
         :accessor obj)
7
    (name :initarg :name
8
          :accessor name))
9
   (:documentation
10
    "I represent common sub-expressions found throughout the code.
11
 
12
 I implement a few categorical extensions. I am a valid
13
 [CAT-MORPH][class] along with fulling the interface for the
14
 [GEB.POLY.SPEC:<POLY>] category.
15
 
16
 The name should come from an algorithm that automatically fines common
17
 sub-expressions and places the appropriate names."))
18
 
19
 
20
 (defclass opaque (cat-obj meta-mixin)
21
   ((name :initarg :name :accessor name)
22
    (code :initarg :code :accessor code))
23
   (:documentation
24
    "I represent an object where we want to hide the implementation
25
 details of what kind of [GEB:SUBSTOBJ][type] I am."))
26
 
27
 (defclass reference (cat-obj cat-morph direct-pointwise-mixin meta-mixin)
28
   ((name :initarg :name :accessor name))
29
   (:documentation
30
    "I represent a reference to an [OPAQUE][class] identifier."))
31
 
32
 (defclass opaque-morph (cat-morph meta-mixin)
33
   ((code :initarg :code
34
          :accessor code
35
          :documentation "the code that represents the underlying morphsism")
36
    (dom :initarg :dom
37
         :accessor dom
38
         :documentation "The dom of the opaque morph")
39
    (codom :initarg :codom
40
           :accessor codom
41
           :documentation "The codom of the opaque morph"))
42
   (:documentation
43
    "This represents a morphsim where we want to deal with an
44
 [OPAQUE][class] that we know intimate details of"))
45
 
46
 (defun make-common-sub-expression (&key obj name)
47
   (make-instance 'common-sub-expression :obj obj :name name))
48
 
49
 (defun reference (name)
50
   (make-instance 'reference :name name))
51
 
52
 (defun opaque-morph (code &key (dom (dom code)) (codom (codom code)))
53
   (make-instance 'opaque-morph :code code :dom dom :codom codom))
54
 
55
 (defun opaque (name code)
56
   (make-instance 'opaque :name name :code code))
57
 
58
 (defclass <natobj> (direct-pointwise-mixin meta-mixin cat-obj cat-morph) ()
59
   (:documentation "the class corresponding to [NATOBJ], the extension of
60
 [SUBSTOBJ][class] adding to Geb bit representation of natural numbers." ))
61
 
62
 (deftype natobj ()
63
   '(or nat-width))
64
 
65
 (defclass <natmorph> (direct-pointwise-mixin meta-mixin cat-morph) ()
66
   (:documentation "the class corresponding to [NATMORPH], the extension of
67
 [SUBSTMORPH][class] adding to Geb basic operations on bit representations
68
 of natural numbers"))
69
 
70
 (deftype natmorph ()
71
   '(or nat-add nat-inj nat-mult nat-sub nat-div nat-const nat-concat
72
        one-bit-to-bool nat-decompose nat-eq nat-lt nat-mod))
73
 
74
 (defclass nat-width (<natobj>)
75
   ((num :initarg :num
76
         :accessor num
77
         :documentation ""))
78
   (:documentation
79
    "the [NAT-WIDTH][class] object. Takes a non-zero natural
80
 number [NUM] and produces an object standing for cardinality
81
 2^([NUM]) corresponding to [NUM]-wide bit number.
82
 
83
 The formal grammar of [NAT-WIDTH][class] is
84
 
85
 ```lisp
86
 (nat-width num)
87
 ```
88
 
89
 where [NAT-WIDTH][class] is the constructor, [NUM] the choice
90
 of a natural number we want to be the width of the bits we
91
 are to consder."))
92
 
93
 (-> nat-width (fixnum) nat-width)
94
 (defun nat-width (num)
95
   (values
96
    (make-instance 'nat-width :num num)))
97
 
98
 (defclass nat-add (<natmorph>)
99
   ((num :initarg :num
100
         :accessor num
101
         :documentation ""))
102
   (:documentation "Given a natural number [NUM] greater than 0, gives a morphsm
103
 (nat-add num) : (nat-mod num) x (nat-mod num) -> (nat-mod num) representing
104
 floored addition of two bits of length n.
105
 
106
 The formal grammar of [NAT-ADD][class] is
107
 
108
 ```lisp
109
 (nat-add num)
110
 ``` "))
111
 
112
 (defclass nat-mult (<natmorph>)
113
   ((num :initarg :num
114
         :accessor num
115
         :documentation ""))
116
   (:documentation "Given a natural number [NUM] greater than 0, gives a morphsm
117
 (nat-mult num) : (nat-mod num) x (nat-mod num) -> (nat-mod n) representing floored
118
 multiplication in natural numbers modulo n.
119
 
120
 The formal grammar of [NAT-MULT][class] is
121
 
122
 ```lisp
123
 (nat-mult num)
124
 ``` "))
125
 
126
 (defclass nat-sub (<natmorph>)
127
   ((num :initarg :num
128
         :accessor num
129
         :documentation ""))
130
   (:documentation "Given a natural number [NUM] greater than 0, gives a morphsm
131
 (nat-sub sum) : (nat-mod num) x (nat-mod num) -> (nat-mod num) representing
132
 floored subtraction of two bits of length n.
133
 
134
 The formal grammar of [NAT-SUB][class] is
135
 
136
 ```lisp
137
 (nat-sub num)
138
 ``` "))
139
 
140
 (defclass nat-div (<natmorph>)
141
   ((num :initarg :num
142
         :accessor num
143
         :documentation ""))
144
   (:documentation "Given a natural number [NUM] greater than 0, gives a morphsm
145
 (nat-div num) : (nat-mod num) x (nat-mod num) -> (nat-mod num) representing
146
 floored division in natural numbers modulo n.
147
 
148
 The formal grammar of [NAT-DIV][class] is
149
 
150
 ```lisp
151
 (nat-div num)
152
 ``` "))
153
 
154
 (defclass nat-const (<natmorph>)
155
   ((num :initarg :num
156
         :accessor num
157
         :documentation "")
158
    (pos :initarg :pos
159
         :accessor pos
160
         :documentation ""))
161
   (:documentation "Given a NUM natural number, gives a morphsm
162
 (nat-const num pos) : so1 -> (nat-width num).
163
 
164
 That is, chooses the POS natural number as a NUM-wide bit number
165
 
166
 The formal grammar of [NAT-ADD][class] is
167
 
168
 ```lisp
169
 (nat-const num pos)
170
 ``` "))
171
 
172
 (defclass nat-inj (<natmorph>)
173
   ((num :initarg :num
174
         :accessor num
175
         :documentation ""))
176
   (:documentation "Given a nutural number [NUM] presents a [NUM]-wide bit number
177
 as a ([NUM] + 1)-wide bit number via injecting.
178
 
179
 The formal grammar of [NAT-INJ][class] is
180
 
181
 ```lisp
182
 (nat-inj num)
183
 ```
184
 
185
 In Geb, the injection presents itself as a morphism
186
 (nat-width num) -> (nat-width (1 + num))"))
187
 
188
 (defclass nat-concat (<natmorph>)
189
   ((num-left :initarg :num-left
190
              :accessor num-left
191
              :documentation "")
192
    (num-right :initarg :num-right
193
               :accessor num-right
194
               :documentation ""))
195
   (:documentation "Given two natural numbers of bit length n and m, concatenates
196
 them in that order giving a bit of length n + m.
197
 
198
 The formal grammar of [NAT-CONCAT][class] is
199
 
200
 ```lisp
201
 (nat-concat num-left num-right)
202
 ```
203
 
204
 In Geb this corresponds to a morphism
205
 (nat-width num-left) x (nat-width num-right) -> (nat-width (n + m))
206
 
207
 For a translation to SeqN simply take x of n width and y of m with and
208
 take x^m + y"))
209
 
210
 (defclass one-bit-to-bool (<natmorph>)
211
   ()
212
   (:documentation "A map nat-width 1 -> bool sending #*0 to
213
 false and #*1 to true"))
214
 
215
 (defclass nat-decompose (<natmorph>)
216
   ((num :initarg :num
217
         :accessor num
218
         :documentation ""))
219
   (:documentation "Morphism nat-width n -> (nat-width 1) x (nat-width (1- n))
220
 splitting a natural number into the last and all but last collection of bits"))
221
 
222
 (defclass nat-eq (<natmorph>)
223
   ((num :initarg :num
224
         :accessor num
225
         :documentation ""))
226
   (:documentation "Morphism nat-width n x nat-width n -> bool
227
 which evaluated to true iff both inputs are the same"))
228
 
229
 (defclass nat-lt (<natmorph>)
230
   ((num :initarg :num
231
         :accessor num
232
         :documentation ""))
233
   (:documentation "Morphism nat-width n x nat-width n -> bool
234
 which evaluated to true iff the first input is less than the second"))
235
 
236
 (defclass nat-mod (<natmorph>)
237
   ((num :initarg :num
238
         :accessor num
239
         :documentation ""))
240
   (:documentation "Morphism nat-width n x nat-width n -> nat-width n
241
 which takes a modulo of the left projection of a pair by the second
242
 projection of a pari"))
243
 
244
 (defun nat-add (num)
245
   (values
246
    (make-instance 'nat-add :num num)))
247
 
248
 
249
 (defun nat-mult (num)
250
   (values
251
    (make-instance 'nat-mult :num num)))
252
 
253
 
254
 (defun nat-sub (num)
255
   (values
256
    (make-instance 'nat-sub :num num)))
257
 
258
 
259
 (defun nat-div (num)
260
   (values
261
    (make-instance 'nat-div :num num)))
262
 
263
 
264
 (defun nat-const (num pos)
265
   (values
266
    (make-instance 'nat-const :num num :pos pos)))
267
 
268
 
269
 (defun nat-inj (num)
270
   (values
271
    (make-instance 'nat-inj :num num)))
272
 
273
 
274
 (defun nat-concat (num-left num-right)
275
   (values
276
    (make-instance 'nat-concat :num-left num-left :num-right num-right)))
277
 
278
 (defun one-bit-to-bool ()
279
   (make-instance 'one-bit-to-bool))
280
 
281
 (defparameter *one-bit-to-bool*
282
   (make-instance 'one-bit-to-bool))
283
 
284
 (def one-bit-to-bool *one-bit-to-bool*)
285
 
286
 (defun nat-decompose (num)
287
   (make-instance 'nat-decompose :num num))
288
 
289
 (defun nat-eq (num)
290
   (make-instance 'nat-eq :num num))
291
 
292
 (defun nat-lt (num)
293
   (make-instance 'nat-lt :num num))
294
 
295
 (defun nat-mod (num)
296
   (make-instance 'nat-mod :num num))
297
 
298
 (defgeneric num (obj))
299
 (defgeneric pos (obj))
300
 (defgeneric num-left (obj))
301
 (defgeneric num-right (obj))
302
 
303
 
304
 
305
 
306
 
307
 
308
 ��