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

KindCoveredAll%
expression308667 46.2
branch1126 42.3
Key
Not instrumented
Conditionalized out
Executed
Not executed
 
Both branches taken
One branch taken
Neither branch taken
1
 (in-package :geb.lambda.trans)
2
 
3
 (named-readtables:in-readtable :fare-quasiquote)
4
 
5
 (deftype stlc-context () `list)
6
 
7
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
8
 ;; Main Transformers
9
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
10
 
11
 (defmethod to-bitc ((obj <stlc>))
12
   "I convert a lambda term into a [GEB.BITC.SPEC:BITC] term
13
 
14
 Note that [\\<STLC\\>] terms with free variables require a context,
15
 and we do not supply them here to conform to the standard interface
16
 
17
 If you want to give a context, please call [to-cat] before
18
 calling me"
19
   (~>> obj
20
        (to-cat nil)
21
        geb.common:to-bitc))
22
 
23
 (defmethod to-poly ((obj <stlc>))
24
   "I convert a lambda term into a [GEB.POLY.SPEC:POLY] term
25
 
26
 Note that [\\<STLC\\>] terms with free variables require a context,
27
 and we do not supply them here to conform to the standard interface
28
 
29
 If you want to give a context, please call [to-cat] before
30
 calling me"
31
   (~>> obj
32
        (to-cat nil)
33
        geb.common:to-poly))
34
 
35
 (defmethod to-seqn ((obj <stlc>))
36
   "I convert a lambda term into a [GEB.SEQN.SPEC:SEQN] term
37
 
38
 Note that [\\<STLC\\>] terms with free variables require a context,
39
 and we do not supply them here to conform to the standard interface
40
 
41
 If you want to give a context, please call [to-cat] before
42
 calling me"
43
   (~>> obj
44
        (to-cat nil)
45
        geb.common:to-seqn))
46
 
47
 (defmethod to-circuit ((obj <stlc>) name)
48
   "I convert a lambda term into a vampir term
49
 
50
 Note that [\\<STLC\\>] terms with free variables require a context,
51
 and we do not supply them here to conform to the standard interface
52
 
53
 If you want to give a context, please call [to-cat] before
54
 calling me"
55
   (assure list
56
     (~> (to-seqn obj)
57
         (geb.common:to-circuit name))))
58
 
59
 (defmethod empty ((class (eql (find-class 'list)))) nil)
60
 
61
 (defmethod to-cat (context (tterm <stlc>))
62
   "Compiles a checked term in said context to a Geb morphism. If the term has
63
 an instance of an erorr term, wraps it in a Maybe monad, otherwise, compiles
64
 according to the term model interpretation of STLC"
65
   (if (errorp tterm)
66
       (to-cat-err context tterm)
67
       (to-cat-cor context tterm)))
68
 
69
 (defun maybe-comp (ob)
70
   "Takes a [SUBSTOBJ][GEB.SPEC:SUBSTOBJ] with possible fun-type instances
71
 and removes them"
72
   (fun-to-hom (maybe ob)))
73
 
74
 (defun maybe-rest (ob)
75
   "Takes a Geb object wrapped in Maybe and gives out the part without the
76
 error node"
77
   (mcadr (maybe-comp ob)))
78
 
79
 (defun dispatch (tterm)
80
   (typecase tterm
81
     (plus #'nat-add)
82
     (minus #'nat-sub)
83
     (times #'nat-mult)
84
     (divide #'nat-div)
85
     (lamb-eq #'nat-eq)
86
     (lamb-lt #'nat-lt)
87
     (modulo #'nat-mod)))
88
 
89
 (defparameter *int* (nat-width 24)
90
   "A Juvix stand-in for a type of integers of their bit-choice.
91
 In this version, the choice is that of 24-bits.")
92
 
93
 (def int *int*)
94
 
95
 (defmethod to-cat-err (context (tterm <stlc>))
96
   "Wrapps compilation in a maybe monad. The inductive hypothesis is:
97
 term TTERM with type TTYPE in context A1....An gets interpreted as a
98
 morphism of type A1 x ... x An x so1 -> 1 + TTYPE"
99
   (labels ((rec (context tterm)
100
              (match-of stlc tterm
101
                ((absurd tcod term)
102
                 (comp (coprod-mor so1
103
                                   (init tcod))
104
                       (rec context term)))
105
                (unit
106
                 (comp (->right so1 so1)
107
                       (terminal (stlc-ctx-to-mu context))))
108
                ((left rty term)
109
                 (comp (coprod-mor so1
110
                                   (->left (ttype term) rty))
111
                       (rec context term)))
112
                ((right lty term)
113
                 (comp (coprod-mor so1
114
                                   (->right lty (ttype term)))
115
                       (rec context term)))
116
                ((case-on on ltm rtm)
117
                 (let ((mcartoon  (mcar (ttype on)))
118
                       (mcadrtoon (mcadr (ttype on)))
119
                       (ctx       (stlc-ctx-to-mu context)))
120
                   (comp (comp (mcase (comp (->left so1 (ttype ltm))
121
                                            (terminal (prod ctx so1)))
122
                                      (comp (mcase (commutes-left
123
                                                    (rec (cons mcartoon context)
124
                                                         ltm))
125
                                                   (commutes-left
126
                                                    (rec (cons mcadrtoon context)
127
                                                         rtm)))
128
                                            (distribute ctx mcartoon mcadrtoon)))
129
                               (distribute ctx
130
                                           so1
131
                                           (coprod mcartoon
132
                                                   mcadrtoon)))
133
                         (geb:pair ctx (rec context on)))))
134
                ((pair ltm rtm)
135
                 (let ((tyltm (ttype ltm))
136
                       (tyrtm (ttype rtm)))
137
                   (comp (mcase (comp (->left so1 (ttype tterm))
138
                                      (terminal (prod (maybe tyltm) so1)))
139
                                (commutes-left (comp
140
                                                (coprod-mor (terminal (prod tyrtm
141
                                                                            so1))
142
                                                            (commutes-left (prod tyrtm tyltm)))
143
                                                (distribute tyrtm
144
                                                            so1
145
                                                            tyltm))))
146
                         (comp (distribute (maybe tyltm)
147
                                           so1
148
                                           tyrtm)
149
                               (geb:pair (rec context (ltm tterm))
150
                                         (rec context (rtm tterm)))))))
151
                ((fst term)
152
                 (let ((ttype (ttype term)))
153
                   (comp (coprod-mor so1 (<-left (mcar ttype) (mcadr ttype)))
154
                         (rec context term))))
155
                ((snd term)
156
                 (let ((ttype (ttype term)))
157
                   (comp (coprod-mor so1 (<-left (mcar ttype) (mcadr ttype)))
158
                         (rec context term))))
159
                (lamb
160
                 (error "No function application passes"))
161
                (app
162
                 (error "No function application passes"))
163
                ((index pos)
164
                 (comp (->right so1 (codom (stlc-ctx-proj context pos)))
165
                       (stlc-ctx-proj context pos)))
166
                ((bit-choice bitv)
167
                 (comp (->right so1 (nat-width 24))
168
                       (comp (nat-const 24 bitv)
169
                             (terminal (stlc-ctx-to-mu context)))))
170
                ((err ttype)
171
                 (comp (->left so1 ttype)
172
                       (terminal (stlc-ctx-to-mu context))))
173
                ((or plus
174
                     minus
175
                     times
176
                     divide
177
                     lamb-eq
178
                     lamb-lt
179
                     modulo)
180
                 (let ((tyltm (ttype (ltm tterm)))
181
                       (tyrtm (ttype (rtm tterm))))
182
                   (labels ((arith (op)
183
                              (comp (mcase (comp (->left so1 (ttype tterm))
184
                                                 (terminal (prod (maybe tyltm) so1)))
185
                                           (commutes-left (comp
186
                                                           (coprod-mor (terminal (prod tyrtm
187
                                                                                       so1))
188
                                                                       (commutes-left (funcall op 24)))
189
                                                           (distribute tyrtm
190
                                                                       so1
191
                                                                       tyltm))))
192
                                    (comp (distribute (maybe tyltm)
193
                                                      so1
194
                                                      tyrtm)
195
                                          (geb:pair (rec context (ltm tterm))
196
                                                    (rec context (rtm tterm)))))))
197
                     (arith (dispatch tterm)))))))
198
            (rec1 (ctx tterm)
199
              (if (typep tterm 'lamb)
200
                  (rec1 (append (tdom tterm) ctx)
201
                        (term tterm))
202
                  (list ctx tterm))))
203
     (if (not (well-defp context tterm))
204
         (error "not a well-defined ~A in said ~A" tterm context)
205
         (let* ((term (geb.lambda.main:reducer tterm))
206
                (recc (rec1 context term))
207
                (car (car recc)))
208
           (rec car
209
                (ann-term1 car
210
                           (cadr recc)))))))
211
 
212
 (defmethod to-cat-cor (context (tterm <stlc>))
213
   "Compiles a checked term in an appropriate context into the
214
 morphism of the GEB category. In detail, it takes a context and a term with
215
 following restrictions: Terms come from [STLC][type]  with occurences of
216
 [SO-HOM-OBJ][GEB.COMMON:SO-HOM-OBJ] replaced by [FUN-TYPE][class] and should
217
 come without the slow of [TTYPE][generic-function] accessor filled for any of
218
 the subterms. Context should be a list of [SUBSTOBJ][GEB.SPEC:SUBSTOBJ] with
219
 the caveat that instead of [SO-HOM-OBJ][GEB.COMMON:SO-HOM-OBJ] we ought to use
220
 [FUN-TYPE][class], a stand-in for the internal hom object with explicit
221
 accessors to the domain and the codomain. Once again, note that it is important
222
 for the context and term to be giving as per above description. While not
223
 always, not doing so result in an error upon evaluation. As an example of a
224
 valid entry we have
225
 
226
 ```lisp
227
  (to-cat-cor (list so1 (fun-type so1 so1)) (app (index 1) (list (index 0))))
228
 ```
229
 
230
 while
231
 
232
 ```lisp
233
 (to-cat-cor (list so1 (so-hom-obj so1 so1)) (app (index 1) (list (index 0))))
234
 ```
235
 
236
 produces an error. Error of such kind mind pop up both on the level of evaluating
237
 [WELL-DEFP][generic-function] and [ANN-TERM1][generic-function].
238
 
239
 Moreover, note that for terms whose typing needs addition of new context
240
 we append contexts on the left rather than on the right contra usual type
241
 theoretic notation for the convenience of computation. That means, e.g. that
242
 asking for a type of a lambda term as below produces:
243
 
244
 ```lisp
245
 LAMBDA> (ttype (term (ann-term1 nil (lamb (list so1 so0) (index 0)))))
246
 s-1
247
 ```
248
 
249
 as we count indeces from the left of the context while appending new types to
250
 the context on the left as well. For more info check [LAMB][class]
251
 
252
 Finally, note that the compilation uncurries the final morphism. That is,
253
 if the type of the term is an exponential object, [TO-CAT-COR] uncurries the
254
 morphism in the Geb category instead producing a morphism into the domain
255
 of the exponential from a corresponding product. If the exponential is
256
 iterated, so is the uncurrying."
257
   (labels ((rec (context tterm)
258
              (match-of stlc tterm
259
                ((absurd tcod term)
260
                 (comp (init tcod)
261
                       (rec context term)))
262
                (unit
263
                 (terminal (stlc-ctx-to-mu context)))
264
                ((left rty term)
265
                 (comp (->left (ttype term) rty)
266
                       (rec context term)))
267
                ((right lty term)
268
                 (comp (->right lty (ttype term))
269
                       (rec context term)))
270
                ((case-on on ltm rtm)
271
                 (let ((mcartoon  (mcar (ttype on)))
272
                       (mcadrtoon (mcadr (ttype on)))
273
                       (ctx       (stlc-ctx-to-mu context)))
274
                   (comp (mcase (commutes-left (rec
275
                                                (cons (fun-to-hom mcartoon) context) ltm))
276
                                (commutes-left (rec
277
                                                (cons  (fun-to-hom mcadrtoon) context) rtm)))
278
                         (comp (distribute ctx mcartoon mcadrtoon)
279
                               (geb:pair ctx (rec context on))))))
280
                ((pair ltm rtm)
281
                 (geb:pair (rec context ltm)
282
                           (rec context rtm)))
283
                ((fst term)
284
                 (let ((tottt (ttype term)))
285
                   (comp (<-left (mcar tottt) (mcadr tottt))
286
                         (rec context term))))
287
                ((snd term)
288
                 (let ((tottt (ttype term)))
289
                   (comp (<-right (mcar tottt) (mcadr tottt))
290
                         (to-cat context term))))
291
                ((lamb tdom term)
292
                 (apply-n (length tdom)
293
                          #'(lambda (x) (curry (commutes-left x)))
294
                          (rec (append tdom context) term)))
295
                ((app fun term)
296
                 (let ((tofun (ttype fun))
297
                       (reducify (reduce #'geb:pair
298
                                         (mapcar #'(lambda (x) (rec context x))
299
                                                 term)
300
                                         :from-end t)))
301
                   (if (typep fun 'lamb)
302
                       (comp (to-cat-cor context fun)
303
                             (geb:pair reducify
304
                                       (stlc-ctx-to-mu context)))
305
                       (comp
306
                        (so-eval (fun-to-hom (mcar tofun))
307
                                 (fun-to-hom (mcadr tofun)))
308
                        (geb:pair (rec context fun)
309
                                  reducify)))))
310
                ((index pos)
311
                 (stlc-ctx-proj context pos))
312
                ((bit-choice bitv)
313
                 (comp (nat-const 24
314
                                  bitv)
315
                       (terminal (stlc-ctx-to-mu context))))
316
                (err
317
                 (error "Not meant for the compiler"))
318
                ((or plus
319
                     minus
320
                     times
321
                     divide
322
                     lamb-eq
323
                     lamb-lt
324
                     modulo)
325
                 (let ((ltm (ltm tterm)))
326
                   (labels ((arith (op)
327
                              (comp (funcall op (num (ttype ltm)))
328
                                    (geb:pair (rec context ltm)
329
                                              (rec context (rtm tterm))))))
330
                     (arith (dispatch tterm)))))))
331
            (rec1 (ctx tterm)
332
              (if (typep tterm 'lamb)
333
                  (rec1 (append (tdom tterm) ctx)
334
                        (term tterm))
335
                  (list ctx tterm))))
336
     (if (not (well-defp context tterm))
337
         (error "not a well-defined ~A in said ~A" tterm context)
338
         (let* ((term (geb.lambda.main:reducer tterm))
339
                (recc (rec1 context term))
340
                (car (car recc)))
341
           (rec car
342
                (ann-term1 car
343
                           (cadr recc)))))))
344
 
345
 (-> stlc-ctx-to-mu (stlc-context) substobj)
346
 (defun stlc-ctx-to-mu (context)
347
   "Converts a generic [<STLC>][type] context into a
348
 [SUBSTMORPH][GEB.SPEC:SUBSTMORPH]. Note that usually contexts can be interpreted
349
 in a category as a $\Sigma$-type$, which in a non-dependent setting gives us a
350
 usual [PROD][class]
351
 
352
 ```lisp
353
 LAMBDA> (stlc-ctx-to-mu (list so1 (fun-to-hom (fun-type geb-bool:bool geb-bool:bool))))
354
 (× s-1
355
    (× (+ GEB-BOOL:FALSE GEB-BOOL:TRUE) (+ GEB-BOOL:FALSE GEB-BOOL:TRUE))
356
    s-1)
357
 ```"
358
   (mvfoldr #'prod (mapcar #'fun-to-hom context) so1))
359
 
360
 (defun stlc-ctx-maybe (context)
361
   "Takes a context seen as product of appropriate [SUBSTOBJ][GEB.SPEC:SUBSTOBJ]
362
 and iteratively applies Maybe to its elements."
363
   (mvfoldr #'prod (mapcar (lambda (x) (maybe-comp x)) context) so1))
364
 
365
 (-> so-hom (substobj substobj) (or t substobj))
366
 (defun so-hom (dom cod)
367
   "Computes the hom-object of two [SUBSTMORPH]s"
368
   (so-hom-obj dom cod))
369
 
370
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
371
 ;; Utility Functions
372
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
373
 
374
 
375
 (defun stlc-ctx-proj (context depth)
376
   "Given a context, we interpret it as a [PROD][class] object of appropriate
377
 length with fibrations given by [PROD][class] projections."
378
   (if (zerop depth)
379
       (<-left (fun-to-hom (car context))
380
               (stlc-ctx-to-mu (cdr context)))
381
       (comp (stlc-ctx-proj (cdr context) (1- depth))
382
             (<-right (fun-to-hom (car context))
383
                      (stlc-ctx-to-mu (cdr context))))))
384
 
385
 (defun prod-rem (num obj)
386
   "Given a product A0 x A1 x ... x An and a positive integer k gives a
387
 corresponding composition of morphisms projecting to Ak x ... x An"
388
   (if (= num 1)
389
       (<-right (mcar obj) (mcadr obj))
390
       (comp (<-right (mcar (apply-n (- num 1) #'mcadr obj))
391
                      (apply-n num #'mcadr obj))
392
             (prod-rem (1- num) obj))))
393
 
394
 (defun prod-proj (num obj)
395
   "Given a product A0 x ... x An and an integer k less than n gives a
396
 corresponding composition of projection morphism to Ak"
397
   (if (zerop num)
398
       (<-left (mcar obj) (mcadr obj))
399
       (let ((codm (codom (prod-rem num obj))))
400
         (comp (<-left (mcar codm) codm)
401
               (prod-rem num obj)))))
402
 
403
 (defun index-to-projection (depth typ-a typ-b prod)
404
   (if (zerop depth)
405
       (comp (<-left typ-a typ-b) prod)
406
       (comp (index-to-projection (1- depth) (mcar typ-b) (mcadr typ-b) prod)
407
             (<-right typ-a typ-b))))
408
 
409
 (-> index-to-obj (fixnum t) t)
410
 (defun index-to-obj (depth typ)
411
   (if (zerop depth)
412
       (mcar typ)
413
       (index-to-obj (1- depth) (mcadr typ))))
414
 
415
 (-> call-objmap (functor t) t)
416
 (defun call-objmap (functor-body arg)
417
   (funcall (obj functor-body) arg))
418
 
419
 (-> call-morphmap (functor t t t) t)
420
 (defun call-morphmap (functor-body typ-a typ-b arg)
421
   (funcall (func functor-body) typ-a typ-b arg))
422
 ��