1283def sm86EncodeShuffle =
1284 (lambda unrestricted guard : (family SM86InstructionGuard) .
1285 (lambda unrestricted destination : (family SM86Register) .
1286 (lambda unrestricted source : (family SM86Register) .
1287 (lambda unrestricted lane : Byte .
1288 (lambda unrestricted segment : (family SM86Unsigned32) .
1289 (lambda unrestricted mode : (family SM86ShuffleMode) .
1290 (lambda unrestricted control : (family SM86Control) .
1291 (nat-eliminate
1292 (lambda unrestricted laneInvalid : Nat . (family SM86InstructionEncodingResult))
1293 (sm86EncodeInstructionFields
1294 sm86OpcodeWarpShuffle
1295 guard
1296 control
1297 (sm86InstructionPrependField
1298 sm86InstructionNaturalSixteen
1299 sm86InstructionNaturalEight
1300 (sm86RegisterNatural destination)
1301 (sm86InstructionPrependField
1302 sm86InstructionNaturalTwentyFour
1303 sm86InstructionNaturalEight
1304 (sm86RegisterNatural source)
1305 (sm86InstructionPrependField
1306 sm86InstructionNaturalForty
1307 sm86InstructionNaturalThirteen
1308 (sm86Unsigned32Natural segment)
1309 (sm86InstructionPrependField
1310 sm86InstructionNaturalFiftyThree
1311 sm86InstructionNaturalFive
1312 (byte-to-nat lane)
1313 (sm86InstructionPrependField
1314 sm86InstructionNaturalFiftyEight
1315 sm86InstructionNaturalTwo
1316 (sm86ShuffleModeNatural mode)
1317 (sm86InstructionOneField
1318 sm86InstructionNaturalEightyOne
1319 sm86InstructionNaturalThree
1320 (byte-to-nat (byte 7)))))))))
1321 (lambda unrestricted invalidPredecessor : Nat .
1322 (lambda unrestricted invalidInduction : (family SM86InstructionEncodingResult) .
1323 (sm86InstructionUnsupported (byte-to-nat (byte 20)))))
1324 (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.