2117def sm86EncodeProgramFromIndex =
2118 (lambda unrestricted program : (family SM86Program) .
2119 (eliminate
2120 SM86Program
2121 (lambda unrestricted current : (family SM86Program) .
2122 (pi unrestricted instructionIndex : Nat . (family SM86ProgramEncodingResult)))
2123 program
2124 (branch
2125 SM86ProgramEnd
2126 .
2127 (lambda unrestricted instructionIndex : Nat .
2128 (constructor
2129 SM86ProgramEncodingResult
2130 SM86ProgramEncodingSucceeded
2131 b""
2132 sm86ProgramTelemetryZero)))
2133 (branch
2134 SM86ProgramNext
2135 head
2136 tail
2137 ih_tail
2138 .
2139 (lambda unrestricted instructionIndex : Nat .
2140 (eliminate
2141 SM86InstructionEncodingResult
2142 (lambda unrestricted current : (family SM86InstructionEncodingResult) .
2143 (family SM86ProgramEncodingResult))
2144 (sm86EncodeInstruction head)
2145 (branch
2146 SM86InstructionEncodingSucceeded
2147 headBytes
2148 headTelemetry
2149 .
2150 (eliminate
2151 SM86ProgramEncodingResult
2152 (lambda unrestricted current : (family SM86ProgramEncodingResult) .
2153 (family SM86ProgramEncodingResult))
2154 (ih_tail (succ instructionIndex))
2155 (branch
2156 SM86ProgramEncodingSucceeded
2157 tailBytes
2158 tailTelemetry
2159 .
2160 (constructor
2161 SM86ProgramEncodingResult
2162 SM86ProgramEncodingSucceeded
2163 (bytes-append headBytes tailBytes)
2164 (sm86MergeProgramTelemetry
2165 (sm86ProgramTelemetryInstruction headTelemetry)
2166 tailTelemetry)))
2167 (branch
2168 SM86ProgramEncodingFailed
2169 failureIndex
2170 failure
2171 failureTelemetry
2172 .
2173 (constructor
2174 SM86ProgramEncodingResult
2175 SM86ProgramEncodingFailed
2176 failureIndex
2177 failure
2178 (sm86MergeProgramTelemetry
2179 (sm86ProgramTelemetryInstruction headTelemetry)
2180 failureTelemetry)))))
2181 (branch
2182 SM86InstructionEncodingFieldFailed
2183 error
2184 position
2185 width
2186 detail
2187 fieldTelemetry
2188 .
2189 (constructor
2190 SM86ProgramEncodingResult
2191 SM86ProgramEncodingFailed
2192 instructionIndex
2193 (constructor
2194 SM86InstructionEncodingResult
2195 SM86InstructionEncodingFieldFailed
2196 error
2197 position
2198 width
2199 detail
2200 fieldTelemetry)
2201 (sm86ProgramTelemetryInstruction fieldTelemetry)))
2202 (branch
2203 SM86InstructionEncodingUnsupported
2204 ordinal
2205 .
2206 (constructor
2207 SM86ProgramEncodingResult
2208 SM86ProgramEncodingFailed
2209 instructionIndex
2210 (constructor
2211 SM86InstructionEncodingResult
2212 SM86InstructionEncodingUnsupported
2213 ordinal)
2214 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.