Compiler.Elaborator

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)))))