module Compiler.AST import Compiler.NaturalOperation -- Synthetic syntax has no source identity; source atoms carry byte ranges. family SyntaxOrigin : Type 0 constructor SyntaxOriginUnknown constructor SyntaxOriginRange field unrestricted syntaxOriginStart : Nat field unrestricted syntaxOriginEnd : Nat end-family family Term : Type 0 constructor Variable field unrestricted spelling : Bytes constructor Universe field unrestricted level : Nat constructor NaturalType constructor NaturalZero constructor NaturalLiteral field unrestricted naturalLiteralValue : Nat constructor NaturalSuccessor recursive unrestricted predecessor constructor Application recursive unrestricted function recursive unrestricted argument constructor NaturalArithmetic field unrestricted naturalArithmeticOperation : (family CoreNaturalOperation) recursive unrestricted naturalArithmeticLeft recursive unrestricted naturalArithmeticRight constructor Lambda field unrestricted quantityTag : Nat field unrestricted binderSpelling : Bytes recursive unrestricted domain recursive unrestricted body constructor Pi field unrestricted quantityTag : Nat field unrestricted binderSpelling : Bytes recursive unrestricted domain recursive unrestricted codomain constructor BytesType constructor BytesLiteral field unrestricted bytesValue : Bytes constructor ByteType constructor ByteLiteral field unrestricted byteValue : Byte constructor TermSequenceEnd constructor TermSequenceNext recursive unrestricted termSequenceHead recursive unrestricted termSequenceTail constructor TermEliminatorBranch field unrestricted branchConstructorSpelling : Bytes recursive unrestricted branchBinderNames recursive unrestricted branchBody constructor FamilyApplication field unrestricted appliedFamilySpelling : Bytes recursive unrestricted familyArguments constructor ConstructorApplication field unrestricted familySpelling : Bytes field unrestricted constructorSpelling : Bytes recursive unrestricted constructorArguments constructor Eliminator field unrestricted eliminatedFamilySpelling : Bytes recursive unrestricted motive recursive unrestricted scrutinee recursive unrestricted branches constructor Match field unrestricted matchedFamilySpelling : Bytes recursive unrestricted matchedScrutinee recursive unrestricted matchBranches constructor MatchWith field unrestricted matchedWithFamilySpelling : Bytes recursive unrestricted matchedWithMotive recursive unrestricted matchedWithScrutinee recursive unrestricted matchWithBranches constructor IntegerLiteral field unrestricted integerLiteralSpelling : Bytes constructor RecordConstruction field unrestricted recordConstructionFamily : Bytes field unrestricted recordConstructionOrigin : (family SyntaxOrigin) recursive unrestricted recordConstructionBindings constructor RecordAssignment field unrestricted recordAssignmentName : Bytes field unrestricted recordAssignmentOrigin : (family SyntaxOrigin) recursive unrestricted recordAssignmentValue constructor RecordProjection field unrestricted recordProjectionFamily : Bytes field unrestricted recordProjectionField : Bytes field unrestricted recordProjectionOrigin : (family SyntaxOrigin) recursive unrestricted recordProjectionValue constructor RecordUpdate field unrestricted recordUpdateFamily : Bytes field unrestricted recordUpdateOrigin : (family SyntaxOrigin) recursive unrestricted recordUpdateValue recursive unrestricted recordUpdateBindings constructor LocalLet field unrestricted localLetQuantityTag : Nat field unrestricted localLetBinderSpelling : Bytes field unrestricted localLetHasAnnotation : Nat recursive unrestricted localLetAnnotation recursive unrestricted localLetValue recursive unrestricted localLetBody constructor DoBlock recursive unrestricted doEffects recursive unrestricted doResult recursive unrestricted doBody constructor DoStep field unrestricted doStepNamed : Nat field unrestricted doStepQuantityTag : Nat field unrestricted doStepBinderSpelling : Bytes recursive unrestricted doStepComputation recursive unrestricted doStepContinuation constructor DoReturn recursive unrestricted doReturnValue end-family family SourceBytes : Type 0 constructor SourceEnd constructor SourceByte field unrestricted sourceByteValue : Byte recursive unrestricted sourceByteRest end-family def parseHead = (lambda unrestricted input : Bytes . (bytes-eliminate (lambda unrestricted remaining : Bytes . (family Term)) (constructor Term Variable b"") (lambda unrestricted head : Byte . (lambda unrestricted tail : Bytes . (lambda unrestricted parsedTail : (family Term) . (nat-eliminate (lambda unrestricted matched : Nat . (family Term)) (constructor Term Variable (bytes-cons head tail)) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family Term) . (constructor Term NaturalZero))) (byte-equal head (byte 48)))))) input)) def sample : (family Term) = (parseHead b"0alpha") def tokenizeSource = (lambda unrestricted input : Bytes . (bytes-eliminate (lambda unrestricted remaining : Bytes . (family SourceBytes)) (constructor SourceBytes SourceEnd) (lambda unrestricted head : Byte . (lambda unrestricted tail : Bytes . (lambda unrestricted tokenizedTail : (family SourceBytes) . (constructor SourceBytes SourceByte head tokenizedTail)))) input)) def tokenizedSample : (family SourceBytes) = (tokenizeSource b"0alpha") def tokenCount : Nat = (eliminate SourceBytes (lambda unrestricted source : (family SourceBytes) . Nat) tokenizedSample (branch SourceEnd . zero) (branch SourceByte sourceByteValue sourceByteRest ih_sourceByteRest . (succ ih_sourceByteRest)))