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

KindCoveredAll%
expression51115 44.3
branch00nil
Key
Not instrumented
Conditionalized out
Executed
Not executed
 
Both branches taken
One branch taken
Neither branch taken
1
 (in-package #:geb.lambda.spec)
2
 
3
 (defclass <stlc> (geb.mixins:direct-pointwise-mixin geb.mixins:meta-mixin geb.mixins:cat-obj) ()
4
   (:documentation
5
    "Class of untyped terms of simply typed lambda claculus. Given our
6
 presentation, we look at the latter as a type theory spanned by empty,
7
 unit types as well as coproduct, product, and function types."))
8
 
9
 (deftype stlc ()
10
   "Type of untyped terms of [STLC][type]. Each class of a term has a slot for a type,
11
 which can be filled by auxillary functions or by user. Types are
12
 represented as [SUBSTOBJ][GEB.SPEC:SUBSTOBJ]."
13
   '(or absurd unit left right case-on pair fst snd lamb app index err
14
     plus times minus divide bit-choice lamb-eq lamb-lt modulo))
15
 
16
 ;; New defgenerics
17
 
18
 (defgeneric term (obj))
19
 (defgeneric tdom (obj))
20
 (defgeneric tcod (obj))
21
 (defgeneric ttype (obj))
22
 (defgeneric rty (obj))
23
 (defgeneric lty (obj))
24
 (defgeneric ltm (obj))
25
 (defgeneric rtm (obj))
26
 (defgeneric on (obj))
27
 (defgeneric fun (obj))
28
 (defgeneric pos (obj))
29
 (defgeneric bitv (obj))
30
 
31
 
32
 (defclass absurd (<stlc>)
33
   ((tcod :initarg :tcod
34
          :accessor tcod
35
          :documentation "An arbitrary type")
36
    (term :initarg :term
37
          :accessor term
38
          :documentation "A term of the empty type")
39
    (ttype :initarg :ttype
40
           :initform nil
41
           :accessor ttype
42
           :documentation ""))
43
   (:documentation
44
    "The [ABSURD][class] term provides an element of an arbitrary type
45
 given a term of the empty type, denoted by [SO0][GEB.SPEC:SO0 class].
46
 The formal grammar of [ABSURD][class] is
47
 
48
 ```lisp
49
 (absurd tcod term)
50
 ```
51
 
52
 where we possibly can include type information by
53
 
54
 ```lisp
55
 (absurd tcod term :ttype ttype)
56
 ```
57
 
58
 The intended semantics are: [TCOD] is a type whose term we want to
59
 get (and hence a [SUBSTOBJ] [GEB.SPEC:SUBSTOBJ]) and [TERM] is a term
60
 of the empty type (and hence an [STLC][type].
61
 
62
 This corresponds to the elimination rule of the empty type. Namely,
63
 given
64
 $$\\Gamma \\vdash \\text{tcod : Type}$$ and
65
 $$\\Gamma \\vdash \\text{term : so0}$$ one deduces
66
 $$\\Gamma \\vdash \\text{(absurd tcod term) : tcod}$$"))
67
 
68
 (defun absurd (tcod term &key (ttype nil))
69
   (values
70
    (make-instance 'absurd :tcod tcod :term term :ttype ttype)))
71
 
72
 (defclass unit (<stlc>)
73
   ((ttype :initarg :ttype
74
           :initform nil
75
           :accessor ttype
76
           :documentation ""))
77
   (:documentation
78
    "The unique term of the unit type, the latter represented by
79
 [SO1][GEB.SPEC:SO1 class]. The formal grammar of [UNIT][class] is
80
 
81
 ```lisp
82
 (unit)
83
 ```
84
 
85
 where we can optionally include type information by
86
 
87
 ```lisp
88
 (unit :ttype ttype)
89
 ```
90
 
91
 Clearly the type of [UNIT][class] is [SO1][GEB.SPEC:SO1 class] but here
92
 we provide all terms untyped.
93
 
94
 This grammar corresponds to the introduction rule of the unit type. Namely
95
 $$\\Gamma \\dashv \\text{(unit) : so1}$$"))
96
 
97
 (defun unit (&key (ttype nil))
98
   (values
99
    (make-instance 'unit :ttype ttype)))
100
 
101
 (defclass left (<stlc>)
102
   ((rty :initarg :rty
103
         :accessor rty
104
         :documentation "Right argument of coproduct type")
105
    (term :initarg :term
106
          :accessor term
107
          :documentation "Term of the left argument of coproduct type")
108
    (ttype :initarg :ttype
109
           :initform nil
110
           :accessor ttype
111
           :documentation ""))
112
   (:documentation
113
    "Term of a coproduct type gotten by injecting into the left type of the coproduct. The formal grammar of
114
 [LEFT][class] is
115
 
116
 ```lisp
117
 (left rty term)
118
 ```
119
 
120
 where we can include optional type information by
121
 
122
 ```lisp
123
 (left rty term :ttype ttype)
124
 ```
125
 
126
 The indended semantics are as follows: [RTY][generic-function] should
127
 be a type (and hence a [SUBSTOBJ][GEB.SPEC:SUBSTOBJ]) and specify the
128
 right part of the coproduct of the type [TTYPE][generic-function] of
129
 the entire term. The term (and hence an [STLC][type]) we are injecting
130
 is [TERM][generic-function].
131
 
132
 This corresponds to the introduction rule of the coproduct type. Namely, given
133
 $$\\Gamma \\dashv \\text{(ttype term) : Type}$$ and
134
 $$\\Gamma \\dashv \\text{rty : Type}$$
135
 with
136
 $$\\Gamma \\dashv \\text{term : (ttype term)}$$ we deduce
137
 $$\\Gamma \\dashv \\text{(left rty term) : (coprod (ttype term) rty)}$$
138
 "))
139
 
140
 (defun left (rty term &key (ttype nil))
141
   (values
142
    (make-instance 'left :rty rty :term term :ttype ttype)))
143
 
144
 (defclass right (<stlc>)
145
   ((lty :initarg :lty
146
         :accessor lty
147
         :documentation "Left argument of coproduct type")
148
    (term :initarg :term
149
          :accessor term
150
          :documentation "Term of the right argument of coproduct type")
151
    (ttype :initarg :ttype
152
           :initform nil
153
           :accessor ttype
154
           :documentation ""))
155
   (:documentation
156
    "Term of a coproduct type gotten by injecting into the right type of
157
 the coproduct. The formal grammar of [RIGHT][class] is
158
 
159
 ```lisp
160
 (right lty term)
161
 ```
162
 
163
 where we can include optional type information by
164
 
165
 ```lisp
166
 (right lty term :ttype ttype)
167
 ```
168
 
169
 The indended semantics are as follows: [LTY] should be a type (and
170
 hence a [SUBSTOBJ][GEB.SPEC:SUBSTOBJ]) and specify the left part of
171
 the coproduct of the type [TTYPE] of the entire term. The term (and
172
 hence an [STLC][type]) we are injecting is [TERM].
173
 
174
 This corresponds to the introduction rule of the coproduct type. Namely, given
175
 $$\\Gamma \\dashv \\text{(ttype term) : Type}$$ and
176
 $$\\Gamma \\dashv \\text{lty : Type}$$
177
 with
178
 $$\\Gamma \\dashv \\text{term : (ttype term)}$$ we deduce
179
 $$\\Gamma \\dashv \\text{(right lty term) : (coprod lty (ttype term))}$$
180
 "))
181
 
182
 (defun right (lty term &key (ttype nil))
183
   (values
184
    (make-instance 'right :lty lty :term term :ttype ttype)))
185
 
186
 (defclass case-on (<stlc>)
187
   ((on :initarg :on
188
        :accessor on
189
        :documentation "Term of coproduct type")
190
    (ltm :initarg :ltm
191
         :accessor ltm
192
         :documentation "Term in context of left argument of coproduct type")
193
    (rtm :initarg :rtm
194
         :accessor rtm
195
         :documentation "Term in context of right argument of coproduct type")
196
    (ttype :initarg :ttype
197
           :initform nil
198
           :accessor ttype
199
           :documentation ""))
200
   (:documentation
201
    "A term of an arbutrary type provided by casing on a coproduct term. The
202
 formal grammar of [CASE-ON][class] is
203
 
204
 ```lisp
205
 (case-on on ltm rtm)
206
 ```
207
 
208
 where we can possibly include type information by
209
 
210
 ```lisp
211
 (case-on on ltm rtm :ttype ttype)
212
 ```
213
 
214
 The intended semantics are as follows: [ON] is a term (and hence an
215
 [STLC][type]) of a coproduct type, and [LTM] and [RTM] terms (hence
216
 also [STLC][type]) of the same type in the context of - appropriately
217
 - (mcar (ttype on)) and (mcadr (ttype on)).
218
 
219
 This corresponds to the elimination rule of the coprodut type. Namely, given
220
 $$\\Gamma \\vdash \\text{on : (coprod (mcar (ttype on)) (mcadr (ttype on)))}$$
221
 and
222
 $$\\text{(mcar (ttype on))} , \\Gamma \\vdash \\text{ltm : (ttype ltm)}$$
223
 , $$\\text{(mcadr (ttype on))} , \\Gamma \\vdash \\text{rtm : (ttype ltm)}$$
224
 we get
225
 $$\\Gamma \\vdash \\text{(case-on on ltm rtm) : (ttype ltm)}$$
226
 Note that in practice we append contexts on the left as computation of
227
 [INDEX][class] is done from the left. Otherwise, the rules are the same as in
228
 usual type theory if context was read from right to left."))
229
 
230
 (defun case-on (on ltm rtm &key (ttype nil))
231
   (values
232
    (make-instance 'case-on :on on :ltm ltm :rtm rtm :ttype ttype)))
233
 
234
 (defclass pair (<stlc>)
235
   ((ltm :initarg :ltm
236
         :accessor ltm
237
         :documentation "Term of left argument of the product type")
238
    (rtm :initarg :rtm
239
         :accessor rtm
240
         :documentation "Term of right argument of the product type")
241
    (ttype :initarg :ttype
242
           :initform nil
243
           :accessor ttype
244
           :documentation ""))
245
   (:documentation
246
    "A term of the product type gotten by pairing a terms of a left and right
247
 parts of the product. The formal grammar of [PAIR][class] is
248
 
249
 ```lisp
250
 (pair ltm rtm)
251
 ```
252
 
253
 where we can possibly include type information by
254
 
255
 ```lisp
256
 (pair ltm rtm :ttype ttype)
257
 ```
258
 
259
 The intended semantics are as follows: [LTM] is a term (and hence an
260
 [STLC][type]) of a left part of the product type whose terms we are
261
 producing. [RTM] is a term (hence also [STLC][type])of the right part
262
 of the product.
263
 
264
 The grammar corresponds to the introdcution rule of the pair type. Given
265
 $$\\Gamma \\vdash \\text{ltm : (mcar (ttype (pair ltm rtm)))}$$ and
266
 $$\\Gamma \\vdash \\text{rtm : (mcadr (ttype (pair ltm rtm)))}$$ we have
267
 $$\\Gamma \\vdash \\text{(pair ltm rtm) : (ttype (pair ltm rtm))}$$
268
 "))
269
 
270
 (defun pair (ltm rtm &key (ttype nil))
271
   (values
272
    (make-instance 'pair :ltm ltm :rtm rtm :ttype ttype)))
273
 
274
 (defclass fst (<stlc>)
275
   ((term :initarg :term
276
          :accessor term
277
          :documentation "Term of product type")
278
    (ttype :initarg :ttype
279
           :initform nil
280
           :accessor ttype
281
           :documentation ""))
282
   (:documentation
283
    "The first projection of a term of a product type.
284
 The formal grammar of [FST][class] is:
285
 
286
 ```lisp
287
 (fst term)
288
 ```
289
 
290
 where we can possibly include type information by
291
 
292
 ```lisp
293
 (fst term :ttype ttype)
294
 ```
295
 
296
 The indended semantics are as follows: [TERM][generic-function] is a
297
 term (and hence an [STLC][type]) of a product type, to whose left part
298
 we are projecting to.
299
 
300
 This corresponds to the first projection function gotten by induction
301
 on a term of a product type."))
302
 
303
 (defun fst (term &key (ttype nil))
304
   (values
305
    (make-instance 'fst :term term :ttype ttype)))
306
 
307
 (defclass snd (<stlc>)
308
   ((term :initarg :term
309
          :accessor term
310
          :documentation "Term of product type")
311
    (ttype :initarg :ttype
312
           :initform nil
313
           :accessor ttype
314
           :documentation ""))
315
    (:documentation
316
     "The second projection of a term of a product type.
317
 The formal grammar of [SND][class] is:
318
 
319
 ```lisp
320
 (snd term)
321
 ```
322
 
323
 where we can possibly include type information by
324
 
325
 ```lisp
326
 (snd term :ttype ttype)
327
 ```
328
 
329
 The indended semantics are as follows: [TERM][generic-function] is a
330
 term (and hence an [STLC][type]) of a product type, to whose right
331
 part we are projecting to.
332
 
333
 This corresponds to the second projection function gotten by induction
334
 on a term of a product type."))
335
 
336
 (defun snd (term &key (ttype nil))
337
   (values
338
    (make-instance 'snd :term term :ttype ttype)))
339
 
340
 (defclass lamb (<stlc>)
341
   ((tdom :initarg :tdom
342
          :accessor tdom
343
          :type     list
344
          :documentation "Domain of the lambda term")
345
    (term :initarg :term
346
          :accessor term
347
          :documentation "Term of the codomain mapped to given a variable of tdom")
348
    (ttype :initarg :ttype
349
           :initform nil
350
           :accessor ttype
351
           :documentation ""))
352
   (:documentation
353
    "A term of a function type gotten by providing a term in the codomain
354
 of the function type by assuming one is given variables in the
355
 specified list of types. [LAMB][class] takes in the [TDOM][generic-function]
356
 accessor a list of types - and hence of [SUBSTOBJ][class] - and in the
357
 [TERM][generic-function] a term - and hence an [STLC][type]. The formal grammar
358
 of [LAMB][class] is:
359
 
360
 ```lisp
361
 (lamb tdom term)
362
 ```
363
 
364
 where we can possibly include type information by
365
 
366
 ```lisp
367
 (lamb tdom term :ttype ttype)
368
 ```
369
 
370
 The intended semnatics are: [TDOM][generic-function] is a list of types (and
371
 hence a list of [SUBSTOBJ][GEB.SPEC:SUBSTOBJ]) whose iterative product of
372
 components form the domain of the function type. [TERM][generic-function]
373
 is a term (and hence an [STLC][type]) of the codomain of the function type
374
 gotten in the context to whom we append the list of the domains.
375
 
376
 For a list of length 1, corresponds to the introduction rule of the function
377
 type. Namely, given
378
 $$\\Gamma \\vdash \\text{tdom : Type}$$ and
379
 $$\\Gamma, \\text{tdom} \\vdash \\text{term : (ttype term)}$$ we have
380
 $$\\Gamma \\vdash \\text{(lamb tdom term) : (so-hom-obj tdom (ttype term))}$$
381
 
382
 For a list of length n, this coreesponds to the iterated lambda type, e.g.
383
 
384
 ```lisp
385
 (lamb (list so1 so0) (index 0))
386
 ```
387
 
388
 is a term of
389
 
390
 ```lisp
391
 (so-hom-obj (prod so1 so0) so0)
392
 ```
393
 
394
 or equivalently
395
 
396
 ```lisp
397
 (so-hom-obj so1 (so-hom-obj so0 so0))
398
 ```
399
 
400
 due to Geb's computational definition of the function type.
401
 
402
 Note that [INDEX][class] 0 in the above code is of type [SO1][class].
403
 So that after annotating the term, one gets
404
 
405
 ```lisp
406
 LAMBDA> (ttype (term (lamb (list so1 so0)) (index 0)))
407
 s-1
408
 ```
409
 
410
 So the counting of indeces starts with the leftmost argument for
411
 computational reasons. In practice, typing of [LAMB][class] corresponds with
412
 taking a list of arguments provided to a lambda term, making it a context
413
 in that order and then counting the index of the varibale. Type-theoretically,
414
 
415
 $$\\Gamma \\vdash \\lambda \\Delta (index i)$$
416
 $$\\Delta, \\Gamma \\vdash (index i)$$
417
 
418
 So that by the operational semantics of [INDEX][class], the type of (index i)
419
 in the above context will be the i'th element of the Delta context counted from
420
 the left. Note that in practice we append contexts on the left as computation of
421
 [INDEX][class] is done from the left. Otherwise, the rules are the same as in
422
 usual type theory if context was read from right to left."))
423
 
424
 (defun lamb (tdom term &key (ttype nil))
425
   (values
426
    (make-instance 'lamb :tdom tdom :term term :ttype ttype)))
427
 
428
 (defclass app (<stlc>)
429
   ((fun :initarg :fun
430
         :accessor fun
431
         :documentation "Term of exponential type")
432
    (term :initarg :term
433
          :accessor term
434
          :type list
435
          :documentation "List of Terms of the domain")
436
    (ttype :initarg :ttype
437
           :initform nil
438
           :accessor ttype
439
           :documentation ""))
440
   (:documentation
441
    "A term of an arbitrary type gotten by applying a function of an iterated
442
 function type with a corresponding codomain iteratively to terms in the
443
 domains. [APP][class] takes as argument for the [FUN][generic-function] accessor
444
 a function - and hence an [STLC][type] - whose function type has domain an
445
 iterated [GEB:PROD][class] of [SUBSTOBJ][class] and for the [TERM][generic-function]
446
 a list of terms - and hence of [STLC][type] - matching the types of the
447
 product. The formal grammar of [APP][class] is
448
 
449
 ```lisp
450
 (app fun term)
451
 ```
452
 
453
 where we can possibly include type information by
454
 
455
 ```lisp
456
 (app fun term :ttype ttype)
457
 ```
458
 
459
 The intended semantics are as follows:
460
 [FUN][generic-function] is a term (and hence an [STLC][type]) of a coproduct
461
  type - say of (so-hom-obj (ttype term) y) - and [TERM][generic-function] is a
462
 list of terms (hence also of [STLC][type]) with nth term in the list having the
463
 n-th part of the function type.
464
 
465
 For a one-argument term list, this corresponds to the elimination rule of the
466
 function type. Given
467
 $$\\Gamma \\vdash \\text{fun : (so-hom-obj (ttype term) y)}$$ and
468
 $$\\Gamma \\vdash \\text{term : (ttype term)}$$ we get
469
 $$\\Gamma \\vdash \\text{(app fun term) : y}$$
470
 
471
 For several arguments, this corresponds to successive function application.
472
 Using currying, this corresponds to, given
473
 
474
 ```
475
 G ⊢ (so-hom-obj (A₁ × ··· × Aâ‚™₋₁) Aâ‚™)
476
 G ⊢ f : (so-hom-obj (A₁ × ··· × Aâ‚™₋₁)
477
 G ⊢ táµ¢ : Aáµ¢
478
 ```
479
 
480
 then for each `i` less than `n` gets us
481
 
482
 ```lisp
483
 G ⊢ (app f t₁ ··· tâ‚™₋₁) : Aâ‚™
484
 ```
485
 
486
 Note again that i'th term should correspond to the ith element of the product
487
 in the codomain counted from the left."))
488
 
489
 (defun app (fun term &key (ttype nil))
490
   (values
491
     (make-instance 'app :fun fun :term term :ttype ttype)))
492
 
493
 (defclass index (<stlc>)
494
   ((pos :initarg :pos
495
         :accessor pos
496
         :documentation "Position of type")
497
    (ttype :initarg :ttype
498
           :initform nil
499
           :accessor ttype
500
           :documentation ""))
501
   (:documentation
502
    "The variable term of an arbitrary type in a context. The formal
503
 grammar of [INDEX][class] is
504
 
505
 ```lisp
506
 (index pos)
507
 ```
508
 
509
 where we can possibly include type information by
510
 
511
 ```lisp
512
 (index pos :ttype ttype)
513
 ```
514
 
515
 The intended semantics are as follows: [POS][generic-function] is a
516
 natural number indicating the position of a type in a context.
517
 
518
 This corresponds to the variable rule. Namely given a context
519
 $$\\Gamma_1 , \\ldots , \\Gamma_{pos} , \\ldots , \\Gamma_k $$ we have
520
 
521
 $$\\Gamma_1 , \\ldots , \\Gamma_k \\vdash \\text{(index pos) :} \\Gamma_{pos}$$
522
 
523
 Note that we add contexts on the left rather than on the right contra classical
524
 type-theoretic notation."))
525
 
526
 (defun index (pos &key (ttype nil))
527
   (values
528
    (make-instance 'index :pos pos :ttype ttype)))
529
 
530
 (defclass err (<stlc>)
531
   ((ttype :initarg :ttype
532
           :initform nil
533
           :accessor ttype
534
           :documentation ""))
535
   (:documentation
536
    "An error term of a type supplied by the user. The formal grammar of
537
 [ERR][class] is
538
 
539
 ```lisp
540
 (err ttype)
541
 ```
542
 
543
 The intended semantics are as follows: [ERR][class] represents an error node
544
 currently having no particular feedback but with functionality to be of an
545
 arbitrary type. Note that this is the only STLC term class which does not
546
 have [TTYPE][generic-function] a possibly empty accessor."))
547
 
548
 (defun err (ttype)
549
   (values
550
    (make-instance 'err :ttype ttype)))
551
 
552
 (defclass plus (<stlc>)
553
   ((ltm :initarg :ltm
554
         :accessor ltm
555
         :documentation "")
556
    (rtm :initarg :rtm
557
         :accessor rtm
558
         :documentation "")
559
    (ttype :initarg :ttype
560
           :initform nil
561
           :accessor ttype
562
           :documentation ""))
563
   (:documentation "A term representing syntactic summation of two bits
564
 of the same width. The formal grammar of [PLUS] is
565
 
566
 ```lisp
567
 (plus ltm rtm)
568
 ```
569
 
570
 where we can possibly supply typing info by
571
 
572
 ```lisp
573
 (plus ltm rtm :ttype ttype)
574
 ```
575
 
576
 Note that the summation is ranged, so if the operation goes
577
 above the bit-size of supplied inputs, the corresponding
578
 Vamp-IR code will not verify."))
579
 
580
 (defun plus (ltm rtm &key (ttype nil))
581
   (values
582
    (make-instance 'plus :ltm ltm :rtm rtm :ttype ttype)))
583
 
584
 (defclass times (<stlc>)
585
   ((ltm :initarg :ltm
586
         :accessor ltm
587
         :documentation "")
588
    (rtm :initarg :rtm
589
         :accessor rtm
590
         :documentation "")
591
    (ttype :initarg :ttype
592
           :initform nil
593
           :accessor ttype
594
           :documentation ""))
595
   (:documentation "A term representing syntactic multiplication of two bits
596
 of the same width. The formal grammar of [TIMES] is
597
 
598
 ```lisp
599
 (times ltm rtm)
600
 ```
601
 
602
 where we can possibly supply typing info by
603
 
604
 ```lisp
605
 (times ltm rtm :ttype ttype)
606
 ```
607
 
608
 Note that the multiplication is ranged, so if the operation goes
609
 above the bit-size of supplied inputs, the corresponding
610
 Vamp-IR code will not verify."))
611
 
612
 (defun times (ltm rtm &key (ttype nil))
613
   (values
614
    (make-instance 'times :ltm ltm :rtm rtm :ttype ttype)))
615
 
616
 (defclass minus (<stlc>)
617
   ((ltm :initarg :ltm
618
         :accessor ltm
619
         :documentation "")
620
    (rtm :initarg :rtm
621
         :accessor rtm
622
         :documentation "")
623
    (ttype :initarg :ttype
624
           :initform nil
625
           :accessor ttype
626
           :documentation ""))
627
   (:documentation "A term representing syntactic subtraction of two bits
628
 of the same width. The formal grammar of [MINUS] is
629
 
630
 ```lisp
631
 (minus ltm rtm)
632
 ```
633
 
634
 where we can possibly supply typing info by
635
 
636
 ```lisp
637
 (minus ltm rtm :ttype ttype)
638
 ```
639
 
640
 Note that the subtraction is ranged, so if the operation goes
641
 below zero, the corresponding Vamp-IR code will not verify."))
642
 
643
 (defun minus (ltm rtm &key (ttype nil))
644
   (values
645
    (make-instance 'minus :ltm ltm :rtm rtm :ttype ttype)))
646
 
647
 (defclass divide (<stlc>)
648
   ((ltm :initarg :ltm
649
         :accessor ltm
650
         :documentation "")
651
    (rtm :initarg :rtm
652
         :accessor rtm
653
         :documentation "")
654
    (ttype :initarg :ttype
655
           :initform nil
656
           :accessor ttype
657
           :documentation ""))
658
   (:documentation "A term representing syntactic division (floored)
659
 of two bits of the same width. The formal grammar of [DIVIDE] is
660
 
661
 ```lisp
662
 (minus ltm rtm)
663
 ```
664
 
665
 where we can possibly supply typing info by
666
 
667
 ```lisp
668
 (minus ltm rtm :ttype ttype)
669
 ```
670
 
671
 "))
672
 
673
 (defun divide (ltm rtm &key (ttype nil))
674
   (values
675
    (make-instance 'divide :ltm ltm :rtm rtm :ttype ttype)))
676
 
677
 (defclass bit-choice (<stlc>)
678
   ((bitv :initarg :bitv
679
          :accessor bitv
680
          :documentation "")
681
    (ttype :initarg :ttype
682
           :initform nil
683
           :accessor ttype
684
           :documentation ""))
685
   (:documentation "A term representing a choice of a bit. The formal
686
 grammar of [BIT-CHOICE] is
687
 
688
 ```lisp
689
 (bit-choice bitv)
690
 ```
691
 
692
 where we can possibly supply typing info by
693
 
694
 ```lisp
695
 (bit-choice bitv :ttype ttype)
696
 ```
697
 
698
 Note that the size of bits matter for the operations one supplies them
699
 to. E.g. (plus (bit-choice #*1) (bit-choice #*00)) is not going to pass
700
 our type-check, as both numbers ought to be of exact same bit-width."))
701
 
702
 (defun bit-choice (bitv &key (ttype nil))
703
   (values
704
    (make-instance 'bit-choice :bitv bitv :ttype ttype)))
705
 
706
 (defclass lamb-eq (<stlc>)
707
   ((ltm :initarg :ltm
708
         :accessor ltm
709
         :documentation "")
710
    (rtm :initarg :rtm
711
         :accessor rtm
712
         :documentation "")
713
    (ttype :initarg :ttype
714
           :initform nil
715
           :accessor ttype
716
           :documentation ""))
717
   (:documentation "lamb-eq predicate takes in two bit inputs of same bit-width
718
 and gives true if they are equal and false otherwise. Note that for the usual
719
 Vamp-IR code interpretations, that means that we associate true with left input
720
 into bool and false with the right. Appropriately, in Vamp-IR the first branch
721
 will be associated with the 0 input and teh second branch with 1."))
722
 
723
 (defun lamb-eq (ltm rtm &key (ttype nil))
724
   (values
725
    (make-instance 'lamb-eq :ltm ltm :rtm rtm :ttype ttype)))
726
 
727
 (defclass lamb-lt (<stlc>)
728
   ((ltm :initarg :ltm
729
         :accessor ltm
730
         :documentation "")
731
    (rtm :initarg :rtm
732
         :accessor rtm
733
         :documentation "")
734
    (ttype :initarg :ttype
735
           :initform nil
736
           :accessor ttype
737
           :documentation ""))
738
   (:documentation "lamb-lt predicate takes in two bit inputs of same bit-width
739
 and gives true if ltm is less than rtm and false otherwise. Note that for the usual
740
 Vamp-IR code interpretations, that means that we associate true with left input
741
 into bool and false with the right. Appropriately, in Vamp-IR the first branch
742
 will be associated with the 0 input and teh second branch with 1."))
743
 
744
 (defun lamb-lt (ltm rtm &key (ttype nil))
745
   (values
746
    (make-instance 'lamb-lt :ltm ltm :rtm rtm :ttype ttype)))
747
 
748
 (defclass modulo (<stlc>)
749
   ((ltm :initarg :ltm
750
         :accessor ltm
751
         :documentation "")
752
    (rtm :initarg :rtm
753
         :accessor rtm
754
         :documentation "")
755
    (ttype :initarg :ttype
756
           :initform nil
757
           :accessor ttype
758
           :documentation ""))
759
   (:documentation "A term representing syntactic modulus of the first number
760
 by the second number. The formal grammar of [MODULO] is
761
 
762
 ```lisp
763
 (modulo ltm rtm)
764
 ```
765
 
766
 where we can possibly supply typing info by
767
 
768
 ```lisp
769
 (modulo ltm rtm :ttype ttype)
770
 ```
771
 
772
 meaning that we take ltm mod rtm"))
773
 
774
 (defun modulo (ltm rtm &key (ttype nil))
775
   (values
776
    (make-instance 'modulo :ltm ltm :rtm rtm :ttype ttype)))
777
 �����������������������������������������������������