module Compiler.DependentCore import Compiler.NormalizationBudget import Model.Config import Model.Word32 import Compiler.NaturalOperation import Compiler.NaturalMagnitude import Compiler.NaturalMagnitudeArithmetic family CoreArithmeticInspection : Type 0 constructor CoreArithmeticValue field unrestricted coreArithmeticDigits : Bytes constructor CoreArithmeticNeutral constructor CoreArithmeticRejected field unrestricted coreArithmeticFailure : (family NaturalMagnitudeFailure) end-family family CoreMultiplicity : Type 0 constructor CoreErased constructor CoreLinear constructor CoreAffine constructor CoreUnrestricted end-family family CorePrimitive : Type 0 constructor CoreByteEqual constructor CoreByteLess constructor CoreNaturalLess constructor CoreNaturalToByte constructor CoreByteToNatural constructor CoreBytesAppend constructor CoreBytesCons constructor CoreBytesLength constructor CoreNaturalEliminate constructor CoreBytesEliminate constructor CoreBytesEqual constructor CoreFileEffect constructor CoreEffects constructor CoreComputation constructor CoreReturn constructor CoreBind constructor CoreReadFile constructor CoreWriteFile constructor CoreLinuxOpenNode constructor CoreLinuxCloseNode constructor CoreLinuxIoctl constructor CoreLinuxMmap constructor CoreLinuxMunmap constructor CoreBytesSetIndex constructor CoreBytesIndexNonzero constructor CoreBytesSetFreeIndex constructor CoreBytesBuilderType constructor CoreBytesBuilderEmpty constructor CoreBytesBuilderChunk constructor CoreBytesBuilderAppend constructor CoreBytesBuilderBuild constructor CoreRuntimeImageV4Build constructor CoreBytesHead constructor CoreBytesTail constructor CoreBytesChecksum end-family family NamedCoreTerm : Type 0 constructor NamedCoreUniverse field unrestricted namedUniverseLevel : Nat constructor NamedCoreNatural constructor NamedCoreNaturalLiteral field unrestricted namedNaturalValue : Bytes constructor NamedCoreVariable field unrestricted namedVariableIdentifier : Bytes constructor NamedCorePi field unrestricted namedPiMultiplicity : (family CoreMultiplicity) field unrestricted namedPiBinder : Bytes recursive unrestricted namedPiDomain recursive unrestricted namedPiCodomain constructor NamedCoreLambda field unrestricted namedLambdaMultiplicity : (family CoreMultiplicity) field unrestricted namedLambdaBinder : Bytes recursive unrestricted namedLambdaDomain recursive unrestricted namedLambdaBody constructor NamedCoreLet field unrestricted namedLetMultiplicity : (family CoreMultiplicity) field unrestricted namedLetBinder : Bytes recursive unrestricted namedLetAnnotation recursive unrestricted namedLetValue recursive unrestricted namedLetBody constructor NamedCoreApplication recursive unrestricted namedApplicationFunction recursive unrestricted namedApplicationArgument constructor NamedCoreNaturalArithmetic field unrestricted namedcoreArithmeticOperation : (family CoreNaturalOperation) recursive unrestricted namedcoreArithmeticLeft recursive unrestricted namedcoreArithmeticRight constructor NamedCoreNaturalSuccessor recursive unrestricted namedNaturalPredecessor constructor NamedCoreByte constructor NamedCoreByteLiteral field unrestricted namedByteValue : Byte constructor NamedCoreBytes constructor NamedCoreBytesLiteral field unrestricted namedBytesValue : Bytes constructor NamedCoreTermSequenceEnd constructor NamedCoreTermSequenceNext recursive unrestricted namedCoreTermSequenceHead recursive unrestricted namedCoreTermSequenceTail constructor NamedCoreFamilyApplication field unrestricted namedCoreFamilyName : Bytes recursive unrestricted namedCoreFamilyArguments constructor NamedCoreConstructorApplication field unrestricted namedCoreConstructorFamilyName : Bytes field unrestricted namedCoreConstructorName : Bytes recursive unrestricted namedCoreConstructorArguments constructor NamedCoreEliminatorBranch field unrestricted namedCoreBranchConstructorName : Bytes recursive unrestricted namedCoreBranchBinderNames recursive unrestricted namedCoreBranchBody constructor NamedCoreEliminator field unrestricted namedCoreEliminatedFamilyName : Bytes recursive unrestricted namedCoreEliminatorMotive recursive unrestricted namedCoreEliminatorScrutinee recursive unrestricted namedCoreEliminatorBranches end-family family CoreTerm : Type 0 constructor CoreUniverse field unrestricted coreUniverseLevel : Nat constructor CoreNatural constructor CoreNaturalLiteral field unrestricted coreNaturalValue : Bytes constructor CoreBound field unrestricted coreBoundIndex : Nat constructor CorePi field unrestricted corePiMultiplicity : (family CoreMultiplicity) recursive unrestricted corePiDomain recursive unrestricted corePiCodomain constructor CoreLambda field unrestricted coreLambdaMultiplicity : (family CoreMultiplicity) recursive unrestricted coreLambdaDomain recursive unrestricted coreLambdaBody constructor CoreLet field unrestricted coreLetMultiplicity : (family CoreMultiplicity) recursive unrestricted coreLetAnnotation recursive unrestricted coreLetValue recursive unrestricted coreLetBody constructor CoreApplication recursive unrestricted coreApplicationFunction recursive unrestricted coreApplicationArgument constructor CoreNaturalArithmetic field unrestricted coreArithmeticOperation : (family CoreNaturalOperation) recursive unrestricted coreArithmeticLeft recursive unrestricted coreArithmeticRight constructor CoreNaturalSuccessor recursive unrestricted coreNaturalPredecessor constructor CoreByte constructor CoreByteLiteral field unrestricted coreByteValue : Byte constructor CoreBytes constructor CoreBytesLiteral field unrestricted coreBytesValue : Bytes constructor CorePrimitiveTerm field unrestricted corePrimitive : (family CorePrimitive) constructor CoreTermSequenceEnd constructor CoreTermSequenceNext recursive unrestricted coreTermSequenceHead recursive unrestricted coreTermSequenceTail constructor CoreFamilyApplication field unrestricted coreFamilyName : Bytes recursive unrestricted coreFamilyArguments constructor CoreConstructorApplication field unrestricted coreConstructorFamilyName : Bytes field unrestricted coreConstructorName : Bytes recursive unrestricted coreConstructorArguments constructor CoreEliminatorBranch field unrestricted coreBranchConstructorName : Bytes field unrestricted coreBranchBinderCount : Nat recursive unrestricted coreBranchBody constructor CoreEliminator field unrestricted coreEliminatedFamilyName : Bytes recursive unrestricted coreEliminatorMotive recursive unrestricted coreEliminatorScrutinee recursive unrestricted coreEliminatorBranches end-family family NameScope : Type 0 constructor EmptyNameScope constructor NameScopeBinding field unrestricted scopeBindingIdentifier : Bytes recursive unrestricted outerNameScope end-family family NameLookupResult : Type 0 constructor NameFound field unrestricted foundNameIndex : Nat constructor NameNotFound field unrestricted missingNameIdentifier : Bytes end-family family CoreResolutionResult : Type 0 constructor CoreResolved field unrestricted resolvedCoreTerm : (family CoreTerm) constructor CoreResolutionFailed field unrestricted unresolvedNameIdentifier : Bytes end-family family NamedCoreVariableInspection : Type 0 constructor NamedCoreVariableFound field unrestricted inspectedNamedCoreVariable : Bytes constructor NamedCoreTermIsNotVariable end-family family EliminatorBranchScopeResolution : Type 0 constructor EliminatorBranchScopeResolved field unrestricted resolvedEliminatorBranchScope : (family NameScope) field unrestricted resolvedEliminatorBranchBinderCount : Nat constructor EliminatorBranchScopeRejected end-family family CoreEliminatorBranchSelection : Type 0 constructor CoreEliminatorBranchSelected field unrestricted selectedCoreEliminatorBinderCount : Nat field unrestricted selectedCoreEliminatorBranchBody : (family CoreTerm) constructor CoreEliminatorBranchMissing end-family family TypeContext : Type 0 constructor EmptyTypeContext constructor TypeContextBinding field unrestricted contextBindingType : (family CoreTerm) recursive unrestricted outerTypeContext end-family family TypeLookupResult : Type 0 constructor TypeFound field unrestricted foundVariableType : (family CoreTerm) constructor TypeNotFound field unrestricted missingVariableIndex : Nat end-family family UniverseInspection : Type 0 constructor IsUniverse field unrestricted inspectedUniverseLevel : Nat constructor NotUniverse end-family family PiInspection : Type 0 constructor IsPi field unrestricted inspectedPiMultiplicity : (family CoreMultiplicity) field unrestricted inspectedPiDomain : (family CoreTerm) field unrestricted inspectedPiCodomain : (family CoreTerm) constructor NotPi end-family family CoreInferenceResult : Type 0 constructor CoreInferred field unrestricted inferredCoreType : (family CoreTerm) constructor CoreInferenceFailed field unrestricted coreInferenceFailureCode : Nat end-family family CorePrimitiveLookupResult : Type 0 constructor CorePrimitiveFound field unrestricted foundCorePrimitive : (family CorePrimitive) constructor CorePrimitiveNotFound field unrestricted missingCorePrimitiveName : Bytes end-family family CoreLiteralInspection : Type 0 constructor CoreNaturalInspected field unrestricted inspectedNaturalValue : Bytes constructor CoreByteInspected field unrestricted inspectedByteValue : Byte constructor CoreBytesInspected field unrestricted inspectedBytesValue : Bytes constructor CoreNotLiteral end-family family CoreFunctionInspection : Type 0 constructor CoreFunctionLambda field unrestricted inspectedLambdaBody : (family CoreTerm) constructor CoreFunctionPrimitive field unrestricted inspectedFunctionPrimitive : (family CorePrimitive) constructor CoreFunctionAppliedPrimitive field unrestricted inspectedAppliedPrimitive : (family CorePrimitive) field unrestricted inspectedPrimitiveArgument : (family CoreTerm) constructor CoreFunctionAppliedPrimitive2 field unrestricted inspectedAppliedPrimitive2 : (family CorePrimitive) field unrestricted inspectedPrimitiveArgument1 : (family CoreTerm) field unrestricted inspectedPrimitiveArgument2 : (family CoreTerm) constructor CoreFunctionAppliedPrimitive3 field unrestricted inspectedAppliedPrimitive3 : (family CorePrimitive) field unrestricted inspectedPrimitiveArgumentFirst : (family CoreTerm) field unrestricted inspectedPrimitiveArgumentSecond : (family CoreTerm) field unrestricted inspectedPrimitiveArgumentThird : (family CoreTerm) constructor CoreFunctionOther end-family -- A completed result has reached a fixed point; exhaustion retains only a -- resumable residual and never claims it is a normal form. Counts are rounds, -- not node visits or wall-clock work. family CoreReductionResult : Type 0 constructor CoreReductionCompleted field unrestricted coreReductionFixedPoint : (family CoreTerm) field unrestricted coreReductionCompletedRounds : Nat constructor CoreReductionExhausted field unrestricted coreReductionResidual : (family CoreTerm) field unrestricted coreReductionExhaustedRounds : Nat end-family -- Exhaustion has no term projection. A parent can consume only a successful -- child, and receives exactly that child's remaining work budget. family CoreWorkResult : Type 0 constructor CoreWorkCompleted field unrestricted coreWorkTerm : (family CoreTerm) field unrestricted coreWorkBudget : (family NormalizationBudget) constructor CoreWorkExhausted field unrestricted coreWorkExhaustedBudget : (family NormalizationBudget) end-family family CoreNaturalWorkState : Type 0 constructor CoreNaturalWorkActive field unrestricted coreNaturalWorkPredecessor : Bytes field unrestricted coreNaturalWorkTerm : (family CoreTerm) field unrestricted coreNaturalWorkBudget : (family NormalizationBudget) constructor CoreNaturalWorkStopped field unrestricted coreNaturalWorkStoppedBudget : (family NormalizationBudget) end-family def coreNaturalOperationCode = Compiler.NaturalOperation/naturalOperationCode def evaluateCoreNaturalOperation = (lambda unrestricted operation : (family CoreNaturalOperation) . (eliminate CoreNaturalOperation (lambda unrestricted current : (family CoreNaturalOperation) . (pi unrestricted left : Bytes . (pi unrestricted right : Bytes . (family NaturalMagnitudeResult)))) operation (branch CoreNaturalAdd . Compiler.NaturalMagnitude/magnitudeAddChecked) (branch CoreNaturalSubtract . Compiler.NaturalMagnitude/magnitudeSubtractChecked) (branch CoreNaturalMultiply . Compiler.NaturalMagnitude/magnitudeMultiplyChecked) (branch CoreNaturalDivide . Compiler.NaturalMagnitude/magnitudeDivideChecked) (branch CoreNaturalModulo . Compiler.NaturalMagnitude/magnitudeModuloChecked))) def coreUnrestricted : (family CoreMultiplicity) = (constructor CoreMultiplicity CoreUnrestricted) def coreUnaryType : (pi unrestricted domain : (family CoreTerm) . (pi unrestricted codomain : (family CoreTerm) . (family CoreTerm))) = (lambda unrestricted domain : (family CoreTerm) . (lambda unrestricted codomain : (family CoreTerm) . (constructor CoreTerm CorePi coreUnrestricted domain codomain))) def coreBinaryType : (pi unrestricted left : (family CoreTerm) . (pi unrestricted right : (family CoreTerm) . (pi unrestricted result : (family CoreTerm) . (family CoreTerm)))) = (lambda unrestricted left : (family CoreTerm) . (lambda unrestricted right : (family CoreTerm) . (lambda unrestricted result : (family CoreTerm) . (constructor CoreTerm CorePi coreUnrestricted left (constructor CoreTerm CorePi coreUnrestricted right result))))) def coreTernaryType : (pi unrestricted first : (family CoreTerm) . (pi unrestricted second : (family CoreTerm) . (pi unrestricted third : (family CoreTerm) . (pi unrestricted result : (family CoreTerm) . (family CoreTerm))))) = (lambda unrestricted first : (family CoreTerm) . (lambda unrestricted second : (family CoreTerm) . (lambda unrestricted third : (family CoreTerm) . (lambda unrestricted result : (family CoreTerm) . (constructor CoreTerm CorePi coreUnrestricted first (constructor CoreTerm CorePi coreUnrestricted second (constructor CoreTerm CorePi coreUnrestricted third result))))))) def coreQuaternaryType : (pi unrestricted first : (family CoreTerm) . (pi unrestricted second : (family CoreTerm) . (pi unrestricted third : (family CoreTerm) . (pi unrestricted fourth : (family CoreTerm) . (pi unrestricted result : (family CoreTerm) . (family CoreTerm)))))) = (lambda unrestricted first : (family CoreTerm) . (lambda unrestricted second : (family CoreTerm) . (lambda unrestricted third : (family CoreTerm) . (lambda unrestricted fourth : (family CoreTerm) . (lambda unrestricted result : (family CoreTerm) . (constructor CoreTerm CorePi coreUnrestricted first (constructor CoreTerm CorePi coreUnrestricted second (constructor CoreTerm CorePi coreUnrestricted third (constructor CoreTerm CorePi coreUnrestricted fourth result))))))))) def coreNaturalEliminateType : (family CoreTerm) = (constructor CoreTerm CorePi coreUnrestricted (constructor CoreTerm CorePi coreUnrestricted (constructor CoreTerm CoreNatural) (constructor CoreTerm CoreUniverse zero)) (constructor CoreTerm CorePi coreUnrestricted (constructor CoreTerm CoreApplication (constructor CoreTerm CoreBound zero) (constructor CoreTerm CoreNaturalLiteral b"")) (constructor CoreTerm CorePi coreUnrestricted (constructor CoreTerm CorePi coreUnrestricted (constructor CoreTerm CoreNatural) (constructor CoreTerm CorePi coreUnrestricted (constructor CoreTerm CoreApplication (constructor CoreTerm CoreBound (succ (succ zero))) (constructor CoreTerm CoreBound zero)) (constructor CoreTerm CoreApplication (constructor CoreTerm CoreBound (succ (succ (succ zero)))) (constructor CoreTerm CoreNaturalSuccessor (constructor CoreTerm CoreBound (succ zero)))))) (constructor CoreTerm CorePi coreUnrestricted (constructor CoreTerm CoreNatural) (constructor CoreTerm CoreApplication (constructor CoreTerm CoreBound (succ (succ (succ zero)))) (constructor CoreTerm CoreBound zero)))))) def coreBytesEliminateType : (family CoreTerm) = (constructor CoreTerm CorePi coreUnrestricted (constructor CoreTerm CorePi coreUnrestricted (constructor CoreTerm CoreBytes) (constructor CoreTerm CoreUniverse zero)) (constructor CoreTerm CorePi coreUnrestricted (constructor CoreTerm CoreApplication (constructor CoreTerm CoreBound zero) (constructor CoreTerm CoreBytesLiteral b"")) (constructor CoreTerm CorePi coreUnrestricted (constructor CoreTerm CorePi coreUnrestricted (constructor CoreTerm CoreByte) (constructor CoreTerm CorePi coreUnrestricted (constructor CoreTerm CoreBytes) (constructor CoreTerm CorePi coreUnrestricted (constructor CoreTerm CoreApplication (constructor CoreTerm CoreBound (succ (succ (succ zero)))) (constructor CoreTerm CoreBound zero)) (constructor CoreTerm CoreApplication (constructor CoreTerm CoreBound (succ (succ (succ (succ zero))))) (constructor CoreTerm CoreApplication (constructor CoreTerm CoreApplication (constructor CoreTerm CorePrimitiveTerm (constructor CorePrimitive CoreBytesCons)) (constructor CoreTerm CoreBound (succ (succ zero)))) (constructor CoreTerm CoreBound (succ zero))))))) (constructor CoreTerm CorePi coreUnrestricted (constructor CoreTerm CoreBytes) (constructor CoreTerm CoreApplication (constructor CoreTerm CoreBound (succ (succ (succ zero)))) (constructor CoreTerm CoreBound zero)))))) def coreFileEffectTerm : (family CoreTerm) = (constructor CoreTerm CorePrimitiveTerm (constructor CorePrimitive CoreFileEffect)) def coreBytesBuilderTerm : (family CoreTerm) = (constructor CoreTerm CorePrimitiveTerm (constructor CorePrimitive CoreBytesBuilderType)) def coreFileEffectRow : (family CoreTerm) = (constructor CoreTerm CoreApplication (constructor CoreTerm CorePrimitiveTerm (constructor CorePrimitive CoreEffects)) coreFileEffectTerm) def coreComputationType = (lambda unrestricted effects : (family CoreTerm) . (lambda unrestricted resultType : (family CoreTerm) . (constructor CoreTerm CoreApplication (constructor CoreTerm CoreApplication (constructor CoreTerm CorePrimitiveTerm (constructor CorePrimitive CoreComputation)) effects) resultType))) def corePrimitiveType : (pi unrestricted primitive : (family CorePrimitive) . (family CoreTerm)) = (lambda unrestricted primitive : (family CorePrimitive) . (eliminate CorePrimitive (lambda unrestricted value : (family CorePrimitive) . (family CoreTerm)) primitive (branch CoreByteEqual . (coreBinaryType (constructor CoreTerm CoreByte) (constructor CoreTerm CoreByte) (constructor CoreTerm CoreNatural))) (branch CoreByteLess . (coreBinaryType (constructor CoreTerm CoreByte) (constructor CoreTerm CoreByte) (constructor CoreTerm CoreNatural))) (branch CoreNaturalLess . (coreBinaryType (constructor CoreTerm CoreNatural) (constructor CoreTerm CoreNatural) (constructor CoreTerm CoreNatural))) (branch CoreNaturalToByte . (coreUnaryType (constructor CoreTerm CoreNatural) (constructor CoreTerm CoreByte))) (branch CoreByteToNatural . (coreUnaryType (constructor CoreTerm CoreByte) (constructor CoreTerm CoreNatural))) (branch CoreBytesAppend . (coreBinaryType (constructor CoreTerm CoreBytes) (constructor CoreTerm CoreBytes) (constructor CoreTerm CoreBytes))) (branch CoreBytesCons . (coreBinaryType (constructor CoreTerm CoreByte) (constructor CoreTerm CoreBytes) (constructor CoreTerm CoreBytes))) (branch CoreBytesLength . (coreUnaryType (constructor CoreTerm CoreBytes) (constructor CoreTerm CoreNatural))) (branch CoreNaturalEliminate . coreNaturalEliminateType) (branch CoreBytesEliminate . coreBytesEliminateType) (branch CoreBytesEqual . (coreBinaryType (constructor CoreTerm CoreBytes) (constructor CoreTerm CoreBytes) (constructor CoreTerm CoreNatural))) (branch CoreFileEffect . (constructor CoreTerm CoreUniverse zero)) (branch CoreEffects . (coreUnaryType (constructor CoreTerm CoreUniverse zero) (constructor CoreTerm CoreUniverse zero))) (branch CoreComputation . (coreBinaryType (constructor CoreTerm CoreUniverse zero) (constructor CoreTerm CoreUniverse zero) (constructor CoreTerm CoreUniverse zero))) (branch CoreReturn . (constructor CoreTerm CoreUniverse zero)) (branch CoreBind . (constructor CoreTerm CoreUniverse zero)) (branch CoreReadFile . (coreUnaryType (constructor CoreTerm CoreBytes) (coreComputationType coreFileEffectRow (constructor CoreTerm CoreBytes)))) (branch CoreWriteFile . (coreBinaryType (constructor CoreTerm CoreBytes) (constructor CoreTerm CoreBytes) (coreComputationType coreFileEffectRow (constructor CoreTerm CoreNatural)))) (branch CoreLinuxOpenNode . (coreUnaryType (constructor CoreTerm CoreBytes) (coreComputationType coreFileEffectRow (constructor CoreTerm CoreBytes)))) (branch CoreLinuxCloseNode . (coreUnaryType (constructor CoreTerm CoreBytes) (coreComputationType coreFileEffectRow (constructor CoreTerm CoreNatural)))) (branch CoreLinuxIoctl . (coreTernaryType (constructor CoreTerm CoreBytes) (constructor CoreTerm CoreBytes) (constructor CoreTerm CoreBytes) (coreComputationType coreFileEffectRow (constructor CoreTerm CoreBytes)))) (branch CoreLinuxMmap . (coreUnaryType (constructor CoreTerm CoreBytes) (coreComputationType coreFileEffectRow (constructor CoreTerm CoreBytes)))) (branch CoreLinuxMunmap . (coreBinaryType (constructor CoreTerm CoreBytes) (constructor CoreTerm CoreBytes) (coreComputationType coreFileEffectRow (constructor CoreTerm CoreNatural)))) (branch CoreBytesSetIndex . (coreBinaryType (constructor CoreTerm CoreBytes) (constructor CoreTerm CoreNatural) (constructor CoreTerm CoreBytes))) (branch CoreBytesIndexNonzero . (coreBinaryType (constructor CoreTerm CoreBytes) (constructor CoreTerm CoreNatural) (constructor CoreTerm CoreNatural))) (branch CoreBytesSetFreeIndex . (coreQuaternaryType (constructor CoreTerm CoreBytes) (constructor CoreTerm CoreNatural) (constructor CoreTerm CoreNatural) (constructor CoreTerm CoreNatural) (constructor CoreTerm CoreBytes))) (branch CoreBytesBuilderType . (constructor CoreTerm CoreUniverse zero)) (branch CoreBytesBuilderEmpty . coreBytesBuilderTerm) (branch CoreBytesBuilderChunk . (coreUnaryType (constructor CoreTerm CoreBytes) coreBytesBuilderTerm)) (branch CoreBytesBuilderAppend . (coreBinaryType coreBytesBuilderTerm coreBytesBuilderTerm coreBytesBuilderTerm)) (branch CoreBytesBuilderBuild . (coreUnaryType coreBytesBuilderTerm (constructor CoreTerm CoreBytes))) (branch CoreRuntimeImageV4Build . (coreUnaryType coreBytesBuilderTerm (constructor CoreTerm CoreBytes))) (branch CoreBytesHead . (coreUnaryType (constructor CoreTerm CoreBytes) (constructor CoreTerm CoreByte))) (branch CoreBytesTail . (coreUnaryType (constructor CoreTerm CoreBytes) (constructor CoreTerm CoreBytes))) (branch CoreBytesChecksum . (coreUnaryType (constructor CoreTerm CoreBytes) (constructor CoreTerm CoreBytes))))) def naturalEqual : (pi unrestricted left : Nat . (pi unrestricted right : Nat . Nat)) = (lambda unrestricted left : Nat . (lambda unrestricted right : Nat . (nat-eliminate (lambda unrestricted result : Nat . Nat) (nat-eliminate (lambda unrestricted result : Nat . Nat) (succ zero) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero)) (nat-less-than right left)) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero)) (nat-less-than left right)))) def coreNaturalAnd : (pi unrestricted left : Nat . (pi unrestricted right : Nat . Nat)) = (lambda unrestricted left : Nat . (lambda unrestricted right : Nat . (nat-eliminate (lambda unrestricted condition : Nat . Nat) zero (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . right)) left))) def coreBytesEqual : (pi unrestricted left : Bytes . (pi unrestricted right : Bytes . Nat)) = (lambda unrestricted left : Bytes . (lambda unrestricted right : Bytes . (bytes-equal left right))) def chooseCorePrimitive : (pi unrestricted matched : Nat . (pi unrestricted primitive : (family CorePrimitive) . (pi unrestricted unmatchedResult : (family CorePrimitiveLookupResult) . (family CorePrimitiveLookupResult)))) = (lambda unrestricted matched : Nat . (lambda unrestricted primitive : (family CorePrimitive) . (lambda unrestricted unmatchedResult : (family CorePrimitiveLookupResult) . (nat-eliminate (lambda unrestricted condition : Nat . (family CorePrimitiveLookupResult)) unmatchedResult (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family CorePrimitiveLookupResult) . (constructor CorePrimitiveLookupResult CorePrimitiveFound primitive))) matched)))) def lookupCoreNativeEffectPrimitive : (pi unrestricted name : Bytes . (family CorePrimitiveLookupResult)) = (lambda unrestricted name : Bytes . (chooseCorePrimitive (coreBytesEqual name b"linux-open-node") (constructor CorePrimitive CoreLinuxOpenNode) (chooseCorePrimitive (coreBytesEqual name b"linux-close-node") (constructor CorePrimitive CoreLinuxCloseNode) (chooseCorePrimitive (coreBytesEqual name b"linux-ioctl") (constructor CorePrimitive CoreLinuxIoctl) (chooseCorePrimitive (coreBytesEqual name b"linux-mmap") (constructor CorePrimitive CoreLinuxMmap) (chooseCorePrimitive (coreBytesEqual name b"linux-munmap") (constructor CorePrimitive CoreLinuxMunmap) (constructor CorePrimitiveLookupResult CorePrimitiveNotFound name))))))) def lookupCoreEffectPrimitive : (pi unrestricted name : Bytes . (family CorePrimitiveLookupResult)) = (lambda unrestricted name : Bytes . (chooseCorePrimitive (coreBytesEqual name b"File") (constructor CorePrimitive CoreFileEffect) (chooseCorePrimitive (coreBytesEqual name b"effects") (constructor CorePrimitive CoreEffects) (chooseCorePrimitive (coreBytesEqual name b"computation") (constructor CorePrimitive CoreComputation) (chooseCorePrimitive (coreBytesEqual name b"return") (constructor CorePrimitive CoreReturn) (chooseCorePrimitive (coreBytesEqual name b"bind") (constructor CorePrimitive CoreBind) (chooseCorePrimitive (coreBytesEqual name b"read-file") (constructor CorePrimitive CoreReadFile) (chooseCorePrimitive (coreBytesEqual name b"write-file") (constructor CorePrimitive CoreWriteFile) (lookupCoreNativeEffectPrimitive name))))))))) def lookupCoreBytesBuilderPrimitive : (pi unrestricted name : Bytes . (family CorePrimitiveLookupResult)) = (lambda unrestricted name : Bytes . (chooseCorePrimitive (coreBytesEqual name b"BytesBuilder") (constructor CorePrimitive CoreBytesBuilderType) (chooseCorePrimitive (coreBytesEqual name b"bytes-builder") (constructor CorePrimitive CoreBytesBuilderType) (chooseCorePrimitive (coreBytesEqual name b"bytes-builder-empty") (constructor CorePrimitive CoreBytesBuilderEmpty) (chooseCorePrimitive (coreBytesEqual name b"bytes-builder-chunk") (constructor CorePrimitive CoreBytesBuilderChunk) (chooseCorePrimitive (coreBytesEqual name b"bytes-builder-append") (constructor CorePrimitive CoreBytesBuilderAppend) (chooseCorePrimitive (coreBytesEqual name b"bytes-builder-build") (constructor CorePrimitive CoreBytesBuilderBuild) (chooseCorePrimitive (coreBytesEqual name b"runtime-image-v4-build") (constructor CorePrimitive CoreRuntimeImageV4Build) (lookupCoreEffectPrimitive name))))))))) def lookupCoreIndexedBytesPrimitive : (pi unrestricted name : Bytes . (family CorePrimitiveLookupResult)) = (lambda unrestricted name : Bytes . (chooseCorePrimitive (coreBytesEqual name b"bytes-set-index") (constructor CorePrimitive CoreBytesSetIndex) (chooseCorePrimitive (coreBytesEqual name b"bytes-index-nonzero") (constructor CorePrimitive CoreBytesIndexNonzero) (chooseCorePrimitive (coreBytesEqual name b"bytes-set-free-index") (constructor CorePrimitive CoreBytesSetFreeIndex) (chooseCorePrimitive (coreBytesEqual name b"bytes-head") (constructor CorePrimitive CoreBytesHead) (chooseCorePrimitive (coreBytesEqual name b"bytes-tail") (constructor CorePrimitive CoreBytesTail) (chooseCorePrimitive (coreBytesEqual name b"bytes-checksum") (constructor CorePrimitive CoreBytesChecksum) (lookupCoreBytesBuilderPrimitive name)))))))) def lookupCorePrimitive : (pi unrestricted name : Bytes . (family CorePrimitiveLookupResult)) = (lambda unrestricted name : Bytes . (chooseCorePrimitive (coreBytesEqual name b"byte-equal") (constructor CorePrimitive CoreByteEqual) (chooseCorePrimitive (coreBytesEqual name b"byte-less-than") (constructor CorePrimitive CoreByteLess) (chooseCorePrimitive (coreBytesEqual name b"nat-less-than") (constructor CorePrimitive CoreNaturalLess) (chooseCorePrimitive (coreBytesEqual name b"nat-to-byte") (constructor CorePrimitive CoreNaturalToByte) (chooseCorePrimitive (coreBytesEqual name b"byte-to-nat") (constructor CorePrimitive CoreByteToNatural) (chooseCorePrimitive (coreBytesEqual name b"bytes-append") (constructor CorePrimitive CoreBytesAppend) (chooseCorePrimitive (coreBytesEqual name b"bytes-cons") (constructor CorePrimitive CoreBytesCons) (chooseCorePrimitive (coreBytesEqual name b"bytes-length") (constructor CorePrimitive CoreBytesLength) (chooseCorePrimitive (coreBytesEqual name b"nat-eliminate") (constructor CorePrimitive CoreNaturalEliminate) (chooseCorePrimitive (coreBytesEqual name b"bytes-eliminate") (constructor CorePrimitive CoreBytesEliminate) (chooseCorePrimitive (coreBytesEqual name b"bytes-equal") (constructor CorePrimitive CoreBytesEqual) (lookupCoreIndexedBytesPrimitive name))))))))))))) def resolveCorePrimitiveName : (pi unrestricted name : Bytes . (family CoreResolutionResult)) = (lambda unrestricted name : Bytes . (eliminate CorePrimitiveLookupResult (lambda unrestricted result : (family CorePrimitiveLookupResult) . (family CoreResolutionResult)) (lookupCorePrimitive name) (branch CorePrimitiveFound primitive . (constructor CoreResolutionResult CoreResolved (constructor CoreTerm CorePrimitiveTerm primitive))) (branch CorePrimitiveNotFound missing . (constructor CoreResolutionResult CoreResolutionFailed missing)))) def naturalAdd : (pi unrestricted left : Nat . (pi unrestricted right : Nat . Nat)) = (lambda unrestricted left : Nat . (lambda unrestricted right : Nat . (nat-eliminate (lambda unrestricted value : Nat . Nat) right (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . (succ induction))) left))) def naturalMaximum : (pi unrestricted left : Nat . (pi unrestricted right : Nat . Nat)) = (lambda unrestricted left : Nat . (lambda unrestricted right : Nat . (nat-eliminate (lambda unrestricted condition : Nat . Nat) left (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . right)) (nat-less-than left right)))) def naturalPredecessor : (pi unrestricted value : Nat . Nat) = (lambda unrestricted value : Nat . (nat-eliminate (lambda unrestricted natural : Nat . Nat) zero (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . predecessor)) value)) def multiplicityCode : (pi unrestricted multiplicity : (family CoreMultiplicity) . Nat) = (lambda unrestricted multiplicity : (family CoreMultiplicity) . (eliminate CoreMultiplicity (lambda unrestricted value : (family CoreMultiplicity) . Nat) multiplicity (branch CoreErased . zero) (branch CoreLinear . (succ zero)) (branch CoreAffine . (succ (succ zero))) (branch CoreUnrestricted . (succ (succ (succ zero)))))) def multiplicityEqual : (pi unrestricted left : (family CoreMultiplicity) . (pi unrestricted right : (family CoreMultiplicity) . Nat)) = (lambda unrestricted left : (family CoreMultiplicity) . (lambda unrestricted right : (family CoreMultiplicity) . (naturalEqual (multiplicityCode left) (multiplicityCode right)))) def incrementNameLookup : (pi unrestricted result : (family NameLookupResult) . (family NameLookupResult)) = (lambda unrestricted result : (family NameLookupResult) . (eliminate NameLookupResult (lambda unrestricted value : (family NameLookupResult) . (family NameLookupResult)) result (branch NameFound index . (constructor NameLookupResult NameFound (succ index))) (branch NameNotFound identifier . (constructor NameLookupResult NameNotFound identifier)))) def lookupNameFrom : (pi unrestricted scope : (family NameScope) . (pi unrestricted identifier : Bytes . (pi unrestricted index : Nat . (family NameLookupResult)))) = (lambda unrestricted scope : (family NameScope) . (eliminate NameScope (lambda unrestricted value : (family NameScope) . (pi unrestricted identifier : Bytes . (pi unrestricted index : Nat . (family NameLookupResult)))) scope (branch EmptyNameScope . (lambda unrestricted identifier : Bytes . (lambda unrestricted index : Nat . (constructor NameLookupResult NameNotFound identifier)))) (branch NameScopeBinding bindingIdentifier outerScope ih_outerScope . (lambda unrestricted identifier : Bytes . (lambda unrestricted index : Nat . (app (nat-eliminate (lambda unrestricted condition : Nat . (pi unrestricted ignored : Nat . (family NameLookupResult))) (lambda unrestricted ignored : Nat . (ih_outerScope identifier (succ index))) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (pi unrestricted ignored : Nat . (family NameLookupResult)) . (lambda unrestricted ignored : Nat . (constructor NameLookupResult NameFound index)))) (coreBytesEqual bindingIdentifier identifier)) zero)))))) def lookupName : (pi unrestricted scope : (family NameScope) . (pi unrestricted identifier : Bytes . (family NameLookupResult))) = (lambda unrestricted scope : (family NameScope) . (lambda unrestricted identifier : Bytes . (lookupNameFrom scope identifier zero))) def combineResolvedPi : (pi unrestricted multiplicity : (family CoreMultiplicity) . (pi unrestricted domainResult : (family CoreResolutionResult) . (pi unrestricted codomainResult : (family CoreResolutionResult) . (family CoreResolutionResult)))) = (lambda unrestricted multiplicity : (family CoreMultiplicity) . (lambda unrestricted domainResult : (family CoreResolutionResult) . (lambda unrestricted codomainResult : (family CoreResolutionResult) . (eliminate CoreResolutionResult (lambda unrestricted value : (family CoreResolutionResult) . (family CoreResolutionResult)) domainResult (branch CoreResolved domain . (eliminate CoreResolutionResult (lambda unrestricted value : (family CoreResolutionResult) . (family CoreResolutionResult)) codomainResult (branch CoreResolved codomain . (constructor CoreResolutionResult CoreResolved (constructor CoreTerm CorePi multiplicity domain codomain))) (branch CoreResolutionFailed identifier . (constructor CoreResolutionResult CoreResolutionFailed identifier)))) (branch CoreResolutionFailed identifier . (constructor CoreResolutionResult CoreResolutionFailed identifier)))))) def combineResolvedLambda : (pi unrestricted multiplicity : (family CoreMultiplicity) . (pi unrestricted domainResult : (family CoreResolutionResult) . (pi unrestricted bodyResult : (family CoreResolutionResult) . (family CoreResolutionResult)))) = (lambda unrestricted multiplicity : (family CoreMultiplicity) . (lambda unrestricted domainResult : (family CoreResolutionResult) . (lambda unrestricted bodyResult : (family CoreResolutionResult) . (eliminate CoreResolutionResult (lambda unrestricted value : (family CoreResolutionResult) . (family CoreResolutionResult)) domainResult (branch CoreResolved domain . (eliminate CoreResolutionResult (lambda unrestricted value : (family CoreResolutionResult) . (family CoreResolutionResult)) bodyResult (branch CoreResolved body . (constructor CoreResolutionResult CoreResolved (constructor CoreTerm CoreLambda multiplicity domain body))) (branch CoreResolutionFailed identifier . (constructor CoreResolutionResult CoreResolutionFailed identifier)))) (branch CoreResolutionFailed identifier . (constructor CoreResolutionResult CoreResolutionFailed identifier)))))) def combineResolvedLetValue = (lambda unrestricted multiplicity : (family CoreMultiplicity) . (lambda unrestricted annotation : (family CoreTerm) . (lambda unrestricted valueResult : (family CoreResolutionResult) . (lambda unrestricted bodyResult : (family CoreResolutionResult) . (eliminate CoreResolutionResult (lambda unrestricted current : (family CoreResolutionResult) . (family CoreResolutionResult)) valueResult (branch CoreResolved value . (eliminate CoreResolutionResult (lambda unrestricted current : (family CoreResolutionResult) . (family CoreResolutionResult)) bodyResult (branch CoreResolved body . (constructor CoreResolutionResult CoreResolved (constructor CoreTerm CoreLet multiplicity annotation value body))) (branch CoreResolutionFailed identifier . (constructor CoreResolutionResult CoreResolutionFailed identifier)))) (branch CoreResolutionFailed identifier . (constructor CoreResolutionResult CoreResolutionFailed identifier))))))) def combineResolvedLet = (lambda unrestricted multiplicity : (family CoreMultiplicity) . (lambda unrestricted annotationResult : (family CoreResolutionResult) . (lambda unrestricted valueResult : (family CoreResolutionResult) . (lambda unrestricted bodyResult : (family CoreResolutionResult) . (eliminate CoreResolutionResult (lambda unrestricted current : (family CoreResolutionResult) . (family CoreResolutionResult)) annotationResult (branch CoreResolved annotation . (combineResolvedLetValue multiplicity annotation valueResult bodyResult)) (branch CoreResolutionFailed identifier . (constructor CoreResolutionResult CoreResolutionFailed identifier))))))) def combineResolvedApplication : (pi unrestricted functionResult : (family CoreResolutionResult) . (pi unrestricted argumentResult : (family CoreResolutionResult) . (family CoreResolutionResult))) = (lambda unrestricted functionResult : (family CoreResolutionResult) . (lambda unrestricted argumentResult : (family CoreResolutionResult) . (eliminate CoreResolutionResult (lambda unrestricted value : (family CoreResolutionResult) . (family CoreResolutionResult)) functionResult (branch CoreResolved function . (eliminate CoreResolutionResult (lambda unrestricted value : (family CoreResolutionResult) . (family CoreResolutionResult)) argumentResult (branch CoreResolved argument . (constructor CoreResolutionResult CoreResolved (constructor CoreTerm CoreApplication function argument))) (branch CoreResolutionFailed identifier . (constructor CoreResolutionResult CoreResolutionFailed identifier)))) (branch CoreResolutionFailed identifier . (constructor CoreResolutionResult CoreResolutionFailed identifier))))) def combineResolvedNaturalSuccessor : (pi unrestricted predecessorResult : (family CoreResolutionResult) . (family CoreResolutionResult)) = (lambda unrestricted predecessorResult : (family CoreResolutionResult) . (eliminate CoreResolutionResult (lambda unrestricted result : (family CoreResolutionResult) . (family CoreResolutionResult)) predecessorResult (branch CoreResolved predecessor . (constructor CoreResolutionResult CoreResolved (constructor CoreTerm CoreNaturalSuccessor predecessor))) (branch CoreResolutionFailed identifier . (constructor CoreResolutionResult CoreResolutionFailed identifier)))) def combineResolvedTermSequence : (pi unrestricted headResult : (family CoreResolutionResult) . (pi unrestricted tailResult : (family CoreResolutionResult) . (family CoreResolutionResult))) = (lambda unrestricted headResult : (family CoreResolutionResult) . (lambda unrestricted tailResult : (family CoreResolutionResult) . (eliminate CoreResolutionResult (lambda unrestricted value : (family CoreResolutionResult) . (family CoreResolutionResult)) headResult (branch CoreResolved head . (eliminate CoreResolutionResult (lambda unrestricted value : (family CoreResolutionResult) . (family CoreResolutionResult)) tailResult (branch CoreResolved tail . (constructor CoreResolutionResult CoreResolved (constructor CoreTerm CoreTermSequenceNext head tail))) (branch CoreResolutionFailed identifier . (constructor CoreResolutionResult CoreResolutionFailed identifier)))) (branch CoreResolutionFailed identifier . (constructor CoreResolutionResult CoreResolutionFailed identifier))))) def combineResolvedFamilyApplication : (pi unrestricted familyName : Bytes . (pi unrestricted argumentResult : (family CoreResolutionResult) . (family CoreResolutionResult))) = (lambda unrestricted familyName : Bytes . (lambda unrestricted argumentResult : (family CoreResolutionResult) . (eliminate CoreResolutionResult (lambda unrestricted value : (family CoreResolutionResult) . (family CoreResolutionResult)) argumentResult (branch CoreResolved arguments . (constructor CoreResolutionResult CoreResolved (constructor CoreTerm CoreFamilyApplication familyName arguments))) (branch CoreResolutionFailed identifier . (constructor CoreResolutionResult CoreResolutionFailed identifier))))) def combineResolvedConstructorApplication : (pi unrestricted familyName : Bytes . (pi unrestricted constructorName : Bytes . (pi unrestricted argumentResult : (family CoreResolutionResult) . (family CoreResolutionResult)))) = (lambda unrestricted familyName : Bytes . (lambda unrestricted constructorName : Bytes . (lambda unrestricted argumentResult : (family CoreResolutionResult) . (eliminate CoreResolutionResult (lambda unrestricted value : (family CoreResolutionResult) . (family CoreResolutionResult)) argumentResult (branch CoreResolved arguments . (constructor CoreResolutionResult CoreResolved (constructor CoreTerm CoreConstructorApplication familyName constructorName arguments))) (branch CoreResolutionFailed identifier . (constructor CoreResolutionResult CoreResolutionFailed identifier)))))) def inspectNamedCoreVariable = (lambda unrestricted term : (family NamedCoreTerm) . (eliminate NamedCoreTerm (lambda unrestricted value : (family NamedCoreTerm) . (family NamedCoreVariableInspection)) term (branch NamedCoreUniverse level . (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable)) (branch NamedCoreNatural . (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable)) (branch NamedCoreNaturalLiteral value . (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable)) (branch NamedCoreVariable identifier . (constructor NamedCoreVariableInspection NamedCoreVariableFound identifier)) (branch NamedCorePi multiplicity binder domain codomain ih_domain ih_codomain . (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable)) (branch NamedCoreLambda multiplicity binder domain body ih_domain ih_body . (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable)) (branch NamedCoreLet multiplicity binder annotation value body ih_annotation ih_value ih_body . (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable)) (branch NamedCoreApplication function argument ih_function ih_argument . (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable)) (branch NamedCoreNaturalArithmetic operation function argument ih_function ih_argument . (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable)) (branch NamedCoreNaturalSuccessor predecessor ih_predecessor . (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable)) (branch NamedCoreByte . (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable)) (branch NamedCoreByteLiteral value . (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable)) (branch NamedCoreBytes . (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable)) (branch NamedCoreBytesLiteral value . (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable)) (branch NamedCoreTermSequenceEnd . (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable)) (branch NamedCoreTermSequenceNext head tail ih_head ih_tail . (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable)) (branch NamedCoreFamilyApplication familyName arguments ih_arguments . (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable)) (branch NamedCoreConstructorApplication familyName constructorName arguments ih_arguments . (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable)) (branch NamedCoreEliminatorBranch constructorName binderNames body ih_binderNames ih_body . (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable)) (branch NamedCoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable)))) def extendEliminatorBranchScope = (lambda unrestricted identifier : Bytes . (lambda unrestricted tailResolution : (family EliminatorBranchScopeResolution) . (eliminate EliminatorBranchScopeResolution (lambda unrestricted value : (family EliminatorBranchScopeResolution) . (family EliminatorBranchScopeResolution)) tailResolution (branch EliminatorBranchScopeResolved scope binderCount . (constructor EliminatorBranchScopeResolution EliminatorBranchScopeResolved (constructor NameScope NameScopeBinding identifier scope) (succ binderCount))) (branch EliminatorBranchScopeRejected . (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected))))) def resolveEliminatorBranchScope = (lambda unrestricted binders : (family NamedCoreTerm) . (eliminate NamedCoreTerm (lambda unrestricted value : (family NamedCoreTerm) . (pi unrestricted scope : (family NameScope) . (family EliminatorBranchScopeResolution))) binders (branch NamedCoreUniverse level . (lambda unrestricted scope : (family NameScope) . (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected))) (branch NamedCoreNatural . (lambda unrestricted scope : (family NameScope) . (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected))) (branch NamedCoreNaturalLiteral value . (lambda unrestricted scope : (family NameScope) . (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected))) (branch NamedCoreVariable identifier . (lambda unrestricted scope : (family NameScope) . (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected))) (branch NamedCorePi multiplicity binder domain codomain ih_domain ih_codomain . (lambda unrestricted scope : (family NameScope) . (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected))) (branch NamedCoreLambda multiplicity binder domain body ih_domain ih_body . (lambda unrestricted scope : (family NameScope) . (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected))) (branch NamedCoreLet multiplicity binder annotation value body ih_annotation ih_value ih_body . (lambda unrestricted scope : (family NameScope) . (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected))) (branch NamedCoreApplication function argument ih_function ih_argument . (lambda unrestricted scope : (family NameScope) . (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected))) (branch NamedCoreNaturalArithmetic operation function argument ih_function ih_argument . (lambda unrestricted scope : (family NameScope) . (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected))) (branch NamedCoreNaturalSuccessor predecessor ih_predecessor . (lambda unrestricted scope : (family NameScope) . (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected))) (branch NamedCoreByte . (lambda unrestricted scope : (family NameScope) . (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected))) (branch NamedCoreByteLiteral value . (lambda unrestricted scope : (family NameScope) . (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected))) (branch NamedCoreBytes . (lambda unrestricted scope : (family NameScope) . (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected))) (branch NamedCoreBytesLiteral value . (lambda unrestricted scope : (family NameScope) . (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected))) (branch NamedCoreTermSequenceEnd . (lambda unrestricted scope : (family NameScope) . (constructor EliminatorBranchScopeResolution EliminatorBranchScopeResolved scope zero))) (branch NamedCoreTermSequenceNext head tail ih_head ih_tail . (lambda unrestricted scope : (family NameScope) . (eliminate NamedCoreVariableInspection (lambda unrestricted inspection : (family NamedCoreVariableInspection) . (family EliminatorBranchScopeResolution)) (inspectNamedCoreVariable head) (branch NamedCoreVariableFound identifier . (extendEliminatorBranchScope identifier (ih_tail scope))) (branch NamedCoreTermIsNotVariable . (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected))))) (branch NamedCoreFamilyApplication familyName arguments ih_arguments . (lambda unrestricted scope : (family NameScope) . (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected))) (branch NamedCoreConstructorApplication familyName constructorName arguments ih_arguments . (lambda unrestricted scope : (family NameScope) . (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected))) (branch NamedCoreEliminatorBranch constructorName binderNames body ih_binderNames ih_body . (lambda unrestricted scope : (family NameScope) . (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected))) (branch NamedCoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . (lambda unrestricted scope : (family NameScope) . (constructor EliminatorBranchScopeResolution EliminatorBranchScopeRejected))))) def finishResolvedEliminatorBranch = (lambda unrestricted constructorName : Bytes . (lambda unrestricted binderCount : Nat . (lambda unrestricted bodyResult : (family CoreResolutionResult) . (eliminate CoreResolutionResult (lambda unrestricted value : (family CoreResolutionResult) . (family CoreResolutionResult)) bodyResult (branch CoreResolved body . (constructor CoreResolutionResult CoreResolved (constructor CoreTerm CoreEliminatorBranch constructorName binderCount body))) (branch CoreResolutionFailed identifier . (constructor CoreResolutionResult CoreResolutionFailed identifier)))))) def finishResolvedEliminatorBranchScope = (lambda unrestricted constructorName : Bytes . (lambda unrestricted resolveBody : (pi unrestricted scope : (family NameScope) . (family CoreResolutionResult)) . (lambda unrestricted scopeResolution : (family EliminatorBranchScopeResolution) . (eliminate EliminatorBranchScopeResolution (lambda unrestricted value : (family EliminatorBranchScopeResolution) . (family CoreResolutionResult)) scopeResolution (branch EliminatorBranchScopeResolved scope binderCount . (finishResolvedEliminatorBranch constructorName binderCount (resolveBody scope))) (branch EliminatorBranchScopeRejected . (constructor CoreResolutionResult CoreResolutionFailed constructorName)))))) def combineResolvedEliminator = (lambda unrestricted familyName : Bytes . (lambda unrestricted motiveResult : (family CoreResolutionResult) . (lambda unrestricted scrutineeResult : (family CoreResolutionResult) . (lambda unrestricted branchesResult : (family CoreResolutionResult) . (eliminate CoreResolutionResult (lambda unrestricted value : (family CoreResolutionResult) . (family CoreResolutionResult)) motiveResult (branch CoreResolved motive . (eliminate CoreResolutionResult (lambda unrestricted value : (family CoreResolutionResult) . (family CoreResolutionResult)) scrutineeResult (branch CoreResolved scrutinee . (eliminate CoreResolutionResult (lambda unrestricted value : (family CoreResolutionResult) . (family CoreResolutionResult)) branchesResult (branch CoreResolved branches . (constructor CoreResolutionResult CoreResolved (constructor CoreTerm CoreEliminator familyName motive scrutinee branches))) (branch CoreResolutionFailed identifier . (constructor CoreResolutionResult CoreResolutionFailed identifier)))) (branch CoreResolutionFailed identifier . (constructor CoreResolutionResult CoreResolutionFailed identifier)))) (branch CoreResolutionFailed identifier . (constructor CoreResolutionResult CoreResolutionFailed identifier))))))) def combineResolvedArithmetic = (lambda unrestricted operation : (family CoreNaturalOperation) . (lambda unrestricted functionResult : (family CoreResolutionResult) . (lambda unrestricted argumentResult : (family CoreResolutionResult) . (eliminate CoreResolutionResult (lambda unrestricted value : (family CoreResolutionResult) . (family CoreResolutionResult)) functionResult (branch CoreResolved function . (eliminate CoreResolutionResult (lambda unrestricted value : (family CoreResolutionResult) . (family CoreResolutionResult)) argumentResult (branch CoreResolved argument . (constructor CoreResolutionResult CoreResolved (constructor CoreTerm CoreNaturalArithmetic operation function argument))) (branch CoreResolutionFailed identifier . (constructor CoreResolutionResult CoreResolutionFailed identifier)))) (branch CoreResolutionFailed identifier . (constructor CoreResolutionResult CoreResolutionFailed identifier)))))) def resolveNamedCore : (pi unrestricted term : (family NamedCoreTerm) . (pi unrestricted scope : (family NameScope) . (family CoreResolutionResult))) = (lambda unrestricted term : (family NamedCoreTerm) . (eliminate NamedCoreTerm (lambda unrestricted value : (family NamedCoreTerm) . (pi unrestricted scope : (family NameScope) . (family CoreResolutionResult))) term (branch NamedCoreUniverse level . (lambda unrestricted scope : (family NameScope) . (constructor CoreResolutionResult CoreResolved (constructor CoreTerm CoreUniverse level)))) (branch NamedCoreNatural . (lambda unrestricted scope : (family NameScope) . (constructor CoreResolutionResult CoreResolved (constructor CoreTerm CoreNatural)))) (branch NamedCoreNaturalLiteral value . (lambda unrestricted scope : (family NameScope) . (constructor CoreResolutionResult CoreResolved (constructor CoreTerm CoreNaturalLiteral value)))) (branch NamedCoreVariable identifier . (lambda unrestricted scope : (family NameScope) . (eliminate NameLookupResult (lambda unrestricted result : (family NameLookupResult) . (family CoreResolutionResult)) (lookupName scope identifier) (branch NameFound index . (constructor CoreResolutionResult CoreResolved (constructor CoreTerm CoreBound index))) (branch NameNotFound missingIdentifier . (resolveCorePrimitiveName missingIdentifier))))) (branch NamedCorePi multiplicity binder domain codomain ih_domain ih_codomain . (lambda unrestricted scope : (family NameScope) . (combineResolvedPi multiplicity (ih_domain scope) (ih_codomain (constructor NameScope NameScopeBinding binder scope))))) (branch NamedCoreLambda multiplicity binder domain body ih_domain ih_body . (lambda unrestricted scope : (family NameScope) . (combineResolvedLambda multiplicity (ih_domain scope) (ih_body (constructor NameScope NameScopeBinding binder scope))))) (branch NamedCoreLet multiplicity binder annotation value body ih_annotation ih_value ih_body . (lambda unrestricted scope : (family NameScope) . (combineResolvedLet multiplicity (ih_annotation scope) (ih_value scope) (ih_body (constructor NameScope NameScopeBinding binder scope))))) (branch NamedCoreApplication function argument ih_function ih_argument . (lambda unrestricted scope : (family NameScope) . (combineResolvedApplication (ih_function scope) (ih_argument scope)))) (branch NamedCoreNaturalArithmetic operation function argument ih_function ih_argument . (lambda unrestricted scope : (family NameScope) . (combineResolvedArithmetic operation (ih_function scope) (ih_argument scope)))) (branch NamedCoreNaturalSuccessor predecessor ih_predecessor . (lambda unrestricted scope : (family NameScope) . (combineResolvedNaturalSuccessor (ih_predecessor scope)))) (branch NamedCoreByte . (lambda unrestricted scope : (family NameScope) . (constructor CoreResolutionResult CoreResolved (constructor CoreTerm CoreByte)))) (branch NamedCoreByteLiteral value . (lambda unrestricted scope : (family NameScope) . (constructor CoreResolutionResult CoreResolved (constructor CoreTerm CoreByteLiteral value)))) (branch NamedCoreBytes . (lambda unrestricted scope : (family NameScope) . (constructor CoreResolutionResult CoreResolved (constructor CoreTerm CoreBytes)))) (branch NamedCoreBytesLiteral value . (lambda unrestricted scope : (family NameScope) . (constructor CoreResolutionResult CoreResolved (constructor CoreTerm CoreBytesLiteral value)))) (branch NamedCoreTermSequenceEnd . (lambda unrestricted scope : (family NameScope) . (constructor CoreResolutionResult CoreResolved (constructor CoreTerm CoreTermSequenceEnd)))) (branch NamedCoreTermSequenceNext head tail ih_head ih_tail . (lambda unrestricted scope : (family NameScope) . (combineResolvedTermSequence (ih_head scope) (ih_tail scope)))) (branch NamedCoreFamilyApplication familyName arguments ih_arguments . (lambda unrestricted scope : (family NameScope) . (combineResolvedFamilyApplication familyName (ih_arguments scope)))) (branch NamedCoreConstructorApplication familyName constructorName arguments ih_arguments . (lambda unrestricted scope : (family NameScope) . (combineResolvedConstructorApplication familyName constructorName (ih_arguments scope)))) (branch NamedCoreEliminatorBranch constructorName binderNames body ih_binderNames ih_body . (lambda unrestricted scope : (family NameScope) . (finishResolvedEliminatorBranchScope constructorName ih_body (resolveEliminatorBranchScope binderNames scope)))) (branch NamedCoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . (lambda unrestricted scope : (family NameScope) . (combineResolvedEliminator familyName (ih_motive scope) (ih_scrutinee scope) (ih_branches scope)))))) def resolveClosedNamedCore : (pi unrestricted term : (family NamedCoreTerm) . (family CoreResolutionResult)) = (lambda unrestricted term : (family NamedCoreTerm) . (resolveNamedCore term (constructor NameScope EmptyNameScope))) -- Part of `shiftCore`, lifted out to keep it inside the §28.3 size and -- nesting limits; the parameters are the locals it still needs. def shiftCorePart1 = (lambda unrestricted index : Nat . (lambda unrestricted cutoff : Nat . (lambda unrestricted amount : Nat . (nat-eliminate (lambda unrestricted condition : Nat . (family CoreTerm)) (constructor CoreTerm CoreBound (naturalAdd index amount)) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family CoreTerm) . (constructor CoreTerm CoreBound index))) (nat-less-than index cutoff))))) def shiftCore : (pi unrestricted term : (family CoreTerm) . (pi unrestricted cutoff : Nat . (pi unrestricted amount : Nat . (family CoreTerm)))) = (lambda unrestricted term : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted value : (family CoreTerm) . (pi unrestricted cutoff : Nat . (pi unrestricted amount : Nat . (family CoreTerm)))) term (branch CoreUniverse level . (lambda unrestricted cutoff : Nat . (lambda unrestricted amount : Nat . (constructor CoreTerm CoreUniverse level)))) (branch CoreNatural . (lambda unrestricted cutoff : Nat . (lambda unrestricted amount : Nat . (constructor CoreTerm CoreNatural)))) (branch CoreNaturalLiteral value . (lambda unrestricted cutoff : Nat . (lambda unrestricted amount : Nat . (constructor CoreTerm CoreNaturalLiteral value)))) (branch CoreBound index . (shiftCorePart1 index)) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . (lambda unrestricted cutoff : Nat . (lambda unrestricted amount : Nat . (constructor CoreTerm CorePi multiplicity (ih_domain cutoff amount) (ih_codomain (succ cutoff) amount))))) (branch CoreLambda multiplicity domain body ih_domain ih_body . (lambda unrestricted cutoff : Nat . (lambda unrestricted amount : Nat . (constructor CoreTerm CoreLambda multiplicity (ih_domain cutoff amount) (ih_body (succ cutoff) amount))))) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . (lambda unrestricted cutoff : Nat . (lambda unrestricted amount : Nat . (constructor CoreTerm CoreLet multiplicity (ih_annotation cutoff amount) (ih_value cutoff amount) (ih_body (succ cutoff) amount))))) (branch CoreApplication function argument ih_function ih_argument . (lambda unrestricted cutoff : Nat . (lambda unrestricted amount : Nat . (constructor CoreTerm CoreApplication (ih_function cutoff amount) (ih_argument cutoff amount))))) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . (lambda unrestricted cutoff : Nat . (lambda unrestricted amount : Nat . (constructor CoreTerm CoreNaturalArithmetic operation (ih_function cutoff amount) (ih_argument cutoff amount))))) (branch CoreNaturalSuccessor predecessor ih_predecessor . (lambda unrestricted cutoff : Nat . (lambda unrestricted amount : Nat . (constructor CoreTerm CoreNaturalSuccessor (ih_predecessor cutoff amount))))) (branch CoreByte . (lambda unrestricted cutoff : Nat . (lambda unrestricted amount : Nat . (constructor CoreTerm CoreByte)))) (branch CoreByteLiteral value . (lambda unrestricted cutoff : Nat . (lambda unrestricted amount : Nat . (constructor CoreTerm CoreByteLiteral value)))) (branch CoreBytes . (lambda unrestricted cutoff : Nat . (lambda unrestricted amount : Nat . (constructor CoreTerm CoreBytes)))) (branch CoreBytesLiteral value . (lambda unrestricted cutoff : Nat . (lambda unrestricted amount : Nat . (constructor CoreTerm CoreBytesLiteral value)))) (branch CorePrimitiveTerm primitive . (lambda unrestricted cutoff : Nat . (lambda unrestricted amount : Nat . (constructor CoreTerm CorePrimitiveTerm primitive)))) (branch CoreTermSequenceEnd . (lambda unrestricted cutoff : Nat . (lambda unrestricted amount : Nat . (constructor CoreTerm CoreTermSequenceEnd)))) (branch CoreTermSequenceNext head tail ih_head ih_tail . (lambda unrestricted cutoff : Nat . (lambda unrestricted amount : Nat . (constructor CoreTerm CoreTermSequenceNext (ih_head cutoff amount) (ih_tail cutoff amount))))) (branch CoreFamilyApplication familyName arguments ih_arguments . (lambda unrestricted cutoff : Nat . (lambda unrestricted amount : Nat . (constructor CoreTerm CoreFamilyApplication familyName (ih_arguments cutoff amount))))) (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . (lambda unrestricted cutoff : Nat . (lambda unrestricted amount : Nat . (constructor CoreTerm CoreConstructorApplication familyName constructorName (ih_arguments cutoff amount))))) (branch CoreEliminatorBranch constructorName binderCount body ih_body . (lambda unrestricted cutoff : Nat . (lambda unrestricted amount : Nat . (constructor CoreTerm CoreEliminatorBranch constructorName binderCount (ih_body (naturalAdd cutoff binderCount) amount))))) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . (lambda unrestricted cutoff : Nat . (lambda unrestricted amount : Nat . (constructor CoreTerm CoreEliminator familyName (ih_motive cutoff amount) (ih_scrutinee cutoff amount) (ih_branches cutoff amount))))))) def shiftCoreBy : (pi unrestricted amount : Nat . (pi unrestricted term : (family CoreTerm) . (family CoreTerm))) = (lambda unrestricted amount : Nat . (lambda unrestricted term : (family CoreTerm) . (shiftCore term zero amount))) -- Part of `substituteCore`, lifted out to keep it inside the §28.3 size and -- nesting limits; the parameters are the locals it still needs. def substituteCorePart1 = (lambda unrestricted index : Nat . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (nat-eliminate (lambda unrestricted equalCondition : Nat . (family CoreTerm)) (nat-eliminate (lambda unrestricted greaterCondition : Nat . (family CoreTerm)) (constructor CoreTerm CoreBound index) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family CoreTerm) . (constructor CoreTerm CoreBound (naturalPredecessor index)))) (nat-less-than depth index)) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family CoreTerm) . (shiftCore replacement zero depth))) (naturalEqual index depth))))) -- Part of `substituteCore`, lifted out to keep it inside the §28.3 size and -- nesting limits; the parameters are the locals it still needs. def substituteCorePart2 = (lambda unrestricted multiplicity : (family CoreMultiplicity) . (lambda unrestricted ih_domain : (pi unrestricted depth : Nat . (pi unrestricted replacement : (family CoreTerm) . (family CoreTerm))) . (lambda unrestricted ih_codomain : (pi unrestricted depth : Nat . (pi unrestricted replacement : (family CoreTerm) . (family CoreTerm))) . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (constructor CoreTerm CorePi multiplicity (ih_domain depth replacement) (ih_codomain (succ depth) replacement))))))) def substituteCore : (pi unrestricted term : (family CoreTerm) . (pi unrestricted depth : Nat . (pi unrestricted replacement : (family CoreTerm) . (family CoreTerm)))) = (lambda unrestricted term : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted value : (family CoreTerm) . (pi unrestricted depth : Nat . (pi unrestricted replacement : (family CoreTerm) . (family CoreTerm)))) term (branch CoreUniverse level . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (constructor CoreTerm CoreUniverse level)))) (branch CoreNatural . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (constructor CoreTerm CoreNatural)))) (branch CoreNaturalLiteral value . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (constructor CoreTerm CoreNaturalLiteral value)))) (branch CoreBound index . (substituteCorePart1 index)) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . (substituteCorePart2 multiplicity ih_domain ih_codomain)) (branch CoreLambda multiplicity domain body ih_domain ih_body . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (constructor CoreTerm CoreLambda multiplicity (ih_domain depth replacement) (ih_body (succ depth) replacement))))) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (constructor CoreTerm CoreLet multiplicity (ih_annotation depth replacement) (ih_value depth replacement) (ih_body (succ depth) replacement))))) (branch CoreApplication function argument ih_function ih_argument . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (constructor CoreTerm CoreApplication (ih_function depth replacement) (ih_argument depth replacement))))) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (constructor CoreTerm CoreNaturalArithmetic operation (ih_function depth replacement) (ih_argument depth replacement))))) (branch CoreNaturalSuccessor predecessor ih_predecessor . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (constructor CoreTerm CoreNaturalSuccessor (ih_predecessor depth replacement))))) (branch CoreByte . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (constructor CoreTerm CoreByte)))) (branch CoreByteLiteral value . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (constructor CoreTerm CoreByteLiteral value)))) (branch CoreBytes . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (constructor CoreTerm CoreBytes)))) (branch CoreBytesLiteral value . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (constructor CoreTerm CoreBytesLiteral value)))) (branch CorePrimitiveTerm primitive . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (constructor CoreTerm CorePrimitiveTerm primitive)))) (branch CoreTermSequenceEnd . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (constructor CoreTerm CoreTermSequenceEnd)))) (branch CoreTermSequenceNext head tail ih_head ih_tail . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (constructor CoreTerm CoreTermSequenceNext (ih_head depth replacement) (ih_tail depth replacement))))) (branch CoreFamilyApplication familyName arguments ih_arguments . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (constructor CoreTerm CoreFamilyApplication familyName (ih_arguments depth replacement))))) (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (constructor CoreTerm CoreConstructorApplication familyName constructorName (ih_arguments depth replacement))))) (branch CoreEliminatorBranch constructorName binderCount body ih_body . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (constructor CoreTerm CoreEliminatorBranch constructorName binderCount (ih_body (naturalAdd depth binderCount) replacement))))) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (constructor CoreTerm CoreEliminator familyName (ih_motive depth replacement) (ih_scrutinee depth replacement) (ih_branches depth replacement))))))) def substituteCoreTop : (pi unrestricted replacement : (family CoreTerm) . (pi unrestricted body : (family CoreTerm) . (family CoreTerm))) = (lambda unrestricted replacement : (family CoreTerm) . (lambda unrestricted body : (family CoreTerm) . (substituteCore body zero replacement))) def reduceCoreTypeApplication : (pi unrestricted function : (family CoreTerm) . (pi unrestricted argument : (family CoreTerm) . (family CoreTerm))) = (lambda unrestricted function : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted value : (family CoreTerm) . (pi unrestricted argument : (family CoreTerm) . (family CoreTerm))) function (branch CoreUniverse level . (lambda unrestricted argument : (family CoreTerm) . (constructor CoreTerm CoreApplication function argument))) (branch CoreNatural . (lambda unrestricted argument : (family CoreTerm) . (constructor CoreTerm CoreApplication function argument))) (branch CoreNaturalLiteral value . (lambda unrestricted argument : (family CoreTerm) . (constructor CoreTerm CoreApplication function argument))) (branch CoreBound index . (lambda unrestricted argument : (family CoreTerm) . (constructor CoreTerm CoreApplication function argument))) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . (lambda unrestricted argument : (family CoreTerm) . (constructor CoreTerm CoreApplication function argument))) (branch CoreLambda multiplicity domain body ih_domain ih_body . (lambda unrestricted argument : (family CoreTerm) . (substituteCoreTop argument body))) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . (lambda unrestricted argument : (family CoreTerm) . (constructor CoreTerm CoreApplication function argument))) (branch CoreApplication nestedFunction nestedArgument ih_nestedFunction ih_nestedArgument . (lambda unrestricted argument : (family CoreTerm) . (constructor CoreTerm CoreApplication function argument))) (branch CoreNaturalArithmetic operation nestedFunction nestedArgument ih_nestedFunction ih_nestedArgument . (lambda unrestricted argument : (family CoreTerm) . (constructor CoreTerm CoreApplication function argument))) (branch CoreNaturalSuccessor predecessor ih_predecessor . (lambda unrestricted argument : (family CoreTerm) . (constructor CoreTerm CoreApplication function argument))) (branch CoreByte . (lambda unrestricted argument : (family CoreTerm) . (constructor CoreTerm CoreApplication function argument))) (branch CoreByteLiteral value . (lambda unrestricted argument : (family CoreTerm) . (constructor CoreTerm CoreApplication function argument))) (branch CoreBytes . (lambda unrestricted argument : (family CoreTerm) . (constructor CoreTerm CoreApplication function argument))) (branch CoreBytesLiteral value . (lambda unrestricted argument : (family CoreTerm) . (constructor CoreTerm CoreApplication function argument))) (branch CorePrimitiveTerm primitive . (lambda unrestricted argument : (family CoreTerm) . (constructor CoreTerm CoreApplication function argument))) (branch CoreTermSequenceEnd . (lambda unrestricted argument : (family CoreTerm) . (constructor CoreTerm CoreApplication function argument))) (branch CoreTermSequenceNext head tail ih_head ih_tail . (lambda unrestricted argument : (family CoreTerm) . (constructor CoreTerm CoreApplication function argument))) (branch CoreFamilyApplication familyName arguments ih_arguments . (lambda unrestricted argument : (family CoreTerm) . (constructor CoreTerm CoreApplication function argument))) (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . (lambda unrestricted argument : (family CoreTerm) . (constructor CoreTerm CoreApplication function argument))) (branch CoreEliminatorBranch constructorName binderCount body ih_body . (lambda unrestricted argument : (family CoreTerm) . (constructor CoreTerm CoreApplication function argument))) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . (lambda unrestricted argument : (family CoreTerm) . (constructor CoreTerm CoreApplication function argument))))) def inspectCoreLiteral : (pi unrestricted term : (family CoreTerm) . (family CoreLiteralInspection)) = (lambda unrestricted term : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted value : (family CoreTerm) . (family CoreLiteralInspection)) term (branch CoreUniverse level . (constructor CoreLiteralInspection CoreNotLiteral)) (branch CoreNatural . (constructor CoreLiteralInspection CoreNotLiteral)) (branch CoreNaturalLiteral value . (constructor CoreLiteralInspection CoreNaturalInspected value)) (branch CoreBound index . (constructor CoreLiteralInspection CoreNotLiteral)) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . (constructor CoreLiteralInspection CoreNotLiteral)) (branch CoreLambda multiplicity domain body ih_domain ih_body . (constructor CoreLiteralInspection CoreNotLiteral)) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . (constructor CoreLiteralInspection CoreNotLiteral)) (branch CoreApplication function argument ih_function ih_argument . (constructor CoreLiteralInspection CoreNotLiteral)) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . (constructor CoreLiteralInspection CoreNotLiteral)) (branch CoreNaturalSuccessor predecessor ih_predecessor . (constructor CoreLiteralInspection CoreNotLiteral)) (branch CoreByte . (constructor CoreLiteralInspection CoreNotLiteral)) (branch CoreByteLiteral value . (constructor CoreLiteralInspection CoreByteInspected value)) (branch CoreBytes . (constructor CoreLiteralInspection CoreNotLiteral)) (branch CoreBytesLiteral value . (constructor CoreLiteralInspection CoreBytesInspected value)) (branch CorePrimitiveTerm primitive . (constructor CoreLiteralInspection CoreNotLiteral)) (branch CoreTermSequenceEnd . (constructor CoreLiteralInspection CoreNotLiteral)) (branch CoreTermSequenceNext head tail ih_head ih_tail . (constructor CoreLiteralInspection CoreNotLiteral)) (branch CoreFamilyApplication familyName arguments ih_arguments . (constructor CoreLiteralInspection CoreNotLiteral)) (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . (constructor CoreLiteralInspection CoreNotLiteral)) (branch CoreEliminatorBranch constructorName binderCount body ih_body . (constructor CoreLiteralInspection CoreNotLiteral)) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . (constructor CoreLiteralInspection CoreNotLiteral)))) def inspectCoreArithmeticRight = (lambda unrestricted operation : (family CoreNaturalOperation) . (lambda unrestricted left : Bytes . (lambda unrestricted right : (family CoreTerm) . (eliminate CoreLiteralInspection (lambda unrestricted current : (family CoreLiteralInspection) . (family CoreArithmeticInspection)) (inspectCoreLiteral right) (branch CoreNaturalInspected digits . (eliminate NaturalMagnitudeResult (lambda unrestricted result : (family NaturalMagnitudeResult) . (family CoreArithmeticInspection)) (evaluateCoreNaturalOperation operation left digits) (branch NaturalMagnitudeAccepted value . (constructor CoreArithmeticInspection CoreArithmeticValue value)) (branch NaturalMagnitudeRejected failure . (constructor CoreArithmeticInspection CoreArithmeticRejected failure)))) (branch CoreByteInspected value . (constructor CoreArithmeticInspection CoreArithmeticNeutral)) (branch CoreBytesInspected value . (constructor CoreArithmeticInspection CoreArithmeticNeutral)) (branch CoreNotLiteral . (constructor CoreArithmeticInspection CoreArithmeticNeutral)))))) -- Callers normalize the operands; an open operand remains neutral. def inspectCoreArithmetic = (lambda unrestricted operation : (family CoreNaturalOperation) . (lambda unrestricted left : (family CoreTerm) . (lambda unrestricted right : (family CoreTerm) . (eliminate CoreLiteralInspection (lambda unrestricted current : (family CoreLiteralInspection) . (family CoreArithmeticInspection)) (inspectCoreLiteral left) (branch CoreNaturalInspected digits . (inspectCoreArithmeticRight operation digits right)) (branch CoreByteInspected value . (constructor CoreArithmeticInspection CoreArithmeticNeutral)) (branch CoreBytesInspected value . (constructor CoreArithmeticInspection CoreArithmeticNeutral)) (branch CoreNotLiteral . (constructor CoreArithmeticInspection CoreArithmeticNeutral)))))) -- A term-returning reducer never manufactures an inadmissible literal. -- Checked inference and erasure expose the explicit rejection separately. def reduceCoreArithmetic = (lambda unrestricted operation : (family CoreNaturalOperation) . (lambda unrestricted left : (family CoreTerm) . (lambda unrestricted right : (family CoreTerm) . (eliminate CoreArithmeticInspection (lambda unrestricted result : (family CoreArithmeticInspection) . (family CoreTerm)) (inspectCoreArithmetic operation left right) (branch CoreArithmeticValue digits . (constructor CoreTerm CoreNaturalLiteral digits)) (branch CoreArithmeticNeutral . (constructor CoreTerm CoreNaturalArithmetic operation left right)) (branch CoreArithmeticRejected failure . (constructor CoreTerm CoreNaturalArithmetic operation left right)))))) def reduceCoreNaturalSuccessor : (pi unrestricted predecessor : (family CoreTerm) . (family CoreTerm)) = (lambda unrestricted predecessor : (family CoreTerm) . (eliminate CoreLiteralInspection (lambda unrestricted inspection : (family CoreLiteralInspection) . (family CoreTerm)) (inspectCoreLiteral predecessor) (branch CoreNaturalInspected value . (constructor CoreTerm CoreNaturalLiteral (Compiler.NaturalMagnitudeArithmetic/magnitudeSuccessor value))) (branch CoreByteInspected value . (constructor CoreTerm CoreNaturalSuccessor predecessor)) (branch CoreBytesInspected value . (constructor CoreTerm CoreNaturalSuccessor predecessor)) (branch CoreNotLiteral . (constructor CoreTerm CoreNaturalSuccessor predecessor)))) -- Closed successors normalize through the same literal reducer as evaluation. def normalizeCoreType : (pi unrestricted term : (family CoreTerm) . (family CoreTerm)) = (lambda unrestricted term : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted value : (family CoreTerm) . (family CoreTerm)) term (branch CoreUniverse level . (constructor CoreTerm CoreUniverse level)) (branch CoreNatural . (constructor CoreTerm CoreNatural)) (branch CoreNaturalLiteral value . (constructor CoreTerm CoreNaturalLiteral value)) (branch CoreBound index . (constructor CoreTerm CoreBound index)) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . (constructor CoreTerm CorePi multiplicity ih_domain ih_codomain)) (branch CoreLambda multiplicity domain body ih_domain ih_body . (constructor CoreTerm CoreLambda multiplicity ih_domain ih_body)) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . (substituteCoreTop ih_value ih_body)) (branch CoreApplication function argument ih_function ih_argument . (reduceCoreTypeApplication ih_function ih_argument)) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . (reduceCoreArithmetic operation ih_function ih_argument)) (branch CoreNaturalSuccessor predecessor ih_predecessor . (reduceCoreNaturalSuccessor ih_predecessor)) (branch CoreByte . (constructor CoreTerm CoreByte)) (branch CoreByteLiteral value . (constructor CoreTerm CoreByteLiteral value)) (branch CoreBytes . (constructor CoreTerm CoreBytes)) (branch CoreBytesLiteral value . (constructor CoreTerm CoreBytesLiteral value)) (branch CorePrimitiveTerm primitive . (constructor CoreTerm CorePrimitiveTerm primitive)) (branch CoreTermSequenceEnd . (constructor CoreTerm CoreTermSequenceEnd)) (branch CoreTermSequenceNext head tail ih_head ih_tail . (constructor CoreTerm CoreTermSequenceNext ih_head ih_tail)) (branch CoreFamilyApplication familyName arguments ih_arguments . (constructor CoreTerm CoreFamilyApplication familyName ih_arguments)) (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . (constructor CoreTerm CoreConstructorApplication familyName constructorName ih_arguments)) (branch CoreEliminatorBranch constructorName binderCount body ih_body . (constructor CoreTerm CoreEliminatorBranch constructorName binderCount ih_body)) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . (constructor CoreTerm CoreEliminator familyName ih_motive ih_scrutinee ih_branches)))) def coreUniverseEqual : (pi unrestricted level : Nat . (pi unrestricted right : (family CoreTerm) . Nat)) = (lambda unrestricted level : Nat . (lambda unrestricted right : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted value : (family CoreTerm) . Nat) right (branch CoreUniverse rightLevel . (naturalEqual level rightLevel)) (branch CoreNatural . zero) (branch CoreNaturalLiteral value . zero) (branch CoreBound index . zero) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero) (branch CoreLambda multiplicity domain body ih_domain ih_body . zero) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . zero) (branch CoreApplication function argument ih_function ih_argument . zero) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . zero) (branch CoreNaturalSuccessor predecessor ih_predecessor . zero) (branch CoreByte . zero) (branch CoreByteLiteral value . zero) (branch CoreBytes . zero) (branch CoreBytesLiteral value . zero) (branch CorePrimitiveTerm primitive . zero) (branch CoreTermSequenceEnd . zero) (branch CoreTermSequenceNext head tail ih_head ih_tail . zero) (branch CoreFamilyApplication familyName arguments ih_arguments . zero) (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . zero) (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . zero)))) def coreNaturalEqual : (pi unrestricted right : (family CoreTerm) . Nat) = (lambda unrestricted right : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted value : (family CoreTerm) . Nat) right (branch CoreUniverse level . zero) (branch CoreNatural . (succ zero)) (branch CoreNaturalLiteral value . zero) (branch CoreBound index . zero) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero) (branch CoreLambda multiplicity domain body ih_domain ih_body . zero) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . zero) (branch CoreApplication function argument ih_function ih_argument . zero) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . zero) (branch CoreNaturalSuccessor predecessor ih_predecessor . zero) (branch CoreByte . zero) (branch CoreByteLiteral value . zero) (branch CoreBytes . zero) (branch CoreBytesLiteral value . zero) (branch CorePrimitiveTerm primitive . zero) (branch CoreTermSequenceEnd . zero) (branch CoreTermSequenceNext head tail ih_head ih_tail . zero) (branch CoreFamilyApplication familyName arguments ih_arguments . zero) (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . zero) (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . zero))) def coreNaturalLiteralEqual : (pi unrestricted value : Bytes . (pi unrestricted right : (family CoreTerm) . Nat)) = (lambda unrestricted value : Bytes . (lambda unrestricted right : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted term : (family CoreTerm) . Nat) right (branch CoreUniverse level . zero) (branch CoreNatural . zero) (branch CoreNaturalLiteral rightValue . (bytes-equal value rightValue)) (branch CoreBound index . zero) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero) (branch CoreLambda multiplicity domain body ih_domain ih_body . zero) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . zero) (branch CoreApplication function argument ih_function ih_argument . zero) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . zero) (branch CoreNaturalSuccessor predecessor ih_predecessor . zero) (branch CoreByte . zero) (branch CoreByteLiteral rightValue . zero) (branch CoreBytes . zero) (branch CoreBytesLiteral rightValue . zero) (branch CorePrimitiveTerm primitive . zero) (branch CoreTermSequenceEnd . zero) (branch CoreTermSequenceNext head tail ih_head ih_tail . zero) (branch CoreFamilyApplication familyName arguments ih_arguments . zero) (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . zero) (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . zero)))) def coreBoundEqual : (pi unrestricted index : Nat . (pi unrestricted right : (family CoreTerm) . Nat)) = (lambda unrestricted index : Nat . (lambda unrestricted right : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted term : (family CoreTerm) . Nat) right (branch CoreUniverse level . zero) (branch CoreNatural . zero) (branch CoreNaturalLiteral value . zero) (branch CoreBound rightIndex . (naturalEqual index rightIndex)) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero) (branch CoreLambda multiplicity domain body ih_domain ih_body . zero) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . zero) (branch CoreApplication function argument ih_function ih_argument . zero) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . zero) (branch CoreNaturalSuccessor predecessor ih_predecessor . zero) (branch CoreByte . zero) (branch CoreByteLiteral value . zero) (branch CoreBytes . zero) (branch CoreBytesLiteral value . zero) (branch CorePrimitiveTerm primitive . zero) (branch CoreTermSequenceEnd . zero) (branch CoreTermSequenceNext head tail ih_head ih_tail . zero) (branch CoreFamilyApplication familyName arguments ih_arguments . zero) (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . zero) (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . zero)))) def corePiEqual : (pi unrestricted multiplicity : (family CoreMultiplicity) . (pi unrestricted domainEqual : (pi unrestricted right : (family CoreTerm) . Nat) . (pi unrestricted codomainEqual : (pi unrestricted right : (family CoreTerm) . Nat) . (pi unrestricted right : (family CoreTerm) . Nat)))) = (lambda unrestricted multiplicity : (family CoreMultiplicity) . (lambda unrestricted domainEqual : (pi unrestricted right : (family CoreTerm) . Nat) . (lambda unrestricted codomainEqual : (pi unrestricted right : (family CoreTerm) . Nat) . (lambda unrestricted right : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted term : (family CoreTerm) . Nat) right (branch CoreUniverse level . zero) (branch CoreNatural . zero) (branch CoreNaturalLiteral value . zero) (branch CoreBound index . zero) (branch CorePi rightMultiplicity rightDomain rightCodomain ih_rightDomain ih_rightCodomain . (coreNaturalAnd (multiplicityEqual multiplicity rightMultiplicity) (coreNaturalAnd (domainEqual rightDomain) (codomainEqual rightCodomain)))) (branch CoreLambda rightMultiplicity rightDomain rightBody ih_rightDomain ih_rightBody . zero) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . zero) (branch CoreApplication function argument ih_function ih_argument . zero) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . zero) (branch CoreNaturalSuccessor predecessor ih_predecessor . zero) (branch CoreByte . zero) (branch CoreByteLiteral value . zero) (branch CoreBytes . zero) (branch CoreBytesLiteral value . zero) (branch CorePrimitiveTerm primitive . zero) (branch CoreTermSequenceEnd . zero) (branch CoreTermSequenceNext head tail ih_head ih_tail . zero) (branch CoreFamilyApplication familyName arguments ih_arguments . zero) (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . zero) (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . zero)))))) def coreLambdaEqual : (pi unrestricted multiplicity : (family CoreMultiplicity) . (pi unrestricted domainEqual : (pi unrestricted right : (family CoreTerm) . Nat) . (pi unrestricted bodyEqual : (pi unrestricted right : (family CoreTerm) . Nat) . (pi unrestricted right : (family CoreTerm) . Nat)))) = (lambda unrestricted multiplicity : (family CoreMultiplicity) . (lambda unrestricted domainEqual : (pi unrestricted right : (family CoreTerm) . Nat) . (lambda unrestricted bodyEqual : (pi unrestricted right : (family CoreTerm) . Nat) . (lambda unrestricted right : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted term : (family CoreTerm) . Nat) right (branch CoreUniverse level . zero) (branch CoreNatural . zero) (branch CoreNaturalLiteral value . zero) (branch CoreBound index . zero) (branch CorePi rightMultiplicity rightDomain rightCodomain ih_rightDomain ih_rightCodomain . zero) (branch CoreLambda rightMultiplicity rightDomain rightBody ih_rightDomain ih_rightBody . (coreNaturalAnd (multiplicityEqual multiplicity rightMultiplicity) (coreNaturalAnd (domainEqual rightDomain) (bodyEqual rightBody)))) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . zero) (branch CoreApplication function argument ih_function ih_argument . zero) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . zero) (branch CoreNaturalSuccessor predecessor ih_predecessor . zero) (branch CoreByte . zero) (branch CoreByteLiteral value . zero) (branch CoreBytes . zero) (branch CoreBytesLiteral value . zero) (branch CorePrimitiveTerm primitive . zero) (branch CoreTermSequenceEnd . zero) (branch CoreTermSequenceNext head tail ih_head ih_tail . zero) (branch CoreFamilyApplication familyName arguments ih_arguments . zero) (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . zero) (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . zero)))))) def coreApplicationEqual : (pi unrestricted functionEqual : (pi unrestricted right : (family CoreTerm) . Nat) . (pi unrestricted argumentEqual : (pi unrestricted right : (family CoreTerm) . Nat) . (pi unrestricted right : (family CoreTerm) . Nat))) = (lambda unrestricted functionEqual : (pi unrestricted right : (family CoreTerm) . Nat) . (lambda unrestricted argumentEqual : (pi unrestricted right : (family CoreTerm) . Nat) . (lambda unrestricted right : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted term : (family CoreTerm) . Nat) right (branch CoreUniverse level . zero) (branch CoreNatural . zero) (branch CoreNaturalLiteral value . zero) (branch CoreBound index . zero) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero) (branch CoreLambda multiplicity domain body ih_domain ih_body . zero) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . zero) (branch CoreApplication rightFunction rightArgument ih_rightFunction ih_rightArgument . (coreNaturalAnd (functionEqual rightFunction) (argumentEqual rightArgument))) (branch CoreNaturalArithmetic operation rightFunction rightArgument ih_rightFunction ih_rightArgument . zero) (branch CoreNaturalSuccessor predecessor ih_predecessor . zero) (branch CoreByte . zero) (branch CoreByteLiteral value . zero) (branch CoreBytes . zero) (branch CoreBytesLiteral value . zero) (branch CorePrimitiveTerm primitive . zero) (branch CoreTermSequenceEnd . zero) (branch CoreTermSequenceNext head tail ih_head ih_tail . zero) (branch CoreFamilyApplication familyName arguments ih_arguments . zero) (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . zero) (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . zero))))) def coreArithmeticEqual = (lambda unrestricted operation : (family CoreNaturalOperation) . (lambda unrestricted functionEqual : (pi unrestricted right : (family CoreTerm) . Nat) . (lambda unrestricted argumentEqual : (pi unrestricted right : (family CoreTerm) . Nat) . (lambda unrestricted right : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted term : (family CoreTerm) . Nat) right (branch CoreUniverse level . zero) (branch CoreNatural . zero) (branch CoreNaturalLiteral value . zero) (branch CoreBound index . zero) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero) (branch CoreLambda multiplicity domain body ih_domain ih_body . zero) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . zero) (branch CoreApplication function argument ih_function ih_argument . zero) (branch CoreNaturalArithmetic rightOperation rightFunction rightArgument ih_rightFunction ih_rightArgument . (coreNaturalAnd (byte-equal (coreNaturalOperationCode operation) (coreNaturalOperationCode rightOperation)) (coreNaturalAnd (functionEqual rightFunction) (argumentEqual rightArgument)))) (branch CoreNaturalSuccessor predecessor ih_predecessor . zero) (branch CoreByte . zero) (branch CoreByteLiteral value . zero) (branch CoreBytes . zero) (branch CoreBytesLiteral value . zero) (branch CorePrimitiveTerm primitive . zero) (branch CoreTermSequenceEnd . zero) (branch CoreTermSequenceNext head tail ih_head ih_tail . zero) (branch CoreFamilyApplication familyName arguments ih_arguments . zero) (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . zero) (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . zero)))))) def coreNaturalSuccessorEqual : (pi unrestricted predecessorEqual : (pi unrestricted right : (family CoreTerm) . Nat) . (pi unrestricted right : (family CoreTerm) . Nat)) = (lambda unrestricted predecessorEqual : (pi unrestricted right : (family CoreTerm) . Nat) . (lambda unrestricted right : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted term : (family CoreTerm) . Nat) right (branch CoreUniverse level . zero) (branch CoreNatural . zero) (branch CoreNaturalLiteral value . zero) (branch CoreBound index . zero) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero) (branch CoreLambda multiplicity domain body ih_domain ih_body . zero) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . zero) (branch CoreApplication function argument ih_function ih_argument . zero) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . zero) (branch CoreNaturalSuccessor predecessor ih_predecessor . (predecessorEqual predecessor)) (branch CoreByte . zero) (branch CoreByteLiteral value . zero) (branch CoreBytes . zero) (branch CoreBytesLiteral value . zero) (branch CorePrimitiveTerm primitive . zero) (branch CoreTermSequenceEnd . zero) (branch CoreTermSequenceNext head tail ih_head ih_tail . zero) (branch CoreFamilyApplication familyName arguments ih_arguments . zero) (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . zero) (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . zero)))) def coreByteEqual : (pi unrestricted right : (family CoreTerm) . Nat) = (lambda unrestricted right : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted term : (family CoreTerm) . Nat) right (branch CoreUniverse level . zero) (branch CoreNatural . zero) (branch CoreNaturalLiteral value . zero) (branch CoreBound index . zero) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero) (branch CoreLambda multiplicity domain body ih_domain ih_body . zero) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . zero) (branch CoreApplication function argument ih_function ih_argument . zero) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . zero) (branch CoreNaturalSuccessor predecessor ih_predecessor . zero) (branch CoreByte . (succ zero)) (branch CoreByteLiteral value . zero) (branch CoreBytes . zero) (branch CoreBytesLiteral value . zero) (branch CorePrimitiveTerm primitive . zero) (branch CoreTermSequenceEnd . zero) (branch CoreTermSequenceNext head tail ih_head ih_tail . zero) (branch CoreFamilyApplication familyName arguments ih_arguments . zero) (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . zero) (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . zero))) def coreByteLiteralEqual : (pi unrestricted value : Byte . (pi unrestricted right : (family CoreTerm) . Nat)) = (lambda unrestricted value : Byte . (lambda unrestricted right : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted term : (family CoreTerm) . Nat) right (branch CoreUniverse level . zero) (branch CoreNatural . zero) (branch CoreNaturalLiteral rightValue . zero) (branch CoreBound index . zero) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero) (branch CoreLambda multiplicity domain body ih_domain ih_body . zero) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . zero) (branch CoreApplication function argument ih_function ih_argument . zero) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . zero) (branch CoreNaturalSuccessor predecessor ih_predecessor . zero) (branch CoreByte . zero) (branch CoreByteLiteral rightValue . (byte-equal value rightValue)) (branch CoreBytes . zero) (branch CoreBytesLiteral rightValue . zero) (branch CorePrimitiveTerm primitive . zero) (branch CoreTermSequenceEnd . zero) (branch CoreTermSequenceNext head tail ih_head ih_tail . zero) (branch CoreFamilyApplication familyName arguments ih_arguments . zero) (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . zero) (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . zero)))) def coreBytesTypeEqual : (pi unrestricted right : (family CoreTerm) . Nat) = (lambda unrestricted right : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted term : (family CoreTerm) . Nat) right (branch CoreUniverse level . zero) (branch CoreNatural . zero) (branch CoreNaturalLiteral value . zero) (branch CoreBound index . zero) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero) (branch CoreLambda multiplicity domain body ih_domain ih_body . zero) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . zero) (branch CoreApplication function argument ih_function ih_argument . zero) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . zero) (branch CoreNaturalSuccessor predecessor ih_predecessor . zero) (branch CoreByte . zero) (branch CoreByteLiteral value . zero) (branch CoreBytes . (succ zero)) (branch CoreBytesLiteral value . zero) (branch CorePrimitiveTerm primitive . zero) (branch CoreTermSequenceEnd . zero) (branch CoreTermSequenceNext head tail ih_head ih_tail . zero) (branch CoreFamilyApplication familyName arguments ih_arguments . zero) (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . zero) (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . zero))) def coreBytesLiteralEqual : (pi unrestricted value : Bytes . (pi unrestricted right : (family CoreTerm) . Nat)) = (lambda unrestricted value : Bytes . (lambda unrestricted right : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted term : (family CoreTerm) . Nat) right (branch CoreUniverse level . zero) (branch CoreNatural . zero) (branch CoreNaturalLiteral rightValue . zero) (branch CoreBound index . zero) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero) (branch CoreLambda multiplicity domain body ih_domain ih_body . zero) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . zero) (branch CoreApplication function argument ih_function ih_argument . zero) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . zero) (branch CoreNaturalSuccessor predecessor ih_predecessor . zero) (branch CoreByte . zero) (branch CoreByteLiteral rightValue . zero) (branch CoreBytes . zero) (branch CoreBytesLiteral rightValue . (coreBytesEqual value rightValue)) (branch CorePrimitiveTerm primitive . zero) (branch CoreTermSequenceEnd . zero) (branch CoreTermSequenceNext head tail ih_head ih_tail . zero) (branch CoreFamilyApplication familyName arguments ih_arguments . zero) (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . zero) (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . zero)))) def corePrimitiveCode : (pi unrestricted primitive : (family CorePrimitive) . Nat) = (lambda unrestricted primitive : (family CorePrimitive) . (eliminate CorePrimitive (lambda unrestricted value : (family CorePrimitive) . Nat) primitive (branch CoreByteEqual . zero) (branch CoreByteLess . (succ zero)) (branch CoreNaturalLess . (succ (succ zero))) (branch CoreNaturalToByte . (succ (succ (succ zero)))) (branch CoreByteToNatural . (succ (succ (succ (succ zero))))) (branch CoreBytesAppend . (succ (succ (succ (succ (succ zero)))))) (branch CoreBytesCons . (succ (succ (succ (succ (succ (succ zero))))))) (branch CoreBytesLength . (succ (succ (succ (succ (succ (succ (succ zero)))))))) (branch CoreNaturalEliminate . (succ (succ (succ (succ (succ (succ (succ (succ zero))))))))) (branch CoreBytesEliminate . (succ (succ (succ (succ (succ (succ (succ (succ (succ zero)))))))))) (branch CoreBytesEqual . (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ zero))))))))))) (branch CoreFileEffect . (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0))) (branch CoreEffects . (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0))) (branch CoreComputation . (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0))) (branch CoreReturn . (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0))) (branch CoreBind . (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0))) (branch CoreReadFile . (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0))) (branch CoreWriteFile . (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0))) (branch CoreLinuxOpenNode . (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0))) (branch CoreLinuxCloseNode . (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0))) (branch CoreLinuxIoctl . (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0))) (branch CoreLinuxMmap . (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0))) (branch CoreLinuxMunmap . (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0))) (branch CoreBytesSetIndex . (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0))) (branch CoreBytesIndexNonzero . (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0))) (branch CoreBytesSetFreeIndex . (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0))) (branch CoreBytesBuilderType . (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0))) (branch CoreBytesBuilderEmpty . (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0))) (branch CoreBytesBuilderChunk . (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0))) (branch CoreBytesBuilderAppend . (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0))) (branch CoreBytesBuilderBuild . (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0))) (branch CoreRuntimeImageV4Build . (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0))) (branch CoreBytesHead . (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0))) (branch CoreBytesTail . (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0))) (branch CoreBytesChecksum . (bytes-length (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0))))) def corePrimitiveTermEqual : (pi unrestricted primitive : (family CorePrimitive) . (pi unrestricted right : (family CoreTerm) . Nat)) = (lambda unrestricted primitive : (family CorePrimitive) . (lambda unrestricted right : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted term : (family CoreTerm) . Nat) right (branch CoreUniverse level . zero) (branch CoreNatural . zero) (branch CoreNaturalLiteral value . zero) (branch CoreBound index . zero) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero) (branch CoreLambda multiplicity domain body ih_domain ih_body . zero) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . zero) (branch CoreApplication function argument ih_function ih_argument . zero) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . zero) (branch CoreNaturalSuccessor predecessor ih_predecessor . zero) (branch CoreByte . zero) (branch CoreByteLiteral value . zero) (branch CoreBytes . zero) (branch CoreBytesLiteral value . zero) (branch CorePrimitiveTerm rightPrimitive . (naturalEqual (corePrimitiveCode primitive) (corePrimitiveCode rightPrimitive))) (branch CoreTermSequenceEnd . zero) (branch CoreTermSequenceNext head tail ih_head ih_tail . zero) (branch CoreFamilyApplication familyName arguments ih_arguments . zero) (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . zero) (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . zero)))) def coreTermSequenceEndEqual = (lambda unrestricted right : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted term : (family CoreTerm) . Nat) right (branch CoreUniverse level . zero) (branch CoreNatural . zero) (branch CoreNaturalLiteral value . zero) (branch CoreBound index . zero) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero) (branch CoreLambda multiplicity domain body ih_domain ih_body . zero) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . zero) (branch CoreApplication function argument ih_function ih_argument . zero) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . zero) (branch CoreNaturalSuccessor predecessor ih_predecessor . zero) (branch CoreByte . zero) (branch CoreByteLiteral value . zero) (branch CoreBytes . zero) (branch CoreBytesLiteral value . zero) (branch CorePrimitiveTerm rightPrimitive . zero) (branch CoreTermSequenceEnd . (succ zero)) (branch CoreTermSequenceNext head tail ih_head ih_tail . zero) (branch CoreFamilyApplication familyName arguments ih_arguments . zero) (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . zero) (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . zero))) def coreTermSequenceNextEqual = (lambda unrestricted headEqual : (pi unrestricted right : (family CoreTerm) . Nat) . (lambda unrestricted tailEqual : (pi unrestricted right : (family CoreTerm) . Nat) . (lambda unrestricted right : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted term : (family CoreTerm) . Nat) right (branch CoreUniverse level . zero) (branch CoreNatural . zero) (branch CoreNaturalLiteral value . zero) (branch CoreBound index . zero) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero) (branch CoreLambda multiplicity domain body ih_domain ih_body . zero) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . zero) (branch CoreApplication function argument ih_function ih_argument . zero) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . zero) (branch CoreNaturalSuccessor predecessor ih_predecessor . zero) (branch CoreByte . zero) (branch CoreByteLiteral value . zero) (branch CoreBytes . zero) (branch CoreBytesLiteral value . zero) (branch CorePrimitiveTerm rightPrimitive . zero) (branch CoreTermSequenceEnd . zero) (branch CoreTermSequenceNext head tail ih_head ih_tail . (coreNaturalAnd (headEqual head) (tailEqual tail))) (branch CoreFamilyApplication familyName arguments ih_arguments . zero) (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . zero) (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . zero))))) def coreFamilyApplicationEqual = (lambda unrestricted familyName : Bytes . (lambda unrestricted argumentsEqual : (pi unrestricted right : (family CoreTerm) . Nat) . (lambda unrestricted right : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted term : (family CoreTerm) . Nat) right (branch CoreUniverse level . zero) (branch CoreNatural . zero) (branch CoreNaturalLiteral value . zero) (branch CoreBound index . zero) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero) (branch CoreLambda multiplicity domain body ih_domain ih_body . zero) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . zero) (branch CoreApplication function argument ih_function ih_argument . zero) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . zero) (branch CoreNaturalSuccessor predecessor ih_predecessor . zero) (branch CoreByte . zero) (branch CoreByteLiteral value . zero) (branch CoreBytes . zero) (branch CoreBytesLiteral value . zero) (branch CorePrimitiveTerm rightPrimitive . zero) (branch CoreTermSequenceEnd . zero) (branch CoreTermSequenceNext head tail ih_head ih_tail . zero) (branch CoreFamilyApplication rightFamilyName arguments ih_arguments . (coreNaturalAnd (coreBytesEqual familyName rightFamilyName) (argumentsEqual arguments))) (branch CoreConstructorApplication rightFamilyName constructorName arguments ih_arguments . zero) (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero) (branch CoreEliminator rightFamilyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . zero))))) def coreConstructorApplicationEqual = (lambda unrestricted familyName : Bytes . (lambda unrestricted constructorName : Bytes . (lambda unrestricted argumentsEqual : (pi unrestricted right : (family CoreTerm) . Nat) . (lambda unrestricted right : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted value : (family CoreTerm) . Nat) right (branch CoreUniverse level . zero) (branch CoreNatural . zero) (branch CoreNaturalLiteral value . zero) (branch CoreBound index . zero) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero) (branch CoreLambda multiplicity domain body ih_domain ih_body . zero) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . zero) (branch CoreApplication function argument ih_function ih_argument . zero) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . zero) (branch CoreNaturalSuccessor predecessor ih_predecessor . zero) (branch CoreByte . zero) (branch CoreByteLiteral value . zero) (branch CoreBytes . zero) (branch CoreBytesLiteral value . zero) (branch CorePrimitiveTerm primitive . zero) (branch CoreTermSequenceEnd . zero) (branch CoreTermSequenceNext head tail ih_head ih_tail . zero) (branch CoreFamilyApplication rightFamilyName arguments ih_arguments . zero) (branch CoreConstructorApplication rightFamilyName rightConstructorName arguments ih_arguments . (coreNaturalAnd (coreNaturalAnd (coreBytesEqual familyName rightFamilyName) (coreBytesEqual constructorName rightConstructorName)) (argumentsEqual arguments))) (branch CoreEliminatorBranch rightConstructorName binderCount body ih_body . zero) (branch CoreEliminator rightFamilyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . zero)))))) def coreEliminatorBranchEqual = (lambda unrestricted constructorName : Bytes . (lambda unrestricted binderCount : Nat . (lambda unrestricted bodyEqual : (pi unrestricted right : (family CoreTerm) . Nat) . (lambda unrestricted right : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted value : (family CoreTerm) . Nat) right (branch CoreUniverse level . zero) (branch CoreNatural . zero) (branch CoreNaturalLiteral value . zero) (branch CoreBound index . zero) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero) (branch CoreLambda multiplicity domain body ih_domain ih_body . zero) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . zero) (branch CoreApplication function argument ih_function ih_argument . zero) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . zero) (branch CoreNaturalSuccessor predecessor ih_predecessor . zero) (branch CoreByte . zero) (branch CoreByteLiteral value . zero) (branch CoreBytes . zero) (branch CoreBytesLiteral value . zero) (branch CorePrimitiveTerm primitive . zero) (branch CoreTermSequenceEnd . zero) (branch CoreTermSequenceNext head tail ih_head ih_tail . zero) (branch CoreFamilyApplication familyName arguments ih_arguments . zero) (branch CoreConstructorApplication familyName rightConstructorName arguments ih_arguments . zero) (branch CoreEliminatorBranch rightConstructorName rightBinderCount rightBody ih_rightBody . (coreNaturalAnd (coreNaturalAnd (coreBytesEqual constructorName rightConstructorName) (naturalEqual binderCount rightBinderCount)) (bodyEqual rightBody))) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . zero)))))) def coreEliminatorEqual = (lambda unrestricted familyName : Bytes . (lambda unrestricted motiveEqual : (pi unrestricted right : (family CoreTerm) . Nat) . (lambda unrestricted scrutineeEqual : (pi unrestricted right : (family CoreTerm) . Nat) . (lambda unrestricted branchesEqual : (pi unrestricted right : (family CoreTerm) . Nat) . (lambda unrestricted right : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted value : (family CoreTerm) . Nat) right (branch CoreUniverse level . zero) (branch CoreNatural . zero) (branch CoreNaturalLiteral value . zero) (branch CoreBound index . zero) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero) (branch CoreLambda multiplicity domain body ih_domain ih_body . zero) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . zero) (branch CoreApplication function argument ih_function ih_argument . zero) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . zero) (branch CoreNaturalSuccessor predecessor ih_predecessor . zero) (branch CoreByte . zero) (branch CoreByteLiteral value . zero) (branch CoreBytes . zero) (branch CoreBytesLiteral value . zero) (branch CorePrimitiveTerm primitive . zero) (branch CoreTermSequenceEnd . zero) (branch CoreTermSequenceNext head tail ih_head ih_tail . zero) (branch CoreFamilyApplication rightFamilyName arguments ih_arguments . zero) (branch CoreConstructorApplication rightFamilyName constructorName arguments ih_arguments . zero) (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero) (branch CoreEliminator rightFamilyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . (coreNaturalAnd (coreNaturalAnd (coreNaturalAnd (coreBytesEqual familyName rightFamilyName) (motiveEqual motive)) (scrutineeEqual scrutinee)) (branchesEqual branches))))))))) def coreLetEqual = (lambda unrestricted multiplicity : (family CoreMultiplicity) . (lambda unrestricted annotationEqual : (pi unrestricted right : (family CoreTerm) . Nat) . (lambda unrestricted valueEqual : (pi unrestricted right : (family CoreTerm) . Nat) . (lambda unrestricted bodyEqual : (pi unrestricted right : (family CoreTerm) . Nat) . (lambda unrestricted right : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted current : (family CoreTerm) . Nat) right (branch CoreUniverse level . zero) (branch CoreNatural . zero) (branch CoreNaturalLiteral value . zero) (branch CoreBound index . zero) (branch CorePi m domain codomain ih_domain ih_codomain . zero) (branch CoreLambda m domain body ih_domain ih_body . zero) (branch CoreLet rightMultiplicity annotation value body ih_annotation ih_value ih_body . (coreNaturalAnd (multiplicityEqual multiplicity rightMultiplicity) (coreNaturalAnd (annotationEqual annotation) (coreNaturalAnd (valueEqual value) (bodyEqual body))))) (branch CoreApplication function argument ih_function ih_argument . zero) (branch CoreNaturalArithmetic operation left right ih_left ih_right . zero) (branch CoreNaturalSuccessor predecessor ih_predecessor . zero) (branch CoreByte . zero) (branch CoreByteLiteral value . zero) (branch CoreBytes . zero) (branch CoreBytesLiteral value . zero) (branch CorePrimitiveTerm primitive . zero) (branch CoreTermSequenceEnd . zero) (branch CoreTermSequenceNext head tail ih_head ih_tail . zero) (branch CoreFamilyApplication family arguments ih_arguments . zero) (branch CoreConstructorApplication family constructor arguments ih_arguments . zero) (branch CoreEliminatorBranch constructor count body ih_body . zero) (branch CoreEliminator family motive scrutinee branches ih_motive ih_scrutinee ih_branches . zero))))))) def coreTermEqual : (pi unrestricted left : (family CoreTerm) . (pi unrestricted right : (family CoreTerm) . Nat)) = (lambda unrestricted left : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted term : (family CoreTerm) . (pi unrestricted right : (family CoreTerm) . Nat)) left (branch CoreUniverse level . (coreUniverseEqual level)) (branch CoreNatural . coreNaturalEqual) (branch CoreNaturalLiteral value . (coreNaturalLiteralEqual value)) (branch CoreBound index . (coreBoundEqual index)) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . (corePiEqual multiplicity ih_domain ih_codomain)) (branch CoreLambda multiplicity domain body ih_domain ih_body . (coreLambdaEqual multiplicity ih_domain ih_body)) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . (coreLetEqual multiplicity ih_annotation ih_value ih_body)) (branch CoreApplication function argument ih_function ih_argument . (coreApplicationEqual ih_function ih_argument)) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . (coreArithmeticEqual operation ih_function ih_argument)) (branch CoreNaturalSuccessor predecessor ih_predecessor . (coreNaturalSuccessorEqual ih_predecessor)) (branch CoreByte . coreByteEqual) (branch CoreByteLiteral value . (coreByteLiteralEqual value)) (branch CoreBytes . coreBytesTypeEqual) (branch CoreBytesLiteral value . (coreBytesLiteralEqual value)) (branch CorePrimitiveTerm primitive . (corePrimitiveTermEqual primitive)) (branch CoreTermSequenceEnd . coreTermSequenceEndEqual) (branch CoreTermSequenceNext head tail ih_head ih_tail . (coreTermSequenceNextEqual ih_head ih_tail)) (branch CoreFamilyApplication familyName arguments ih_arguments . (coreFamilyApplicationEqual familyName ih_arguments)) (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . (coreConstructorApplicationEqual familyName constructorName ih_arguments)) (branch CoreEliminatorBranch constructorName binderCount body ih_body . (coreEliminatorBranchEqual constructorName binderCount ih_body)) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . (coreEliminatorEqual familyName ih_motive ih_scrutinee ih_branches)))) -- The existing compiler policy is 64 reduction rounds. Public callers can -- supply their own budget; this is not a bound on work within one round. def coreNormalizationDefaultRounds = (byte-to-nat (byte 64)) def coreNormalizationResourceFailureCode = (byte-to-nat (byte 89)) def countCoreReductionRound = (lambda unrestricted result : (family CoreReductionResult) . (eliminate CoreReductionResult (lambda unrestricted value : (family CoreReductionResult) . (family CoreReductionResult)) result (branch CoreReductionCompleted term rounds . (constructor CoreReductionResult CoreReductionCompleted term (succ rounds))) (branch CoreReductionExhausted term rounds . (constructor CoreReductionResult CoreReductionExhausted term (succ rounds))))) def reduceCoreWithBudget = (lambda unrestricted step : (pi unrestricted term : (family CoreTerm) . (family CoreTerm)) . (lambda unrestricted budget : Nat . (nat-eliminate (lambda unrestricted remaining : Nat . (pi unrestricted term : (family CoreTerm) . (family CoreReductionResult))) (lambda unrestricted term : (family CoreTerm) . (constructor CoreReductionResult CoreReductionExhausted term zero)) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (pi unrestricted term : (family CoreTerm) . (family CoreReductionResult)) . (lambda unrestricted term : (family CoreTerm) . (app (lambda unrestricted reduced : (family CoreTerm) . (app (nat-eliminate (lambda unrestricted equal : Nat . (pi unrestricted trigger : Nat . (family CoreReductionResult))) (lambda unrestricted trigger : Nat . (countCoreReductionRound (induction reduced))) (lambda unrestricted prior : Nat . (lambda unrestricted ignored : (pi unrestricted trigger : Nat . (family CoreReductionResult)) . (lambda unrestricted trigger : Nat . (constructor CoreReductionResult CoreReductionCompleted reduced (succ zero))))) (coreTermEqual term reduced)) zero)) (step term))))) budget))) def coreNormalizationDefaultWork = (constructor ModelWord32 ModelWord32Value (byte 0) (byte 0) (byte 1) (byte 0)) def chooseCoreEliminatorBranch = (lambda unrestricted first : (family CoreEliminatorBranchSelection) . (lambda unrestricted second : (family CoreEliminatorBranchSelection) . (eliminate CoreEliminatorBranchSelection (lambda unrestricted value : (family CoreEliminatorBranchSelection) . (family CoreEliminatorBranchSelection)) first (branch CoreEliminatorBranchSelected binderCount body . first) (branch CoreEliminatorBranchMissing . second)))) def findCoreEliminatorBranch = (lambda unrestricted constructorName : Bytes . (lambda unrestricted branches : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted value : (family CoreTerm) . (family CoreEliminatorBranchSelection)) branches (branch CoreUniverse level . (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)) (branch CoreNatural . (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)) (branch CoreNaturalLiteral value . (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)) (branch CoreBound index . (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)) (branch CoreLambda multiplicity domain body ih_domain ih_body . (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)) (branch CoreApplication function argument ih_function ih_argument . (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)) (branch CoreNaturalSuccessor predecessor ih_predecessor . (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)) (branch CoreByte . (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)) (branch CoreByteLiteral value . (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)) (branch CoreBytes . (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)) (branch CoreBytesLiteral value . (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)) (branch CorePrimitiveTerm primitive . (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)) (branch CoreTermSequenceEnd . (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)) (branch CoreTermSequenceNext head tail ih_head ih_tail . (chooseCoreEliminatorBranch ih_head ih_tail)) (branch CoreFamilyApplication familyName arguments ih_arguments . (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)) (branch CoreConstructorApplication familyName nestedConstructorName arguments ih_arguments . (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing)) (branch CoreEliminatorBranch branchConstructorName binderCount body ih_body . (nat-eliminate (lambda unrestricted matches : Nat . (family CoreEliminatorBranchSelection)) (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family CoreEliminatorBranchSelection) . (constructor CoreEliminatorBranchSelection CoreEliminatorBranchSelected binderCount body))) (coreBytesEqual branchConstructorName constructorName))) (branch CoreEliminator familyName motive scrutinee nestedBranches ih_motive ih_scrutinee ih_branches . (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing))))) def coreNaturalSaturatingSubtract = (lambda unrestricted left : Nat . (lambda unrestricted right : Nat . (nat-eliminate (lambda unrestricted remaining : Nat . Nat) left (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . (naturalPredecessor induction))) right))) def coreTermSequenceCount = (lambda unrestricted sequence : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted value : (family CoreTerm) . Nat) sequence (branch CoreUniverse level . zero) (branch CoreNatural . zero) (branch CoreNaturalLiteral value . zero) (branch CoreBound index . zero) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . zero) (branch CoreLambda multiplicity domain body ih_domain ih_body . zero) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . zero) (branch CoreApplication function argument ih_function ih_argument . zero) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . zero) (branch CoreNaturalSuccessor predecessor ih_predecessor . zero) (branch CoreByte . zero) (branch CoreByteLiteral value . zero) (branch CoreBytes . zero) (branch CoreBytesLiteral value . zero) (branch CorePrimitiveTerm primitive . zero) (branch CoreTermSequenceEnd . zero) (branch CoreTermSequenceNext head tail ih_head ih_tail . (succ ih_tail)) (branch CoreFamilyApplication familyName arguments ih_arguments . zero) (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . zero) (branch CoreEliminatorBranch constructorName binderCount body ih_body . zero) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . zero))) def appendCoreTermSequenceForEliminator = (lambda unrestricted left : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted value : (family CoreTerm) . (pi unrestricted right : (family CoreTerm) . (family CoreTerm))) left (branch CoreUniverse level . (lambda unrestricted right : (family CoreTerm) . left)) (branch CoreNatural . (lambda unrestricted right : (family CoreTerm) . left)) (branch CoreNaturalLiteral value . (lambda unrestricted right : (family CoreTerm) . left)) (branch CoreBound index . (lambda unrestricted right : (family CoreTerm) . left)) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . (lambda unrestricted right : (family CoreTerm) . left)) (branch CoreLambda multiplicity domain body ih_domain ih_body . (lambda unrestricted right : (family CoreTerm) . left)) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . (lambda unrestricted right : (family CoreTerm) . left)) (branch CoreApplication function argument ih_function ih_argument . (lambda unrestricted right : (family CoreTerm) . left)) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . (lambda unrestricted right : (family CoreTerm) . left)) (branch CoreNaturalSuccessor predecessor ih_predecessor . (lambda unrestricted right : (family CoreTerm) . left)) (branch CoreByte . (lambda unrestricted right : (family CoreTerm) . left)) (branch CoreByteLiteral value . (lambda unrestricted right : (family CoreTerm) . left)) (branch CoreBytes . (lambda unrestricted right : (family CoreTerm) . left)) (branch CoreBytesLiteral value . (lambda unrestricted right : (family CoreTerm) . left)) (branch CorePrimitiveTerm primitive . (lambda unrestricted right : (family CoreTerm) . left)) (branch CoreTermSequenceEnd . (lambda unrestricted right : (family CoreTerm) . right)) (branch CoreTermSequenceNext head tail ih_head ih_tail . (lambda unrestricted right : (family CoreTerm) . (constructor CoreTerm CoreTermSequenceNext head (ih_tail right)))) (branch CoreFamilyApplication familyName arguments ih_arguments . (lambda unrestricted right : (family CoreTerm) . left)) (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . (lambda unrestricted right : (family CoreTerm) . left)) (branch CoreEliminatorBranch constructorName binderCount body ih_body . (lambda unrestricted right : (family CoreTerm) . left)) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . (lambda unrestricted right : (family CoreTerm) . left)))) def instantiateCoreEliminatorBranch = (lambda unrestricted supplied : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted value : (family CoreTerm) . (pi unrestricted body : (family CoreTerm) . (family CoreTerm))) supplied (branch CoreUniverse level . (lambda unrestricted body : (family CoreTerm) . body)) (branch CoreNatural . (lambda unrestricted body : (family CoreTerm) . body)) (branch CoreNaturalLiteral value . (lambda unrestricted body : (family CoreTerm) . body)) (branch CoreBound index . (lambda unrestricted body : (family CoreTerm) . body)) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . (lambda unrestricted body : (family CoreTerm) . body)) (branch CoreLambda multiplicity domain body ih_domain ih_body . (lambda unrestricted branchBody : (family CoreTerm) . branchBody)) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . (lambda unrestricted branchBody : (family CoreTerm) . branchBody)) (branch CoreApplication function argument ih_function ih_argument . (lambda unrestricted body : (family CoreTerm) . body)) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . (lambda unrestricted body : (family CoreTerm) . body)) (branch CoreNaturalSuccessor predecessor ih_predecessor . (lambda unrestricted body : (family CoreTerm) . body)) (branch CoreByte . (lambda unrestricted body : (family CoreTerm) . body)) (branch CoreByteLiteral value . (lambda unrestricted body : (family CoreTerm) . body)) (branch CoreBytes . (lambda unrestricted body : (family CoreTerm) . body)) (branch CoreBytesLiteral value . (lambda unrestricted body : (family CoreTerm) . body)) (branch CorePrimitiveTerm primitive . (lambda unrestricted body : (family CoreTerm) . body)) (branch CoreTermSequenceEnd . (lambda unrestricted body : (family CoreTerm) . body)) (branch CoreTermSequenceNext head tail ih_head ih_tail . (lambda unrestricted body : (family CoreTerm) . (substituteCoreTop head (ih_tail body)))) (branch CoreFamilyApplication familyName arguments ih_arguments . (lambda unrestricted body : (family CoreTerm) . body)) (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . (lambda unrestricted body : (family CoreTerm) . body)) (branch CoreEliminatorBranch constructorName binderCount body ih_body . (lambda unrestricted branchBody : (family CoreTerm) . branchBody)) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . (lambda unrestricted body : (family CoreTerm) . body)))) def dropCoreTermSequenceForEliminator = (lambda unrestricted sequence : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted value : (family CoreTerm) . (pi unrestricted count : Nat . (family CoreTerm))) sequence (branch CoreUniverse level . (lambda unrestricted count : Nat . sequence)) (branch CoreNatural . (lambda unrestricted count : Nat . sequence)) (branch CoreNaturalLiteral value . (lambda unrestricted count : Nat . sequence)) (branch CoreBound index . (lambda unrestricted count : Nat . sequence)) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . (lambda unrestricted count : Nat . sequence)) (branch CoreLambda multiplicity domain body ih_domain ih_body . (lambda unrestricted count : Nat . sequence)) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . (lambda unrestricted count : Nat . sequence)) (branch CoreApplication function argument ih_function ih_argument . (lambda unrestricted count : Nat . sequence)) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . (lambda unrestricted count : Nat . sequence)) (branch CoreNaturalSuccessor predecessor ih_predecessor . (lambda unrestricted count : Nat . sequence)) (branch CoreByte . (lambda unrestricted count : Nat . sequence)) (branch CoreByteLiteral value . (lambda unrestricted count : Nat . sequence)) (branch CoreBytes . (lambda unrestricted count : Nat . sequence)) (branch CoreBytesLiteral value . (lambda unrestricted count : Nat . sequence)) (branch CorePrimitiveTerm primitive . (lambda unrestricted count : Nat . sequence)) (branch CoreTermSequenceEnd . (lambda unrestricted count : Nat . (constructor CoreTerm CoreTermSequenceEnd))) (branch CoreTermSequenceNext head tail ih_head ih_tail . (lambda unrestricted count : Nat . (nat-eliminate (lambda unrestricted remaining : Nat . (family CoreTerm)) (constructor CoreTerm CoreTermSequenceNext head tail) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family CoreTerm) . (ih_tail predecessor))) count))) (branch CoreFamilyApplication familyName arguments ih_arguments . (lambda unrestricted count : Nat . sequence)) (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . (lambda unrestricted count : Nat . sequence)) (branch CoreEliminatorBranch constructorName binderCount body ih_body . (lambda unrestricted count : Nat . sequence)) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . (lambda unrestricted count : Nat . sequence)))) def finishCoreEliminatorReduction = (lambda unrestricted familyName : Bytes . (lambda unrestricted motive : (family CoreTerm) . (lambda unrestricted scrutinee : (family CoreTerm) . (lambda unrestricted branches : (family CoreTerm) . (lambda unrestricted arguments : (family CoreTerm) . (lambda unrestricted inductionCandidates : (family CoreTerm) . (lambda unrestricted selection : (family CoreEliminatorBranchSelection) . (eliminate CoreEliminatorBranchSelection (lambda unrestricted value : (family CoreEliminatorBranchSelection) . (family CoreTerm)) selection (branch CoreEliminatorBranchSelected binderCount body . (app (lambda unrestricted argumentCount : Nat . (app (lambda unrestricted recursiveCount : Nat . (app (lambda unrestricted valueCount : Nat . (app (lambda unrestricted inductionResults : (family CoreTerm) . (app (lambda unrestricted supplied : (family CoreTerm) . (nat-eliminate (lambda unrestricted arityMatches : Nat . (family CoreTerm)) (constructor CoreTerm CoreEliminator familyName motive scrutinee branches) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family CoreTerm) . (instantiateCoreEliminatorBranch supplied body))) (naturalEqual (coreTermSequenceCount supplied) binderCount))) (appendCoreTermSequenceForEliminator arguments inductionResults))) (dropCoreTermSequenceForEliminator inductionCandidates valueCount))) (coreNaturalSaturatingSubtract argumentCount recursiveCount))) (coreNaturalSaturatingSubtract binderCount argumentCount))) (coreTermSequenceCount arguments))) (branch CoreEliminatorBranchMissing . (constructor CoreTerm CoreEliminator familyName motive scrutinee branches)))))))))) def reduceCoreGenericEliminator = (lambda unrestricted familyName : Bytes . (lambda unrestricted motive : (family CoreTerm) . (lambda unrestricted scrutinee : (family CoreTerm) . (lambda unrestricted branches : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted value : (family CoreTerm) . (family CoreTerm)) scrutinee (branch CoreUniverse level . (constructor CoreTerm CoreEliminator familyName motive scrutinee branches)) (branch CoreNatural . (constructor CoreTerm CoreEliminator familyName motive scrutinee branches)) (branch CoreNaturalLiteral value . (constructor CoreTerm CoreEliminator familyName motive scrutinee branches)) (branch CoreBound index . (constructor CoreTerm CoreEliminator familyName motive scrutinee branches)) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . (constructor CoreTerm CoreEliminator familyName motive scrutinee branches)) (branch CoreLambda multiplicity domain body ih_domain ih_body . (constructor CoreTerm CoreEliminator familyName motive scrutinee branches)) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . (constructor CoreTerm CoreEliminator familyName motive (substituteCoreTop ih_value ih_body) branches)) (branch CoreApplication function argument ih_function ih_argument . (constructor CoreTerm CoreEliminator familyName motive scrutinee branches)) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . (constructor CoreTerm CoreEliminator familyName motive scrutinee branches)) (branch CoreNaturalSuccessor predecessor ih_predecessor . (constructor CoreTerm CoreEliminator familyName motive scrutinee branches)) (branch CoreByte . (constructor CoreTerm CoreEliminator familyName motive scrutinee branches)) (branch CoreByteLiteral value . (constructor CoreTerm CoreEliminator familyName motive scrutinee branches)) (branch CoreBytes . (constructor CoreTerm CoreEliminator familyName motive scrutinee branches)) (branch CoreBytesLiteral value . (constructor CoreTerm CoreEliminator familyName motive scrutinee branches)) (branch CorePrimitiveTerm primitive . (constructor CoreTerm CoreEliminator familyName motive scrutinee branches)) (branch CoreTermSequenceEnd . (constructor CoreTerm CoreTermSequenceEnd)) (branch CoreTermSequenceNext head tail ih_head ih_tail . (constructor CoreTerm CoreTermSequenceNext ih_head ih_tail)) (branch CoreFamilyApplication constructorFamily arguments ih_arguments . (constructor CoreTerm CoreEliminator familyName motive scrutinee branches)) (branch CoreConstructorApplication constructorFamily constructorName arguments ih_arguments . (nat-eliminate (lambda unrestricted familyMatches : Nat . (family CoreTerm)) (constructor CoreTerm CoreEliminator familyName motive scrutinee branches) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family CoreTerm) . (finishCoreEliminatorReduction familyName motive scrutinee branches arguments ih_arguments (findCoreEliminatorBranch constructorName branches)))) (coreBytesEqual constructorFamily familyName))) (branch CoreEliminatorBranch constructorName binderCount body ih_body . (constructor CoreTerm CoreEliminator familyName motive scrutinee branches)) (branch CoreEliminator nestedFamily nestedMotive nestedScrutinee nestedBranches ih_motive ih_scrutinee ih_branches . (constructor CoreTerm CoreEliminator familyName motive scrutinee branches))))))) def coreWorkOne = (constructor ModelWord32 ModelWord32Value (byte 1) (byte 0) (byte 0) (byte 0)) def coreWorkBind = (lambda unrestricted result : (family CoreWorkResult) . (lambda unrestricted continuation : (pi unrestricted term : (family CoreTerm) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) . (eliminate CoreWorkResult (lambda unrestricted current : (family CoreWorkResult) . (family CoreWorkResult)) result (branch CoreWorkCompleted term budget . (continuation term budget)) (branch CoreWorkExhausted budget . (constructor CoreWorkResult CoreWorkExhausted budget))))) def coreWorkCharge = (lambda unrestricted amount : (family ModelWord32) . (lambda unrestricted budget : (family NormalizationBudget) . (lambda unrestricted continuation : (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult)) . (eliminate NormalizationChargeResult (lambda unrestricted current : (family NormalizationChargeResult) . (family CoreWorkResult)) (Compiler.NormalizationBudget/chargeNormalizationBudget amount budget) (branch NormalizationCharged remaining . (continuation remaining)) (branch NormalizationChargeExhausted unchanged rejected . (constructor CoreWorkResult CoreWorkExhausted unchanged)) (branch NormalizationChargeInvalid . (constructor CoreWorkResult CoreWorkExhausted budget)))))) def coreWorkChoose = (lambda unrestricted condition : Nat . (lambda unrestricted selected : (pi unrestricted force : Nat . (family CoreWorkResult)) . (lambda unrestricted fallback : (pi unrestricted force : Nat . (family CoreWorkResult)) . (app (nat-eliminate (lambda unrestricted value : Nat . (pi unrestricted force : Nat . (family CoreWorkResult))) fallback (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (pi unrestricted force : Nat . (family CoreWorkResult)) . selected)) condition) zero)))) def extendCoreFunctionInspection : (pi unrestricted inspection : (family CoreFunctionInspection) . (pi unrestricted argument : (family CoreTerm) . (family CoreFunctionInspection))) = (lambda unrestricted inspection : (family CoreFunctionInspection) . (lambda unrestricted argument : (family CoreTerm) . (eliminate CoreFunctionInspection (lambda unrestricted value : (family CoreFunctionInspection) . (family CoreFunctionInspection)) inspection (branch CoreFunctionLambda body . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CoreFunctionPrimitive primitive . (constructor CoreFunctionInspection CoreFunctionAppliedPrimitive primitive argument)) (branch CoreFunctionAppliedPrimitive primitive first . (constructor CoreFunctionInspection CoreFunctionAppliedPrimitive2 primitive first argument)) (branch CoreFunctionAppliedPrimitive2 primitive first second . (constructor CoreFunctionInspection CoreFunctionAppliedPrimitive3 primitive first second argument)) (branch CoreFunctionAppliedPrimitive3 primitive first second third . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CoreFunctionOther . (constructor CoreFunctionInspection CoreFunctionOther))))) def inspectCoreFunction : (pi unrestricted term : (family CoreTerm) . (family CoreFunctionInspection)) = (lambda unrestricted term : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted value : (family CoreTerm) . (family CoreFunctionInspection)) term (branch CoreUniverse level . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CoreNatural . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CoreNaturalLiteral value . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CoreBound index . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CoreLambda multiplicity domain body ih_domain ih_body . (constructor CoreFunctionInspection CoreFunctionLambda body)) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CoreApplication function argument ih_function ih_argument . (extendCoreFunctionInspection ih_function argument)) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CoreNaturalSuccessor predecessor ih_predecessor . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CoreByte . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CoreByteLiteral value . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CoreBytes . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CoreBytesLiteral value . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CorePrimitiveTerm primitive . (constructor CoreFunctionInspection CoreFunctionPrimitive primitive)) (branch CoreTermSequenceEnd . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CoreTermSequenceNext head tail ih_head ih_tail . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CoreFamilyApplication familyName arguments ih_arguments . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CoreEliminatorBranch constructorName binderCount body ih_body . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . (constructor CoreFunctionInspection CoreFunctionOther)))) -- Reserve unary metadata work before invoking legacy index arithmetic. def coreWorkChargeNatural = (lambda unrestricted amount : Nat . (lambda unrestricted budget : (family NormalizationBudget) . (lambda unrestricted continue : (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult)) . (eliminate NormalizationChargeResult (lambda unrestricted current : (family NormalizationChargeResult) . (family CoreWorkResult)) (chargeNormalizationNatural amount budget) (branch NormalizationCharged remaining . (continue remaining)) (branch NormalizationChargeExhausted remaining cost . (constructor CoreWorkResult CoreWorkExhausted remaining)) (branch NormalizationChargeInvalid . (constructor CoreWorkResult CoreWorkExhausted budget)))))) def workShiftCoreTree = (lambda unrestricted term : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted current : (family CoreTerm) . (pi unrestricted depth : Nat . (pi unrestricted amount : Nat . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))))) term (branch CoreUniverse coreUniverseLevel . (lambda unrestricted depth : Nat . (lambda unrestricted amount : Nat . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreUniverse coreUniverseLevel) remaining))))))) (branch CoreNatural . (lambda unrestricted depth : Nat . (lambda unrestricted amount : Nat . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreNatural) remaining))))))) (branch CoreNaturalLiteral coreNaturalValue . (lambda unrestricted depth : Nat . (lambda unrestricted amount : Nat . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreNaturalLiteral coreNaturalValue) remaining))))))) (branch CoreBound coreBoundIndex . (lambda unrestricted depth : Nat . (lambda unrestricted amount : Nat . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkChoose (nat-less-than coreBoundIndex depth) (lambda unrestricted force : Nat . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreBound coreBoundIndex) remaining)) (lambda unrestricted force : Nat . (coreWorkChargeNatural coreBoundIndex remaining (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (shiftCorePart1 coreBoundIndex depth amount) remaining))))))))))) (branch CorePi corePiMultiplicity corePiDomain corePiCodomain ih_corePiDomain ih_corePiCodomain . (lambda unrestricted depth : Nat . (lambda unrestricted amount : Nat . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_corePiDomain depth amount remaining) (lambda unrestricted new_corePiDomain : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_corePiCodomain (succ depth) amount remaining) (lambda unrestricted new_corePiCodomain : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CorePi corePiMultiplicity new_corePiDomain new_corePiCodomain) remaining))))))))))))) (branch CoreLambda coreLambdaMultiplicity coreLambdaDomain coreLambdaBody ih_coreLambdaDomain ih_coreLambdaBody . (lambda unrestricted depth : Nat . (lambda unrestricted amount : Nat . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreLambdaDomain depth amount remaining) (lambda unrestricted new_coreLambdaDomain : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreLambdaBody (succ depth) amount remaining) (lambda unrestricted new_coreLambdaBody : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreLambda coreLambdaMultiplicity new_coreLambdaDomain new_coreLambdaBody) remaining))))))))))))) (branch CoreLet coreLetMultiplicity coreLetAnnotation coreLetValue coreLetBody ih_coreLetAnnotation ih_coreLetValue ih_coreLetBody . (lambda unrestricted depth : Nat . (lambda unrestricted amount : Nat . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreLetAnnotation depth amount remaining) (lambda unrestricted new_coreLetAnnotation : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreLetValue depth amount remaining) (lambda unrestricted new_coreLetValue : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreLetBody (succ depth) amount remaining) (lambda unrestricted new_coreLetBody : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreLet coreLetMultiplicity new_coreLetAnnotation new_coreLetValue new_coreLetBody) remaining)))))))))))))))) (branch CoreApplication coreApplicationFunction coreApplicationArgument ih_coreApplicationFunction ih_coreApplicationArgument . (lambda unrestricted depth : Nat . (lambda unrestricted amount : Nat . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreApplicationFunction depth amount remaining) (lambda unrestricted new_coreApplicationFunction : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreApplicationArgument depth amount remaining) (lambda unrestricted new_coreApplicationArgument : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreApplication new_coreApplicationFunction new_coreApplicationArgument) remaining))))))))))))) (branch CoreNaturalArithmetic coreArithmeticOperation coreArithmeticLeft coreArithmeticRight ih_coreArithmeticLeft ih_coreArithmeticRight . (lambda unrestricted depth : Nat . (lambda unrestricted amount : Nat . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreArithmeticLeft depth amount remaining) (lambda unrestricted new_coreArithmeticLeft : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreArithmeticRight depth amount remaining) (lambda unrestricted new_coreArithmeticRight : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreNaturalArithmetic coreArithmeticOperation new_coreArithmeticLeft new_coreArithmeticRight) remaining))))))))))))) (branch CoreNaturalSuccessor coreNaturalPredecessor ih_coreNaturalPredecessor . (lambda unrestricted depth : Nat . (lambda unrestricted amount : Nat . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreNaturalPredecessor depth amount remaining) (lambda unrestricted new_coreNaturalPredecessor : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreNaturalSuccessor new_coreNaturalPredecessor) remaining)))))))))) (branch CoreByte . (lambda unrestricted depth : Nat . (lambda unrestricted amount : Nat . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreByte) remaining))))))) (branch CoreByteLiteral coreByteValue . (lambda unrestricted depth : Nat . (lambda unrestricted amount : Nat . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreByteLiteral coreByteValue) remaining))))))) (branch CoreBytes . (lambda unrestricted depth : Nat . (lambda unrestricted amount : Nat . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreBytes) remaining))))))) (branch CoreBytesLiteral coreBytesValue . (lambda unrestricted depth : Nat . (lambda unrestricted amount : Nat . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreBytesLiteral coreBytesValue) remaining))))))) (branch CorePrimitiveTerm corePrimitive . (lambda unrestricted depth : Nat . (lambda unrestricted amount : Nat . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CorePrimitiveTerm corePrimitive) remaining))))))) (branch CoreTermSequenceEnd . (lambda unrestricted depth : Nat . (lambda unrestricted amount : Nat . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreTermSequenceEnd) remaining))))))) (branch CoreTermSequenceNext coreTermSequenceHead coreTermSequenceTail ih_coreTermSequenceHead ih_coreTermSequenceTail . (lambda unrestricted depth : Nat . (lambda unrestricted amount : Nat . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreTermSequenceHead depth amount remaining) (lambda unrestricted new_coreTermSequenceHead : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreTermSequenceTail depth amount remaining) (lambda unrestricted new_coreTermSequenceTail : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreTermSequenceNext new_coreTermSequenceHead new_coreTermSequenceTail) remaining))))))))))))) (branch CoreFamilyApplication coreFamilyName coreFamilyArguments ih_coreFamilyArguments . (lambda unrestricted depth : Nat . (lambda unrestricted amount : Nat . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreFamilyArguments depth amount remaining) (lambda unrestricted new_coreFamilyArguments : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreFamilyApplication coreFamilyName new_coreFamilyArguments) remaining)))))))))) (branch CoreConstructorApplication coreConstructorFamilyName coreConstructorName coreConstructorArguments ih_coreConstructorArguments . (lambda unrestricted depth : Nat . (lambda unrestricted amount : Nat . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreConstructorArguments depth amount remaining) (lambda unrestricted new_coreConstructorArguments : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreConstructorApplication coreConstructorFamilyName coreConstructorName new_coreConstructorArguments) remaining)))))))))) (branch CoreEliminatorBranch coreBranchConstructorName coreBranchBinderCount coreBranchBody ih_coreBranchBody . (lambda unrestricted depth : Nat . (lambda unrestricted amount : Nat . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkChargeNatural depth remaining (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreBranchBody (naturalAdd depth coreBranchBinderCount) amount remaining) (lambda unrestricted new_coreBranchBody : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreEliminatorBranch coreBranchConstructorName coreBranchBinderCount new_coreBranchBody) remaining)))))))))))) (branch CoreEliminator coreEliminatedFamilyName coreEliminatorMotive coreEliminatorScrutinee coreEliminatorBranches ih_coreEliminatorMotive ih_coreEliminatorScrutinee ih_coreEliminatorBranches . (lambda unrestricted depth : Nat . (lambda unrestricted amount : Nat . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreEliminatorMotive depth amount remaining) (lambda unrestricted new_coreEliminatorMotive : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreEliminatorScrutinee depth amount remaining) (lambda unrestricted new_coreEliminatorScrutinee : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreEliminatorBranches depth amount remaining) (lambda unrestricted new_coreEliminatorBranches : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreEliminator coreEliminatedFamilyName new_coreEliminatorMotive new_coreEliminatorScrutinee new_coreEliminatorBranches) remaining)))))))))))))))))) -- A zero shift preserves the existing immutable graph. It does not copy the -- replacement or traverse its descendants merely to return an equal term. def workShiftCore = (lambda unrestricted term : (family CoreTerm) . (lambda unrestricted cutoff : Nat . (lambda unrestricted amount : Nat . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkChoose (naturalEqual amount zero) (lambda unrestricted force : Nat . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted term remaining)))) (lambda unrestricted force : Nat . (workShiftCoreTree term cutoff amount budget))))))) def workSubstituteCoreTree = (lambda unrestricted term : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted current : (family CoreTerm) . (pi unrestricted depth : Nat . (pi unrestricted replacement : (family CoreTerm) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))))) term (branch CoreUniverse coreUniverseLevel . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreUniverse coreUniverseLevel) remaining))))))) (branch CoreNatural . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreNatural) remaining))))))) (branch CoreNaturalLiteral coreNaturalValue . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreNaturalLiteral coreNaturalValue) remaining))))))) (branch CoreBound coreBoundIndex . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkChoose (naturalEqual coreBoundIndex depth) (lambda unrestricted force : Nat . (workShiftCore replacement zero depth remaining)) (lambda unrestricted force : Nat . (coreWorkChoose (nat-less-than depth coreBoundIndex) (lambda unrestricted force : Nat . (coreWorkChargeNatural coreBoundIndex remaining (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (substituteCorePart1 coreBoundIndex depth replacement) remaining)))) (lambda unrestricted force : Nat . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreBound coreBoundIndex) remaining))))))))))) (branch CorePi corePiMultiplicity corePiDomain corePiCodomain ih_corePiDomain ih_corePiCodomain . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_corePiDomain depth replacement remaining) (lambda unrestricted new_corePiDomain : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_corePiCodomain (succ depth) replacement remaining) (lambda unrestricted new_corePiCodomain : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CorePi corePiMultiplicity new_corePiDomain new_corePiCodomain) remaining))))))))))))) (branch CoreLambda coreLambdaMultiplicity coreLambdaDomain coreLambdaBody ih_coreLambdaDomain ih_coreLambdaBody . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreLambdaDomain depth replacement remaining) (lambda unrestricted new_coreLambdaDomain : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreLambdaBody (succ depth) replacement remaining) (lambda unrestricted new_coreLambdaBody : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreLambda coreLambdaMultiplicity new_coreLambdaDomain new_coreLambdaBody) remaining))))))))))))) (branch CoreLet coreLetMultiplicity coreLetAnnotation coreLetValue coreLetBody ih_coreLetAnnotation ih_coreLetValue ih_coreLetBody . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreLetAnnotation depth replacement remaining) (lambda unrestricted new_coreLetAnnotation : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreLetValue depth replacement remaining) (lambda unrestricted new_coreLetValue : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreLetBody (succ depth) replacement remaining) (lambda unrestricted new_coreLetBody : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreLet coreLetMultiplicity new_coreLetAnnotation new_coreLetValue new_coreLetBody) remaining)))))))))))))))) (branch CoreApplication coreApplicationFunction coreApplicationArgument ih_coreApplicationFunction ih_coreApplicationArgument . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreApplicationFunction depth replacement remaining) (lambda unrestricted new_coreApplicationFunction : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreApplicationArgument depth replacement remaining) (lambda unrestricted new_coreApplicationArgument : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreApplication new_coreApplicationFunction new_coreApplicationArgument) remaining))))))))))))) (branch CoreNaturalArithmetic coreArithmeticOperation coreArithmeticLeft coreArithmeticRight ih_coreArithmeticLeft ih_coreArithmeticRight . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreArithmeticLeft depth replacement remaining) (lambda unrestricted new_coreArithmeticLeft : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreArithmeticRight depth replacement remaining) (lambda unrestricted new_coreArithmeticRight : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreNaturalArithmetic coreArithmeticOperation new_coreArithmeticLeft new_coreArithmeticRight) remaining))))))))))))) (branch CoreNaturalSuccessor coreNaturalPredecessor ih_coreNaturalPredecessor . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreNaturalPredecessor depth replacement remaining) (lambda unrestricted new_coreNaturalPredecessor : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreNaturalSuccessor new_coreNaturalPredecessor) remaining)))))))))) (branch CoreByte . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreByte) remaining))))))) (branch CoreByteLiteral coreByteValue . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreByteLiteral coreByteValue) remaining))))))) (branch CoreBytes . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreBytes) remaining))))))) (branch CoreBytesLiteral coreBytesValue . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreBytesLiteral coreBytesValue) remaining))))))) (branch CorePrimitiveTerm corePrimitive . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CorePrimitiveTerm corePrimitive) remaining))))))) (branch CoreTermSequenceEnd . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreTermSequenceEnd) remaining))))))) (branch CoreTermSequenceNext coreTermSequenceHead coreTermSequenceTail ih_coreTermSequenceHead ih_coreTermSequenceTail . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreTermSequenceHead depth replacement remaining) (lambda unrestricted new_coreTermSequenceHead : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreTermSequenceTail depth replacement remaining) (lambda unrestricted new_coreTermSequenceTail : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreTermSequenceNext new_coreTermSequenceHead new_coreTermSequenceTail) remaining))))))))))))) (branch CoreFamilyApplication coreFamilyName coreFamilyArguments ih_coreFamilyArguments . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreFamilyArguments depth replacement remaining) (lambda unrestricted new_coreFamilyArguments : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreFamilyApplication coreFamilyName new_coreFamilyArguments) remaining)))))))))) (branch CoreConstructorApplication coreConstructorFamilyName coreConstructorName coreConstructorArguments ih_coreConstructorArguments . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreConstructorArguments depth replacement remaining) (lambda unrestricted new_coreConstructorArguments : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreConstructorApplication coreConstructorFamilyName coreConstructorName new_coreConstructorArguments) remaining)))))))))) (branch CoreEliminatorBranch coreBranchConstructorName coreBranchBinderCount coreBranchBody ih_coreBranchBody . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkChargeNatural depth remaining (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreBranchBody (naturalAdd depth coreBranchBinderCount) replacement remaining) (lambda unrestricted new_coreBranchBody : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreEliminatorBranch coreBranchConstructorName coreBranchBinderCount new_coreBranchBody) remaining)))))))))))) (branch CoreEliminator coreEliminatedFamilyName coreEliminatorMotive coreEliminatorScrutinee coreEliminatorBranches ih_coreEliminatorMotive ih_coreEliminatorScrutinee ih_coreEliminatorBranches . (lambda unrestricted depth : Nat . (lambda unrestricted replacement : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreEliminatorMotive depth replacement remaining) (lambda unrestricted new_coreEliminatorMotive : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreEliminatorScrutinee depth replacement remaining) (lambda unrestricted new_coreEliminatorScrutinee : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreEliminatorBranches depth replacement remaining) (lambda unrestricted new_coreEliminatorBranches : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreEliminator coreEliminatedFamilyName new_coreEliminatorMotive new_coreEliminatorScrutinee new_coreEliminatorBranches) remaining)))))))))))))))))) def workSubstituteCoreTop = (lambda unrestricted replacement : (family CoreTerm) . (lambda unrestricted body : (family CoreTerm) . (workSubstituteCoreTree body zero replacement))) def workApplyCoreFunctionOnce = (lambda unrestricted function : (family CoreTerm) . (lambda unrestricted argument : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (eliminate CoreFunctionInspection (lambda unrestricted current : (family CoreFunctionInspection) . (family CoreWorkResult)) (inspectCoreFunction function) (branch CoreFunctionLambda body . (workSubstituteCoreTop argument body remaining)) (branch CoreFunctionPrimitive primitive . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreApplication function argument) remaining)) (branch CoreFunctionAppliedPrimitive primitive first . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreApplication function argument) remaining)) (branch CoreFunctionAppliedPrimitive2 primitive first second . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreApplication function argument) remaining)) (branch CoreFunctionAppliedPrimitive3 primitive first second third . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreApplication function argument) remaining)) (branch CoreFunctionOther . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreApplication function argument) remaining)))))))) def corePrimitiveApplication : (pi unrestricted primitive : (family CorePrimitive) . (pi unrestricted argument : (family CoreTerm) . (family CoreTerm))) = (lambda unrestricted primitive : (family CorePrimitive) . (lambda unrestricted argument : (family CoreTerm) . (constructor CoreTerm CoreApplication (constructor CoreTerm CorePrimitiveTerm primitive) argument))) def corePrimitiveApplication2 : (pi unrestricted primitive : (family CorePrimitive) . (pi unrestricted left : (family CoreTerm) . (pi unrestricted right : (family CoreTerm) . (family CoreTerm)))) = (lambda unrestricted primitive : (family CorePrimitive) . (lambda unrestricted left : (family CoreTerm) . (lambda unrestricted right : (family CoreTerm) . (constructor CoreTerm CoreApplication (corePrimitiveApplication primitive left) right)))) def corePrimitiveApplication3 : (pi unrestricted primitive : (family CorePrimitive) . (pi unrestricted first : (family CoreTerm) . (pi unrestricted second : (family CoreTerm) . (pi unrestricted third : (family CoreTerm) . (family CoreTerm))))) = (lambda unrestricted primitive : (family CorePrimitive) . (lambda unrestricted first : (family CoreTerm) . (lambda unrestricted second : (family CoreTerm) . (lambda unrestricted third : (family CoreTerm) . (constructor CoreTerm CoreApplication (corePrimitiveApplication2 primitive first second) third))))) def reduceCoreNaturalToByte : (pi unrestricted argument : (family CoreTerm) . (family CoreTerm)) = (lambda unrestricted argument : (family CoreTerm) . (eliminate CoreLiteralInspection (lambda unrestricted inspection : (family CoreLiteralInspection) . (family CoreTerm)) (inspectCoreLiteral argument) (branch CoreNaturalInspected value . (constructor CoreTerm CoreByteLiteral (Compiler.NaturalMagnitudeArithmetic/magnitudeLowByte value))) (branch CoreByteInspected value . (corePrimitiveApplication (constructor CorePrimitive CoreNaturalToByte) argument)) (branch CoreBytesInspected value . (corePrimitiveApplication (constructor CorePrimitive CoreNaturalToByte) argument)) (branch CoreNotLiteral . (corePrimitiveApplication (constructor CorePrimitive CoreNaturalToByte) argument)))) def reduceCoreByteToNatural : (pi unrestricted argument : (family CoreTerm) . (family CoreTerm)) = (lambda unrestricted argument : (family CoreTerm) . (eliminate CoreLiteralInspection (lambda unrestricted inspection : (family CoreLiteralInspection) . (family CoreTerm)) (inspectCoreLiteral argument) (branch CoreNaturalInspected value . (corePrimitiveApplication (constructor CorePrimitive CoreByteToNatural) argument)) (branch CoreByteInspected value . (constructor CoreTerm CoreNaturalLiteral (Compiler.NaturalMagnitudeArithmetic/magnitudeFromNatural (byte-to-nat value)))) (branch CoreBytesInspected value . (corePrimitiveApplication (constructor CorePrimitive CoreByteToNatural) argument)) (branch CoreNotLiteral . (corePrimitiveApplication (constructor CorePrimitive CoreByteToNatural) argument)))) def reduceCoreBytesLength : (pi unrestricted argument : (family CoreTerm) . (family CoreTerm)) = (lambda unrestricted argument : (family CoreTerm) . (eliminate CoreLiteralInspection (lambda unrestricted inspection : (family CoreLiteralInspection) . (family CoreTerm)) (inspectCoreLiteral argument) (branch CoreNaturalInspected value . (corePrimitiveApplication (constructor CorePrimitive CoreBytesLength) argument)) (branch CoreByteInspected value . (corePrimitiveApplication (constructor CorePrimitive CoreBytesLength) argument)) (branch CoreBytesInspected value . (constructor CoreTerm CoreNaturalLiteral (Compiler.NaturalMagnitudeArithmetic/magnitudeFromNatural (bytes-length value)))) (branch CoreNotLiteral . (corePrimitiveApplication (constructor CorePrimitive CoreBytesLength) argument)))) def reduceDirectCorePrimitive : (pi unrestricted primitive : (family CorePrimitive) . (pi unrestricted argument : (family CoreTerm) . (family CoreTerm))) = (lambda unrestricted primitive : (family CorePrimitive) . (eliminate CorePrimitive (lambda unrestricted value : (family CorePrimitive) . (pi unrestricted argument : (family CoreTerm) . (family CoreTerm))) primitive (branch CoreByteEqual . (corePrimitiveApplication primitive)) (branch CoreByteLess . (corePrimitiveApplication primitive)) (branch CoreNaturalLess . (corePrimitiveApplication primitive)) (branch CoreNaturalToByte . reduceCoreNaturalToByte) (branch CoreByteToNatural . reduceCoreByteToNatural) (branch CoreBytesAppend . (corePrimitiveApplication primitive)) (branch CoreBytesCons . (corePrimitiveApplication primitive)) (branch CoreBytesLength . reduceCoreBytesLength) (branch CoreNaturalEliminate . (corePrimitiveApplication primitive)) (branch CoreBytesEliminate . (corePrimitiveApplication primitive)) (branch CoreBytesEqual . (corePrimitiveApplication primitive)) (branch CoreFileEffect . (corePrimitiveApplication primitive)) (branch CoreEffects . (corePrimitiveApplication primitive)) (branch CoreComputation . (corePrimitiveApplication primitive)) (branch CoreReturn . (corePrimitiveApplication primitive)) (branch CoreBind . (corePrimitiveApplication primitive)) (branch CoreReadFile . (corePrimitiveApplication primitive)) (branch CoreWriteFile . (corePrimitiveApplication primitive)) (branch CoreLinuxOpenNode . (corePrimitiveApplication primitive)) (branch CoreLinuxCloseNode . (corePrimitiveApplication primitive)) (branch CoreLinuxIoctl . (corePrimitiveApplication primitive)) (branch CoreLinuxMmap . (corePrimitiveApplication primitive)) (branch CoreLinuxMunmap . (corePrimitiveApplication primitive)) (branch CoreBytesSetIndex . (corePrimitiveApplication primitive)) (branch CoreBytesIndexNonzero . (corePrimitiveApplication primitive)) (branch CoreBytesSetFreeIndex . (corePrimitiveApplication primitive)) (branch CoreBytesBuilderType . (corePrimitiveApplication primitive)) (branch CoreBytesBuilderEmpty . (corePrimitiveApplication primitive)) (branch CoreBytesBuilderChunk . (corePrimitiveApplication primitive)) (branch CoreBytesBuilderAppend . (corePrimitiveApplication primitive)) (branch CoreBytesBuilderBuild . (corePrimitiveApplication primitive)) (branch CoreRuntimeImageV4Build . (corePrimitiveApplication primitive)) (branch CoreBytesHead . (corePrimitiveApplication primitive)) (branch CoreBytesTail . (corePrimitiveApplication primitive)) (branch CoreBytesChecksum . (corePrimitiveApplication primitive)))) def reduceCoreByteEqual : (pi unrestricted left : (family CoreTerm) . (pi unrestricted right : (family CoreTerm) . (family CoreTerm))) = (lambda unrestricted left : (family CoreTerm) . (lambda unrestricted right : (family CoreTerm) . (eliminate CoreLiteralInspection (lambda unrestricted leftInspection : (family CoreLiteralInspection) . (family CoreTerm)) (inspectCoreLiteral left) (branch CoreNaturalInspected value . (corePrimitiveApplication2 (constructor CorePrimitive CoreByteEqual) left right)) (branch CoreByteInspected leftValue . (eliminate CoreLiteralInspection (lambda unrestricted rightInspection : (family CoreLiteralInspection) . (family CoreTerm)) (inspectCoreLiteral right) (branch CoreNaturalInspected value . (corePrimitiveApplication2 (constructor CorePrimitive CoreByteEqual) left right)) (branch CoreByteInspected rightValue . (constructor CoreTerm CoreNaturalLiteral (Compiler.NaturalMagnitudeArithmetic/magnitudeFromNatural (byte-equal leftValue rightValue)))) (branch CoreBytesInspected value . (corePrimitiveApplication2 (constructor CorePrimitive CoreByteEqual) left right)) (branch CoreNotLiteral . (corePrimitiveApplication2 (constructor CorePrimitive CoreByteEqual) left right)))) (branch CoreBytesInspected value . (corePrimitiveApplication2 (constructor CorePrimitive CoreByteEqual) left right)) (branch CoreNotLiteral . (corePrimitiveApplication2 (constructor CorePrimitive CoreByteEqual) left right))))) def reduceCoreByteLess : (pi unrestricted left : (family CoreTerm) . (pi unrestricted right : (family CoreTerm) . (family CoreTerm))) = (lambda unrestricted left : (family CoreTerm) . (lambda unrestricted right : (family CoreTerm) . (eliminate CoreLiteralInspection (lambda unrestricted leftInspection : (family CoreLiteralInspection) . (family CoreTerm)) (inspectCoreLiteral left) (branch CoreNaturalInspected value . (corePrimitiveApplication2 (constructor CorePrimitive CoreByteLess) left right)) (branch CoreByteInspected leftValue . (eliminate CoreLiteralInspection (lambda unrestricted rightInspection : (family CoreLiteralInspection) . (family CoreTerm)) (inspectCoreLiteral right) (branch CoreNaturalInspected value . (corePrimitiveApplication2 (constructor CorePrimitive CoreByteLess) left right)) (branch CoreByteInspected rightValue . (constructor CoreTerm CoreNaturalLiteral (Compiler.NaturalMagnitudeArithmetic/magnitudeFromNatural (byte-less-than leftValue rightValue)))) (branch CoreBytesInspected value . (corePrimitiveApplication2 (constructor CorePrimitive CoreByteLess) left right)) (branch CoreNotLiteral . (corePrimitiveApplication2 (constructor CorePrimitive CoreByteLess) left right)))) (branch CoreBytesInspected value . (corePrimitiveApplication2 (constructor CorePrimitive CoreByteLess) left right)) (branch CoreNotLiteral . (corePrimitiveApplication2 (constructor CorePrimitive CoreByteLess) left right))))) def reduceCoreNaturalLess : (pi unrestricted left : (family CoreTerm) . (pi unrestricted right : (family CoreTerm) . (family CoreTerm))) = (lambda unrestricted left : (family CoreTerm) . (lambda unrestricted right : (family CoreTerm) . (eliminate CoreLiteralInspection (lambda unrestricted leftInspection : (family CoreLiteralInspection) . (family CoreTerm)) (inspectCoreLiteral left) (branch CoreNaturalInspected leftValue . (eliminate CoreLiteralInspection (lambda unrestricted rightInspection : (family CoreLiteralInspection) . (family CoreTerm)) (inspectCoreLiteral right) (branch CoreNaturalInspected rightValue . (constructor CoreTerm CoreNaturalLiteral (Compiler.NaturalMagnitudeArithmetic/magnitudeFromNatural (Compiler.NaturalMagnitudeArithmetic/magnitudeLess leftValue rightValue)))) (branch CoreByteInspected value . (corePrimitiveApplication2 (constructor CorePrimitive CoreNaturalLess) left right)) (branch CoreBytesInspected value . (corePrimitiveApplication2 (constructor CorePrimitive CoreNaturalLess) left right)) (branch CoreNotLiteral . (corePrimitiveApplication2 (constructor CorePrimitive CoreNaturalLess) left right)))) (branch CoreByteInspected value . (corePrimitiveApplication2 (constructor CorePrimitive CoreNaturalLess) left right)) (branch CoreBytesInspected value . (corePrimitiveApplication2 (constructor CorePrimitive CoreNaturalLess) left right)) (branch CoreNotLiteral . (corePrimitiveApplication2 (constructor CorePrimitive CoreNaturalLess) left right))))) def reduceCoreBytesAppend : (pi unrestricted left : (family CoreTerm) . (pi unrestricted right : (family CoreTerm) . (family CoreTerm))) = (lambda unrestricted left : (family CoreTerm) . (lambda unrestricted right : (family CoreTerm) . (eliminate CoreLiteralInspection (lambda unrestricted leftInspection : (family CoreLiteralInspection) . (family CoreTerm)) (inspectCoreLiteral left) (branch CoreNaturalInspected value . (corePrimitiveApplication2 (constructor CorePrimitive CoreBytesAppend) left right)) (branch CoreByteInspected value . (corePrimitiveApplication2 (constructor CorePrimitive CoreBytesAppend) left right)) (branch CoreBytesInspected leftValue . (eliminate CoreLiteralInspection (lambda unrestricted rightInspection : (family CoreLiteralInspection) . (family CoreTerm)) (inspectCoreLiteral right) (branch CoreNaturalInspected value . (corePrimitiveApplication2 (constructor CorePrimitive CoreBytesAppend) left right)) (branch CoreByteInspected value . (corePrimitiveApplication2 (constructor CorePrimitive CoreBytesAppend) left right)) (branch CoreBytesInspected rightValue . (constructor CoreTerm CoreBytesLiteral (bytes-append leftValue rightValue))) (branch CoreNotLiteral . (corePrimitiveApplication2 (constructor CorePrimitive CoreBytesAppend) left right)))) (branch CoreNotLiteral . (corePrimitiveApplication2 (constructor CorePrimitive CoreBytesAppend) left right))))) def reduceCoreBytesEqual : (pi unrestricted left : (family CoreTerm) . (pi unrestricted right : (family CoreTerm) . (family CoreTerm))) = (lambda unrestricted left : (family CoreTerm) . (lambda unrestricted right : (family CoreTerm) . (eliminate CoreLiteralInspection (lambda unrestricted leftInspection : (family CoreLiteralInspection) . (family CoreTerm)) (inspectCoreLiteral left) (branch CoreNaturalInspected value . (corePrimitiveApplication2 (constructor CorePrimitive CoreBytesEqual) left right)) (branch CoreByteInspected value . (corePrimitiveApplication2 (constructor CorePrimitive CoreBytesEqual) left right)) (branch CoreBytesInspected leftValue . (eliminate CoreLiteralInspection (lambda unrestricted rightInspection : (family CoreLiteralInspection) . (family CoreTerm)) (inspectCoreLiteral right) (branch CoreNaturalInspected value . (corePrimitiveApplication2 (constructor CorePrimitive CoreBytesEqual) left right)) (branch CoreByteInspected value . (corePrimitiveApplication2 (constructor CorePrimitive CoreBytesEqual) left right)) (branch CoreBytesInspected rightValue . (constructor CoreTerm CoreNaturalLiteral (Compiler.NaturalMagnitudeArithmetic/magnitudeFromNatural (bytes-equal leftValue rightValue)))) (branch CoreNotLiteral . (corePrimitiveApplication2 (constructor CorePrimitive CoreBytesEqual) left right)))) (branch CoreNotLiteral . (corePrimitiveApplication2 (constructor CorePrimitive CoreBytesEqual) left right))))) def reduceCoreBytesCons : (pi unrestricted left : (family CoreTerm) . (pi unrestricted right : (family CoreTerm) . (family CoreTerm))) = (lambda unrestricted left : (family CoreTerm) . (lambda unrestricted right : (family CoreTerm) . (eliminate CoreLiteralInspection (lambda unrestricted leftInspection : (family CoreLiteralInspection) . (family CoreTerm)) (inspectCoreLiteral left) (branch CoreNaturalInspected value . (corePrimitiveApplication2 (constructor CorePrimitive CoreBytesCons) left right)) (branch CoreByteInspected leftValue . (eliminate CoreLiteralInspection (lambda unrestricted rightInspection : (family CoreLiteralInspection) . (family CoreTerm)) (inspectCoreLiteral right) (branch CoreNaturalInspected value . (corePrimitiveApplication2 (constructor CorePrimitive CoreBytesCons) left right)) (branch CoreByteInspected value . (corePrimitiveApplication2 (constructor CorePrimitive CoreBytesCons) left right)) (branch CoreBytesInspected rightValue . (constructor CoreTerm CoreBytesLiteral (bytes-cons leftValue rightValue))) (branch CoreNotLiteral . (corePrimitiveApplication2 (constructor CorePrimitive CoreBytesCons) left right)))) (branch CoreBytesInspected value . (corePrimitiveApplication2 (constructor CorePrimitive CoreBytesCons) left right)) (branch CoreNotLiteral . (corePrimitiveApplication2 (constructor CorePrimitive CoreBytesCons) left right))))) def reduceAppliedCorePrimitive : (pi unrestricted primitive : (family CorePrimitive) . (pi unrestricted left : (family CoreTerm) . (pi unrestricted right : (family CoreTerm) . (family CoreTerm)))) = (lambda unrestricted primitive : (family CorePrimitive) . (eliminate CorePrimitive (lambda unrestricted value : (family CorePrimitive) . (pi unrestricted left : (family CoreTerm) . (pi unrestricted right : (family CoreTerm) . (family CoreTerm)))) primitive (branch CoreByteEqual . reduceCoreByteEqual) (branch CoreByteLess . reduceCoreByteLess) (branch CoreNaturalLess . reduceCoreNaturalLess) (branch CoreNaturalToByte . (corePrimitiveApplication2 primitive)) (branch CoreByteToNatural . (corePrimitiveApplication2 primitive)) (branch CoreBytesAppend . reduceCoreBytesAppend) (branch CoreBytesCons . reduceCoreBytesCons) (branch CoreBytesLength . (corePrimitiveApplication2 primitive)) (branch CoreNaturalEliminate . (corePrimitiveApplication2 primitive)) (branch CoreBytesEliminate . (corePrimitiveApplication2 primitive)) (branch CoreBytesEqual . reduceCoreBytesEqual) (branch CoreFileEffect . (corePrimitiveApplication2 primitive)) (branch CoreEffects . (corePrimitiveApplication2 primitive)) (branch CoreComputation . (corePrimitiveApplication2 primitive)) (branch CoreReturn . (corePrimitiveApplication2 primitive)) (branch CoreBind . (corePrimitiveApplication2 primitive)) (branch CoreReadFile . (corePrimitiveApplication2 primitive)) (branch CoreWriteFile . (corePrimitiveApplication2 primitive)) (branch CoreLinuxOpenNode . (corePrimitiveApplication2 primitive)) (branch CoreLinuxCloseNode . (corePrimitiveApplication2 primitive)) (branch CoreLinuxIoctl . (corePrimitiveApplication2 primitive)) (branch CoreLinuxMmap . (corePrimitiveApplication2 primitive)) (branch CoreLinuxMunmap . (corePrimitiveApplication2 primitive)) (branch CoreBytesSetIndex . (corePrimitiveApplication2 primitive)) (branch CoreBytesIndexNonzero . (corePrimitiveApplication2 primitive)) (branch CoreBytesSetFreeIndex . (corePrimitiveApplication2 primitive)) (branch CoreBytesBuilderType . (corePrimitiveApplication2 primitive)) (branch CoreBytesBuilderEmpty . (corePrimitiveApplication2 primitive)) (branch CoreBytesBuilderChunk . (corePrimitiveApplication2 primitive)) (branch CoreBytesBuilderAppend . (corePrimitiveApplication2 primitive)) (branch CoreBytesBuilderBuild . (corePrimitiveApplication2 primitive)) (branch CoreRuntimeImageV4Build . (corePrimitiveApplication2 primitive)) (branch CoreBytesHead . (corePrimitiveApplication2 primitive)) (branch CoreBytesTail . (corePrimitiveApplication2 primitive)) (branch CoreBytesChecksum . (corePrimitiveApplication2 primitive)))) def corePrimitiveApplication4 : (pi unrestricted primitive : (family CorePrimitive) . (pi unrestricted first : (family CoreTerm) . (pi unrestricted second : (family CoreTerm) . (pi unrestricted third : (family CoreTerm) . (pi unrestricted fourth : (family CoreTerm) . (family CoreTerm)))))) = (lambda unrestricted primitive : (family CorePrimitive) . (lambda unrestricted first : (family CoreTerm) . (lambda unrestricted second : (family CoreTerm) . (lambda unrestricted third : (family CoreTerm) . (lambda unrestricted fourth : (family CoreTerm) . (constructor CoreTerm CoreApplication (corePrimitiveApplication3 primitive first second third) fourth)))))) def applyCoreFunctionOnce : (pi unrestricted function : (family CoreTerm) . (pi unrestricted argument : (family CoreTerm) . (family CoreTerm))) = (lambda unrestricted function : (family CoreTerm) . (lambda unrestricted argument : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted value : (family CoreTerm) . (family CoreTerm)) function (branch CoreUniverse level . (constructor CoreTerm CoreApplication function argument)) (branch CoreNatural . (constructor CoreTerm CoreApplication function argument)) (branch CoreNaturalLiteral value . (constructor CoreTerm CoreApplication function argument)) (branch CoreBound index . (constructor CoreTerm CoreApplication function argument)) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . (constructor CoreTerm CoreApplication function argument)) (branch CoreLambda multiplicity domain body ih_domain ih_body . (substituteCoreTop argument body)) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . (constructor CoreTerm CoreApplication (substituteCoreTop value body) argument)) (branch CoreApplication nestedFunction nestedArgument ih_nestedFunction ih_nestedArgument . (constructor CoreTerm CoreApplication function argument)) (branch CoreNaturalArithmetic operation nestedFunction nestedArgument ih_nestedFunction ih_nestedArgument . (constructor CoreTerm CoreApplication function argument)) (branch CoreNaturalSuccessor predecessor ih_predecessor . (constructor CoreTerm CoreApplication function argument)) (branch CoreByte . (constructor CoreTerm CoreApplication function argument)) (branch CoreByteLiteral value . (constructor CoreTerm CoreApplication function argument)) (branch CoreBytes . (constructor CoreTerm CoreApplication function argument)) (branch CoreBytesLiteral value . (constructor CoreTerm CoreApplication function argument)) (branch CorePrimitiveTerm primitive . (constructor CoreTerm CoreApplication function argument)) (branch CoreTermSequenceEnd . (constructor CoreTerm CoreApplication function argument)) (branch CoreTermSequenceNext head tail ih_head ih_tail . (constructor CoreTerm CoreApplication function argument)) (branch CoreFamilyApplication familyName arguments ih_arguments . (constructor CoreTerm CoreApplication function argument)) (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . (constructor CoreTerm CoreApplication function argument)) (branch CoreEliminatorBranch constructorName binderCount body ih_body . (constructor CoreTerm CoreApplication function argument)) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . (constructor CoreTerm CoreApplication function argument))))) def reduceNaturalEliminateStep : (pi unrestricted successorCase : (family CoreTerm) . (pi unrestricted predecessor : Bytes . (pi unrestricted induction : (family CoreTerm) . (family CoreTerm)))) = (lambda unrestricted successorCase : (family CoreTerm) . (lambda unrestricted predecessor : Bytes . (lambda unrestricted induction : (family CoreTerm) . (applyCoreFunctionOnce (applyCoreFunctionOnce successorCase (constructor CoreTerm CoreNaturalLiteral predecessor)) induction)))) def reduceCoreNaturalEliminate : (pi unrestricted motive : (family CoreTerm) . (pi unrestricted zeroCase : (family CoreTerm) . (pi unrestricted successorCase : (family CoreTerm) . (pi unrestricted scrutinee : (family CoreTerm) . (family CoreTerm))))) = (lambda unrestricted motive : (family CoreTerm) . (lambda unrestricted zeroCase : (family CoreTerm) . (lambda unrestricted successorCase : (family CoreTerm) . (lambda unrestricted scrutinee : (family CoreTerm) . (eliminate CoreLiteralInspection (lambda unrestricted inspection : (family CoreLiteralInspection) . (family CoreTerm)) (inspectCoreLiteral scrutinee) (branch CoreNaturalInspected value . (second (Compiler.NaturalMagnitudeArithmetic/magnitudeIterate (sigma unrestricted predecessor : Bytes . (family CoreTerm)) value (lambda unrestricted state : (sigma unrestricted predecessor : Bytes . (family CoreTerm)) . (pair (sigma unrestricted predecessor : Bytes . (family CoreTerm)) (Compiler.NaturalMagnitudeArithmetic/magnitudeSuccessor (first state)) (reduceNaturalEliminateStep successorCase (first state) (second state)))) (pair (sigma unrestricted predecessor : Bytes . (family CoreTerm)) b"" zeroCase)))) (branch CoreByteInspected value . (corePrimitiveApplication4 (constructor CorePrimitive CoreNaturalEliminate) motive zeroCase successorCase scrutinee)) (branch CoreBytesInspected value . (corePrimitiveApplication4 (constructor CorePrimitive CoreNaturalEliminate) motive zeroCase successorCase scrutinee)) (branch CoreNotLiteral . (corePrimitiveApplication4 (constructor CorePrimitive CoreNaturalEliminate) motive zeroCase successorCase scrutinee))))))) def reduceBytesEliminateStep : (pi unrestricted consCase : (family CoreTerm) . (pi unrestricted head : Byte . (pi unrestricted tail : Bytes . (pi unrestricted induction : (family CoreTerm) . (family CoreTerm))))) = (lambda unrestricted consCase : (family CoreTerm) . (lambda unrestricted head : Byte . (lambda unrestricted tail : Bytes . (lambda unrestricted induction : (family CoreTerm) . (applyCoreFunctionOnce (applyCoreFunctionOnce (applyCoreFunctionOnce consCase (constructor CoreTerm CoreByteLiteral head)) (constructor CoreTerm CoreBytesLiteral tail)) induction))))) def reduceCoreBytesEliminate : (pi unrestricted motive : (family CoreTerm) . (pi unrestricted emptyCase : (family CoreTerm) . (pi unrestricted consCase : (family CoreTerm) . (pi unrestricted scrutinee : (family CoreTerm) . (family CoreTerm))))) = (lambda unrestricted motive : (family CoreTerm) . (lambda unrestricted emptyCase : (family CoreTerm) . (lambda unrestricted consCase : (family CoreTerm) . (lambda unrestricted scrutinee : (family CoreTerm) . (eliminate CoreLiteralInspection (lambda unrestricted inspection : (family CoreLiteralInspection) . (family CoreTerm)) (inspectCoreLiteral scrutinee) (branch CoreNaturalInspected value . (corePrimitiveApplication4 (constructor CorePrimitive CoreBytesEliminate) motive emptyCase consCase scrutinee)) (branch CoreByteInspected value . (corePrimitiveApplication4 (constructor CorePrimitive CoreBytesEliminate) motive emptyCase consCase scrutinee)) (branch CoreBytesInspected value . (bytes-eliminate (lambda unrestricted remaining : Bytes . (family CoreTerm)) emptyCase (reduceBytesEliminateStep consCase) value)) (branch CoreNotLiteral . (corePrimitiveApplication4 (constructor CorePrimitive CoreBytesEliminate) motive emptyCase consCase scrutinee))))))) def reduceAppliedCoreEliminator : (pi unrestricted primitive : (family CorePrimitive) . (pi unrestricted first : (family CoreTerm) . (pi unrestricted second : (family CoreTerm) . (pi unrestricted third : (family CoreTerm) . (pi unrestricted fourth : (family CoreTerm) . (family CoreTerm)))))) = (lambda unrestricted primitive : (family CorePrimitive) . (eliminate CorePrimitive (lambda unrestricted value : (family CorePrimitive) . (pi unrestricted first : (family CoreTerm) . (pi unrestricted second : (family CoreTerm) . (pi unrestricted third : (family CoreTerm) . (pi unrestricted fourth : (family CoreTerm) . (family CoreTerm)))))) primitive (branch CoreByteEqual . (corePrimitiveApplication4 primitive)) (branch CoreByteLess . (corePrimitiveApplication4 primitive)) (branch CoreNaturalLess . (corePrimitiveApplication4 primitive)) (branch CoreNaturalToByte . (corePrimitiveApplication4 primitive)) (branch CoreByteToNatural . (corePrimitiveApplication4 primitive)) (branch CoreBytesAppend . (corePrimitiveApplication4 primitive)) (branch CoreBytesCons . (corePrimitiveApplication4 primitive)) (branch CoreBytesLength . (corePrimitiveApplication4 primitive)) (branch CoreNaturalEliminate . reduceCoreNaturalEliminate) (branch CoreBytesEliminate . reduceCoreBytesEliminate) (branch CoreBytesEqual . (corePrimitiveApplication4 primitive)) (branch CoreFileEffect . (corePrimitiveApplication4 primitive)) (branch CoreEffects . (corePrimitiveApplication4 primitive)) (branch CoreComputation . (corePrimitiveApplication4 primitive)) (branch CoreReturn . (corePrimitiveApplication4 primitive)) (branch CoreBind . (corePrimitiveApplication4 primitive)) (branch CoreReadFile . (corePrimitiveApplication4 primitive)) (branch CoreWriteFile . (corePrimitiveApplication4 primitive)) (branch CoreLinuxOpenNode . (corePrimitiveApplication4 primitive)) (branch CoreLinuxCloseNode . (corePrimitiveApplication4 primitive)) (branch CoreLinuxIoctl . (corePrimitiveApplication4 primitive)) (branch CoreLinuxMmap . (corePrimitiveApplication4 primitive)) (branch CoreLinuxMunmap . (corePrimitiveApplication4 primitive)) (branch CoreBytesSetIndex . (corePrimitiveApplication4 primitive)) (branch CoreBytesIndexNonzero . (corePrimitiveApplication4 primitive)) (branch CoreBytesSetFreeIndex . (corePrimitiveApplication4 primitive)) (branch CoreBytesBuilderType . (corePrimitiveApplication4 primitive)) (branch CoreBytesBuilderEmpty . (corePrimitiveApplication4 primitive)) (branch CoreBytesBuilderChunk . (corePrimitiveApplication4 primitive)) (branch CoreBytesBuilderAppend . (corePrimitiveApplication4 primitive)) (branch CoreBytesBuilderBuild . (corePrimitiveApplication4 primitive)) (branch CoreRuntimeImageV4Build . (corePrimitiveApplication4 primitive)) (branch CoreBytesHead . (corePrimitiveApplication4 primitive)) (branch CoreBytesTail . (corePrimitiveApplication4 primitive)) (branch CoreBytesChecksum . (corePrimitiveApplication4 primitive)))) def finishCoreNaturalWorkStep = (lambda unrestricted predecessor : Bytes . (lambda unrestricted result : (family CoreWorkResult) . (eliminate CoreWorkResult (lambda unrestricted current : (family CoreWorkResult) . (family CoreNaturalWorkState)) result (branch CoreWorkCompleted term budget . (constructor CoreNaturalWorkState CoreNaturalWorkActive (Compiler.NaturalMagnitudeArithmetic/magnitudeSuccessor predecessor) term budget)) (branch CoreWorkExhausted budget . (constructor CoreNaturalWorkState CoreNaturalWorkStopped budget))))) def stepCoreNaturalWork = (lambda unrestricted successorCase : (family CoreTerm) . (lambda unrestricted state : (family CoreNaturalWorkState) . (eliminate CoreNaturalWorkState (lambda unrestricted current : (family CoreNaturalWorkState) . (family CoreNaturalWorkState)) state (branch CoreNaturalWorkActive predecessor term budget . (finishCoreNaturalWorkStep predecessor (coreWorkBind (workApplyCoreFunctionOnce successorCase (constructor CoreTerm CoreNaturalLiteral predecessor) budget) (lambda unrestricted applied : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (workApplyCoreFunctionOnce applied term remaining)))))) (branch CoreNaturalWorkStopped budget . state)))) -- Every composed block checks for exhaustion before entering its inner loop. def repeatCoreNaturalWorkSmall = (lambda unrestricted count : Nat . (lambda unrestricted step : (pi unrestricted state : (family CoreNaturalWorkState) . (family CoreNaturalWorkState)) . (lambda unrestricted state : (family CoreNaturalWorkState) . (eliminate CoreNaturalWorkState (lambda unrestricted current : (family CoreNaturalWorkState) . (family CoreNaturalWorkState)) state (branch CoreNaturalWorkActive predecessor term budget . (nat-eliminate (lambda unrestricted index : Nat . (family CoreNaturalWorkState)) state (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family CoreNaturalWorkState) . (step induction))) count)) (branch CoreNaturalWorkStopped budget . state))))) def iterateCoreNaturalWork = (lambda unrestricted digits : Bytes . (lambda unrestricted step : (pi unrestricted state : (family CoreNaturalWorkState) . (family CoreNaturalWorkState)) . (lambda unrestricted seed : (family CoreNaturalWorkState) . (app (bytes-eliminate (lambda unrestricted remaining : Bytes . (pi unrestricted step : (pi unrestricted state : (family CoreNaturalWorkState) . (family CoreNaturalWorkState)) . (pi unrestricted seed : (family CoreNaturalWorkState) . (family CoreNaturalWorkState)))) (lambda unrestricted step : (pi unrestricted state : (family CoreNaturalWorkState) . (family CoreNaturalWorkState)) . (lambda unrestricted seed : (family CoreNaturalWorkState) . seed)) (lambda unrestricted head : Byte . (lambda unrestricted tail : Bytes . (lambda unrestricted continue : (pi unrestricted step : (pi unrestricted state : (family CoreNaturalWorkState) . (family CoreNaturalWorkState)) . (pi unrestricted seed : (family CoreNaturalWorkState) . (family CoreNaturalWorkState))) . (lambda unrestricted step : (pi unrestricted state : (family CoreNaturalWorkState) . (family CoreNaturalWorkState)) . (lambda unrestricted seed : (family CoreNaturalWorkState) . (continue (lambda unrestricted state : (family CoreNaturalWorkState) . (repeatCoreNaturalWorkSmall (byte-to-nat (byte 10)) step state)) (repeatCoreNaturalWorkSmall (byte-to-nat head) step seed))))))) digits) step seed)))) def finishCoreNaturalWork = (lambda unrestricted state : (family CoreNaturalWorkState) . (eliminate CoreNaturalWorkState (lambda unrestricted current : (family CoreNaturalWorkState) . (family CoreWorkResult)) state (branch CoreNaturalWorkActive predecessor term budget . (constructor CoreWorkResult CoreWorkCompleted term budget)) (branch CoreNaturalWorkStopped budget . (constructor CoreWorkResult CoreWorkExhausted budget)))) -- Each natural transition costs at least one unit. Reject an unaffordable -- count before iteration; substitutions then debit the shared remaining budget. def workNaturalEliminate = (lambda unrestricted digits : Bytes . (lambda unrestricted zeroCase : (family CoreTerm) . (lambda unrestricted successorCase : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (eliminate NormalizationCostResult (lambda unrestricted current : (family NormalizationCostResult) . (family CoreWorkResult)) (Compiler.NormalizationBudget/normalizationCostFromMagnitude digits) (branch NormalizationCostWord cost . (coreWorkCharge cost budget (lambda unrestricted remaining : (family NormalizationBudget) . (finishCoreNaturalWork (iterateCoreNaturalWork digits (stepCoreNaturalWork successorCase) (constructor CoreNaturalWorkState CoreNaturalWorkActive b"" zeroCase remaining)))))) (branch NormalizationCostTooLarge . (constructor CoreWorkResult CoreWorkExhausted budget)) (branch NormalizationCostInvalid . (constructor CoreWorkResult CoreWorkExhausted budget))))))) def workReduceNaturalEliminator = (lambda unrestricted motive : (family CoreTerm) . (lambda unrestricted zeroCase : (family CoreTerm) . (lambda unrestricted successorCase : (family CoreTerm) . (lambda unrestricted scrutinee : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (eliminate CoreLiteralInspection (lambda unrestricted current : (family CoreLiteralInspection) . (family CoreWorkResult)) (inspectCoreLiteral scrutinee) (branch CoreNaturalInspected digits . (workNaturalEliminate digits zeroCase successorCase budget)) (branch CoreByteInspected value . (constructor CoreWorkResult CoreWorkCompleted (corePrimitiveApplication4 (constructor CorePrimitive CoreNaturalEliminate) motive zeroCase successorCase scrutinee) budget)) (branch CoreBytesInspected value . (constructor CoreWorkResult CoreWorkCompleted (corePrimitiveApplication4 (constructor CorePrimitive CoreNaturalEliminate) motive zeroCase successorCase scrutinee) budget)) (branch CoreNotLiteral . (constructor CoreWorkResult CoreWorkCompleted (corePrimitiveApplication4 (constructor CorePrimitive CoreNaturalEliminate) motive zeroCase successorCase scrutinee) budget)))))))) -- Natural folds and beta substitution share the meter. Primitive byte payload -- costs and generic family induction still need separate accounting. def coreWorkChargeBytes = (lambda unrestricted payload : Bytes . (lambda unrestricted budget : (family NormalizationBudget) . (lambda unrestricted continue : (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult)) . (eliminate NormalizationChargeResult (lambda unrestricted result : (family NormalizationChargeResult) . (family CoreWorkResult)) (chargeNormalizationBytes payload budget) (branch NormalizationCharged remaining . (continue remaining)) (branch NormalizationChargeExhausted remaining amount . (constructor CoreWorkResult CoreWorkExhausted remaining)) (branch NormalizationChargeInvalid . (constructor CoreWorkResult CoreWorkExhausted budget)))))) def workInspectCoreBytes = (lambda unrestricted value : (family CoreTerm) . (lambda unrestricted selected : (pi unrestricted payload : Bytes . (family CoreWorkResult)) . (lambda unrestricted fallback : (pi unrestricted force : Nat . (family CoreWorkResult)) . (eliminate CoreLiteralInspection (lambda unrestricted current : (family CoreLiteralInspection) . (family CoreWorkResult)) (inspectCoreLiteral value) (branch CoreNaturalInspected payload . (fallback zero)) (branch CoreByteInspected payload . (fallback zero)) (branch CoreBytesInspected payload . (selected payload)) (branch CoreNotLiteral . (fallback zero)))))) def workInspectCoreNatural = (lambda unrestricted value : (family CoreTerm) . (lambda unrestricted selected : (pi unrestricted payload : Bytes . (family CoreWorkResult)) . (lambda unrestricted fallback : (pi unrestricted force : Nat . (family CoreWorkResult)) . (eliminate CoreLiteralInspection (lambda unrestricted current : (family CoreLiteralInspection) . (family CoreWorkResult)) (inspectCoreLiteral value) (branch CoreNaturalInspected payload . (selected payload)) (branch CoreByteInspected payload . (fallback zero)) (branch CoreBytesInspected payload . (fallback zero)) (branch CoreNotLiteral . (fallback zero)))))) def workInspectCoreByte = (lambda unrestricted value : (family CoreTerm) . (lambda unrestricted selected : (pi unrestricted payload : Byte . (family CoreWorkResult)) . (lambda unrestricted fallback : (pi unrestricted force : Nat . (family CoreWorkResult)) . (eliminate CoreLiteralInspection (lambda unrestricted current : (family CoreLiteralInspection) . (family CoreWorkResult)) (inspectCoreLiteral value) (branch CoreNaturalInspected payload . (fallback zero)) (branch CoreByteInspected payload . (selected payload)) (branch CoreBytesInspected payload . (fallback zero)) (branch CoreNotLiteral . (fallback zero)))))) -- The inspection callback selects only the literal kind admitted by this primitive. def workReduceCorePayloadPair = (lambda unrestricted inspect : (pi unrestricted term : (family CoreTerm) . (pi unrestricted selected : (pi unrestricted payload : Bytes . (family CoreWorkResult)) . (pi unrestricted fallback : (pi unrestricted force : Nat . (family CoreWorkResult)) . (family CoreWorkResult)))) . (lambda unrestricted primitive : (family CorePrimitive) . (lambda unrestricted left : (family CoreTerm) . (lambda unrestricted right : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (app (lambda unrestricted neutral : (pi unrestricted force : Nat . (family CoreWorkResult)) . (inspect left (lambda unrestricted leftPayload : Bytes . (inspect right (lambda unrestricted rightPayload : Bytes . (coreWorkChargeBytes leftPayload budget (lambda unrestricted afterLeft : (family NormalizationBudget) . (coreWorkChargeBytes rightPayload afterLeft (lambda unrestricted afterRight : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCorePrimitive primitive left right) afterRight)))))) neutral)) neutral)) (lambda unrestricted force : Nat . (constructor CoreWorkResult CoreWorkCompleted (corePrimitiveApplication2 primitive left right) budget)))))))) def workReduceCorePayloadUnary = (lambda unrestricted inspect : (pi unrestricted term : (family CoreTerm) . (pi unrestricted selected : (pi unrestricted payload : Bytes . (family CoreWorkResult)) . (pi unrestricted fallback : (pi unrestricted force : Nat . (family CoreWorkResult)) . (family CoreWorkResult)))) . (lambda unrestricted primitive : (family CorePrimitive) . (lambda unrestricted argument : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (inspect argument (lambda unrestricted payload : Bytes . (coreWorkChargeBytes payload budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (reduceDirectCorePrimitive primitive argument) remaining)))) (lambda unrestricted force : Nat . (constructor CoreWorkResult CoreWorkCompleted (corePrimitiveApplication primitive argument) budget))))))) def workReduceCoreBytesCons = (lambda unrestricted left : (family CoreTerm) . (lambda unrestricted right : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (app (lambda unrestricted neutral : (pi unrestricted force : Nat . (family CoreWorkResult)) . (workInspectCoreByte left (lambda unrestricted head : Byte . (workInspectCoreBytes right (lambda unrestricted tail : Bytes . (coreWorkCharge coreWorkOne budget (lambda unrestricted afterHead : (family NormalizationBudget) . (coreWorkChargeBytes tail afterHead (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (reduceCoreBytesCons left right) remaining)))))) neutral)) neutral)) (lambda unrestricted force : Nat . (constructor CoreWorkResult CoreWorkCompleted (corePrimitiveApplication2 (constructor CorePrimitive CoreBytesCons) left right) budget)))))) def workReduceCoreBytesAppend = (workReduceCorePayloadPair workInspectCoreBytes (constructor CorePrimitive CoreBytesAppend)) def workReduceAppliedCorePrimitive = (lambda unrestricted primitive : (family CorePrimitive) . (lambda unrestricted left : (family CoreTerm) . (lambda unrestricted right : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (eliminate CorePrimitive (lambda unrestricted current : (family CorePrimitive) . (family CoreWorkResult)) primitive (branch CoreByteEqual . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCorePrimitive primitive left right) budget)) (branch CoreByteLess . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCorePrimitive primitive left right) budget)) (branch CoreNaturalLess . (workReduceCorePayloadPair workInspectCoreNatural primitive left right budget)) (branch CoreNaturalToByte . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCorePrimitive primitive left right) budget)) (branch CoreByteToNatural . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCorePrimitive primitive left right) budget)) (branch CoreBytesAppend . (workReduceCoreBytesAppend left right budget)) (branch CoreBytesCons . (workReduceCoreBytesCons left right budget)) (branch CoreBytesLength . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCorePrimitive primitive left right) budget)) (branch CoreNaturalEliminate . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCorePrimitive primitive left right) budget)) (branch CoreBytesEliminate . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCorePrimitive primitive left right) budget)) (branch CoreBytesEqual . (workReduceCorePayloadPair workInspectCoreBytes primitive left right budget)) (branch CoreFileEffect . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCorePrimitive primitive left right) budget)) (branch CoreEffects . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCorePrimitive primitive left right) budget)) (branch CoreComputation . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCorePrimitive primitive left right) budget)) (branch CoreReturn . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCorePrimitive primitive left right) budget)) (branch CoreBind . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCorePrimitive primitive left right) budget)) (branch CoreReadFile . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCorePrimitive primitive left right) budget)) (branch CoreWriteFile . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCorePrimitive primitive left right) budget)) (branch CoreLinuxOpenNode . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCorePrimitive primitive left right) budget)) (branch CoreLinuxCloseNode . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCorePrimitive primitive left right) budget)) (branch CoreLinuxIoctl . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCorePrimitive primitive left right) budget)) (branch CoreLinuxMmap . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCorePrimitive primitive left right) budget)) (branch CoreLinuxMunmap . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCorePrimitive primitive left right) budget)) (branch CoreBytesSetIndex . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCorePrimitive primitive left right) budget)) (branch CoreBytesIndexNonzero . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCorePrimitive primitive left right) budget)) (branch CoreBytesSetFreeIndex . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCorePrimitive primitive left right) budget)) (branch CoreBytesBuilderType . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCorePrimitive primitive left right) budget)) (branch CoreBytesBuilderEmpty . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCorePrimitive primitive left right) budget)) (branch CoreBytesBuilderChunk . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCorePrimitive primitive left right) budget)) (branch CoreBytesBuilderAppend . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCorePrimitive primitive left right) budget)) (branch CoreBytesBuilderBuild . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCorePrimitive primitive left right) budget)) (branch CoreRuntimeImageV4Build . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCorePrimitive primitive left right) budget)) (branch CoreBytesHead . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCorePrimitive primitive left right) budget)) (branch CoreBytesTail . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCorePrimitive primitive left right) budget)) (branch CoreBytesChecksum . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCorePrimitive primitive left right) budget))))))) def workReduceDirectCorePrimitive = (lambda unrestricted primitive : (family CorePrimitive) . (lambda unrestricted argument : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (eliminate CorePrimitive (lambda unrestricted current : (family CorePrimitive) . (family CoreWorkResult)) primitive (branch CoreByteEqual . (constructor CoreWorkResult CoreWorkCompleted (reduceDirectCorePrimitive primitive argument) budget)) (branch CoreByteLess . (constructor CoreWorkResult CoreWorkCompleted (reduceDirectCorePrimitive primitive argument) budget)) (branch CoreNaturalLess . (constructor CoreWorkResult CoreWorkCompleted (reduceDirectCorePrimitive primitive argument) budget)) (branch CoreNaturalToByte . (workReduceCorePayloadUnary workInspectCoreNatural primitive argument budget)) (branch CoreByteToNatural . (constructor CoreWorkResult CoreWorkCompleted (reduceDirectCorePrimitive primitive argument) budget)) (branch CoreBytesAppend . (constructor CoreWorkResult CoreWorkCompleted (reduceDirectCorePrimitive primitive argument) budget)) (branch CoreBytesCons . (constructor CoreWorkResult CoreWorkCompleted (reduceDirectCorePrimitive primitive argument) budget)) (branch CoreBytesLength . (workReduceCorePayloadUnary workInspectCoreBytes primitive argument budget)) (branch CoreNaturalEliminate . (constructor CoreWorkResult CoreWorkCompleted (reduceDirectCorePrimitive primitive argument) budget)) (branch CoreBytesEliminate . (constructor CoreWorkResult CoreWorkCompleted (reduceDirectCorePrimitive primitive argument) budget)) (branch CoreBytesEqual . (constructor CoreWorkResult CoreWorkCompleted (reduceDirectCorePrimitive primitive argument) budget)) (branch CoreFileEffect . (constructor CoreWorkResult CoreWorkCompleted (reduceDirectCorePrimitive primitive argument) budget)) (branch CoreEffects . (constructor CoreWorkResult CoreWorkCompleted (reduceDirectCorePrimitive primitive argument) budget)) (branch CoreComputation . (constructor CoreWorkResult CoreWorkCompleted (reduceDirectCorePrimitive primitive argument) budget)) (branch CoreReturn . (constructor CoreWorkResult CoreWorkCompleted (reduceDirectCorePrimitive primitive argument) budget)) (branch CoreBind . (constructor CoreWorkResult CoreWorkCompleted (reduceDirectCorePrimitive primitive argument) budget)) (branch CoreReadFile . (constructor CoreWorkResult CoreWorkCompleted (reduceDirectCorePrimitive primitive argument) budget)) (branch CoreWriteFile . (constructor CoreWorkResult CoreWorkCompleted (reduceDirectCorePrimitive primitive argument) budget)) (branch CoreLinuxOpenNode . (constructor CoreWorkResult CoreWorkCompleted (reduceDirectCorePrimitive primitive argument) budget)) (branch CoreLinuxCloseNode . (constructor CoreWorkResult CoreWorkCompleted (reduceDirectCorePrimitive primitive argument) budget)) (branch CoreLinuxIoctl . (constructor CoreWorkResult CoreWorkCompleted (reduceDirectCorePrimitive primitive argument) budget)) (branch CoreLinuxMmap . (constructor CoreWorkResult CoreWorkCompleted (reduceDirectCorePrimitive primitive argument) budget)) (branch CoreLinuxMunmap . (constructor CoreWorkResult CoreWorkCompleted (reduceDirectCorePrimitive primitive argument) budget)) (branch CoreBytesSetIndex . (constructor CoreWorkResult CoreWorkCompleted (reduceDirectCorePrimitive primitive argument) budget)) (branch CoreBytesIndexNonzero . (constructor CoreWorkResult CoreWorkCompleted (reduceDirectCorePrimitive primitive argument) budget)) (branch CoreBytesSetFreeIndex . (constructor CoreWorkResult CoreWorkCompleted (reduceDirectCorePrimitive primitive argument) budget)) (branch CoreBytesBuilderType . (constructor CoreWorkResult CoreWorkCompleted (reduceDirectCorePrimitive primitive argument) budget)) (branch CoreBytesBuilderEmpty . (constructor CoreWorkResult CoreWorkCompleted (reduceDirectCorePrimitive primitive argument) budget)) (branch CoreBytesBuilderChunk . (constructor CoreWorkResult CoreWorkCompleted (reduceDirectCorePrimitive primitive argument) budget)) (branch CoreBytesBuilderAppend . (constructor CoreWorkResult CoreWorkCompleted (reduceDirectCorePrimitive primitive argument) budget)) (branch CoreBytesBuilderBuild . (constructor CoreWorkResult CoreWorkCompleted (reduceDirectCorePrimitive primitive argument) budget)) (branch CoreRuntimeImageV4Build . (constructor CoreWorkResult CoreWorkCompleted (reduceDirectCorePrimitive primitive argument) budget)) (branch CoreBytesHead . (constructor CoreWorkResult CoreWorkCompleted (reduceDirectCorePrimitive primitive argument) budget)) (branch CoreBytesTail . (constructor CoreWorkResult CoreWorkCompleted (reduceDirectCorePrimitive primitive argument) budget)) (branch CoreBytesChecksum . (constructor CoreWorkResult CoreWorkCompleted (reduceDirectCorePrimitive primitive argument) budget)))))) -- The payload charge bounds construction of the fold continuations. Each -- demanded branch application/substitution then consumes the same remaining budget. def workReduceBytesEliminateStep = (lambda unrestricted consCase : (family CoreTerm) . (lambda unrestricted head : Byte . (lambda unrestricted tail : Bytes . (lambda unrestricted induction : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkBind (workApplyCoreFunctionOnce consCase (constructor CoreTerm CoreByteLiteral head) budget) (lambda unrestricted withHead : (family CoreTerm) . (lambda unrestricted afterHead : (family NormalizationBudget) . (coreWorkBind (workApplyCoreFunctionOnce withHead (constructor CoreTerm CoreBytesLiteral tail) afterHead) (lambda unrestricted withTail : (family CoreTerm) . (lambda unrestricted afterTail : (family NormalizationBudget) . (workApplyCoreFunctionOnce withTail induction afterTail)))))))))))) def workReduceBytesEliminator = (lambda unrestricted motive : (family CoreTerm) . (lambda unrestricted emptyCase : (family CoreTerm) . (lambda unrestricted consCase : (family CoreTerm) . (lambda unrestricted scrutinee : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (workInspectCoreBytes scrutinee (lambda unrestricted payload : Bytes . (coreWorkChargeBytes payload budget (lambda unrestricted remaining : (family NormalizationBudget) . (app (bytes-eliminate (lambda unrestricted current : Bytes . (pi unrestricted allowance : (family NormalizationBudget) . (family CoreWorkResult))) (lambda unrestricted allowance : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted emptyCase allowance)) (lambda unrestricted head : Byte . (lambda unrestricted tail : Bytes . (lambda unrestricted induction : (pi unrestricted allowance : (family NormalizationBudget) . (family CoreWorkResult)) . (lambda unrestricted allowance : (family NormalizationBudget) . (coreWorkBind (induction allowance) (lambda unrestricted value : (family CoreTerm) . (lambda unrestricted afterInduction : (family NormalizationBudget) . (workReduceBytesEliminateStep consCase head tail value afterInduction)))))))) payload) remaining)))) (lambda unrestricted force : Nat . (constructor CoreWorkResult CoreWorkCompleted (corePrimitiveApplication4 (constructor CorePrimitive CoreBytesEliminate) motive emptyCase consCase scrutinee) budget)))))))) def workReduceAppliedEliminator = (lambda unrestricted primitive : (family CorePrimitive) . (lambda unrestricted first : (family CoreTerm) . (lambda unrestricted second : (family CoreTerm) . (lambda unrestricted third : (family CoreTerm) . (lambda unrestricted fourth : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (eliminate CorePrimitive (lambda unrestricted current : (family CorePrimitive) . (family CoreWorkResult)) primitive (branch CoreByteEqual . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCoreEliminator primitive first second third fourth) budget)) (branch CoreByteLess . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCoreEliminator primitive first second third fourth) budget)) (branch CoreNaturalLess . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCoreEliminator primitive first second third fourth) budget)) (branch CoreNaturalToByte . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCoreEliminator primitive first second third fourth) budget)) (branch CoreByteToNatural . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCoreEliminator primitive first second third fourth) budget)) (branch CoreBytesAppend . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCoreEliminator primitive first second third fourth) budget)) (branch CoreBytesCons . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCoreEliminator primitive first second third fourth) budget)) (branch CoreBytesLength . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCoreEliminator primitive first second third fourth) budget)) (branch CoreNaturalEliminate . (workReduceNaturalEliminator first second third fourth budget)) (branch CoreBytesEliminate . (workReduceBytesEliminator first second third fourth budget)) (branch CoreBytesEqual . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCoreEliminator primitive first second third fourth) budget)) (branch CoreFileEffect . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCoreEliminator primitive first second third fourth) budget)) (branch CoreEffects . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCoreEliminator primitive first second third fourth) budget)) (branch CoreComputation . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCoreEliminator primitive first second third fourth) budget)) (branch CoreReturn . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCoreEliminator primitive first second third fourth) budget)) (branch CoreBind . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCoreEliminator primitive first second third fourth) budget)) (branch CoreReadFile . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCoreEliminator primitive first second third fourth) budget)) (branch CoreWriteFile . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCoreEliminator primitive first second third fourth) budget)) (branch CoreLinuxOpenNode . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCoreEliminator primitive first second third fourth) budget)) (branch CoreLinuxCloseNode . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCoreEliminator primitive first second third fourth) budget)) (branch CoreLinuxIoctl . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCoreEliminator primitive first second third fourth) budget)) (branch CoreLinuxMmap . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCoreEliminator primitive first second third fourth) budget)) (branch CoreLinuxMunmap . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCoreEliminator primitive first second third fourth) budget)) (branch CoreBytesSetIndex . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCoreEliminator primitive first second third fourth) budget)) (branch CoreBytesIndexNonzero . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCoreEliminator primitive first second third fourth) budget)) (branch CoreBytesSetFreeIndex . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCoreEliminator primitive first second third fourth) budget)) (branch CoreBytesBuilderType . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCoreEliminator primitive first second third fourth) budget)) (branch CoreBytesBuilderEmpty . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCoreEliminator primitive first second third fourth) budget)) (branch CoreBytesBuilderChunk . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCoreEliminator primitive first second third fourth) budget)) (branch CoreBytesBuilderAppend . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCoreEliminator primitive first second third fourth) budget)) (branch CoreBytesBuilderBuild . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCoreEliminator primitive first second third fourth) budget)) (branch CoreRuntimeImageV4Build . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCoreEliminator primitive first second third fourth) budget)) (branch CoreBytesHead . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCoreEliminator primitive first second third fourth) budget)) (branch CoreBytesTail . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCoreEliminator primitive first second third fourth) budget)) (branch CoreBytesChecksum . (constructor CoreWorkResult CoreWorkCompleted (reduceAppliedCoreEliminator primitive first second third fourth) budget))))))))) -- Search branch metadata under the shared budget; names are payload-charged. def workFindCoreEliminatorBranch = (lambda unrestricted constructorName : Bytes . (lambda unrestricted branches : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted value : (family CoreTerm) . (pi unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult)))) branches (branch CoreUniverse level . (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing) remaining)))))) (branch CoreNatural . (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing) remaining)))))) (branch CoreNaturalLiteral value . (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing) remaining)))))) (branch CoreBound index . (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing) remaining)))))) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing) remaining)))))) (branch CoreLambda multiplicity domain body ih_domain ih_body . (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing) remaining)))))) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing) remaining)))))) (branch CoreApplication function argument ih_function ih_argument . (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing) remaining)))))) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing) remaining)))))) (branch CoreNaturalSuccessor predecessor ih_predecessor . (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing) remaining)))))) (branch CoreByte . (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing) remaining)))))) (branch CoreByteLiteral value . (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing) remaining)))))) (branch CoreBytes . (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing) remaining)))))) (branch CoreBytesLiteral value . (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing) remaining)))))) (branch CorePrimitiveTerm primitive . (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing) remaining)))))) (branch CoreTermSequenceEnd . (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing) remaining)))))) (branch CoreTermSequenceNext head tail ih_head ih_tail . (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (ih_head (lambda unrestricted selection : (family CoreEliminatorBranchSelection) . (lambda unrestricted afterHead : (family NormalizationBudget) . (eliminate CoreEliminatorBranchSelection (lambda unrestricted current : (family CoreEliminatorBranchSelection) . (family CoreWorkResult)) selection (branch CoreEliminatorBranchSelected count body . (continuation selection afterHead)) (branch CoreEliminatorBranchMissing . (ih_tail continuation afterHead))))) remaining)))))) (branch CoreFamilyApplication familyName arguments ih_arguments . (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing) remaining)))))) (branch CoreConstructorApplication familyName nestedConstructorName arguments ih_arguments . (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing) remaining)))))) (branch CoreEliminatorBranch branchConstructorName binderCount body ih_body . (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkChargeBytes constructorName remaining (lambda unrestricted afterName : (family NormalizationBudget) . (coreWorkChargeBytes branchConstructorName afterName (lambda unrestricted afterBranchName : (family NormalizationBudget) . (coreWorkChoose (bytes-equal constructorName branchConstructorName) (lambda unrestricted force : Nat . (continuation (constructor CoreEliminatorBranchSelection CoreEliminatorBranchSelected binderCount body) afterBranchName)) (lambda unrestricted force : Nat . (continuation (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing) afterBranchName)))))))))))) (branch CoreEliminator familyName motive scrutinee nestedBranches ih_motive ih_scrutinee ih_branches . (lambda unrestricted continuation : (pi unrestricted selection : (family CoreEliminatorBranchSelection) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation (constructor CoreEliminatorBranchSelection CoreEliminatorBranchMissing) remaining))))))))) def workInstantiateCoreEliminatorBranch = (lambda unrestricted supplied : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted value : (family CoreTerm) . (pi unrestricted body : (family CoreTerm) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult)))) supplied (branch CoreUniverse level . (lambda unrestricted body : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted body remaining)))))) (branch CoreNatural . (lambda unrestricted body : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted body remaining)))))) (branch CoreNaturalLiteral value . (lambda unrestricted body : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted body remaining)))))) (branch CoreBound index . (lambda unrestricted body : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted body remaining)))))) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . (lambda unrestricted body : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted body remaining)))))) (branch CoreLambda multiplicity domain body ih_domain ih_body . (lambda unrestricted branchBody : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted branchBody remaining)))))) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . (lambda unrestricted branchBody : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted branchBody remaining)))))) (branch CoreApplication function argument ih_function ih_argument . (lambda unrestricted body : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted body remaining)))))) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . (lambda unrestricted body : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted body remaining)))))) (branch CoreNaturalSuccessor predecessor ih_predecessor . (lambda unrestricted body : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted body remaining)))))) (branch CoreByte . (lambda unrestricted body : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted body remaining)))))) (branch CoreByteLiteral value . (lambda unrestricted body : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted body remaining)))))) (branch CoreBytes . (lambda unrestricted body : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted body remaining)))))) (branch CoreBytesLiteral value . (lambda unrestricted body : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted body remaining)))))) (branch CorePrimitiveTerm primitive . (lambda unrestricted body : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted body remaining)))))) (branch CoreTermSequenceEnd . (lambda unrestricted body : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted body remaining)))))) (branch CoreTermSequenceNext head tail ih_head ih_tail . (lambda unrestricted body : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_tail body remaining) (lambda unrestricted afterTail : (family CoreTerm) . (lambda unrestricted afterTailBudget : (family NormalizationBudget) . (workSubstituteCoreTop head afterTail afterTailBudget))))))))) (branch CoreFamilyApplication familyName arguments ih_arguments . (lambda unrestricted body : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted body remaining)))))) (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . (lambda unrestricted body : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted body remaining)))))) (branch CoreEliminatorBranch constructorName binderCount body ih_body . (lambda unrestricted branchBody : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted branchBody remaining)))))) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . (lambda unrestricted body : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted body remaining)))))))) def workCountCoreTermSequence = (lambda unrestricted sequence : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted current : (family CoreTerm) . (pi unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult)))) sequence (branch CoreUniverse level . (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation zero remaining)))))) (branch CoreNatural . (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation zero remaining)))))) (branch CoreNaturalLiteral value . (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation zero remaining)))))) (branch CoreBound index . (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation zero remaining)))))) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation zero remaining)))))) (branch CoreLambda multiplicity domain body ih_domain ih_body . (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation zero remaining)))))) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation zero remaining)))))) (branch CoreApplication function argument ih_function ih_argument . (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation zero remaining)))))) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation zero remaining)))))) (branch CoreNaturalSuccessor predecessor ih_predecessor . (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation zero remaining)))))) (branch CoreByte . (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation zero remaining)))))) (branch CoreByteLiteral value . (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation zero remaining)))))) (branch CoreBytes . (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation zero remaining)))))) (branch CoreBytesLiteral value . (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation zero remaining)))))) (branch CorePrimitiveTerm primitive . (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation zero remaining)))))) (branch CoreTermSequenceEnd . (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation zero remaining)))))) (branch CoreTermSequenceNext head tail ih_head ih_tail . (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (ih_tail (lambda unrestricted count : Nat . (lambda unrestricted afterTail : (family NormalizationBudget) . (continuation (succ count) afterTail))) remaining)))))) (branch CoreFamilyApplication familyName arguments ih_arguments . (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation zero remaining)))))) (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation zero remaining)))))) (branch CoreEliminatorBranch constructorName binderCount body ih_body . (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation zero remaining)))))) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . (lambda unrestricted continuation : (pi unrestricted count : Nat . (pi unrestricted remaining : (family NormalizationBudget) . (family CoreWorkResult))) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (continuation zero remaining)))))))) def workReserveCoreSequenceProduct = (lambda unrestricted right : (family CoreTerm) . (lambda unrestricted left : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted current : (family CoreTerm) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) left (branch CoreUniverse level . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted left remaining))))) (branch CoreNatural . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted left remaining))))) (branch CoreNaturalLiteral value . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted left remaining))))) (branch CoreBound index . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted left remaining))))) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted left remaining))))) (branch CoreLambda multiplicity domain body ih_domain ih_body . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted left remaining))))) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted left remaining))))) (branch CoreApplication function argument ih_function ih_argument . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted left remaining))))) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted left remaining))))) (branch CoreNaturalSuccessor predecessor ih_predecessor . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted left remaining))))) (branch CoreByte . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted left remaining))))) (branch CoreByteLiteral value . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted left remaining))))) (branch CoreBytes . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted left remaining))))) (branch CoreBytesLiteral value . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted left remaining))))) (branch CorePrimitiveTerm primitive . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted left remaining))))) (branch CoreTermSequenceEnd . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted left remaining))))) (branch CoreTermSequenceNext head tail ih_head ih_tail . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_tail remaining) (lambda unrestricted ignored : (family CoreTerm) . (lambda unrestricted afterTail : (family NormalizationBudget) . (workCountCoreTermSequence right (lambda unrestricted count : Nat . (lambda unrestricted afterCount : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted left afterCount))) afterTail)))))))) (branch CoreFamilyApplication familyName arguments ih_arguments . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted left remaining))))) (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted left remaining))))) (branch CoreEliminatorBranch constructorName binderCount body ih_body . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted left remaining))))) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted left remaining)))))))) -- Reserve a conservative quadratic allowance for bounded arity arithmetic, -- counting, dropping and appending. Substitution consumes its own shared charges. def workReserveCoreEliminatorBookkeeping = (lambda unrestricted arguments : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (nat-eliminate (lambda unrestricted current : Nat . (family CoreWorkResult)) (constructor CoreWorkResult CoreWorkCompleted arguments budget) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family CoreWorkResult) . (coreWorkBind induction (lambda unrestricted ignored : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (workReserveCoreSequenceProduct arguments arguments remaining)))))) (byte-to-nat (byte 16))))) def workFinishCoreEliminatorReduction = (lambda unrestricted familyName : Bytes . (lambda unrestricted motive : (family CoreTerm) . (lambda unrestricted scrutinee : (family CoreTerm) . (lambda unrestricted branches : (family CoreTerm) . (lambda unrestricted arguments : (family CoreTerm) . (lambda unrestricted inductionCandidates : (family CoreTerm) . (lambda unrestricted selection : (family CoreEliminatorBranchSelection) . (lambda unrestricted budget : (family NormalizationBudget) . (app (lambda unrestricted neutral : (pi unrestricted force : Nat . (family CoreWorkResult)) . (eliminate CoreEliminatorBranchSelection (lambda unrestricted current : (family CoreEliminatorBranchSelection) . (family CoreWorkResult)) selection (branch CoreEliminatorBranchSelected binderCount body . (workCountCoreTermSequence arguments (lambda unrestricted argumentCount : Nat . (lambda unrestricted afterCount : (family NormalizationBudget) . (coreWorkChoose (coreNaturalAnd (nat-less-than binderCount (succ (naturalAdd argumentCount argumentCount))) (nat-less-than (nat-less-than binderCount argumentCount) (succ zero))) (lambda unrestricted force : Nat . (coreWorkBind (workReserveCoreEliminatorBookkeeping arguments afterCount) (lambda unrestricted ignored : (family CoreTerm) . (lambda unrestricted afterBookkeeping : (family NormalizationBudget) . (app (lambda unrestricted recursiveCount : Nat . (app (lambda unrestricted valueCount : Nat . (app (lambda unrestricted supplied : (family CoreTerm) . (coreWorkChoose (naturalEqual (coreTermSequenceCount supplied) binderCount) (lambda unrestricted force : Nat . (workInstantiateCoreEliminatorBranch supplied body afterBookkeeping)) (lambda unrestricted force : Nat . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreEliminator familyName motive scrutinee branches) afterBookkeeping)))) (appendCoreTermSequenceForEliminator arguments (dropCoreTermSequenceForEliminator inductionCandidates valueCount)))) (coreNaturalSaturatingSubtract argumentCount recursiveCount))) (coreNaturalSaturatingSubtract binderCount argumentCount)))))) (lambda unrestricted force : Nat . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreEliminator familyName motive scrutinee branches) afterCount))))) budget)) (branch CoreEliminatorBranchMissing . (neutral zero)))) (lambda unrestricted force : Nat . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreEliminator familyName motive scrutinee branches) budget))))))))))) def workReduceCoreGenericEliminator = (lambda unrestricted familyName : Bytes . (lambda unrestricted motive : (family CoreTerm) . (lambda unrestricted scrutinee : (family CoreTerm) . (lambda unrestricted branches : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted current : (family CoreTerm) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) scrutinee (branch CoreUniverse level . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreEliminator familyName motive scrutinee branches) remaining))))) (branch CoreNatural . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreEliminator familyName motive scrutinee branches) remaining))))) (branch CoreNaturalLiteral value . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreEliminator familyName motive scrutinee branches) remaining))))) (branch CoreBound index . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreEliminator familyName motive scrutinee branches) remaining))))) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreEliminator familyName motive scrutinee branches) remaining))))) (branch CoreLambda multiplicity domain body ih_domain ih_body . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreEliminator familyName motive scrutinee branches) remaining))))) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_value remaining) (lambda unrestricted newValue : (family CoreTerm) . (lambda unrestricted afterValue : (family NormalizationBudget) . (coreWorkBind (ih_body afterValue) (lambda unrestricted newBody : (family CoreTerm) . (lambda unrestricted afterBody : (family NormalizationBudget) . (workSubstituteCoreTop newValue newBody afterBody))))))))))) (branch CoreApplication function argument ih_function ih_argument . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreEliminator familyName motive scrutinee branches) remaining))))) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreEliminator familyName motive scrutinee branches) remaining))))) (branch CoreNaturalSuccessor predecessor ih_predecessor . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreEliminator familyName motive scrutinee branches) remaining))))) (branch CoreByte . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreEliminator familyName motive scrutinee branches) remaining))))) (branch CoreByteLiteral value . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreEliminator familyName motive scrutinee branches) remaining))))) (branch CoreBytes . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreEliminator familyName motive scrutinee branches) remaining))))) (branch CoreBytesLiteral value . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreEliminator familyName motive scrutinee branches) remaining))))) (branch CorePrimitiveTerm primitive . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreEliminator familyName motive scrutinee branches) remaining))))) (branch CoreTermSequenceEnd . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreTermSequenceEnd) remaining))))) (branch CoreTermSequenceNext head tail ih_head ih_tail . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_head remaining) (lambda unrestricted newHead : (family CoreTerm) . (lambda unrestricted afterHead : (family NormalizationBudget) . (coreWorkBind (ih_tail afterHead) (lambda unrestricted newTail : (family CoreTerm) . (lambda unrestricted afterTail : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreTermSequenceNext newHead newTail) afterTail))))))))))) (branch CoreFamilyApplication constructorFamily arguments ih_arguments . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreEliminator familyName motive scrutinee branches) remaining))))) (branch CoreConstructorApplication constructorFamily constructorName arguments ih_arguments . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkChargeBytes familyName remaining (lambda unrestricted afterName : (family NormalizationBudget) . (coreWorkChargeBytes constructorFamily afterName (lambda unrestricted afterFamily : (family NormalizationBudget) . (coreWorkChoose (bytes-equal familyName constructorFamily) (lambda unrestricted force : Nat . (workFindCoreEliminatorBranch constructorName branches (lambda unrestricted selection : (family CoreEliminatorBranchSelection) . (lambda unrestricted afterSelection : (family NormalizationBudget) . (coreWorkBind (ih_arguments afterSelection) (lambda unrestricted candidates : (family CoreTerm) . (lambda unrestricted afterArguments : (family NormalizationBudget) . (workFinishCoreEliminatorReduction familyName motive scrutinee branches arguments candidates selection afterArguments)))))) afterFamily)) (lambda unrestricted force : Nat . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreEliminator familyName motive scrutinee branches) afterFamily))))))))))) (branch CoreEliminatorBranch constructorName binderCount body ih_body . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreEliminator familyName motive scrutinee branches) remaining))))) (branch CoreEliminator nestedFamily nestedMotive nestedScrutinee nestedBranches ih_motive ih_scrutinee ih_branches . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreEliminator familyName motive scrutinee branches) remaining)))))))))) -- Both payloads must already be charged before this bounded product walk. def workReserveCorePayloadProduct = (lambda unrestricted rows : Bytes . (lambda unrestricted columns : Bytes . (bytes-eliminate (lambda unrestricted current : Bytes . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) (lambda unrestricted budget : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreNatural) budget)) (lambda unrestricted head : Byte . (lambda unrestricted tail : Bytes . (lambda unrestricted induction : (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult)) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkBind (induction budget) (lambda unrestricted ignored : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkChargeBytes columns remaining (lambda unrestricted afterRow : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreNatural) afterRow)))))))))) rows))) def workReserveCoreDivision = (lambda unrestricted left : Bytes . (lambda unrestricted right : Bytes . (lambda unrestricted budget : (family NormalizationBudget) . (nat-eliminate (lambda unrestricted current : Nat . (family CoreWorkResult)) (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreNatural) budget) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family CoreWorkResult) . (coreWorkBind induction (lambda unrestricted ignored : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (workReserveCorePayloadProduct left right remaining)))))) (byte-to-nat (byte 9)))))) def workReserveCoreArithmetic = (lambda unrestricted operation : (family CoreNaturalOperation) . (lambda unrestricted left : Bytes . (lambda unrestricted right : Bytes . (lambda unrestricted budget : (family NormalizationBudget) . (eliminate CoreNaturalOperation (lambda unrestricted current : (family CoreNaturalOperation) . (family CoreWorkResult)) operation (branch CoreNaturalAdd . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreNatural) budget)) (branch CoreNaturalSubtract . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreNatural) budget)) (branch CoreNaturalMultiply . (coreWorkChoose (coreNaturalAnd (nat-less-than zero (bytes-length left)) (nat-less-than zero (bytes-length right))) (lambda unrestricted force : Nat . (coreWorkBind (workReserveCorePayloadProduct right left budget) (lambda unrestricted ignored : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (workReserveCorePayloadProduct right right remaining))))) (lambda unrestricted force : Nat . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreNatural) budget)))) (branch CoreNaturalDivide . (workReserveCoreDivision left right budget)) (branch CoreNaturalModulo . (workReserveCoreDivision left right budget))))))) def workReduceCoreArithmetic = (lambda unrestricted operation : (family CoreNaturalOperation) . (lambda unrestricted left : (family CoreTerm) . (lambda unrestricted right : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (app (lambda unrestricted neutral : (pi unrestricted force : Nat . (family CoreWorkResult)) . (workInspectCoreNatural left (lambda unrestricted leftDigits : Bytes . (workInspectCoreNatural right (lambda unrestricted rightDigits : Bytes . (coreWorkChargeBytes leftDigits budget (lambda unrestricted afterLeft : (family NormalizationBudget) . (coreWorkChargeBytes rightDigits afterLeft (lambda unrestricted afterRight : (family NormalizationBudget) . (coreWorkBind (workReserveCoreArithmetic operation leftDigits rightDigits afterRight) (lambda unrestricted ignored : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (reduceCoreArithmetic operation left right) remaining))))))))) neutral)) neutral)) (lambda unrestricted force : Nat . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreNaturalArithmetic operation left right) budget))))))) def workReduceCoreNaturalSuccessor = (lambda unrestricted predecessor : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (workInspectCoreNatural predecessor (lambda unrestricted digits : Bytes . (coreWorkChargeBytes digits budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (reduceCoreNaturalSuccessor predecessor) remaining)))) (lambda unrestricted force : Nat . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreNaturalSuccessor predecessor) budget))))) def workReduceCoreApplication = (lambda unrestricted function : (family CoreTerm) . (lambda unrestricted argument : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (eliminate CoreFunctionInspection (lambda unrestricted current : (family CoreFunctionInspection) . (family CoreWorkResult)) (inspectCoreFunction function) (branch CoreFunctionLambda body . (workSubstituteCoreTop argument body remaining)) (branch CoreFunctionPrimitive primitive . (workReduceDirectCorePrimitive primitive argument remaining)) (branch CoreFunctionAppliedPrimitive primitive first . (workReduceAppliedCorePrimitive primitive first argument remaining)) (branch CoreFunctionAppliedPrimitive2 primitive first second . (constructor CoreWorkResult CoreWorkCompleted (corePrimitiveApplication3 primitive first second argument) remaining)) (branch CoreFunctionAppliedPrimitive3 primitive first second third . (workReduceAppliedEliminator primitive first second third argument remaining)) (branch CoreFunctionOther . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreApplication function argument) remaining)))))))) def workNormalizeCoreOne = (lambda unrestricted full : Nat . (lambda unrestricted term : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted current : (family CoreTerm) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult))) term (branch CoreUniverse coreUniverseLevel . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreUniverse coreUniverseLevel) remaining))))) (branch CoreNatural . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreNatural) remaining))))) (branch CoreNaturalLiteral coreNaturalValue . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreNaturalLiteral coreNaturalValue) remaining))))) (branch CoreBound coreBoundIndex . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreBound coreBoundIndex) remaining))))) (branch CorePi corePiMultiplicity corePiDomain corePiCodomain ih_corePiDomain ih_corePiCodomain . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_corePiDomain remaining) (lambda unrestricted new_corePiDomain : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_corePiCodomain remaining) (lambda unrestricted new_corePiCodomain : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CorePi corePiMultiplicity new_corePiDomain new_corePiCodomain) remaining))))))))))) (branch CoreLambda coreLambdaMultiplicity coreLambdaDomain coreLambdaBody ih_coreLambdaDomain ih_coreLambdaBody . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreLambdaDomain remaining) (lambda unrestricted new_coreLambdaDomain : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreLambdaBody remaining) (lambda unrestricted new_coreLambdaBody : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreLambda coreLambdaMultiplicity new_coreLambdaDomain new_coreLambdaBody) remaining))))))))))) (branch CoreLet coreLetMultiplicity coreLetAnnotation coreLetValue coreLetBody ih_coreLetAnnotation ih_coreLetValue ih_coreLetBody . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreLetValue remaining) (lambda unrestricted new_coreLetValue : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreLetBody remaining) (lambda unrestricted new_coreLetBody : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (workSubstituteCoreTop new_coreLetValue new_coreLetBody remaining))))))))))) (branch CoreApplication coreApplicationFunction coreApplicationArgument ih_coreApplicationFunction ih_coreApplicationArgument . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreApplicationFunction remaining) (lambda unrestricted new_coreApplicationFunction : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreApplicationArgument remaining) (lambda unrestricted new_coreApplicationArgument : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkChoose full (lambda unrestricted force : Nat . (workReduceCoreApplication new_coreApplicationFunction new_coreApplicationArgument remaining)) (lambda unrestricted force : Nat . (workApplyCoreFunctionOnce new_coreApplicationFunction new_coreApplicationArgument remaining))))))))))))) (branch CoreNaturalArithmetic coreArithmeticOperation coreArithmeticLeft coreArithmeticRight ih_coreArithmeticLeft ih_coreArithmeticRight . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreArithmeticLeft remaining) (lambda unrestricted new_coreArithmeticLeft : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreArithmeticRight remaining) (lambda unrestricted new_coreArithmeticRight : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (workReduceCoreArithmetic coreArithmeticOperation new_coreArithmeticLeft new_coreArithmeticRight remaining))))))))))) (branch CoreNaturalSuccessor coreNaturalPredecessor ih_coreNaturalPredecessor . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreNaturalPredecessor remaining) (lambda unrestricted new_coreNaturalPredecessor : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (workReduceCoreNaturalSuccessor new_coreNaturalPredecessor remaining)))))))) (branch CoreByte . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreByte) remaining))))) (branch CoreByteLiteral coreByteValue . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreByteLiteral coreByteValue) remaining))))) (branch CoreBytes . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreBytes) remaining))))) (branch CoreBytesLiteral coreBytesValue . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreBytesLiteral coreBytesValue) remaining))))) (branch CorePrimitiveTerm corePrimitive . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CorePrimitiveTerm corePrimitive) remaining))))) (branch CoreTermSequenceEnd . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreTermSequenceEnd) remaining))))) (branch CoreTermSequenceNext coreTermSequenceHead coreTermSequenceTail ih_coreTermSequenceHead ih_coreTermSequenceTail . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreTermSequenceHead remaining) (lambda unrestricted new_coreTermSequenceHead : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreTermSequenceTail remaining) (lambda unrestricted new_coreTermSequenceTail : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreTermSequenceNext new_coreTermSequenceHead new_coreTermSequenceTail) remaining))))))))))) (branch CoreFamilyApplication coreFamilyName coreFamilyArguments ih_coreFamilyArguments . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreFamilyArguments remaining) (lambda unrestricted new_coreFamilyArguments : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreFamilyApplication coreFamilyName new_coreFamilyArguments) remaining)))))))) (branch CoreConstructorApplication coreConstructorFamilyName coreConstructorName coreConstructorArguments ih_coreConstructorArguments . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreConstructorArguments remaining) (lambda unrestricted new_coreConstructorArguments : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreConstructorApplication coreConstructorFamilyName coreConstructorName new_coreConstructorArguments) remaining)))))))) (branch CoreEliminatorBranch coreBranchConstructorName coreBranchBinderCount coreBranchBody ih_coreBranchBody . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreBranchBody remaining) (lambda unrestricted new_coreBranchBody : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreEliminatorBranch coreBranchConstructorName coreBranchBinderCount new_coreBranchBody) remaining)))))))) (branch CoreEliminator coreEliminatedFamilyName coreEliminatorMotive coreEliminatorScrutinee coreEliminatorBranches ih_coreEliminatorMotive ih_coreEliminatorScrutinee ih_coreEliminatorBranches . (lambda unrestricted budget : (family NormalizationBudget) . (coreWorkCharge coreWorkOne budget (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreEliminatorMotive remaining) (lambda unrestricted new_coreEliminatorMotive : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreEliminatorScrutinee remaining) (lambda unrestricted new_coreEliminatorScrutinee : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkBind (ih_coreEliminatorBranches remaining) (lambda unrestricted new_coreEliminatorBranches : (family CoreTerm) . (lambda unrestricted remaining : (family NormalizationBudget) . (coreWorkChoose full (lambda unrestricted force : Nat . (workReduceCoreGenericEliminator coreEliminatedFamilyName new_coreEliminatorMotive new_coreEliminatorScrutinee new_coreEliminatorBranches remaining)) (lambda unrestricted force : Nat . (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreEliminator coreEliminatedFamilyName new_coreEliminatorMotive new_coreEliminatorScrutinee new_coreEliminatorBranches) remaining))))))))))))))))))) def workReduceCoreRounds = (lambda unrestricted full : Nat . (lambda unrestricted rounds : Nat . (nat-eliminate (lambda unrestricted remaining : Nat . (pi unrestricted term : (family CoreTerm) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreReductionResult)))) (lambda unrestricted term : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (constructor CoreReductionResult CoreReductionExhausted term zero))) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (pi unrestricted term : (family CoreTerm) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreReductionResult))) . (lambda unrestricted term : (family CoreTerm) . (lambda unrestricted budget : (family NormalizationBudget) . (eliminate CoreWorkResult (lambda unrestricted current : (family CoreWorkResult) . (family CoreReductionResult)) (workNormalizeCoreOne full term budget) (branch CoreWorkCompleted reduced remaining . (app (nat-eliminate (lambda unrestricted equal : Nat . (pi unrestricted force : Nat . (family CoreReductionResult))) (lambda unrestricted force : Nat . (countCoreReductionRound (induction reduced remaining))) (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (pi unrestricted force : Nat . (family CoreReductionResult)) . (lambda unrestricted force : Nat . (constructor CoreReductionResult CoreReductionCompleted reduced (succ zero))))) (coreTermEqual term reduced)) zero)) (branch CoreWorkExhausted remaining . (constructor CoreReductionResult CoreReductionExhausted term (succ zero)))))))) rounds))) def workNormalizeCoreWithLimit = (lambda unrestricted full : Nat . (lambda unrestricted rounds : Nat . (lambda unrestricted limit : (family ModelWord32) . (lambda unrestricted term : (family CoreTerm) . (workReduceCoreRounds full rounds term (Compiler.NormalizationBudget/normalizationBudget limit)))))) def normalizeCoreTypeWithWorkBudget = (workNormalizeCoreWithLimit zero) def normalizeCoreTypeWithBudget = (lambda unrestricted rounds : Nat . (normalizeCoreTypeWithWorkBudget rounds coreNormalizationDefaultWork)) -- Continue only with a completed normal form. Resource exhaustion is distinct -- from an inferred type mismatch and never supplies a residual to admission. def withCoreNormalization = (lambda unrestricted budget : Nat . (lambda unrestricted term : (family CoreTerm) . (lambda unrestricted continuation : (pi unrestricted normal : (family CoreTerm) . (family CoreInferenceResult)) . (eliminate CoreReductionResult (lambda unrestricted result : (family CoreReductionResult) . (family CoreInferenceResult)) (normalizeCoreTypeWithBudget budget term) (branch CoreReductionCompleted normal rounds . (continuation normal)) (branch CoreReductionExhausted residual rounds . (constructor CoreInferenceResult CoreInferenceFailed coreNormalizationResourceFailureCode)))))) def inferNormalizedCoreTypeWithBudget = (lambda unrestricted budget : Nat . (lambda unrestricted term : (family CoreTerm) . (withCoreNormalization budget term (lambda unrestricted normal : (family CoreTerm) . (constructor CoreInferenceResult CoreInferred normal))))) def shiftTypeLookup : (pi unrestricted result : (family TypeLookupResult) . (family TypeLookupResult)) = (lambda unrestricted result : (family TypeLookupResult) . (eliminate TypeLookupResult (lambda unrestricted value : (family TypeLookupResult) . (family TypeLookupResult)) result (branch TypeFound variableType . (constructor TypeLookupResult TypeFound (shiftCoreBy (succ zero) variableType))) (branch TypeNotFound index . (constructor TypeLookupResult TypeNotFound (succ index))))) def lookupTypeWithShift : (pi unrestricted context : (family TypeContext) . (pi unrestricted index : Nat . (pi unrestricted amount : Nat . (pi unrestricted originalIndex : Nat . (family TypeLookupResult))))) = (lambda unrestricted context : (family TypeContext) . (eliminate TypeContext (lambda unrestricted value : (family TypeContext) . (pi unrestricted index : Nat . (pi unrestricted amount : Nat . (pi unrestricted originalIndex : Nat . (family TypeLookupResult))))) context (branch EmptyTypeContext . (lambda unrestricted index : Nat . (lambda unrestricted amount : Nat . (lambda unrestricted originalIndex : Nat . (constructor TypeLookupResult TypeNotFound originalIndex))))) (branch TypeContextBinding bindingType outerContext ih_outerContext . (lambda unrestricted index : Nat . (lambda unrestricted amount : Nat . (lambda unrestricted originalIndex : Nat . (app (nat-eliminate (lambda unrestricted value : Nat . (pi unrestricted ignored : Nat . (family TypeLookupResult))) (lambda unrestricted ignored : Nat . (constructor TypeLookupResult TypeFound (shiftCoreBy amount bindingType))) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (pi unrestricted ignored : Nat . (family TypeLookupResult)) . (lambda unrestricted ignored : Nat . (ih_outerContext predecessor (succ amount) originalIndex)))) index) zero))))))) def lookupType : (pi unrestricted context : (family TypeContext) . (pi unrestricted index : Nat . (family TypeLookupResult))) = (lambda unrestricted context : (family TypeContext) . (lambda unrestricted index : Nat . (lookupTypeWithShift context index (succ zero) index))) def inspectUniverse : (pi unrestricted term : (family CoreTerm) . (family UniverseInspection)) = (lambda unrestricted term : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted value : (family CoreTerm) . (family UniverseInspection)) term (branch CoreUniverse level . (constructor UniverseInspection IsUniverse level)) (branch CoreNatural . (constructor UniverseInspection NotUniverse)) (branch CoreNaturalLiteral value . (constructor UniverseInspection NotUniverse)) (branch CoreBound index . (constructor UniverseInspection NotUniverse)) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . (constructor UniverseInspection NotUniverse)) (branch CoreLambda multiplicity domain body ih_domain ih_body . (constructor UniverseInspection NotUniverse)) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . (constructor UniverseInspection NotUniverse)) (branch CoreApplication function argument ih_function ih_argument . (constructor UniverseInspection NotUniverse)) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . (constructor UniverseInspection NotUniverse)) (branch CoreNaturalSuccessor predecessor ih_predecessor . (constructor UniverseInspection NotUniverse)) (branch CoreByte . (constructor UniverseInspection NotUniverse)) (branch CoreByteLiteral value . (constructor UniverseInspection NotUniverse)) (branch CoreBytes . (constructor UniverseInspection NotUniverse)) (branch CoreBytesLiteral value . (constructor UniverseInspection NotUniverse)) (branch CorePrimitiveTerm primitive . (constructor UniverseInspection NotUniverse)) (branch CoreTermSequenceEnd . (constructor UniverseInspection NotUniverse)) (branch CoreTermSequenceNext head tail ih_head ih_tail . (constructor UniverseInspection NotUniverse)) (branch CoreFamilyApplication familyName arguments ih_arguments . (constructor UniverseInspection NotUniverse)) (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . (constructor UniverseInspection NotUniverse)) (branch CoreEliminatorBranch constructorName binderCount body ih_body . (constructor UniverseInspection NotUniverse)) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . (constructor UniverseInspection NotUniverse)))) def inspectPi : (pi unrestricted term : (family CoreTerm) . (family PiInspection)) = (lambda unrestricted term : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted value : (family CoreTerm) . (family PiInspection)) term (branch CoreUniverse level . (constructor PiInspection NotPi)) (branch CoreNatural . (constructor PiInspection NotPi)) (branch CoreNaturalLiteral value . (constructor PiInspection NotPi)) (branch CoreBound index . (constructor PiInspection NotPi)) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . (constructor PiInspection IsPi multiplicity domain codomain)) (branch CoreLambda multiplicity domain body ih_domain ih_body . (constructor PiInspection NotPi)) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . (constructor PiInspection NotPi)) (branch CoreApplication function argument ih_function ih_argument . (constructor PiInspection NotPi)) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . (constructor PiInspection NotPi)) (branch CoreNaturalSuccessor predecessor ih_predecessor . (constructor PiInspection NotPi)) (branch CoreByte . (constructor PiInspection NotPi)) (branch CoreByteLiteral value . (constructor PiInspection NotPi)) (branch CoreBytes . (constructor PiInspection NotPi)) (branch CoreBytesLiteral value . (constructor PiInspection NotPi)) (branch CorePrimitiveTerm primitive . (constructor PiInspection NotPi)) (branch CoreTermSequenceEnd . (constructor PiInspection NotPi)) (branch CoreTermSequenceNext head tail ih_head ih_tail . (constructor PiInspection NotPi)) (branch CoreFamilyApplication familyName arguments ih_arguments . (constructor PiInspection NotPi)) (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . (constructor PiInspection NotPi)) (branch CoreEliminatorBranch constructorName binderCount body ih_body . (constructor PiInspection NotPi)) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . (constructor PiInspection NotPi)))) def coreFamilyInferenceFailureCode = (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ zero)))))))))))))) def inferNaturalSuccessorType : (pi unrestricted predecessorResult : (family CoreInferenceResult) . (family CoreInferenceResult)) = (lambda unrestricted predecessorResult : (family CoreInferenceResult) . (eliminate CoreInferenceResult (lambda unrestricted result : (family CoreInferenceResult) . (family CoreInferenceResult)) predecessorResult (branch CoreInferred predecessorType . (nat-eliminate (lambda unrestricted matched : Nat . (family CoreInferenceResult)) (constructor CoreInferenceResult CoreInferenceFailed (succ (succ (succ (succ (succ (succ (succ zero)))))))) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family CoreInferenceResult) . (constructor CoreInferenceResult CoreInferred (constructor CoreTerm CoreNatural)))) (coreTermEqual predecessorType (constructor CoreTerm CoreNatural)))) (branch CoreInferenceFailed code . (constructor CoreInferenceResult CoreInferenceFailed code)))) def inferUniversePair : (pi unrestricted domainInspection : (family UniverseInspection) . (pi unrestricted codomainInspection : (family UniverseInspection) . (family CoreInferenceResult))) = (lambda unrestricted domainInspection : (family UniverseInspection) . (lambda unrestricted codomainInspection : (family UniverseInspection) . (eliminate UniverseInspection (lambda unrestricted inspection : (family UniverseInspection) . (family CoreInferenceResult)) domainInspection (branch IsUniverse domainLevel . (eliminate UniverseInspection (lambda unrestricted inspection : (family UniverseInspection) . (family CoreInferenceResult)) codomainInspection (branch IsUniverse codomainLevel . (constructor CoreInferenceResult CoreInferred (constructor CoreTerm CoreUniverse (naturalMaximum domainLevel codomainLevel)))) (branch NotUniverse . (constructor CoreInferenceResult CoreInferenceFailed (succ (succ (succ zero))))))) (branch NotUniverse . (constructor CoreInferenceResult CoreInferenceFailed (succ (succ zero))))))) def inferPiType : (pi unrestricted multiplicity : (family CoreMultiplicity) . (pi unrestricted domainResult : (family CoreInferenceResult) . (pi unrestricted codomainResult : (family CoreInferenceResult) . (family CoreInferenceResult)))) = (lambda unrestricted multiplicity : (family CoreMultiplicity) . (lambda unrestricted domainResult : (family CoreInferenceResult) . (lambda unrestricted codomainResult : (family CoreInferenceResult) . (eliminate CoreInferenceResult (lambda unrestricted result : (family CoreInferenceResult) . (family CoreInferenceResult)) domainResult (branch CoreInferred domainType . (eliminate CoreInferenceResult (lambda unrestricted result : (family CoreInferenceResult) . (family CoreInferenceResult)) codomainResult (branch CoreInferred codomainType . (inferUniversePair (inspectUniverse domainType) (inspectUniverse codomainType))) (branch CoreInferenceFailed code . (constructor CoreInferenceResult CoreInferenceFailed code)))) (branch CoreInferenceFailed code . (constructor CoreInferenceResult CoreInferenceFailed code)))))) def inferLambdaBody : (pi unrestricted multiplicity : (family CoreMultiplicity) . (pi unrestricted domain : (family CoreTerm) . (pi unrestricted bodyResult : (family CoreInferenceResult) . (family CoreInferenceResult)))) = (lambda unrestricted multiplicity : (family CoreMultiplicity) . (lambda unrestricted domain : (family CoreTerm) . (lambda unrestricted bodyResult : (family CoreInferenceResult) . (eliminate CoreInferenceResult (lambda unrestricted result : (family CoreInferenceResult) . (family CoreInferenceResult)) bodyResult (branch CoreInferred bodyType . (constructor CoreInferenceResult CoreInferred (constructor CoreTerm CorePi multiplicity domain bodyType))) (branch CoreInferenceFailed code . (constructor CoreInferenceResult CoreInferenceFailed code)))))) def inferLambdaFromUniverse : (pi unrestricted multiplicity : (family CoreMultiplicity) . (pi unrestricted domain : (family CoreTerm) . (pi unrestricted inspection : (family UniverseInspection) . (pi unrestricted bodyResult : (family CoreInferenceResult) . (family CoreInferenceResult))))) = (lambda unrestricted multiplicity : (family CoreMultiplicity) . (lambda unrestricted domain : (family CoreTerm) . (lambda unrestricted inspection : (family UniverseInspection) . (lambda unrestricted bodyResult : (family CoreInferenceResult) . (eliminate UniverseInspection (lambda unrestricted value : (family UniverseInspection) . (family CoreInferenceResult)) inspection (branch IsUniverse level . (inferLambdaBody multiplicity domain bodyResult)) (branch NotUniverse . (constructor CoreInferenceResult CoreInferenceFailed (succ (succ (succ (succ zero))))))))))) def inferLambdaType : (pi unrestricted multiplicity : (family CoreMultiplicity) . (pi unrestricted domain : (family CoreTerm) . (pi unrestricted domainResult : (family CoreInferenceResult) . (pi unrestricted bodyResult : (family CoreInferenceResult) . (family CoreInferenceResult))))) = (lambda unrestricted multiplicity : (family CoreMultiplicity) . (lambda unrestricted domain : (family CoreTerm) . (lambda unrestricted domainResult : (family CoreInferenceResult) . (lambda unrestricted bodyResult : (family CoreInferenceResult) . (eliminate CoreInferenceResult (lambda unrestricted result : (family CoreInferenceResult) . (family CoreInferenceResult)) domainResult (branch CoreInferred domainType . (inferLambdaFromUniverse multiplicity domain (inspectUniverse domainType) bodyResult)) (branch CoreInferenceFailed code . (constructor CoreInferenceResult CoreInferenceFailed code))))))) def inferApplicationNormalizedDomain = (lambda unrestricted budget : Nat . (lambda unrestricted argument : (family CoreTerm) . (lambda unrestricted codomain : (family CoreTerm) . (lambda unrestricted argumentType : (family CoreTerm) . (lambda unrestricted domain : (family CoreTerm) . (app (nat-eliminate (lambda unrestricted equal : Nat . (pi unrestricted trigger : Nat . (family CoreInferenceResult))) (lambda unrestricted trigger : Nat . (constructor CoreInferenceResult CoreInferenceFailed (byte-to-nat (byte 6)))) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (pi unrestricted trigger : Nat . (family CoreInferenceResult)) . (lambda unrestricted trigger : Nat . (inferNormalizedCoreTypeWithBudget budget (substituteCoreTop argument codomain))))) (coreTermEqual argumentType domain)) zero)))))) -- The budget bounds each requested normal form, not aggregate inference work. def inferApplicationArgumentWithBudget = (lambda unrestricted budget : Nat . (lambda unrestricted argument : (family CoreTerm) . (lambda unrestricted domain : (family CoreTerm) . (lambda unrestricted codomain : (family CoreTerm) . (lambda unrestricted argumentResult : (family CoreInferenceResult) . (eliminate CoreInferenceResult (lambda unrestricted result : (family CoreInferenceResult) . (family CoreInferenceResult)) argumentResult (branch CoreInferred argumentType . (withCoreNormalization budget argumentType (lambda unrestricted normalArgumentType : (family CoreTerm) . (withCoreNormalization budget domain (inferApplicationNormalizedDomain budget argument codomain normalArgumentType))))) (branch CoreInferenceFailed code . (constructor CoreInferenceResult CoreInferenceFailed code)))))))) def inferApplicationArgument = (inferApplicationArgumentWithBudget coreNormalizationDefaultRounds) def inferApplicationPi : (pi unrestricted argument : (family CoreTerm) . (pi unrestricted inspection : (family PiInspection) . (pi unrestricted argumentResult : (family CoreInferenceResult) . (family CoreInferenceResult)))) = (lambda unrestricted argument : (family CoreTerm) . (lambda unrestricted inspection : (family PiInspection) . (lambda unrestricted argumentResult : (family CoreInferenceResult) . (eliminate PiInspection (lambda unrestricted value : (family PiInspection) . (family CoreInferenceResult)) inspection (branch IsPi multiplicity domain codomain . (inferApplicationArgument argument domain codomain argumentResult)) (branch NotPi . (constructor CoreInferenceResult CoreInferenceFailed (succ (succ (succ (succ (succ zero))))))))))) def inferApplicationType : (pi unrestricted argument : (family CoreTerm) . (pi unrestricted functionResult : (family CoreInferenceResult) . (pi unrestricted argumentResult : (family CoreInferenceResult) . (family CoreInferenceResult)))) = (lambda unrestricted argument : (family CoreTerm) . (lambda unrestricted functionResult : (family CoreInferenceResult) . (lambda unrestricted argumentResult : (family CoreInferenceResult) . (eliminate CoreInferenceResult (lambda unrestricted result : (family CoreInferenceResult) . (family CoreInferenceResult)) functionResult (branch CoreInferred functionType . (withCoreNormalization coreNormalizationDefaultRounds functionType (lambda unrestricted normalFunctionType : (family CoreTerm) . (inferApplicationPi argument (inspectPi normalFunctionType) argumentResult)))) (branch CoreInferenceFailed code . (constructor CoreInferenceResult CoreInferenceFailed code)))))) def extendCoreInferenceFunctionInspection = (lambda unrestricted inspection : (family CoreFunctionInspection) . (lambda unrestricted argument : (family CoreTerm) . (eliminate CoreFunctionInspection (lambda unrestricted value : (family CoreFunctionInspection) . (family CoreFunctionInspection)) inspection (branch CoreFunctionLambda body . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CoreFunctionPrimitive primitive . (constructor CoreFunctionInspection CoreFunctionAppliedPrimitive primitive argument)) (branch CoreFunctionAppliedPrimitive primitive first . (constructor CoreFunctionInspection CoreFunctionAppliedPrimitive2 primitive first argument)) (branch CoreFunctionAppliedPrimitive2 primitive first second . (constructor CoreFunctionInspection CoreFunctionAppliedPrimitive3 primitive first second argument)) (branch CoreFunctionAppliedPrimitive3 primitive first second third . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CoreFunctionOther . (constructor CoreFunctionInspection CoreFunctionOther))))) def inspectCoreInferenceFunction = (lambda unrestricted term : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted value : (family CoreTerm) . (family CoreFunctionInspection)) term (branch CoreUniverse level . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CoreNatural . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CoreNaturalLiteral value . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CoreBound index . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CoreLambda multiplicity domain body ih_domain ih_body . (constructor CoreFunctionInspection CoreFunctionLambda body)) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CoreApplication function argument ih_function ih_argument . (extendCoreInferenceFunctionInspection ih_function argument)) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CoreNaturalSuccessor predecessor ih_predecessor . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CoreByte . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CoreByteLiteral value . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CoreBytes . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CoreBytesLiteral value . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CorePrimitiveTerm primitive . (constructor CoreFunctionInspection CoreFunctionPrimitive primitive)) (branch CoreTermSequenceEnd . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CoreTermSequenceNext head tail ih_head ih_tail . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CoreFamilyApplication familyName arguments ih_arguments . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CoreEliminatorBranch constructorName binderCount body ih_body . (constructor CoreFunctionInspection CoreFunctionOther)) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . (constructor CoreFunctionInspection CoreFunctionOther)))) def corePrimitiveMatches = (lambda unrestricted left : (family CorePrimitive) . (lambda unrestricted right : (family CorePrimitive) . (naturalEqual (corePrimitiveCode left) (corePrimitiveCode right)))) def coreEffectRowValid = (lambda unrestricted row : (family CoreTerm) . (eliminate CoreFunctionInspection (lambda unrestricted inspection : (family CoreFunctionInspection) . Nat) (inspectCoreInferenceFunction row) (branch CoreFunctionLambda body . zero) (branch CoreFunctionPrimitive primitive . zero) (branch CoreFunctionAppliedPrimitive primitive effect . (nat-eliminate (lambda unrestricted matched : Nat . Nat) zero (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . (eliminate CoreFunctionInspection (lambda unrestricted effectInspection : (family CoreFunctionInspection) . Nat) (inspectCoreInferenceFunction effect) (branch CoreFunctionLambda body . zero) (branch CoreFunctionPrimitive effectPrimitive . (corePrimitiveMatches effectPrimitive (constructor CorePrimitive CoreFileEffect))) (branch CoreFunctionAppliedPrimitive ignored first . zero) (branch CoreFunctionAppliedPrimitive2 ignored first second . zero) (branch CoreFunctionAppliedPrimitive3 ignored first second third . zero) (branch CoreFunctionOther . zero)))) (corePrimitiveMatches primitive (constructor CorePrimitive CoreEffects)))) (branch CoreFunctionAppliedPrimitive2 primitive first second . zero) (branch CoreFunctionAppliedPrimitive3 primitive first second third . zero) (branch CoreFunctionOther . zero))) def inferCoreEffectHead = (lambda unrestricted effects : (family CoreTerm) . (lambda unrestricted argumentResult : (family CoreInferenceResult) . (eliminate CoreInferenceResult (lambda unrestricted result : (family CoreInferenceResult) . (family CoreInferenceResult)) argumentResult (branch CoreInferred effectType . (eliminate UniverseInspection (lambda unrestricted inspection : (family UniverseInspection) . (family CoreInferenceResult)) (inspectUniverse effectType) (branch IsUniverse level . (nat-eliminate (lambda unrestricted valid : Nat . (family CoreInferenceResult)) (constructor CoreInferenceResult CoreInferenceFailed (succ (succ (succ (succ (succ (succ zero))))))) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family CoreInferenceResult) . (constructor CoreInferenceResult CoreInferred (constructor CoreTerm CoreUniverse zero)))) (coreEffectRowValid effects))) (branch NotUniverse . (constructor CoreInferenceResult CoreInferenceFailed (succ (succ (succ (succ (succ (succ zero)))))))))) (branch CoreInferenceFailed code . (constructor CoreInferenceResult CoreInferenceFailed code))))) def inferCoreReturnApplication = (lambda unrestricted effects : (family CoreTerm) . (lambda unrestricted functionResult : (family CoreInferenceResult) . (lambda unrestricted valueResult : (family CoreInferenceResult) . (eliminate CoreInferenceResult (lambda unrestricted result : (family CoreInferenceResult) . (family CoreInferenceResult)) functionResult (branch CoreInferred marker . (eliminate CoreInferenceResult (lambda unrestricted result : (family CoreInferenceResult) . (family CoreInferenceResult)) valueResult (branch CoreInferred valueType . (constructor CoreInferenceResult CoreInferred (coreComputationType effects valueType))) (branch CoreInferenceFailed code . (constructor CoreInferenceResult CoreInferenceFailed code)))) (branch CoreInferenceFailed code . (constructor CoreInferenceResult CoreInferenceFailed code)))))) def inferCoreBindResultType = (lambda unrestricted functionResult : (family CoreInferenceResult) . (lambda unrestricted resultTypeResult : (family CoreInferenceResult) . (eliminate CoreInferenceResult (lambda unrestricted result : (family CoreInferenceResult) . (family CoreInferenceResult)) functionResult (branch CoreInferred marker . (eliminate CoreInferenceResult (lambda unrestricted result : (family CoreInferenceResult) . (family CoreInferenceResult)) resultTypeResult (branch CoreInferred resultUniverse . (eliminate UniverseInspection (lambda unrestricted inspection : (family UniverseInspection) . (family CoreInferenceResult)) (inspectUniverse resultUniverse) (branch IsUniverse level . (constructor CoreInferenceResult CoreInferred (constructor CoreTerm CoreUniverse zero))) (branch NotUniverse . (constructor CoreInferenceResult CoreInferenceFailed (succ (succ (succ (succ (succ (succ zero)))))))))) (branch CoreInferenceFailed code . (constructor CoreInferenceResult CoreInferenceFailed code)))) (branch CoreInferenceFailed code . (constructor CoreInferenceResult CoreInferenceFailed code))))) def coreBindContinuationType = (lambda unrestricted effects : (family CoreTerm) . (lambda unrestricted resultType : (family CoreTerm) . (lambda unrestricted inputType : (family CoreTerm) . (constructor CoreTerm CorePi coreUnrestricted (constructor CoreTerm CorePi coreUnrestricted inputType (coreComputationType (shiftCoreBy (succ zero) effects) (shiftCoreBy (succ zero) resultType))) (coreComputationType (shiftCoreBy (succ zero) effects) (shiftCoreBy (succ zero) resultType)))))) def coreEffectInferenceFailure = (constructor CoreInferenceResult CoreInferenceFailed (succ (succ (succ (succ (succ (succ zero))))))) def coreInferredBindContinuation = (lambda unrestricted effects : (family CoreTerm) . (lambda unrestricted resultType : (family CoreTerm) . (lambda unrestricted inputType : (family CoreTerm) . (constructor CoreInferenceResult CoreInferred (coreBindContinuationType effects resultType inputType))))) def inferCoreBindInspection = (lambda unrestricted effects : (family CoreTerm) . (lambda unrestricted resultType : (family CoreTerm) . (lambda unrestricted inspection : (family CoreFunctionInspection) . (eliminate CoreFunctionInspection (lambda unrestricted value : (family CoreFunctionInspection) . (family CoreInferenceResult)) inspection (branch CoreFunctionLambda body . coreEffectInferenceFailure) (branch CoreFunctionPrimitive primitive . coreEffectInferenceFailure) (branch CoreFunctionAppliedPrimitive primitive first . coreEffectInferenceFailure) (branch CoreFunctionAppliedPrimitive2 primitive inputEffects inputType . (nat-eliminate (lambda unrestricted valid : Nat . (family CoreInferenceResult)) coreEffectInferenceFailure (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family CoreInferenceResult) . (coreInferredBindContinuation effects resultType inputType))) (coreNaturalAnd (corePrimitiveMatches primitive (constructor CorePrimitive CoreComputation)) (coreNaturalAnd (coreEffectRowValid effects) (coreEffectRowValid inputEffects))))) (branch CoreFunctionAppliedPrimitive3 primitive first second third . coreEffectInferenceFailure) (branch CoreFunctionOther . coreEffectInferenceFailure))))) def inferCoreBindInputResult = (lambda unrestricted effects : (family CoreTerm) . (lambda unrestricted resultType : (family CoreTerm) . (lambda unrestricted inputResult : (family CoreInferenceResult) . (eliminate CoreInferenceResult (lambda unrestricted result : (family CoreInferenceResult) . (family CoreInferenceResult)) inputResult (branch CoreInferred inputComputationType . (inferCoreBindInspection effects resultType (inspectCoreInferenceFunction inputComputationType))) (branch CoreInferenceFailed code . (constructor CoreInferenceResult CoreInferenceFailed code)))))) def inferCoreBindInput = (lambda unrestricted effects : (family CoreTerm) . (lambda unrestricted resultType : (family CoreTerm) . (lambda unrestricted functionResult : (family CoreInferenceResult) . (lambda unrestricted inputResult : (family CoreInferenceResult) . (eliminate CoreInferenceResult (lambda unrestricted result : (family CoreInferenceResult) . (family CoreInferenceResult)) functionResult (branch CoreInferred marker . (inferCoreBindInputResult effects resultType inputResult)) (branch CoreInferenceFailed code . (constructor CoreInferenceResult CoreInferenceFailed code))))))) def inferCoreApplicationDefault = (lambda unrestricted argument : (family CoreTerm) . (lambda unrestricted functionResult : (family CoreInferenceResult) . (lambda unrestricted argumentResult : (family CoreInferenceResult) . (inferApplicationType argument functionResult argumentResult)))) def inferCorePrimitiveApplication = (lambda unrestricted argument : (family CoreTerm) . (lambda unrestricted functionResult : (family CoreInferenceResult) . (lambda unrestricted argumentResult : (family CoreInferenceResult) . (lambda unrestricted primitive : (family CorePrimitive) . (nat-eliminate (lambda unrestricted special : Nat . (family CoreInferenceResult)) (inferCoreApplicationDefault argument functionResult argumentResult) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family CoreInferenceResult) . (inferCoreEffectHead argument argumentResult))) (nat-eliminate (lambda unrestricted returnMatch : Nat . Nat) (corePrimitiveMatches primitive (constructor CorePrimitive CoreBind)) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . (succ zero))) (corePrimitiveMatches primitive (constructor CorePrimitive CoreReturn)))))))) def inferCoreAppliedPrimitiveApplication = (lambda unrestricted argument : (family CoreTerm) . (lambda unrestricted functionResult : (family CoreInferenceResult) . (lambda unrestricted argumentResult : (family CoreInferenceResult) . (lambda unrestricted primitive : (family CorePrimitive) . (lambda unrestricted effects : (family CoreTerm) . (nat-eliminate (lambda unrestricted isReturn : Nat . (family CoreInferenceResult)) (nat-eliminate (lambda unrestricted isBind : Nat . (family CoreInferenceResult)) (inferCoreApplicationDefault argument functionResult argumentResult) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family CoreInferenceResult) . (inferCoreBindResultType functionResult argumentResult))) (corePrimitiveMatches primitive (constructor CorePrimitive CoreBind))) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family CoreInferenceResult) . (inferCoreReturnApplication effects functionResult argumentResult))) (corePrimitiveMatches primitive (constructor CorePrimitive CoreReturn)))))))) def inferCoreAppliedPrimitive2Application = (lambda unrestricted argument : (family CoreTerm) . (lambda unrestricted functionResult : (family CoreInferenceResult) . (lambda unrestricted argumentResult : (family CoreInferenceResult) . (lambda unrestricted primitive : (family CorePrimitive) . (lambda unrestricted effects : (family CoreTerm) . (lambda unrestricted resultType : (family CoreTerm) . (nat-eliminate (lambda unrestricted isBind : Nat . (family CoreInferenceResult)) (inferCoreApplicationDefault argument functionResult argumentResult) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family CoreInferenceResult) . (inferCoreBindInput effects resultType functionResult argumentResult))) (corePrimitiveMatches primitive (constructor CorePrimitive CoreBind))))))))) def inferCoreApplicationInspection = (lambda unrestricted argument : (family CoreTerm) . (lambda unrestricted functionResult : (family CoreInferenceResult) . (lambda unrestricted argumentResult : (family CoreInferenceResult) . (lambda unrestricted inspection : (family CoreFunctionInspection) . (eliminate CoreFunctionInspection (lambda unrestricted inspection : (family CoreFunctionInspection) . (family CoreInferenceResult)) inspection (branch CoreFunctionLambda body . (inferCoreApplicationDefault argument functionResult argumentResult)) (branch CoreFunctionPrimitive primitive . (inferCorePrimitiveApplication argument functionResult argumentResult primitive)) (branch CoreFunctionAppliedPrimitive primitive effects . (inferCoreAppliedPrimitiveApplication argument functionResult argumentResult primitive effects)) (branch CoreFunctionAppliedPrimitive2 primitive effects resultType . (inferCoreAppliedPrimitive2Application argument functionResult argumentResult primitive effects resultType)) (branch CoreFunctionAppliedPrimitive3 primitive first second third . (inferCoreApplicationDefault argument functionResult argumentResult)) (branch CoreFunctionOther . (inferCoreApplicationDefault argument functionResult argumentResult))))))) def inferCoreApplicationWithEffects = (lambda unrestricted function : (family CoreTerm) . (lambda unrestricted argument : (family CoreTerm) . (lambda unrestricted functionResult : (family CoreInferenceResult) . (lambda unrestricted argumentResult : (family CoreInferenceResult) . (inferCoreApplicationInspection argument functionResult argumentResult (inspectCoreInferenceFunction function)))))) def inferCoreEliminatorApplicationResult = (lambda unrestricted motive : (family CoreTerm) . (lambda unrestricted scrutinee : (family CoreTerm) . (lambda unrestricted applicationResult : (family CoreInferenceResult) . (eliminate CoreInferenceResult (lambda unrestricted result : (family CoreInferenceResult) . (family CoreInferenceResult)) applicationResult (branch CoreInferred motiveApplicationUniverse . (inferNormalizedCoreTypeWithBudget coreNormalizationDefaultRounds (constructor CoreTerm CoreApplication motive scrutinee))) (branch CoreInferenceFailed code . (constructor CoreInferenceResult CoreInferenceFailed code)))))) def inferCoreEliminatorResult = (lambda unrestricted motive : (family CoreTerm) . (lambda unrestricted scrutinee : (family CoreTerm) . (lambda unrestricted motiveResult : (family CoreInferenceResult) . (lambda unrestricted scrutineeResult : (family CoreInferenceResult) . (inferCoreEliminatorApplicationResult motive scrutinee (inferCoreApplicationWithEffects motive scrutinee motiveResult scrutineeResult)))))) def coreNaturalMagnitudeFailureCode = (succ coreFamilyInferenceFailureCode) def inferCoreNaturalMagnitude = (lambda unrestricted digits : Bytes . (eliminate NaturalMagnitudeResult (lambda unrestricted result : (family NaturalMagnitudeResult) . (family CoreInferenceResult)) (Compiler.NaturalMagnitude/magnitudeDecodeCanonical digits) (branch NaturalMagnitudeAccepted valid . (constructor CoreInferenceResult CoreInferred (constructor CoreTerm CoreNatural))) (branch NaturalMagnitudeRejected failure . (constructor CoreInferenceResult CoreInferenceFailed coreNaturalMagnitudeFailureCode)))) def inferCoreArithmeticInspection = (lambda unrestricted inspection : (family CoreArithmeticInspection) . (eliminate CoreArithmeticInspection (lambda unrestricted current : (family CoreArithmeticInspection) . (family CoreInferenceResult)) inspection (branch CoreArithmeticValue digits . (inferCoreNaturalMagnitude digits)) (branch CoreArithmeticNeutral . (constructor CoreInferenceResult CoreInferred (constructor CoreTerm CoreNatural))) (branch CoreArithmeticRejected failure . (constructor CoreInferenceResult CoreInferenceFailed coreNaturalMagnitudeFailureCode)))) def inferCoreNormalizedArithmetic = (lambda unrestricted budget : Nat . (lambda unrestricted operation : (family CoreNaturalOperation) . (lambda unrestricted left : (family CoreTerm) . (lambda unrestricted right : (family CoreTerm) . (withCoreNormalization budget left (lambda unrestricted normalLeft : (family CoreTerm) . (withCoreNormalization budget right (lambda unrestricted normalRight : (family CoreTerm) . (inferCoreArithmeticInspection (inspectCoreArithmetic operation normalLeft normalRight)))))))))) -- Operand witnesses establish Nat typing. The proof predicate consumes the -- same checked normal forms directly, without constructing an inference result. def coreArithmeticAdmissionRight = (lambda unrestricted operation : (family CoreNaturalOperation) . (lambda unrestricted left : (family CoreTerm) . (lambda unrestricted rightResult : (family CoreReductionResult) . (eliminate CoreReductionResult (lambda unrestricted result : (family CoreReductionResult) . Nat) rightResult (branch CoreReductionCompleted right rounds . (eliminate CoreArithmeticInspection (lambda unrestricted inspection : (family CoreArithmeticInspection) . Nat) (inspectCoreArithmetic operation left right) (branch CoreArithmeticValue digits . (succ zero)) (branch CoreArithmeticNeutral . (succ zero)) (branch CoreArithmeticRejected failure . zero))) (branch CoreReductionExhausted residual rounds . zero))))) def coreArithmeticAdmissible = (lambda unrestricted operation : (family CoreNaturalOperation) . (lambda unrestricted left : (family CoreTerm) . (lambda unrestricted right : (family CoreTerm) . (eliminate CoreReductionResult (lambda unrestricted result : (family CoreReductionResult) . Nat) (normalizeCoreTypeWithBudget coreNormalizationDefaultRounds left) (branch CoreReductionCompleted normalLeft rounds . (coreArithmeticAdmissionRight operation normalLeft (normalizeCoreTypeWithBudget coreNormalizationDefaultRounds right))) (branch CoreReductionExhausted residual rounds . zero))))) def inferCoreArithmeticOperands = (lambda unrestricted operation : (family CoreNaturalOperation) . (lambda unrestricted left : (family CoreTerm) . (lambda unrestricted right : (family CoreTerm) . (lambda unrestricted leftResult : (family CoreInferenceResult) . (lambda unrestricted rightResult : (family CoreInferenceResult) . (eliminate CoreInferenceResult (lambda unrestricted current : (family CoreInferenceResult) . (family CoreInferenceResult)) (inferNaturalSuccessorType leftResult) (branch CoreInferred leftType . (eliminate CoreInferenceResult (lambda unrestricted current : (family CoreInferenceResult) . (family CoreInferenceResult)) (inferNaturalSuccessorType rightResult) (branch CoreInferred rightType . (inferCoreNormalizedArithmetic coreNormalizationDefaultRounds operation left right)) (branch CoreInferenceFailed code . (constructor CoreInferenceResult CoreInferenceFailed code)))) (branch CoreInferenceFailed code . (constructor CoreInferenceResult CoreInferenceFailed code)))))))) def finishInferCoreLetBody = (lambda unrestricted value : (family CoreTerm) . (lambda unrestricted bodyResult : (family CoreInferenceResult) . (eliminate CoreInferenceResult (lambda unrestricted result : (family CoreInferenceResult) . (family CoreInferenceResult)) bodyResult (branch CoreInferred bodyType . (constructor CoreInferenceResult CoreInferred (substituteCoreTop value bodyType))) (branch CoreInferenceFailed code . (constructor CoreInferenceResult CoreInferenceFailed code))))) def finishInferCoreLetValue = (lambda unrestricted annotation : (family CoreTerm) . (lambda unrestricted value : (family CoreTerm) . (lambda unrestricted valueResult : (family CoreInferenceResult) . (lambda unrestricted bodyResult : (family CoreInferenceResult) . (eliminate CoreInferenceResult (lambda unrestricted result : (family CoreInferenceResult) . (family CoreInferenceResult)) valueResult (branch CoreInferred valueType . (nat-eliminate (lambda unrestricted matches : Nat . (family CoreInferenceResult)) (constructor CoreInferenceResult CoreInferenceFailed (succ (succ (succ (succ (succ zero)))))) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family CoreInferenceResult) . (finishInferCoreLetBody value bodyResult))) (coreTermEqual (normalizeCoreType valueType) (normalizeCoreType annotation)))) (branch CoreInferenceFailed code . (constructor CoreInferenceResult CoreInferenceFailed code))))))) def finishInferCoreLetAnnotation = (lambda unrestricted annotation : (family CoreTerm) . (lambda unrestricted value : (family CoreTerm) . (lambda unrestricted annotationResult : (family CoreInferenceResult) . (lambda unrestricted valueResult : (family CoreInferenceResult) . (lambda unrestricted bodyResult : (family CoreInferenceResult) . (eliminate CoreInferenceResult (lambda unrestricted result : (family CoreInferenceResult) . (family CoreInferenceResult)) annotationResult (branch CoreInferred annotationType . (eliminate UniverseInspection (lambda unrestricted inspection : (family UniverseInspection) . (family CoreInferenceResult)) (inspectUniverse (normalizeCoreType annotationType)) (branch IsUniverse level . (finishInferCoreLetValue annotation value valueResult bodyResult)) (branch NotUniverse . (constructor CoreInferenceResult CoreInferenceFailed (succ (succ (succ (succ zero)))))))) (branch CoreInferenceFailed code . (constructor CoreInferenceResult CoreInferenceFailed code)))))))) def inferCore : (pi unrestricted term : (family CoreTerm) . (pi unrestricted context : (family TypeContext) . (family CoreInferenceResult))) = (lambda unrestricted term : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted value : (family CoreTerm) . (pi unrestricted context : (family TypeContext) . (family CoreInferenceResult))) term (branch CoreUniverse level . (lambda unrestricted context : (family TypeContext) . (constructor CoreInferenceResult CoreInferred (constructor CoreTerm CoreUniverse (succ level))))) (branch CoreNatural . (lambda unrestricted context : (family TypeContext) . (constructor CoreInferenceResult CoreInferred (constructor CoreTerm CoreUniverse zero)))) (branch CoreNaturalLiteral value . (lambda unrestricted context : (family TypeContext) . (inferCoreNaturalMagnitude value))) (branch CoreBound index . (lambda unrestricted context : (family TypeContext) . (eliminate TypeLookupResult (lambda unrestricted result : (family TypeLookupResult) . (family CoreInferenceResult)) (lookupType context index) (branch TypeFound variableType . (constructor CoreInferenceResult CoreInferred variableType)) (branch TypeNotFound missingIndex . (constructor CoreInferenceResult CoreInferenceFailed (succ zero)))))) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . (lambda unrestricted context : (family TypeContext) . (inferPiType multiplicity (ih_domain context) (ih_codomain (constructor TypeContext TypeContextBinding domain context))))) (branch CoreLambda multiplicity domain body ih_domain ih_body . (lambda unrestricted context : (family TypeContext) . (inferLambdaType multiplicity domain (ih_domain context) (ih_body (constructor TypeContext TypeContextBinding domain context))))) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . (lambda unrestricted context : (family TypeContext) . (finishInferCoreLetAnnotation annotation value (ih_annotation context) (ih_value context) (ih_body (constructor TypeContext TypeContextBinding annotation context))))) (branch CoreApplication function argument ih_function ih_argument . (lambda unrestricted context : (family TypeContext) . (inferCoreApplicationWithEffects function argument (ih_function context) (ih_argument context)))) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . (lambda unrestricted context : (family TypeContext) . (inferCoreArithmeticOperands operation function argument (ih_function context) (ih_argument context)))) (branch CoreNaturalSuccessor predecessor ih_predecessor . (lambda unrestricted context : (family TypeContext) . (inferNaturalSuccessorType (ih_predecessor context)))) (branch CoreByte . (lambda unrestricted context : (family TypeContext) . (constructor CoreInferenceResult CoreInferred (constructor CoreTerm CoreUniverse zero)))) (branch CoreByteLiteral value . (lambda unrestricted context : (family TypeContext) . (constructor CoreInferenceResult CoreInferred (constructor CoreTerm CoreByte)))) (branch CoreBytes . (lambda unrestricted context : (family TypeContext) . (constructor CoreInferenceResult CoreInferred (constructor CoreTerm CoreUniverse zero)))) (branch CoreBytesLiteral value . (lambda unrestricted context : (family TypeContext) . (constructor CoreInferenceResult CoreInferred (constructor CoreTerm CoreBytes)))) (branch CorePrimitiveTerm primitive . (lambda unrestricted context : (family TypeContext) . (constructor CoreInferenceResult CoreInferred (corePrimitiveType primitive)))) (branch CoreTermSequenceEnd . (lambda unrestricted context : (family TypeContext) . (constructor CoreInferenceResult CoreInferenceFailed coreFamilyInferenceFailureCode))) (branch CoreTermSequenceNext head tail ih_head ih_tail . (lambda unrestricted context : (family TypeContext) . (constructor CoreInferenceResult CoreInferenceFailed coreFamilyInferenceFailureCode))) (branch CoreFamilyApplication familyName arguments ih_arguments . (lambda unrestricted context : (family TypeContext) . (constructor CoreInferenceResult CoreInferenceFailed coreFamilyInferenceFailureCode))) (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . (lambda unrestricted context : (family TypeContext) . (constructor CoreInferenceResult CoreInferenceFailed coreFamilyInferenceFailureCode))) (branch CoreEliminatorBranch constructorName binderCount body ih_body . (lambda unrestricted context : (family TypeContext) . (constructor CoreInferenceResult CoreInferenceFailed coreFamilyInferenceFailureCode))) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . (lambda unrestricted context : (family TypeContext) . (constructor CoreInferenceResult CoreInferenceFailed coreFamilyInferenceFailureCode))))) def inferClosedCore : (pi unrestricted term : (family CoreTerm) . (family CoreInferenceResult)) = (lambda unrestricted term : (family CoreTerm) . (inferCore term (constructor TypeContext EmptyTypeContext))) def reduceCoreApplication : (pi unrestricted function : (family CoreTerm) . (pi unrestricted argument : (family CoreTerm) . (family CoreTerm))) = (lambda unrestricted function : (family CoreTerm) . (lambda unrestricted argument : (family CoreTerm) . (eliminate CoreFunctionInspection (lambda unrestricted inspection : (family CoreFunctionInspection) . (family CoreTerm)) (inspectCoreFunction function) (branch CoreFunctionLambda body . (substituteCoreTop argument body)) (branch CoreFunctionPrimitive primitive . (reduceDirectCorePrimitive primitive argument)) (branch CoreFunctionAppliedPrimitive primitive left . (reduceAppliedCorePrimitive primitive left argument)) (branch CoreFunctionAppliedPrimitive2 primitive first second . (corePrimitiveApplication3 primitive first second argument)) (branch CoreFunctionAppliedPrimitive3 primitive first second third . (reduceAppliedCoreEliminator primitive first second third argument)) (branch CoreFunctionOther . (constructor CoreTerm CoreApplication function argument))))) def betaReduceOne : (pi unrestricted term : (family CoreTerm) . (family CoreTerm)) = (lambda unrestricted term : (family CoreTerm) . (eliminate CoreTerm (lambda unrestricted value : (family CoreTerm) . (family CoreTerm)) term (branch CoreUniverse level . (constructor CoreTerm CoreUniverse level)) (branch CoreNatural . (constructor CoreTerm CoreNatural)) (branch CoreNaturalLiteral value . (constructor CoreTerm CoreNaturalLiteral value)) (branch CoreBound index . (constructor CoreTerm CoreBound index)) (branch CorePi multiplicity domain codomain ih_domain ih_codomain . (constructor CoreTerm CorePi multiplicity ih_domain ih_codomain)) (branch CoreLambda multiplicity domain body ih_domain ih_body . (constructor CoreTerm CoreLambda multiplicity ih_domain ih_body)) (branch CoreLet multiplicity annotation value body ih_annotation ih_value ih_body . (substituteCoreTop ih_value ih_body)) (branch CoreApplication function argument ih_function ih_argument . (reduceCoreApplication ih_function ih_argument)) (branch CoreNaturalArithmetic operation function argument ih_function ih_argument . (reduceCoreArithmetic operation ih_function ih_argument)) (branch CoreNaturalSuccessor predecessor ih_predecessor . (reduceCoreNaturalSuccessor ih_predecessor)) (branch CoreByte . (constructor CoreTerm CoreByte)) (branch CoreByteLiteral value . (constructor CoreTerm CoreByteLiteral value)) (branch CoreBytes . (constructor CoreTerm CoreBytes)) (branch CoreBytesLiteral value . (constructor CoreTerm CoreBytesLiteral value)) (branch CorePrimitiveTerm primitive . (constructor CoreTerm CorePrimitiveTerm primitive)) (branch CoreTermSequenceEnd . (constructor CoreTerm CoreTermSequenceEnd)) (branch CoreTermSequenceNext head tail ih_head ih_tail . (constructor CoreTerm CoreTermSequenceNext ih_head ih_tail)) (branch CoreFamilyApplication familyName arguments ih_arguments . (constructor CoreTerm CoreFamilyApplication familyName ih_arguments)) (branch CoreConstructorApplication familyName constructorName arguments ih_arguments . (constructor CoreTerm CoreConstructorApplication familyName constructorName ih_arguments)) (branch CoreEliminatorBranch constructorName binderCount body ih_body . (constructor CoreTerm CoreEliminatorBranch constructorName binderCount ih_body)) (branch CoreEliminator familyName motive scrutinee branches ih_motive ih_scrutinee ih_branches . (reduceCoreGenericEliminator familyName ih_motive ih_scrutinee ih_branches)))) def betaNormalizeWithWorkBudget = (workNormalizeCoreWithLimit (succ zero)) def betaNormalizeCheckedWithFuel = (lambda unrestricted rounds : Nat . (betaNormalizeWithWorkBudget rounds coreNormalizationDefaultWork)) -- Compatibility projection: this historical API returns the residual on -- exhaustion. New admission paths must consume CoreReductionResult instead. def betaNormalizeWithFuel = (lambda unrestricted fuel : Nat . (lambda unrestricted term : (family CoreTerm) . (eliminate CoreReductionResult (lambda unrestricted result : (family CoreReductionResult) . (family CoreTerm)) (betaNormalizeCheckedWithFuel fuel term) (branch CoreReductionCompleted normal rounds . normal) (branch CoreReductionExhausted residual rounds . residual))))