2194def sm86EncodeProgramFromIndex =
2195 (lambda unrestricted program : (family SM86Program) .
2196 (eliminate
2197 SM86Program
2198 (lambda unrestricted current : (family SM86Program) .
2199 (pi unrestricted instructionIndex : Nat . (family SM86ProgramEncodingResult)))
2200 program
2201 (branch
2202 SM86ProgramEnd
2203 .
2204 (lambda unrestricted instructionIndex : Nat .
2205 (constructor
2206 SM86ProgramEncodingResult
2207 SM86ProgramEncodingSucceeded
2208 b""
2209 sm86ProgramTelemetryZero)))
2210 (branch
2211 SM86ProgramNext
2212 head
2213 tail
2214 ih_tail
2215 .
2216 (lambda unrestricted instructionIndex : Nat .
2217 (eliminate
2218 SM86InstructionEncodingResult
2219 (lambda unrestricted current : (family SM86InstructionEncodingResult) .
2220 (family SM86ProgramEncodingResult))
2221 (sm86EncodeInstruction head)
2222 (branch
2223 SM86InstructionEncodingSucceeded
2224 headBytes
2225 headTelemetry
2226 .
2227 (eliminate
2228 SM86ProgramEncodingResult
2229 (lambda unrestricted current : (family SM86ProgramEncodingResult) .
2230 (family SM86ProgramEncodingResult))
2231 (ih_tail (succ instructionIndex))
2232 (branch
2233 SM86ProgramEncodingSucceeded
2234 tailBytes
2235 tailTelemetry
2236 .
2237 (constructor
2238 SM86ProgramEncodingResult
2239 SM86ProgramEncodingSucceeded
2240 (bytes-append headBytes tailBytes)
2241 (sm86MergeProgramTelemetry
2242 (sm86ProgramTelemetryInstruction headTelemetry)
2243 tailTelemetry)))
2244 (branch
2245 SM86ProgramEncodingFailed
2246 failureIndex
2247 failure
2248 failureTelemetry
2249 .
2250 (constructor
2251 SM86ProgramEncodingResult
2252 SM86ProgramEncodingFailed
2253 failureIndex
2254 failure
2255 (sm86MergeProgramTelemetry
2256 (sm86ProgramTelemetryInstruction headTelemetry)
2257 failureTelemetry)))))
2258 (branch
2259 SM86InstructionEncodingFieldFailed
2260 error
2261 position
2262 width
2263 detail
2264 fieldTelemetry
2265 .
2266 (constructor
2267 SM86ProgramEncodingResult
2268 SM86ProgramEncodingFailed
2269 instructionIndex
2270 (constructor
2271 SM86InstructionEncodingResult
2272 SM86InstructionEncodingFieldFailed
2273 error
2274 position
2275 width
2276 detail
2277 fieldTelemetry)
2278 (sm86ProgramTelemetryInstruction fieldTelemetry)))
2279 (branch
2280 SM86InstructionEncodingUnsupported
2281 ordinal
2282 .
2283 (constructor
2284 SM86ProgramEncodingResult
2285 SM86ProgramEncodingFailed
2286 instructionIndex
2287 (constructor
2288 SM86InstructionEncodingResult
2289 SM86InstructionEncodingUnsupported
2290 ordinal)
2291 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.