1module Compiler.Codegen
2
3import Compiler.AST
4import Compiler.Lexer
5import Compiler.Parser
6import Compiler.Elaborator
7import Compiler.MachineX86
8
9family CodegenResult : Type 0
10constructor CodeGenerated
11field unrestricted machineCode : Bytes
12constructor CodegenUnboundVariable
13field unrestricted codegenUnboundSpelling : Bytes
14constructor CodegenUnsupportedTerm
15field unrestricted codegenUnsupportedCode : Nat
16
17end-family
18
19def codegenInitialState : (family X86MachineState) =
20 (constructor
21 X86MachineState
22 X86MachineStateValue
23 x86UndefinedClass
24 x86UndefinedClass
25 x86UndefinedClass
26 x86UndefinedClass)
27
28def codegenExitArgumentState : (family X86MachineState) =
29 (constructor
30 X86MachineState
31 X86MachineStateValue
32 x86UndefinedClass
33 x86Word64Class
34 x86UndefinedClass
35 x86UndefinedClass)
36
37def codegenExitState : (family X86MachineState) =
38 (constructor
39 X86MachineState
40 X86MachineStateValue
41 x86Word64Class
42 x86Word64Class
43 x86UndefinedClass
44 x86UndefinedClass)
45
46def codegenExitTail :
47 (family X86Program codegenExitArgumentState codegenExitState x86OneSystemCall) =
48 (constructor
49 X86Program
50 X86ProgramPureNext
51 codegenExitArgumentState
52 codegenExitState
53 codegenExitState
54 x86OneSystemCall
55 (constructor
56 X86Instruction
57 X86MoveEAXImmediate32
58 x86UndefinedClass
59 x86Word64Class
60 x86UndefinedClass
61 x86UndefinedClass
62 (x86Immediate32 (byte 60)))
63 (constructor
64 X86Program
65 X86ProgramSystemCallNext
66 codegenExitState
67 codegenExitState
68 codegenExitState
69 x86NoEffects
70 (constructor X86Instruction X86SystemCall x86Word64Class x86UndefinedClass x86UndefinedClass)
71 (constructor X86Program X86ProgramEnd codegenExitState)))
72
73def lowerClosedNaturalProgram =
74 (lambda unrestricted value : (family ClosedNatural) .
75 (app
76 (eliminate
77 ClosedNatural
78 (lambda unrestricted term : (family ClosedNatural) .
79 (pi unrestricted tail : (family X86Program codegenExitArgumentState codegenExitState x86OneSystemCall) .
80 (family X86Program codegenInitialState codegenExitState x86OneSystemCall)))
81 value
82 (branch
83 ClosedZero
84 .
85 (lambda unrestricted tail : (family X86Program codegenExitArgumentState codegenExitState x86OneSystemCall) .
86 (constructor
87 X86Program
88 X86ProgramPureNext
89 codegenInitialState
90 codegenExitArgumentState
91 codegenExitState
92 x86OneSystemCall
93 (constructor
94 X86Instruction
95 X86ZeroEDI32
96 x86UndefinedClass
97 x86UndefinedClass
98 x86UndefinedClass
99 x86UndefinedClass)
100 tail)))
101 (branch
102 ClosedSuccessor
103 closedPredecessor
104 ih_closedPredecessor
105 .
106 (lambda unrestricted tail : (family X86Program codegenExitArgumentState codegenExitState x86OneSystemCall) .
107 (ih_closedPredecessor
108 (constructor
109 X86Program
110 X86ProgramPureNext
111 codegenExitArgumentState
112 codegenExitArgumentState
113 codegenExitState
114 x86OneSystemCall
115 (constructor
116 X86Instruction
117 X86IncrementRDI64
118 x86UndefinedClass
119 x86UndefinedClass
120 x86UndefinedClass)
121 tail)))))
122 codegenExitTail))
123
124def lowerClosedNaturalValue =
125 (lambda unrestricted value : (family ClosedNatural) .
126 (x86EncodeProgram
127 codegenInitialState
128 codegenExitState
129 x86OneSystemCall
130 (lowerClosedNaturalProgram value)))
131
132def fixedZeroMachineCode : Bytes =
133 (lowerClosedNaturalValue (constructor ClosedNatural ClosedZero))
134
135def lowerByteProgram =
136 (lambda unrestricted value : Byte .
137 (constructor
138 X86Program
139 X86ProgramPureNext
140 codegenInitialState
141 codegenExitArgumentState
142 codegenExitState
143 x86OneSystemCall
144 (constructor
145 X86Instruction
146 X86MoveEDIImmediate32
147 x86UndefinedClass
148 x86UndefinedClass
149 x86UndefinedClass
150 x86UndefinedClass
151 (x86Immediate32 value))
152 codegenExitTail))
153
154def lowerByteValue =
155 (lambda unrestricted value : Byte .
156 (x86EncodeProgram
157 codegenInitialState
158 codegenExitState
159 x86OneSystemCall
160 (lowerByteProgram value)))
161
162def codegenStdoutRAXState : (family X86MachineState) =
163 (constructor
164 X86MachineState
165 X86MachineStateValue
166 x86Word64Class
167 x86UndefinedClass
168 x86UndefinedClass
169 x86UndefinedClass)
170
171def codegenStdoutRDIState : (family X86MachineState) =
172 (constructor
173 X86MachineState
174 X86MachineStateValue
175 x86Word64Class
176 x86Word64Class
177 x86UndefinedClass
178 x86UndefinedClass)
179
180def codegenStdoutRSIState : (family X86MachineState) =
181 (constructor
182 X86MachineState
183 X86MachineStateValue
184 x86Word64Class
185 x86Word64Class
186 x86AddressClass
187 x86UndefinedClass)
188
189def codegenStdoutReadyState : (family X86MachineState) =
190 (constructor
191 X86MachineState
192 X86MachineStateValue
193 x86Word64Class
194 x86Word64Class
195 x86AddressClass
196 x86Word64Class)
197
198def codegenTwoSystemCalls : (family X86EffectTrace) =
199 (constructor X86EffectTrace X86SystemCallEffect x86OneSystemCall)
200
201def lowerBytesProgram =
202 (lambda unrestricted value : Bytes .
203 (constructor
204 X86Program
205 X86ProgramPureNext
206 codegenInitialState
207 codegenStdoutRAXState
208 codegenStdoutReadyState
209 codegenTwoSystemCalls
210 (constructor
211 X86Instruction
212 X86MoveEAXImmediate32
213 x86UndefinedClass
214 x86UndefinedClass
215 x86UndefinedClass
216 x86UndefinedClass
217 (x86Immediate32 (byte 1)))
218 (constructor
219 X86Program
220 X86ProgramPureNext
221 codegenStdoutRAXState
222 codegenStdoutRDIState
223 codegenStdoutReadyState
224 codegenTwoSystemCalls
225 (constructor
226 X86Instruction
227 X86MoveEDIImmediate32
228 x86Word64Class
229 x86UndefinedClass
230 x86UndefinedClass
231 x86UndefinedClass
232 (x86Immediate32 (byte 1)))
233 (constructor
234 X86Program
235 X86ProgramPureNext
236 codegenStdoutRDIState
237 codegenStdoutRSIState
238 codegenStdoutReadyState
239 codegenTwoSystemCalls
240 (constructor
241 X86Instruction
242 X86LoadRSIRIPRelative
243 x86Word64Class
244 x86Word64Class
245 x86UndefinedClass
246 x86UndefinedClass
247 (x86Immediate32 (byte 16)))
248 (constructor
249 X86Program
250 X86ProgramPureNext
251 codegenStdoutRSIState
252 codegenStdoutReadyState
253 codegenStdoutReadyState
254 codegenTwoSystemCalls
255 (constructor
256 X86Instruction
257 X86MoveEDXImmediate32
258 x86Word64Class
259 x86Word64Class
260 x86AddressClass
261 x86UndefinedClass
262 (x86Immediate32 (nat-to-byte (bytes-length value))))
263 (constructor
264 X86Program
265 X86ProgramSystemCallNext
266 codegenStdoutReadyState
267 codegenStdoutReadyState
268 codegenStdoutReadyState
269 x86OneSystemCall
270 (constructor
271 X86Instruction
272 X86SystemCall
273 x86Word64Class
274 x86AddressClass
275 x86Word64Class)
276 (constructor
277 X86Program
278 X86ProgramPureNext
279 codegenStdoutReadyState
280 codegenStdoutReadyState
281 codegenStdoutReadyState
282 x86OneSystemCall
283 (constructor
284 X86Instruction
285 X86ZeroEDI32
286 x86Word64Class
287 x86Word64Class
288 x86AddressClass
289 x86Word64Class)
290 (constructor
291 X86Program
292 X86ProgramPureNext
293 codegenStdoutReadyState
294 codegenStdoutReadyState
295 codegenStdoutReadyState
296 x86OneSystemCall
297 (constructor
298 X86Instruction
299 X86MoveEAXImmediate32
300 x86Word64Class
301 x86Word64Class
302 x86AddressClass
303 x86Word64Class
304 (x86Immediate32 (byte 60)))
305 (constructor
306 X86Program
307 X86ProgramSystemCallNext
308 codegenStdoutReadyState
309 codegenStdoutReadyState
310 codegenStdoutReadyState
311 x86NoEffects
312 (constructor
313 X86Instruction
314 X86SystemCall
315 x86Word64Class
316 x86AddressClass
317 x86Word64Class)
318 (constructor X86Program X86ProgramEnd codegenStdoutReadyState))))))))))
319
320def lowerBytesValue =
321 (lambda unrestricted value : Bytes .
322 (bytes-append
323 (x86EncodeProgram
324 codegenInitialState
325 codegenStdoutReadyState
326 codegenTwoSystemCalls
327 (lowerBytesProgram value))
328 value))
329
330def inlineByteCapacity1 : Bytes =
331 (bytes 0)
332
333def inlineByteCapacity2 : Bytes =
334 (bytes-append inlineByteCapacity1 inlineByteCapacity1)
335
336def inlineByteCapacity4 : Bytes =
337 (bytes-append inlineByteCapacity2 inlineByteCapacity2)
338
339def inlineByteCapacity8 : Bytes =
340 (bytes-append inlineByteCapacity4 inlineByteCapacity4)
341
342def inlineByteCapacity16 : Bytes =
343 (bytes-append inlineByteCapacity8 inlineByteCapacity8)
344
345def inlineByteCapacity32 : Bytes =
346 (bytes-append inlineByteCapacity16 inlineByteCapacity16)
347
348def inlineByteCapacity64 : Bytes =
349 (bytes-append inlineByteCapacity32 inlineByteCapacity32)
350
351def inlineByteCapacity128 : Bytes =
352 (bytes-append inlineByteCapacity64 inlineByteCapacity64)
353
354def compileBytesValue =
355 (lambda unrestricted value : Bytes .
356 (nat-eliminate
357 (lambda unrestricted fits : Nat . (family CodegenResult))
358 (constructor
359 CodegenResult
360 CodegenUnsupportedTerm
361 (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ zero)))))))))))))
362 (lambda unrestricted predecessor : Nat .
363 (lambda unrestricted induction : (family CodegenResult) .
364 (constructor CodegenResult CodeGenerated (lowerBytesValue value))))
365 (nat-less-than (bytes-length value) (succ (bytes-length inlineByteCapacity128)))))
366
367def compileClosedNaturalElaboration =
368 (lambda unrestricted result : (family ClosedNaturalElaboration) .
369 (eliminate
370 ClosedNaturalElaboration
371 (lambda unrestricted value : (family ClosedNaturalElaboration) . (family CodegenResult))
372 result
373 (branch
374 NaturalElaborated
375 elaboratedNatural
376 .
377 (constructor CodegenResult CodeGenerated (lowerClosedNaturalValue elaboratedNatural)))
378 (branch BytesElaborated elaboratedBytes . (compileBytesValue elaboratedBytes))
379 (branch
380 ByteElaborated
381 elaboratedByte
382 .
383 (constructor CodegenResult CodeGenerated (lowerByteValue elaboratedByte)))
384 (branch
385 PrimitivePartial
386 elaboratedPartial
387 .
388 (constructor CodegenResult CodegenUnsupportedTerm (succ (succ (succ zero)))))
389 (branch
390 UnboundVariable
391 unboundSpelling
392 .
393 (constructor CodegenResult CodegenUnboundVariable unboundSpelling))
394 (branch
395 UnsupportedTerm
396 unsupportedCode
397 .
398 (constructor CodegenResult CodegenUnsupportedTerm unsupportedCode))))
399
400def codegenSample : (family CodegenResult) =
401 (compileClosedNaturalElaboration elaboratedParserSample)
402
403def codegenFingerprint : Nat =
404 (eliminate
405 CodegenResult
406 (lambda unrestricted result : (family CodegenResult) . Nat)
407 codegenSample
408 (branch CodeGenerated machineCode . (bytes-length machineCode))
409 (branch CodegenUnboundVariable codegenUnboundSpelling . zero)
410 (branch CodegenUnsupportedTerm codegenUnsupportedCode . zero))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.