Coverage report: /home/runner/work/geb/geb/test/lambda.lisp

KindCoveredAll%
expression247345 71.6
branch00nil
Key
Not instrumented
Conditionalized out
Executed
Not executed
 
Both branches taken
One branch taken
Neither branch taken
1
 (in-package :geb-test)
2
 
3
 (define-test geb.lambda
4
   :parent geb-test-suite)
5
 
6
 (def unit-term
7
   (lambda:unit))
8
 
9
 (def pair-of-units-term
10
   (lambda:pair unit-term unit-term))
11
 
12
 (def fst-pair-of-units-term
13
   (lambda:fst pair-of-units-term))
14
 
15
 (def snd-pair-of-units-term
16
   (lambda:snd pair-of-units-term))
17
 
18
 (def right-inj
19
   (lambda:right so0 unit-term))
20
 
21
 (def left-inj
22
   (lambda:left so0 unit-term))
23
 
24
 (def pair-of-injs
25
   (lambda:pair right-inj
26
                left-inj))
27
 
28
 (def on-l-r-term
29
   (lambda:case-on left-inj right-inj right-inj))
30
 
31
 (def so01-coprod
32
     (coprod so0 so1))
33
 
34
 (def so10-coprod
35
   (coprod so1 so0))
36
 
37
 (def so1-prod
38
   (prod so1 so1))
39
 
40
 (def lamb-term
41
   (lambda:lamb (list so1-prod) unit-term))
42
 
43
 (def multi-lamb-term
44
   (lambda:lamb (list so1 so0) (lambda:index 0)))
45
 
46
 (def multi-lambterm-type
47
   (lambda:type-of-term-w-fun nil multi-lamb-term))
48
 
49
 (def app-term
50
   (lambda:app lamb-term (list pair-of-units-term)))
51
 
52
 (def multi-app-term
53
   (lambda:app multi-lamb-term (list (lambda:index 0) (lambda:index 1))))
54
 
55
 (def context-list
56
   (list so1 so0 so01-coprod (geb.lambda.main:fun-type so0 so1)))
57
 
58
 (define-test type-of-unit-term-test
59
   :parent geb.lambda
60
   (is obj-equalp
61
       so1
62
       (lambda:type-of-term nil unit-term)
63
       "type of unit is so1"))
64
 
65
 (define-test type-of-pair-terms-test
66
   :parent geb.lambda
67
   (is obj-equalp
68
       so1-prod
69
       (lambda:type-of-term nil pair-of-units-term)
70
       "type of product of units is product of so1's")
71
   (is obj-equalp
72
       so1
73
       (lambda:type-of-term
74
        nil
75
        (lambda:ltm (lambda:annotated-term nil pair-of-units-term)))
76
       "type of the left unit term is so1")
77
   (is obj-equalp
78
       so1
79
       (lambda:type-of-term
80
        nil
81
        (lambda:rtm (lambda:annotated-term nil pair-of-units-term)))))
82
 
83
 (define-test fst-unit-term-test
84
   :parent geb.lambda
85
   (is obj-equalp
86
       so1
87
       (lambda:type-of-term nil fst-pair-of-units-term)
88
       "type of the projection from (prod so1 so1) is so1")
89
   (is obj-equalp
90
       so1-prod
91
       (lambda:type-of-term
92
        nil
93
        (lambda:term (lambda:annotated-term nil fst-pair-of-units-term)))
94
       "type of the term being projected is (prod so1 so1)"))
95
 
96
 (define-test snd-unit-term-test
97
   :parent geb.lambda
98
   (is obj-equalp
99
       so1
100
       (lambda:type-of-term nil snd-pair-of-units-term)
101
       "type of the projection from (prod so1 so1) is so1")
102
   (is obj-equalp
103
       so1-prod
104
       (lambda:type-of-term
105
        nil
106
        (lambda:term (lambda:annotated-term nil snd-pair-of-units-term)))
107
       "type of the term being projected is (prod so1 so1)"))
108
 
109
 (define-test proj-term-test
110
   :parent geb.lambda
111
   (is obj-equalp
112
       (prod so01-coprod so10-coprod)
113
       (lambda:type-of-term nil pair-of-injs)
114
       "type of a pair of injection is a product of coproducts")
115
   (is obj-equalp
116
       so01-coprod
117
       (lambda:type-of-term nil
118
                            (lambda:ltm
119
                             (lambda:annotated-term nil pair-of-injs)))
120
       "test type annotation for the left term")
121
   (is obj-equalp
122
       so10-coprod
123
       (lambda:type-of-term nil
124
                            (lambda:rtm
125
                             (lambda:annotated-term nil pair-of-injs)))
126
       "test type annotation for the right term"))
127
 
128
 
129
 (define-test casing-test
130
   :parent geb.lambda
131
   (is obj-equalp
132
       so01-coprod
133
       (lambda:type-of-term nil on-l-r-term)
134
       "type of term gotten from the casing")
135
   (is obj-equalp
136
       so01-coprod
137
       (lambda:type-of-term nil
138
                            (lambda:ltm
139
                             (lambda:annotated-term nil on-l-r-term)))
140
       "test type annotation for left term")
141
   (is obj-equalp
142
       so01-coprod
143
       (lambda:type-of-term nil
144
                            (lambda:rtm
145
                             (lambda:annotated-term nil on-l-r-term)))
146
       "test type annotation for right term")
147
   (is obj-equalp
148
       so10-coprod
149
       (lambda:type-of-term nil
150
                            (lambda:on
151
                             (lambda:annotated-term nil on-l-r-term)))
152
       "type of annotated term supplied for the start of casing is that
153
       of the supplied coproduct"))
154
 
155
 (define-test inl-test
156
   :parent geb.lambda
157
   (is obj-equalp
158
       so01-coprod
159
       (lambda:type-of-term nil right-inj)
160
       "type of injection is a coproduct")
161
   (is obj-equalp
162
       so1
163
       (lambda:type-of-term nil
164
                            (lambda:term
165
                             (lambda:annotated-term nil right-inj)))
166
       "test of the type of the annotated right term"))
167
 
168
 (define-test inr-test
169
   :parent geb.lambda
170
   (is obj-equalp
171
       so10-coprod
172
       (lambda:type-of-term nil left-inj)
173
       "type of injection is a coproduct")
174
   (is obj-equalp
175
       so1
176
       (lambda:type-of-term nil
177
                            (lambda:term
178
                             (lambda:annotated-term nil left-inj)))
179
       "test of the type of the annotated left term"))
180
 
181
 (define-test lamb-test
182
   :parent geb.lambda
183
   (is obj-equalp
184
       (so-hom-obj so1-prod so1)
185
       (lambda:type-of-term nil
186
                            lamb-term)
187
       "test type of lambda term")
188
   (is obj-equalp
189
       so1
190
       (lambda:type-of-term nil
191
                            (lambda:term
192
                             (lambda:annotated-term nil
193
                                                    lamb-term)))
194
       "test type of annotated term for the lambda term"))
195
 
196
 (define-test app-test
197
   :parent geb.lambda
198
   (is obj-equalp
199
       so1
200
       (lambda:type-of-term nil (lambda:app lamb-term (list pair-of-units-term)))
201
       "type of function application term")
202
   (is obj-equalp
203
       (so-hom-obj so1-prod so1)
204
       (lambda:type-of-term nil
205
                            (lambda:fun
206
                             (lambda:annotated-term nil
207
                                                    app-term)))
208
       "test annotated fun term")
209
   (is obj-equalp
210
       so1-prod
211
       (lambda:type-of-term nil
212
                            (car (lambda:term
213
                                  (lambda:annotated-term nil
214
                                                         app-term))))))
215
 
216
 (define-test index-tests
217
   :parent geb.lambda
218
   (is obj-equalp
219
       so1
220
       (lambda:type-of-term context-list (lambda:index 0)))
221
   (is obj-equalp
222
       so0
223
       (lambda:type-of-term context-list (lambda:index 1)))
224
   (is obj-equalp
225
       so01-coprod
226
       (lambda:type-of-term context-list (lambda:index 2)))
227
   (is obj-equalp
228
       (so-hom-obj so0 so1)
229
       (lambda:type-of-term context-list (lambda:index 3))))
230
 
231
 
232
 (define-test absurd-index-test
233
   :parent geb.lambda
234
   (is obj-equalp
235
       so0
236
       (lambda:type-of-term
237
        context-list
238
        (lambda:term (lambda:annotated-term context-list
239
                                            (lambda:absurd so1 (lambda:index 1)))))))
240
 
241
 (define-test exp-hom-test
242
   :parent geb.lambda
243
   (is obj-equalp
244
       (so-hom-obj (coprod so0 (so-hom-obj so1 so1))
245
                   (prod so1 (so-hom-obj so0 so1)))
246
       (lambda:type-of-term
247
        nil
248
        (lambda:fun
249
         (lambda:app (lambda:lamb
250
                      (list (coprod so0 (geb.lambda.main:fun-type so0 so1)))
251
                      (lambda:pair
252
                       unit-term
253
                       (lambda:lamb (list so1)
254
                                    (lambda:lamb (list so0)
255
                                                 (lambda:index 0)))))
256
                     (list (lambda:right so0
257
                                         (lambda:lamb (list so1) unit-term))))))))
258
 
259
 (define-test multi-lambda-test
260
   :parent geb.lambda
261
   (is obj-equalp
262
       so1
263
       (mcadr multi-lambterm-type))
264
   (is obj-equalp
265
       (prod so1 so0)
266
       (mcar multi-lambterm-type)))
267
 
268
 (define-test multi-app-term
269
   (is obj-equalp
270
       so1
271
       (lambda:type-of-term (list so1 so0) multi-app-term))
272
   (is obj-equalp
273
       (prod so1 so0)
274
       (mcar (lambda:fun (lambda:ann-term1 (list so1 so0) multi-app-term)))))
275
 
276