2296def sm86EncodeProgramFromIndex =
2297 (lambda unrestricted program : (family SM86Program) .
2298 (eliminate
2299 SM86Program
2300 (lambda unrestricted current : (family SM86Program) .
2301 (pi unrestricted instructionIndex : Nat . (family SM86ProgramEncodingResult)))
2302 program
2303 (branch
2304 SM86ProgramEnd
2305 .
2306 (lambda unrestricted instructionIndex : Nat .
2307 (constructor
2308 SM86ProgramEncodingResult
2309 SM86ProgramEncodingSucceeded
2310 b""
2311 sm86ProgramTelemetryZero)))
2312 (branch
2313 SM86ProgramNext
2314 head
2315 tail
2316 ih_tail
2317 .
2318 (lambda unrestricted instructionIndex : Nat .
2319 (eliminate
2320 SM86InstructionEncodingResult
2321 (lambda unrestricted current : (family SM86InstructionEncodingResult) .
2322 (family SM86ProgramEncodingResult))
2323 (sm86EncodeInstruction head)
2324 (branch
2325 SM86InstructionEncodingSucceeded
2326 headBytes
2327 headTelemetry
2328 .
2329 (eliminate
2330 SM86ProgramEncodingResult
2331 (lambda unrestricted current : (family SM86ProgramEncodingResult) .
2332 (family SM86ProgramEncodingResult))
2333 (ih_tail (succ instructionIndex))
2334 (branch
2335 SM86ProgramEncodingSucceeded
2336 tailBytes
2337 tailTelemetry
2338 .
2339 (constructor
2340 SM86ProgramEncodingResult
2341 SM86ProgramEncodingSucceeded
2342 (bytes-append headBytes tailBytes)
2343 (sm86MergeProgramTelemetry
2344 (sm86ProgramTelemetryInstruction headTelemetry)
2345 tailTelemetry)))
2346 (branch
2347 SM86ProgramEncodingFailed
2348 failureIndex
2349 failure
2350 failureTelemetry
2351 .
2352 (constructor
2353 SM86ProgramEncodingResult
2354 SM86ProgramEncodingFailed
2355 failureIndex
2356 failure
2357 (sm86MergeProgramTelemetry
2358 (sm86ProgramTelemetryInstruction headTelemetry)
2359 failureTelemetry)))))
2360 (branch
2361 SM86InstructionEncodingFieldFailed
2362 error
2363 position
2364 width
2365 detail
2366 fieldTelemetry
2367 .
2368 (constructor
2369 SM86ProgramEncodingResult
2370 SM86ProgramEncodingFailed
2371 instructionIndex
2372 (constructor
2373 SM86InstructionEncodingResult
2374 SM86InstructionEncodingFieldFailed
2375 error
2376 position
2377 width
2378 detail
2379 fieldTelemetry)
2380 (sm86ProgramTelemetryInstruction fieldTelemetry)))
2381 (branch
2382 SM86InstructionEncodingUnsupported
2383 ordinal
2384 .
2385 (constructor
2386 SM86ProgramEncodingResult
2387 SM86ProgramEncodingFailed
2388 instructionIndex
2389 (constructor
2390 SM86InstructionEncodingResult
2391 SM86InstructionEncodingUnsupported
2392 ordinal)
2393 sm86ProgramTelemetryZero)))))))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.