module Compiler.Parser import Compiler.AST import Compiler.NaturalOperation import Compiler.Lexer import Compiler.IntegerLiteral import Compiler.QuotedLiteral import Data.UTF8 import Compiler.LanguageEdition import Std.Natural family Syntax : Type 0 constructor SyntaxAtom field unrestricted syntaxSpelling : Bytes field unrestricted syntaxAtomOrigin : (family SyntaxOrigin) constructor SyntaxEmpty constructor SyntaxCons recursive unrestricted syntaxHead recursive unrestricted syntaxTail constructor SyntaxNode recursive unrestricted syntaxChildren end-family family SyntaxStack : Type 0 constructor SyntaxStackEnd constructor SyntaxStackFrame field unrestricted parentForest : (family Syntax) recursive unrestricted outerStack end-family family StructuralParseState : Type 0 constructor StructuralActive field unrestricted currentForest : (family Syntax) field unrestricted currentStack : (family SyntaxStack) constructor StructuralFailed field unrestricted structuralFailureCode : Nat end-family family StructuralParseResult : Type 0 constructor StructuralParsed field unrestricted parsedSyntax : (family Syntax) constructor StructuralParseFailed field unrestricted parseFailureCode : Nat field unrestricted parseFailureOrigin : (family SyntaxOrigin) end-family family StreamingStructuralState : Type 0 constructor StreamingStructuralActive field unrestricted pendingAtom : Bytes field unrestricted streamingForest : (family Syntax) field unrestricted streamingStack : (family SyntaxStack) field unrestricted streamingAtomOrigin : (family SyntaxOrigin) constructor StreamingStructuralFailed field unrestricted streamingFailureCode : Nat field unrestricted streamingFailureOrigin : (family SyntaxOrigin) field unrestricted streamingRecoveryAtom : Bytes field unrestricted streamingRecoveryOrigin : (family SyntaxOrigin) end-family family TermList : Type 0 constructor TermListEnd constructor TermListNext field unrestricted listedTerm : (family Term) recursive unrestricted listedRest end-family family TermDecodeResult : Type 0 constructor TermDecoded field unrestricted decodedTerm : (family Term) constructor TermsDecoded field unrestricted decodedTerms : (family TermList) constructor TermDecodeFailed field unrestricted termDecodeFailureCode : Nat field unrestricted termDecodeFailureOrigin : (family SyntaxOrigin) end-family family DecimalDigitResult : Type 0 constructor DecimalDigitMatched field unrestricted decimalDigitValue : Nat constructor NotDecimalDigit end-family family DecimalParseResult : Type 0 constructor DecimalParsed field unrestricted decimalNaturalValue : Nat constructor DecimalInvalid end-family family NaturalTermResult : Type 0 constructor NaturalTermDecoded field unrestricted naturalTermValue : Nat constructor NotNaturalTerm end-family family NaturalLiteralParseResult : Type 0 constructor NaturalLiteralParsed field unrestricted parsedNaturalLiteral : Nat constructor NaturalLiteralParseFailed field unrestricted naturalLiteralParseFailure : (family IntegerLiteralFailure) end-family family SourceByteResult : Type 0 constructor SourceByteDecoded field unrestricted decodedSourceByte : Byte constructor SourceByteInvalid end-family family SourceBytesResult : Type 0 constructor SourceBytesDecoded field unrestricted decodedSourceBytes : Bytes constructor SourceBytesInvalid end-family family TermSpellingResult : Type 0 constructor TermSpellingDecoded field unrestricted decodedTermSpelling : Bytes constructor TermHasNoSpelling end-family family QuantityDecodeResult : Type 0 constructor QuantityDecoded field unrestricted decodedQuantityTag : Nat constructor QuantityInvalid end-family family TermApplicationSpine : Type 0 constructor TermApplicationSpineValue field unrestricted spineHead : (family Term) field unrestricted spineArguments : (family TermList) end-family family LocalLetBindingDecodeResult : Type 0 constructor LocalLetBindingDecoded field unrestricted decodedLocalLetQuantity : Nat field unrestricted decodedLocalLetBinder : Bytes field unrestricted decodedLocalLetHasAnnotation : Nat field unrestricted decodedLocalLetAnnotation : (family Term) field unrestricted decodedLocalLetValue : (family Term) constructor LocalLetBindingDecodeFailed end-family family DoBodyDecodeResult : Type 0 constructor DoBodyDecoded field unrestricted decodedDoBody : (family Term) constructor DoBodyDecodeFailed end-family family DoStepDecodeResult : Type 0 constructor DoStepDecoded field unrestricted decodedDoStepNamed : Nat field unrestricted decodedDoStepQuantity : Nat field unrestricted decodedDoStepBinder : Bytes field unrestricted decodedDoStepComputation : (family Term) constructor DoStepDecodeFailed end-family family ParserStripStep : Type 0 constructor ParserStripStepValue field unrestricted parserStripEmit : Bytes field unrestricted parserStripNext : Nat end-family def consumeStructuralToken = (lambda unrestricted token : (family LexToken) . (lambda unrestricted state : (family StructuralParseState) . (eliminate StructuralParseState (lambda unrestricted value : (family StructuralParseState) . (family StructuralParseState)) state (branch StructuralActive currentForest currentStack . (eliminate LexToken (lambda unrestricted value : (family LexToken) . (family StructuralParseState)) token (branch TokenOpen . (eliminate SyntaxStack (lambda unrestricted value : (family SyntaxStack) . (family StructuralParseState)) currentStack (branch SyntaxStackEnd . (constructor StructuralParseState StructuralFailed (succ zero))) (branch SyntaxStackFrame parentForest outerStack ih_outerStack . (constructor StructuralParseState StructuralActive (constructor Syntax SyntaxCons (constructor Syntax SyntaxNode currentForest) parentForest) outerStack)))) (branch TokenClose . (constructor StructuralParseState StructuralActive (constructor Syntax SyntaxEmpty) (constructor SyntaxStack SyntaxStackFrame currentForest currentStack))) (branch TokenBoundary . (constructor StructuralParseState StructuralActive currentForest currentStack)) (branch TokenAtom atomSpelling . (constructor StructuralParseState StructuralActive (constructor Syntax SyntaxCons (constructor Syntax SyntaxAtom atomSpelling (constructor SyntaxOrigin SyntaxOriginUnknown)) currentForest) currentStack)))) (branch StructuralFailed structuralFailureCode . (constructor StructuralParseState StructuralFailed structuralFailureCode))))) def parseTokenStream : (pi unrestricted stream : (family TokenStream) . (family StructuralParseState)) = (lambda unrestricted stream : (family TokenStream) . (eliminate TokenStream (lambda unrestricted value : (family TokenStream) . (family StructuralParseState)) stream (branch TokenEnd . (constructor StructuralParseState StructuralActive (constructor Syntax SyntaxEmpty) (constructor SyntaxStack SyntaxStackEnd))) (branch TokenNext nextToken tokenRest ih_tokenRest . (consumeStructuralToken nextToken ih_tokenRest)))) def rejectAdditionalRoots = (lambda unrestricted root : (family Syntax) . (lambda unrestricted tail : (family Syntax) . (eliminate Syntax (lambda unrestricted value : (family Syntax) . (family StructuralParseResult)) tail (branch SyntaxAtom syntaxSpelling origin . (constructor StructuralParseResult StructuralParseFailed (succ (succ (succ zero))) (constructor SyntaxOrigin SyntaxOriginUnknown))) (branch SyntaxEmpty . (constructor StructuralParseResult StructuralParsed root)) (branch SyntaxCons syntaxHead syntaxTail ih_syntaxHead ih_syntaxTail . (constructor StructuralParseResult StructuralParseFailed (succ (succ (succ zero))) (constructor SyntaxOrigin SyntaxOriginUnknown))) (branch SyntaxNode syntaxChildren ih_syntaxChildren . (constructor StructuralParseResult StructuralParseFailed (succ (succ (succ zero))) (constructor SyntaxOrigin SyntaxOriginUnknown)))))) def finishStructuralForest = (lambda unrestricted forest : (family Syntax) . (eliminate Syntax (lambda unrestricted value : (family Syntax) . (family StructuralParseResult)) forest (branch SyntaxAtom syntaxSpelling origin . (constructor StructuralParseResult StructuralParsed forest)) (branch SyntaxEmpty . (constructor StructuralParseResult StructuralParseFailed (succ (succ (succ (succ zero)))) (constructor SyntaxOrigin SyntaxOriginUnknown))) (branch SyntaxCons syntaxHead syntaxTail ih_syntaxHead ih_syntaxTail . (rejectAdditionalRoots syntaxHead syntaxTail)) (branch SyntaxNode syntaxChildren ih_syntaxChildren . (constructor StructuralParseResult StructuralParsed forest)))) def finishStructuralStack = (lambda unrestricted forest : (family Syntax) . (lambda unrestricted stack : (family SyntaxStack) . (eliminate SyntaxStack (lambda unrestricted value : (family SyntaxStack) . (family StructuralParseResult)) stack (branch SyntaxStackEnd . (finishStructuralForest forest)) (branch SyntaxStackFrame parentForest outerStack ih_outerStack . (constructor StructuralParseResult StructuralParseFailed (succ (succ zero)) (constructor SyntaxOrigin SyntaxOriginUnknown)))))) def finishStructuralParse = (lambda unrestricted state : (family StructuralParseState) . (eliminate StructuralParseState (lambda unrestricted value : (family StructuralParseState) . (family StructuralParseResult)) state (branch StructuralActive currentForest currentStack . (finishStructuralStack currentForest currentStack)) (branch StructuralFailed structuralFailureCode . (constructor StructuralParseResult StructuralParseFailed structuralFailureCode (constructor SyntaxOrigin SyntaxOriginUnknown))))) def syntaxOriginRebaseRange = (lambda unrestricted origin : (family SyntaxOrigin) . (lambda unrestricted relativeStart : Nat . (lambda unrestricted relativeEnd : Nat . (eliminate SyntaxOrigin (lambda unrestricted current : (family SyntaxOrigin) . (family SyntaxOrigin)) origin (branch SyntaxOriginUnknown . (constructor SyntaxOrigin SyntaxOriginUnknown)) (branch SyntaxOriginRange start end . (constructor SyntaxOrigin SyntaxOriginRange (Std.Natural/naturalAdd start relativeStart) (Std.Natural/naturalAdd start relativeEnd))))))) def flushStreamingAtom = (lambda unrestricted state : (family StreamingStructuralState) . (eliminate StreamingStructuralState (lambda unrestricted value : (family StreamingStructuralState) . (family StreamingStructuralState)) state (branch StreamingStructuralActive pendingAtom streamingForest streamingStack origin . (nat-eliminate (lambda unrestricted atomLength : Nat . (family StreamingStructuralState)) (constructor StreamingStructuralState StreamingStructuralActive b"" streamingForest streamingStack (constructor SyntaxOrigin SyntaxOriginUnknown)) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family StreamingStructuralState) . (eliminate QuotedLiteralResult (lambda unrestricted checked : (family QuotedLiteralResult) . (family StreamingStructuralState)) (Compiler.QuotedLiteral/quotedValidateSourceAtom pendingAtom) (branch QuotedLiteralDecoded payload . (constructor StreamingStructuralState StreamingStructuralActive b"" (constructor Syntax SyntaxCons (constructor Syntax SyntaxAtom pendingAtom origin) streamingForest) streamingStack (constructor SyntaxOrigin SyntaxOriginUnknown))) (branch QuotedLiteralFailed failure start end . (constructor StreamingStructuralState StreamingStructuralFailed (Compiler.QuotedLiteral/quotedLiteralFailureCode failure) (syntaxOriginRebaseRange origin start end) b"" (constructor SyntaxOrigin SyntaxOriginUnknown)))))) (bytes-length pendingAtom))) (branch StreamingStructuralFailed streamingFailureCode structuralFailureOrigin recoveryAtom recoveryOrigin . (eliminate QuotedLiteralResult (lambda unrestricted checked : (family QuotedLiteralResult) . (family StreamingStructuralState)) (Compiler.QuotedLiteral/quotedValidateSourceAtom recoveryAtom) (branch QuotedLiteralDecoded payload . (constructor StreamingStructuralState StreamingStructuralFailed streamingFailureCode structuralFailureOrigin b"" (constructor SyntaxOrigin SyntaxOriginUnknown))) (branch QuotedLiteralFailed failure start end . (constructor StreamingStructuralState StreamingStructuralFailed (Compiler.QuotedLiteral/quotedLiteralFailureCode failure) (syntaxOriginRebaseRange recoveryOrigin start end) b"" (constructor SyntaxOrigin SyntaxOriginUnknown))))))) def prependStreamingAtomByte = (lambda unrestricted byte : Byte . (lambda unrestricted state : (family StreamingStructuralState) . (eliminate StreamingStructuralState (lambda unrestricted value : (family StreamingStructuralState) . (family StreamingStructuralState)) state (branch StreamingStructuralActive pendingAtom streamingForest streamingStack origin . (constructor StreamingStructuralState StreamingStructuralActive (bytes-cons byte pendingAtom) streamingForest streamingStack origin)) (branch StreamingStructuralFailed streamingFailureCode structuralFailureOrigin recoveryAtom recoveryOrigin . (constructor StreamingStructuralState StreamingStructuralFailed streamingFailureCode structuralFailureOrigin (bytes-cons byte recoveryAtom) recoveryOrigin))))) def applyStreamingStructuralToken = (lambda unrestricted token : (family LexToken) . (lambda unrestricted state : (family StreamingStructuralState) . (eliminate StreamingStructuralState (lambda unrestricted value : (family StreamingStructuralState) . (family StreamingStructuralState)) (flushStreamingAtom state) (branch StreamingStructuralActive pendingAtom streamingForest streamingStack origin . (eliminate StructuralParseState (lambda unrestricted value : (family StructuralParseState) . (family StreamingStructuralState)) (consumeStructuralToken token (constructor StructuralParseState StructuralActive streamingForest streamingStack)) (branch StructuralActive currentForest currentStack . (constructor StreamingStructuralState StreamingStructuralActive b"" currentForest currentStack (constructor SyntaxOrigin SyntaxOriginUnknown))) (branch StructuralFailed structuralFailureCode . (constructor StreamingStructuralState StreamingStructuralFailed structuralFailureCode (constructor SyntaxOrigin SyntaxOriginUnknown) b"" (constructor SyntaxOrigin SyntaxOriginUnknown))))) (branch StreamingStructuralFailed streamingFailureCode structuralFailureOrigin recoveryAtom recoveryOrigin . (constructor StreamingStructuralState StreamingStructuralFailed streamingFailureCode structuralFailureOrigin recoveryAtom recoveryOrigin))))) def consumeStreamingSourceByte = (lambda unrestricted byte : Byte . (lambda unrestricted state : (family StreamingStructuralState) . (eliminate ByteClass (lambda unrestricted value : (family ByteClass) . (family StreamingStructuralState)) (classifyByte byte) (branch OpenDelimiter . (applyStreamingStructuralToken (constructor LexToken TokenOpen) state)) (branch CloseDelimiter . (applyStreamingStructuralToken (constructor LexToken TokenClose) state)) (branch Whitespace . (flushStreamingAtom state)) (branch DecimalDigit . (prependStreamingAtomByte byte state)) (branch IdentifierByte . (prependStreamingAtomByte byte state))))) def finishStreamingStructuralState = (lambda unrestricted state : (family StreamingStructuralState) . (eliminate StreamingStructuralState (lambda unrestricted value : (family StreamingStructuralState) . (family StructuralParseResult)) (flushStreamingAtom state) (branch StreamingStructuralActive pendingAtom streamingForest streamingStack origin . (finishStructuralParse (constructor StructuralParseState StructuralActive streamingForest streamingStack))) (branch StreamingStructuralFailed streamingFailureCode structuralFailureOrigin recoveryAtom recoveryOrigin . (constructor StructuralParseResult StructuralParseFailed streamingFailureCode structuralFailureOrigin)))) def parserCommentDashByte = (byte 45) def parserCommentNewlineByte = (byte 10) -- Byte-level comment stripping with Stage-0 parity: "--" begins a comment -- only at token start (a dash inside an identifier is name material), and a -- comment runs to the end of its line. States: 0 between tokens, 1 inside -- an atom, 2 pending single dash, 3 inside a comment. Each byte reduces to -- one emitted byte string plus one next state so the fold recurses exactly -- once per byte. def parserStripStateBetween = zero def parserStripStateAtom = (succ zero) def parserStripStatePendingDash = (succ (succ zero)) def parserStripStateComment = (succ (succ (succ zero))) def parserStripStep = (lambda unrestricted emit : Bytes . (lambda unrestricted next : Nat . (constructor ParserStripStep ParserStripStepValue emit next))) def parserStripTokenStep = (lambda unrestricted head : Byte . (eliminate ByteClass (lambda unrestricted value : (family ByteClass) . (family ParserStripStep)) (classifyByte head) (branch OpenDelimiter . (parserStripStep (bytes-cons head b"") parserStripStateBetween)) (branch CloseDelimiter . (parserStripStep (bytes-cons head b"") parserStripStateBetween)) (branch Whitespace . (parserStripStep (bytes-cons head b"") parserStripStateBetween)) (branch DecimalDigit . (parserStripStep (bytes-cons head b"") parserStripStateAtom)) (branch IdentifierByte . (parserStripStep (bytes-cons head b"") parserStripStateAtom)))) def parserStripBetweenStep = (lambda unrestricted head : Byte . (nat-eliminate (lambda unrestricted headIsDash : Nat . (family ParserStripStep)) (parserStripTokenStep head) (lambda unrestricted dashPredecessor : Nat . (lambda unrestricted dashInduction : (family ParserStripStep) . (parserStripStep b"" parserStripStatePendingDash))) (byte-equal head parserCommentDashByte))) def parserStripPendingStep = (lambda unrestricted head : Byte . (nat-eliminate (lambda unrestricted headIsDash : Nat . (family ParserStripStep)) (eliminate ParserStripStep (lambda unrestricted value : (family ParserStripStep) . (family ParserStripStep)) (parserStripTokenStep head) (branch ParserStripStepValue emit next . (parserStripStep (bytes-cons parserCommentDashByte emit) next))) (lambda unrestricted secondDashPredecessor : Nat . (lambda unrestricted secondDashInduction : (family ParserStripStep) . (parserStripStep b"" parserStripStateComment))) (byte-equal head parserCommentDashByte))) def parserStripCommentStep = (lambda unrestricted head : Byte . (nat-eliminate (lambda unrestricted headIsNewline : Nat . (family ParserStripStep)) (parserStripStep b"" parserStripStateComment) (lambda unrestricted newlinePredecessor : Nat . (lambda unrestricted newlineInduction : (family ParserStripStep) . (parserStripStep (bytes-cons parserCommentNewlineByte b"") parserStripStateBetween))) (byte-equal head parserCommentNewlineByte))) def parserStripByteStep = (lambda unrestricted head : Byte . (lambda unrestricted state : Nat . (nat-eliminate (lambda unrestricted stateZero : Nat . (family ParserStripStep)) (parserStripBetweenStep head) (lambda unrestricted stateOne : Nat . (lambda unrestricted inductionOne : (family ParserStripStep) . (nat-eliminate (lambda unrestricted innerOne : Nat . (family ParserStripStep)) (parserStripTokenStep head) (lambda unrestricted stateTwo : Nat . (lambda unrestricted inductionTwo : (family ParserStripStep) . (nat-eliminate (lambda unrestricted innerTwo : Nat . (family ParserStripStep)) (parserStripPendingStep head) (lambda unrestricted stateThree : Nat . (lambda unrestricted inductionThree : (family ParserStripStep) . (parserStripCommentStep head))) stateTwo))) stateOne))) state))) -- The comment strip machine is fused into the structural fold. Bytes are a -- flat native array in the runtime, so rebuilding a stripped copy of the -- source byte-by-byte copies the whole suffix per byte (quadratic memory). -- Instead the fold is continuation-passing: the strip state flows forward -- through the function argument while the parse state flows backward -- through the result, and each emitted byte is consumed directly with no -- byte-string rebuilding. A comment that reaches end-of-input emits -- nothing, matching the trusted lexer. def parserInitialStreamingState = (constructor StreamingStructuralState StreamingStructuralActive b"" (constructor Syntax SyntaxEmpty) (constructor SyntaxStack SyntaxStackEnd) (constructor SyntaxOrigin SyntaxOriginUnknown)) def parserLocatePendingAtom = (lambda unrestricted offset : Nat . (lambda unrestricted state : (family StreamingStructuralState) . (eliminate StreamingStructuralState (lambda unrestricted current : (family StreamingStructuralState) . (family StreamingStructuralState)) state (branch StreamingStructuralActive pending forest stack origin . (constructor StreamingStructuralState StreamingStructuralActive pending forest stack (constructor SyntaxOrigin SyntaxOriginRange offset (Std.Natural/naturalAdd offset (bytes-length pending))))) (branch StreamingStructuralFailed code structuralFailureOrigin recoveryAtom recoveryOrigin . (constructor StreamingStructuralState StreamingStructuralFailed code structuralFailureOrigin recoveryAtom (constructor SyntaxOrigin SyntaxOriginRange offset (Std.Natural/naturalAdd offset (bytes-length recoveryAtom)))))))) def parserPrependLocatedByte = (lambda unrestricted offset : Nat . (lambda unrestricted head : Byte . (lambda unrestricted state : (family StreamingStructuralState) . (parserLocatePendingAtom offset (prependStreamingAtomByte head state))))) def parserConsumeEmittedBytes = (lambda unrestricted endOffset : Nat . (lambda unrestricted emit : Bytes . (app (bytes-eliminate (lambda unrestricted remaining : Bytes . (pi unrestricted offset : Nat . (pi unrestricted state : (family StreamingStructuralState) . (family StreamingStructuralState)))) (lambda unrestricted offset : Nat . (lambda unrestricted state : (family StreamingStructuralState) . state)) (lambda unrestricted head : Byte . (lambda unrestricted tail : Bytes . (lambda unrestricted continue : (pi unrestricted offset : Nat . (pi unrestricted state : (family StreamingStructuralState) . (family StreamingStructuralState))) . (lambda unrestricted offset : Nat . (lambda unrestricted state : (family StreamingStructuralState) . (parserLocatePendingAtom offset (consumeStreamingSourceByte head (continue (succ offset) state)))))))) emit) (Std.Natural/naturalSaturatingSubtract endOffset (bytes-length emit))))) def parserFinishStripState = (lambda unrestricted offset : Nat . (lambda unrestricted stripState : Nat . (nat-eliminate (lambda unrestricted stateZero : Nat . (family StreamingStructuralState)) parserInitialStreamingState (lambda unrestricted stateOne : Nat . (lambda unrestricted inductionOne : (family StreamingStructuralState) . (nat-eliminate (lambda unrestricted innerOne : Nat . (family StreamingStructuralState)) parserInitialStreamingState (lambda unrestricted stateTwo : Nat . (lambda unrestricted inductionTwo : (family StreamingStructuralState) . (nat-eliminate (lambda unrestricted innerTwo : Nat . (family StreamingStructuralState)) (parserPrependLocatedByte (Std.Natural/naturalPredecessor offset) parserCommentDashByte parserInitialStreamingState) (lambda unrestricted stateThree : Nat . (lambda unrestricted inductionThree : (family StreamingStructuralState) . parserInitialStreamingState)) stateTwo))) stateOne))) stripState))) -- Thunked branch selection keeps the unselected continuation unforced. def parserChooseStreamingState = (lambda unrestricted condition : Nat . (lambda unrestricted yes : (pi unrestricted force : Nat . (family StreamingStructuralState)) . (lambda unrestricted no : (pi unrestricted force : Nat . (family StreamingStructuralState)) . (app (nat-eliminate (lambda unrestricted flag : Nat . (pi unrestricted force : Nat . (family StreamingStructuralState))) no (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : (pi unrestricted force : Nat . (family StreamingStructuralState)) . yes)) condition) zero)))) def parserStripIsComment = (lambda unrestricted stripState : Nat . (nat-eliminate (lambda unrestricted value : Nat . Nat) zero (lambda unrestricted pred3 : Nat . (lambda unrestricted unused : Nat . (nat-eliminate (lambda unrestricted value : Nat . Nat) zero (lambda unrestricted pred2 : Nat . (lambda unrestricted unused : Nat . (nat-eliminate (lambda unrestricted value : Nat . Nat) zero (lambda unrestricted pred1 : Nat . (lambda unrestricted unused : Nat . (nat-eliminate (lambda unrestricted value : Nat . Nat) (succ zero) (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : Nat . zero)) pred1))) pred2))) pred3))) stripState)) def parserQuoteIsEscaped = (lambda unrestricted quoteState : Nat . (nat-eliminate (lambda unrestricted value : Nat . Nat) zero (lambda unrestricted pred2 : Nat . (lambda unrestricted unused : Nat . (nat-eliminate (lambda unrestricted value : Nat . Nat) zero (lambda unrestricted pred1 : Nat . (lambda unrestricted unused : Nat . (nat-eliminate (lambda unrestricted value : Nat . Nat) (succ zero) (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : Nat . zero)) pred1))) pred2))) quoteState)) def parserOutsideSourceByteUnchecked = (lambda unrestricted bytePrefix : Nat . (lambda unrestricted offset : Nat . (lambda unrestricted head : Byte . (lambda unrestricted stripState : Nat . (lambda unrestricted continue : (pi unrestricted quoteState : Nat . (pi unrestricted stripState : Nat . (family StreamingStructuralState))) . (parserChooseStreamingState (parserStripIsComment stripState) (lambda unrestricted force : Nat . (eliminate ParserStripStep (lambda unrestricted value : (family ParserStripStep) . (family StreamingStructuralState)) (parserStripByteStep head stripState) (branch ParserStripStepValue emit next . (parserConsumeEmittedBytes (succ offset) emit (continue zero next))))) (lambda unrestricted force : Nat . (parserChooseStreamingState (byte-equal head (byte 34)) (lambda unrestricted force : Nat . (parserChooseStreamingState bytePrefix (lambda unrestricted force : Nat . (parserPrependLocatedByte offset head (continue (succ zero) parserStripStateAtom))) (lambda unrestricted force : Nat . (flushStreamingAtom (parserPrependLocatedByte offset head (continue (succ zero) parserStripStateAtom)))))) (lambda unrestricted force : Nat . (eliminate ParserStripStep (lambda unrestricted value : (family ParserStripStep) . (family StreamingStructuralState)) (parserStripByteStep head stripState) (branch ParserStripStepValue emit next . (parserConsumeEmittedBytes (succ offset) emit (continue zero next))))))))))))) -- Only ASCII token separators may be control bytes outside payloads. def parserSourceControlInvalid = (lambda unrestricted value : Byte . (nat-eliminate (lambda unrestricted low : Nat . Nat) (byte-equal value (byte 127)) (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : Nat . (nat-eliminate (lambda unrestricted whitespace : Nat . Nat) (succ zero) (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : Nat . zero)) (Compiler.Lexer/isWhitespace value)))) (byte-less-than value (byte 32)))) -- Unicode is legal only in a quoted token or a comment, never an identifier. def parserOutsideSourceByte = (lambda unrestricted bytePrefix : Nat . (lambda unrestricted offset : Nat . (lambda unrestricted head : Byte . (lambda unrestricted stripState : Nat . (lambda unrestricted continue : (pi unrestricted quoteState : Nat . (pi unrestricted stripState : Nat . (family StreamingStructuralState))) . (parserChooseStreamingState (parserStripIsComment stripState) (lambda unrestricted force : Nat . (parserOutsideSourceByteUnchecked bytePrefix offset head stripState continue)) (lambda unrestricted force : Nat . (parserChooseStreamingState (byte-less-than head (byte 128)) (lambda unrestricted force : Nat . (parserChooseStreamingState (parserSourceControlInvalid head) (lambda unrestricted force : Nat . (constructor StreamingStructuralState StreamingStructuralFailed (byte-to-nat (byte 103)) (constructor SyntaxOrigin SyntaxOriginUnknown) b"" (constructor SyntaxOrigin SyntaxOriginUnknown))) (lambda unrestricted force : Nat . (parserOutsideSourceByteUnchecked bytePrefix offset head stripState continue)))) (lambda unrestricted force : Nat . (constructor StreamingStructuralState StreamingStructuralFailed (byte-to-nat (byte 102)) (constructor SyntaxOrigin SyntaxOriginUnknown) b"" (constructor SyntaxOrigin SyntaxOriginUnknown))))))))))) -- Both quote modes reject source newlines; an escape never hides CR/LF. def parserQuotedSourceByte = (lambda unrestricted offset : Nat . (lambda unrestricted head : Byte . (lambda unrestricted quoteState : Nat . (lambda unrestricted stripState : Nat . (lambda unrestricted continue : (pi unrestricted quoteState : Nat . (pi unrestricted stripState : Nat . (family StreamingStructuralState))) . (parserChooseStreamingState (byte-equal head (byte 13)) (lambda unrestricted force : Nat . (constructor StreamingStructuralState StreamingStructuralFailed (byte-to-nat (byte 96)) (constructor SyntaxOrigin SyntaxOriginRange offset (succ offset)) (bytes-cons head b"") (constructor SyntaxOrigin SyntaxOriginRange offset (succ offset)))) (lambda unrestricted force : Nat . (parserChooseStreamingState (byte-equal head (byte 10)) (lambda unrestricted force : Nat . (constructor StreamingStructuralState StreamingStructuralFailed (byte-to-nat (byte 96)) (constructor SyntaxOrigin SyntaxOriginRange offset (succ offset)) (bytes-cons head b"") (constructor SyntaxOrigin SyntaxOriginRange offset (succ offset)))) (lambda unrestricted force : Nat . (parserChooseStreamingState (parserQuoteIsEscaped quoteState) (lambda unrestricted force : Nat . (parserPrependLocatedByte offset head (continue (succ zero) stripState))) (lambda unrestricted force : Nat . (parserChooseStreamingState (byte-equal head (byte 34)) (lambda unrestricted force : Nat . (parserPrependLocatedByte offset head (flushStreamingAtom (continue zero parserStripStateBetween)))) (lambda unrestricted force : Nat . (parserChooseStreamingState (byte-equal head (byte 92)) (lambda unrestricted force : Nat . (parserPrependLocatedByte offset head (continue (succ (succ zero)) stripState))) (lambda unrestricted force : Nat . (parserPrependLocatedByte offset head (continue (succ zero) stripState))))))))))))))))) -- Quote state flows forward (0 outside,1 quoted,2 escaped); atom construction -- flows backwards. Quoted bytes never become delimiters or comment markers. def parserNextBytePrefix = (lambda unrestricted head : Byte . (lambda unrestricted quoteState : Nat . (lambda unrestricted stripState : Nat . (Std.Natural/naturalAnd (Std.Natural/naturalIsZero quoteState) (Std.Natural/naturalAnd (byte-equal head (byte 98)) (Std.Natural/naturalIsZero stripState)))))) def parseStreamingValidSource = (lambda unrestricted rawSource : Bytes . (app (bytes-eliminate (lambda unrestricted remaining : Bytes . (pi unrestricted offset : Nat . (pi unrestricted quoteState : Nat . (pi unrestricted stripState : Nat . (pi unrestricted bytePrefix : Nat . (family StreamingStructuralState)))))) (lambda unrestricted offset : Nat . (lambda unrestricted quoteState : Nat . (lambda unrestricted stripState : Nat . (lambda unrestricted bytePrefix : Nat . (parserFinishStripState offset stripState))))) (lambda unrestricted head : Byte . (lambda unrestricted tail : Bytes . (lambda unrestricted continue : (pi unrestricted offset : Nat . (pi unrestricted quoteState : Nat . (pi unrestricted stripState : Nat . (pi unrestricted bytePrefix : Nat . (family StreamingStructuralState))))) . (lambda unrestricted offset : Nat . (lambda unrestricted quoteState : Nat . (lambda unrestricted stripState : Nat . (lambda unrestricted bytePrefix : Nat . (app (lambda unrestricted next : (pi unrestricted nextQuote : Nat . (pi unrestricted nextStrip : Nat . (family StreamingStructuralState))) . (parserChooseStreamingState quoteState (lambda unrestricted force : Nat . (parserQuotedSourceByte offset head quoteState stripState next)) (lambda unrestricted force : Nat . (parserOutsideSourceByte bytePrefix offset head stripState next)))) (lambda unrestricted nextQuote : Nat . (lambda unrestricted nextStrip : Nat . (continue (succ offset) nextQuote nextStrip (parserNextBytePrefix head quoteState stripState)))))))))))) rawSource) zero zero parserStripStateBetween zero)) -- A forest uses the same scanner and stack checks as an expression. Its -- wrapper exists only in Syntax, so it cannot change source tokenization. def finishStreamingStructuralForest = (lambda unrestricted state : (family StreamingStructuralState) . (eliminate StreamingStructuralState (lambda unrestricted current : (family StreamingStructuralState) . (family StructuralParseResult)) (flushStreamingAtom state) (branch StreamingStructuralActive pending forest stack origin . (eliminate SyntaxStack (lambda unrestricted current : (family SyntaxStack) . (family StructuralParseResult)) stack (branch SyntaxStackEnd . (constructor StructuralParseResult StructuralParsed (constructor Syntax SyntaxNode forest))) (branch SyntaxStackFrame parent outer ih_outer . (constructor StructuralParseResult StructuralParseFailed (succ (succ zero)) (constructor SyntaxOrigin SyntaxOriginUnknown))))) (branch StreamingStructuralFailed code structuralFailureOrigin recoveryAtom recoveryOrigin . (constructor StructuralParseResult StructuralParseFailed code structuralFailureOrigin)))) def parseStructuralValidSource = (lambda unrestricted rawSource : Bytes . (finishStreamingStructuralState (parseStreamingValidSource rawSource))) -- Validate the whole byte source once, before comments/literals can hide bytes. def parseStructuralSourceWithFinalizer = (lambda unrestricted finish : (pi unrestricted state : (family StreamingStructuralState) . (family StructuralParseResult)) . (lambda unrestricted rawSource : Bytes . (eliminate UTF8DecodeResult (lambda unrestricted decoded : (family UTF8DecodeResult) . (family StructuralParseResult)) (Data.UTF8/decodeUTF8 rawSource) (branch UTF8DecodeSucceeded points . (finish (parseStreamingValidSource rawSource))) (branch UTF8DecodeFailed failure offset . (constructor StructuralParseResult StructuralParseFailed (byte-to-nat (byte 101)) (constructor SyntaxOrigin SyntaxOriginUnknown)))))) def parseStructuralSource = (parseStructuralSourceWithFinalizer finishStreamingStructuralState) def parseStructuralSourceForest = (parseStructuralSourceWithFinalizer finishStreamingStructuralForest) def addNatural = (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 syntaxWeight = (lambda unrestricted syntax : (family Syntax) . (eliminate Syntax (lambda unrestricted value : (family Syntax) . Nat) syntax (branch SyntaxAtom syntaxSpelling origin . (bytes-length syntaxSpelling)) (branch SyntaxEmpty . zero) (branch SyntaxCons syntaxHead syntaxTail ih_syntaxHead ih_syntaxTail . (addNatural ih_syntaxHead ih_syntaxTail)) (branch SyntaxNode syntaxChildren ih_syntaxChildren . (succ ih_syntaxChildren)))) def structuralResultCode = (lambda unrestricted result : (family StructuralParseResult) . (eliminate StructuralParseResult (lambda unrestricted value : (family StructuralParseResult) . Nat) result (branch StructuralParsed parsedSyntax . (syntaxWeight parsedSyntax)) (branch StructuralParseFailed parseFailureCode structuralFailureOrigin . parseFailureCode))) def structuralParserSample : Nat = (structuralResultCode (parseStructuralSource b"(alpha (beta gamma))")) def parserNaturalAnd = (lambda unrestricted left : Nat . (lambda unrestricted right : Nat . (nat-eliminate (lambda unrestricted value : Nat . Nat) zero (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . right)) left))) def parserNaturalOr = (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 zero))) left))) def bytesEqual = (lambda unrestricted left : Bytes . (lambda unrestricted right : Bytes . (bytes-equal left right))) def zeroSpelling = b"zero" def decimalZeroSpelling = b"0" def successorSpelling = b"succ" def applicationSpelling = b"app" def lambdaSpelling = b"lambda" def piSpelling = b"pi" def erasedSpelling = b"erased" def linearSpelling = b"linear" def affineSpelling = b"affine" def unrestrictedSpelling = b"unrestricted" def colonSpelling = b":" def dotSpelling = b"." def naturalTypeSpelling = b"Nat" def universeTypeSpelling = b"Type" def bytesTypeSpelling = b"Bytes" def byteTypeSpelling = b"Byte" def byteLiteralSpelling = b"byte" def bytesLiteralSpelling = b"bytes" -- Canonical spelling of the bytes-cons primitive. The parser lowers a -- computed bytes expression to bytes-cons applications, and the elaborator -- resolves the same spelling; both use this single definition. def bytesConsSpelling = b"bytes-cons" def familyApplicationSpelling = b"family" def constructorApplicationSpelling = b"constructor" def eliminatorSpelling = b"eliminate" def branchSpelling = b"branch" def matchSpelling = b"match" def matchWithSpelling = b"match-with" def caseSpelling = b"case" def inductionMarkerSpelling = b"ih" def recordSpelling = b"record" def projectSpelling = b"project" def updateSpelling = b"update" def equalsSpelling = b"=" def letStarSpelling = b"let*" def inSpelling = b"in" def doSpelling = b"do" def returnSpelling = b"return" def leftArrowSpelling = b"<-" def chooseDecimalDigit = (lambda unrestricted matched : Nat . (lambda unrestricted digitValue : Nat . (lambda unrestricted fallback : (family DecimalDigitResult) . (nat-eliminate (lambda unrestricted value : Nat . (family DecimalDigitResult)) fallback (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family DecimalDigitResult) . (constructor DecimalDigitResult DecimalDigitMatched digitValue))) matched)))) def decodeDecimalDigit = (lambda unrestricted value : Byte . (chooseDecimalDigit (byte-equal value (byte 48)) zero (chooseDecimalDigit (byte-equal value (byte 49)) (succ zero) (chooseDecimalDigit (byte-equal value (byte 50)) (succ (succ zero)) (chooseDecimalDigit (byte-equal value (byte 51)) (succ (succ (succ zero))) (chooseDecimalDigit (byte-equal value (byte 52)) (succ (succ (succ (succ zero)))) (chooseDecimalDigit (byte-equal value (byte 53)) (succ (succ (succ (succ (succ zero))))) (chooseDecimalDigit (byte-equal value (byte 54)) (succ (succ (succ (succ (succ (succ zero)))))) (chooseDecimalDigit (byte-equal value (byte 55)) (succ (succ (succ (succ (succ (succ (succ zero))))))) (chooseDecimalDigit (byte-equal value (byte 56)) (succ (succ (succ (succ (succ (succ (succ (succ zero)))))))) (chooseDecimalDigit (byte-equal value (byte 57)) (succ (succ (succ (succ (succ (succ (succ (succ (succ zero))))))))) (constructor DecimalDigitResult NotDecimalDigit)))))))))))) def naturalDouble = (lambda unrestricted value : Nat . (addNatural value value)) def naturalQuadruple = (lambda unrestricted value : Nat . (naturalDouble (naturalDouble value))) def naturalOctuple = (lambda unrestricted value : Nat . (naturalDouble (naturalQuadruple value))) def advanceDecimal = (lambda unrestricted accumulator : Nat . (lambda unrestricted digitValue : Nat . (addNatural (naturalOctuple accumulator) (addNatural (naturalDouble accumulator) digitValue)))) def parseDecimalSpelling = (lambda unrestricted spelling : Bytes . (app (bytes-eliminate (lambda unrestricted remaining : Bytes . (pi unrestricted accumulator : Nat . (family DecimalParseResult))) (lambda unrestricted accumulator : Nat . (constructor DecimalParseResult DecimalParsed accumulator)) (lambda unrestricted head : Byte . (lambda unrestricted tail : Bytes . (lambda unrestricted parseTail : (pi unrestricted accumulator : Nat . (family DecimalParseResult)) . (lambda unrestricted accumulator : Nat . (eliminate DecimalDigitResult (lambda unrestricted result : (family DecimalDigitResult) . (family DecimalParseResult)) (decodeDecimalDigit head) (branch DecimalDigitMatched decimalDigitValue . (parseTail (advanceDecimal accumulator decimalDigitValue))) (branch NotDecimalDigit . (constructor DecimalParseResult DecimalInvalid))))))) spelling) zero)) def scaleNaturalLiteral = (lambda unrestricted radix : (family IntegerLiteralRadix) . (lambda unrestricted value : Nat . (eliminate IntegerLiteralRadix (lambda unrestricted current : (family IntegerLiteralRadix) . Nat) radix (branch IntegerLiteralDecimal . (advanceDecimal value zero)) (branch IntegerLiteralBinary . (naturalDouble value)) (branch IntegerLiteralHexadecimal . (naturalDouble (naturalOctuple value)))))) def foldNaturalLiteralDigits = (lambda unrestricted radix : (family IntegerLiteralRadix) . (lambda unrestricted digits : Bytes . (app (bytes-eliminate (lambda unrestricted remaining : Bytes . (pi unrestricted accumulator : Nat . (family NaturalLiteralParseResult))) (lambda unrestricted accumulator : Nat . (constructor NaturalLiteralParseResult NaturalLiteralParsed accumulator)) (lambda unrestricted head : Byte . (lambda unrestricted tail : Bytes . (lambda unrestricted continue : (pi unrestricted accumulator : Nat . (family NaturalLiteralParseResult)) . (lambda unrestricted accumulator : Nat . (eliminate IntegerLiteralDigitResult (lambda unrestricted value : (family IntegerLiteralDigitResult) . (family NaturalLiteralParseResult)) (Compiler.IntegerLiteral/integerLiteralDecodeDigit radix head) (branch IntegerLiteralDigitValue digit . (continue (addNatural (scaleNaturalLiteral radix accumulator) digit))) (branch IntegerLiteralDigitFailed failure . (constructor NaturalLiteralParseResult NaturalLiteralParseFailed failure))))))) (Compiler.IntegerLiteral/integerLiteralStripSeparators digits)) zero))) -- Shared exact Nat accumulation for universe levels and expected Nat literals. -- Range is not capped to a machine word; compact storage remains separate work. def parseNaturalLiteralDigits = (lambda unrestricted radix : (family IntegerLiteralRadix) . (lambda unrestricted digits : Bytes . (eliminate IntegerLiteralSyntaxResult (lambda unrestricted result : (family IntegerLiteralSyntaxResult) . (family NaturalLiteralParseResult)) (Compiler.IntegerLiteral/integerLiteralValidateSeparators radix digits) (branch IntegerLiteralSyntaxAccepted . (foldNaturalLiteralDigits radix digits)) (branch IntegerLiteralSyntaxFailed failure . (constructor NaturalLiteralParseResult NaturalLiteralParseFailed failure))))) def chooseNaturalLiteralParse = (lambda unrestricted flag : Nat . (lambda unrestricted yes : (pi unrestricted force : Nat . (family NaturalLiteralParseResult)) . (lambda unrestricted no : (pi unrestricted force : Nat . (family NaturalLiteralParseResult)) . (app (nat-eliminate (lambda unrestricted value : Nat . (pi unrestricted force : Nat . (family NaturalLiteralParseResult))) no (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalLiteralParseResult)) . yes)) flag) zero)))) def parseUnsignedNaturalLiteral = (lambda unrestricted spelling : Bytes . (chooseNaturalLiteralParse (byte-equal (bytes-head spelling) (byte 48)) (lambda unrestricted force : Nat . (chooseNaturalLiteralParse (addNatural (byte-equal (bytes-head (bytes-tail spelling)) (byte 120)) (byte-equal (bytes-head (bytes-tail spelling)) (byte 88))) (lambda unrestricted force : Nat . (parseNaturalLiteralDigits (constructor IntegerLiteralRadix IntegerLiteralHexadecimal) (bytes-tail (bytes-tail spelling)))) (lambda unrestricted force : Nat . (chooseNaturalLiteralParse (addNatural (byte-equal (bytes-head (bytes-tail spelling)) (byte 98)) (byte-equal (bytes-head (bytes-tail spelling)) (byte 66))) (lambda unrestricted force : Nat . (parseNaturalLiteralDigits (constructor IntegerLiteralRadix IntegerLiteralBinary) (bytes-tail (bytes-tail spelling)))) (lambda unrestricted force : Nat . (parseNaturalLiteralDigits (constructor IntegerLiteralRadix IntegerLiteralDecimal) spelling)))))) (lambda unrestricted force : Nat . (parseNaturalLiteralDigits (constructor IntegerLiteralRadix IntegerLiteralDecimal) spelling)))) def naturalLiteralAsTermValue = (lambda unrestricted result : (family NaturalLiteralParseResult) . (eliminate NaturalLiteralParseResult (lambda unrestricted value : (family NaturalLiteralParseResult) . (family NaturalTermResult)) result (branch NaturalLiteralParsed value . (constructor NaturalTermResult NaturalTermDecoded value)) (branch NaturalLiteralParseFailed failure . (constructor NaturalTermResult NotNaturalTerm)))) def termFromNatural = (lambda unrestricted value : Nat . (constructor Term NaturalLiteral value)) def naturalValueFromTerm = (lambda unrestricted term : (family Term) . (eliminate Term (lambda unrestricted value : (family Term) . (family NaturalTermResult)) term (branch Variable spelling . (constructor NaturalTermResult NotNaturalTerm)) (branch Universe level . (constructor NaturalTermResult NotNaturalTerm)) (branch NaturalType . (constructor NaturalTermResult NotNaturalTerm)) (branch NaturalZero . (constructor NaturalTermResult NaturalTermDecoded zero)) (branch NaturalLiteral naturalLiteralValue . (constructor NaturalTermResult NaturalTermDecoded naturalLiteralValue)) (branch NaturalSuccessor predecessor ih_predecessor . (eliminate NaturalTermResult (lambda unrestricted result : (family NaturalTermResult) . (family NaturalTermResult)) ih_predecessor (branch NaturalTermDecoded naturalTermValue . (constructor NaturalTermResult NaturalTermDecoded (succ naturalTermValue))) (branch NotNaturalTerm . (constructor NaturalTermResult NotNaturalTerm)))) (branch Application function argument ih_function ih_argument . (constructor NaturalTermResult NotNaturalTerm)) (branch NaturalArithmetic operation function argument ih_function ih_argument . (constructor NaturalTermResult NotNaturalTerm)) (branch Lambda quantityTag binderSpelling domain body ih_domain ih_body . (constructor NaturalTermResult NotNaturalTerm)) (branch Pi quantityTag binderSpelling domain codomain ih_domain ih_codomain . (constructor NaturalTermResult NotNaturalTerm)) (branch BytesType . (constructor NaturalTermResult NotNaturalTerm)) (branch BytesLiteral bytesValue . (constructor NaturalTermResult NotNaturalTerm)) (branch ByteType . (constructor NaturalTermResult NotNaturalTerm)) (branch ByteLiteral byteValue . (constructor NaturalTermResult NotNaturalTerm)) (branch TermSequenceEnd . (constructor NaturalTermResult NotNaturalTerm)) (branch TermSequenceNext sequenceHead sequenceTail ih_sequenceHead ih_sequenceTail . (constructor NaturalTermResult NotNaturalTerm)) (branch TermEliminatorBranch constructorSpelling binderNames body ih_binderNames ih_body . (constructor NaturalTermResult NotNaturalTerm)) (branch FamilyApplication familySpelling familyArguments ih_familyArguments . (constructor NaturalTermResult NotNaturalTerm)) (branch ConstructorApplication familySpelling constructorSpelling constructorArguments ih_constructorArguments . (constructor NaturalTermResult NotNaturalTerm)) (branch Eliminator eliminatedFamilySpelling motive scrutinee branches ih_motive ih_scrutinee ih_branches . (constructor NaturalTermResult NotNaturalTerm)) (branch Match family scrutinee branches ih_scrutinee ih_branches . (constructor NaturalTermResult NotNaturalTerm)) (branch MatchWith family motive scrutinee branches ih_motive ih_scrutinee ih_branches . (constructor NaturalTermResult NotNaturalTerm)) (branch IntegerLiteral integerLiteralSpelling . (eliminate DecimalParseResult (lambda unrestricted result : (family DecimalParseResult) . (family NaturalTermResult)) (parseDecimalSpelling integerLiteralSpelling) (branch DecimalParsed value . (constructor NaturalTermResult NaturalTermDecoded value)) (branch DecimalInvalid . (constructor NaturalTermResult NotNaturalTerm)))) (branch RecordConstruction name origin bindings ih_bindings . (constructor NaturalTermResult NotNaturalTerm)) (branch RecordAssignment name origin value ih_value . (constructor NaturalTermResult NotNaturalTerm)) (branch RecordProjection name field origin value ih_value . (constructor NaturalTermResult NotNaturalTerm)) (branch RecordUpdate name origin value bindings ih_value ih_bindings . (constructor NaturalTermResult NotNaturalTerm)) (branch LocalLet quantity binder hasAnnotation annotation value body ih_annotation ih_value ih_body . (constructor NaturalTermResult NotNaturalTerm)) (branch DoBlock effects result body ih_effects ih_result ih_body . (constructor NaturalTermResult NotNaturalTerm)) (branch DoStep named quantity binder computation continuation ih_computation ih_continuation . (constructor NaturalTermResult NotNaturalTerm)) (branch DoReturn value ih_value . (constructor NaturalTermResult NotNaturalTerm)))) def naturalLessThan = (lambda unrestricted left : Nat . (lambda unrestricted right : Nat . (nat-less-than left right))) def naturalOne = (succ zero) def byteModulus = (naturalDouble (naturalDouble (naturalDouble (naturalDouble (naturalDouble (naturalDouble (naturalDouble (naturalDouble naturalOne)))))))) def sourceByteFromTerm = (lambda unrestricted term : (family Term) . (eliminate NaturalTermResult (lambda unrestricted result : (family NaturalTermResult) . (family SourceByteResult)) (naturalValueFromTerm term) (branch NaturalTermDecoded naturalTermValue . (nat-eliminate (lambda unrestricted fits : Nat . (family SourceByteResult)) (constructor SourceByteResult SourceByteInvalid) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SourceByteResult) . (constructor SourceByteResult SourceByteDecoded (nat-to-byte naturalTermValue)))) (naturalLessThan naturalTermValue byteModulus))) (branch NotNaturalTerm . (constructor SourceByteResult SourceByteInvalid)))) def sourceBytesFromTerms = (lambda unrestricted terms : (family TermList) . (eliminate TermList (lambda unrestricted value : (family TermList) . (family SourceBytesResult)) terms (branch TermListEnd . (constructor SourceBytesResult SourceBytesDecoded b"")) (branch TermListNext listedTerm listedRest ih_listedRest . (eliminate SourceByteResult (lambda unrestricted result : (family SourceByteResult) . (family SourceBytesResult)) (sourceByteFromTerm listedTerm) (branch SourceByteDecoded decodedSourceByte . (eliminate SourceBytesResult (lambda unrestricted result : (family SourceBytesResult) . (family SourceBytesResult)) ih_listedRest (branch SourceBytesDecoded decodedSourceBytes . (constructor SourceBytesResult SourceBytesDecoded (bytes-cons decodedSourceByte decodedSourceBytes))) (branch SourceBytesInvalid . (constructor SourceBytesResult SourceBytesInvalid)))) (branch SourceByteInvalid . (constructor SourceBytesResult SourceBytesInvalid)))))) def finishByteLiteral = (lambda unrestricted decodedSourceByte : Byte . (lambda unrestricted remaining : (family TermList) . (eliminate TermList (lambda unrestricted value : (family TermList) . (family TermDecodeResult)) remaining (branch TermListEnd . (constructor TermDecodeResult TermDecoded (constructor Term ByteLiteral decodedSourceByte))) (branch TermListNext listedTerm listedRest ih_listedRest . (constructor TermDecodeResult TermDecodeFailed (succ (succ (succ (succ (succ (succ zero)))))) (constructor SyntaxOrigin SyntaxOriginUnknown)))))) def decodeByteLiteral = (lambda unrestricted argumentTerm : (family Term) . (lambda unrestricted remaining : (family TermList) . (eliminate SourceByteResult (lambda unrestricted result : (family SourceByteResult) . (family TermDecodeResult)) (sourceByteFromTerm argumentTerm) (branch SourceByteDecoded decodedSourceByte . (finishByteLiteral decodedSourceByte remaining)) (branch SourceByteInvalid . (constructor TermDecodeResult TermDecodeFailed (succ (succ (succ (succ (succ (succ (succ (succ zero)))))))) (constructor SyntaxOrigin SyntaxOriginUnknown)))))) -- A bytes expression whose members are all natural literals below 256 is a -- BytesLiteral. Any other member turns the whole expression into a -- bytes-cons application chain over the empty literal, with literal members -- lowered to byte literals -- the same meaning the trusted elaborator gives -- a bytes expression with computed members. def bytesElementTerm = (lambda unrestricted element : (family Term) . (eliminate SourceByteResult (lambda unrestricted result : (family SourceByteResult) . (family Term)) (sourceByteFromTerm element) (branch SourceByteDecoded decodedSourceByte . (constructor Term ByteLiteral decodedSourceByte)) (branch SourceByteInvalid . element))) def bytesElementChain = (lambda unrestricted terms : (family TermList) . (eliminate TermList (lambda unrestricted value : (family TermList) . (family Term)) terms (branch TermListEnd . (constructor Term BytesLiteral b"")) (branch TermListNext listedTerm listedRest ih_listedRest . (constructor Term Application (constructor Term Application (constructor Term Variable bytesConsSpelling) (bytesElementTerm listedTerm)) ih_listedRest)))) def decodeBytesLiteral = (lambda unrestricted firstTerm : (family Term) . (lambda unrestricted remaining : (family TermList) . (eliminate SourceBytesResult (lambda unrestricted result : (family SourceBytesResult) . (family TermDecodeResult)) (sourceBytesFromTerms (constructor TermList TermListNext firstTerm remaining)) (branch SourceBytesDecoded decodedSourceBytes . (constructor TermDecodeResult TermDecoded (constructor Term BytesLiteral decodedSourceBytes))) (branch SourceBytesInvalid . (constructor TermDecodeResult TermDecoded (bytesElementChain (constructor TermList TermListNext firstTerm remaining))))))) -- Delay both alternatives: ordinary compact literals must not be decoded as -- unary universe levels or bytes by a branch whose head did not match. def chooseNamedDecode = (lambda unrestricted matched : Nat . (lambda unrestricted selected : (pi unrestricted force : Nat . (family TermDecodeResult)) . (lambda unrestricted fallback : (pi unrestricted force : Nat . (family TermDecodeResult)) . (app (nat-eliminate (lambda unrestricted value : Nat . (pi unrestricted force : Nat . (family TermDecodeResult))) fallback (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (pi unrestricted force : Nat . (family TermDecodeResult)) . selected)) matched) zero)))) def chooseDecodedAtom = (lambda unrestricted matched : Nat . (lambda unrestricted matchedTerm : (family Term) . (lambda unrestricted fallback : (family TermDecodeResult) . (nat-eliminate (lambda unrestricted value : Nat . (family TermDecodeResult)) fallback (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family TermDecodeResult) . (constructor TermDecodeResult TermDecoded matchedTerm))) matched)))) -- Preserve numeric-looking atoms as raw bytes for expected-type elaboration. -- The lexer already keeps the complete atom spelling, including sign, radix, -- and separators; this only distinguishes numeric candidates from names. def integerSpellingTailStartsDigit = (lambda unrestricted spelling : Bytes . (bytes-eliminate (lambda unrestricted remaining : Bytes . Nat) zero (lambda unrestricted head : Byte . (lambda unrestricted tail : Bytes . (lambda unrestricted ignored : Nat . (isDecimalDigit head)))) spelling)) def integerSpellingLooksNumeric = (lambda unrestricted spelling : Bytes . (bytes-eliminate (lambda unrestricted remaining : Bytes . Nat) zero (lambda unrestricted head : Byte . (lambda unrestricted tail : Bytes . (lambda unrestricted ignored : Nat . (nat-eliminate (lambda unrestricted matchedDigit : Nat . Nat) (nat-eliminate (lambda unrestricted matchedMinus : Nat . Nat) zero (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . (integerSpellingTailStartsDigit tail))) (byte-equal head (byte 45))) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . (succ zero))) (isDecimalDigit head))))) spelling)) def decodeUnquotedAtom = (lambda unrestricted spelling : Bytes . (chooseDecodedAtom (bytesEqual spelling zeroSpelling) (constructor Term NaturalZero) (chooseDecodedAtom (bytesEqual spelling naturalTypeSpelling) (constructor Term NaturalType) (chooseDecodedAtom (bytesEqual spelling bytesTypeSpelling) (constructor Term BytesType) (chooseDecodedAtom (bytesEqual spelling byteTypeSpelling) (constructor Term ByteType) (nat-eliminate (lambda unrestricted matched : Nat . (family TermDecodeResult)) (constructor TermDecodeResult TermDecoded (constructor Term Variable spelling)) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family TermDecodeResult) . (constructor TermDecodeResult TermDecoded (constructor Term IntegerLiteral spelling)))) (integerSpellingLooksNumeric spelling))))))) -- Literal payloads lower to the existing BytesLiteral AST constructor. def decodeQuotedByteAtom = (lambda unrestricted spelling : Bytes . (eliminate QuotedLiteralResult (lambda unrestricted result : (family QuotedLiteralResult) . (family TermDecodeResult)) (Compiler.QuotedLiteral/quotedDecodeByteLiteral spelling) (branch QuotedLiteralDecoded bytes . (constructor TermDecodeResult TermDecoded (constructor Term BytesLiteral bytes))) (branch QuotedLiteralFailed failure offset endOffset . (constructor TermDecodeResult TermDecodeFailed (Compiler.QuotedLiteral/quotedLiteralFailureCode failure) (constructor SyntaxOrigin SyntaxOriginRange offset endOffset))))) def decodeNonTextAtom = (lambda unrestricted spelling : Bytes . (app (nat-eliminate (lambda unrestricted matched : Nat . (pi unrestricted force : Nat . (family TermDecodeResult))) (lambda unrestricted force : Nat . (decodeUnquotedAtom spelling)) (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : (pi unrestricted force : Nat . (family TermDecodeResult)) . (lambda unrestricted force : Nat . (decodeQuotedByteAtom spelling)))) (nat-eliminate (lambda unrestricted isB : Nat . Nat) zero (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : Nat . (byte-equal (bytes-head (bytes-tail spelling)) (byte 34)))) (byte-equal (bytes-head spelling) (byte 98)))) zero)) -- A text literal is the explicit checked constructor, never a trusted Text node. def decodedTextLiteralTerm = (lambda unrestricted payload : Bytes . (constructor Term ConstructorApplication b"StdText" b"StdTextOf" (constructor Term TermSequenceNext (constructor Term BytesLiteral payload) (constructor Term TermSequenceNext (constructor Term Application (constructor Term Application (constructor Term Variable b"refl") (constructor Term FamilyApplication b"StdBool" (constructor Term TermSequenceEnd))) (constructor Term ConstructorApplication b"StdBool" b"StdTrue" (constructor Term TermSequenceEnd))) (constructor Term TermSequenceEnd))))) def decodeQuotedTextAtom = (lambda unrestricted spelling : Bytes . (eliminate QuotedLiteralResult (lambda unrestricted result : (family QuotedLiteralResult) . (family TermDecodeResult)) (Compiler.QuotedLiteral/quotedDecodeTextLiteral spelling) (branch QuotedLiteralDecoded payload . (constructor TermDecodeResult TermDecoded (decodedTextLiteralTerm payload))) (branch QuotedLiteralFailed failure offset endOffset . (constructor TermDecodeResult TermDecodeFailed (Compiler.QuotedLiteral/quotedLiteralFailureCode failure) (constructor SyntaxOrigin SyntaxOriginRange offset endOffset))))) def decodeAtom = (lambda unrestricted spelling : Bytes . (app (nat-eliminate (lambda unrestricted matched : Nat . (pi unrestricted force : Nat . (family TermDecodeResult))) (lambda unrestricted force : Nat . (decodeNonTextAtom spelling)) (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : (pi unrestricted force : Nat . (family TermDecodeResult)) . (lambda unrestricted force : Nat . (decodeQuotedTextAtom spelling)))) (byte-equal (bytes-head spelling) (byte 34))) zero)) def requireNoMoreArguments = (lambda unrestricted resultTerm : (family Term) . (lambda unrestricted remaining : (family TermList) . (eliminate TermList (lambda unrestricted value : (family TermList) . (family TermDecodeResult)) remaining (branch TermListEnd . (constructor TermDecodeResult TermDecoded resultTerm)) (branch TermListNext listedTerm listedRest ih_listedRest . (constructor TermDecodeResult TermDecodeFailed (succ (succ (succ (succ (succ (succ zero)))))) (constructor SyntaxOrigin SyntaxOriginUnknown)))))) def decodeUniverseApplication = (lambda unrestricted levelTerm : (family Term) . (lambda unrestricted remaining : (family TermList) . (eliminate NaturalTermResult (lambda unrestricted value : (family NaturalTermResult) . (family TermDecodeResult)) (naturalValueFromTerm levelTerm) (branch NaturalTermDecoded level . (requireNoMoreArguments (constructor Term Universe level) remaining)) (branch NotNaturalTerm . (constructor TermDecodeResult TermDecodeFailed (succ (succ (succ (succ (succ (succ (succ (succ zero)))))))) (constructor SyntaxOrigin SyntaxOriginUnknown)))))) def foldOrdinaryApplicationTail = (lambda unrestricted remaining : (family TermList) . (eliminate TermList (lambda unrestricted value : (family TermList) . (pi unrestricted accumulator : (family Term) . (family Term))) remaining (branch TermListEnd . (lambda unrestricted accumulator : (family Term) . accumulator)) (branch TermListNext listedTerm listedRest ih_listedRest . (lambda unrestricted accumulator : (family Term) . (ih_listedRest (constructor Term Application accumulator listedTerm)))))) def decodeApplicationTail = (lambda unrestricted functionTerm : (family Term) . (lambda unrestricted remaining : (family TermList) . (eliminate TermList (lambda unrestricted value : (family TermList) . (family TermDecodeResult)) remaining (branch TermListEnd . (constructor TermDecodeResult TermDecodeFailed (succ (succ (succ (succ (succ (succ zero)))))) (constructor SyntaxOrigin SyntaxOriginUnknown))) (branch TermListNext listedTerm listedRest ih_listedRest . (constructor TermDecodeResult TermDecoded (foldOrdinaryApplicationTail listedRest (constructor Term Application functionTerm listedTerm))))))) def decodeOrdinaryHead = (lambda unrestricted functionTerm : (family Term) . (lambda unrestricted argumentTerm : (family Term) . (lambda unrestricted remaining : (family TermList) . (constructor TermDecodeResult TermDecoded (foldOrdinaryApplicationTail remaining (constructor Term Application functionTerm argumentTerm)))))) def termSpelling = (lambda unrestricted term : (family Term) . (eliminate Term (lambda unrestricted value : (family Term) . (family TermSpellingResult)) term (branch Variable spelling . (constructor TermSpellingResult TermSpellingDecoded spelling)) (branch Universe level . (constructor TermSpellingResult TermHasNoSpelling)) (branch NaturalType . (constructor TermSpellingResult TermHasNoSpelling)) (branch NaturalZero . (constructor TermSpellingResult TermHasNoSpelling)) (branch NaturalLiteral naturalLiteralValue . (constructor TermSpellingResult TermHasNoSpelling)) (branch NaturalSuccessor predecessor ih_predecessor . (constructor TermSpellingResult TermHasNoSpelling)) (branch Application function argument ih_function ih_argument . (constructor TermSpellingResult TermHasNoSpelling)) (branch NaturalArithmetic operation function argument ih_function ih_argument . (constructor TermSpellingResult TermHasNoSpelling)) (branch Lambda quantityTag binderSpelling domain body ih_domain ih_body . (constructor TermSpellingResult TermHasNoSpelling)) (branch Pi quantityTag binderSpelling domain codomain ih_domain ih_codomain . (constructor TermSpellingResult TermHasNoSpelling)) (branch BytesType . (constructor TermSpellingResult TermHasNoSpelling)) (branch BytesLiteral bytesValue . (constructor TermSpellingResult TermHasNoSpelling)) (branch ByteType . (constructor TermSpellingResult TermHasNoSpelling)) (branch ByteLiteral byteValue . (constructor TermSpellingResult TermHasNoSpelling)) (branch TermSequenceEnd . (constructor TermSpellingResult TermHasNoSpelling)) (branch TermSequenceNext sequenceHead sequenceTail ih_sequenceHead ih_sequenceTail . (constructor TermSpellingResult TermHasNoSpelling)) (branch TermEliminatorBranch constructorSpelling binderNames body ih_binderNames ih_body . (constructor TermSpellingResult TermHasNoSpelling)) (branch FamilyApplication familySpelling familyArguments ih_familyArguments . (constructor TermSpellingResult TermHasNoSpelling)) (branch ConstructorApplication familySpelling constructorSpelling constructorArguments ih_constructorArguments . (constructor TermSpellingResult TermHasNoSpelling)) (branch Eliminator eliminatedFamilySpelling motive scrutinee branches ih_motive ih_scrutinee ih_branches . (constructor TermSpellingResult TermHasNoSpelling)) (branch Match family scrutinee branches ih_scrutinee ih_branches . (constructor TermSpellingResult TermHasNoSpelling)) (branch MatchWith family motive scrutinee branches ih_motive ih_scrutinee ih_branches . (constructor TermSpellingResult TermHasNoSpelling)) (branch IntegerLiteral integerLiteralSpelling . (constructor TermSpellingResult TermHasNoSpelling)) (branch RecordConstruction name origin bindings ih_bindings . (constructor TermSpellingResult TermHasNoSpelling)) (branch RecordAssignment name origin value ih_value . (constructor TermSpellingResult TermHasNoSpelling)) (branch RecordProjection name field origin value ih_value . (constructor TermSpellingResult TermHasNoSpelling)) (branch RecordUpdate name origin value bindings ih_value ih_bindings . (constructor TermSpellingResult TermHasNoSpelling)) (branch LocalLet quantity binder hasAnnotation annotation value body ih_annotation ih_value ih_body . (constructor TermSpellingResult TermHasNoSpelling)) (branch DoBlock effects result body ih_effects ih_result ih_body . (constructor TermSpellingResult TermHasNoSpelling)) (branch DoStep named quantity binder computation continuation ih_computation ih_continuation . (constructor TermSpellingResult TermHasNoSpelling)) (branch DoReturn value ih_value . (constructor TermSpellingResult TermHasNoSpelling)))) def chooseQuantityDecode = (lambda unrestricted matched : Nat . (lambda unrestricted quantityTag : Nat . (lambda unrestricted fallback : (family QuantityDecodeResult) . (nat-eliminate (lambda unrestricted value : Nat . (family QuantityDecodeResult)) fallback (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family QuantityDecodeResult) . (constructor QuantityDecodeResult QuantityDecoded quantityTag))) matched)))) def decodeQuantitySpelling = (lambda unrestricted spelling : Bytes . (chooseQuantityDecode (bytesEqual spelling erasedSpelling) zero (chooseQuantityDecode (bytesEqual spelling linearSpelling) (succ zero) (chooseQuantityDecode (bytesEqual spelling affineSpelling) (succ (succ zero)) (chooseQuantityDecode (bytesEqual spelling unrestrictedSpelling) (succ (succ (succ zero))) (constructor QuantityDecodeResult QuantityInvalid)))))) def appendTermListOne = (lambda unrestricted terms : (family TermList) . (lambda unrestricted term : (family Term) . (eliminate TermList (lambda unrestricted value : (family TermList) . (family TermList)) terms (branch TermListEnd . (constructor TermList TermListNext term (constructor TermList TermListEnd))) (branch TermListNext head tail ih_tail . (constructor TermList TermListNext head ih_tail))))) def appendSpineArgument = (lambda unrestricted spine : (family TermApplicationSpine) . (lambda unrestricted argument : (family Term) . (eliminate TermApplicationSpine (lambda unrestricted value : (family TermApplicationSpine) . (family TermApplicationSpine)) spine (branch TermApplicationSpineValue head arguments . (constructor TermApplicationSpine TermApplicationSpineValue head (appendTermListOne arguments argument)))))) def termApplicationSpine = (lambda unrestricted term : (family Term) . (eliminate Term (lambda unrestricted value : (family Term) . (family TermApplicationSpine)) term (branch Variable spelling . (constructor TermApplicationSpine TermApplicationSpineValue (constructor Term Variable spelling) (constructor TermList TermListEnd))) (branch Universe level . (constructor TermApplicationSpine TermApplicationSpineValue (constructor Term Universe level) (constructor TermList TermListEnd))) (branch NaturalType . (constructor TermApplicationSpine TermApplicationSpineValue (constructor Term NaturalType) (constructor TermList TermListEnd))) (branch NaturalZero . (constructor TermApplicationSpine TermApplicationSpineValue (constructor Term NaturalZero) (constructor TermList TermListEnd))) (branch NaturalLiteral value . (constructor TermApplicationSpine TermApplicationSpineValue (constructor Term NaturalLiteral value) (constructor TermList TermListEnd))) (branch NaturalSuccessor predecessor ih . (constructor TermApplicationSpine TermApplicationSpineValue (constructor Term NaturalSuccessor predecessor) (constructor TermList TermListEnd))) (branch Application function argument ih_function ih_argument . (appendSpineArgument ih_function argument)) (branch NaturalArithmetic operation function argument ih_function ih_argument . (constructor TermApplicationSpine TermApplicationSpineValue (constructor Term NaturalArithmetic operation function argument) (constructor TermList TermListEnd))) (branch Lambda quantity binder domain body ih_domain ih_body . (constructor TermApplicationSpine TermApplicationSpineValue (constructor Term Lambda quantity binder domain body) (constructor TermList TermListEnd))) (branch Pi quantity binder domain body ih_domain ih_body . (constructor TermApplicationSpine TermApplicationSpineValue (constructor Term Pi quantity binder domain body) (constructor TermList TermListEnd))) (branch BytesType . (constructor TermApplicationSpine TermApplicationSpineValue (constructor Term BytesType) (constructor TermList TermListEnd))) (branch BytesLiteral value . (constructor TermApplicationSpine TermApplicationSpineValue (constructor Term BytesLiteral value) (constructor TermList TermListEnd))) (branch ByteType . (constructor TermApplicationSpine TermApplicationSpineValue (constructor Term ByteType) (constructor TermList TermListEnd))) (branch ByteLiteral value . (constructor TermApplicationSpine TermApplicationSpineValue (constructor Term ByteLiteral value) (constructor TermList TermListEnd))) (branch TermSequenceEnd . (constructor TermApplicationSpine TermApplicationSpineValue (constructor Term TermSequenceEnd) (constructor TermList TermListEnd))) (branch TermSequenceNext head tail ih_head ih_tail . (constructor TermApplicationSpine TermApplicationSpineValue (constructor Term TermSequenceNext head tail) (constructor TermList TermListEnd))) (branch TermEliminatorBranch constructor binders body ih_binders ih_body . (constructor TermApplicationSpine TermApplicationSpineValue (constructor Term TermEliminatorBranch constructor binders body) (constructor TermList TermListEnd))) (branch FamilyApplication family arguments ih_arguments . (constructor TermApplicationSpine TermApplicationSpineValue (constructor Term FamilyApplication family arguments) (constructor TermList TermListEnd))) (branch ConstructorApplication family constructor arguments ih_arguments . (constructor TermApplicationSpine TermApplicationSpineValue (constructor Term ConstructorApplication family constructor arguments) (constructor TermList TermListEnd))) (branch Eliminator family motive scrutinee branches ih_motive ih_scrutinee ih_branches . (constructor TermApplicationSpine TermApplicationSpineValue (constructor Term Eliminator family motive scrutinee branches) (constructor TermList TermListEnd))) (branch Match family scrutinee branches ih_scrutinee ih_branches . (constructor TermApplicationSpine TermApplicationSpineValue (constructor Term Match family scrutinee branches) (constructor TermList TermListEnd))) (branch MatchWith family motive scrutinee branches ih_motive ih_scrutinee ih_branches . (constructor TermApplicationSpine TermApplicationSpineValue (constructor Term MatchWith family motive scrutinee branches) (constructor TermList TermListEnd))) (branch IntegerLiteral spelling . (constructor TermApplicationSpine TermApplicationSpineValue (constructor Term IntegerLiteral spelling) (constructor TermList TermListEnd))) (branch RecordConstruction name origin bindings ih_bindings . (constructor TermApplicationSpine TermApplicationSpineValue (constructor Term RecordConstruction name origin bindings) (constructor TermList TermListEnd))) (branch RecordAssignment name origin value ih_value . (constructor TermApplicationSpine TermApplicationSpineValue (constructor Term RecordAssignment name origin value) (constructor TermList TermListEnd))) (branch RecordProjection name field origin value ih_value . (constructor TermApplicationSpine TermApplicationSpineValue (constructor Term RecordProjection name field origin value) (constructor TermList TermListEnd))) (branch RecordUpdate name origin value bindings ih_value ih_bindings . (constructor TermApplicationSpine TermApplicationSpineValue (constructor Term RecordUpdate name origin value bindings) (constructor TermList TermListEnd))) (branch LocalLet quantity binder hasAnnotation annotation value body ih_annotation ih_value ih_body . (constructor TermApplicationSpine TermApplicationSpineValue (constructor Term LocalLet quantity binder hasAnnotation annotation value body) (constructor TermList TermListEnd))) (branch DoBlock effects result body ih_effects ih_result ih_body . (constructor TermApplicationSpine TermApplicationSpineValue (constructor Term DoBlock effects result body) (constructor TermList TermListEnd))) (branch DoStep named quantity binder computation continuation ih_computation ih_continuation . (constructor TermApplicationSpine TermApplicationSpineValue (constructor Term DoStep named quantity binder computation continuation) (constructor TermList TermListEnd))) (branch DoReturn value ih_value . (constructor TermApplicationSpine TermApplicationSpineValue (constructor Term DoReturn value) (constructor TermList TermListEnd))))) def decodeLocalLetAnnotatedTail = (lambda unrestricted quantity : Nat . (lambda unrestricted binder : Bytes . (lambda unrestricted terms : (family TermList) . (eliminate TermList (lambda unrestricted value : (family TermList) . (family LocalLetBindingDecodeResult)) terms (branch TermListEnd . (constructor LocalLetBindingDecodeResult LocalLetBindingDecodeFailed)) (branch TermListNext annotation afterAnnotation ih_afterAnnotation . (eliminate TermList (lambda unrestricted value : (family TermList) . (family LocalLetBindingDecodeResult)) afterAnnotation (branch TermListEnd . (constructor LocalLetBindingDecodeResult LocalLetBindingDecodeFailed)) (branch TermListNext equalsTerm afterEquals ih_afterEquals . (eliminate TermSpellingResult (lambda unrestricted result : (family TermSpellingResult) . (family LocalLetBindingDecodeResult)) (termSpelling equalsTerm) (branch TermSpellingDecoded spelling . (nat-eliminate (lambda unrestricted matched : Nat . (family LocalLetBindingDecodeResult)) (constructor LocalLetBindingDecodeResult LocalLetBindingDecodeFailed) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family LocalLetBindingDecodeResult) . (eliminate TermList (lambda unrestricted value : (family TermList) . (family LocalLetBindingDecodeResult)) afterEquals (branch TermListEnd . (constructor LocalLetBindingDecodeResult LocalLetBindingDecodeFailed)) (branch TermListNext value rest ih_rest . (eliminate TermList (lambda unrestricted value : (family TermList) . (family LocalLetBindingDecodeResult)) rest (branch TermListEnd . (constructor LocalLetBindingDecodeResult LocalLetBindingDecoded quantity binder (succ zero) annotation value)) (branch TermListNext extra tail ih_tail . (constructor LocalLetBindingDecodeResult LocalLetBindingDecodeFailed))))))) (bytesEqual spelling equalsSpelling))) (branch TermHasNoSpelling . (constructor LocalLetBindingDecodeResult LocalLetBindingDecodeFailed)))))))))) def decodeLocalLetInferredTail = (lambda unrestricted quantity : Nat . (lambda unrestricted binder : Bytes . (lambda unrestricted terms : (family TermList) . (eliminate TermList (lambda unrestricted value : (family TermList) . (family LocalLetBindingDecodeResult)) terms (branch TermListEnd . (constructor LocalLetBindingDecodeResult LocalLetBindingDecodeFailed)) (branch TermListNext value rest ih_rest . (eliminate TermList (lambda unrestricted value : (family TermList) . (family LocalLetBindingDecodeResult)) rest (branch TermListEnd . (constructor LocalLetBindingDecodeResult LocalLetBindingDecoded quantity binder zero (constructor Term NaturalType) value)) (branch TermListNext extra tail ih_tail . (constructor LocalLetBindingDecodeResult LocalLetBindingDecodeFailed)))))))) def decodeLocalLetBindingTail = (lambda unrestricted quantity : Nat . (lambda unrestricted binder : Bytes . (lambda unrestricted punctuation : Bytes . (lambda unrestricted terms : (family TermList) . (nat-eliminate (lambda unrestricted matched : Nat . (family LocalLetBindingDecodeResult)) (nat-eliminate (lambda unrestricted matchedColon : Nat . (family LocalLetBindingDecodeResult)) (constructor LocalLetBindingDecodeResult LocalLetBindingDecodeFailed) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family LocalLetBindingDecodeResult) . (decodeLocalLetAnnotatedTail quantity binder terms))) (bytesEqual punctuation colonSpelling)) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family LocalLetBindingDecodeResult) . (decodeLocalLetInferredTail quantity binder terms))) (bytesEqual punctuation equalsSpelling)))))) def decodeLocalLetBindingArguments = (lambda unrestricted quantity : Nat . (lambda unrestricted arguments : (family TermList) . (eliminate TermList (lambda unrestricted value : (family TermList) . (family LocalLetBindingDecodeResult)) arguments (branch TermListEnd . (constructor LocalLetBindingDecodeResult LocalLetBindingDecodeFailed)) (branch TermListNext binderTerm afterBinder ih_afterBinder . (eliminate TermSpellingResult (lambda unrestricted result : (family TermSpellingResult) . (family LocalLetBindingDecodeResult)) (termSpelling binderTerm) (branch TermSpellingDecoded binder . (eliminate TermList (lambda unrestricted value : (family TermList) . (family LocalLetBindingDecodeResult)) afterBinder (branch TermListEnd . (constructor LocalLetBindingDecodeResult LocalLetBindingDecodeFailed)) (branch TermListNext punctuationTerm terms ih_terms . (eliminate TermSpellingResult (lambda unrestricted result : (family TermSpellingResult) . (family LocalLetBindingDecodeResult)) (termSpelling punctuationTerm) (branch TermSpellingDecoded punctuation . (decodeLocalLetBindingTail quantity binder punctuation terms)) (branch TermHasNoSpelling . (constructor LocalLetBindingDecodeResult LocalLetBindingDecodeFailed)))))) (branch TermHasNoSpelling . (constructor LocalLetBindingDecodeResult LocalLetBindingDecodeFailed))))))) def decodeLocalLetBinding = (lambda unrestricted term : (family Term) . (eliminate TermApplicationSpine (lambda unrestricted value : (family TermApplicationSpine) . (family LocalLetBindingDecodeResult)) (termApplicationSpine term) (branch TermApplicationSpineValue head arguments . (eliminate TermSpellingResult (lambda unrestricted result : (family TermSpellingResult) . (family LocalLetBindingDecodeResult)) (termSpelling head) (branch TermSpellingDecoded quantitySpelling . (eliminate QuantityDecodeResult (lambda unrestricted result : (family QuantityDecodeResult) . (family LocalLetBindingDecodeResult)) (decodeQuantitySpelling quantitySpelling) (branch QuantityDecoded quantity . (decodeLocalLetBindingArguments quantity arguments)) (branch QuantityInvalid . (constructor LocalLetBindingDecodeResult LocalLetBindingDecodeFailed)))) (branch TermHasNoSpelling . (constructor LocalLetBindingDecodeResult LocalLetBindingDecodeFailed)))))) def localLetSyntaxFailure = (constructor TermDecodeResult TermDecodeFailed (byte-to-nat (byte 27)) (constructor SyntaxOrigin SyntaxOriginUnknown)) def decodeLocalLetAfterIn = (lambda unrestricted terms : (family TermList) . (eliminate TermList (lambda unrestricted value : (family TermList) . (family TermDecodeResult)) terms (branch TermListEnd . localLetSyntaxFailure) (branch TermListNext body rest ih_rest . (eliminate TermList (lambda unrestricted value : (family TermList) . (family TermDecodeResult)) rest (branch TermListEnd . (constructor TermDecodeResult TermDecoded body)) (branch TermListNext extra tail ih_tail . localLetSyntaxFailure))))) def finishDecodedLocalLetBinding = (lambda unrestricted tailResult : (family TermDecodeResult) . (lambda unrestricted bindingResult : (family LocalLetBindingDecodeResult) . (eliminate LocalLetBindingDecodeResult (lambda unrestricted value : (family LocalLetBindingDecodeResult) . (family TermDecodeResult)) bindingResult (branch LocalLetBindingDecoded quantity binder hasAnnotation annotation value . (eliminate TermDecodeResult (lambda unrestricted result : (family TermDecodeResult) . (family TermDecodeResult)) tailResult (branch TermDecoded body . (constructor TermDecodeResult TermDecoded (constructor Term LocalLet quantity binder hasAnnotation annotation value body))) (branch TermsDecoded terms . localLetSyntaxFailure) (branch TermDecodeFailed code origin . (constructor TermDecodeResult TermDecodeFailed code origin)))) (branch LocalLetBindingDecodeFailed . localLetSyntaxFailure)))) def decodeLocalLetSequence = (lambda unrestricted terms : (family TermList) . (eliminate TermList (lambda unrestricted value : (family TermList) . (family TermDecodeResult)) terms (branch TermListEnd . localLetSyntaxFailure) (branch TermListNext head rest ih_rest . (eliminate TermSpellingResult (lambda unrestricted result : (family TermSpellingResult) . (family TermDecodeResult)) (termSpelling head) (branch TermSpellingDecoded spelling . (nat-eliminate (lambda unrestricted matched : Nat . (family TermDecodeResult)) (finishDecodedLocalLetBinding ih_rest (decodeLocalLetBinding head)) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family TermDecodeResult) . (decodeLocalLetAfterIn rest))) (bytesEqual spelling inSpelling))) (branch TermHasNoSpelling . (finishDecodedLocalLetBinding ih_rest (decodeLocalLetBinding head))))))) def decodeDoReturnArguments = (lambda unrestricted arguments : (family TermList) . (eliminate TermList (lambda unrestricted value : (family TermList) . (family DoBodyDecodeResult)) arguments (branch TermListEnd . (constructor DoBodyDecodeResult DoBodyDecodeFailed)) (branch TermListNext finalValue rest ih_rest . (eliminate TermList (lambda unrestricted value : (family TermList) . (family DoBodyDecodeResult)) rest (branch TermListEnd . (constructor DoBodyDecodeResult DoBodyDecoded (constructor Term DoReturn finalValue))) (branch TermListNext extra tail ih_tail . (constructor DoBodyDecodeResult DoBodyDecodeFailed)))))) def decodeDoReturn = (lambda unrestricted term : (family Term) . (eliminate TermApplicationSpine (lambda unrestricted value : (family TermApplicationSpine) . (family DoBodyDecodeResult)) (termApplicationSpine term) (branch TermApplicationSpineValue head arguments . (eliminate TermSpellingResult (lambda unrestricted result : (family TermSpellingResult) . (family DoBodyDecodeResult)) (termSpelling head) (branch TermSpellingDecoded spelling . (nat-eliminate (lambda unrestricted matched : Nat . (family DoBodyDecodeResult)) (constructor DoBodyDecodeResult DoBodyDecodeFailed) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family DoBodyDecodeResult) . (decodeDoReturnArguments arguments))) (bytesEqual spelling returnSpelling))) (branch TermHasNoSpelling . (constructor DoBodyDecodeResult DoBodyDecodeFailed)))))) def decodeDoNamedTail = (lambda unrestricted quantity : Nat . (lambda unrestricted binder : Bytes . (lambda unrestricted arguments : (family TermList) . (eliminate TermList (lambda unrestricted value : (family TermList) . (family DoStepDecodeResult)) arguments (branch TermListEnd . (constructor DoStepDecodeResult DoStepDecodeFailed)) (branch TermListNext arrowTerm afterArrow ih_afterArrow . (eliminate TermSpellingResult (lambda unrestricted result : (family TermSpellingResult) . (family DoStepDecodeResult)) (termSpelling arrowTerm) (branch TermSpellingDecoded arrow . (nat-eliminate (lambda unrestricted matched : Nat . (family DoStepDecodeResult)) (constructor DoStepDecodeResult DoStepDecodeFailed) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family DoStepDecodeResult) . (eliminate TermList (lambda unrestricted value : (family TermList) . (family DoStepDecodeResult)) afterArrow (branch TermListEnd . (constructor DoStepDecodeResult DoStepDecodeFailed)) (branch TermListNext computation rest ih_rest . (eliminate TermList (lambda unrestricted value : (family TermList) . (family DoStepDecodeResult)) rest (branch TermListEnd . (constructor DoStepDecodeResult DoStepDecoded (succ zero) quantity binder computation)) (branch TermListNext extra tail ih_tail . (constructor DoStepDecodeResult DoStepDecodeFailed))))))) (bytesEqual arrow leftArrowSpelling))) (branch TermHasNoSpelling . (constructor DoStepDecodeResult DoStepDecodeFailed)))))))) def decodeDoLongNamed = (lambda unrestricted quantity : Nat . (lambda unrestricted arguments : (family TermList) . (eliminate TermList (lambda unrestricted value : (family TermList) . (family DoStepDecodeResult)) arguments (branch TermListEnd . (constructor DoStepDecodeResult DoStepDecodeFailed)) (branch TermListNext binderTerm rest ih_rest . (eliminate TermSpellingResult (lambda unrestricted result : (family TermSpellingResult) . (family DoStepDecodeResult)) (termSpelling binderTerm) (branch TermSpellingDecoded binder . (decodeDoNamedTail quantity binder rest)) (branch TermHasNoSpelling . (constructor DoStepDecodeResult DoStepDecodeFailed))))))) def chooseDecodedDoStep = (lambda unrestricted original : (family Term) . (lambda unrestricted preferred : (family DoStepDecodeResult) . (eliminate DoStepDecodeResult (lambda unrestricted value : (family DoStepDecodeResult) . (family DoStepDecodeResult)) preferred (branch DoStepDecoded named quantity binder computation . preferred) (branch DoStepDecodeFailed . (constructor DoStepDecodeResult DoStepDecoded zero (succ (succ (succ zero))) b"" original))))) def decodeDoStep = (lambda unrestricted term : (family Term) . (eliminate TermApplicationSpine (lambda unrestricted value : (family TermApplicationSpine) . (family DoStepDecodeResult)) (termApplicationSpine term) (branch TermApplicationSpineValue head arguments . (eliminate TermSpellingResult (lambda unrestricted result : (family TermSpellingResult) . (family DoStepDecodeResult)) (termSpelling head) (branch TermSpellingDecoded headSpelling . (chooseDecodedDoStep term (eliminate QuantityDecodeResult (lambda unrestricted result : (family QuantityDecodeResult) . (family DoStepDecodeResult)) (decodeQuantitySpelling headSpelling) (branch QuantityDecoded quantity . (decodeDoLongNamed quantity arguments)) (branch QuantityInvalid . (decodeDoNamedTail (succ (succ (succ zero))) headSpelling arguments))))) (branch TermHasNoSpelling . (constructor DoStepDecodeResult DoStepDecoded zero (succ (succ (succ zero))) b"" term)))))) def prependDoStep = (lambda unrestricted step : (family Term) . (lambda unrestricted tailResult : (family DoBodyDecodeResult) . (eliminate DoBodyDecodeResult (lambda unrestricted result : (family DoBodyDecodeResult) . (family DoBodyDecodeResult)) tailResult (branch DoBodyDecoded continuation . (eliminate DoStepDecodeResult (lambda unrestricted decoded : (family DoStepDecodeResult) . (family DoBodyDecodeResult)) (decodeDoStep step) (branch DoStepDecoded named quantity binder computation . (constructor DoBodyDecodeResult DoBodyDecoded (constructor Term DoStep named quantity binder computation continuation))) (branch DoStepDecodeFailed . (constructor DoBodyDecodeResult DoBodyDecodeFailed)))) (branch DoBodyDecodeFailed . (constructor DoBodyDecodeResult DoBodyDecodeFailed))))) def decodeDoBody = (lambda unrestricted terms : (family TermList) . (eliminate TermList (lambda unrestricted value : (family TermList) . (family DoBodyDecodeResult)) terms (branch TermListEnd . (constructor DoBodyDecodeResult DoBodyDecodeFailed)) (branch TermListNext head rest ih_rest . (eliminate TermList (lambda unrestricted value : (family TermList) . (family DoBodyDecodeResult)) rest (branch TermListEnd . (decodeDoReturn head)) (branch TermListNext next tail ih_tail . (prependDoStep head ih_rest)))))) def decodeDoApplication = (lambda unrestricted effects : (family Term) . (lambda unrestricted remaining : (family TermList) . (eliminate TermList (lambda unrestricted value : (family TermList) . (family TermDecodeResult)) remaining (branch TermListEnd . localLetSyntaxFailure) (branch TermListNext result bodyTerms ih_bodyTerms . (eliminate DoBodyDecodeResult (lambda unrestricted decoded : (family DoBodyDecodeResult) . (family TermDecodeResult)) (decodeDoBody bodyTerms) (branch DoBodyDecoded body . (constructor TermDecodeResult TermDecoded (constructor Term DoBlock effects result body))) (branch DoBodyDecodeFailed . localLetSyntaxFailure)))))) def binderDecodeFailed = (lambda unrestricted code : Nat . (constructor TermDecodeResult TermDecodeFailed code (constructor SyntaxOrigin SyntaxOriginUnknown))) def binderSyntaxFailureCode = (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ zero))))))))))))) def finishBinderForm = (lambda unrestricted formTag : Nat . (lambda unrestricted quantityTag : Nat . (lambda unrestricted binderSpelling : Bytes . (lambda unrestricted domain : (family Term) . (lambda unrestricted body : (family Term) . (lambda unrestricted remaining : (family TermList) . (eliminate TermList (lambda unrestricted value : (family TermList) . (family TermDecodeResult)) remaining (branch TermListEnd . (nat-eliminate (lambda unrestricted value : Nat . (family TermDecodeResult)) (constructor TermDecodeResult TermDecoded (constructor Term Lambda quantityTag binderSpelling domain body)) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family TermDecodeResult) . (constructor TermDecodeResult TermDecoded (constructor Term Pi quantityTag binderSpelling domain body)))) formTag)) (branch TermListNext listedTerm listedRest ih_listedRest . (binderDecodeFailed binderSyntaxFailureCode))))))))) def decodeBinderAfterDot = (lambda unrestricted formTag : Nat . (lambda unrestricted quantityTag : Nat . (lambda unrestricted binderSpelling : Bytes . (lambda unrestricted domain : (family Term) . (lambda unrestricted remaining : (family TermList) . (eliminate TermList (lambda unrestricted value : (family TermList) . (family TermDecodeResult)) remaining (branch TermListEnd . (binderDecodeFailed binderSyntaxFailureCode)) (branch TermListNext body bodyRest ih_bodyRest . (finishBinderForm formTag quantityTag binderSpelling domain body bodyRest)))))))) def decodeBinderAfterDomain = (lambda unrestricted formTag : Nat . (lambda unrestricted quantityTag : Nat . (lambda unrestricted binderSpelling : Bytes . (lambda unrestricted domain : (family Term) . (lambda unrestricted remaining : (family TermList) . (eliminate TermList (lambda unrestricted value : (family TermList) . (family TermDecodeResult)) remaining (branch TermListEnd . (binderDecodeFailed binderSyntaxFailureCode)) (branch TermListNext dotTerm afterDot ih_afterDot . (eliminate TermSpellingResult (lambda unrestricted result : (family TermSpellingResult) . (family TermDecodeResult)) (termSpelling dotTerm) (branch TermSpellingDecoded punctuationSpelling . (nat-eliminate (lambda unrestricted matched : Nat . (family TermDecodeResult)) (binderDecodeFailed binderSyntaxFailureCode) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family TermDecodeResult) . (decodeBinderAfterDot formTag quantityTag binderSpelling domain afterDot))) (bytesEqual punctuationSpelling dotSpelling))) (branch TermHasNoSpelling . (binderDecodeFailed binderSyntaxFailureCode)))))))))) def decodeBinderAfterColon = (lambda unrestricted formTag : Nat . (lambda unrestricted quantityTag : Nat . (lambda unrestricted binderSpelling : Bytes . (lambda unrestricted remaining : (family TermList) . (eliminate TermList (lambda unrestricted value : (family TermList) . (family TermDecodeResult)) remaining (branch TermListEnd . (binderDecodeFailed binderSyntaxFailureCode)) (branch TermListNext domain afterDomain ih_afterDomain . (decodeBinderAfterDomain formTag quantityTag binderSpelling domain afterDomain))))))) def decodeBinderAfterName = (lambda unrestricted formTag : Nat . (lambda unrestricted quantityTag : Nat . (lambda unrestricted binderSpelling : Bytes . (lambda unrestricted remaining : (family TermList) . (eliminate TermList (lambda unrestricted value : (family TermList) . (family TermDecodeResult)) remaining (branch TermListEnd . (binderDecodeFailed binderSyntaxFailureCode)) (branch TermListNext colonTerm afterColon ih_afterColon . (eliminate TermSpellingResult (lambda unrestricted result : (family TermSpellingResult) . (family TermDecodeResult)) (termSpelling colonTerm) (branch TermSpellingDecoded punctuationSpelling . (nat-eliminate (lambda unrestricted matched : Nat . (family TermDecodeResult)) (binderDecodeFailed binderSyntaxFailureCode) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family TermDecodeResult) . (decodeBinderAfterColon formTag quantityTag binderSpelling afterColon))) (bytesEqual punctuationSpelling colonSpelling))) (branch TermHasNoSpelling . (binderDecodeFailed binderSyntaxFailureCode))))))))) def decodeBinderQuantity = (lambda unrestricted formTag : Nat . (lambda unrestricted quantityResult : (family QuantityDecodeResult) . (lambda unrestricted remaining : (family TermList) . (eliminate QuantityDecodeResult (lambda unrestricted result : (family QuantityDecodeResult) . (family TermDecodeResult)) quantityResult (branch QuantityDecoded quantityTag . (eliminate TermList (lambda unrestricted value : (family TermList) . (family TermDecodeResult)) remaining (branch TermListEnd . (binderDecodeFailed binderSyntaxFailureCode)) (branch TermListNext binderTerm afterName ih_afterName . (eliminate TermSpellingResult (lambda unrestricted result : (family TermSpellingResult) . (family TermDecodeResult)) (termSpelling binderTerm) (branch TermSpellingDecoded binderSpelling . (decodeBinderAfterName formTag quantityTag binderSpelling afterName)) (branch TermHasNoSpelling . (binderDecodeFailed binderSyntaxFailureCode)))))) (branch QuantityInvalid . (binderDecodeFailed binderSyntaxFailureCode)))))) def decodeBinderForm = (lambda unrestricted formTag : Nat . (lambda unrestricted quantityTerm : (family Term) . (lambda unrestricted remaining : (family TermList) . (eliminate TermSpellingResult (lambda unrestricted result : (family TermSpellingResult) . (family TermDecodeResult)) (termSpelling quantityTerm) (branch TermSpellingDecoded quantitySpelling . (decodeBinderQuantity formTag (decodeQuantitySpelling quantitySpelling) remaining)) (branch TermHasNoSpelling . (binderDecodeFailed binderSyntaxFailureCode)))))) def familyTermSyntaxFailureCode = (succ binderSyntaxFailureCode) def familyTermDecodeFailed = (constructor TermDecodeResult TermDecodeFailed familyTermSyntaxFailureCode (constructor SyntaxOrigin SyntaxOriginUnknown)) def termListToTermSequence = (lambda unrestricted terms : (family TermList) . (eliminate TermList (lambda unrestricted value : (family TermList) . (family Term)) terms (branch TermListEnd . (constructor Term TermSequenceEnd)) (branch TermListNext listedTerm listedRest ih_listedRest . (constructor Term TermSequenceNext listedTerm ih_listedRest)))) def decodeFamilyApplication = (lambda unrestricted familyTerm : (family Term) . (lambda unrestricted arguments : (family TermList) . (eliminate TermSpellingResult (lambda unrestricted result : (family TermSpellingResult) . (family TermDecodeResult)) (termSpelling familyTerm) (branch TermSpellingDecoded familyName . (constructor TermDecodeResult TermDecoded (constructor Term FamilyApplication familyName (termListToTermSequence arguments)))) (branch TermHasNoSpelling . familyTermDecodeFailed)))) def decodeConstructorApplication = (lambda unrestricted familyTerm : (family Term) . (lambda unrestricted remaining : (family TermList) . (eliminate TermSpellingResult (lambda unrestricted result : (family TermSpellingResult) . (family TermDecodeResult)) (termSpelling familyTerm) (branch TermSpellingDecoded familyName . (eliminate TermList (lambda unrestricted value : (family TermList) . (family TermDecodeResult)) remaining (branch TermListEnd . familyTermDecodeFailed) (branch TermListNext constructorTerm arguments ih_arguments . (eliminate TermSpellingResult (lambda unrestricted result : (family TermSpellingResult) . (family TermDecodeResult)) (termSpelling constructorTerm) (branch TermSpellingDecoded constructorName . (constructor TermDecodeResult TermDecoded (constructor Term ConstructorApplication familyName constructorName (termListToTermSequence arguments)))) (branch TermHasNoSpelling . familyTermDecodeFailed))))) (branch TermHasNoSpelling . familyTermDecodeFailed)))) def finishTermEliminatorBranch = (lambda unrestricted constructorName : Bytes . (lambda unrestricted reversedBinders : (family Term) . (lambda unrestricted remaining : (family TermList) . (eliminate TermList (lambda unrestricted value : (family TermList) . (family TermDecodeResult)) remaining (branch TermListEnd . familyTermDecodeFailed) (branch TermListNext body afterBody ih_afterBody . (eliminate TermList (lambda unrestricted value : (family TermList) . (family TermDecodeResult)) afterBody (branch TermListEnd . (constructor TermDecodeResult TermDecoded (constructor Term TermEliminatorBranch constructorName reversedBinders body))) (branch TermListNext extra afterExtra ih_afterExtra . familyTermDecodeFailed))))))) def decodeTermEliminatorBranchMembers = (lambda unrestricted members : (family TermList) . (eliminate TermList (lambda unrestricted value : (family TermList) . (pi unrestricted constructorName : Bytes . (pi unrestricted reversedBinders : (family Term) . (family TermDecodeResult)))) members (branch TermListEnd . (lambda unrestricted constructorName : Bytes . (lambda unrestricted reversedBinders : (family Term) . familyTermDecodeFailed))) (branch TermListNext member remaining ih_remaining . (lambda unrestricted constructorName : Bytes . (lambda unrestricted reversedBinders : (family Term) . (eliminate TermSpellingResult (lambda unrestricted result : (family TermSpellingResult) . (family TermDecodeResult)) (termSpelling member) (branch TermSpellingDecoded spelling . (nat-eliminate (lambda unrestricted matchedDot : Nat . (family TermDecodeResult)) (ih_remaining constructorName (constructor Term TermSequenceNext member reversedBinders)) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family TermDecodeResult) . (finishTermEliminatorBranch constructorName reversedBinders remaining))) (bytesEqual spelling dotSpelling))) (branch TermHasNoSpelling . familyTermDecodeFailed))))))) def decodeTermEliminatorBranch = (lambda unrestricted constructorTerm : (family Term) . (lambda unrestricted remaining : (family TermList) . (eliminate TermSpellingResult (lambda unrestricted result : (family TermSpellingResult) . (family TermDecodeResult)) (termSpelling constructorTerm) (branch TermSpellingDecoded constructorName . (decodeTermEliminatorBranchMembers remaining constructorName (constructor Term TermSequenceEnd))) (branch TermHasNoSpelling . familyTermDecodeFailed)))) def decodeEliminatorAfterFamily = (lambda unrestricted familyName : Bytes . (lambda unrestricted remaining : (family TermList) . (eliminate TermList (lambda unrestricted value : (family TermList) . (family TermDecodeResult)) remaining (branch TermListEnd . familyTermDecodeFailed) (branch TermListNext motive afterMotive ih_afterMotive . (eliminate TermList (lambda unrestricted value : (family TermList) . (family TermDecodeResult)) afterMotive (branch TermListEnd . familyTermDecodeFailed) (branch TermListNext scrutinee branches ih_branches . (constructor TermDecodeResult TermDecoded (constructor Term Eliminator familyName motive scrutinee (termListToTermSequence branches))))))))) def decodeEliminatorApplication = (lambda unrestricted familyTerm : (family Term) . (lambda unrestricted remaining : (family TermList) . (eliminate TermSpellingResult (lambda unrestricted result : (family TermSpellingResult) . (family TermDecodeResult)) (termSpelling familyTerm) (branch TermSpellingDecoded familyName . (decodeEliminatorAfterFamily familyName remaining)) (branch TermHasNoSpelling . familyTermDecodeFailed)))) def decodeMatchAfterFamily = (lambda unrestricted familyName : Bytes . (lambda unrestricted remaining : (family TermList) . (eliminate TermList (lambda unrestricted value : (family TermList) . (family TermDecodeResult)) remaining (branch TermListEnd . familyTermDecodeFailed) (branch TermListNext scrutinee branches ih_branches . (constructor TermDecodeResult TermDecoded (constructor Term Match familyName scrutinee (termListToTermSequence branches))))))) def decodeMatchApplication = (lambda unrestricted familyTerm : (family Term) . (lambda unrestricted remaining : (family TermList) . (eliminate TermSpellingResult (lambda unrestricted value : (family TermSpellingResult) . (family TermDecodeResult)) (termSpelling familyTerm) (branch TermSpellingDecoded familyName . (decodeMatchAfterFamily familyName remaining)) (branch TermHasNoSpelling . familyTermDecodeFailed)))) def decodeMatchWithAfterFamily = (lambda unrestricted familyName : Bytes . (lambda unrestricted remaining : (family TermList) . (eliminate TermList (lambda unrestricted value : (family TermList) . (family TermDecodeResult)) remaining (branch TermListEnd . familyTermDecodeFailed) (branch TermListNext motive afterMotive ih_afterMotive . (eliminate TermList (lambda unrestricted value : (family TermList) . (family TermDecodeResult)) afterMotive (branch TermListEnd . familyTermDecodeFailed) (branch TermListNext scrutinee branches ih_branches . (constructor TermDecodeResult TermDecoded (constructor Term MatchWith familyName motive scrutinee (termListToTermSequence branches))))))))) def decodeMatchWithApplication = (lambda unrestricted familyTerm : (family Term) . (lambda unrestricted remaining : (family TermList) . (eliminate TermSpellingResult (lambda unrestricted value : (family TermSpellingResult) . (family TermDecodeResult)) (termSpelling familyTerm) (branch TermSpellingDecoded familyName . (decodeMatchWithAfterFamily familyName remaining)) (branch TermHasNoSpelling . familyTermDecodeFailed)))) def arithmeticArityFailureCode = (succ familyTermSyntaxFailureCode) def unsupportedEditionFormCode = (succ arithmeticArityFailureCode) def arithmeticArityFailure = (constructor TermDecodeResult TermDecodeFailed arithmeticArityFailureCode (constructor SyntaxOrigin SyntaxOriginUnknown)) def decodeArithmeticArguments = (lambda unrestricted operation : (family CoreNaturalOperation) . (lambda unrestricted left : (family Term) . (lambda unrestricted remaining : (family TermList) . (eliminate TermList (lambda unrestricted terms : (family TermList) . (family TermDecodeResult)) remaining (branch TermListEnd . arithmeticArityFailure) (branch TermListNext right rest ih_rest . (eliminate TermList (lambda unrestricted terms : (family TermList) . (family TermDecodeResult)) rest (branch TermListEnd . (constructor TermDecodeResult TermDecoded (constructor Term NaturalArithmetic operation left right))) (branch TermListNext extra tail ih_tail . arithmeticArityFailure))))))) def decodePrimitiveVariableHead = (lambda unrestricted spelling : Bytes . (lambda unrestricted functionTerm : (family Term) . (lambda unrestricted argumentTerm : (family Term) . (lambda unrestricted remaining : (family TermList) . (chooseNamedDecode (bytesEqual spelling byteLiteralSpelling) (lambda unrestricted force : Nat . (decodeByteLiteral argumentTerm remaining)) (lambda unrestricted force : Nat . (chooseNamedDecode (bytesEqual spelling bytesLiteralSpelling) (lambda unrestricted force : Nat . (decodeBytesLiteral argumentTerm remaining)) (lambda unrestricted force : Nat . (nat-eliminate (lambda unrestricted matchedSuccessor : Nat . (family TermDecodeResult)) (nat-eliminate (lambda unrestricted matchedApplication : Nat . (family TermDecodeResult)) (decodeOrdinaryHead functionTerm argumentTerm remaining) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family TermDecodeResult) . (decodeApplicationTail argumentTerm remaining))) (bytesEqual spelling applicationSpelling)) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family TermDecodeResult) . (requireNoMoreArguments (constructor Term NaturalSuccessor argumentTerm) remaining))) (bytesEqual spelling successorSpelling)))))))))) def decodeRecordConstruction = (lambda unrestricted familyTerm : (family Term) . (lambda unrestricted bindings : (family TermList) . (eliminate TermSpellingResult (lambda unrestricted result : (family TermSpellingResult) . (family TermDecodeResult)) (termSpelling familyTerm) (branch TermSpellingDecoded familyName . (constructor TermDecodeResult TermDecoded (constructor Term RecordConstruction familyName (constructor SyntaxOrigin SyntaxOriginUnknown) (termListToTermSequence bindings)))) (branch TermHasNoSpelling . familyTermDecodeFailed)))) def decodeRecordProjectionField = (lambda unrestricted familyName : Bytes . (lambda unrestricted fieldTerm : (family Term) . (lambda unrestricted remaining : (family TermList) . (eliminate TermSpellingResult (lambda unrestricted result : (family TermSpellingResult) . (family TermDecodeResult)) (termSpelling fieldTerm) (branch TermSpellingDecoded fieldName . (eliminate TermList (lambda unrestricted terms : (family TermList) . (family TermDecodeResult)) remaining (branch TermListEnd . familyTermDecodeFailed) (branch TermListNext recordValue tail ih_tail . (eliminate TermList (lambda unrestricted terms : (family TermList) . (family TermDecodeResult)) tail (branch TermListEnd . (constructor TermDecodeResult TermDecoded (constructor Term RecordProjection familyName fieldName (constructor SyntaxOrigin SyntaxOriginUnknown) recordValue))) (branch TermListNext extra rest ih_rest . familyTermDecodeFailed))))) (branch TermHasNoSpelling . familyTermDecodeFailed))))) def decodeRecordProjection = (lambda unrestricted familyTerm : (family Term) . (lambda unrestricted remaining : (family TermList) . (eliminate TermSpellingResult (lambda unrestricted result : (family TermSpellingResult) . (family TermDecodeResult)) (termSpelling familyTerm) (branch TermSpellingDecoded familyName . (eliminate TermList (lambda unrestricted terms : (family TermList) . (family TermDecodeResult)) remaining (branch TermListEnd . familyTermDecodeFailed) (branch TermListNext fieldTerm tail ih_tail . (decodeRecordProjectionField familyName fieldTerm tail)))) (branch TermHasNoSpelling . familyTermDecodeFailed)))) def decodeRecordUpdate = (lambda unrestricted familyTerm : (family Term) . (lambda unrestricted remaining : (family TermList) . (eliminate TermSpellingResult (lambda unrestricted result : (family TermSpellingResult) . (family TermDecodeResult)) (termSpelling familyTerm) (branch TermSpellingDecoded familyName . (eliminate TermList (lambda unrestricted terms : (family TermList) . (family TermDecodeResult)) remaining (branch TermListEnd . familyTermDecodeFailed) (branch TermListNext recordValue bindings ih_bindings . (constructor TermDecodeResult TermDecoded (constructor Term RecordUpdate familyName (constructor SyntaxOrigin SyntaxOriginUnknown) recordValue (termListToTermSequence bindings)))))) (branch TermHasNoSpelling . familyTermDecodeFailed)))) def decodeRecordVariableHead = (lambda unrestricted spelling : Bytes . (lambda unrestricted functionTerm : (family Term) . (lambda unrestricted familyTerm : (family Term) . (lambda unrestricted remaining : (family TermList) . (chooseNamedDecode (bytesEqual spelling recordSpelling) (lambda unrestricted force : Nat . (decodeRecordConstruction familyTerm remaining)) (lambda unrestricted force : Nat . (chooseNamedDecode (bytesEqual spelling projectSpelling) (lambda unrestricted force : Nat . (decodeRecordProjection familyTerm remaining)) (lambda unrestricted force : Nat . (chooseNamedDecode (bytesEqual spelling updateSpelling) (lambda unrestricted force : Nat . (decodeRecordUpdate familyTerm remaining)) (lambda unrestricted force : Nat . (decodePrimitiveVariableHead spelling functionTerm familyTerm remaining))))))))))) def decodeMatchVariableHead = (lambda unrestricted spelling : Bytes . (lambda unrestricted functionTerm : (family Term) . (lambda unrestricted familyTerm : (family Term) . (lambda unrestricted remaining : (family TermList) . (chooseNamedDecode (bytesEqual spelling matchSpelling) (lambda unrestricted force : Nat . (decodeMatchApplication familyTerm remaining)) (lambda unrestricted force : Nat . (chooseNamedDecode (bytesEqual spelling matchWithSpelling) (lambda unrestricted force : Nat . (decodeMatchWithApplication familyTerm remaining)) (lambda unrestricted force : Nat . (decodeRecordVariableHead spelling functionTerm familyTerm remaining))))))))) def decodeNonBinderVariableHead = (lambda unrestricted spelling : Bytes . (lambda unrestricted functionTerm : (family Term) . (lambda unrestricted argumentTerm : (family Term) . (lambda unrestricted remaining : (family TermList) . (chooseNamedDecode (bytesEqual spelling universeTypeSpelling) (lambda unrestricted force : Nat . (decodeUniverseApplication argumentTerm remaining)) (lambda unrestricted force : Nat . (chooseNamedDecode (bytesEqual spelling familyApplicationSpelling) (lambda unrestricted force : Nat . (decodeFamilyApplication argumentTerm remaining)) (lambda unrestricted force : Nat . (chooseNamedDecode (bytesEqual spelling constructorApplicationSpelling) (lambda unrestricted force : Nat . (decodeConstructorApplication argumentTerm remaining)) (lambda unrestricted force : Nat . (chooseNamedDecode (bytesEqual spelling eliminatorSpelling) (lambda unrestricted force : Nat . (decodeEliminatorApplication argumentTerm remaining)) (lambda unrestricted force : Nat . (chooseNamedDecode (parserNaturalOr (bytesEqual spelling branchSpelling) (bytesEqual spelling caseSpelling)) (lambda unrestricted force : Nat . (decodeTermEliminatorBranch argumentTerm remaining)) (lambda unrestricted force : Nat . (decodeMatchVariableHead spelling functionTerm argumentTerm remaining))))))))))))))) def decodeNonArithmeticVariableHead = (lambda unrestricted spelling : Bytes . (lambda unrestricted functionTerm : (family Term) . (lambda unrestricted argumentTerm : (family Term) . (lambda unrestricted remaining : (family TermList) . (chooseNamedDecode (bytesEqual spelling doSpelling) (lambda unrestricted force : Nat . (decodeDoApplication argumentTerm remaining)) (lambda unrestricted force : Nat . (chooseNamedDecode (bytesEqual spelling letStarSpelling) (lambda unrestricted force : Nat . (decodeLocalLetSequence (constructor TermList TermListNext argumentTerm remaining))) (lambda unrestricted force : Nat . (chooseNamedDecode (bytesEqual spelling lambdaSpelling) (lambda unrestricted force : Nat . (decodeBinderForm zero argumentTerm remaining)) (lambda unrestricted force : Nat . (chooseNamedDecode (bytesEqual spelling piSpelling) (lambda unrestricted force : Nat . (decodeBinderForm (succ zero) argumentTerm remaining)) (lambda unrestricted force : Nat . (decodeNonBinderVariableHead spelling functionTerm argumentTerm remaining))))))))))))) -- Recognize fixed arithmetic heads before speculative decoding of unrelated -- forms: a compact operand must never enter a universe/byte unary decoder. def decodeVariableHead = (lambda unrestricted spelling : Bytes . (lambda unrestricted functionTerm : (family Term) . (lambda unrestricted argumentTerm : (family Term) . (lambda unrestricted remaining : (family TermList) . (eliminate NaturalOperationLookup (lambda unrestricted result : (family NaturalOperationLookup) . (family TermDecodeResult)) (Compiler.NaturalOperation/lookupNaturalOperation spelling) (branch NaturalOperationFound operation . (decodeArithmeticArguments operation argumentTerm remaining)) (branch NaturalOperationMissing . (decodeNonArithmeticVariableHead spelling functionTerm argumentTerm remaining))))))) def decodeNullaryTerm = (lambda unrestricted term : (family Term) . (eliminate Term (lambda unrestricted value : (family Term) . (family TermDecodeResult)) term (branch Variable spelling . (eliminate NaturalOperationLookup (lambda unrestricted result : (family NaturalOperationLookup) . (family TermDecodeResult)) (Compiler.NaturalOperation/lookupNaturalOperation spelling) (branch NaturalOperationFound operation . arithmeticArityFailure) (branch NaturalOperationMissing . (chooseNamedDecode (bytesEqual spelling bytesLiteralSpelling) (lambda unrestricted force : Nat . (constructor TermDecodeResult TermDecoded (constructor Term BytesLiteral b""))) (lambda unrestricted force : Nat . (constructor TermDecodeResult TermDecoded term)))))) (branch Universe level . (constructor TermDecodeResult TermDecoded term)) (branch NaturalType . (constructor TermDecodeResult TermDecoded term)) (branch NaturalZero . (constructor TermDecodeResult TermDecoded term)) (branch NaturalLiteral naturalLiteralValue . (constructor TermDecodeResult TermDecoded term)) (branch NaturalSuccessor predecessor ih_predecessor . (constructor TermDecodeResult TermDecoded term)) (branch Application function argument ih_function ih_argument . (constructor TermDecodeResult TermDecoded term)) (branch NaturalArithmetic operation function argument ih_function ih_argument . (constructor TermDecodeResult TermDecoded term)) (branch Lambda quantityTag binderSpelling domain body ih_domain ih_body . (constructor TermDecodeResult TermDecoded term)) (branch Pi quantityTag binderSpelling domain codomain ih_domain ih_codomain . (constructor TermDecodeResult TermDecoded term)) (branch BytesType . (constructor TermDecodeResult TermDecoded term)) (branch BytesLiteral bytesValue . (constructor TermDecodeResult TermDecoded term)) (branch ByteType . (constructor TermDecodeResult TermDecoded term)) (branch ByteLiteral byteValue . (constructor TermDecodeResult TermDecoded term)) (branch TermSequenceEnd . (constructor TermDecodeResult TermDecoded term)) (branch TermSequenceNext sequenceHead sequenceTail ih_sequenceHead ih_sequenceTail . (constructor TermDecodeResult TermDecoded term)) (branch TermEliminatorBranch constructorSpelling binderNames body ih_binderNames ih_body . (constructor TermDecodeResult TermDecoded term)) (branch FamilyApplication familySpelling familyArguments ih_familyArguments . (constructor TermDecodeResult TermDecoded term)) (branch ConstructorApplication familySpelling constructorSpelling constructorArguments ih_constructorArguments . (constructor TermDecodeResult TermDecoded term)) (branch Eliminator eliminatedFamilySpelling motive scrutinee branches ih_motive ih_scrutinee ih_branches . (constructor TermDecodeResult TermDecoded term)) (branch Match family scrutinee branches ih_scrutinee ih_branches . (constructor TermDecodeResult TermDecoded term)) (branch MatchWith family motive scrutinee branches ih_motive ih_scrutinee ih_branches . (constructor TermDecodeResult TermDecoded term)) (branch IntegerLiteral integerLiteralSpelling . (constructor TermDecodeResult TermDecoded term)) (branch RecordConstruction name origin bindings ih_bindings . (constructor TermDecodeResult TermDecoded term)) (branch RecordAssignment name origin value ih_value . (constructor TermDecodeResult TermDecoded term)) (branch RecordProjection name field origin value ih_value . (constructor TermDecodeResult TermDecoded term)) (branch RecordUpdate name origin value bindings ih_value ih_bindings . (constructor TermDecodeResult TermDecoded term)) (branch LocalLet quantity binder hasAnnotation annotation value body ih_annotation ih_value ih_body . (constructor TermDecodeResult TermDecoded term)) (branch DoBlock effects result body ih_effects ih_result ih_body . (constructor TermDecodeResult TermDecoded term)) (branch DoStep named quantity binder computation continuation ih_computation ih_continuation . (constructor TermDecodeResult TermDecoded term)) (branch DoReturn value ih_value . (constructor TermDecodeResult TermDecoded term)))) def decodeHeadWithArgument = (lambda unrestricted functionTerm : (family Term) . (lambda unrestricted argumentTerm : (family Term) . (lambda unrestricted remaining : (family TermList) . (eliminate Term (lambda unrestricted value : (family Term) . (family TermDecodeResult)) functionTerm (branch Variable spelling . (decodeVariableHead spelling functionTerm argumentTerm remaining)) (branch Universe level . (decodeOrdinaryHead functionTerm argumentTerm remaining)) (branch NaturalType . (decodeOrdinaryHead functionTerm argumentTerm remaining)) (branch NaturalZero . (decodeOrdinaryHead functionTerm argumentTerm remaining)) (branch NaturalLiteral naturalLiteralValue . (decodeOrdinaryHead functionTerm argumentTerm remaining)) (branch NaturalSuccessor predecessor ih_predecessor . (decodeOrdinaryHead functionTerm argumentTerm remaining)) (branch Application function argument ih_function ih_argument . (decodeOrdinaryHead functionTerm argumentTerm remaining)) (branch NaturalArithmetic operation function argument ih_function ih_argument . (decodeOrdinaryHead functionTerm argumentTerm remaining)) (branch Lambda quantityTag binderSpelling domain body ih_domain ih_body . (decodeOrdinaryHead functionTerm argumentTerm remaining)) (branch Pi quantityTag binderSpelling domain codomain ih_domain ih_codomain . (decodeOrdinaryHead functionTerm argumentTerm remaining)) (branch BytesType . (decodeOrdinaryHead functionTerm argumentTerm remaining)) (branch BytesLiteral bytesValue . (decodeOrdinaryHead functionTerm argumentTerm remaining)) (branch ByteType . (decodeOrdinaryHead functionTerm argumentTerm remaining)) (branch ByteLiteral byteValue . (decodeOrdinaryHead functionTerm argumentTerm remaining)) (branch TermSequenceEnd . (decodeOrdinaryHead functionTerm argumentTerm remaining)) (branch TermSequenceNext sequenceHead sequenceTail ih_sequenceHead ih_sequenceTail . (decodeOrdinaryHead functionTerm argumentTerm remaining)) (branch TermEliminatorBranch constructorSpelling binderNames body ih_binderNames ih_body . (decodeOrdinaryHead functionTerm argumentTerm remaining)) (branch FamilyApplication familySpelling familyArguments ih_familyArguments . (decodeOrdinaryHead functionTerm argumentTerm remaining)) (branch ConstructorApplication familySpelling constructorSpelling constructorArguments ih_constructorArguments . (decodeOrdinaryHead functionTerm argumentTerm remaining)) (branch Eliminator eliminatedFamilySpelling motive scrutinee branches ih_motive ih_scrutinee ih_branches . (decodeOrdinaryHead functionTerm argumentTerm remaining)) (branch Match family scrutinee branches ih_scrutinee ih_branches . (decodeOrdinaryHead functionTerm argumentTerm remaining)) (branch MatchWith family motive scrutinee branches ih_motive ih_scrutinee ih_branches . (decodeOrdinaryHead functionTerm argumentTerm remaining)) (branch IntegerLiteral integerLiteralSpelling . (decodeOrdinaryHead functionTerm argumentTerm remaining)) (branch RecordConstruction name origin bindings ih_bindings . (decodeOrdinaryHead functionTerm argumentTerm remaining)) (branch RecordAssignment name origin value ih_value . (decodeOrdinaryHead functionTerm argumentTerm remaining)) (branch RecordProjection name field origin value ih_value . (decodeOrdinaryHead functionTerm argumentTerm remaining)) (branch RecordUpdate name origin value bindings ih_value ih_bindings . (decodeOrdinaryHead functionTerm argumentTerm remaining)) (branch LocalLet quantity binder hasAnnotation annotation value body ih_annotation ih_value ih_body . (decodeOrdinaryHead functionTerm argumentTerm remaining)) (branch DoBlock effects result body ih_effects ih_result ih_body . (decodeOrdinaryHead functionTerm argumentTerm remaining)) (branch DoStep named quantity binder computation continuation ih_computation ih_continuation . (decodeOrdinaryHead functionTerm argumentTerm remaining)) (branch DoReturn value ih_value . (decodeOrdinaryHead functionTerm argumentTerm remaining)))))) def decodeRecordAssignmentTerms = (lambda unrestricted name : Bytes . (lambda unrestricted origin : (family SyntaxOrigin) . (lambda unrestricted terms : (family TermList) . (eliminate TermList (lambda unrestricted current : (family TermList) . (family TermDecodeResult)) terms (branch TermListEnd . familyTermDecodeFailed) (branch TermListNext nameTerm afterName ih_afterName . (eliminate TermList (lambda unrestricted current : (family TermList) . (family TermDecodeResult)) afterName (branch TermListEnd . familyTermDecodeFailed) (branch TermListNext equalsTerm afterEquals ih_afterEquals . (eliminate TermList (lambda unrestricted current : (family TermList) . (family TermDecodeResult)) afterEquals (branch TermListEnd . familyTermDecodeFailed) (branch TermListNext value afterValue ih_afterValue . (eliminate TermList (lambda unrestricted current : (family TermList) . (family TermDecodeResult)) afterValue (branch TermListEnd . (constructor TermDecodeResult TermDecoded (constructor Term RecordAssignment name origin value))) (branch TermListNext extra rest ih_rest . familyTermDecodeFailed))))))))))) def finishDecodedRecordAssignmentTail = (lambda unrestricted name : Bytes . (lambda unrestricted origin : (family SyntaxOrigin) . (lambda unrestricted afterEquals : (family Syntax) . (lambda unrestricted terms : (family TermList) . (lambda unrestricted fallback : (family TermDecodeResult) . (eliminate Syntax (lambda unrestricted current : (family Syntax) . (family TermDecodeResult)) afterEquals (branch SyntaxAtom spelling atomOrigin . fallback) (branch SyntaxEmpty . fallback) (branch SyntaxCons value afterValue ih_value ih_afterValue . (eliminate Syntax (lambda unrestricted current : (family Syntax) . (family TermDecodeResult)) afterValue (branch SyntaxAtom spelling atomOrigin . fallback) (branch SyntaxEmpty . (decodeRecordAssignmentTerms name origin terms)) (branch SyntaxCons extra rest ih_extra ih_rest . fallback) (branch SyntaxNode children ih_children . fallback))) (branch SyntaxNode children ih_children . fallback))))))) def finishDecodedRecordAssignmentAfterName = (lambda unrestricted name : Bytes . (lambda unrestricted origin : (family SyntaxOrigin) . (lambda unrestricted afterName : (family Syntax) . (lambda unrestricted terms : (family TermList) . (lambda unrestricted fallback : (family TermDecodeResult) . (eliminate Syntax (lambda unrestricted current : (family Syntax) . (family TermDecodeResult)) afterName (branch SyntaxAtom spelling atomOrigin . fallback) (branch SyntaxEmpty . fallback) (branch SyntaxCons equals afterEquals ih_equals ih_afterEquals . (eliminate Syntax (lambda unrestricted current : (family Syntax) . (family TermDecodeResult)) equals (branch SyntaxAtom spelling equalsOrigin . (app (nat-eliminate (lambda unrestricted matched : Nat . (pi unrestricted force : Nat . (family TermDecodeResult))) (lambda unrestricted force : Nat . fallback) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (pi unrestricted force : Nat . (family TermDecodeResult)) . (lambda unrestricted force : Nat . (finishDecodedRecordAssignmentTail name origin afterEquals terms fallback)))) (bytesEqual spelling equalsSpelling)) zero)) (branch SyntaxEmpty . fallback) (branch SyntaxCons head tail ih_head ih_tail . fallback) (branch SyntaxNode children ih_children . fallback))) (branch SyntaxNode children ih_children . fallback))))))) def finishDecodedNode = (lambda unrestricted children : (family Syntax) . (lambda unrestricted terms : (family TermList) . (lambda unrestricted fallback : (family TermDecodeResult) . (eliminate Syntax (lambda unrestricted current : (family Syntax) . (family TermDecodeResult)) children (branch SyntaxAtom spelling origin . fallback) (branch SyntaxEmpty . fallback) (branch SyntaxCons name afterName ih_name ih_afterName . (eliminate Syntax (lambda unrestricted current : (family Syntax) . (family TermDecodeResult)) name (branch SyntaxAtom spelling origin . (finishDecodedRecordAssignmentAfterName spelling origin afterName terms fallback)) (branch SyntaxEmpty . fallback) (branch SyntaxCons head tail ih_head ih_tail . fallback) (branch SyntaxNode nested ih_nested . fallback))) (branch SyntaxNode nested ih_nested . fallback))))) def finishDecodedTerms = (lambda unrestricted terms : (family TermList) . (eliminate TermList (lambda unrestricted value : (family TermList) . (family TermDecodeResult)) terms (branch TermListEnd . (constructor TermDecodeResult TermDecodeFailed (succ (succ (succ (succ (succ zero))))) (constructor SyntaxOrigin SyntaxOriginUnknown))) (branch TermListNext listedTerm listedRest ih_listedRest . (eliminate TermList (lambda unrestricted value : (family TermList) . (family TermDecodeResult)) listedRest (branch TermListEnd . (decodeNullaryTerm listedTerm)) (branch TermListNext nextTerm remainingTerms ih_remainingTerms . (decodeHeadWithArgument listedTerm nextTerm remainingTerms)))))) def bareUniverseLevel = (lambda unrestricted term : (family Term) . (eliminate Term (lambda unrestricted value : (family Term) . (family NaturalTermResult)) term (branch Variable spelling . (constructor NaturalTermResult NotNaturalTerm)) (branch Universe level . (constructor NaturalTermResult NotNaturalTerm)) (branch NaturalType . (constructor NaturalTermResult NotNaturalTerm)) (branch NaturalZero . (constructor NaturalTermResult NotNaturalTerm)) (branch NaturalLiteral value . (constructor NaturalTermResult NotNaturalTerm)) (branch NaturalSuccessor predecessor ih . (constructor NaturalTermResult NotNaturalTerm)) (branch Application function argument ihf iha . (constructor NaturalTermResult NotNaturalTerm)) (branch NaturalArithmetic operation function argument ihf iha . (constructor NaturalTermResult NotNaturalTerm)) (branch Lambda quantity binder domain body ihd ihb . (constructor NaturalTermResult NotNaturalTerm)) (branch Pi quantity binder domain body ihd ihb . (constructor NaturalTermResult NotNaturalTerm)) (branch BytesType . (constructor NaturalTermResult NotNaturalTerm)) (branch BytesLiteral value . (constructor NaturalTermResult NotNaturalTerm)) (branch ByteType . (constructor NaturalTermResult NotNaturalTerm)) (branch ByteLiteral value . (constructor NaturalTermResult NotNaturalTerm)) (branch TermSequenceEnd . (constructor NaturalTermResult NotNaturalTerm)) (branch TermSequenceNext head tail ihh iht . (constructor NaturalTermResult NotNaturalTerm)) (branch TermEliminatorBranch constructor binders body ihb ihbody . (constructor NaturalTermResult NotNaturalTerm)) (branch FamilyApplication family arguments iha . (constructor NaturalTermResult NotNaturalTerm)) (branch ConstructorApplication family constructor arguments iha . (constructor NaturalTermResult NotNaturalTerm)) (branch Eliminator family motive scrutinee branches ihm ihs ihb . (constructor NaturalTermResult NotNaturalTerm)) (branch Match family scrutinee branches ihs ihb . (constructor NaturalTermResult NotNaturalTerm)) (branch MatchWith family motive scrutinee branches ihm ihs ihb . (constructor NaturalTermResult NotNaturalTerm)) (branch IntegerLiteral spelling . (naturalLiteralAsTermValue (parseUnsignedNaturalLiteral spelling))) (branch RecordConstruction name origin bindings ih_bindings . (constructor NaturalTermResult NotNaturalTerm)) (branch RecordAssignment name origin value ih_value . (constructor NaturalTermResult NotNaturalTerm)) (branch RecordProjection name field origin value ih_value . (constructor NaturalTermResult NotNaturalTerm)) (branch RecordUpdate name origin value bindings ih_value ih_bindings . (constructor NaturalTermResult NotNaturalTerm)) (branch LocalLet quantity binder hasAnnotation annotation value body ih_annotation ih_value ih_body . (constructor NaturalTermResult NotNaturalTerm)) (branch DoBlock effects result body ih_effects ih_result ih_body . (constructor NaturalTermResult NotNaturalTerm)) (branch DoStep named quantity binder computation continuation ih_computation ih_continuation . (constructor NaturalTermResult NotNaturalTerm)) (branch DoReturn value ih_value . (constructor NaturalTermResult NotNaturalTerm)))) -- The structural fold runs right-to-left. Consume exactly the adjacent numeric -- token after Type; punctuation and following arguments stay in the tail. def prependUniverseSequence = (lambda unrestricted head : (family Term) . (lambda unrestricted tail : (family TermList) . (eliminate TermList (lambda unrestricted value : (family TermList) . (family TermList)) tail (branch TermListEnd . (constructor TermList TermListNext head tail)) (branch TermListNext level remaining ih_remaining . (eliminate NaturalTermResult (lambda unrestricted value : (family NaturalTermResult) . (family TermList)) (bareUniverseLevel level) (branch NaturalTermDecoded value . (constructor TermList TermListNext (constructor Term Universe value) remaining)) (branch NotNaturalTerm . (constructor TermList TermListNext head tail))))))) def prependDecodedSequence = (lambda unrestricted head : (family Term) . (lambda unrestricted tail : (family TermList) . (eliminate TermSpellingResult (lambda unrestricted value : (family TermSpellingResult) . (family TermList)) (termSpelling head) (branch TermSpellingDecoded spelling . (nat-eliminate (lambda unrestricted match : Nat . (family TermList)) (constructor TermList TermListNext head tail) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family TermList) . (prependUniverseSequence head tail))) (bytesEqual spelling universeTypeSpelling))) (branch TermHasNoSpelling . (constructor TermList TermListNext head tail))))) def combineDecodedSequence = (lambda unrestricted headResult : (family TermDecodeResult) . (lambda unrestricted tailResult : (family TermDecodeResult) . (eliminate TermDecodeResult (lambda unrestricted value : (family TermDecodeResult) . (family TermDecodeResult)) headResult (branch TermDecoded decodedTerm . (eliminate TermDecodeResult (lambda unrestricted value : (family TermDecodeResult) . (family TermDecodeResult)) tailResult (branch TermDecoded tailTerm . (constructor TermDecodeResult TermDecodeFailed (succ (succ (succ (succ (succ zero))))) (constructor SyntaxOrigin SyntaxOriginUnknown))) (branch TermsDecoded decodedTerms . (constructor TermDecodeResult TermsDecoded (prependDecodedSequence decodedTerm decodedTerms))) (branch TermDecodeFailed termDecodeFailureCode termFailureOrigin . (constructor TermDecodeResult TermDecodeFailed termDecodeFailureCode termFailureOrigin)))) (branch TermsDecoded decodedTerms . (constructor TermDecodeResult TermDecodeFailed (succ (succ (succ (succ (succ zero))))) (constructor SyntaxOrigin SyntaxOriginUnknown))) (branch TermDecodeFailed termDecodeFailureCode termFailureOrigin . (constructor TermDecodeResult TermDecodeFailed termDecodeFailureCode termFailureOrigin))))) -- Literal decoders return token-relative ranges; rebase only at an atom. def termDecodeAttachOrigin = (lambda unrestricted origin : (family SyntaxOrigin) . (lambda unrestricted result : (family TermDecodeResult) . (eliminate TermDecodeResult (lambda unrestricted current : (family TermDecodeResult) . (family TermDecodeResult)) result (branch TermDecoded term . (constructor TermDecodeResult TermDecoded term)) (branch TermsDecoded terms . (constructor TermDecodeResult TermsDecoded terms)) (branch TermDecodeFailed code relative . (constructor TermDecodeResult TermDecodeFailed code (eliminate SyntaxOrigin (lambda unrestricted current : (family SyntaxOrigin) . (family SyntaxOrigin)) origin (branch SyntaxOriginUnknown . (constructor SyntaxOrigin SyntaxOriginUnknown)) (branch SyntaxOriginRange start end . (eliminate SyntaxOrigin (lambda unrestricted current : (family SyntaxOrigin) . (family SyntaxOrigin)) relative (branch SyntaxOriginUnknown . (constructor SyntaxOrigin SyntaxOriginUnknown)) (branch SyntaxOriginRange relativeStart relativeEnd . (constructor SyntaxOrigin SyntaxOriginRange (Std.Natural/naturalAdd start relativeStart) (Std.Natural/naturalAdd start relativeEnd))))))))))) def decodeSyntax = (lambda unrestricted syntax : (family Syntax) . (eliminate Syntax (lambda unrestricted value : (family Syntax) . (family TermDecodeResult)) syntax (branch SyntaxAtom syntaxSpelling origin . (termDecodeAttachOrigin origin (decodeAtom syntaxSpelling))) (branch SyntaxEmpty . (constructor TermDecodeResult TermsDecoded (constructor TermList TermListEnd))) (branch SyntaxCons syntaxHead syntaxTail ih_syntaxHead ih_syntaxTail . (combineDecodedSequence ih_syntaxHead ih_syntaxTail)) (branch SyntaxNode syntaxChildren ih_syntaxChildren . (eliminate TermDecodeResult (lambda unrestricted value : (family TermDecodeResult) . (family TermDecodeResult)) ih_syntaxChildren (branch TermDecoded decodedTerm . (constructor TermDecodeResult TermDecodeFailed (succ (succ (succ (succ (succ zero))))) (constructor SyntaxOrigin SyntaxOriginUnknown))) (branch TermsDecoded decodedTerms . (finishDecodedNode syntaxChildren decodedTerms (finishDecodedTerms decodedTerms))) (branch TermDecodeFailed termDecodeFailureCode termFailureOrigin . (constructor TermDecodeResult TermDecodeFailed termDecodeFailureCode termFailureOrigin)))))) def syntaxAtomIsArithmetic = (lambda unrestricted syntax : (family Syntax) . (eliminate Syntax (lambda unrestricted current : (family Syntax) . Nat) syntax (branch SyntaxAtom spelling origin . (eliminate NaturalOperationLookup (lambda unrestricted result : (family NaturalOperationLookup) . Nat) (Compiler.NaturalOperation/lookupNaturalOperation spelling) (branch NaturalOperationFound operation . (succ zero)) (branch NaturalOperationMissing . zero))) (branch SyntaxEmpty . zero) (branch SyntaxCons head tail ih_head ih_tail . zero) (branch SyntaxNode children ih_children . zero))) def syntaxArithmeticHead = (lambda unrestricted syntax : (family Syntax) . (eliminate Syntax (lambda unrestricted current : (family Syntax) . Nat) syntax (branch SyntaxAtom spelling origin . zero) (branch SyntaxEmpty . zero) (branch SyntaxCons head tail ih_head ih_tail . (syntaxAtomIsArithmetic head)) (branch SyntaxNode children ih_children . zero))) def parserFlagOr = (lambda unrestricted left : Nat . (lambda unrestricted right : Nat . (nat-eliminate (lambda unrestricted flag : Nat . Nat) right (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . (succ zero))) left))) def syntaxAtomIsNamedRecord = (lambda unrestricted syntax : (family Syntax) . (eliminate Syntax (lambda unrestricted current : (family Syntax) . Nat) syntax (branch SyntaxAtom spelling origin . (parserFlagOr (bytesEqual spelling recordSpelling) (parserFlagOr (bytesEqual spelling projectSpelling) (bytesEqual spelling updateSpelling)))) (branch SyntaxEmpty . zero) (branch SyntaxCons head tail ih_head ih_tail . zero) (branch SyntaxNode children ih_children . zero))) def syntaxNamedRecordHead = (lambda unrestricted syntax : (family Syntax) . (eliminate Syntax (lambda unrestricted current : (family Syntax) . Nat) syntax (branch SyntaxAtom spelling origin . zero) (branch SyntaxEmpty . zero) (branch SyntaxCons head tail ih_head ih_tail . (syntaxAtomIsNamedRecord head)) (branch SyntaxNode children ih_children . zero))) def syntaxAtomIsReadableMatching = (lambda unrestricted syntax : (family Syntax) . (eliminate Syntax (lambda unrestricted current : (family Syntax) . Nat) syntax (branch SyntaxAtom spelling origin . (parserFlagOr (bytesEqual spelling matchSpelling) (bytesEqual spelling matchWithSpelling))) (branch SyntaxEmpty . zero) (branch SyntaxCons head tail ih_head ih_tail . zero) (branch SyntaxNode children ih_children . zero))) def syntaxReadableMatchingHead = (lambda unrestricted syntax : (family Syntax) . (eliminate Syntax (lambda unrestricted current : (family Syntax) . Nat) syntax (branch SyntaxAtom spelling origin . zero) (branch SyntaxEmpty . zero) (branch SyntaxCons head tail ih_head ih_tail . (syntaxAtomIsReadableMatching head)) (branch SyntaxNode children ih_children . zero))) def syntaxAtomIsSequencing = (lambda unrestricted syntax : (family Syntax) . (eliminate Syntax (lambda unrestricted current : (family Syntax) . Nat) syntax (branch SyntaxAtom spelling origin . (parserFlagOr (bytesEqual spelling letStarSpelling) (bytesEqual spelling doSpelling))) (branch SyntaxEmpty . zero) (branch SyntaxCons head tail ih_head ih_tail . zero) (branch SyntaxNode children ih_children . zero))) def syntaxSequencingHead = (lambda unrestricted syntax : (family Syntax) . (eliminate Syntax (lambda unrestricted current : (family Syntax) . Nat) syntax (branch SyntaxAtom spelling origin . zero) (branch SyntaxEmpty . zero) (branch SyntaxCons head tail ih_head ih_tail . (syntaxAtomIsSequencing head)) (branch SyntaxNode children ih_children . zero))) -- Only form heads are reserved; identifiers in binder or value positions are not. def syntaxUsesArithmetic = (lambda unrestricted syntax : (family Syntax) . (eliminate Syntax (lambda unrestricted current : (family Syntax) . Nat) syntax (branch SyntaxAtom spelling origin . zero) (branch SyntaxEmpty . zero) (branch SyntaxCons head tail ih_head ih_tail . (parserFlagOr ih_head ih_tail)) (branch SyntaxNode children ih_children . (parserFlagOr (syntaxArithmeticHead children) ih_children)))) def syntaxUsesNamedRecords = (lambda unrestricted syntax : (family Syntax) . (eliminate Syntax (lambda unrestricted current : (family Syntax) . Nat) syntax (branch SyntaxAtom spelling origin . zero) (branch SyntaxEmpty . zero) (branch SyntaxCons head tail ih_head ih_tail . (parserFlagOr ih_head ih_tail)) (branch SyntaxNode children ih_children . (parserFlagOr (syntaxNamedRecordHead children) ih_children)))) def syntaxUsesReadableMatching = (lambda unrestricted syntax : (family Syntax) . (eliminate Syntax (lambda unrestricted current : (family Syntax) . Nat) syntax (branch SyntaxAtom spelling origin . zero) (branch SyntaxEmpty . zero) (branch SyntaxCons head tail ih_head ih_tail . (parserFlagOr ih_head ih_tail)) (branch SyntaxNode children ih_children . (parserFlagOr (syntaxReadableMatchingHead children) ih_children)))) def syntaxUsesSequencing = (lambda unrestricted syntax : (family Syntax) . (eliminate Syntax (lambda unrestricted current : (family Syntax) . Nat) syntax (branch SyntaxAtom spelling origin . zero) (branch SyntaxEmpty . zero) (branch SyntaxCons head tail ih_head ih_tail . (parserFlagOr ih_head ih_tail)) (branch SyntaxNode children ih_children . (parserFlagOr (syntaxSequencingHead children) ih_children)))) -- Literal spelling stays intact in SyntaxAtom, including the optional b prefix. def syntaxUsesQuotedLiterals = (lambda unrestricted syntax : (family Syntax) . (eliminate Syntax (lambda unrestricted current : (family Syntax) . Nat) syntax (branch SyntaxAtom spelling origin . (parserFlagOr (byte-equal (bytes-head spelling) (byte 34)) (nat-eliminate (lambda unrestricted flag : Nat . Nat) zero (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : Nat . (byte-equal (bytes-head (bytes-tail spelling)) (byte 34)))) (byte-equal (bytes-head spelling) (byte 98))))) (branch SyntaxEmpty . zero) (branch SyntaxCons head tail ih_head ih_tail . (parserFlagOr ih_head ih_tail)) (branch SyntaxNode children ih_children . ih_children))) def parserEditionUseAllowed = (lambda unrestricted allowed : Nat . (lambda unrestricted used : Nat . (nat-eliminate (lambda unrestricted flag : Nat . Nat) (nat-eliminate (lambda unrestricted flag : Nat . Nat) (succ zero) (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : Nat . zero)) used) (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : Nat . (succ zero))) allowed))) def syntaxAllowedInEdition = (lambda unrestricted edition : (family LanguageEdition) . (lambda unrestricted syntax : (family Syntax) . (parserNaturalAnd (parserEditionUseAllowed (Compiler.LanguageEdition/editionAllowsNamedRecords edition) (syntaxUsesNamedRecords syntax)) (parserNaturalAnd (parserEditionUseAllowed (Compiler.LanguageEdition/editionAllowsSequencing edition) (syntaxUsesSequencing syntax)) (parserNaturalAnd (parserEditionUseAllowed (Compiler.LanguageEdition/editionAllowsReadableMatching edition) (syntaxUsesReadableMatching syntax)) (parserNaturalAnd (parserEditionUseAllowed (Compiler.LanguageEdition/editionAllowsNaturalArithmetic edition) (syntaxUsesArithmetic syntax)) (parserEditionUseAllowed (Compiler.LanguageEdition/editionAllowsQuotedLiterals edition) (syntaxUsesQuotedLiterals syntax)))))))) def decodeSyntaxInEdition = (lambda unrestricted edition : (family LanguageEdition) . (lambda unrestricted syntax : (family Syntax) . (app (nat-eliminate (lambda unrestricted allowed : Nat . (pi unrestricted force : Nat . (family TermDecodeResult))) (lambda unrestricted force : Nat . (constructor TermDecodeResult TermDecodeFailed unsupportedEditionFormCode (constructor SyntaxOrigin SyntaxOriginUnknown))) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (pi unrestricted force : Nat . (family TermDecodeResult)) . (lambda unrestricted force : Nat . (decodeSyntax syntax)))) (syntaxAllowedInEdition edition syntax)) zero))) def decodeStructuralResultInEdition = (lambda unrestricted edition : (family LanguageEdition) . (lambda unrestricted result : (family StructuralParseResult) . (eliminate StructuralParseResult (lambda unrestricted current : (family StructuralParseResult) . (family TermDecodeResult)) result (branch StructuralParsed syntax . (decodeSyntaxInEdition edition syntax)) (branch StructuralParseFailed code structuralFailureOrigin . (constructor TermDecodeResult TermDecodeFailed code structuralFailureOrigin))))) def decodeStructuralResult = (decodeStructuralResultInEdition (constructor LanguageEdition Alpha2026)) def applicationSpineLength = (lambda unrestricted term : (family Term) . (eliminate Term (lambda unrestricted value : (family Term) . Nat) term (branch Variable spelling . zero) (branch Universe level . zero) (branch NaturalType . zero) (branch NaturalZero . zero) (branch NaturalLiteral naturalLiteralValue . zero) (branch NaturalSuccessor predecessor ih_predecessor . zero) (branch Application function argument ih_function ih_argument . (succ ih_function)) (branch NaturalArithmetic operation function argument ih_function ih_argument . zero) (branch Lambda quantityTag binderSpelling domain body ih_domain ih_body . zero) (branch Pi quantityTag binderSpelling domain codomain ih_domain ih_codomain . zero) (branch BytesType . zero) (branch BytesLiteral bytesValue . zero) (branch ByteType . zero) (branch ByteLiteral byteValue . zero) (branch TermSequenceEnd . zero) (branch TermSequenceNext sequenceHead sequenceTail ih_sequenceHead ih_sequenceTail . zero) (branch TermEliminatorBranch constructorSpelling binderNames body ih_binderNames ih_body . zero) (branch FamilyApplication familySpelling familyArguments ih_familyArguments . zero) (branch ConstructorApplication familySpelling constructorSpelling constructorArguments ih_constructorArguments . zero) (branch Eliminator eliminatedFamilySpelling motive scrutinee branches ih_motive ih_scrutinee ih_branches . zero) (branch Match family scrutinee branches ih_scrutinee ih_branches . zero) (branch MatchWith family motive scrutinee branches ih_motive ih_scrutinee ih_branches . zero) (branch IntegerLiteral integerLiteralSpelling . zero) (branch RecordConstruction name origin bindings ih_bindings . zero) (branch RecordAssignment name origin value ih_value . zero) (branch RecordProjection name field origin value ih_value . zero) (branch RecordUpdate name origin value bindings ih_value ih_bindings . zero) (branch LocalLet quantity binder hasAnnotation annotation value body ih_annotation ih_value ih_body . zero) (branch DoBlock effects result body ih_effects ih_result ih_body . zero) (branch DoStep named quantity binder computation continuation ih_computation ih_continuation . zero) (branch DoReturn value ih_value . zero))) def parseLexedHead = (lambda unrestricted stream : (family LexedBytes) . (eliminate LexedBytes (lambda unrestricted value : (family LexedBytes) . (family Term)) stream (branch LexEnd . (constructor Term Variable b"")) (branch LexByte tokenClass tokenSpelling lexedRest ih_lexedRest . (eliminate ByteClass (lambda unrestricted value : (family ByteClass) . (family Term)) tokenClass (branch OpenDelimiter . ih_lexedRest) (branch CloseDelimiter . ih_lexedRest) (branch Whitespace . ih_lexedRest) (branch DecimalDigit . (constructor Term NaturalZero)) (branch IdentifierByte . (constructor Term Variable (bytes-cons tokenSpelling b""))))))) def parseSource = (lambda unrestricted source : Bytes . (parseLexedHead (lexSource source))) def parserSample : (family Term) = (parseSource b"( 0 )") def parserFingerprint : Nat = (eliminate Term (lambda unrestricted term : (family Term) . Nat) parserSample (branch Variable spelling . zero) (branch Universe level . (succ zero)) (branch NaturalType . (succ (succ zero))) (branch NaturalZero . (succ (succ (succ (succ (succ (succ (succ zero)))))))) (branch NaturalLiteral naturalLiteralValue . (succ (succ (succ (succ (succ (succ (succ zero)))))))) (branch NaturalSuccessor predecessor ih_predecessor . zero) (branch Application function argument ih_function ih_argument . zero) (branch NaturalArithmetic operation function argument ih_function ih_argument . zero) (branch Lambda quantityTag binderSpelling domain body ih_domain ih_body . zero) (branch Pi quantityTag binderSpelling domain codomain ih_domain ih_codomain . zero) (branch BytesType . zero) (branch BytesLiteral bytesValue . zero) (branch ByteType . zero) (branch ByteLiteral byteValue . zero) (branch TermSequenceEnd . zero) (branch TermSequenceNext sequenceHead sequenceTail ih_sequenceHead ih_sequenceTail . zero) (branch TermEliminatorBranch constructorSpelling binderNames body ih_binderNames ih_body . zero) (branch FamilyApplication familySpelling familyArguments ih_familyArguments . zero) (branch ConstructorApplication familySpelling constructorSpelling constructorArguments ih_constructorArguments . zero) (branch Eliminator eliminatedFamilySpelling motive scrutinee branches ih_motive ih_scrutinee ih_branches . zero) (branch Match family scrutinee branches ih_scrutinee ih_branches . zero) (branch MatchWith family motive scrutinee branches ih_motive ih_scrutinee ih_branches . zero) (branch IntegerLiteral integerLiteralSpelling . zero) (branch RecordConstruction name origin bindings ih_bindings . zero) (branch RecordAssignment name origin value ih_value . zero) (branch RecordProjection name field origin value ih_value . zero) (branch RecordUpdate name origin value bindings ih_value ih_bindings . zero) (branch LocalLet quantity binder hasAnnotation annotation value body ih_annotation ih_value ih_body . zero) (branch DoBlock effects result body ih_effects ih_result ih_body . zero) (branch DoStep named quantity binder computation continuation ih_computation ih_continuation . zero) (branch DoReturn value ih_value . zero)) -- Removing a synthetic prefix changes coordinates, never token spelling. def syntaxOriginDropPrefix = (lambda unrestricted prefix : Nat . (lambda unrestricted origin : (family SyntaxOrigin) . (eliminate SyntaxOrigin (lambda unrestricted current : (family SyntaxOrigin) . (family SyntaxOrigin)) origin (branch SyntaxOriginUnknown . (constructor SyntaxOrigin SyntaxOriginUnknown)) (branch SyntaxOriginRange start end . (nat-eliminate (lambda unrestricted overlaps : Nat . (family SyntaxOrigin)) (constructor SyntaxOrigin SyntaxOriginRange (Std.Natural/naturalSaturatingSubtract start prefix) (Std.Natural/naturalSaturatingSubtract end prefix)) (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : (family SyntaxOrigin) . (constructor SyntaxOrigin SyntaxOriginUnknown))) (nat-less-than start prefix)))))) def syntaxDropOriginPrefix = (lambda unrestricted prefix : Nat . (lambda unrestricted syntax : (family Syntax) . (eliminate Syntax (lambda unrestricted current : (family Syntax) . (family Syntax)) syntax (branch SyntaxAtom spelling origin . (constructor Syntax SyntaxAtom spelling (syntaxOriginDropPrefix prefix origin))) (branch SyntaxEmpty . (constructor Syntax SyntaxEmpty)) (branch SyntaxCons head tail ih_head ih_tail . (constructor Syntax SyntaxCons ih_head ih_tail)) (branch SyntaxNode children ih_children . (constructor Syntax SyntaxNode ih_children)))))