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

KindCoveredAll%
expression7641211 63.1
branch5894 61.7
Key
Not instrumented
Conditionalized out
Executed
Not executed
 
Both branches taken
One branch taken
Neither branch taken
1
 (in-package #:geb.lambda.main)
2
 
3
 (defclass fun-type (geb.mixins:direct-pointwise-mixin geb.mixins:cat-obj)
4
   ((mcar :initarg :mcar
5
          :accessor mcar
6
          :documentation "")
7
    (mcadr :initarg :mcadr
8
           :accessor mcadr
9
           :documentation ""))
10
   (:documentation
11
    "Stand-in for the [SO-HOM-OBJ][GEB.COMMON:SO-HOM-OBJ] object. It does not have
12
 any computational properties and can be seen as just a function of two arguments
13
 with accessors [MCAR][generic-function] to the first argument and
14
 [MCADR][generic-function] to the second argument. There is an evident canonical
15
 way to associate [FUN-TYPE][class] and [SO-HOM-OBJ][GEB.COMMON:SO-HOM-OBJ]
16
 pointwise."))
17
 
18
 (defun fun-type (mcar mcadr)
19
   (make-instance 'fun-type :mcar mcar :mcadr mcadr))
20
 
21
 (-> index-check (fixnum list) cat-obj)
22
 (defun index-check (i ctx)
23
   "Given an natural number I and a context, checks that the context is of
24
 length at least I and then produces the Ith entry of the context counted
25
 from the left starting with 0."
26
   (let ((l (length ctx)))
27
     (if (< i l)
28
         (nth i ctx)
29
         (error "Argument exceeds length of context"))))
30
 
31
 ;; Types all terms inside a given lambda term with respect to a context
32
 ;; with the caveat of producing a stand-in of the exponential object
33
 
34
 ;; We assume that the compiler receives all the info using the exp-aux
35
 ;; class instead of the usual hom-obj for the well-defp predicate
36
 
37
 
38
 (defgeneric ann-term1 (ctx tterm)
39
   (:documentation
40
    "Given a list of [SUBSTOBJ][GEB.SPEC:SUBSTOBJ] objects with
41
 [SO-HOM-OBJ][GEB.COMMON:SO-HOM-OBJ] occurences replaced by [FUN-TYPE][class]
42
 and an [STLC][type] similarly replacing type occurences of the hom object
43
 to [FUN-TYPE][class], provides the [TTYPE][generic-function] accessor to all
44
 subterms as well as the term itself, using [FUN-TYPE][class]. Once again,
45
 note  that it is important for the context and term to be giving as
46
 per above description. While not always, not doing so result in an error upon
47
 evaluation. As an example of a valid entry we have
48
 
49
 ```lisp
50
  (ann-term1 (list so1 (fun-type so1 so1)) (app (index 1) (list (index 0))))
51
 ```
52
 
53
 while
54
 
55
 ```lisp
56
 (ann-term1 (list so1 (so-hom-obj so1 so1)) (app (index 1) (list (index 0))))
57
 ```
58
 
59
 produces an error trying to use. This warning applies to other
60
 functions taking in context and terms below as well.
61
 
62
 Moreover, note that for terms whose typing needs addition of new context
63
 we append contexts on the left rather than on the right contra usual type
64
 theoretic notation for the convenience of computation. That means, e.g. that
65
 asking for a type of a lambda term as below produces:
66
 
67
 ```lisp
68
 LAMBDA> (ttype (term (ann-term1 (lambda (list so1 so0) (index 0)))))
69
 s-1
70
 ```
71
 
72
 as we count indeces from the left of the context while appending new types to
73
 the context on the left as well. For more info check [LAMB][class]"))
74
 
75
 
76
 (defmethod ann-term1 (ctx (tterm <stlc>))
77
   ;; cahce check
78
   (if (ttype tterm)
79
       tterm
80
       (match-of stlc tterm
81
         ((absurd tcod term) (absurd tcod (ann-term1 ctx term) :ttype tcod))
82
         (unit               (unit :ttype so1))
83
         ((left rty term)    (let ((lant (ann-term1 ctx term)))
84
                               (left rty
85
                                     lant
86
                                     :ttype (coprod (ttype lant) rty))))
87
         ((right lty term)   (let ((rant (ann-term1 ctx term)))
88
                               (right lty
89
                                      rant
90
                                      :ttype (coprod lty (ttype rant)))))
91
         ((pair ltm rtm)     (let ((lant (ann-term1 ctx ltm))
92
                                   (rant (ann-term1 ctx rtm)))
93
                               (pair lant
94
                                     rant
95
                                     :ttype (prod (ttype lant) (ttype rant)))))
96
         ((fst term)         (let* ((ann-term     (ann-term1 ctx term))
97
                                    (type-of-term (ttype (ann-term1 ctx term))))
98
                               (if (typep type-of-term 'prod)
99
                                   (fst ann-term
100
                                        :ttype (mcar type-of-term))
101
                                   (error "type of term not of product type"))))
102
         ((snd term)          (let* ((ann-term     (ann-term1 ctx term))
103
                                     (type-of-term (ttype ann-term)))
104
                                (if (typep type-of-term 'prod)
105
                                    (snd ann-term :ttype (mcadr type-of-term))
106
                                    (error "type of term not of product type"))))
107
         ((lamb tdom term)   (let ((ant (ann-term1 (append tdom ctx) term)))
108
                               (lamb tdom
109
                                     ant
110
                                     :ttype (fun-type (reduce #'prod tdom
111
                                                              :from-end t)
112
                                                      (ttype ant)))))
113
         ((app fun term) (let ((anfun (ann-term1 ctx fun)))
114
                           (app anfun
115
                                (mapcar (lambda (trm) (ann-term1 ctx trm)) term)
116
                                :ttype (mcadr (ttype anfun)))))
117
         ((index pos)        (index pos
118
                                    :ttype (index-check pos ctx)))
119
         ((err ttype)        (err ttype))
120
         ((plus ltm rtm)        (let ((ant (ann-term1 ctx ltm)))
121
                                  (plus ant
122
                                        (ann-term1 ctx rtm)
123
                                        :ttype (ttype ant))))
124
         ((times ltm rtm)        (let ((ant (ann-term1 ctx ltm)))
125
                                   (times ant
126
                                          (ann-term1 ctx rtm)
127
                                          :ttype (nat-width 24))))
128
         ((minus ltm rtm)        (let ((ant (ann-term1 ctx ltm)))
129
                                   (minus ant
130
                                          (ann-term1 ctx rtm)
131
                                          :ttype (nat-width 24))))
132
         ((divide ltm rtm)        (let ((ant (ann-term1 ctx ltm)))
133
                                    (divide ant
134
                                            (ann-term1 ctx rtm)
135
                                            :ttype (nat-width 24))))
136
         ((bit-choice bitv)       (bit-choice bitv
137
                                              :ttype (nat-width 24)))
138
         ((lamb-eq ltm rtm)         (lamb-eq (ann-term1 ctx ltm)
139
                                             (ann-term1 ctx rtm)
140
                                             :ttype (coprod so1 so1)))
141
         ((lamb-lt ltm rtm)         (lamb-lt (ann-term1 ctx ltm)
142
                                             (ann-term1 ctx rtm)
143
                                             :ttype (coprod so1 so1)))
144
         ((modulo ltm rtm)          (let ((ant (ann-term1 ctx ltm)))
145
                                      (modulo ant
146
                                              (ann-term1 ctx rtm)
147
                                              :ttype (ttype ant))))
148
         ((case-on on ltm rtm)
149
          (let* ((ann-on     (ann-term1 ctx on))
150
                 (type-of-on (ttype ann-on))
151
                 (ann-left   (ann-term1 (cons  (mcar type-of-on) ctx) ltm))
152
                 (ann-right  (ann-term1 (cons (mcadr type-of-on) ctx) rtm)))
153
            (if (typep type-of-on 'coprod)
154
                (case-on ann-on ann-left ann-right :ttype (ttype ann-left))
155
                (error "type of on not of coproduct type")))))))
156
 
157
 ;; Changes the stand in Geb term with exponential stand-ins
158
 ;; to one containing actual hom-objects
159
 (defun fun-to-hom (t1)
160
   "Given a [SUBSTOBJ][GEB.SPEC:SUBSTOBJ] whose subobjects might have a
161
 [FUN-TYPE][class] occurence replaces all occurences of [FUN-TYPE][class] with a
162
 suitable [SO-HOM-OBJ][GEB.COMMON:SO-HOM-OBJ], hence giving a pure
163
 [SUBSTOBJ][GEB.SPEC:SUBSTOBJ]
164
 
165
 ```lisp
166
 LAMBDA> (fun-to-hom (fun-type geb-bool:bool geb-bool:bool))
167
 (× (+ GEB-BOOL:FALSE GEB-BOOL:TRUE) (+ GEB-BOOL:FALSE GEB-BOOL:TRUE))
168
 ```"
169
   (cond ((typep t1 'prod)     (prod (fun-to-hom (mcar t1))
170
                                     (fun-to-hom (mcadr t1))))
171
         ((typep t1 'coprod)   (coprod (fun-to-hom (mcar t1))
172
                                       (fun-to-hom (mcadr t1))))
173
         ((typep t1 'fun-type) (so-hom-obj (fun-to-hom (mcar t1))
174
                                           (fun-to-hom (mcadr t1))))
175
         (t                    t1)))
176
 
177
 ;; Changes all annotated terms' types to actual Geb objects
178
 
179
 (defun ann-term2 (tterm)
180
   "Given an [STLC][type] term with a [TTYPE][generic-function] accessor from
181
 [ANN-TERM1][generic-function] - i.e. including possible [FUN-TYPE][class]
182
 occurences - re-annotates the term and its subterms with actual
183
 [SUBSTOBJ][GEB.SPEC:SUBSTOBJ] objects."
184
   (match-of stlc tterm
185
     ((absurd tcod term)    (absurd (fun-to-hom tcod)
186
                                    (ann-term2 term)
187
                                    :ttype (fun-to-hom (ttype tterm))))
188
     (unit                   tterm)
189
     ((right lty term)       (right (fun-to-hom lty)
190
                                    (ann-term2 term)
191
                                    :ttype (fun-to-hom (ttype tterm))))
192
     ((left rty term)        (left (fun-to-hom rty)
193
                                   (ann-term2 term)
194
                                   :ttype (fun-to-hom (ttype tterm))))
195
     ((case-on on ltm rtm)  (case-on (ann-term2 on)
196
                                     (ann-term2 ltm)
197
                                     (ann-term2 rtm)
198
                                     :ttype (fun-to-hom (ttype tterm))))
199
     ((pair ltm rtm)        (pair (ann-term2 ltm)
200
                                  (ann-term2 rtm)
201
                                  :ttype (fun-to-hom (ttype tterm))))
202
     ((fst term)            (fst (ann-term2 term)
203
                                 :ttype (fun-to-hom (ttype tterm))))
204
     ((snd term)            (snd (ann-term2 term)
205
                                 :ttype (fun-to-hom (ttype tterm))))
206
     ((lamb tdom term)      (lamb (mapcar #'fun-to-hom tdom)
207
                                  (ann-term2 term)
208
                                  :ttype (fun-to-hom (ttype tterm))))
209
     ((app fun term)        (app (ann-term2 fun)
210
                                 (mapcar #'ann-term2 term)
211
                                 :ttype (fun-to-hom (ttype tterm))))
212
     ((index pos)           (index pos
213
                                   :ttype (fun-to-hom (ttype tterm))))
214
     ((err ttype)           (err (fun-to-hom ttype)))
215
     ((or plus
216
          times
217
          minus
218
          divide
219
          modulo
220
          bit-choice
221
          lamb-eq
222
          lamb-lt)
223
      tterm)))
224
 
225
 (defun annotated-term (ctx term)
226
   "Given a context consisting of a list of [SUBSTOBJ][GEB.SPEC:SUBSTOBJ]
227
 with occurences of [SO-HOM-OBJ][GEB.COMMON:SO-HOM-OBJ] replaced by
228
 [FUN-TYPE][class] and an [STLC][type] term with similarly replaced occurences
229
 of [SO-HOM-OBJ][GEB.COMMON:SO-HOM-OBJ], provides an [STLC][type] with all
230
 subterms typed, i.e. providing the [TTYPE][generic-function] accessor,
231
 which is a pure [SUBSTOBJ][GEB.SPEC:SUBSTOBJ]"
232
   (ann-term2 (ann-term1 ctx term)))
233
 
234
 
235
 ;; Produces a type of a lambda term in a context
236
 ;; with a stand-in for the exponential object
237
 
238
 (defun type-of-term-w-fun (ctx tterm)
239
   "Given a context consisting of a list of [SUBSTOBJ][GEB.SPEC:SUBSTOBJ] with
240
 occurences of [SO-HOM-OBJ][GEB.COMMON:SO-HOM-OBJ] replaced by [FUN-TYPE][class]
241
 and an [STLC][type] term with similarly replaced occurences of
242
 [SO-HOM-OBJ][GEB.COMMON:SO-HOM-OBJ], gives out a type of the whole term with
243
 occurences of [SO-HOM-OBJ][GEB.COMMON:SO-HOM-OBJ] replaced by [FUN-TYPE][class]."
244
   (ttype (ann-term1 ctx tterm)))
245
 
246
 ;; Actual type info
247
 
248
 (defun type-of-term (ctx tterm)
249
   "Given a context consisting of a list of [SUBSTOBJ][GEB.SPEC:SUBSTOBJ] with
250
 occurences of [SO-HOM-OBJ][GEB.COMMON:SO-HOM-OBJ] replaced by [FUN-TYPE][class]
251
 and an [STLC][type] term with similarly replaced occurences of
252
 [SO-HOM-OBJ][GEB.COMMON:SO-HOM-OBJ], provides the type of the whole term,
253
 which is a pure [SUBSTOBJ][type]."
254
   (fun-to-hom (type-of-term-w-fun ctx tterm)))
255
 
256
 ;;Predicate checking that a term in a given context is well-typed
257
 
258
 (defgeneric well-defp (ctx tterm)
259
   (:documentation
260
    "Given a context consisting of a list of [SUBSTOBJ][GEB.SPEC:SUBSTOBJ]
261
 with occurences of [SO-HOM-OBJ][GEB.COMMON:SO-HOM-OBJ] replaced by
262
 [FUN-TYPE][class] and an [STLC][type] term with similarly replaced
263
 occurences of [SO-HOM-OBJ][GEB.COMMON:SO-HOM-OBJ], checks that the term
264
 is well-defined in the context based on structural rules of simply
265
 typed lambda calculus. returns the t if it is, otherwise returning
266
 nil"))
267
 
268
 (defmethod well-defp (ctx (tterm <stlc>))
269
   (labels ((check (tterm)
270
              (match-of stlc tterm
271
                ((absurd)
272
                 (and (check (term tterm))
273
                      (obj-equalp (ttype (term tterm)) so0)))
274
                ((left term)
275
                 (and (check term)
276
                      (obj-equalp (mcar (ttype tterm)) (ttype term))))
277
                ((right term)
278
                 (and (check term)
279
                      (obj-equalp (mcadr (ttype tterm)) (ttype term))))
280
                ((pair ltm rtm)
281
                 (and (check ltm)
282
                      (check rtm)))
283
                ((fst term)
284
                 (and (check term)
285
                      (obj-equalp (ttype tterm) (mcar (ttype term)))))
286
                ((snd term)
287
                 (and (check term)
288
                      (obj-equalp (ttype tterm) (mcadr (ttype term)))))
289
                ((case-on on ltm rtm)
290
                 (and (check ltm)
291
                      (check rtm)
292
                      (check on)
293
                      (obj-equalp (ttype ltm) (ttype rtm))))
294
                ((lamb tdom term)
295
                 (let ((lambda-type (ttype tterm)))
296
                   (and (check term)
297
                        (obj-equalp (mcar lambda-type) (reduce #'prod tdom))
298
                        (obj-equalp (mcadr lambda-type) (ttype term)))))
299
                ((app fun term)
300
                 (and (check fun)
301
                      (check (reduce #'pair term :from-end t))
302
                      (typep (ttype fun) 'fun-type)
303
                      (obj-equalp (ttype fun)
304
                                  (fun-type (reduce #'prod
305
                                                    (mapcar #'ttype term)
306
                                                    :from-end t)
307
                                            (ttype tterm)))))
308
                ((or plus
309
                     minus
310
                     times
311
                     divide
312
                     modulo)
313
                 (obj-equalp (ttype (ltm tterm))
314
                             (ttype (rtm tterm))))
315
                ((or lamb-eq
316
                     lamb-lt)
317
                 t)
318
                (index t)
319
                (unit t)
320
                (err t)
321
                (bit-choice t))))
322
     (let ((term (ignore-errors
323
                  (ann-term1 ctx tterm))))
324
       (and term (check term)))))
325
 
326
 (defun errorp (tterm)
327
   "Evaluates to true iff the term has an error subterm."
328
   (cond ((or (typep tterm 'index)
329
              (typep tterm 'unit)
330
              (typep tterm 'bit-choice))
331
          nil)
332
         ((typep tterm 'err)       t)
333
         ((typep tterm 'case-on)   (or (errorp (on tterm))
334
                                       (errorp (rtm tterm))
335
                                       (errorp (ltm tterm))))
336
         ((typep tterm 'pair)      (or (errorp (ltm tterm))
337
                                       (errorp (rtm tterm))))
338
         ((typep tterm 'app)       (or (errorp (fun tterm))
339
                                       (some #'identity
340
                                             (mapcar
341
                                              (lambda (x) (errorp x))
342
                                              (term tterm)))))
343
         ((or (typep tterm 'plus)
344
              (typep tterm 'minus)
345
              (typep tterm 'times)
346
              (typep tterm 'divide)
347
              (typep tterm 'lamb-eq)
348
              (typep tterm 'lamb-lt)
349
              (typep tterm 'modulo))
350
          (or (errorp (ltm tterm))
351
              (errorp (rtm tterm))))
352
         (t                        (errorp (term tterm)))))
353
 
354
 (defun dispatch (tterm)
355
   "A dispatch refering the class of a term to its function"
356
   (typecase tterm
357
     (absurd #'absurd)
358
     (unit   #'unit)
359
     (left   #'left)
360
     (right   #'right)
361
     (case-on #'case-on)
362
     (fst #'fst)
363
     (snd #'snd)
364
     (pair #'pair)
365
     (lamb #'lamb)
366
     (app #'app)
367
     (index #'index)
368
     (err #'err)
369
     (bit-choice #'bit-choice)
370
     (plus #'plus)
371
     (minus #'minus)
372
     (divide #'divide)
373
     (times #'times)
374
     (lamb-eq #'lamb-eq)
375
     (lamb-lt #'lamb-lt)
376
     (modulo  #'modulo)))
377
 
378
 (defun dispatch-arith (tterm)
379
   "A dispatch refering the class of an arithmetic term
380
 to its corresponding operation"
381
   (typecase tterm
382
     (plus #'+)
383
     (minus #'-)
384
     (divide #'floor)
385
     (times #'*)
386
     (lamb-eq #'=)
387
     (lamb-lt #'<)
388
     (modulo #'mod)))
389
 
390
 (defun index-excess (tterm)
391
   "Checks all indeces occuring in a term which will be substituted.
392
 If position exceeds n, adds depth to the index. Necessary for
393
 beta-substitution of indices which point outside of the app term"
394
   (labels ((rec (n tterm)
395
              (typecase tterm
396
                (absurd    (absurd (tcod tterm)
397
                                   (rec n (term tterm))))
398
                (left      (left (rty tterm)
399
                                 (rec n (term tterm))))
400
                (right     (right (lty tterm)
401
                                  (rec n (term tterm))))
402
                (case-on   (case-on (rec n (on tterm))
403
                                    (rec (1+ n) (ltm tterm))
404
                                    (rec (1+ n) (rtm tterm))))
405
                (fst       (fst (rec n (term tterm))))
406
                (snd       (snd (rec n (term tterm))))
407
                (lamb      (lamb (tdom tterm)
408
                                 (rec (1+ n) (term tterm))))
409
                (app       (app (rec n (fun tterm))
410
                                (list (rec n (car (term tterm))))))
411
                (index     (if (>= (pos tterm) n)
412
                               (index (1+ (pos tterm)))
413
                               tterm))
414
                ((or unit
415
                     err
416
                     bit-choice)
417
                 tterm)
418
                ((or plus
419
                     times
420
                     minus
421
                     divide
422
                     lamb-eq
423
                     lamb-lt
424
                     pair
425
                     modulo)
426
                 (funcall (dispatch tterm)
427
                          (rec n (ltm tterm))
428
                          (rec n (rtm tterm)))))))
429
     (rec 0 tterm)))
430
 
431
 (defun index-lack (n tterm)
432
   "Checks if a term has made substitutions and decreases the index
433
 of term accordingly"
434
   (labels ((rec (n tterm)
435
              (if (typep tterm 'list)
436
                  tterm
437
                  (typecase tterm
438
                    (absurd    (absurd (tcod tterm)
439
                                       (rec n (term tterm))))
440
                    (left      (left (rty tterm)
441
                                     (rec n (term tterm))))
442
                    (right     (right (lty tterm)
443
                                      (rec n (term tterm))))
444
                    (case-on   (case-on (rec n (on tterm))
445
                                        (rec (1+ n) (ltm tterm))
446
                                        (rec (1+ n) (rtm tterm))))
447
                    (fst       (fst (rec n (term tterm))))
448
                    (snd       (snd (rec n (term tterm))))
449
                    (lamb      (lamb (tdom tterm)
450
                                     (rec (1+ n) (term tterm))))
451
                    (app      (app (rec n (fun tterm))
452
                                   (list (rec n (car (term tterm))))))
453
                    (index     (if (> (pos tterm) n)
454
                                   (index (1- (pos tterm)))
455
                                   tterm))
456
                    ((or unit
457
                         err
458
                         bit-choice)
459
                     tterm)
460
                    ((or plus
461
                         times
462
                         minus
463
                         divide
464
                         lamb-eq
465
                         lamb-lt
466
                         pair
467
                         modulo)
468
                     (funcall (dispatch tterm)
469
                              (rec n (ltm tterm))
470
                              (rec n (rtm tterm))))))))
471
     (rec n tterm)))
472
 
473
 (defun delist (tterm)
474
   "We mark substituted terms by listing them. This function recovers the car
475
 of the list."
476
   (if (typep tterm 'list)
477
       (car tterm)
478
       (typecase tterm
479
         (absurd  (absurd (tcod tterm)
480
                          (delist (term tterm))))
481
         (left    (left (rty tterm)
482
                        (delist (term tterm))))
483
         (right   (right (lty tterm)
484
                         (delist (term tterm))))
485
         (case-on (case-on (delist (on tterm))
486
                           (delist (ltm tterm))
487
                           (delist (rtm tterm))))
488
         (fst     (fst (delist (term tterm))))
489
         (snd     (snd (delist (term tterm))))
490
         (lamb    (lamb (tdom tterm)
491
                        (delist (term tterm))))
492
         (app     (app (delist (fun tterm))
493
                       (list (delist (car (term tterm))))))
494
         ((or unit
495
              err
496
              index
497
              bit-choice)
498
          tterm)
499
         ((or plus
500
              times
501
              minus
502
              divide
503
              lamb-eq
504
              lamb-lt
505
              pair
506
              modulo)
507
          (funcall (dispatch tterm)
508
                   (delist (ltm tterm))
509
                   (delist (rtm tterm)))))))
510
 
511
 (defun sub (ind term-to-replace sub-in)
512
   "Substitutes the occurence of index (ind) inside of the top
513
 subterms of sub-on by term-to-replace. We mark replaced terms by
514
 listing them"
515
   (typecase sub-in
516
     (absurd   (absurd (tcod sub-in) (sub ind
517
                                          term-to-replace
518
                                          (term sub-in))))
519
     (left     (left (rty sub-in) (sub ind
520
                                       term-to-replace
521
                                       (term sub-in))))
522
     (right     (right (lty sub-in) (sub ind
523
                                         term-to-replace
524
                                         (term sub-in))))
525
     (case-on   (case-on (sub ind
526
                              term-to-replace
527
                              (on sub-in))
528
                         (sub (1+ ind)
529
                              (index-excess term-to-replace)
530
                              (ltm sub-in))
531
                         (sub (1+ ind)
532
                              (index-excess term-to-replace)
533
                              (rtm sub-in))))
534
     (fst        (fst (substitute ind
535
                                  term-to-replace
536
                                  (term sub-in))))
537
     (snd        (snd (substitute ind
538
                                  term-to-replace
539
                                  (term sub-in))))
540
     (lamb      (lamb (tdom sub-in)
541
                      (sub (1+ ind)
542
                           (index-excess term-to-replace)
543
                           (term sub-in))))
544
     (app        (app (sub ind term-to-replace (fun sub-in))
545
                      (list (sub ind term-to-replace (car (term sub-in))))))
546
     (index      (if (= (pos sub-in) ind)
547
                     (list term-to-replace)
548
                     sub-in))
549
     ((or unit
550
          err
551
          bit-choice)
552
      sub-in)
553
     ((or plus
554
          times
555
          minus
556
          divide
557
          lamb-eq
558
          lamb-lt
559
          pair
560
          modulo)
561
      (funcall (dispatch sub-in)
562
               (sub ind term-to-replace (ltm sub-in))
563
               (sub ind term-to-replace (rtm sub-in))))))
564
 
565
 (defun reducer (tterm)
566
   "Reduces a given Lambda term by applying explict beta-reduction
567
 when possible alongside arithmetic simplification. We assume that the
568
 lambda and app terms are  1-argument"
569
   (typecase tterm
570
     (absurd   (absurd (tcod tterm) (reducer (term tterm))))
571
     (left     (left (rty tterm) (reducer (term tterm))))
572
     (right    (right (lty tterm) (reducer (term tterm))))
573
     (case-on  (let ((on (on tterm))
574
                     (ltm (ltm tterm))
575
                     (rtm (rtm tterm)))
576
                 (cond ((typep on 'left)  (substitute-zero on ltm))
577
                       ((typep on 'right) (substitute-zero on rtm))
578
                       (t                 (case-on (reducer on)
579
                                                   (reducer ltm)
580
                                                   (reducer rtm))))))
581
     (pair     (pair (reducer (ltm tterm))
582
                     (reducer (rtm tterm))))
583
     (fst      (let ((term (term tterm)))
584
                 (if (typep (reducer term) 'pair)
585
                     (reducer (ltm term))
586
                     (fst (reducer term)))))
587
     (snd      (let ((term (term tterm)))
588
                 (if (typep (reducer term) 'pair)
589
                     (reducer (rtm term))
590
                     (snd (reducer term)))))
591
     (lamb     (lamb (tdom tterm) (reducer (term tterm))))
592
     (app
593
      (let ((fun (fun tterm))
594
            (term (car (term tterm))))
595
        (cond ((typep fun 'lamb)
596
               (substitute-zero (reducer term) (reducer (term fun))))
597
              ((and (typep fun 'case-on)
598
                    (typep (ltm fun) 'lamb)
599
                    (typep (rtm fun) 'lamb))
600
               (let ((irec (index-excess (reducer term))))
601
                 (flet ((zero-index (term)
602
                          (substitute-zero irec (reducer (term term)))))
603
                   (reducer (case-on (reducer (on fun))
604
                                     (zero-index (ltm fun))
605
                                     (zero-index (rtm fun)))))))
606
              ((and (typep fun 'case-on)
607
                    (typep (ltm fun) 'lamb)
608
                    (typep (rtm fun) 'case-on))
609
               (reducer (case-on (reducer (on fun))
610
                                 (substitute-zero (index-excess (reducer term))
611
                                                  (reducer (term (ltm fun))))
612
                                 (reducer (app (rtm fun)
613
                                               (list (index-excess term)))))))
614
              ((and (typep fun 'case-on)
615
                    (typep (ltm fun) 'lamb)
616
                    (typep (rtm fun) 'case-on))
617
               (reducer (case-on (reducer (on fun))
618
                                 (reducer (app (ltm fun)
619
                                               (list (index-excess term))))
620
                                 (substitute-zero (index-excess (reducer term))
621
                                                  (reducer (term (rtm fun)))))))
622
              ((typep fun 'err)
623
               (err (mcadr (ttype fun))))
624
              (t (app (reducer fun) (list (reducer term)))))))
625
     ((or lamb-eq
626
          lamb-lt)
627
      (let ((ltm (ltm tterm))
628
            (rtm (rtm tterm)))
629
        (if (and (typep ltm 'bit-choice)
630
                 (typep rtm 'bit-choice))
631
            (if (funcall (dispatch-arith tterm)
632
                         (bitv ltm)
633
                         (bitv rtm))
634
                (left so1 (unit))
635
                (right so1 (unit)))
636
            (funcall (dispatch tterm)
637
                     (reducer ltm)
638
                     (reducer rtm)))))
639
     ((or plus
640
          times
641
          minus
642
          divide
643
          modulo)
644
      (let ((ltm (ltm tterm))
645
            (rtm (rtm tterm)))
646
        (if (and (typep ltm 'bit-choice)
647
                 (typep rtm 'bit-choice))
648
            (bit-choice
649
             (funcall (dispatch-arith tterm)
650
                      (bitv ltm)
651
                      (bitv rtm)))
652
            (funcall (dispatch tterm)
653
                     (reducer ltm)
654
                     (reducer rtm)))))
655
     ((or unit
656
          index
657
          err
658
          bit-choice)
659
      tterm)))
660
 
661
 (defun substitute-zero (replaced-term replacing-term)
662
   "Substitutes the zero'th index, and properly marks it"
663
   (delist (index-lack 0 (sub 0 replaced-term replacing-term))))
664
 �