188def coppeliusBuildDeviceImagesFrom =
189 (lambda unrestricted images : (family CoppeliusDeviceImages) .
190 (eliminate
191 CoppeliusDeviceImages
192 (lambda unrestricted current : (family CoppeliusDeviceImages) .
193 (pi unrestricted builder : BytesBuilder .
194 (pi unrestricted cursor : Nat .
195 (pi unrestricted count : Nat .
196 (family CoppeliusDeviceImagesBuildResult)))))
197 images
198 (branch
199 CoppeliusDeviceImagesEnd
200 .
201 (lambda unrestricted builder : BytesBuilder .
202 (lambda unrestricted cursor : Nat .
203 (lambda unrestricted count : Nat .
204 (constructor
205 CoppeliusDeviceImagesBuildResult
206 CoppeliusDeviceImagesBuildReady
207 builder
208 cursor
209 count)))))
210 (branch
211 CoppeliusDeviceImagesNext
212 image
213 tail
214 induction
215 .
216 (lambda unrestricted builder : BytesBuilder .
217 (lambda unrestricted cursor : Nat .
218 (lambda unrestricted count : Nat .
219 (eliminate
220 CoppeliusDeviceImage
221 (lambda unrestricted current : (family CoppeliusDeviceImage) .
222 (family CoppeliusDeviceImagesBuildResult))
223 image
224 (branch
225 CoppeliusDeviceImageValue
226 identity
227 program
228 material
229 registers
230 blockX
231 sharedBytes
232 .
233 (nat-eliminate
234 (lambda unrestricted nonempty : Nat .
235 (family CoppeliusDeviceImagesBuildResult))
236 (constructor
237 CoppeliusDeviceImagesBuildResult
238 CoppeliusDeviceImagesBuildFailed
239 identity)
240 (lambda unrestricted materialPredecessor : Nat .
241 (lambda unrestricted materialInduction : (family CoppeliusDeviceImagesBuildResult) .
242 (let unrestricted padding = (coppeliusDevicePadding cursor)
243 in
244 (induction
245 (bytes-builder-append
246 builder
247 (bytes-builder-append
248 (bytes-builder-chunk (coppeliusDeviceZeroBytes padding))
249 (bytes-builder-chunk material)))
250 (naturalAdd cursor (naturalAdd padding (bytes-length material)))
251 (succ count)))))
252 (naturalNonzero (bytes-length material)))))))))))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.