1313def sm121LowerContextOf =
1314 (lambda unrestricted addressing : (family SM121SharedAddressing) .
1315 (lambda unrestricted decoded : (family SM121LowerDecodedList) .
1316 (lambda unrestricted count : Nat .
1317 (let unrestricted named =
1318 (sm121LowerDecodedFold (family SM121LowerMask) decoded sm121LowerMaskEmpty
1319 (lambda unrestricted mask : (family SM121LowerMask) .
1320 (lambda unrestricted item : (family SM121LowerDecoded) .
1321 (sm121LowerMaskAll mask (sm121LowerDecodedRegisters item))))) in
1322 (let unrestricted barriers =
1323 (sm121LowerDecodedFold (family SM121LowerMask) decoded sm121LowerMaskEmpty
1324 (lambda unrestricted mask : (family SM121LowerMask) .
1325 (lambda unrestricted item : (family SM121LowerDecoded) .
1326 (sm121LowerMaskAll mask (sm121LowerDecodedBarriers item))))) in
1327 -- the scoreboards of the instructions that read or write registers
1328 (let unrestricted bearing =
1329 (sm121LowerDecodedFold (family SM121LowerMask) decoded sm121LowerMaskEmpty
1330 (lambda unrestricted mask : (family SM121LowerMask) .
1331 (lambda unrestricted item : (family SM121LowerDecoded) .
1332 (sm121LowerSelect (family SM121LowerMask)
1333 (sm121LowerIsEmpty (sm121LowerDecodedRegisters item))
1334 mask
1335 (sm121LowerMaskAll mask (sm121LowerDecodedBarriers item)))))) in
1336 (let unrestricted unused =
1337 (sm121LowerFirst sm121LowerBarrierCount
1338 (lambda unrestricted barrier : Nat .
1339 (naturalIsZero (sm121LowerMaskHas barriers barrier)))) in
1340 (let unrestricted free =
1341 (lambda unrestricted register : Nat .
1342 (naturalIsZero (sm121LowerMaskHas named register))) in
1343 (let unrestricted freeBarrier =
1344 (naturalSelect (naturalEqual unused sm121LowerBarrierCount)
1345 (nat-subtract sm121LowerBarrierCount 1)
1346 unused) in
1347 (constructor SM121LowerContext SM121LowerContextValue
1348 freeBarrier
1349 (sm121LowerFirst count free)
1350 (sm121LowerFirst (nat-subtract count 1)
1351 (lambda unrestricted register : Nat .
1352 (naturalAnd
1353 (naturalIsZero (nat-modulo register 2))
1354 (naturalAnd (free register) (free (succ register))))))
1355 count
1356 addressing
1357 (sm121LowerWaitAllOf bearing freeBarrier)))))))))))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.