1339def sm86EncodeShuffle =
1340 (lambda unrestricted guard : (family SM86InstructionGuard) .
1341 (lambda unrestricted destination : (family SM86Register) .
1342 (lambda unrestricted source : (family SM86Register) .
1343 (lambda unrestricted lane : Byte .
1344 (lambda unrestricted segment : (family SM86Unsigned32) .
1345 (lambda unrestricted mode : (family SM86ShuffleMode) .
1346 (lambda unrestricted control : (family SM86Control) .
1347 (nat-eliminate
1348 (lambda unrestricted laneInvalid : Nat . (family SM86InstructionEncodingResult))
1349 (sm86EncodeInstructionFields
1350 sm86OpcodeWarpShuffle
1351 guard
1352 control
1353 (sm86InstructionPrependField
1354 sm86InstructionNaturalSixteen
1355 sm86InstructionNaturalEight
1356 (sm86RegisterNatural destination)
1357 (sm86InstructionPrependField
1358 sm86InstructionNaturalTwentyFour
1359 sm86InstructionNaturalEight
1360 (sm86RegisterNatural source)
1361 (sm86InstructionPrependField
1362 sm86InstructionNaturalForty
1363 sm86InstructionNaturalThirteen
1364 (sm86Unsigned32Natural segment)
1365 (sm86InstructionPrependField
1366 sm86InstructionNaturalFiftyThree
1367 sm86InstructionNaturalFive
1368 (byte-to-nat lane)
1369 (sm86InstructionPrependField
1370 sm86InstructionNaturalFiftyEight
1371 sm86InstructionNaturalTwo
1372 (sm86ShuffleModeNatural mode)
1373 (sm86InstructionOneField
1374 sm86InstructionNaturalEightyOne
1375 sm86InstructionNaturalThree
1376 (byte-to-nat (byte 7)))))))))
1377 (lambda unrestricted invalidPredecessor : Nat .
1378 (lambda unrestricted invalidInduction : (family SM86InstructionEncodingResult) .
1379 (sm86InstructionUnsupported (byte-to-nat (byte 20)))))
1380 (nat-less-than (byte-to-nat (byte 31)) (byte-to-nat lane))))))))))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.