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

KindCoveredAll%
expression016 0.0
branch00nil
Key
Not instrumented
Conditionalized out
Executed
Not executed
 
Both branches taken
One branch taken
Neither branch taken
1
 (in-package :geb.utils)
2
 
3
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
4
 ;; API module
5
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
6
 
7
 (geb.utils:muffle-package-variance
8
  (uiop:define-package #:geb.lambda.main
9
    (:documentation "A basic lambda calculus model")
10
    (:mix #:geb.lambda.spec #:geb.common #:common-lisp)
11
    (:reexport #:geb.lambda.spec)
12
    (:export #:@lambda-api)))
13
 
14
 (in-package #:geb.lambda.main)
15
 
16
 (pax:defsection @lambda-api (:title "Main functionality")
17
   "This covers the main API for the STLC module"
18
 
19
   (ann-term1          pax:generic-function)
20
   (index-check        pax:function)
21
   (fun-to-hom         pax:function)
22
   (ann-term2          pax:function)
23
   (annotated-term     pax:function)
24
   (type-of-term-w-fun pax:function)
25
   (type-of-term       pax:function)
26
   (well-defp          pax:generic-function)
27
   (fun-type           pax:class)
28
   (fun-type           pax:function)
29
   (errorp             pax:function)
30
   (reducer            pax:function)
31
 
32
   (mcar              (pax:method () (fun-type)))
33
   (mcadr             (pax:method () (fun-type))))
34
 
35
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
36
 ;; trans module
37
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
38
 
39
 (in-package :geb.utils)
40
 
41
 (geb.utils:muffle-package-variance
42
  (uiop:define-package #:geb.lambda.trans
43
    (:documentation "A basic lambda translator into other parts of geb")
44
    (:mix #:geb.lambda.spec #:geb.common #:common-lisp :geb.lambda.main)
45
    (:export #:@utility #:@stlc-conversion)))
46
 
47
 (in-package #:geb.lambda.trans)
48
 
49
 (pax:defsection @utility (:title "Utility Functionality")
50
   "These are utility functions relating to translating lambda terms to other types"
51
   (stlc-ctx-to-mu  pax:function)
52
   (so-hom  pax:function))
53
 
54
 (pax:defsection @stlc-conversion (:title "Transition Functions")
55
   "These functions deal with transforming the data structure to other
56
 data types"
57
 
58
   "One important note about the lambda conversions is that all
59
 transition functions except [TO-CAT] do not take a context.
60
 
61
 Thus if the [\\<STLC\\>] term contains free variables, then call
62
 [TO-CAT] and give it the desired context before calling
63
 any other transition functions"
64
   (to-cat     (pax:method () (t <stlc>)))
65
   (to-poly    (pax:method () (<stlc>)))
66
   (to-bitc    (pax:method () (<stlc>)))
67
   (to-seqn    (pax:method () (<stlc>)))
68
   (to-circuit (pax:method () (<stlc> t)))
69
   (@utility   pax:section))
70
 
71
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
72
 ;; lambda module
73
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
74
 
75
 (in-package :geb.utils)
76
 
77
 (geb.utils:muffle-package-variance
78
  (uiop:define-package #:geb.lambda
79
    (:documentation "A basic lambda calculus model")
80
    (:mix #:geb.lambda.spec #:geb.lambda.trans #:geb.common #:common-lisp)
81
    (:use-reexport #:geb.lambda.spec #:geb.lambda.main #:geb.lambda.trans)
82
    (:export #:@stlc)))
83
 
84
 (in-package #:geb.lambda)
85
 
86
 (pax:defsection @stlc (:title "The Simply Typed Lambda Calculus model")
87
   "This covers GEB's view on simply typed lambda calculus
88
 
89
 This serves as a useful frontend for those wishing to write a compiler
90
 to GEB and do not wish to target the categorical model.
91
 
92
 If one is targeting their compiler to the frontend, then the following
93
 code should be useful for you.
94
 
95
 ```lisp
96
 (in-package :geb.lambda.main)
97
 
98
 MAIN>
99
 (to-circuit
100
  (lamb (list (coprod so1 so1))
101
               (index 0))
102
  :id)
103
 (def id x1 = {
104
    (x1)
105
  };)
106
 
107
 MAIN>
108
 (to-circuit
109
  (lamb (list (coprod so1 so1))
110
               (case-on (index 0)
111
                               (lamb (list so1)
112
                                            (right so1 (unit)))
113
                               (lamb (list so1)
114
                                            (left so1 (unit)))))
115
  :not)
116
 (def not x1 = {
117
    (((1 - x1) * 1) + (x1 * 0), ((1 - x1) * 1) + (x1 * 0))
118
  };)
119
 
120
 MAIN> (to-circuit (lamb (list geb-bool:bool)
121
                         (left so1 (right so1 (index 0)))) :foo)
122
 (def foo x1 = {
123
    (0, 1, x1)
124
  };)
125
 ```
126
 
127
 For testing purposes, it may be useful to go to the `BITC` backend and
128
 run our interpreter
129
 
130
 
131
 ```lisp
132
 MAIN>
133
 (gapply (to-bitc
134
          (lamb (list (coprod so1 so1))
135
                (case-on (index 0)
136
                         (lamb (list so1)
137
                               (right so1 (unit)))
138
                         (lamb (list so1)
139
                               (left so1 (unit))))))
140
         #*1)
141
 #*00
142
 MAIN>
143
 (gapply (to-bitc
144
          (lamb (list (coprod so1 so1))
145
                (case-on (index 0)
146
                         (lamb (list so1)
147
                               (right so1 (unit)))
148
                         (lamb (list so1)
149
                               (left so1 (unit))))))
150
         #*0)
151
 #*11
152
 ```
153
 
154
 "
155
   (@lambda-specs pax:section)
156
   (@lambda-api  pax:section)
157
   (@stlc-conversion pax:section))