Large source region · 5,902 lines
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)))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.