Source/Packages

Runtime.DeviceArenaCertificate

packages/execution/src/Runtime/DeviceArenaCertificate.alpha

1,800 lines133 declarations66.8 KiBSHA-256 74ef7fffbf20

def · lines 1072–1132

deviceArenaRepeat

Full file
a repeat's body launches, standing for all its iterations: spans widened by the iteration's deltas, and the repeat's generator added
1072def deviceArenaRepeat =
1073  (lambda unrestricted count : Nat .
1074    (lambda unrestricted extent : Nat .
1075      (lambda unrestricted iteration : (family NvidiaParameterIteration) .
1076        (lambda unrestricted body : (family DeviceArenaLaunches) .
1077          (deviceArenaMapLaunches
1078            (lambda unrestricted launch : (family DeviceArenaLaunch) .
1079              (eliminate
1080                DeviceArenaLaunch
1081                (lambda unrestricted current : (family DeviceArenaLaunch) .
1082                  (family DeviceArenaLaunch))
1083                (eliminate
1084                  NvidiaParameterIteration
1085                  (lambda unrestricted current : (family NvidiaParameterIteration) .
1086                    (family DeviceArenaLaunch))
1087                  iteration
1088                  (branch NvidiaParameterIterationUnchanged . launch)
1089                  (branch
1090                    NvidiaParameterIterationAffine
1091                    adjustments
1092                    .
1093                    (deviceArenaWidenLaunch
1094                      (naturalSaturatingSubtract count 1)
1095                      (deviceArenaFold deviceArenaAccumulate adjustments launch)))
1096                  (branch
1097                    NvidiaParameterIterationQuotientRemainder
1098                    divisor
1099                    remainders
1100                    quotients
1101                    .
1102                    (deviceArenaWidenLaunch
1103                      (naturalDivideUnchecked (naturalSaturatingSubtract count 1) divisor)
1104                      (deviceArenaFold
1105                        deviceArenaAccumulate
1106                        quotients
1107                        (deviceArenaWidenLaunch
1108                          (naturalSaturatingSubtract
1109                            (naturalSelect (naturalLess count divisor) count divisor)
1110                            1)
1111                          (deviceArenaFold deviceArenaAccumulate remainders launch)))))
1112                  (branch NvidiaParameterIterationTable frames . (deviceArenaFrames frames launch)))
1113                (branch
1114                  DeviceArenaLaunchValue
1115                  identity
1116                  base
1117                  generators
1118                  spans
1119                  .
1120                  (constructor
1121                    DeviceArenaLaunch
1122                    DeviceArenaLaunchValue
1123                    identity
1124                    base
1125                    (constructor
1126                      DeviceArenaGenerators
1127                      DeviceArenaGeneratorsNext
1128                      extent
1129                      count
1130                      generators)
1131                    spans))))
1132            body)))))

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.