The commands from body offset `offset`, in order: each record's offset is
the length of those before it, so shared routine code can be addressed.
1276def nativePhysicalImageEncodeCommandsFrom =
1277 (lambda unrestricted format : (family NativePhysicalImageFormat) .
1278 (lambda unrestricted commands : (family NativePhysicalCommands) .
1279 (eliminate
1280 NativePhysicalCommands
1281 (lambda unrestricted current : (family NativePhysicalCommands) .
1282 (pi unrestricted offset : Nat .
1283 (pi unrestricted held : (family StdList (family NativePhysicalImageRoutineCode)) .
1284 (family NativePhysicalEncodedCommandsResult))))
1285 commands
1286 (branch
1287 NativePhysicalCommandsEnd
1288 .
1289 (lambda unrestricted offset : Nat .
1290 (lambda unrestricted held : (family StdList (family NativePhysicalImageRoutineCode)) .
1291 (constructor
1292 NativePhysicalEncodedCommandsResult
1293 NativePhysicalCommandsEncoded
1294 (constructor
1295 NativePhysicalEncodedCommands
1296 NativePhysicalEncodedCommandsValue
1297 b""
1298 zero
1299 zero
1300 zero
1301 zero)))))
1302 (branch
1303 NativePhysicalCommandsNext
1304 head
1305 tail
1306 induction
1307 .
1308 (lambda unrestricted offset : Nat .
1309 (lambda unrestricted held : (family StdList (family NativePhysicalImageRoutineCode)) .
1310 (eliminate
1311 NativePhysicalCommand
1312 (lambda unrestricted current : (family NativePhysicalCommand) .
1313 (family NativePhysicalEncodedCommandsResult))
1314 head
1315 (branch
1316 NativePhysicalCommandValue
1317 operation
1318 errorIdentity
1319 .
1320 (eliminate
1321 NativePhysicalImageSharedEncoding
1322 (lambda unrestricted current : (family NativePhysicalImageSharedEncoding) .
1323 (family NativePhysicalEncodedCommandsResult))
1324 (nativePhysicalImageEncodeShared format offset held operation errorIdentity)
1325 (branch
1326 NativePhysicalImageSharedEncodingValue
1327 headResult
1328 heldAfter
1329 .
1330 (eliminate
1331 NativePhysicalEncodedCommandResult
1332 (lambda unrestricted current : (family NativePhysicalEncodedCommandResult) .
1333 (family NativePhysicalEncodedCommandsResult))
1334 headResult
1335 (branch
1336 NativePhysicalCommandEncoded
1337 encoded
1338 .
1339 (eliminate
1340 NativePhysicalEncodedCommand
1341 (lambda unrestricted current : (family NativePhysicalEncodedCommand) .
1342 (family NativePhysicalEncodedCommandsResult))
1343 encoded
1344 (branch
1345 NativePhysicalEncodedCommandValue
1346 bytes
1347 payloadBytes
1348 auxiliaryBytes
1349 errorBytes
1350 .
1351 (eliminate
1352 NativePhysicalEncodedCommandsResult
1353 (lambda unrestricted current : (family NativePhysicalEncodedCommandsResult) .
1354 (family NativePhysicalEncodedCommandsResult))
1355 (induction (naturalAdd offset (bytes-length bytes)) heldAfter)
1356 (branch
1357 NativePhysicalCommandsEncoded
1358 encodedTail
1359 .
1360 (eliminate
1361 NativePhysicalEncodedCommands
1362 (lambda unrestricted current : (family NativePhysicalEncodedCommands) .
1363 (family NativePhysicalEncodedCommandsResult))
1364 encodedTail
1365 (branch
1366 NativePhysicalEncodedCommandsValue
1367 tailBytes
1368 tailCount
1369 tailPayload
1370 tailAuxiliary
1371 tailError
1372 .
1373 (constructor
1374 NativePhysicalEncodedCommandsResult
1375 NativePhysicalCommandsEncoded
1376 (constructor
1377 NativePhysicalEncodedCommands
1378 NativePhysicalEncodedCommandsValue
1379 (bytes-append bytes tailBytes)
1380 (succ tailCount)
1381 (naturalAdd payloadBytes tailPayload)
1382 (naturalAdd auxiliaryBytes tailAuxiliary)
1383 (naturalAdd errorBytes tailError))))))
1384 (branch
1385 NativePhysicalCommandsEncodingFailed
1386 error
1387 ordinal
1388 .
1389 (constructor
1390 NativePhysicalEncodedCommandsResult
1391 NativePhysicalCommandsEncodingFailed
1392 error
1393 (succ ordinal)))))))
1394 (branch
1395 NativePhysicalCommandEncodingFailed
1396 error
1397 .
1398 (constructor
1399 NativePhysicalEncodedCommandsResult
1400 NativePhysicalCommandsEncodingFailed
1401 error
1402 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.