1module Compiler.Lexer
2
3family ByteClass : Type 0
4constructor OpenDelimiter
5constructor CloseDelimiter
6constructor Whitespace
7constructor DecimalDigit
8constructor IdentifierByte
9
10end-family
11
12family LexedBytes : Type 0
13constructor LexEnd
14constructor LexByte
15field unrestricted tokenClass : (family ByteClass)
16field unrestricted tokenSpelling : Byte
17recursive unrestricted lexedRest
18
19end-family
20
21family LexToken : Type 0
22constructor TokenOpen
23constructor TokenClose
24constructor TokenBoundary
25constructor TokenAtom
26field unrestricted atomSpelling : Bytes
27
28end-family
29
30family TokenStream : Type 0
31constructor TokenEnd
32constructor TokenNext
33field unrestricted nextToken : (family LexToken)
34recursive unrestricted tokenRest
35
36end-family
37
38def isWhitespace =
39 (lambda unrestricted byte : Byte .
40 (nat-eliminate
41 (lambda unrestricted matchedSpace : Nat . Nat)
42 (nat-eliminate
43 (lambda unrestricted matchedLineFeed : Nat . Nat)
44 (nat-eliminate
45 (lambda unrestricted matchedCarriageReturn : Nat . Nat)
46 (byte-equal byte (byte 9))
47 (lambda unrestricted predecessor : Nat .
48 (lambda unrestricted induction : Nat . (succ zero)))
49 (byte-equal byte (byte 13)))
50 (lambda unrestricted predecessor : Nat .
51 (lambda unrestricted induction : Nat . (succ zero)))
52 (byte-equal byte (byte 10)))
53 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . (succ zero)))
54 (byte-equal byte (byte 32))))
55
56def isDecimalDigit =
57 (lambda unrestricted byte : Byte .
58 (nat-eliminate
59 (lambda unrestricted belowLowerBound : Nat . Nat)
60 (nat-eliminate
61 (lambda unrestricted belowUpperBound : Nat . Nat)
62 zero
63 (lambda unrestricted predecessor : Nat .
64 (lambda unrestricted induction : Nat . (succ zero)))
65 (byte-less-than byte (byte 58)))
66 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero))
67 (byte-less-than byte (byte 48))))
68
69def classifyByte =
70 (lambda unrestricted byte : Byte .
71 (nat-eliminate
72 (lambda unrestricted matchedOpen : Nat . (family ByteClass))
73 (nat-eliminate
74 (lambda unrestricted matchedClose : Nat . (family ByteClass))
75 (nat-eliminate
76 (lambda unrestricted matchedWhitespace : Nat . (family ByteClass))
77 (nat-eliminate
78 (lambda unrestricted matchedDigit : Nat . (family ByteClass))
79 (constructor ByteClass IdentifierByte)
80 (lambda unrestricted predecessor : Nat .
81 (lambda unrestricted induction : (family ByteClass) .
82 (constructor ByteClass DecimalDigit)))
83 (isDecimalDigit byte))
84 (lambda unrestricted predecessor : Nat .
85 (lambda unrestricted induction : (family ByteClass) .
86 (constructor ByteClass Whitespace)))
87 (isWhitespace byte))
88 (lambda unrestricted predecessor : Nat .
89 (lambda unrestricted induction : (family ByteClass) .
90 (constructor ByteClass CloseDelimiter)))
91 (byte-equal byte (byte 41)))
92 (lambda unrestricted predecessor : Nat .
93 (lambda unrestricted induction : (family ByteClass) . (constructor ByteClass OpenDelimiter)))
94 (byte-equal byte (byte 40))))
95
96def lexSource =
97 (lambda unrestricted input : Bytes .
98 (bytes-eliminate
99 (lambda unrestricted remaining : Bytes . (family LexedBytes))
100 (constructor LexedBytes LexEnd)
101 (lambda unrestricted head : Byte .
102 (lambda unrestricted tail : Bytes .
103 (lambda unrestricted lexedTail : (family LexedBytes) .
104 (constructor LexedBytes LexByte (classifyByte head) head lexedTail))))
105 input))
106
107def prependAtomByte =
108 (lambda unrestricted byte : Byte .
109 (lambda unrestricted stream : (family TokenStream) .
110 (eliminate
111 TokenStream
112 (lambda unrestricted value : (family TokenStream) . (family TokenStream))
113 stream
114 (branch
115 TokenEnd
116 .
117 (constructor
118 TokenStream
119 TokenNext
120 (constructor LexToken TokenAtom (bytes-cons byte b""))
121 (constructor TokenStream TokenEnd)))
122 (branch
123 TokenNext
124 nextToken
125 tokenRest
126 ih_tokenRest
127 .
128 (eliminate
129 LexToken
130 (lambda unrestricted value : (family LexToken) . (family TokenStream))
131 nextToken
132 (branch
133 TokenOpen
134 .
135 (constructor
136 TokenStream
137 TokenNext
138 (constructor LexToken TokenAtom (bytes-cons byte b""))
139 (constructor TokenStream TokenNext nextToken tokenRest)))
140 (branch
141 TokenClose
142 .
143 (constructor
144 TokenStream
145 TokenNext
146 (constructor LexToken TokenAtom (bytes-cons byte b""))
147 (constructor TokenStream TokenNext nextToken tokenRest)))
148 (branch
149 TokenBoundary
150 .
151 (constructor
152 TokenStream
153 TokenNext
154 (constructor LexToken TokenAtom (bytes-cons byte b""))
155 (constructor TokenStream TokenNext nextToken tokenRest)))
156 (branch
157 TokenAtom
158 atomSpelling
159 .
160 (constructor
161 TokenStream
162 TokenNext
163 (constructor LexToken TokenAtom (bytes-cons byte atomSpelling))
164 tokenRest)))))))
165
166def lexTokens =
167 (lambda unrestricted input : Bytes .
168 (bytes-eliminate
169 (lambda unrestricted remaining : Bytes . (family TokenStream))
170 (constructor TokenStream TokenEnd)
171 (lambda unrestricted head : Byte .
172 (lambda unrestricted tail : Bytes .
173 (lambda unrestricted lexedTail : (family TokenStream) .
174 (eliminate
175 ByteClass
176 (lambda unrestricted value : (family ByteClass) . (family TokenStream))
177 (classifyByte head)
178 (branch
179 OpenDelimiter
180 .
181 (constructor TokenStream TokenNext (constructor LexToken TokenOpen) lexedTail))
182 (branch
183 CloseDelimiter
184 .
185 (constructor TokenStream TokenNext (constructor LexToken TokenClose) lexedTail))
186 (branch
187 Whitespace
188 .
189 (constructor TokenStream TokenNext (constructor LexToken TokenBoundary) lexedTail))
190 (branch DecimalDigit . (prependAtomByte head lexedTail))
191 (branch IdentifierByte . (prependAtomByte head lexedTail))))))
192 input))
193
194def lexedFingerprint =
195 (lambda unrestricted stream : (family LexedBytes) .
196 (eliminate
197 LexedBytes
198 (lambda unrestricted value : (family LexedBytes) . Nat)
199 stream
200 (branch LexEnd . zero)
201 (branch
202 LexByte
203 tokenClass
204 tokenSpelling
205 lexedRest
206 ih_lexedRest
207 .
208 (eliminate
209 ByteClass
210 (lambda unrestricted value : (family ByteClass) . Nat)
211 tokenClass
212 (branch OpenDelimiter . (succ ih_lexedRest))
213 (branch CloseDelimiter . (succ (succ ih_lexedRest)))
214 (branch Whitespace . (succ (succ (succ ih_lexedRest))))
215 (branch DecimalDigit . (succ (succ (succ (succ ih_lexedRest)))))
216 (branch IdentifierByte . (succ (succ (succ (succ (succ ih_lexedRest))))))))))
217
218def lexerSample : (family LexedBytes) =
219 (lexSource b"(a0)")The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.