110def quotedByteStep =
111 (lambda unrestricted head : Byte .
112 (lambda unrestricted state : (family QuotedByteState) .
113 (lambda unrestricted offset : Nat .
114 (lambda unrestricted continue : (pi unrestricted state : (family QuotedByteState) . (pi unrestricted offset : Nat . (family QuotedLiteralResult))) .
115 (eliminate
116 QuotedByteState
117 (lambda unrestricted current : (family QuotedByteState) . (family QuotedLiteralResult))
118 state
119 (branch
120 QuotedNormal
121 .
122 (quotedChoose
123 (byte-equal head (byte 13))
124 (lambda unrestricted force : Nat .
125 (constructor
126 QuotedLiteralResult
127 QuotedLiteralFailed
128 (constructor QuotedLiteralFailure QuotedNewline)
129 offset
130 (succ offset)))
131 (lambda unrestricted force : Nat .
132 (quotedChoose
133 (byte-equal head (byte 10))
134 (lambda unrestricted force : Nat .
135 (constructor
136 QuotedLiteralResult
137 QuotedLiteralFailed
138 (constructor QuotedLiteralFailure QuotedNewline)
139 offset
140 (succ offset)))
141 (lambda unrestricted force : Nat .
142 (quotedChoose
143 (byte-equal head (byte 34))
144 (lambda unrestricted force : Nat .
145 (continue (constructor QuotedByteState QuotedClosed) (succ offset)))
146 (lambda unrestricted force : Nat .
147 (quotedChoose
148 (byte-equal head (byte 92))
149 (lambda unrestricted force : Nat .
150 (continue
151 (constructor QuotedByteState QuotedEscape offset)
152 (succ offset)))
153 (lambda unrestricted force : Nat .
154 (quotedChoose
155 (byte-less-than head (byte 128))
156 (lambda unrestricted force : Nat .
157 (quotedPrepend
158 head
159 (continue
160 (constructor QuotedByteState QuotedNormal)
161 (succ offset))))
162 (lambda unrestricted force : Nat .
163 (continue
164 (constructor
165 QuotedByteState
166 QuotedFailureTail
167 (constructor QuotedLiteralFailure QuotedNonASCII)
168 offset
169 zero)
170 (succ offset)))))))))))))
171 (branch
172 QuotedEscape
173 start
174 .
175 (quotedChoose
176 (byte-equal head (byte 13))
177 (lambda unrestricted force : Nat .
178 (constructor
179 QuotedLiteralResult
180 QuotedLiteralFailed
181 (constructor QuotedLiteralFailure QuotedNewline)
182 offset
183 (succ offset)))
184 (lambda unrestricted force : Nat .
185 (quotedChoose
186 (byte-equal head (byte 10))
187 (lambda unrestricted force : Nat .
188 (constructor
189 QuotedLiteralResult
190 QuotedLiteralFailed
191 (constructor QuotedLiteralFailure QuotedNewline)
192 offset
193 (succ offset)))
194 (lambda unrestricted force : Nat .
195 (quotedChoose
196 (byte-equal head (byte 92))
197 (lambda unrestricted force : Nat .
198 (quotedPrepend
199 (byte 92)
200 (continue (constructor QuotedByteState QuotedNormal) (succ offset))))
201 (lambda unrestricted force : Nat .
202 (quotedChoose
203 (byte-equal head (byte 34))
204 (lambda unrestricted force : Nat .
205 (quotedPrepend
206 (byte 34)
207 (continue (constructor QuotedByteState QuotedNormal) (succ offset))))
208 (lambda unrestricted force : Nat .
209 (quotedChoose
210 (byte-equal head (byte 114))
211 (lambda unrestricted force : Nat .
212 (quotedPrepend
213 (byte 13)
214 (continue
215 (constructor QuotedByteState QuotedNormal)
216 (succ offset))))
217 (lambda unrestricted force : Nat .
218 (quotedChoose
219 (byte-equal head (byte 116))
220 (lambda unrestricted force : Nat .
221 (quotedPrepend
222 (byte 9)
223 (continue
224 (constructor QuotedByteState QuotedNormal)
225 (succ offset))))
226 (lambda unrestricted force : Nat .
227 (quotedChoose
228 (byte-equal head (byte 110))
229 (lambda unrestricted force : Nat .
230 (quotedPrepend
231 (byte 10)
232 (continue
233 (constructor QuotedByteState QuotedNormal)
234 (succ offset))))
235 (lambda unrestricted force : Nat .
236 (quotedChoose
237 (byte-equal head (byte 120))
238 (lambda unrestricted force : Nat .
239 (continue
240 (constructor QuotedByteState QuotedHexHigh start)
241 (succ offset)))
242 (lambda unrestricted force : Nat .
243 (continue
244 (constructor
245 QuotedByteState
246 QuotedFailureTail
247 (constructor QuotedLiteralFailure QuotedUnknownEscape)
248 start
249 zero)
250 (succ offset)))))))))))))))))))
251 (branch
252 QuotedHexHigh
253 start
254 .
255 (eliminate
256 IntegerLiteralDigitResult
257 (lambda unrestricted decoded : (family IntegerLiteralDigitResult) .
258 (family QuotedLiteralResult))
259 (Compiler.IntegerLiteral/integerLiteralDecodeHex head)
260 (branch
261 IntegerLiteralDigitValue
262 digit
263 .
264 (continue (constructor QuotedByteState QuotedHexLow start digit) (succ offset)))
265 (branch
266 IntegerLiteralDigitFailed
267 failure
268 .
269 (quotedChoose
270 (quotedRecoveryBoundary head)
271 (lambda unrestricted force : Nat .
272 (constructor
273 QuotedLiteralResult
274 QuotedLiteralFailed
275 (constructor QuotedLiteralFailure QuotedBadHex)
276 start
277 offset))
278 (lambda unrestricted force : Nat .
279 (continue
280 (constructor
281 QuotedByteState
282 QuotedFailureTail
283 (constructor QuotedLiteralFailure QuotedBadHex)
284 start
285 (succ zero))
286 (succ offset)))))))
287 (branch
288 QuotedHexLow
289 start
290 high
291 .
292 (eliminate
293 IntegerLiteralDigitResult
294 (lambda unrestricted decoded : (family IntegerLiteralDigitResult) .
295 (family QuotedLiteralResult))
296 (Compiler.IntegerLiteral/integerLiteralDecodeHex head)
297 (branch
298 IntegerLiteralDigitValue
299 digit
300 .
301 (quotedPrepend
302 (nat-to-byte
303 (Std.Natural/naturalAdd
304 (Std.Natural/naturalMultiply high (byte-to-nat (byte 16)))
305 digit))
306 (continue (constructor QuotedByteState QuotedNormal) (succ offset))))
307 (branch
308 IntegerLiteralDigitFailed
309 failure
310 .
311 (quotedChoose
312 (quotedRecoveryBoundary head)
313 (lambda unrestricted force : Nat .
314 (constructor
315 QuotedLiteralResult
316 QuotedLiteralFailed
317 (constructor QuotedLiteralFailure QuotedBadHex)
318 start
319 offset))
320 (lambda unrestricted force : Nat .
321 (continue
322 (constructor
323 QuotedByteState
324 QuotedFailureTail
325 (constructor QuotedLiteralFailure QuotedBadHex)
326 start
327 zero)
328 (succ offset)))))))
329 (branch
330 QuotedFailureTail
331 failure
332 start
333 remaining
334 .
335 (quotedChoose
336 (Data.UTF8/utf8ContinuationValid head)
337 (lambda unrestricted force : Nat .
338 (continue
339 (constructor QuotedByteState QuotedFailureTail failure start remaining)
340 (succ offset)))
341 (lambda unrestricted force : Nat .
342 (quotedChoose
343 remaining
344 (lambda unrestricted force : Nat .
345 (quotedChoose
346 (quotedRecoveryBoundary head)
347 (lambda unrestricted force : Nat .
348 (constructor QuotedLiteralResult QuotedLiteralFailed failure start offset))
349 (lambda unrestricted force : Nat .
350 (continue
351 (constructor QuotedByteState QuotedFailureTail failure start zero)
352 (succ offset)))))
353 (lambda unrestricted force : Nat .
354 (constructor QuotedLiteralResult QuotedLiteralFailed failure start offset))))))
355 (branch
356 QuotedClosed
357 .
358 (constructor
359 QuotedLiteralResult
360 QuotedLiteralFailed
361 (constructor QuotedLiteralFailure QuotedTrailingInput)
362 offset
363 (succ offset))))))))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.