module Compiler.Elaborator

import Compiler.AST
import Compiler.Lexer
import Compiler.Parser

family ClosedNatural : Type 0
constructor ClosedZero
constructor ClosedSuccessor
recursive unrestricted closedPredecessor

end-family

family PartialPrimitive : Type 0
constructor PartialByteComparison
field unrestricted partialComparisonOperation : Nat
field unrestricted partialComparisonLeft : Byte
constructor PartialNaturalLessThan
field unrestricted partialNaturalLeft : (family ClosedNatural)
constructor PartialBytesCons
field unrestricted partialConsHead : Byte
constructor PartialBytesAppend
field unrestricted partialAppendLeft : Bytes

end-family

family ClosedNaturalElaboration : Type 0
constructor NaturalElaborated
field unrestricted elaboratedNatural : (family ClosedNatural)
constructor BytesElaborated
field unrestricted elaboratedBytes : Bytes
constructor ByteElaborated
field unrestricted elaboratedByte : Byte
constructor PrimitivePartial
field unrestricted elaboratedPartial : (family PartialPrimitive)
constructor UnboundVariable
field unrestricted unboundSpelling : Bytes
constructor UnsupportedTerm
field unrestricted unsupportedCode : Nat

end-family

def closeNaturalLiteral =
  (lambda unrestricted value : Nat .
    (nat-eliminate
      (lambda unrestricted remaining : Nat . (family ClosedNatural))
      (constructor ClosedNatural ClosedZero)
      (lambda unrestricted predecessor : Nat .
        (lambda unrestricted induction : (family ClosedNatural) .
          (constructor ClosedNatural ClosedSuccessor induction)))
      value))

def openClosedNatural =
  (lambda unrestricted value : (family ClosedNatural) .
    (eliminate
      ClosedNatural
      (lambda unrestricted remaining : (family ClosedNatural) . Nat)
      value
      (branch ClosedZero . zero)
      (branch ClosedSuccessor closedPredecessor ih_closedPredecessor . (succ ih_closedPredecessor))))

def byteToNaturalSpelling =
  b"byte-to-nat"

def naturalToByteSpelling =
  b"nat-to-byte"

def bytesLengthSpelling =
  b"bytes-length"

def byteEqualSpelling =
  b"byte-equal"

def byteLessThanSpelling =
  b"byte-less-than"

def naturalLessThanSpelling =
  b"nat-less-than"

def bytesAppendSpelling =
  b"bytes-append"

def unsupportedApplicationResult =
  (constructor ClosedNaturalElaboration UnsupportedTerm (succ (succ (succ zero))))

def elaborateSuccessorArgument =
  (lambda unrestricted result : (family ClosedNaturalElaboration) .
    (eliminate
      ClosedNaturalElaboration
      (lambda unrestricted value : (family ClosedNaturalElaboration) .
        (family ClosedNaturalElaboration))
      result
      (branch
        NaturalElaborated
        elaboratedNatural
        .
        (constructor
          ClosedNaturalElaboration
          NaturalElaborated
          (constructor ClosedNatural ClosedSuccessor elaboratedNatural)))
      (branch BytesElaborated elaboratedBytes . unsupportedApplicationResult)
      (branch ByteElaborated elaboratedByte . unsupportedApplicationResult)
      (branch PrimitivePartial elaboratedPartial . unsupportedApplicationResult)
      (branch
        UnboundVariable
        unboundSpelling
        .
        (constructor ClosedNaturalElaboration UnboundVariable unboundSpelling))
      (branch
        UnsupportedTerm
        unsupportedCode
        .
        (constructor ClosedNaturalElaboration UnsupportedTerm unsupportedCode))))

def elaborateByteToNaturalArgument =
  (lambda unrestricted result : (family ClosedNaturalElaboration) .
    (eliminate
      ClosedNaturalElaboration
      (lambda unrestricted value : (family ClosedNaturalElaboration) .
        (family ClosedNaturalElaboration))
      result
      (branch NaturalElaborated elaboratedNatural . unsupportedApplicationResult)
      (branch BytesElaborated elaboratedBytes . unsupportedApplicationResult)
      (branch
        ByteElaborated
        elaboratedByte
        .
        (constructor
          ClosedNaturalElaboration
          NaturalElaborated
          (closeNaturalLiteral (byte-to-nat elaboratedByte))))
      (branch PrimitivePartial elaboratedPartial . unsupportedApplicationResult)
      (branch
        UnboundVariable
        unboundSpelling
        .
        (constructor ClosedNaturalElaboration UnboundVariable unboundSpelling))
      (branch
        UnsupportedTerm
        unsupportedCode
        .
        (constructor ClosedNaturalElaboration UnsupportedTerm unsupportedCode))))

def elaborateNaturalToByteArgument =
  (lambda unrestricted result : (family ClosedNaturalElaboration) .
    (eliminate
      ClosedNaturalElaboration
      (lambda unrestricted value : (family ClosedNaturalElaboration) .
        (family ClosedNaturalElaboration))
      result
      (branch
        NaturalElaborated
        elaboratedNatural
        .
        (constructor
          ClosedNaturalElaboration
          ByteElaborated
          (nat-to-byte (openClosedNatural elaboratedNatural))))
      (branch BytesElaborated elaboratedBytes . unsupportedApplicationResult)
      (branch ByteElaborated elaboratedByte . unsupportedApplicationResult)
      (branch PrimitivePartial elaboratedPartial . unsupportedApplicationResult)
      (branch
        UnboundVariable
        unboundSpelling
        .
        (constructor ClosedNaturalElaboration UnboundVariable unboundSpelling))
      (branch
        UnsupportedTerm
        unsupportedCode
        .
        (constructor ClosedNaturalElaboration UnsupportedTerm unsupportedCode))))

def elaborateBytesLengthArgument =
  (lambda unrestricted result : (family ClosedNaturalElaboration) .
    (eliminate
      ClosedNaturalElaboration
      (lambda unrestricted value : (family ClosedNaturalElaboration) .
        (family ClosedNaturalElaboration))
      result
      (branch NaturalElaborated elaboratedNatural . unsupportedApplicationResult)
      (branch
        BytesElaborated
        elaboratedBytes
        .
        (constructor
          ClosedNaturalElaboration
          NaturalElaborated
          (closeNaturalLiteral (bytes-length elaboratedBytes))))
      (branch ByteElaborated elaboratedByte . unsupportedApplicationResult)
      (branch PrimitivePartial elaboratedPartial . unsupportedApplicationResult)
      (branch
        UnboundVariable
        unboundSpelling
        .
        (constructor ClosedNaturalElaboration UnboundVariable unboundSpelling))
      (branch
        UnsupportedTerm
        unsupportedCode
        .
        (constructor ClosedNaturalElaboration UnsupportedTerm unsupportedCode))))

def elaborateByteComparisonValue =
  (lambda unrestricted operation : Nat .
    (lambda unrestricted left : Byte .
      (lambda unrestricted right : (family ClosedNaturalElaboration) .
        (eliminate
          ClosedNaturalElaboration
          (lambda unrestricted value : (family ClosedNaturalElaboration) .
            (family ClosedNaturalElaboration))
          right
          (branch NaturalElaborated elaboratedNatural . unsupportedApplicationResult)
          (branch BytesElaborated elaboratedBytes . unsupportedApplicationResult)
          (branch
            ByteElaborated
            elaboratedByte
            .
            (constructor
              ClosedNaturalElaboration
              NaturalElaborated
              (closeNaturalLiteral
                (nat-eliminate
                  (lambda unrestricted selectedOperation : Nat . Nat)
                  (byte-equal left elaboratedByte)
                  (lambda unrestricted predecessor : Nat .
                    (lambda unrestricted induction : Nat . (byte-less-than left elaboratedByte)))
                  operation))))
          (branch PrimitivePartial elaboratedPartial . unsupportedApplicationResult)
          (branch
            UnboundVariable
            unboundSpelling
            .
            (constructor ClosedNaturalElaboration UnboundVariable unboundSpelling))
          (branch
            UnsupportedTerm
            unsupportedCode
            .
            (constructor ClosedNaturalElaboration UnsupportedTerm unsupportedCode))))))

def beginByteComparison =
  (lambda unrestricted operation : Nat .
    (lambda unrestricted left : (family ClosedNaturalElaboration) .
      (eliminate
        ClosedNaturalElaboration
        (lambda unrestricted value : (family ClosedNaturalElaboration) .
          (family ClosedNaturalElaboration))
        left
        (branch NaturalElaborated elaboratedNatural . unsupportedApplicationResult)
        (branch BytesElaborated elaboratedBytes . unsupportedApplicationResult)
        (branch
          ByteElaborated
          elaboratedByte
          .
          (constructor
            ClosedNaturalElaboration
            PrimitivePartial
            (constructor PartialPrimitive PartialByteComparison operation elaboratedByte)))
        (branch PrimitivePartial elaboratedPartial . unsupportedApplicationResult)
        (branch
          UnboundVariable
          unboundSpelling
          .
          (constructor ClosedNaturalElaboration UnboundVariable unboundSpelling))
        (branch
          UnsupportedTerm
          unsupportedCode
          .
          (constructor ClosedNaturalElaboration UnsupportedTerm unsupportedCode)))))

def elaborateNaturalLessThanValue =
  (lambda unrestricted left : (family ClosedNatural) .
    (lambda unrestricted right : (family ClosedNaturalElaboration) .
      (eliminate
        ClosedNaturalElaboration
        (lambda unrestricted value : (family ClosedNaturalElaboration) .
          (family ClosedNaturalElaboration))
        right
        (branch
          NaturalElaborated
          elaboratedNatural
          .
          (constructor
            ClosedNaturalElaboration
            NaturalElaborated
            (closeNaturalLiteral
              (nat-less-than (openClosedNatural left) (openClosedNatural elaboratedNatural)))))
        (branch BytesElaborated elaboratedBytes . unsupportedApplicationResult)
        (branch ByteElaborated elaboratedByte . unsupportedApplicationResult)
        (branch PrimitivePartial elaboratedPartial . unsupportedApplicationResult)
        (branch
          UnboundVariable
          unboundSpelling
          .
          (constructor ClosedNaturalElaboration UnboundVariable unboundSpelling))
        (branch
          UnsupportedTerm
          unsupportedCode
          .
          (constructor ClosedNaturalElaboration UnsupportedTerm unsupportedCode)))))

def beginNaturalLessThan =
  (lambda unrestricted left : (family ClosedNaturalElaboration) .
    (eliminate
      ClosedNaturalElaboration
      (lambda unrestricted value : (family ClosedNaturalElaboration) .
        (family ClosedNaturalElaboration))
      left
      (branch
        NaturalElaborated
        elaboratedNatural
        .
        (constructor
          ClosedNaturalElaboration
          PrimitivePartial
          (constructor PartialPrimitive PartialNaturalLessThan elaboratedNatural)))
      (branch BytesElaborated elaboratedBytes . unsupportedApplicationResult)
      (branch ByteElaborated elaboratedByte . unsupportedApplicationResult)
      (branch PrimitivePartial elaboratedPartial . unsupportedApplicationResult)
      (branch
        UnboundVariable
        unboundSpelling
        .
        (constructor ClosedNaturalElaboration UnboundVariable unboundSpelling))
      (branch
        UnsupportedTerm
        unsupportedCode
        .
        (constructor ClosedNaturalElaboration UnsupportedTerm unsupportedCode))))

def beginBytesCons =
  (lambda unrestricted left : (family ClosedNaturalElaboration) .
    (eliminate
      ClosedNaturalElaboration
      (lambda unrestricted value : (family ClosedNaturalElaboration) .
        (family ClosedNaturalElaboration))
      left
      (branch NaturalElaborated elaboratedNatural . unsupportedApplicationResult)
      (branch BytesElaborated elaboratedBytes . unsupportedApplicationResult)
      (branch
        ByteElaborated
        elaboratedByte
        .
        (constructor
          ClosedNaturalElaboration
          PrimitivePartial
          (constructor PartialPrimitive PartialBytesCons elaboratedByte)))
      (branch PrimitivePartial elaboratedPartial . unsupportedApplicationResult)
      (branch
        UnboundVariable
        unboundSpelling
        .
        (constructor ClosedNaturalElaboration UnboundVariable unboundSpelling))
      (branch
        UnsupportedTerm
        unsupportedCode
        .
        (constructor ClosedNaturalElaboration UnsupportedTerm unsupportedCode))))

def beginBytesAppend =
  (lambda unrestricted left : (family ClosedNaturalElaboration) .
    (eliminate
      ClosedNaturalElaboration
      (lambda unrestricted value : (family ClosedNaturalElaboration) .
        (family ClosedNaturalElaboration))
      left
      (branch NaturalElaborated elaboratedNatural . unsupportedApplicationResult)
      (branch
        BytesElaborated
        elaboratedBytes
        .
        (constructor
          ClosedNaturalElaboration
          PrimitivePartial
          (constructor PartialPrimitive PartialBytesAppend elaboratedBytes)))
      (branch ByteElaborated elaboratedByte . unsupportedApplicationResult)
      (branch PrimitivePartial elaboratedPartial . unsupportedApplicationResult)
      (branch
        UnboundVariable
        unboundSpelling
        .
        (constructor ClosedNaturalElaboration UnboundVariable unboundSpelling))
      (branch
        UnsupportedTerm
        unsupportedCode
        .
        (constructor ClosedNaturalElaboration UnsupportedTerm unsupportedCode))))

def completeBytesCons =
  (lambda unrestricted head : Byte .
    (lambda unrestricted right : (family ClosedNaturalElaboration) .
      (eliminate
        ClosedNaturalElaboration
        (lambda unrestricted value : (family ClosedNaturalElaboration) .
          (family ClosedNaturalElaboration))
        right
        (branch NaturalElaborated elaboratedNatural . unsupportedApplicationResult)
        (branch
          BytesElaborated
          elaboratedBytes
          .
          (constructor ClosedNaturalElaboration BytesElaborated (bytes-cons head elaboratedBytes)))
        (branch ByteElaborated elaboratedByte . unsupportedApplicationResult)
        (branch PrimitivePartial elaboratedPartial . unsupportedApplicationResult)
        (branch
          UnboundVariable
          unboundSpelling
          .
          (constructor ClosedNaturalElaboration UnboundVariable unboundSpelling))
        (branch
          UnsupportedTerm
          unsupportedCode
          .
          (constructor ClosedNaturalElaboration UnsupportedTerm unsupportedCode)))))

def completeBytesAppend =
  (lambda unrestricted left : Bytes .
    (lambda unrestricted right : (family ClosedNaturalElaboration) .
      (eliminate
        ClosedNaturalElaboration
        (lambda unrestricted value : (family ClosedNaturalElaboration) .
          (family ClosedNaturalElaboration))
        right
        (branch NaturalElaborated elaboratedNatural . unsupportedApplicationResult)
        (branch
          BytesElaborated
          elaboratedBytes
          .
          (constructor ClosedNaturalElaboration BytesElaborated (bytes-append left elaboratedBytes)))
        (branch ByteElaborated elaboratedByte . unsupportedApplicationResult)
        (branch PrimitivePartial elaboratedPartial . unsupportedApplicationResult)
        (branch
          UnboundVariable
          unboundSpelling
          .
          (constructor ClosedNaturalElaboration UnboundVariable unboundSpelling))
        (branch
          UnsupportedTerm
          unsupportedCode
          .
          (constructor ClosedNaturalElaboration UnsupportedTerm unsupportedCode)))))

def choosePrimitiveElaboration =
  (lambda unrestricted matched : Nat .
    (lambda unrestricted selected : (family ClosedNaturalElaboration) .
      (lambda unrestricted fallback : (family ClosedNaturalElaboration) .
        (nat-eliminate
          (lambda unrestricted value : Nat . (family ClosedNaturalElaboration))
          fallback
          (lambda unrestricted predecessor : Nat .
            (lambda unrestricted induction : (family ClosedNaturalElaboration) . selected))
          matched))))

def selectPrimitiveBySpelling =
  (lambda unrestricted sourceSpelling : Bytes .
    (lambda unrestricted candidateSpelling : Bytes .
      (lambda unrestricted selected : (family ClosedNaturalElaboration) .
        (lambda unrestricted fallback : (family ClosedNaturalElaboration) .
          (choosePrimitiveElaboration
            (bytesEqual sourceSpelling candidateSpelling)
            selected
            fallback)))))

def chooseBytesAppendApplication =
  (lambda unrestricted spelling : Bytes .
    (lambda unrestricted argument : (family ClosedNaturalElaboration) .
      (selectPrimitiveBySpelling
        spelling
        bytesAppendSpelling
        (beginBytesAppend argument)
        unsupportedApplicationResult)))

def chooseBytesConsApplication =
  (lambda unrestricted spelling : Bytes .
    (lambda unrestricted argument : (family ClosedNaturalElaboration) .
      (selectPrimitiveBySpelling
        spelling
        bytesConsSpelling
        (beginBytesCons argument)
        (chooseBytesAppendApplication spelling argument))))

def chooseNaturalLessApplication =
  (lambda unrestricted spelling : Bytes .
    (lambda unrestricted argument : (family ClosedNaturalElaboration) .
      (selectPrimitiveBySpelling
        spelling
        naturalLessThanSpelling
        (beginNaturalLessThan argument)
        (chooseBytesConsApplication spelling argument))))

def chooseByteLessApplication =
  (lambda unrestricted spelling : Bytes .
    (lambda unrestricted argument : (family ClosedNaturalElaboration) .
      (selectPrimitiveBySpelling
        spelling
        byteLessThanSpelling
        (beginByteComparison (succ zero) argument)
        (chooseNaturalLessApplication spelling argument))))

def chooseByteEqualApplication =
  (lambda unrestricted spelling : Bytes .
    (lambda unrestricted argument : (family ClosedNaturalElaboration) .
      (selectPrimitiveBySpelling
        spelling
        byteEqualSpelling
        (beginByteComparison zero argument)
        (chooseByteLessApplication spelling argument))))

def chooseBytesLengthApplication =
  (lambda unrestricted spelling : Bytes .
    (lambda unrestricted argument : (family ClosedNaturalElaboration) .
      (selectPrimitiveBySpelling
        spelling
        bytesLengthSpelling
        (elaborateBytesLengthArgument argument)
        (chooseByteEqualApplication spelling argument))))

def chooseNaturalToByteApplication =
  (lambda unrestricted spelling : Bytes .
    (lambda unrestricted argument : (family ClosedNaturalElaboration) .
      (selectPrimitiveBySpelling
        spelling
        naturalToByteSpelling
        (elaborateNaturalToByteArgument argument)
        (chooseBytesLengthApplication spelling argument))))

def chooseByteToNaturalApplication =
  (lambda unrestricted spelling : Bytes .
    (lambda unrestricted argument : (family ClosedNaturalElaboration) .
      (selectPrimitiveBySpelling
        spelling
        byteToNaturalSpelling
        (elaborateByteToNaturalArgument argument)
        (chooseNaturalToByteApplication spelling argument))))

def elaboratePrimitiveApplication =
  (lambda unrestricted spelling : Bytes .
    (lambda unrestricted argument : (family ClosedNaturalElaboration) .
      (selectPrimitiveBySpelling
        spelling
        successorSpelling
        (elaborateSuccessorArgument argument)
        (chooseByteToNaturalApplication spelling argument))))

def applyElaboratedFunction =
  (lambda unrestricted function : (family ClosedNaturalElaboration) .
    (lambda unrestricted argument : (family ClosedNaturalElaboration) .
      (eliminate
        ClosedNaturalElaboration
        (lambda unrestricted value : (family ClosedNaturalElaboration) .
          (family ClosedNaturalElaboration))
        function
        (branch NaturalElaborated elaboratedNatural . unsupportedApplicationResult)
        (branch BytesElaborated elaboratedBytes . unsupportedApplicationResult)
        (branch ByteElaborated elaboratedByte . unsupportedApplicationResult)
        (branch
          PrimitivePartial
          elaboratedPartial
          .
          (eliminate
            PartialPrimitive
            (lambda unrestricted value : (family PartialPrimitive) .
              (family ClosedNaturalElaboration))
            elaboratedPartial
            (branch
              PartialByteComparison
              partialComparisonOperation
              partialComparisonLeft
              .
              (elaborateByteComparisonValue
                partialComparisonOperation
                partialComparisonLeft
                argument))
            (branch
              PartialNaturalLessThan
              partialNaturalLeft
              .
              (elaborateNaturalLessThanValue partialNaturalLeft argument))
            (branch PartialBytesCons partialConsHead . (completeBytesCons partialConsHead argument))
            (branch
              PartialBytesAppend
              partialAppendLeft
              .
              (completeBytesAppend partialAppendLeft argument))))
        (branch
          UnboundVariable
          unboundSpelling
          .
          (constructor ClosedNaturalElaboration UnboundVariable unboundSpelling))
        (branch
          UnsupportedTerm
          unsupportedCode
          .
          (constructor ClosedNaturalElaboration UnsupportedTerm unsupportedCode)))))

-- Part of `elaborateClosedNatural`, lifted out to keep it inside the §28.3 size and
-- nesting limits; the parameters are the locals it still needs.
def elaborateClosedNaturalPart1 =
  (lambda unrestricted function : (family Term) .
    (lambda unrestricted ih_function : (family ClosedNaturalElaboration) .
      (lambda unrestricted ih_argument : (family ClosedNaturalElaboration) .
        (eliminate
          Term
          (lambda unrestricted value : (family Term) . (family ClosedNaturalElaboration))
          function
          (branch Variable spelling . (elaboratePrimitiveApplication spelling ih_argument))
          (branch Universe level . (applyElaboratedFunction ih_function ih_argument))
          (branch NaturalType . (applyElaboratedFunction ih_function ih_argument))
          (branch NaturalZero . (applyElaboratedFunction ih_function ih_argument))
          (branch
            NaturalLiteral
            naturalLiteralValue
            .
            (applyElaboratedFunction ih_function ih_argument))
          (branch
            NaturalSuccessor
            predecessor
            ih_predecessor
            .
            (applyElaboratedFunction ih_function ih_argument))
          (branch
            Application
            nestedFunction
            nestedArgument
            ih_nestedFunction
            ih_nestedArgument
            .
            (applyElaboratedFunction ih_function ih_argument))
          (branch
            NaturalArithmetic
            operation
            nestedFunction
            nestedArgument
            ih_nestedFunction
            ih_nestedArgument
            .
            unsupportedApplicationResult)
          (branch
            Lambda
            quantityTag
            binderSpelling
            domain
            body
            ih_domain
            ih_body
            .
            (applyElaboratedFunction ih_function ih_argument))
          (branch
            Pi
            quantityTag
            binderSpelling
            domain
            codomain
            ih_domain
            ih_codomain
            .
            (applyElaboratedFunction ih_function ih_argument))
          (branch BytesType . (applyElaboratedFunction ih_function ih_argument))
          (branch BytesLiteral bytesValue . (applyElaboratedFunction ih_function ih_argument))
          (branch ByteType . (applyElaboratedFunction ih_function ih_argument))
          (branch ByteLiteral byteValue . (applyElaboratedFunction ih_function ih_argument))
          (branch TermSequenceEnd . (applyElaboratedFunction ih_function ih_argument))
          (branch
            TermSequenceNext
            sequenceHead
            sequenceTail
            ih_sequenceHead
            ih_sequenceTail
            .
            (applyElaboratedFunction ih_function ih_argument))
          (branch
            TermEliminatorBranch
            constructorSpelling
            binderNames
            body
            ih_binderNames
            ih_body
            .
            (applyElaboratedFunction ih_function ih_argument))
          (branch
            FamilyApplication
            familySpelling
            familyArguments
            ih_familyArguments
            .
            (applyElaboratedFunction ih_function ih_argument))
          (branch
            ConstructorApplication
            familySpelling
            constructorSpelling
            constructorArguments
            ih_constructorArguments
            .
            (applyElaboratedFunction ih_function ih_argument))
          (branch
            Eliminator
            eliminatedFamilySpelling
            motive
            scrutinee
            branches
            ih_motive
            ih_scrutinee
            ih_branches
            .
            (applyElaboratedFunction ih_function ih_argument))
          (branch
            Match
            family
            scrutinee
            branches
            ih_scrutinee
            ih_branches
            .
            (applyElaboratedFunction ih_function ih_argument))
          (branch
            MatchWith
            family
            motive
            scrutinee
            branches
            ih_motive
            ih_scrutinee
            ih_branches
            .
            (applyElaboratedFunction ih_function ih_argument))
          (branch IntegerLiteral spelling . (applyElaboratedFunction ih_function ih_argument))
          (branch
            RecordConstruction
            name
            origin
            bindings
            ih_bindings
            .
            (applyElaboratedFunction ih_function ih_argument))
          (branch
            RecordAssignment
            name
            origin
            value
            ih_value
            .
            (applyElaboratedFunction ih_function ih_argument))
          (branch
            RecordProjection
            name
            field
            origin
            value
            ih_value
            .
            (applyElaboratedFunction ih_function ih_argument))
          (branch
            RecordUpdate
            name
            origin
            value
            bindings
            ih_value
            ih_bindings
            .
            (applyElaboratedFunction ih_function ih_argument))
          (branch
            LocalLet
            quantity
            binder
            hasAnnotation
            annotation
            value
            body
            ih_annotation
            ih_value
            ih_body
            .
            (applyElaboratedFunction ih_function ih_argument))
          (branch
            DoBlock
            effects
            result
            body
            ih_effects
            ih_result
            ih_body
            .
            (applyElaboratedFunction ih_function ih_argument))
          (branch
            DoStep
            named
            quantity
            binder
            computation
            continuation
            ih_computation
            ih_continuation
            .
            (applyElaboratedFunction ih_function ih_argument))
          (branch DoReturn value ih_value . (applyElaboratedFunction ih_function ih_argument))))))

def elaborateClosedNatural =
  (lambda unrestricted term : (family Term) .
    (eliminate
      Term
      (lambda unrestricted value : (family Term) . (family ClosedNaturalElaboration))
      term
      (branch Variable spelling . (constructor ClosedNaturalElaboration UnboundVariable spelling))
      (branch Universe level . (constructor ClosedNaturalElaboration UnsupportedTerm (succ zero)))
      (branch
        NaturalType
        .
        (constructor ClosedNaturalElaboration UnsupportedTerm (succ (succ zero))))
      (branch
        NaturalZero
        .
        (constructor
          ClosedNaturalElaboration
          NaturalElaborated
          (constructor ClosedNatural ClosedZero)))
      (branch
        NaturalLiteral
        naturalLiteralValue
        .
        (constructor
          ClosedNaturalElaboration
          NaturalElaborated
          (closeNaturalLiteral naturalLiteralValue)))
      (branch
        NaturalSuccessor
        predecessor
        ih_predecessor
        .
        (eliminate
          ClosedNaturalElaboration
          (lambda unrestricted result : (family ClosedNaturalElaboration) .
            (family ClosedNaturalElaboration))
          ih_predecessor
          (branch
            NaturalElaborated
            elaboratedNatural
            .
            (constructor
              ClosedNaturalElaboration
              NaturalElaborated
              (constructor ClosedNatural ClosedSuccessor elaboratedNatural)))
          (branch
            BytesElaborated
            elaboratedBytes
            .
            (constructor
              ClosedNaturalElaboration
              UnsupportedTerm
              (succ (succ (succ (succ (succ (succ zero))))))))
          (branch
            ByteElaborated
            elaboratedByte
            .
            (constructor
              ClosedNaturalElaboration
              UnsupportedTerm
              (succ (succ (succ (succ (succ (succ (succ (succ zero))))))))))
          (branch PrimitivePartial elaboratedPartial . unsupportedApplicationResult)
          (branch
            UnboundVariable
            unboundSpelling
            .
            (constructor ClosedNaturalElaboration UnboundVariable unboundSpelling))
          (branch
            UnsupportedTerm
            unsupportedCode
            .
            (constructor ClosedNaturalElaboration UnsupportedTerm unsupportedCode))))
      (branch
        Application
        function
        argument
        ih_function
        ih_argument
        .
        (elaborateClosedNaturalPart1 function ih_function ih_argument))
      (branch
        NaturalArithmetic
        operation
        function
        argument
        ih_function
        ih_argument
        .
        unsupportedApplicationResult)
      (branch
        Lambda
        quantityTag
        binderSpelling
        domain
        body
        ih_domain
        ih_body
        .
        (constructor ClosedNaturalElaboration UnsupportedTerm (succ (succ (succ (succ zero))))))
      (branch
        Pi
        quantityTag
        binderSpelling
        domain
        codomain
        ih_domain
        ih_codomain
        .
        (constructor ClosedNaturalElaboration UnsupportedTerm (succ (succ (succ (succ zero))))))
      (branch
        BytesType
        .
        (constructor
          ClosedNaturalElaboration
          UnsupportedTerm
          (succ (succ (succ (succ (succ zero)))))))
      (branch
        BytesLiteral
        bytesValue
        .
        (constructor ClosedNaturalElaboration BytesElaborated bytesValue))
      (branch
        ByteType
        .
        (constructor
          ClosedNaturalElaboration
          UnsupportedTerm
          (succ (succ (succ (succ (succ (succ (succ zero)))))))))
      (branch
        ByteLiteral
        byteValue
        .
        (constructor ClosedNaturalElaboration ByteElaborated byteValue))
      (branch
        TermSequenceEnd
        .
        (constructor
          ClosedNaturalElaboration
          UnsupportedTerm
          (succ (succ (succ (succ (succ (succ (succ (succ (succ zero)))))))))))
      (branch
        TermSequenceNext
        sequenceHead
        sequenceTail
        ih_sequenceHead
        ih_sequenceTail
        .
        (constructor
          ClosedNaturalElaboration
          UnsupportedTerm
          (succ (succ (succ (succ (succ (succ (succ (succ (succ zero)))))))))))
      (branch
        TermEliminatorBranch
        constructorSpelling
        binderNames
        body
        ih_binderNames
        ih_body
        .
        (constructor
          ClosedNaturalElaboration
          UnsupportedTerm
          (succ (succ (succ (succ (succ (succ (succ (succ (succ zero)))))))))))
      (branch
        FamilyApplication
        familySpelling
        familyArguments
        ih_familyArguments
        .
        (constructor
          ClosedNaturalElaboration
          UnsupportedTerm
          (succ (succ (succ (succ (succ (succ (succ (succ (succ zero)))))))))))
      (branch
        ConstructorApplication
        familySpelling
        constructorSpelling
        constructorArguments
        ih_constructorArguments
        .
        (constructor
          ClosedNaturalElaboration
          UnsupportedTerm
          (succ (succ (succ (succ (succ (succ (succ (succ (succ zero)))))))))))
      (branch
        Eliminator
        eliminatedFamilySpelling
        motive
        scrutinee
        branches
        ih_motive
        ih_scrutinee
        ih_branches
        .
        (constructor
          ClosedNaturalElaboration
          UnsupportedTerm
          (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ zero))))))))))))
      (branch
        Match
        family
        scrutinee
        branches
        ih_scrutinee
        ih_branches
        .
        (constructor ClosedNaturalElaboration UnsupportedTerm (succ zero)))
      (branch
        MatchWith
        family
        motive
        scrutinee
        branches
        ih_motive
        ih_scrutinee
        ih_branches
        .
        (constructor ClosedNaturalElaboration UnsupportedTerm (succ zero)))
      (branch
        IntegerLiteral
        spelling
        .
        (eliminate
          NaturalTermResult
          (lambda unrestricted result : (family NaturalTermResult) .
            (family ClosedNaturalElaboration))
          (Compiler.Parser/naturalValueFromTerm (constructor Term IntegerLiteral spelling))
          (branch
            NaturalTermDecoded
            value
            .
            (constructor ClosedNaturalElaboration NaturalElaborated (closeNaturalLiteral value)))
          (branch
            NotNaturalTerm
            .
            (constructor ClosedNaturalElaboration UnsupportedTerm (succ zero)))))
      (branch
        RecordConstruction
        name
        origin
        bindings
        ih_bindings
        .
        (constructor ClosedNaturalElaboration UnsupportedTerm (succ zero)))
      (branch
        RecordAssignment
        name
        origin
        value
        ih_value
        .
        (constructor ClosedNaturalElaboration UnsupportedTerm (succ zero)))
      (branch
        RecordProjection
        name
        field
        origin
        value
        ih_value
        .
        (constructor ClosedNaturalElaboration UnsupportedTerm (succ zero)))
      (branch
        RecordUpdate
        name
        origin
        value
        bindings
        ih_value
        ih_bindings
        .
        (constructor ClosedNaturalElaboration UnsupportedTerm (succ zero)))
      (branch
        LocalLet
        quantity
        binder
        hasAnnotation
        annotation
        value
        body
        ih_annotation
        ih_value
        ih_body
        .
        (constructor ClosedNaturalElaboration UnsupportedTerm (succ zero)))
      (branch
        DoBlock
        effects
        result
        body
        ih_effects
        ih_result
        ih_body
        .
        (constructor ClosedNaturalElaboration UnsupportedTerm (succ zero)))
      (branch
        DoStep
        named
        quantity
        binder
        computation
        continuation
        ih_computation
        ih_continuation
        .
        (constructor ClosedNaturalElaboration UnsupportedTerm (succ zero)))
      (branch
        DoReturn
        value
        ih_value
        .
        (constructor ClosedNaturalElaboration UnsupportedTerm (succ zero)))))

def elaboratedParserSample : (family ClosedNaturalElaboration) =
  (elaborateClosedNatural parserSample)

def elaborationFingerprint : Nat =
  (eliminate
    ClosedNaturalElaboration
    (lambda unrestricted result : (family ClosedNaturalElaboration) . Nat)
    elaboratedParserSample
    (branch
      NaturalElaborated
      elaboratedNatural
      .
      (eliminate
        ClosedNatural
        (lambda unrestricted value : (family ClosedNatural) . Nat)
        elaboratedNatural
        (branch
          ClosedZero
          .
          (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ zero))))))))))))
        (branch
          ClosedSuccessor
          closedPredecessor
          ih_closedPredecessor
          .
          (succ ih_closedPredecessor))))
    (branch BytesElaborated elaboratedBytes . (bytes-length elaboratedBytes))
    (branch ByteElaborated elaboratedByte . (byte-to-nat elaboratedByte))
    (branch PrimitivePartial elaboratedPartial . zero)
    (branch UnboundVariable unboundSpelling . zero)
    (branch UnsupportedTerm unsupportedCode . zero))