1module Compiler.ApplicationBuilder
2
3import Compiler.AST
4import Compiler.DependentCore
5
6family ApplicationBuilderError : Type 0
7constructor ApplicationBuilderNoError
8constructor ApplicationBuilderConstructorArityMismatch
9field unrestricted applicationBuilderExpectedArity : Nat
10field unrestricted applicationBuilderSuppliedArity : Nat
11constructor ApplicationBuilderEmptyBinderName
12constructor ApplicationBuilderBinderFreshnessExhausted
13field unrestricted applicationBuilderFreshnessAttempts : Nat
14constructor ApplicationBuilderHostParserForbidden
15constructor ApplicationBuilderHostFallbackForbidden
16end-family
17
18family ApplicationBuilderTelemetry : Type 0
19constructor ApplicationBuilderTelemetryValue
20field unrestricted applicationBuilderRequestedArguments : Nat
21field unrestricted applicationBuilderObservedArguments : Nat
22field unrestricted applicationBuilderUnaryApplicationsEmitted : Nat
23field unrestricted applicationBuilderConstructorChecks : Nat
24field unrestricted applicationBuilderFreshnessProbes : Nat
25field unrestricted applicationBuilderHostParserCalls : Nat
26field unrestricted applicationBuilderHostFallbackCalls : Nat
27field unrestricted applicationBuilderResultCode : Bytes
28end-family
29
30family ApplicationBuilderTermArguments : Type 0
31constructor ApplicationBuilderTermArgumentsEnd
32constructor ApplicationBuilderTermArgumentsNext
33field unrestricted applicationBuilderTermArgument : (family Term)
34recursive unrestricted applicationBuilderRemainingTermArguments
35end-family
36
37family ApplicationBuilderNamedCoreArguments : Type 0
38constructor ApplicationBuilderNamedCoreArgumentsEnd
39constructor ApplicationBuilderNamedCoreArgumentsNext
40field unrestricted applicationBuilderNamedCoreArgument : (family NamedCoreTerm)
41recursive unrestricted applicationBuilderRemainingNamedCoreArguments
42end-family
43
44family ApplicationBuilderCoreArguments : Type 0
45constructor ApplicationBuilderCoreArgumentsEnd
46constructor ApplicationBuilderCoreArgumentsNext
47field unrestricted applicationBuilderCoreArgument : (family CoreTerm)
48recursive unrestricted applicationBuilderRemainingCoreArguments
49end-family
50
51family TermApplicationBuildResult : Type 0
52constructor TermApplicationBuilt
53field unrestricted builtTermApplication : (family Term)
54field unrestricted termApplicationBuildTelemetry : (family ApplicationBuilderTelemetry)
55constructor TermApplicationRejected
56field unrestricted rejectedTermApplicationError : (family ApplicationBuilderError)
57field unrestricted rejectedTermApplicationTelemetry : (family ApplicationBuilderTelemetry)
58end-family
59
60family NamedCoreApplicationBuildResult : Type 0
61constructor NamedCoreApplicationBuilt
62field unrestricted builtNamedCoreApplication : (family NamedCoreTerm)
63field unrestricted namedCoreApplicationBuildTelemetry : (family ApplicationBuilderTelemetry)
64constructor NamedCoreApplicationRejected
65field unrestricted rejectedNamedCoreApplicationError : (family ApplicationBuilderError)
66field unrestricted rejectedNamedCoreApplicationTelemetry : (family ApplicationBuilderTelemetry)
67end-family
68
69family CoreApplicationBuildResult : Type 0
70constructor CoreApplicationBuilt
71field unrestricted builtCoreApplication : (family CoreTerm)
72field unrestricted coreApplicationBuildTelemetry : (family ApplicationBuilderTelemetry)
73constructor CoreApplicationRejected
74field unrestricted rejectedCoreApplicationError : (family ApplicationBuilderError)
75field unrestricted rejectedCoreApplicationTelemetry : (family ApplicationBuilderTelemetry)
76end-family
77
78family FreshBinderNameResult : Type 0
79constructor FreshBinderNameBuilt
80field unrestricted builtFreshBinderName : Bytes
81field unrestricted builtFreshBinderProbes : Nat
82constructor FreshBinderNameRejected
83field unrestricted rejectedFreshBinderError : (family ApplicationBuilderError)
84field unrestricted rejectedFreshBinderProbes : Nat
85end-family
86
87def applicationBuilderSuccessCode = b"APP-000"
88def applicationBuilderArityCode = b"APP-001"
89def applicationBuilderEmptyBinderCode = b"APP-002"
90def applicationBuilderFreshnessCode = b"APP-003"
91def applicationBuilderHostParserCode = b"APP-004"
92def applicationBuilderHostFallbackCode = b"APP-005"
93
94def applicationBuilderErrorStableCode :
95 (pi unrestricted error : (family ApplicationBuilderError) . Bytes) =
96 (lambda unrestricted error : (family ApplicationBuilderError) .
97 (eliminate ApplicationBuilderError
98 (lambda unrestricted value : (family ApplicationBuilderError) . Bytes)
99 error
100 (branch ApplicationBuilderNoError . applicationBuilderSuccessCode)
101 (branch ApplicationBuilderConstructorArityMismatch expected supplied .
102 applicationBuilderArityCode)
103 (branch ApplicationBuilderEmptyBinderName .
104 applicationBuilderEmptyBinderCode)
105 (branch ApplicationBuilderBinderFreshnessExhausted attempts .
106 applicationBuilderFreshnessCode)
107 (branch ApplicationBuilderHostParserForbidden .
108 applicationBuilderHostParserCode)
109 (branch ApplicationBuilderHostFallbackForbidden .
110 applicationBuilderHostFallbackCode)))
111
112def applicationBuilderTelemetryFor :
113 (pi unrestricted requested : Nat .
114 (pi unrestricted observed : Nat .
115 (pi unrestricted emitted : Nat .
116 (pi unrestricted constructorChecks : Nat .
117 (pi unrestricted freshnessProbes : Nat .
118 (pi unrestricted resultCode : Bytes .
119 (family ApplicationBuilderTelemetry))))))) =
120 (lambda unrestricted requested : Nat .
121 (lambda unrestricted observed : Nat .
122 (lambda unrestricted emitted : Nat .
123 (lambda unrestricted constructorChecks : Nat .
124 (lambda unrestricted freshnessProbes : Nat .
125 (lambda unrestricted resultCode : Bytes .
126 (constructor ApplicationBuilderTelemetry
127 ApplicationBuilderTelemetryValue
128 requested
129 observed
130 emitted
131 constructorChecks
132 freshnessProbes
133 zero
134 zero
135 resultCode)))))))
136
137def applicationBuilderNativeOnly : Nat =
138 (app
139 (app coreNaturalAnd
140 (app
141 (app naturalEqual zero)
142 zero))
143 (app
144 (app naturalEqual zero)
145 zero))
146
147def applicationBuilderApply :
148 (pi unrestricted function : (family Term) .
149 (pi unrestricted argument : (family Term) . (family Term))) =
150 (lambda unrestricted function : (family Term) .
151 (lambda unrestricted argument : (family Term) .
152 (constructor Term Application function argument)))
153
154def app2 :
155 (pi unrestricted function : (family Term) .
156 (pi unrestricted first : (family Term) .
157 (pi unrestricted second : (family Term) . (family Term)))) =
158 (lambda unrestricted function : (family Term) .
159 (lambda unrestricted first : (family Term) .
160 (lambda unrestricted second : (family Term) .
161 (constructor Term Application
162 (constructor Term Application function first)
163 second))))
164
165def app3 :
166 (pi unrestricted function : (family Term) .
167 (pi unrestricted first : (family Term) .
168 (pi unrestricted second : (family Term) .
169 (pi unrestricted third : (family Term) . (family Term))))) =
170 (lambda unrestricted function : (family Term) .
171 (lambda unrestricted first : (family Term) .
172 (lambda unrestricted second : (family Term) .
173 (lambda unrestricted third : (family Term) .
174 (constructor Term Application
175 (constructor Term Application
176 (constructor Term Application function first)
177 second)
178 third)))))
179
180def app4 :
181 (pi unrestricted function : (family Term) .
182 (pi unrestricted first : (family Term) .
183 (pi unrestricted second : (family Term) .
184 (pi unrestricted third : (family Term) .
185 (pi unrestricted fourth : (family Term) . (family Term)))))) =
186 (lambda unrestricted function : (family Term) .
187 (lambda unrestricted first : (family Term) .
188 (lambda unrestricted second : (family Term) .
189 (lambda unrestricted third : (family Term) .
190 (lambda unrestricted fourth : (family Term) .
191 (constructor Term Application
192 (constructor Term Application
193 (constructor Term Application
194 (constructor Term Application function first)
195 second)
196 third)
197 fourth))))))
198
199def appN :
200 (pi unrestricted function : (family Term) .
201 (pi unrestricted arguments : (family ApplicationBuilderTermArguments) .
202 (family Term))) =
203 (lambda unrestricted function : (family Term) .
204 (lambda unrestricted arguments : (family ApplicationBuilderTermArguments) .
205 (app
206 (eliminate ApplicationBuilderTermArguments
207 (lambda unrestricted value : (family ApplicationBuilderTermArguments) .
208 (pi unrestricted accumulated : (family Term) . (family Term)))
209 arguments
210 (branch ApplicationBuilderTermArgumentsEnd .
211 (lambda unrestricted accumulated : (family Term) . accumulated))
212 (branch ApplicationBuilderTermArgumentsNext argument remaining induction .
213 (lambda unrestricted accumulated : (family Term) .
214 (app induction
215 (constructor Term Application accumulated argument)))))
216 function)))
217
218def namedCoreApplicationBuilderApply :
219 (pi unrestricted function : (family NamedCoreTerm) .
220 (pi unrestricted argument : (family NamedCoreTerm) .
221 (family NamedCoreTerm))) =
222 (lambda unrestricted function : (family NamedCoreTerm) .
223 (lambda unrestricted argument : (family NamedCoreTerm) .
224 (constructor NamedCoreTerm NamedCoreApplication function argument)))
225
226def namedCoreApp2 :
227 (pi unrestricted function : (family NamedCoreTerm) .
228 (pi unrestricted first : (family NamedCoreTerm) .
229 (pi unrestricted second : (family NamedCoreTerm) .
230 (family NamedCoreTerm)))) =
231 (lambda unrestricted function : (family NamedCoreTerm) .
232 (lambda unrestricted first : (family NamedCoreTerm) .
233 (lambda unrestricted second : (family NamedCoreTerm) .
234 (constructor NamedCoreTerm NamedCoreApplication
235 (constructor NamedCoreTerm NamedCoreApplication function first)
236 second))))
237
238def namedCoreApp3 :
239 (pi unrestricted function : (family NamedCoreTerm) .
240 (pi unrestricted first : (family NamedCoreTerm) .
241 (pi unrestricted second : (family NamedCoreTerm) .
242 (pi unrestricted third : (family NamedCoreTerm) .
243 (family NamedCoreTerm))))) =
244 (lambda unrestricted function : (family NamedCoreTerm) .
245 (lambda unrestricted first : (family NamedCoreTerm) .
246 (lambda unrestricted second : (family NamedCoreTerm) .
247 (lambda unrestricted third : (family NamedCoreTerm) .
248 (constructor NamedCoreTerm NamedCoreApplication
249 (constructor NamedCoreTerm NamedCoreApplication
250 (constructor NamedCoreTerm NamedCoreApplication function first)
251 second)
252 third)))))
253
254def namedCoreApp4 :
255 (pi unrestricted function : (family NamedCoreTerm) .
256 (pi unrestricted first : (family NamedCoreTerm) .
257 (pi unrestricted second : (family NamedCoreTerm) .
258 (pi unrestricted third : (family NamedCoreTerm) .
259 (pi unrestricted fourth : (family NamedCoreTerm) .
260 (family NamedCoreTerm)))))) =
261 (lambda unrestricted function : (family NamedCoreTerm) .
262 (lambda unrestricted first : (family NamedCoreTerm) .
263 (lambda unrestricted second : (family NamedCoreTerm) .
264 (lambda unrestricted third : (family NamedCoreTerm) .
265 (lambda unrestricted fourth : (family NamedCoreTerm) .
266 (constructor NamedCoreTerm NamedCoreApplication
267 (constructor NamedCoreTerm NamedCoreApplication
268 (constructor NamedCoreTerm NamedCoreApplication
269 (constructor NamedCoreTerm NamedCoreApplication function first)
270 second)
271 third)
272 fourth))))))
273
274def namedCoreAppN :
275 (pi unrestricted function : (family NamedCoreTerm) .
276 (pi unrestricted arguments : (family ApplicationBuilderNamedCoreArguments) .
277 (family NamedCoreTerm))) =
278 (lambda unrestricted function : (family NamedCoreTerm) .
279 (lambda unrestricted arguments : (family ApplicationBuilderNamedCoreArguments) .
280 (app
281 (eliminate ApplicationBuilderNamedCoreArguments
282 (lambda unrestricted value : (family ApplicationBuilderNamedCoreArguments) .
283 (pi unrestricted accumulated : (family NamedCoreTerm) .
284 (family NamedCoreTerm)))
285 arguments
286 (branch ApplicationBuilderNamedCoreArgumentsEnd .
287 (lambda unrestricted accumulated : (family NamedCoreTerm) . accumulated))
288 (branch ApplicationBuilderNamedCoreArgumentsNext argument remaining induction .
289 (lambda unrestricted accumulated : (family NamedCoreTerm) .
290 (app induction
291 (constructor NamedCoreTerm NamedCoreApplication
292 accumulated argument)))))
293 function)))
294
295def coreApplicationBuilderApply :
296 (pi unrestricted function : (family CoreTerm) .
297 (pi unrestricted argument : (family CoreTerm) . (family CoreTerm))) =
298 (lambda unrestricted function : (family CoreTerm) .
299 (lambda unrestricted argument : (family CoreTerm) .
300 (constructor CoreTerm CoreApplication function argument)))
301
302def coreApp2 :
303 (pi unrestricted function : (family CoreTerm) .
304 (pi unrestricted first : (family CoreTerm) .
305 (pi unrestricted second : (family CoreTerm) . (family CoreTerm)))) =
306 (lambda unrestricted function : (family CoreTerm) .
307 (lambda unrestricted first : (family CoreTerm) .
308 (lambda unrestricted second : (family CoreTerm) .
309 (constructor CoreTerm CoreApplication
310 (constructor CoreTerm CoreApplication function first)
311 second))))
312
313def coreApp3 :
314 (pi unrestricted function : (family CoreTerm) .
315 (pi unrestricted first : (family CoreTerm) .
316 (pi unrestricted second : (family CoreTerm) .
317 (pi unrestricted third : (family CoreTerm) . (family CoreTerm))))) =
318 (lambda unrestricted function : (family CoreTerm) .
319 (lambda unrestricted first : (family CoreTerm) .
320 (lambda unrestricted second : (family CoreTerm) .
321 (lambda unrestricted third : (family CoreTerm) .
322 (constructor CoreTerm CoreApplication
323 (constructor CoreTerm CoreApplication
324 (constructor CoreTerm CoreApplication function first)
325 second)
326 third)))))
327
328def coreApp4 :
329 (pi unrestricted function : (family CoreTerm) .
330 (pi unrestricted first : (family CoreTerm) .
331 (pi unrestricted second : (family CoreTerm) .
332 (pi unrestricted third : (family CoreTerm) .
333 (pi unrestricted fourth : (family CoreTerm) . (family CoreTerm)))))) =
334 (lambda unrestricted function : (family CoreTerm) .
335 (lambda unrestricted first : (family CoreTerm) .
336 (lambda unrestricted second : (family CoreTerm) .
337 (lambda unrestricted third : (family CoreTerm) .
338 (lambda unrestricted fourth : (family CoreTerm) .
339 (constructor CoreTerm CoreApplication
340 (constructor CoreTerm CoreApplication
341 (constructor CoreTerm CoreApplication
342 (constructor CoreTerm CoreApplication function first)
343 second)
344 third)
345 fourth))))))
346
347def coreAppN :
348 (pi unrestricted function : (family CoreTerm) .
349 (pi unrestricted arguments : (family ApplicationBuilderCoreArguments) .
350 (family CoreTerm))) =
351 (lambda unrestricted function : (family CoreTerm) .
352 (lambda unrestricted arguments : (family ApplicationBuilderCoreArguments) .
353 (app
354 (eliminate ApplicationBuilderCoreArguments
355 (lambda unrestricted value : (family ApplicationBuilderCoreArguments) .
356 (pi unrestricted accumulated : (family CoreTerm) . (family CoreTerm)))
357 arguments
358 (branch ApplicationBuilderCoreArgumentsEnd .
359 (lambda unrestricted accumulated : (family CoreTerm) . accumulated))
360 (branch ApplicationBuilderCoreArgumentsNext argument remaining induction .
361 (lambda unrestricted accumulated : (family CoreTerm) .
362 (app induction
363 (constructor CoreTerm CoreApplication accumulated argument)))))
364 function)))
365
366def applicationBuilderTermArgumentCount :
367 (pi unrestricted arguments : (family ApplicationBuilderTermArguments) . Nat) =
368 (lambda unrestricted arguments : (family ApplicationBuilderTermArguments) .
369 (eliminate ApplicationBuilderTermArguments
370 (lambda unrestricted value : (family ApplicationBuilderTermArguments) . Nat)
371 arguments
372 (branch ApplicationBuilderTermArgumentsEnd . zero)
373 (branch ApplicationBuilderTermArgumentsNext argument remaining induction .
374 (succ induction))))
375
376def applicationBuilderNamedCoreArgumentCount :
377 (pi unrestricted arguments : (family ApplicationBuilderNamedCoreArguments) . Nat) =
378 (lambda unrestricted arguments : (family ApplicationBuilderNamedCoreArguments) .
379 (eliminate ApplicationBuilderNamedCoreArguments
380 (lambda unrestricted value : (family ApplicationBuilderNamedCoreArguments) . Nat)
381 arguments
382 (branch ApplicationBuilderNamedCoreArgumentsEnd . zero)
383 (branch ApplicationBuilderNamedCoreArgumentsNext argument remaining induction .
384 (succ induction))))
385
386def applicationBuilderCoreArgumentCount :
387 (pi unrestricted arguments : (family ApplicationBuilderCoreArguments) . Nat) =
388 (lambda unrestricted arguments : (family ApplicationBuilderCoreArguments) .
389 (eliminate ApplicationBuilderCoreArguments
390 (lambda unrestricted value : (family ApplicationBuilderCoreArguments) . Nat)
391 arguments
392 (branch ApplicationBuilderCoreArgumentsEnd . zero)
393 (branch ApplicationBuilderCoreArgumentsNext argument remaining induction .
394 (succ induction))))
395
396def applicationBuilderTermArgumentSequence :
397 (pi unrestricted arguments : (family ApplicationBuilderTermArguments) .
398 (family Term)) =
399 (lambda unrestricted arguments : (family ApplicationBuilderTermArguments) .
400 (eliminate ApplicationBuilderTermArguments
401 (lambda unrestricted value : (family ApplicationBuilderTermArguments) .
402 (family Term))
403 arguments
404 (branch ApplicationBuilderTermArgumentsEnd .
405 (constructor Term TermSequenceEnd))
406 (branch ApplicationBuilderTermArgumentsNext argument remaining induction .
407 (constructor Term TermSequenceNext argument induction))))
408
409def applicationBuilderNamedCoreArgumentSequence :
410 (pi unrestricted arguments : (family ApplicationBuilderNamedCoreArguments) .
411 (family NamedCoreTerm)) =
412 (lambda unrestricted arguments : (family ApplicationBuilderNamedCoreArguments) .
413 (eliminate ApplicationBuilderNamedCoreArguments
414 (lambda unrestricted value : (family ApplicationBuilderNamedCoreArguments) .
415 (family NamedCoreTerm))
416 arguments
417 (branch ApplicationBuilderNamedCoreArgumentsEnd .
418 (constructor NamedCoreTerm NamedCoreTermSequenceEnd))
419 (branch ApplicationBuilderNamedCoreArgumentsNext argument remaining induction .
420 (constructor NamedCoreTerm NamedCoreTermSequenceNext argument induction))))
421
422def applicationBuilderCoreArgumentSequence :
423 (pi unrestricted arguments : (family ApplicationBuilderCoreArguments) .
424 (family CoreTerm)) =
425 (lambda unrestricted arguments : (family ApplicationBuilderCoreArguments) .
426 (eliminate ApplicationBuilderCoreArguments
427 (lambda unrestricted value : (family ApplicationBuilderCoreArguments) .
428 (family CoreTerm))
429 arguments
430 (branch ApplicationBuilderCoreArgumentsEnd .
431 (constructor CoreTerm CoreTermSequenceEnd))
432 (branch ApplicationBuilderCoreArgumentsNext argument remaining induction .
433 (constructor CoreTerm CoreTermSequenceNext argument induction))))
434
435def buildAppN :
436 (pi unrestricted function : (family Term) .
437 (pi unrestricted arguments : (family ApplicationBuilderTermArguments) .
438 (family TermApplicationBuildResult))) =
439 (lambda unrestricted function : (family Term) .
440 (lambda unrestricted arguments : (family ApplicationBuilderTermArguments) .
441 (constructor TermApplicationBuildResult TermApplicationBuilt
442 (app (app appN function) arguments)
443 (constructor ApplicationBuilderTelemetry
444 ApplicationBuilderTelemetryValue
445 (app applicationBuilderTermArgumentCount arguments)
446 (app applicationBuilderTermArgumentCount arguments)
447 (app applicationBuilderTermArgumentCount arguments)
448 zero
449 zero
450 zero
451 zero
452 applicationBuilderSuccessCode))))
453
454def buildTermConstructorApplication :
455 (pi unrestricted familyName : Bytes .
456 (pi unrestricted constructorName : Bytes .
457 (pi unrestricted expectedArity : Nat .
458 (pi unrestricted arguments : (family ApplicationBuilderTermArguments) .
459 (family TermApplicationBuildResult))))) =
460 (lambda unrestricted familyName : Bytes .
461 (lambda unrestricted constructorName : Bytes .
462 (lambda unrestricted expectedArity : Nat .
463 (lambda unrestricted arguments : (family ApplicationBuilderTermArguments) .
464 (nat-eliminate
465 (lambda unrestricted matched : Nat .
466 (family TermApplicationBuildResult))
467 (constructor TermApplicationBuildResult TermApplicationRejected
468 (constructor ApplicationBuilderError
469 ApplicationBuilderConstructorArityMismatch
470 expectedArity
471 (app applicationBuilderTermArgumentCount arguments))
472 (constructor ApplicationBuilderTelemetry
473 ApplicationBuilderTelemetryValue
474 expectedArity
475 (app applicationBuilderTermArgumentCount arguments)
476 zero
477 (succ zero)
478 zero
479 zero
480 zero
481 applicationBuilderArityCode))
482 (lambda unrestricted predecessor : Nat .
483 (lambda unrestricted induction : (family TermApplicationBuildResult) .
484 (constructor TermApplicationBuildResult TermApplicationBuilt
485 (constructor Term ConstructorApplication
486 familyName
487 constructorName
488 (app applicationBuilderTermArgumentSequence arguments))
489 (constructor ApplicationBuilderTelemetry
490 ApplicationBuilderTelemetryValue
491 expectedArity
492 (app applicationBuilderTermArgumentCount arguments)
493 zero
494 (succ zero)
495 zero
496 zero
497 zero
498 applicationBuilderSuccessCode))))
499 (app
500 (app naturalEqual expectedArity)
501 (app applicationBuilderTermArgumentCount arguments)))))))
502
503def buildNamedCoreConstructorApplication :
504 (pi unrestricted familyName : Bytes .
505 (pi unrestricted constructorName : Bytes .
506 (pi unrestricted expectedArity : Nat .
507 (pi unrestricted arguments : (family ApplicationBuilderNamedCoreArguments) .
508 (family NamedCoreApplicationBuildResult))))) =
509 (lambda unrestricted familyName : Bytes .
510 (lambda unrestricted constructorName : Bytes .
511 (lambda unrestricted expectedArity : Nat .
512 (lambda unrestricted arguments : (family ApplicationBuilderNamedCoreArguments) .
513 (nat-eliminate
514 (lambda unrestricted matched : Nat .
515 (family NamedCoreApplicationBuildResult))
516 (constructor NamedCoreApplicationBuildResult NamedCoreApplicationRejected
517 (constructor ApplicationBuilderError
518 ApplicationBuilderConstructorArityMismatch
519 expectedArity
520 (app applicationBuilderNamedCoreArgumentCount arguments))
521 (constructor ApplicationBuilderTelemetry
522 ApplicationBuilderTelemetryValue
523 expectedArity
524 (app applicationBuilderNamedCoreArgumentCount arguments)
525 zero
526 (succ zero)
527 zero
528 zero
529 zero
530 applicationBuilderArityCode))
531 (lambda unrestricted predecessor : Nat .
532 (lambda unrestricted induction : (family NamedCoreApplicationBuildResult) .
533 (constructor NamedCoreApplicationBuildResult NamedCoreApplicationBuilt
534 (constructor NamedCoreTerm NamedCoreConstructorApplication
535 familyName
536 constructorName
537 (app applicationBuilderNamedCoreArgumentSequence arguments))
538 (constructor ApplicationBuilderTelemetry
539 ApplicationBuilderTelemetryValue
540 expectedArity
541 (app applicationBuilderNamedCoreArgumentCount arguments)
542 zero
543 (succ zero)
544 zero
545 zero
546 zero
547 applicationBuilderSuccessCode))))
548 (app
549 (app naturalEqual expectedArity)
550 (app applicationBuilderNamedCoreArgumentCount arguments)))))))
551
552def buildCoreConstructorApplication :
553 (pi unrestricted familyName : Bytes .
554 (pi unrestricted constructorName : Bytes .
555 (pi unrestricted expectedArity : Nat .
556 (pi unrestricted arguments : (family ApplicationBuilderCoreArguments) .
557 (family CoreApplicationBuildResult))))) =
558 (lambda unrestricted familyName : Bytes .
559 (lambda unrestricted constructorName : Bytes .
560 (lambda unrestricted expectedArity : Nat .
561 (lambda unrestricted arguments : (family ApplicationBuilderCoreArguments) .
562 (nat-eliminate
563 (lambda unrestricted matched : Nat .
564 (family CoreApplicationBuildResult))
565 (constructor CoreApplicationBuildResult CoreApplicationRejected
566 (constructor ApplicationBuilderError
567 ApplicationBuilderConstructorArityMismatch
568 expectedArity
569 (app applicationBuilderCoreArgumentCount arguments))
570 (constructor ApplicationBuilderTelemetry
571 ApplicationBuilderTelemetryValue
572 expectedArity
573 (app applicationBuilderCoreArgumentCount arguments)
574 zero
575 (succ zero)
576 zero
577 zero
578 zero
579 applicationBuilderArityCode))
580 (lambda unrestricted predecessor : Nat .
581 (lambda unrestricted induction : (family CoreApplicationBuildResult) .
582 (constructor CoreApplicationBuildResult CoreApplicationBuilt
583 (constructor CoreTerm CoreConstructorApplication
584 familyName
585 constructorName
586 (app applicationBuilderCoreArgumentSequence arguments))
587 (constructor ApplicationBuilderTelemetry
588 ApplicationBuilderTelemetryValue
589 expectedArity
590 (app applicationBuilderCoreArgumentCount arguments)
591 zero
592 (succ zero)
593 zero
594 zero
595 zero
596 applicationBuilderSuccessCode))))
597 (app
598 (app naturalEqual expectedArity)
599 (app applicationBuilderCoreArgumentCount arguments)))))))
600
601def applicationBuilderScopeDepth :
602 (pi unrestricted scope : (family NameScope) . Nat) =
603 (lambda unrestricted scope : (family NameScope) .
604 (eliminate NameScope
605 (lambda unrestricted value : (family NameScope) . Nat)
606 scope
607 (branch EmptyNameScope . zero)
608 (branch NameScopeBinding identifier outer induction .
609 (succ induction))))
610
611def applicationBuilderScopeContains :
612 (pi unrestricted scope : (family NameScope) .
613 (pi unrestricted candidate : Bytes . Nat)) =
614 (lambda unrestricted scope : (family NameScope) .
615 (eliminate NameScope
616 (lambda unrestricted value : (family NameScope) .
617 (pi unrestricted candidate : Bytes . Nat))
618 scope
619 (branch EmptyNameScope .
620 (lambda unrestricted candidate : Bytes . zero))
621 (branch NameScopeBinding identifier outer induction .
622 (lambda unrestricted candidate : Bytes .
623 (nat-eliminate
624 (lambda unrestricted matched : Nat . Nat)
625 (app induction candidate)
626 (lambda unrestricted predecessor : Nat .
627 (lambda unrestricted ignored : Nat . (succ zero)))
628 (bytes-equal identifier candidate))))))
629
630def applicationBuilderIncrementFreshResult :
631 (pi unrestricted result : (family FreshBinderNameResult) .
632 (family FreshBinderNameResult)) =
633 (lambda unrestricted result : (family FreshBinderNameResult) .
634 (eliminate FreshBinderNameResult
635 (lambda unrestricted value : (family FreshBinderNameResult) .
636 (family FreshBinderNameResult))
637 result
638 (branch FreshBinderNameBuilt name probes .
639 (constructor FreshBinderNameResult FreshBinderNameBuilt
640 name (succ probes)))
641 (branch FreshBinderNameRejected error probes .
642 (constructor FreshBinderNameResult FreshBinderNameRejected
643 error (succ probes)))))
644
645def applicationBuilderFreshBinderSearch :
646 (pi unrestricted fuel : Nat .
647 (pi unrestricted candidate : Bytes .
648 (pi unrestricted scope : (family NameScope) .
649 (family FreshBinderNameResult)))) =
650 (lambda unrestricted fuel : Nat .
651 (nat-eliminate
652 (lambda unrestricted remainingFuel : Nat .
653 (pi unrestricted candidate : Bytes .
654 (pi unrestricted scope : (family NameScope) .
655 (family FreshBinderNameResult))))
656 (lambda unrestricted candidate : Bytes .
657 (lambda unrestricted scope : (family NameScope) .
658 (constructor FreshBinderNameResult FreshBinderNameRejected
659 (constructor ApplicationBuilderError
660 ApplicationBuilderBinderFreshnessExhausted zero)
661 zero)))
662 (lambda unrestricted predecessor : Nat .
663 (lambda unrestricted induction :
664 (pi unrestricted candidate : Bytes .
665 (pi unrestricted scope : (family NameScope) .
666 (family FreshBinderNameResult))) .
667 (lambda unrestricted candidate : Bytes .
668 (lambda unrestricted scope : (family NameScope) .
669 (nat-eliminate
670 (lambda unrestricted collision : Nat .
671 (family FreshBinderNameResult))
672 (constructor FreshBinderNameResult FreshBinderNameBuilt
673 candidate (succ zero))
674 (lambda unrestricted ignoredPredecessor : Nat .
675 (lambda unrestricted ignoredInduction : (family FreshBinderNameResult) .
676 (app applicationBuilderIncrementFreshResult
677 (app
678 (app induction
679 (bytes-append candidate b"'"))
680 scope))))
681 (app
682 (app applicationBuilderScopeContains scope)
683 candidate))))))
684 fuel))
685
686def freshBinderName :
687 (pi unrestricted candidate : Bytes .
688 (pi unrestricted scope : (family NameScope) .
689 (family FreshBinderNameResult))) =
690 (lambda unrestricted candidate : Bytes .
691 (lambda unrestricted scope : (family NameScope) .
692 (nat-eliminate
693 (lambda unrestricted candidateLength : Nat .
694 (family FreshBinderNameResult))
695 (constructor FreshBinderNameResult FreshBinderNameRejected
696 (constructor ApplicationBuilderError ApplicationBuilderEmptyBinderName)
697 zero)
698 (lambda unrestricted predecessor : Nat .
699 (lambda unrestricted induction : (family FreshBinderNameResult) .
700 (app
701 (app
702 (app applicationBuilderFreshBinderSearch
703 (succ (app applicationBuilderScopeDepth scope)))
704 candidate)
705 scope)))
706 (bytes-length candidate))))
707
708def checkBinderNameFresh :
709 (pi unrestricted candidate : Bytes .
710 (pi unrestricted scope : (family NameScope) .
711 (family FreshBinderNameResult))) =
712 (lambda unrestricted candidate : Bytes .
713 (lambda unrestricted scope : (family NameScope) .
714 (nat-eliminate
715 (lambda unrestricted candidateLength : Nat .
716 (family FreshBinderNameResult))
717 (constructor FreshBinderNameResult FreshBinderNameRejected
718 (constructor ApplicationBuilderError ApplicationBuilderEmptyBinderName)
719 zero)
720 (lambda unrestricted predecessor : Nat .
721 (lambda unrestricted induction : (family FreshBinderNameResult) .
722 (nat-eliminate
723 (lambda unrestricted collision : Nat .
724 (family FreshBinderNameResult))
725 (constructor FreshBinderNameResult FreshBinderNameBuilt
726 candidate (succ zero))
727 (lambda unrestricted ignoredPredecessor : Nat .
728 (lambda unrestricted ignoredInduction : (family FreshBinderNameResult) .
729 (constructor FreshBinderNameResult FreshBinderNameRejected
730 (constructor ApplicationBuilderError
731 ApplicationBuilderBinderFreshnessExhausted (succ zero))
732 (succ zero))))
733 (app
734 (app applicationBuilderScopeContains scope)
735 candidate))))
736 (bytes-length candidate))))
737
738def applicationBuilderFreshnessTelemetry :
739 (pi unrestricted result : (family FreshBinderNameResult) .
740 (family ApplicationBuilderTelemetry)) =
741 (lambda unrestricted result : (family FreshBinderNameResult) .
742 (eliminate FreshBinderNameResult
743 (lambda unrestricted value : (family FreshBinderNameResult) .
744 (family ApplicationBuilderTelemetry))
745 result
746 (branch FreshBinderNameBuilt name probes .
747 (constructor ApplicationBuilderTelemetry
748 ApplicationBuilderTelemetryValue
749 zero
750 zero
751 zero
752 zero
753 probes
754 zero
755 zero
756 applicationBuilderSuccessCode))
757 (branch FreshBinderNameRejected error probes .
758 (constructor ApplicationBuilderTelemetry
759 ApplicationBuilderTelemetryValue
760 zero
761 zero
762 zero
763 zero
764 probes
765 zero
766 zero
767 (app applicationBuilderErrorStableCode error)))))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.