module Compiler.ApplicationBuilder

import Compiler.AST
import Compiler.DependentCore

family ApplicationBuilderError : Type 0
constructor ApplicationBuilderNoError
constructor ApplicationBuilderConstructorArityMismatch
field unrestricted applicationBuilderExpectedArity : Nat
field unrestricted applicationBuilderSuppliedArity : Nat
constructor ApplicationBuilderEmptyBinderName
constructor ApplicationBuilderBinderFreshnessExhausted
field unrestricted applicationBuilderFreshnessAttempts : Nat
constructor ApplicationBuilderHostParserForbidden
constructor ApplicationBuilderHostFallbackForbidden
end-family

family ApplicationBuilderTelemetry : Type 0
constructor ApplicationBuilderTelemetryValue
field unrestricted applicationBuilderRequestedArguments : Nat
field unrestricted applicationBuilderObservedArguments : Nat
field unrestricted applicationBuilderUnaryApplicationsEmitted : Nat
field unrestricted applicationBuilderConstructorChecks : Nat
field unrestricted applicationBuilderFreshnessProbes : Nat
field unrestricted applicationBuilderHostParserCalls : Nat
field unrestricted applicationBuilderHostFallbackCalls : Nat
field unrestricted applicationBuilderResultCode : Bytes
end-family

family ApplicationBuilderTermArguments : Type 0
constructor ApplicationBuilderTermArgumentsEnd
constructor ApplicationBuilderTermArgumentsNext
field unrestricted applicationBuilderTermArgument : (family Term)
recursive unrestricted applicationBuilderRemainingTermArguments
end-family

family ApplicationBuilderNamedCoreArguments : Type 0
constructor ApplicationBuilderNamedCoreArgumentsEnd
constructor ApplicationBuilderNamedCoreArgumentsNext
field unrestricted applicationBuilderNamedCoreArgument : (family NamedCoreTerm)
recursive unrestricted applicationBuilderRemainingNamedCoreArguments
end-family

family ApplicationBuilderCoreArguments : Type 0
constructor ApplicationBuilderCoreArgumentsEnd
constructor ApplicationBuilderCoreArgumentsNext
field unrestricted applicationBuilderCoreArgument : (family CoreTerm)
recursive unrestricted applicationBuilderRemainingCoreArguments
end-family

family TermApplicationBuildResult : Type 0
constructor TermApplicationBuilt
field unrestricted builtTermApplication : (family Term)
field unrestricted termApplicationBuildTelemetry : (family ApplicationBuilderTelemetry)
constructor TermApplicationRejected
field unrestricted rejectedTermApplicationError : (family ApplicationBuilderError)
field unrestricted rejectedTermApplicationTelemetry : (family ApplicationBuilderTelemetry)
end-family

family NamedCoreApplicationBuildResult : Type 0
constructor NamedCoreApplicationBuilt
field unrestricted builtNamedCoreApplication : (family NamedCoreTerm)
field unrestricted namedCoreApplicationBuildTelemetry : (family ApplicationBuilderTelemetry)
constructor NamedCoreApplicationRejected
field unrestricted rejectedNamedCoreApplicationError : (family ApplicationBuilderError)
field unrestricted rejectedNamedCoreApplicationTelemetry : (family ApplicationBuilderTelemetry)
end-family

family CoreApplicationBuildResult : Type 0
constructor CoreApplicationBuilt
field unrestricted builtCoreApplication : (family CoreTerm)
field unrestricted coreApplicationBuildTelemetry : (family ApplicationBuilderTelemetry)
constructor CoreApplicationRejected
field unrestricted rejectedCoreApplicationError : (family ApplicationBuilderError)
field unrestricted rejectedCoreApplicationTelemetry : (family ApplicationBuilderTelemetry)
end-family

family FreshBinderNameResult : Type 0
constructor FreshBinderNameBuilt
field unrestricted builtFreshBinderName : Bytes
field unrestricted builtFreshBinderProbes : Nat
constructor FreshBinderNameRejected
field unrestricted rejectedFreshBinderError : (family ApplicationBuilderError)
field unrestricted rejectedFreshBinderProbes : Nat
end-family

def applicationBuilderSuccessCode = b"APP-000"
def applicationBuilderArityCode = b"APP-001"
def applicationBuilderEmptyBinderCode = b"APP-002"
def applicationBuilderFreshnessCode = b"APP-003"
def applicationBuilderHostParserCode = b"APP-004"
def applicationBuilderHostFallbackCode = b"APP-005"

def applicationBuilderErrorStableCode :
  (pi unrestricted error : (family ApplicationBuilderError) . Bytes) =
  (lambda unrestricted error : (family ApplicationBuilderError) .
    (eliminate ApplicationBuilderError
      (lambda unrestricted value : (family ApplicationBuilderError) . Bytes)
      error
      (branch ApplicationBuilderNoError . applicationBuilderSuccessCode)
      (branch ApplicationBuilderConstructorArityMismatch expected supplied .
        applicationBuilderArityCode)
      (branch ApplicationBuilderEmptyBinderName .
        applicationBuilderEmptyBinderCode)
      (branch ApplicationBuilderBinderFreshnessExhausted attempts .
        applicationBuilderFreshnessCode)
      (branch ApplicationBuilderHostParserForbidden .
        applicationBuilderHostParserCode)
      (branch ApplicationBuilderHostFallbackForbidden .
        applicationBuilderHostFallbackCode)))

def applicationBuilderTelemetryFor :
  (pi unrestricted requested : Nat .
    (pi unrestricted observed : Nat .
      (pi unrestricted emitted : Nat .
        (pi unrestricted constructorChecks : Nat .
          (pi unrestricted freshnessProbes : Nat .
            (pi unrestricted resultCode : Bytes .
              (family ApplicationBuilderTelemetry))))))) =
  (lambda unrestricted requested : Nat .
    (lambda unrestricted observed : Nat .
      (lambda unrestricted emitted : Nat .
        (lambda unrestricted constructorChecks : Nat .
          (lambda unrestricted freshnessProbes : Nat .
            (lambda unrestricted resultCode : Bytes .
              (constructor ApplicationBuilderTelemetry
                ApplicationBuilderTelemetryValue
                requested
                observed
                emitted
                constructorChecks
                freshnessProbes
                zero
                zero
                resultCode)))))))

def applicationBuilderNativeOnly : Nat =
  (app
    (app coreNaturalAnd
      (app
        (app naturalEqual zero)
        zero))
    (app
      (app naturalEqual zero)
      zero))

def applicationBuilderApply :
  (pi unrestricted function : (family Term) .
    (pi unrestricted argument : (family Term) . (family Term))) =
  (lambda unrestricted function : (family Term) .
    (lambda unrestricted argument : (family Term) .
      (constructor Term Application function argument)))

def app2 :
  (pi unrestricted function : (family Term) .
    (pi unrestricted first : (family Term) .
      (pi unrestricted second : (family Term) . (family Term)))) =
  (lambda unrestricted function : (family Term) .
    (lambda unrestricted first : (family Term) .
      (lambda unrestricted second : (family Term) .
        (constructor Term Application
          (constructor Term Application function first)
          second))))

def app3 :
  (pi unrestricted function : (family Term) .
    (pi unrestricted first : (family Term) .
      (pi unrestricted second : (family Term) .
        (pi unrestricted third : (family Term) . (family Term))))) =
  (lambda unrestricted function : (family Term) .
    (lambda unrestricted first : (family Term) .
      (lambda unrestricted second : (family Term) .
        (lambda unrestricted third : (family Term) .
          (constructor Term Application
            (constructor Term Application
              (constructor Term Application function first)
              second)
            third)))))

def app4 :
  (pi unrestricted function : (family Term) .
    (pi unrestricted first : (family Term) .
      (pi unrestricted second : (family Term) .
        (pi unrestricted third : (family Term) .
          (pi unrestricted fourth : (family Term) . (family Term)))))) =
  (lambda unrestricted function : (family Term) .
    (lambda unrestricted first : (family Term) .
      (lambda unrestricted second : (family Term) .
        (lambda unrestricted third : (family Term) .
          (lambda unrestricted fourth : (family Term) .
            (constructor Term Application
              (constructor Term Application
                (constructor Term Application
                  (constructor Term Application function first)
                  second)
                third)
              fourth))))))

def appN :
  (pi unrestricted function : (family Term) .
    (pi unrestricted arguments : (family ApplicationBuilderTermArguments) .
      (family Term))) =
  (lambda unrestricted function : (family Term) .
    (lambda unrestricted arguments : (family ApplicationBuilderTermArguments) .
      (app
        (eliminate ApplicationBuilderTermArguments
          (lambda unrestricted value : (family ApplicationBuilderTermArguments) .
            (pi unrestricted accumulated : (family Term) . (family Term)))
          arguments
          (branch ApplicationBuilderTermArgumentsEnd .
            (lambda unrestricted accumulated : (family Term) . accumulated))
          (branch ApplicationBuilderTermArgumentsNext argument remaining induction .
            (lambda unrestricted accumulated : (family Term) .
              (app induction
                (constructor Term Application accumulated argument)))))
        function)))

def namedCoreApplicationBuilderApply :
  (pi unrestricted function : (family NamedCoreTerm) .
    (pi unrestricted argument : (family NamedCoreTerm) .
      (family NamedCoreTerm))) =
  (lambda unrestricted function : (family NamedCoreTerm) .
    (lambda unrestricted argument : (family NamedCoreTerm) .
      (constructor NamedCoreTerm NamedCoreApplication function argument)))

def namedCoreApp2 :
  (pi unrestricted function : (family NamedCoreTerm) .
    (pi unrestricted first : (family NamedCoreTerm) .
      (pi unrestricted second : (family NamedCoreTerm) .
        (family NamedCoreTerm)))) =
  (lambda unrestricted function : (family NamedCoreTerm) .
    (lambda unrestricted first : (family NamedCoreTerm) .
      (lambda unrestricted second : (family NamedCoreTerm) .
        (constructor NamedCoreTerm NamedCoreApplication
          (constructor NamedCoreTerm NamedCoreApplication function first)
          second))))

def namedCoreApp3 :
  (pi unrestricted function : (family NamedCoreTerm) .
    (pi unrestricted first : (family NamedCoreTerm) .
      (pi unrestricted second : (family NamedCoreTerm) .
        (pi unrestricted third : (family NamedCoreTerm) .
          (family NamedCoreTerm))))) =
  (lambda unrestricted function : (family NamedCoreTerm) .
    (lambda unrestricted first : (family NamedCoreTerm) .
      (lambda unrestricted second : (family NamedCoreTerm) .
        (lambda unrestricted third : (family NamedCoreTerm) .
          (constructor NamedCoreTerm NamedCoreApplication
            (constructor NamedCoreTerm NamedCoreApplication
              (constructor NamedCoreTerm NamedCoreApplication function first)
              second)
            third)))))

def namedCoreApp4 :
  (pi unrestricted function : (family NamedCoreTerm) .
    (pi unrestricted first : (family NamedCoreTerm) .
      (pi unrestricted second : (family NamedCoreTerm) .
        (pi unrestricted third : (family NamedCoreTerm) .
          (pi unrestricted fourth : (family NamedCoreTerm) .
            (family NamedCoreTerm)))))) =
  (lambda unrestricted function : (family NamedCoreTerm) .
    (lambda unrestricted first : (family NamedCoreTerm) .
      (lambda unrestricted second : (family NamedCoreTerm) .
        (lambda unrestricted third : (family NamedCoreTerm) .
          (lambda unrestricted fourth : (family NamedCoreTerm) .
            (constructor NamedCoreTerm NamedCoreApplication
              (constructor NamedCoreTerm NamedCoreApplication
                (constructor NamedCoreTerm NamedCoreApplication
                  (constructor NamedCoreTerm NamedCoreApplication function first)
                  second)
                third)
              fourth))))))

def namedCoreAppN :
  (pi unrestricted function : (family NamedCoreTerm) .
    (pi unrestricted arguments : (family ApplicationBuilderNamedCoreArguments) .
      (family NamedCoreTerm))) =
  (lambda unrestricted function : (family NamedCoreTerm) .
    (lambda unrestricted arguments : (family ApplicationBuilderNamedCoreArguments) .
      (app
        (eliminate ApplicationBuilderNamedCoreArguments
          (lambda unrestricted value : (family ApplicationBuilderNamedCoreArguments) .
            (pi unrestricted accumulated : (family NamedCoreTerm) .
              (family NamedCoreTerm)))
          arguments
          (branch ApplicationBuilderNamedCoreArgumentsEnd .
            (lambda unrestricted accumulated : (family NamedCoreTerm) . accumulated))
          (branch ApplicationBuilderNamedCoreArgumentsNext argument remaining induction .
            (lambda unrestricted accumulated : (family NamedCoreTerm) .
              (app induction
                (constructor NamedCoreTerm NamedCoreApplication
                  accumulated argument)))))
        function)))

def coreApplicationBuilderApply :
  (pi unrestricted function : (family CoreTerm) .
    (pi unrestricted argument : (family CoreTerm) . (family CoreTerm))) =
  (lambda unrestricted function : (family CoreTerm) .
    (lambda unrestricted argument : (family CoreTerm) .
      (constructor CoreTerm CoreApplication function argument)))

def coreApp2 :
  (pi unrestricted function : (family CoreTerm) .
    (pi unrestricted first : (family CoreTerm) .
      (pi unrestricted second : (family CoreTerm) . (family CoreTerm)))) =
  (lambda unrestricted function : (family CoreTerm) .
    (lambda unrestricted first : (family CoreTerm) .
      (lambda unrestricted second : (family CoreTerm) .
        (constructor CoreTerm CoreApplication
          (constructor CoreTerm CoreApplication function first)
          second))))

def coreApp3 :
  (pi unrestricted function : (family CoreTerm) .
    (pi unrestricted first : (family CoreTerm) .
      (pi unrestricted second : (family CoreTerm) .
        (pi unrestricted third : (family CoreTerm) . (family CoreTerm))))) =
  (lambda unrestricted function : (family CoreTerm) .
    (lambda unrestricted first : (family CoreTerm) .
      (lambda unrestricted second : (family CoreTerm) .
        (lambda unrestricted third : (family CoreTerm) .
          (constructor CoreTerm CoreApplication
            (constructor CoreTerm CoreApplication
              (constructor CoreTerm CoreApplication function first)
              second)
            third)))))

def coreApp4 :
  (pi unrestricted function : (family CoreTerm) .
    (pi unrestricted first : (family CoreTerm) .
      (pi unrestricted second : (family CoreTerm) .
        (pi unrestricted third : (family CoreTerm) .
          (pi unrestricted fourth : (family CoreTerm) . (family CoreTerm)))))) =
  (lambda unrestricted function : (family CoreTerm) .
    (lambda unrestricted first : (family CoreTerm) .
      (lambda unrestricted second : (family CoreTerm) .
        (lambda unrestricted third : (family CoreTerm) .
          (lambda unrestricted fourth : (family CoreTerm) .
            (constructor CoreTerm CoreApplication
              (constructor CoreTerm CoreApplication
                (constructor CoreTerm CoreApplication
                  (constructor CoreTerm CoreApplication function first)
                  second)
                third)
              fourth))))))

def coreAppN :
  (pi unrestricted function : (family CoreTerm) .
    (pi unrestricted arguments : (family ApplicationBuilderCoreArguments) .
      (family CoreTerm))) =
  (lambda unrestricted function : (family CoreTerm) .
    (lambda unrestricted arguments : (family ApplicationBuilderCoreArguments) .
      (app
        (eliminate ApplicationBuilderCoreArguments
          (lambda unrestricted value : (family ApplicationBuilderCoreArguments) .
            (pi unrestricted accumulated : (family CoreTerm) . (family CoreTerm)))
          arguments
          (branch ApplicationBuilderCoreArgumentsEnd .
            (lambda unrestricted accumulated : (family CoreTerm) . accumulated))
          (branch ApplicationBuilderCoreArgumentsNext argument remaining induction .
            (lambda unrestricted accumulated : (family CoreTerm) .
              (app induction
                (constructor CoreTerm CoreApplication accumulated argument)))))
        function)))

def applicationBuilderTermArgumentCount :
  (pi unrestricted arguments : (family ApplicationBuilderTermArguments) . Nat) =
  (lambda unrestricted arguments : (family ApplicationBuilderTermArguments) .
    (eliminate ApplicationBuilderTermArguments
      (lambda unrestricted value : (family ApplicationBuilderTermArguments) . Nat)
      arguments
      (branch ApplicationBuilderTermArgumentsEnd . zero)
      (branch ApplicationBuilderTermArgumentsNext argument remaining induction .
        (succ induction))))

def applicationBuilderNamedCoreArgumentCount :
  (pi unrestricted arguments : (family ApplicationBuilderNamedCoreArguments) . Nat) =
  (lambda unrestricted arguments : (family ApplicationBuilderNamedCoreArguments) .
    (eliminate ApplicationBuilderNamedCoreArguments
      (lambda unrestricted value : (family ApplicationBuilderNamedCoreArguments) . Nat)
      arguments
      (branch ApplicationBuilderNamedCoreArgumentsEnd . zero)
      (branch ApplicationBuilderNamedCoreArgumentsNext argument remaining induction .
        (succ induction))))

def applicationBuilderCoreArgumentCount :
  (pi unrestricted arguments : (family ApplicationBuilderCoreArguments) . Nat) =
  (lambda unrestricted arguments : (family ApplicationBuilderCoreArguments) .
    (eliminate ApplicationBuilderCoreArguments
      (lambda unrestricted value : (family ApplicationBuilderCoreArguments) . Nat)
      arguments
      (branch ApplicationBuilderCoreArgumentsEnd . zero)
      (branch ApplicationBuilderCoreArgumentsNext argument remaining induction .
        (succ induction))))

def applicationBuilderTermArgumentSequence :
  (pi unrestricted arguments : (family ApplicationBuilderTermArguments) .
    (family Term)) =
  (lambda unrestricted arguments : (family ApplicationBuilderTermArguments) .
    (eliminate ApplicationBuilderTermArguments
      (lambda unrestricted value : (family ApplicationBuilderTermArguments) .
        (family Term))
      arguments
      (branch ApplicationBuilderTermArgumentsEnd .
        (constructor Term TermSequenceEnd))
      (branch ApplicationBuilderTermArgumentsNext argument remaining induction .
        (constructor Term TermSequenceNext argument induction))))

def applicationBuilderNamedCoreArgumentSequence :
  (pi unrestricted arguments : (family ApplicationBuilderNamedCoreArguments) .
    (family NamedCoreTerm)) =
  (lambda unrestricted arguments : (family ApplicationBuilderNamedCoreArguments) .
    (eliminate ApplicationBuilderNamedCoreArguments
      (lambda unrestricted value : (family ApplicationBuilderNamedCoreArguments) .
        (family NamedCoreTerm))
      arguments
      (branch ApplicationBuilderNamedCoreArgumentsEnd .
        (constructor NamedCoreTerm NamedCoreTermSequenceEnd))
      (branch ApplicationBuilderNamedCoreArgumentsNext argument remaining induction .
        (constructor NamedCoreTerm NamedCoreTermSequenceNext argument induction))))

def applicationBuilderCoreArgumentSequence :
  (pi unrestricted arguments : (family ApplicationBuilderCoreArguments) .
    (family CoreTerm)) =
  (lambda unrestricted arguments : (family ApplicationBuilderCoreArguments) .
    (eliminate ApplicationBuilderCoreArguments
      (lambda unrestricted value : (family ApplicationBuilderCoreArguments) .
        (family CoreTerm))
      arguments
      (branch ApplicationBuilderCoreArgumentsEnd .
        (constructor CoreTerm CoreTermSequenceEnd))
      (branch ApplicationBuilderCoreArgumentsNext argument remaining induction .
        (constructor CoreTerm CoreTermSequenceNext argument induction))))

def buildAppN :
  (pi unrestricted function : (family Term) .
    (pi unrestricted arguments : (family ApplicationBuilderTermArguments) .
      (family TermApplicationBuildResult))) =
  (lambda unrestricted function : (family Term) .
    (lambda unrestricted arguments : (family ApplicationBuilderTermArguments) .
      (constructor TermApplicationBuildResult TermApplicationBuilt
        (app (app appN function) arguments)
        (constructor ApplicationBuilderTelemetry
          ApplicationBuilderTelemetryValue
          (app applicationBuilderTermArgumentCount arguments)
          (app applicationBuilderTermArgumentCount arguments)
          (app applicationBuilderTermArgumentCount arguments)
          zero
          zero
          zero
          zero
          applicationBuilderSuccessCode))))

def buildTermConstructorApplication :
  (pi unrestricted familyName : Bytes .
    (pi unrestricted constructorName : Bytes .
      (pi unrestricted expectedArity : Nat .
        (pi unrestricted arguments : (family ApplicationBuilderTermArguments) .
          (family TermApplicationBuildResult))))) =
  (lambda unrestricted familyName : Bytes .
    (lambda unrestricted constructorName : Bytes .
      (lambda unrestricted expectedArity : Nat .
        (lambda unrestricted arguments : (family ApplicationBuilderTermArguments) .
          (nat-eliminate
            (lambda unrestricted matched : Nat .
              (family TermApplicationBuildResult))
            (constructor TermApplicationBuildResult TermApplicationRejected
              (constructor ApplicationBuilderError
                ApplicationBuilderConstructorArityMismatch
                expectedArity
                (app applicationBuilderTermArgumentCount arguments))
              (constructor ApplicationBuilderTelemetry
                ApplicationBuilderTelemetryValue
                expectedArity
                (app applicationBuilderTermArgumentCount arguments)
                zero
                (succ zero)
                zero
                zero
                zero
                applicationBuilderArityCode))
            (lambda unrestricted predecessor : Nat .
              (lambda unrestricted induction : (family TermApplicationBuildResult) .
                (constructor TermApplicationBuildResult TermApplicationBuilt
                  (constructor Term ConstructorApplication
                    familyName
                    constructorName
                    (app applicationBuilderTermArgumentSequence arguments))
                  (constructor ApplicationBuilderTelemetry
                    ApplicationBuilderTelemetryValue
                    expectedArity
                    (app applicationBuilderTermArgumentCount arguments)
                    zero
                    (succ zero)
                    zero
                    zero
                    zero
                    applicationBuilderSuccessCode))))
            (app
              (app naturalEqual expectedArity)
              (app applicationBuilderTermArgumentCount arguments)))))))

def buildNamedCoreConstructorApplication :
  (pi unrestricted familyName : Bytes .
    (pi unrestricted constructorName : Bytes .
      (pi unrestricted expectedArity : Nat .
        (pi unrestricted arguments : (family ApplicationBuilderNamedCoreArguments) .
          (family NamedCoreApplicationBuildResult))))) =
  (lambda unrestricted familyName : Bytes .
    (lambda unrestricted constructorName : Bytes .
      (lambda unrestricted expectedArity : Nat .
        (lambda unrestricted arguments : (family ApplicationBuilderNamedCoreArguments) .
          (nat-eliminate
            (lambda unrestricted matched : Nat .
              (family NamedCoreApplicationBuildResult))
            (constructor NamedCoreApplicationBuildResult NamedCoreApplicationRejected
              (constructor ApplicationBuilderError
                ApplicationBuilderConstructorArityMismatch
                expectedArity
                (app applicationBuilderNamedCoreArgumentCount arguments))
              (constructor ApplicationBuilderTelemetry
                ApplicationBuilderTelemetryValue
                expectedArity
                (app applicationBuilderNamedCoreArgumentCount arguments)
                zero
                (succ zero)
                zero
                zero
                zero
                applicationBuilderArityCode))
            (lambda unrestricted predecessor : Nat .
              (lambda unrestricted induction : (family NamedCoreApplicationBuildResult) .
                (constructor NamedCoreApplicationBuildResult NamedCoreApplicationBuilt
                  (constructor NamedCoreTerm NamedCoreConstructorApplication
                    familyName
                    constructorName
                    (app applicationBuilderNamedCoreArgumentSequence arguments))
                  (constructor ApplicationBuilderTelemetry
                    ApplicationBuilderTelemetryValue
                    expectedArity
                    (app applicationBuilderNamedCoreArgumentCount arguments)
                    zero
                    (succ zero)
                    zero
                    zero
                    zero
                    applicationBuilderSuccessCode))))
            (app
              (app naturalEqual expectedArity)
              (app applicationBuilderNamedCoreArgumentCount arguments)))))))

def buildCoreConstructorApplication :
  (pi unrestricted familyName : Bytes .
    (pi unrestricted constructorName : Bytes .
      (pi unrestricted expectedArity : Nat .
        (pi unrestricted arguments : (family ApplicationBuilderCoreArguments) .
          (family CoreApplicationBuildResult))))) =
  (lambda unrestricted familyName : Bytes .
    (lambda unrestricted constructorName : Bytes .
      (lambda unrestricted expectedArity : Nat .
        (lambda unrestricted arguments : (family ApplicationBuilderCoreArguments) .
          (nat-eliminate
            (lambda unrestricted matched : Nat .
              (family CoreApplicationBuildResult))
            (constructor CoreApplicationBuildResult CoreApplicationRejected
              (constructor ApplicationBuilderError
                ApplicationBuilderConstructorArityMismatch
                expectedArity
                (app applicationBuilderCoreArgumentCount arguments))
              (constructor ApplicationBuilderTelemetry
                ApplicationBuilderTelemetryValue
                expectedArity
                (app applicationBuilderCoreArgumentCount arguments)
                zero
                (succ zero)
                zero
                zero
                zero
                applicationBuilderArityCode))
            (lambda unrestricted predecessor : Nat .
              (lambda unrestricted induction : (family CoreApplicationBuildResult) .
                (constructor CoreApplicationBuildResult CoreApplicationBuilt
                  (constructor CoreTerm CoreConstructorApplication
                    familyName
                    constructorName
                    (app applicationBuilderCoreArgumentSequence arguments))
                  (constructor ApplicationBuilderTelemetry
                    ApplicationBuilderTelemetryValue
                    expectedArity
                    (app applicationBuilderCoreArgumentCount arguments)
                    zero
                    (succ zero)
                    zero
                    zero
                    zero
                    applicationBuilderSuccessCode))))
            (app
              (app naturalEqual expectedArity)
              (app applicationBuilderCoreArgumentCount arguments)))))))

def applicationBuilderScopeDepth :
  (pi unrestricted scope : (family NameScope) . Nat) =
  (lambda unrestricted scope : (family NameScope) .
    (eliminate NameScope
      (lambda unrestricted value : (family NameScope) . Nat)
      scope
      (branch EmptyNameScope . zero)
      (branch NameScopeBinding identifier outer induction .
        (succ induction))))

def applicationBuilderScopeContains :
  (pi unrestricted scope : (family NameScope) .
    (pi unrestricted candidate : Bytes . Nat)) =
  (lambda unrestricted scope : (family NameScope) .
    (eliminate NameScope
      (lambda unrestricted value : (family NameScope) .
        (pi unrestricted candidate : Bytes . Nat))
      scope
      (branch EmptyNameScope .
        (lambda unrestricted candidate : Bytes . zero))
      (branch NameScopeBinding identifier outer induction .
        (lambda unrestricted candidate : Bytes .
          (nat-eliminate
            (lambda unrestricted matched : Nat . Nat)
            (app induction candidate)
            (lambda unrestricted predecessor : Nat .
              (lambda unrestricted ignored : Nat . (succ zero)))
            (bytes-equal identifier candidate))))))

def applicationBuilderIncrementFreshResult :
  (pi unrestricted result : (family FreshBinderNameResult) .
    (family FreshBinderNameResult)) =
  (lambda unrestricted result : (family FreshBinderNameResult) .
    (eliminate FreshBinderNameResult
      (lambda unrestricted value : (family FreshBinderNameResult) .
        (family FreshBinderNameResult))
      result
      (branch FreshBinderNameBuilt name probes .
        (constructor FreshBinderNameResult FreshBinderNameBuilt
          name (succ probes)))
      (branch FreshBinderNameRejected error probes .
        (constructor FreshBinderNameResult FreshBinderNameRejected
          error (succ probes)))))

def applicationBuilderFreshBinderSearch :
  (pi unrestricted fuel : Nat .
    (pi unrestricted candidate : Bytes .
      (pi unrestricted scope : (family NameScope) .
        (family FreshBinderNameResult)))) =
  (lambda unrestricted fuel : Nat .
    (nat-eliminate
      (lambda unrestricted remainingFuel : Nat .
        (pi unrestricted candidate : Bytes .
          (pi unrestricted scope : (family NameScope) .
            (family FreshBinderNameResult))))
      (lambda unrestricted candidate : Bytes .
        (lambda unrestricted scope : (family NameScope) .
          (constructor FreshBinderNameResult FreshBinderNameRejected
            (constructor ApplicationBuilderError
              ApplicationBuilderBinderFreshnessExhausted zero)
            zero)))
      (lambda unrestricted predecessor : Nat .
        (lambda unrestricted induction :
          (pi unrestricted candidate : Bytes .
            (pi unrestricted scope : (family NameScope) .
              (family FreshBinderNameResult))) .
          (lambda unrestricted candidate : Bytes .
            (lambda unrestricted scope : (family NameScope) .
              (nat-eliminate
                (lambda unrestricted collision : Nat .
                  (family FreshBinderNameResult))
                (constructor FreshBinderNameResult FreshBinderNameBuilt
                  candidate (succ zero))
                (lambda unrestricted ignoredPredecessor : Nat .
                  (lambda unrestricted ignoredInduction : (family FreshBinderNameResult) .
                    (app applicationBuilderIncrementFreshResult
                      (app
                        (app induction
                          (bytes-append candidate b"'"))
                        scope))))
                (app
                  (app applicationBuilderScopeContains scope)
                  candidate))))))
      fuel))

def freshBinderName :
  (pi unrestricted candidate : Bytes .
    (pi unrestricted scope : (family NameScope) .
      (family FreshBinderNameResult))) =
  (lambda unrestricted candidate : Bytes .
    (lambda unrestricted scope : (family NameScope) .
      (nat-eliminate
        (lambda unrestricted candidateLength : Nat .
          (family FreshBinderNameResult))
        (constructor FreshBinderNameResult FreshBinderNameRejected
          (constructor ApplicationBuilderError ApplicationBuilderEmptyBinderName)
          zero)
        (lambda unrestricted predecessor : Nat .
          (lambda unrestricted induction : (family FreshBinderNameResult) .
            (app
              (app
                (app applicationBuilderFreshBinderSearch
                  (succ (app applicationBuilderScopeDepth scope)))
                candidate)
              scope)))
        (bytes-length candidate))))

def checkBinderNameFresh :
  (pi unrestricted candidate : Bytes .
    (pi unrestricted scope : (family NameScope) .
      (family FreshBinderNameResult))) =
  (lambda unrestricted candidate : Bytes .
    (lambda unrestricted scope : (family NameScope) .
      (nat-eliminate
        (lambda unrestricted candidateLength : Nat .
          (family FreshBinderNameResult))
        (constructor FreshBinderNameResult FreshBinderNameRejected
          (constructor ApplicationBuilderError ApplicationBuilderEmptyBinderName)
          zero)
        (lambda unrestricted predecessor : Nat .
          (lambda unrestricted induction : (family FreshBinderNameResult) .
            (nat-eliminate
              (lambda unrestricted collision : Nat .
                (family FreshBinderNameResult))
              (constructor FreshBinderNameResult FreshBinderNameBuilt
                candidate (succ zero))
              (lambda unrestricted ignoredPredecessor : Nat .
                (lambda unrestricted ignoredInduction : (family FreshBinderNameResult) .
                  (constructor FreshBinderNameResult FreshBinderNameRejected
                    (constructor ApplicationBuilderError
                      ApplicationBuilderBinderFreshnessExhausted (succ zero))
                    (succ zero))))
              (app
                (app applicationBuilderScopeContains scope)
                candidate))))
        (bytes-length candidate))))

def applicationBuilderFreshnessTelemetry :
  (pi unrestricted result : (family FreshBinderNameResult) .
    (family ApplicationBuilderTelemetry)) =
  (lambda unrestricted result : (family FreshBinderNameResult) .
    (eliminate FreshBinderNameResult
      (lambda unrestricted value : (family FreshBinderNameResult) .
        (family ApplicationBuilderTelemetry))
      result
      (branch FreshBinderNameBuilt name probes .
        (constructor ApplicationBuilderTelemetry
          ApplicationBuilderTelemetryValue
          zero
          zero
          zero
          zero
          probes
          zero
          zero
          applicationBuilderSuccessCode))
      (branch FreshBinderNameRejected error probes .
        (constructor ApplicationBuilderTelemetry
          ApplicationBuilderTelemetryValue
          zero
          zero
          zero
          zero
          probes
          zero
          zero
          (app applicationBuilderErrorStableCode error)))))