Compiler.Elaborator

1module Compiler.Elaborator
2
3import Compiler.AST
4import Compiler.Lexer
5import Compiler.Parser
6
7family ClosedNatural : Type 0
8constructor ClosedZero
9constructor ClosedSuccessor
10recursive unrestricted closedPredecessor
11
12end-family
13
14family PartialPrimitive : Type 0
15constructor PartialByteComparison
16field unrestricted partialComparisonOperation : Nat
17field unrestricted partialComparisonLeft : Byte
18constructor PartialNaturalLessThan
19field unrestricted partialNaturalLeft : (family ClosedNatural)
20constructor PartialBytesCons
21field unrestricted partialConsHead : Byte
22constructor PartialBytesAppend
23field unrestricted partialAppendLeft : Bytes
24
25end-family
26
27family ClosedNaturalElaboration : Type 0
28constructor NaturalElaborated
29field unrestricted elaboratedNatural : (family ClosedNatural)
30constructor BytesElaborated
31field unrestricted elaboratedBytes : Bytes
32constructor ByteElaborated
33field unrestricted elaboratedByte : Byte
34constructor PrimitivePartial
35field unrestricted elaboratedPartial : (family PartialPrimitive)
36constructor UnboundVariable
37field unrestricted unboundSpelling : Bytes
38constructor UnsupportedTerm
39field unrestricted unsupportedCode : Nat
40
41end-family
42
43def closeNaturalLiteral =
44  (lambda unrestricted value : Nat .
45    (nat-eliminate
46      (lambda unrestricted remaining : Nat . (family ClosedNatural))
47      (constructor ClosedNatural ClosedZero)
48      (lambda unrestricted predecessor : Nat .
49        (lambda unrestricted induction : (family ClosedNatural) .
50          (constructor ClosedNatural ClosedSuccessor induction)))
51      value))
52
53def openClosedNatural =
54  (lambda unrestricted value : (family ClosedNatural) .
55    (eliminate
56      ClosedNatural
57      (lambda unrestricted remaining : (family ClosedNatural) . Nat)
58      value
59      (branch ClosedZero . zero)
60      (branch ClosedSuccessor closedPredecessor ih_closedPredecessor . (succ ih_closedPredecessor))))
61
62def byteToNaturalSpelling =
63  b"byte-to-nat"
64
65def naturalToByteSpelling =
66  b"nat-to-byte"
67
68def bytesLengthSpelling =
69  b"bytes-length"
70
71def byteEqualSpelling =
72  b"byte-equal"
73
74def byteLessThanSpelling =
75  b"byte-less-than"
76
77def naturalLessThanSpelling =
78  b"nat-less-than"
79
80def bytesAppendSpelling =
81  b"bytes-append"
82
83def unsupportedApplicationResult =
84  (constructor ClosedNaturalElaboration UnsupportedTerm (succ (succ (succ zero))))
85
86def elaborateSuccessorArgument =
87  (lambda unrestricted result : (family ClosedNaturalElaboration) .
88    (eliminate
89      ClosedNaturalElaboration
90      (lambda unrestricted value : (family ClosedNaturalElaboration) .
91        (family ClosedNaturalElaboration))
92      result
93      (branch
94        NaturalElaborated
95        elaboratedNatural
96        .
97        (constructor
98          ClosedNaturalElaboration
99          NaturalElaborated
100          (constructor ClosedNatural ClosedSuccessor elaboratedNatural)))
101      (branch BytesElaborated elaboratedBytes . unsupportedApplicationResult)
102      (branch ByteElaborated elaboratedByte . unsupportedApplicationResult)
103      (branch PrimitivePartial elaboratedPartial . unsupportedApplicationResult)
104      (branch
105        UnboundVariable
106        unboundSpelling
107        .
108        (constructor ClosedNaturalElaboration UnboundVariable unboundSpelling))
109      (branch
110        UnsupportedTerm
111        unsupportedCode
112        .
113        (constructor ClosedNaturalElaboration UnsupportedTerm unsupportedCode))))
114
115def elaborateByteToNaturalArgument =
116  (lambda unrestricted result : (family ClosedNaturalElaboration) .
117    (eliminate
118      ClosedNaturalElaboration
119      (lambda unrestricted value : (family ClosedNaturalElaboration) .
120        (family ClosedNaturalElaboration))
121      result
122      (branch NaturalElaborated elaboratedNatural . unsupportedApplicationResult)
123      (branch BytesElaborated elaboratedBytes . unsupportedApplicationResult)
124      (branch
125        ByteElaborated
126        elaboratedByte
127        .
128        (constructor
129          ClosedNaturalElaboration
130          NaturalElaborated
131          (closeNaturalLiteral (byte-to-nat elaboratedByte))))
132      (branch PrimitivePartial elaboratedPartial . unsupportedApplicationResult)
133      (branch
134        UnboundVariable
135        unboundSpelling
136        .
137        (constructor ClosedNaturalElaboration UnboundVariable unboundSpelling))
138      (branch
139        UnsupportedTerm
140        unsupportedCode
141        .
142        (constructor ClosedNaturalElaboration UnsupportedTerm unsupportedCode))))
143
144def elaborateNaturalToByteArgument =
145  (lambda unrestricted result : (family ClosedNaturalElaboration) .
146    (eliminate
147      ClosedNaturalElaboration
148      (lambda unrestricted value : (family ClosedNaturalElaboration) .
149        (family ClosedNaturalElaboration))
150      result
151      (branch
152        NaturalElaborated
153        elaboratedNatural
154        .
155        (constructor
156          ClosedNaturalElaboration
157          ByteElaborated
158          (nat-to-byte (openClosedNatural elaboratedNatural))))
159      (branch BytesElaborated elaboratedBytes . unsupportedApplicationResult)
160      (branch ByteElaborated elaboratedByte . unsupportedApplicationResult)
161      (branch PrimitivePartial elaboratedPartial . unsupportedApplicationResult)
162      (branch
163        UnboundVariable
164        unboundSpelling
165        .
166        (constructor ClosedNaturalElaboration UnboundVariable unboundSpelling))
167      (branch
168        UnsupportedTerm
169        unsupportedCode
170        .
171        (constructor ClosedNaturalElaboration UnsupportedTerm unsupportedCode))))
172
173def elaborateBytesLengthArgument =
174  (lambda unrestricted result : (family ClosedNaturalElaboration) .
175    (eliminate
176      ClosedNaturalElaboration
177      (lambda unrestricted value : (family ClosedNaturalElaboration) .
178        (family ClosedNaturalElaboration))
179      result
180      (branch NaturalElaborated elaboratedNatural . unsupportedApplicationResult)
181      (branch
182        BytesElaborated
183        elaboratedBytes
184        .
185        (constructor
186          ClosedNaturalElaboration
187          NaturalElaborated
188          (closeNaturalLiteral (bytes-length elaboratedBytes))))
189      (branch ByteElaborated elaboratedByte . unsupportedApplicationResult)
190      (branch PrimitivePartial elaboratedPartial . unsupportedApplicationResult)
191      (branch
192        UnboundVariable
193        unboundSpelling
194        .
195        (constructor ClosedNaturalElaboration UnboundVariable unboundSpelling))
196      (branch
197        UnsupportedTerm
198        unsupportedCode
199        .
200        (constructor ClosedNaturalElaboration UnsupportedTerm unsupportedCode))))
201
202def elaborateByteComparisonValue =
203  (lambda unrestricted operation : Nat .
204    (lambda unrestricted left : Byte .
205      (lambda unrestricted right : (family ClosedNaturalElaboration) .
206        (eliminate
207          ClosedNaturalElaboration
208          (lambda unrestricted value : (family ClosedNaturalElaboration) .
209            (family ClosedNaturalElaboration))
210          right
211          (branch NaturalElaborated elaboratedNatural . unsupportedApplicationResult)
212          (branch BytesElaborated elaboratedBytes . unsupportedApplicationResult)
213          (branch
214            ByteElaborated
215            elaboratedByte
216            .
217            (constructor
218              ClosedNaturalElaboration
219              NaturalElaborated
220              (closeNaturalLiteral
221                (nat-eliminate
222                  (lambda unrestricted selectedOperation : Nat . Nat)
223                  (byte-equal left elaboratedByte)
224                  (lambda unrestricted predecessor : Nat .
225                    (lambda unrestricted induction : Nat . (byte-less-than left elaboratedByte)))
226                  operation))))
227          (branch PrimitivePartial elaboratedPartial . unsupportedApplicationResult)
228          (branch
229            UnboundVariable
230            unboundSpelling
231            .
232            (constructor ClosedNaturalElaboration UnboundVariable unboundSpelling))
233          (branch
234            UnsupportedTerm
235            unsupportedCode
236            .
237            (constructor ClosedNaturalElaboration UnsupportedTerm unsupportedCode))))))
238
239def beginByteComparison =
240  (lambda unrestricted operation : Nat .
241    (lambda unrestricted left : (family ClosedNaturalElaboration) .
242      (eliminate
243        ClosedNaturalElaboration
244        (lambda unrestricted value : (family ClosedNaturalElaboration) .
245          (family ClosedNaturalElaboration))
246        left
247        (branch NaturalElaborated elaboratedNatural . unsupportedApplicationResult)
248        (branch BytesElaborated elaboratedBytes . unsupportedApplicationResult)
249        (branch
250          ByteElaborated
251          elaboratedByte
252          .
253          (constructor
254            ClosedNaturalElaboration
255            PrimitivePartial
256            (constructor PartialPrimitive PartialByteComparison operation elaboratedByte)))
257        (branch PrimitivePartial elaboratedPartial . unsupportedApplicationResult)
258        (branch
259          UnboundVariable
260          unboundSpelling
261          .
262          (constructor ClosedNaturalElaboration UnboundVariable unboundSpelling))
263        (branch
264          UnsupportedTerm
265          unsupportedCode
266          .
267          (constructor ClosedNaturalElaboration UnsupportedTerm unsupportedCode)))))
268
269def elaborateNaturalLessThanValue =
270  (lambda unrestricted left : (family ClosedNatural) .
271    (lambda unrestricted right : (family ClosedNaturalElaboration) .
272      (eliminate
273        ClosedNaturalElaboration
274        (lambda unrestricted value : (family ClosedNaturalElaboration) .
275          (family ClosedNaturalElaboration))
276        right
277        (branch
278          NaturalElaborated
279          elaboratedNatural
280          .
281          (constructor
282            ClosedNaturalElaboration
283            NaturalElaborated
284            (closeNaturalLiteral
285              (nat-less-than (openClosedNatural left) (openClosedNatural elaboratedNatural)))))
286        (branch BytesElaborated elaboratedBytes . unsupportedApplicationResult)
287        (branch ByteElaborated elaboratedByte . unsupportedApplicationResult)
288        (branch PrimitivePartial elaboratedPartial . unsupportedApplicationResult)
289        (branch
290          UnboundVariable
291          unboundSpelling
292          .
293          (constructor ClosedNaturalElaboration UnboundVariable unboundSpelling))
294        (branch
295          UnsupportedTerm
296          unsupportedCode
297          .
298          (constructor ClosedNaturalElaboration UnsupportedTerm unsupportedCode)))))
299
300def beginNaturalLessThan =
301  (lambda unrestricted left : (family ClosedNaturalElaboration) .
302    (eliminate
303      ClosedNaturalElaboration
304      (lambda unrestricted value : (family ClosedNaturalElaboration) .
305        (family ClosedNaturalElaboration))
306      left
307      (branch
308        NaturalElaborated
309        elaboratedNatural
310        .
311        (constructor
312          ClosedNaturalElaboration
313          PrimitivePartial
314          (constructor PartialPrimitive PartialNaturalLessThan elaboratedNatural)))
315      (branch BytesElaborated elaboratedBytes . unsupportedApplicationResult)
316      (branch ByteElaborated elaboratedByte . unsupportedApplicationResult)
317      (branch PrimitivePartial elaboratedPartial . unsupportedApplicationResult)
318      (branch
319        UnboundVariable
320        unboundSpelling
321        .
322        (constructor ClosedNaturalElaboration UnboundVariable unboundSpelling))
323      (branch
324        UnsupportedTerm
325        unsupportedCode
326        .
327        (constructor ClosedNaturalElaboration UnsupportedTerm unsupportedCode))))
328
329def beginBytesCons =
330  (lambda unrestricted left : (family ClosedNaturalElaboration) .
331    (eliminate
332      ClosedNaturalElaboration
333      (lambda unrestricted value : (family ClosedNaturalElaboration) .
334        (family ClosedNaturalElaboration))
335      left
336      (branch NaturalElaborated elaboratedNatural . unsupportedApplicationResult)
337      (branch BytesElaborated elaboratedBytes . unsupportedApplicationResult)
338      (branch
339        ByteElaborated
340        elaboratedByte
341        .
342        (constructor
343          ClosedNaturalElaboration
344          PrimitivePartial
345          (constructor PartialPrimitive PartialBytesCons elaboratedByte)))
346      (branch PrimitivePartial elaboratedPartial . unsupportedApplicationResult)
347      (branch
348        UnboundVariable
349        unboundSpelling
350        .
351        (constructor ClosedNaturalElaboration UnboundVariable unboundSpelling))
352      (branch
353        UnsupportedTerm
354        unsupportedCode
355        .
356        (constructor ClosedNaturalElaboration UnsupportedTerm unsupportedCode))))
357
358def beginBytesAppend =
359  (lambda unrestricted left : (family ClosedNaturalElaboration) .
360    (eliminate
361      ClosedNaturalElaboration
362      (lambda unrestricted value : (family ClosedNaturalElaboration) .
363        (family ClosedNaturalElaboration))
364      left
365      (branch NaturalElaborated elaboratedNatural . unsupportedApplicationResult)
366      (branch
367        BytesElaborated
368        elaboratedBytes
369        .
370        (constructor
371          ClosedNaturalElaboration
372          PrimitivePartial
373          (constructor PartialPrimitive PartialBytesAppend elaboratedBytes)))
374      (branch ByteElaborated elaboratedByte . unsupportedApplicationResult)
375      (branch PrimitivePartial elaboratedPartial . unsupportedApplicationResult)
376      (branch
377        UnboundVariable
378        unboundSpelling
379        .
380        (constructor ClosedNaturalElaboration UnboundVariable unboundSpelling))
381      (branch
382        UnsupportedTerm
383        unsupportedCode
384        .
385        (constructor ClosedNaturalElaboration UnsupportedTerm unsupportedCode))))
386
387def completeBytesCons =
388  (lambda unrestricted head : Byte .
389    (lambda unrestricted right : (family ClosedNaturalElaboration) .
390      (eliminate
391        ClosedNaturalElaboration
392        (lambda unrestricted value : (family ClosedNaturalElaboration) .
393          (family ClosedNaturalElaboration))
394        right
395        (branch NaturalElaborated elaboratedNatural . unsupportedApplicationResult)
396        (branch
397          BytesElaborated
398          elaboratedBytes
399          .
400          (constructor ClosedNaturalElaboration BytesElaborated (bytes-cons head elaboratedBytes)))
401        (branch ByteElaborated elaboratedByte . unsupportedApplicationResult)
402        (branch PrimitivePartial elaboratedPartial . unsupportedApplicationResult)
403        (branch
404          UnboundVariable
405          unboundSpelling
406          .
407          (constructor ClosedNaturalElaboration UnboundVariable unboundSpelling))
408        (branch
409          UnsupportedTerm
410          unsupportedCode
411          .
412          (constructor ClosedNaturalElaboration UnsupportedTerm unsupportedCode)))))
413
414def completeBytesAppend =
415  (lambda unrestricted left : Bytes .
416    (lambda unrestricted right : (family ClosedNaturalElaboration) .
417      (eliminate
418        ClosedNaturalElaboration
419        (lambda unrestricted value : (family ClosedNaturalElaboration) .
420          (family ClosedNaturalElaboration))
421        right
422        (branch NaturalElaborated elaboratedNatural . unsupportedApplicationResult)
423        (branch
424          BytesElaborated
425          elaboratedBytes
426          .
427          (constructor ClosedNaturalElaboration BytesElaborated (bytes-append left elaboratedBytes)))
428        (branch ByteElaborated elaboratedByte . unsupportedApplicationResult)
429        (branch PrimitivePartial elaboratedPartial . unsupportedApplicationResult)
430        (branch
431          UnboundVariable
432          unboundSpelling
433          .
434          (constructor ClosedNaturalElaboration UnboundVariable unboundSpelling))
435        (branch
436          UnsupportedTerm
437          unsupportedCode
438          .
439          (constructor ClosedNaturalElaboration UnsupportedTerm unsupportedCode)))))
440
441def choosePrimitiveElaboration =
442  (lambda unrestricted matched : Nat .
443    (lambda unrestricted selected : (family ClosedNaturalElaboration) .
444      (lambda unrestricted fallback : (family ClosedNaturalElaboration) .
445        (nat-eliminate
446          (lambda unrestricted value : Nat . (family ClosedNaturalElaboration))
447          fallback
448          (lambda unrestricted predecessor : Nat .
449            (lambda unrestricted induction : (family ClosedNaturalElaboration) . selected))
450          matched))))
451
452def selectPrimitiveBySpelling =
453  (lambda unrestricted sourceSpelling : Bytes .
454    (lambda unrestricted candidateSpelling : Bytes .
455      (lambda unrestricted selected : (family ClosedNaturalElaboration) .
456        (lambda unrestricted fallback : (family ClosedNaturalElaboration) .
457          (choosePrimitiveElaboration
458            (bytesEqual sourceSpelling candidateSpelling)
459            selected
460            fallback)))))
461
462def chooseBytesAppendApplication =
463  (lambda unrestricted spelling : Bytes .
464    (lambda unrestricted argument : (family ClosedNaturalElaboration) .
465      (selectPrimitiveBySpelling
466        spelling
467        bytesAppendSpelling
468        (beginBytesAppend argument)
469        unsupportedApplicationResult)))
470
471def chooseBytesConsApplication =
472  (lambda unrestricted spelling : Bytes .
473    (lambda unrestricted argument : (family ClosedNaturalElaboration) .
474      (selectPrimitiveBySpelling
475        spelling
476        bytesConsSpelling
477        (beginBytesCons argument)
478        (chooseBytesAppendApplication spelling argument))))
479
480def chooseNaturalLessApplication =
481  (lambda unrestricted spelling : Bytes .
482    (lambda unrestricted argument : (family ClosedNaturalElaboration) .
483      (selectPrimitiveBySpelling
484        spelling
485        naturalLessThanSpelling
486        (beginNaturalLessThan argument)
487        (chooseBytesConsApplication spelling argument))))
488
489def chooseByteLessApplication =
490  (lambda unrestricted spelling : Bytes .
491    (lambda unrestricted argument : (family ClosedNaturalElaboration) .
492      (selectPrimitiveBySpelling
493        spelling
494        byteLessThanSpelling
495        (beginByteComparison (succ zero) argument)
496        (chooseNaturalLessApplication spelling argument))))
497
498def chooseByteEqualApplication =
499  (lambda unrestricted spelling : Bytes .
500    (lambda unrestricted argument : (family ClosedNaturalElaboration) .
501      (selectPrimitiveBySpelling
502        spelling
503        byteEqualSpelling
504        (beginByteComparison zero argument)
505        (chooseByteLessApplication spelling argument))))
506
507def chooseBytesLengthApplication =
508  (lambda unrestricted spelling : Bytes .
509    (lambda unrestricted argument : (family ClosedNaturalElaboration) .
510      (selectPrimitiveBySpelling
511        spelling
512        bytesLengthSpelling
513        (elaborateBytesLengthArgument argument)
514        (chooseByteEqualApplication spelling argument))))
515
516def chooseNaturalToByteApplication =
517  (lambda unrestricted spelling : Bytes .
518    (lambda unrestricted argument : (family ClosedNaturalElaboration) .
519      (selectPrimitiveBySpelling
520        spelling
521        naturalToByteSpelling
522        (elaborateNaturalToByteArgument argument)
523        (chooseBytesLengthApplication spelling argument))))
524
525def chooseByteToNaturalApplication =
526  (lambda unrestricted spelling : Bytes .
527    (lambda unrestricted argument : (family ClosedNaturalElaboration) .
528      (selectPrimitiveBySpelling
529        spelling
530        byteToNaturalSpelling
531        (elaborateByteToNaturalArgument argument)
532        (chooseNaturalToByteApplication spelling argument))))
533
534def elaboratePrimitiveApplication =
535  (lambda unrestricted spelling : Bytes .
536    (lambda unrestricted argument : (family ClosedNaturalElaboration) .
537      (selectPrimitiveBySpelling
538        spelling
539        successorSpelling
540        (elaborateSuccessorArgument argument)
541        (chooseByteToNaturalApplication spelling argument))))
542
543def applyElaboratedFunction =
544  (lambda unrestricted function : (family ClosedNaturalElaboration) .
545    (lambda unrestricted argument : (family ClosedNaturalElaboration) .
546      (eliminate
547        ClosedNaturalElaboration
548        (lambda unrestricted value : (family ClosedNaturalElaboration) .
549          (family ClosedNaturalElaboration))
550        function
551        (branch NaturalElaborated elaboratedNatural . unsupportedApplicationResult)
552        (branch BytesElaborated elaboratedBytes . unsupportedApplicationResult)
553        (branch ByteElaborated elaboratedByte . unsupportedApplicationResult)
554        (branch
555          PrimitivePartial
556          elaboratedPartial
557          .
558          (eliminate
559            PartialPrimitive
560            (lambda unrestricted value : (family PartialPrimitive) .
561              (family ClosedNaturalElaboration))
562            elaboratedPartial
563            (branch
564              PartialByteComparison
565              partialComparisonOperation
566              partialComparisonLeft
567              .
568              (elaborateByteComparisonValue
569                partialComparisonOperation
570                partialComparisonLeft
571                argument))
572            (branch
573              PartialNaturalLessThan
574              partialNaturalLeft
575              .
576              (elaborateNaturalLessThanValue partialNaturalLeft argument))
577            (branch PartialBytesCons partialConsHead . (completeBytesCons partialConsHead argument))
578            (branch
579              PartialBytesAppend
580              partialAppendLeft
581              .
582              (completeBytesAppend partialAppendLeft argument))))
583        (branch
584          UnboundVariable
585          unboundSpelling
586          .
587          (constructor ClosedNaturalElaboration UnboundVariable unboundSpelling))
588        (branch
589          UnsupportedTerm
590          unsupportedCode
591          .
592          (constructor ClosedNaturalElaboration UnsupportedTerm unsupportedCode)))))
593
594-- Part of `elaborateClosedNatural`, lifted out to keep it inside the §28.3 size and
595-- nesting limits; the parameters are the locals it still needs.
596def elaborateClosedNaturalPart1 =
597  (lambda unrestricted function : (family Term) .
598    (lambda unrestricted ih_function : (family ClosedNaturalElaboration) .
599      (lambda unrestricted ih_argument : (family ClosedNaturalElaboration) .
600        (eliminate
601          Term
602          (lambda unrestricted value : (family Term) . (family ClosedNaturalElaboration))
603          function
604          (branch Variable spelling . (elaboratePrimitiveApplication spelling ih_argument))
605          (branch Universe level . (applyElaboratedFunction ih_function ih_argument))
606          (branch NaturalType . (applyElaboratedFunction ih_function ih_argument))
607          (branch NaturalZero . (applyElaboratedFunction ih_function ih_argument))
608          (branch
609            NaturalLiteral
610            naturalLiteralValue
611            .
612            (applyElaboratedFunction ih_function ih_argument))
613          (branch
614            NaturalSuccessor
615            predecessor
616            ih_predecessor
617            .
618            (applyElaboratedFunction ih_function ih_argument))
619          (branch
620            Application
621            nestedFunction
622            nestedArgument
623            ih_nestedFunction
624            ih_nestedArgument
625            .
626            (applyElaboratedFunction ih_function ih_argument))
627          (branch
628            NaturalArithmetic
629            operation
630            nestedFunction
631            nestedArgument
632            ih_nestedFunction
633            ih_nestedArgument
634            .
635            unsupportedApplicationResult)
636          (branch
637            Lambda
638            quantityTag
639            binderSpelling
640            domain
641            body
642            ih_domain
643            ih_body
644            .
645            (applyElaboratedFunction ih_function ih_argument))
646          (branch
647            Pi
648            quantityTag
649            binderSpelling
650            domain
651            codomain
652            ih_domain
653            ih_codomain
654            .
655            (applyElaboratedFunction ih_function ih_argument))
656          (branch BytesType . (applyElaboratedFunction ih_function ih_argument))
657          (branch BytesLiteral bytesValue . (applyElaboratedFunction ih_function ih_argument))
658          (branch ByteType . (applyElaboratedFunction ih_function ih_argument))
659          (branch ByteLiteral byteValue . (applyElaboratedFunction ih_function ih_argument))
660          (branch TermSequenceEnd . (applyElaboratedFunction ih_function ih_argument))
661          (branch
662            TermSequenceNext
663            sequenceHead
664            sequenceTail
665            ih_sequenceHead
666            ih_sequenceTail
667            .
668            (applyElaboratedFunction ih_function ih_argument))
669          (branch
670            TermEliminatorBranch
671            constructorSpelling
672            binderNames
673            body
674            ih_binderNames
675            ih_body
676            .
677            (applyElaboratedFunction ih_function ih_argument))
678          (branch
679            FamilyApplication
680            familySpelling
681            familyArguments
682            ih_familyArguments
683            .
684            (applyElaboratedFunction ih_function ih_argument))
685          (branch
686            ConstructorApplication
687            familySpelling
688            constructorSpelling
689            constructorArguments
690            ih_constructorArguments
691            .
692            (applyElaboratedFunction ih_function ih_argument))
693          (branch
694            Eliminator
695            eliminatedFamilySpelling
696            motive
697            scrutinee
698            branches
699            ih_motive
700            ih_scrutinee
701            ih_branches
702            .
703            (applyElaboratedFunction ih_function ih_argument))
704          (branch
705            Match
706            family
707            scrutinee
708            branches
709            ih_scrutinee
710            ih_branches
711            .
712            (applyElaboratedFunction ih_function ih_argument))
713          (branch
714            MatchWith
715            family
716            motive
717            scrutinee
718            branches
719            ih_motive
720            ih_scrutinee
721            ih_branches
722            .
723            (applyElaboratedFunction ih_function ih_argument))
724          (branch IntegerLiteral spelling . (applyElaboratedFunction ih_function ih_argument))
725          (branch
726            RecordConstruction
727            name
728            origin
729            bindings
730            ih_bindings
731            .
732            (applyElaboratedFunction ih_function ih_argument))
733          (branch
734            RecordAssignment
735            name
736            origin
737            value
738            ih_value
739            .
740            (applyElaboratedFunction ih_function ih_argument))
741          (branch
742            RecordProjection
743            name
744            field
745            origin
746            value
747            ih_value
748            .
749            (applyElaboratedFunction ih_function ih_argument))
750          (branch
751            RecordUpdate
752            name
753            origin
754            value
755            bindings
756            ih_value
757            ih_bindings
758            .
759            (applyElaboratedFunction ih_function ih_argument))
760          (branch
761            LocalLet
762            quantity
763            binder
764            hasAnnotation
765            annotation
766            value
767            body
768            ih_annotation
769            ih_value
770            ih_body
771            .
772            (applyElaboratedFunction ih_function ih_argument))
773          (branch
774            DoBlock
775            effects
776            result
777            body
778            ih_effects
779            ih_result
780            ih_body
781            .
782            (applyElaboratedFunction ih_function ih_argument))
783          (branch
784            DoStep
785            named
786            quantity
787            binder
788            computation
789            continuation
790            ih_computation
791            ih_continuation
792            .
793            (applyElaboratedFunction ih_function ih_argument))
794          (branch DoReturn value ih_value . (applyElaboratedFunction ih_function ih_argument))))))
795
796def elaborateClosedNatural =
797  (lambda unrestricted term : (family Term) .
798    (eliminate
799      Term
800      (lambda unrestricted value : (family Term) . (family ClosedNaturalElaboration))
801      term
802      (branch Variable spelling . (constructor ClosedNaturalElaboration UnboundVariable spelling))
803      (branch Universe level . (constructor ClosedNaturalElaboration UnsupportedTerm (succ zero)))
804      (branch
805        NaturalType
806        .
807        (constructor ClosedNaturalElaboration UnsupportedTerm (succ (succ zero))))
808      (branch
809        NaturalZero
810        .
811        (constructor
812          ClosedNaturalElaboration
813          NaturalElaborated
814          (constructor ClosedNatural ClosedZero)))
815      (branch
816        NaturalLiteral
817        naturalLiteralValue
818        .
819        (constructor
820          ClosedNaturalElaboration
821          NaturalElaborated
822          (closeNaturalLiteral naturalLiteralValue)))
823      (branch
824        NaturalSuccessor
825        predecessor
826        ih_predecessor
827        .
828        (eliminate
829          ClosedNaturalElaboration
830          (lambda unrestricted result : (family ClosedNaturalElaboration) .
831            (family ClosedNaturalElaboration))
832          ih_predecessor
833          (branch
834            NaturalElaborated
835            elaboratedNatural
836            .
837            (constructor
838              ClosedNaturalElaboration
839              NaturalElaborated
840              (constructor ClosedNatural ClosedSuccessor elaboratedNatural)))
841          (branch
842            BytesElaborated
843            elaboratedBytes
844            .
845            (constructor
846              ClosedNaturalElaboration
847              UnsupportedTerm
848              (succ (succ (succ (succ (succ (succ zero))))))))
849          (branch
850            ByteElaborated
851            elaboratedByte
852            .
853            (constructor
854              ClosedNaturalElaboration
855              UnsupportedTerm
856              (succ (succ (succ (succ (succ (succ (succ (succ zero))))))))))
857          (branch PrimitivePartial elaboratedPartial . unsupportedApplicationResult)
858          (branch
859            UnboundVariable
860            unboundSpelling
861            .
862            (constructor ClosedNaturalElaboration UnboundVariable unboundSpelling))
863          (branch
864            UnsupportedTerm
865            unsupportedCode
866            .
867            (constructor ClosedNaturalElaboration UnsupportedTerm unsupportedCode))))
868      (branch
869        Application
870        function
871        argument
872        ih_function
873        ih_argument
874        .
875        (elaborateClosedNaturalPart1 function ih_function ih_argument))
876      (branch
877        NaturalArithmetic
878        operation
879        function
880        argument
881        ih_function
882        ih_argument
883        .
884        unsupportedApplicationResult)
885      (branch
886        Lambda
887        quantityTag
888        binderSpelling
889        domain
890        body
891        ih_domain
892        ih_body
893        .
894        (constructor ClosedNaturalElaboration UnsupportedTerm (succ (succ (succ (succ zero))))))
895      (branch
896        Pi
897        quantityTag
898        binderSpelling
899        domain
900        codomain
901        ih_domain
902        ih_codomain
903        .
904        (constructor ClosedNaturalElaboration UnsupportedTerm (succ (succ (succ (succ zero))))))
905      (branch
906        BytesType
907        .
908        (constructor
909          ClosedNaturalElaboration
910          UnsupportedTerm
911          (succ (succ (succ (succ (succ zero)))))))
912      (branch
913        BytesLiteral
914        bytesValue
915        .
916        (constructor ClosedNaturalElaboration BytesElaborated bytesValue))
917      (branch
918        ByteType
919        .
920        (constructor
921          ClosedNaturalElaboration
922          UnsupportedTerm
923          (succ (succ (succ (succ (succ (succ (succ zero)))))))))
924      (branch
925        ByteLiteral
926        byteValue
927        .
928        (constructor ClosedNaturalElaboration ByteElaborated byteValue))
929      (branch
930        TermSequenceEnd
931        .
932        (constructor
933          ClosedNaturalElaboration
934          UnsupportedTerm
935          (succ (succ (succ (succ (succ (succ (succ (succ (succ zero)))))))))))
936      (branch
937        TermSequenceNext
938        sequenceHead
939        sequenceTail
940        ih_sequenceHead
941        ih_sequenceTail
942        .
943        (constructor
944          ClosedNaturalElaboration
945          UnsupportedTerm
946          (succ (succ (succ (succ (succ (succ (succ (succ (succ zero)))))))))))
947      (branch
948        TermEliminatorBranch
949        constructorSpelling
950        binderNames
951        body
952        ih_binderNames
953        ih_body
954        .
955        (constructor
956          ClosedNaturalElaboration
957          UnsupportedTerm
958          (succ (succ (succ (succ (succ (succ (succ (succ (succ zero)))))))))))
959      (branch
960        FamilyApplication
961        familySpelling
962        familyArguments
963        ih_familyArguments
964        .
965        (constructor
966          ClosedNaturalElaboration
967          UnsupportedTerm
968          (succ (succ (succ (succ (succ (succ (succ (succ (succ zero)))))))))))
969      (branch
970        ConstructorApplication
971        familySpelling
972        constructorSpelling
973        constructorArguments
974        ih_constructorArguments
975        .
976        (constructor
977          ClosedNaturalElaboration
978          UnsupportedTerm
979          (succ (succ (succ (succ (succ (succ (succ (succ (succ zero)))))))))))
980      (branch
981        Eliminator
982        eliminatedFamilySpelling
983        motive
984        scrutinee
985        branches
986        ih_motive
987        ih_scrutinee
988        ih_branches
989        .
990        (constructor
991          ClosedNaturalElaboration
992          UnsupportedTerm
993          (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ zero))))))))))))
994      (branch
995        Match
996        family
997        scrutinee
998        branches
999        ih_scrutinee
1000        ih_branches
1001        .
1002        (constructor ClosedNaturalElaboration UnsupportedTerm (succ zero)))
1003      (branch
1004        MatchWith
1005        family
1006        motive
1007        scrutinee
1008        branches
1009        ih_motive
1010        ih_scrutinee
1011        ih_branches
1012        .
1013        (constructor ClosedNaturalElaboration UnsupportedTerm (succ zero)))
1014      (branch
1015        IntegerLiteral
1016        spelling
1017        .
1018        (eliminate
1019          NaturalTermResult
1020          (lambda unrestricted result : (family NaturalTermResult) .
1021            (family ClosedNaturalElaboration))
1022          (Compiler.Parser/naturalValueFromTerm (constructor Term IntegerLiteral spelling))
1023          (branch
1024            NaturalTermDecoded
1025            value
1026            .
1027            (constructor ClosedNaturalElaboration NaturalElaborated (closeNaturalLiteral value)))
1028          (branch
1029            NotNaturalTerm
1030            .
1031            (constructor ClosedNaturalElaboration UnsupportedTerm (succ zero)))))
1032      (branch
1033        RecordConstruction
1034        name
1035        origin
1036        bindings
1037        ih_bindings
1038        .
1039        (constructor ClosedNaturalElaboration UnsupportedTerm (succ zero)))
1040      (branch
1041        RecordAssignment
1042        name
1043        origin
1044        value
1045        ih_value
1046        .
1047        (constructor ClosedNaturalElaboration UnsupportedTerm (succ zero)))
1048      (branch
1049        RecordProjection
1050        name
1051        field
1052        origin
1053        value
1054        ih_value
1055        .
1056        (constructor ClosedNaturalElaboration UnsupportedTerm (succ zero)))
1057      (branch
1058        RecordUpdate
1059        name
1060        origin
1061        value
1062        bindings
1063        ih_value
1064        ih_bindings
1065        .
1066        (constructor ClosedNaturalElaboration UnsupportedTerm (succ zero)))
1067      (branch
1068        LocalLet
1069        quantity
1070        binder
1071        hasAnnotation
1072        annotation
1073        value
1074        body
1075        ih_annotation
1076        ih_value
1077        ih_body
1078        .
1079        (constructor ClosedNaturalElaboration UnsupportedTerm (succ zero)))
1080      (branch
1081        DoBlock
1082        effects
1083        result
1084        body
1085        ih_effects
1086        ih_result
1087        ih_body
1088        .
1089        (constructor ClosedNaturalElaboration UnsupportedTerm (succ zero)))
1090      (branch
1091        DoStep
1092        named
1093        quantity
1094        binder
1095        computation
1096        continuation
1097        ih_computation
1098        ih_continuation
1099        .
1100        (constructor ClosedNaturalElaboration UnsupportedTerm (succ zero)))
1101      (branch
1102        DoReturn
1103        value
1104        ih_value
1105        .
1106        (constructor ClosedNaturalElaboration UnsupportedTerm (succ zero)))))
1107
1108def elaboratedParserSample : (family ClosedNaturalElaboration) =
1109  (elaborateClosedNatural parserSample)
1110
1111def elaborationFingerprint : Nat =
1112  (eliminate
1113    ClosedNaturalElaboration
1114    (lambda unrestricted result : (family ClosedNaturalElaboration) . Nat)
1115    elaboratedParserSample
1116    (branch
1117      NaturalElaborated
1118      elaboratedNatural
1119      .
1120      (eliminate
1121        ClosedNatural
1122        (lambda unrestricted value : (family ClosedNatural) . Nat)
1123        elaboratedNatural
1124        (branch
1125          ClosedZero
1126          .
1127          (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ zero))))))))))))
1128        (branch
1129          ClosedSuccessor
1130          closedPredecessor
1131          ih_closedPredecessor
1132          .
1133          (succ ih_closedPredecessor))))
1134    (branch BytesElaborated elaboratedBytes . (bytes-length elaboratedBytes))
1135    (branch ByteElaborated elaboratedByte . (byte-to-nat elaboratedByte))
1136    (branch PrimitivePartial elaboratedPartial . zero)
1137    (branch UnboundVariable unboundSpelling . zero)
1138    (branch UnsupportedTerm unsupportedCode . zero))