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

KindCoveredAll%
expression455678 67.1
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.trans
4
   :parent geb-test-suite)
5
 
6
 (def pair-bool-stlc
7
   (lambda:pair
8
    (lambda:right so1 (lambda:unit))
9
    (lambda:left so1 (lambda:unit))))
10
 
11
 (def lambda-not-with-lambda
12
   (lambda:lamb
13
    (list (coprod so1 so1))
14
    (lambda:case-on (lambda:index 0)
15
                    (lambda:lamb (list so1) (lambda:right so1 (lambda:unit)))
16
                    (lambda:lamb (list so1) (lambda:left so1 (lambda:unit))))))
17
 
18
 (def lambda-not-without-lambda
19
   (lambda:lamb
20
    (list (coprod so1 so1))
21
    (lambda:case-on (lambda:index 0)
22
                    (lambda:right so1 (lambda:unit))
23
                    (lambda:left so1 (lambda:unit)))))
24
 
25
 (def proper-not
26
   (lambda:lamb
27
    (list (coprod so1 so1))
28
    (lambda:case-on (lambda:index 0)
29
                    (lambda:right so1 (lambda:index 0))
30
                    (lambda:left so1 (lambda:index 0)))))
31
 
32
 (def lambda-pairing
33
   (lambda:lamb (list geb-bool:bool)
34
                (lambda:pair (lambda:right so1 (lambda:index 0))
35
                             (lambda:left so1 (lambda:index 0)))))
36
 
37
 (def bool-id
38
   (lambda:lamb (list (coprod so1 so1)) (geb.lambda:index 0)))
39
 
40
 (def case-error-left
41
   (lambda:case-on (lambda:left so1 (lambda:unit))
42
                   (lambda:err so1)
43
                   (lambda:unit)))
44
 
45
 (def case-error-right
46
   (lambda:case-on (lambda:left so1 (lambda:unit))
47
                   (lambda:unit)
48
                   (lambda:err so1)))
49
 
50
 (def case-error-top
51
   (lambda:case-on (lambda:err (coprod so1 so1))
52
                   (lambda:unit)
53
                   (lambda:unit)))
54
 
55
 (def context-dependent-case
56
   (lambda:case-on (lambda:index 0)
57
                   (lambda:err so1)
58
                   (lambda:unit)))
59
 
60
 (def one-bit
61
   (lambda:bit-choice 1))
62
 
63
 (def plus-one
64
   (lambda:lamb (list (nat-width 24)) (lambda:plus (lambda:index 0)
65
                                                   one-bit)))
66
 (def minus-one
67
   (lambda:lamb (list (nat-width 24)) (lambda:minus (lambda:index 0)
68
                                                    one-bit)))
69
 
70
 (def less-than-1 (lambda:lamb (list (nat-width 24))
71
                               (lambda:case-on (lambda:lamb-lt (lambda:index 0)
72
                                                               one-bit)
73
                                               (lambda:bit-choice 0)
74
                                               (lambda:bit-choice 1))))
75
 (def is-1 (lambda:lamb (list (nat-width 24))
76
                        (lambda:case-on (lambda:lamb-eq (lambda:index 0)
77
                                                        one-bit)
78
                                        (lambda:bit-choice 0)
79
                                        (lambda:bit-choice 1))))
80
 
81
 (def issue-58-circuit
82
   (to-circuit
83
    (lambda:case-on
84
     (lambda:left so1 (lambda:unit))
85
     (lambda:lamb (list so1) (lambda:right so1 (lambda:unit)))
86
     (lambda:lamb (list so1) (lambda:left so1 (lambda:unit))))
87
    :tc_issue_58))
88
 
89
 (defparameter *issue-94-circuit*
90
   (lambda:app (lambda:lamb (list (lambda:fun-type
91
                                   (lambda:fun-type (coprod so1 so1)
92
                                                    (coprod so1 so1))
93
                                   (coprod so1 so1)))
94
                            (lambda:app (lambda:index 0)
95
                                        (list (lambda:lamb (list (coprod so1 so1))
96
                                                           (lambda:index 0)))))
97
               (list (lambda:lamb (list (lambda:fun-type (coprod so1 so1)
98
                                                         (coprod so1 so1)))
99
                                  (lambda:left so1 (lambda:unit))))))
100
 
101
 
102
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
103
 ;;                    Interpreter tests                      ;;
104
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
105
 
106
 (define-test lambda.trans-eval :parent geb.lambda.trans)
107
 
108
 (define-test lambda.case-works-as-expected :parent lambda.trans-eval
109
   (is equalp #*0 (gapply (to-bitc lambda-not-with-lambda) #*1))
110
   (is equalp #*1 (gapply (to-bitc lambda-not-with-lambda) #*0))
111
   (is equalp
112
       (gapply (to-bitc lambda-not-without-lambda) #*0)
113
       (gapply (to-bitc lambda-not-with-lambda) #*0))
114
   (is equalp
115
       (gapply (to-bitc lambda-not-without-lambda) #*1)
116
       (gapply (to-bitc lambda-not-with-lambda) #*1))
117
   (is equalp (list 0 0) (gapply (to-seqn lambda-not-with-lambda) (list 1 0 0)))
118
   (is equalp (list 1 0) (gapply (to-seqn lambda-not-with-lambda) (list 0 0 0)))
119
   (is equalp (gapply (to-seqn lambda-not-without-lambda) (list 0 0 0))
120
              (gapply (to-seqn lambda-not-with-lambda) (list 0 0 0)))
121
   (is equalp (gapply (to-seqn lambda-not-without-lambda) (list 1 0 0))
122
              (gapply (to-seqn lambda-not-with-lambda) (list 1 0 0))))
123
 
124
 (define-test lambda.preserves-pair :parent lambda.trans-eval
125
   (is obj-equalp
126
       (list (right (right so1))
127
             (left (right so1)))
128
       (gapply (to-cat nil lambda-pairing) (list (right so1) so1))))
129
 
130
 
131
 (define-test gapply-bool-id :parent lambda.trans-eval
132
   (is obj-equalp
133
       (right so1)
134
       (gapply
135
        (to-cat nil bool-id)
136
        (list (right so1) so1)))
137
   (is obj-equalp
138
       (left so1)
139
       (gapply
140
        (to-cat nil bool-id)
141
        (list (left so1) so1)))
142
   (is obj-equalp #*0 (gapply (to-bitc bool-id) #*0))
143
   (is obj-equalp #*1 (gapply (to-bitc bool-id) #*1))
144
   (is obj-equalp (list 0 0) (gapply (to-seqn bool-id) (list 0 0 0)))
145
   (is obj-equalp (list 1 0) (gapply (to-seqn bool-id) (list 1 0 0))))
146
 
147
 (define-test lambda.not-works :parent lambda.trans-eval
148
   (is obj-equalp (left so1)  (gapply (to-cat nil proper-not)
149
                                      (list (geb:right so1) so1)))
150
   (is obj-equalp (right so1) (gapply (to-cat nil proper-not)
151
                                      (list (geb:left so1) so1)))
152
   (is equalp #*0 (gapply (to-bitc proper-not) #*1))
153
   (is equalp #*1 (gapply (to-bitc proper-not) #*0))
154
   (is equalp (list 0 0) (gapply (to-seqn proper-not) (list 1 0 0)))
155
   (is equalp (list 1 0) (gapply (to-seqn proper-not) (list 0 0 0))))
156
 
157
 (define-test error-handling-case :parent lambda.trans-eval
158
   (is obj-equalp (left so1) (gapply (to-cat nil case-error-left)
159
                                     (list so1)))
160
   (is obj-equalp (right so1) (gapply (to-cat nil case-error-right)
161
                                      (list so1)))
162
   (is obj-equalp (left so1) (gapply (to-cat nil case-error-top)
163
                                     (list so1)))
164
   (is obj-equalp (left so1) (gapply (to-cat (list (coprod so1 so1))
165
                                             context-dependent-case)
166
                                     (list (left so1)
167
                                           so1)))
168
   (is obj-equalp (right so1) (gapply (to-cat (list (coprod so1 so1))
169
                                              context-dependent-case)
170
                                      (list (right so1)
171
                                            so1))))
172
 
173
 (define-test arithmetic-compilation :parent lambda.trans-eval
174
   (is obj-equalp 1 (gapply (to-cat nil plus-one) (list 0 so1)))
175
   (is obj-equalp 2 (gapply (to-cat nil plus-one) (list 1 so1)))
176
   (is obj-equalp (list 1) (gapply (to-seqn plus-one) (list 0 0)))
177
   (is obj-equalp (list 2) (gapply (to-seqn plus-one) (list 1 0)))
178
   (is obj-equalp 0 (gapply (to-cat nil less-than-1) (list 0 so1)))
179
   (is obj-equalp 1 (gapply (to-cat nil less-than-1) (list 1 so1)))
180
   (is obj-equalp (list 0) (gapply (to-seqn less-than-1) (list 0 so1)))
181
   (is obj-equalp (list 1) (gapply (to-seqn less-than-1) (list 1 so1)))
182
   (is obj-equalp 0 (gapply (to-cat nil is-1) (list 1 so1)))
183
   (is obj-equalp 1 (gapply (to-cat nil is-1) (list 0 so1)))
184
   (is obj-equalp (list 0) (gapply (to-seqn is-1) (list 1 so1)))
185
   (is obj-equalp (list 1) (gapply (to-seqn is-1) (list 0 so1))))
186
 
187
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
188
 ;;               Compile checked term tests                  ;;
189
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
190
 
191
 (define-test compile-checked-term :parent geb.lambda.trans
192
   (is obj-equalp
193
       (to-cat nil (lambda:unit))
194
       (geb:terminal so1)
195
       "compile unit"))
196
 
197
 (define-test stlc-ctx-to-mu :parent compile-checked-term
198
   (is equalp
199
       (lambda:stlc-ctx-to-mu nil)
200
       so1
201
       "compile in a nil context"))
202
 
203
 (define-test fold-singleton-unit-context :parent compile-checked-term
204
   (is obj-equalp
205
       (lambda:stlc-ctx-to-mu (list so1))
206
       (prod so1 so1)
207
       "fold singleton unit context"))
208
 
209
 (define-test fold-singleton-bool-context :parent compile-checked-term
210
   (is obj-equalp
211
       (lambda:stlc-ctx-to-mu (list geb-bool:bool))
212
       (prod geb-bool:bool so1)
213
       "fold singleton bool context"))
214
 
215
 (define-test fold-multi-object-context :parent compile-checked-term
216
   (is obj-equalp
217
       (lambda:stlc-ctx-to-mu  (list geb-bool:bool so0 so1))
218
       (prod geb-bool:bool (prod so0 (prod so1 so1)))
219
       "fold multi-object context"))
220
 
221
 (define-test so-hom-so1-so1 :parent compile-checked-term
222
   (is equalp
223
       (lambda:so-hom so1 so1)
224
       so1
225
       "compute hom(so1,so1)"))
226
 
227
 
228
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
229
 ;;                Vampir Extractions Tests                   ;;
230
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
231
 
232
 ;; vampir extraction tests, make better tests please.
233
 
234
 (define-test lambda-vampir-test :parent geb.lambda.trans
235
   (of-type list (to-circuit
236
                  (lambda:left so1 (lambda:unit))
237
                  :tc_unit_to_bool_left))
238
   (of-type list (to-circuit
239
                  (lambda:right so1 (lambda:unit))
240
                  :tc_unit_to_bool_right))
241
   (of-type list (to-circuit (lambda:fst pair-bool-stlc) :tc_fst_bool))
242
   (of-type list (to-circuit (lambda:unit) :tc_unit_to_unit))
243
   (of-type list (to-circuit (to-cat (list so0)
244
                                     (lambda:absurd so1 (lambda:index 0)))
245
                             :tc_void_to_unit))
246
   (of-type list issue-58-circuit))
247
 
248
 (define-test issue-94-compiles :parent geb.lambda.trans
249
   (parachute:finish
250
    (geb.entry:compile-down :stlc t
251
                            :entry "geb-test::*issue-94-circuit*"
252
                            :stream nil)))