1module Compiler.AST
2
3import Compiler.NaturalOperation
4
5-- Synthetic syntax has no source identity; source atoms carry byte ranges.
6family SyntaxOrigin : Type 0
7constructor SyntaxOriginUnknown
8constructor SyntaxOriginRange
9field unrestricted syntaxOriginStart : Nat
10field unrestricted syntaxOriginEnd : Nat
11
12end-family
13
14family Term : Type 0
15constructor Variable
16field unrestricted spelling : Bytes
17constructor Universe
18field unrestricted level : Nat
19constructor NaturalType
20constructor NaturalZero
21constructor NaturalLiteral
22field unrestricted naturalLiteralValue : Nat
23constructor NaturalSuccessor
24recursive unrestricted predecessor
25constructor Application
26recursive unrestricted function
27recursive unrestricted argument
28constructor NaturalArithmetic
29field unrestricted naturalArithmeticOperation : (family CoreNaturalOperation)
30recursive unrestricted naturalArithmeticLeft
31recursive unrestricted naturalArithmeticRight
32constructor Lambda
33field unrestricted quantityTag : Nat
34field unrestricted binderSpelling : Bytes
35recursive unrestricted domain
36recursive unrestricted body
37constructor Pi
38field unrestricted quantityTag : Nat
39field unrestricted binderSpelling : Bytes
40recursive unrestricted domain
41recursive unrestricted codomain
42constructor BytesType
43constructor BytesLiteral
44field unrestricted bytesValue : Bytes
45constructor ByteType
46constructor ByteLiteral
47field unrestricted byteValue : Byte
48constructor TermSequenceEnd
49constructor TermSequenceNext
50recursive unrestricted termSequenceHead
51recursive unrestricted termSequenceTail
52constructor TermEliminatorBranch
53field unrestricted branchConstructorSpelling : Bytes
54recursive unrestricted branchBinderNames
55recursive unrestricted branchBody
56constructor FamilyApplication
57field unrestricted appliedFamilySpelling : Bytes
58recursive unrestricted familyArguments
59constructor ConstructorApplication
60field unrestricted familySpelling : Bytes
61field unrestricted constructorSpelling : Bytes
62recursive unrestricted constructorArguments
63constructor Eliminator
64field unrestricted eliminatedFamilySpelling : Bytes
65recursive unrestricted motive
66recursive unrestricted scrutinee
67recursive unrestricted branches
68constructor Match
69field unrestricted matchedFamilySpelling : Bytes
70recursive unrestricted matchedScrutinee
71recursive unrestricted matchBranches
72constructor MatchWith
73field unrestricted matchedWithFamilySpelling : Bytes
74recursive unrestricted matchedWithMotive
75recursive unrestricted matchedWithScrutinee
76recursive unrestricted matchWithBranches
77constructor IntegerLiteral
78field unrestricted integerLiteralSpelling : Bytes
79constructor RecordConstruction
80field unrestricted recordConstructionFamily : Bytes
81field unrestricted recordConstructionOrigin : (family SyntaxOrigin)
82recursive unrestricted recordConstructionBindings
83constructor RecordAssignment
84field unrestricted recordAssignmentName : Bytes
85field unrestricted recordAssignmentOrigin : (family SyntaxOrigin)
86recursive unrestricted recordAssignmentValue
87constructor RecordProjection
88field unrestricted recordProjectionFamily : Bytes
89field unrestricted recordProjectionField : Bytes
90field unrestricted recordProjectionOrigin : (family SyntaxOrigin)
91recursive unrestricted recordProjectionValue
92constructor RecordUpdate
93field unrestricted recordUpdateFamily : Bytes
94field unrestricted recordUpdateOrigin : (family SyntaxOrigin)
95recursive unrestricted recordUpdateValue
96recursive unrestricted recordUpdateBindings
97constructor LocalLet
98field unrestricted localLetQuantityTag : Nat
99field unrestricted localLetBinderSpelling : Bytes
100field unrestricted localLetHasAnnotation : Nat
101recursive unrestricted localLetAnnotation
102recursive unrestricted localLetValue
103recursive unrestricted localLetBody
104constructor DoBlock
105recursive unrestricted doEffects
106recursive unrestricted doResult
107recursive unrestricted doBody
108constructor DoStep
109field unrestricted doStepNamed : Nat
110field unrestricted doStepQuantityTag : Nat
111field unrestricted doStepBinderSpelling : Bytes
112recursive unrestricted doStepComputation
113recursive unrestricted doStepContinuation
114constructor DoReturn
115recursive unrestricted doReturnValue
116
117end-family
118
119family SourceBytes : Type 0
120constructor SourceEnd
121constructor SourceByte
122field unrestricted sourceByteValue : Byte
123recursive unrestricted sourceByteRest
124
125end-family
126
127def parseHead =
128 (lambda unrestricted input : Bytes .
129 (bytes-eliminate
130 (lambda unrestricted remaining : Bytes . (family Term))
131 (constructor Term Variable b"")
132 (lambda unrestricted head : Byte .
133 (lambda unrestricted tail : Bytes .
134 (lambda unrestricted parsedTail : (family Term) .
135 (nat-eliminate
136 (lambda unrestricted matched : Nat . (family Term))
137 (constructor Term Variable (bytes-cons head tail))
138 (lambda unrestricted predecessor : Nat .
139 (lambda unrestricted induction : (family Term) . (constructor Term NaturalZero)))
140 (byte-equal head (byte 48))))))
141 input))
142
143def sample : (family Term) =
144 (parseHead b"0alpha")
145
146def tokenizeSource =
147 (lambda unrestricted input : Bytes .
148 (bytes-eliminate
149 (lambda unrestricted remaining : Bytes . (family SourceBytes))
150 (constructor SourceBytes SourceEnd)
151 (lambda unrestricted head : Byte .
152 (lambda unrestricted tail : Bytes .
153 (lambda unrestricted tokenizedTail : (family SourceBytes) .
154 (constructor SourceBytes SourceByte head tokenizedTail))))
155 input))
156
157def tokenizedSample : (family SourceBytes) =
158 (tokenizeSource b"0alpha")
159
160def tokenCount : Nat =
161 (eliminate
162 SourceBytes
163 (lambda unrestricted source : (family SourceBytes) . Nat)
164 tokenizedSample
165 (branch SourceEnd . zero)
166 (branch SourceByte sourceByteValue sourceByteRest ih_sourceByteRest . (succ ih_sourceByteRest)))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.