2242def sm121LowerCheckStep =
2243 (lambda unrestricted joins : (family SM121LowerRegisters) .
2244 (lambda unrestricted trace : (family SM121LowerTrace) .
2245 (lambda unrestricted op : (family SM121LowerOp) .
2246 (eliminate
2247 SM121LowerTrace
2248 (lambda unrestricted current : (family SM121LowerTrace) . (family SM121LowerTrace))
2249 trace
2250 (branch SM121LowerTraceValue time fixedResults predicates written reading hazards position .
2251 (eliminate
2252 SM121LowerOp
2253 (lambda unrestricted current : (family SM121LowerOp) . (family SM121LowerTrace))
2254 op
2255 (branch SM121LowerOpValue low high class reads writes predicateReads predicateWrites constantLoad label join target .
2256 (let unrestricted mask = (sm121LowerField high sm121LowerWaitPlace sm121LowerWaitSpan) in
2257 (let unrestricted writtenNow = (sm121LowerBoardsWait written mask) in
2258 (let unrestricted readingNow = (sm121LowerBoardsWait reading mask) in
2259 (let unrestricted fixed = (sm121LowerFixed class) in
2260 (let unrestricted row = (sm121LowerReaderRowOf class) in
2261 (let unrestricted early =
2262 (nat-add
2263 (sm121LowerCount reads
2264 (lambda unrestricted register : Nat .
2265 (nat-less-than time (sm121LowerReady fixedResults row register))))
2266 (nat-add
2267 (sm121LowerCount writes
2268 (lambda unrestricted register : Nat .
2269 (nat-less-than time
2270 (sm121LowerReady fixedResults sm121LowerRowAlu register))))
2271 (sm121LowerCount (sm121LowerAppend predicateReads predicateWrites)
2272 (lambda unrestricted predicate : Nat .
2273 (nat-less-than time (sm121LowerPredicateReady predicates predicate)))))) in
2274 (let unrestricted unwaited =
2275 (nat-add
2276 (sm121LowerCount (sm121LowerAppend reads writes) (sm121LowerBoardsHas writtenNow))
2277 (sm121LowerCount writes (sm121LowerBoardsHas readingNow))) in
2278 (let unrestricted variableWrite =
2279 (naturalAnd (naturalIsZero fixed) (naturalIsZero (sm121LowerIsEmpty writes))) in
2280 (let unrestricted writeBarrier =
2281 (sm121LowerField high sm121LowerWriteBarrierPlace sm121LowerBarrierSpan) in
2282 (let unrestricted readBarrier =
2283 (sm121LowerField high sm121LowerReadBarrierPlace sm121LowerBarrierSpan) in
2284 (let unrestricted lateRead =
2285 (naturalAnd
2286 (naturalAnd (naturalIsZero fixed) (sm121LowerHasResult class))
2287 (naturalAnd (naturalIsZero constantLoad) (naturalIsZero (sm121LowerIsEmpty reads)))) in
2288 (constructor SM121LowerTrace SM121LowerTraceValue
2289 (nat-add time (sm121LowerStall high))
2290 (sm121LowerPendingPrune
2291 (sm121LowerPendingWrite fixedResults writes time class fixed)
2292 (nat-add time (sm121LowerStall high))
2293 sm121LowerLongestReadAfterWrite)
2294 (sm121LowerPendingPrune
2295 (sm121LowerPendingWrite predicates predicateWrites time
2296 (constructor SM121LowerClass SM121LowerDualAlu) 1)
2297 (nat-add time (sm121LowerStall high))
2298 sm121LowerPredicateLatency)
2299 (sm121LowerSelect (family SM121LowerBoards) variableWrite
2300 (sm121LowerBoardsAdd writtenNow writes writeBarrier)
2301 writtenNow)
2302 (sm121LowerSelect (family SM121LowerBoards) lateRead
2303 (sm121LowerBoardsAdd readingNow reads
2304 (naturalSelect (naturalEqual readBarrier sm121LowerNoBarrier)
2305 sm121LowerUnguarded readBarrier))
2306 readingNow)
2307 (nat-add hazards
2308 (nat-add
2309 (nat-add (nat-add early unwaited)
2310 (naturalSelect
2311 (naturalAnd variableWrite (naturalEqual writeBarrier sm121LowerNoBarrier))
2312 1 zero))
2313 -- a join: nothing in flight once its waits retire
2314 (sm121LowerSelectLazy Nat (sm121LowerHas joins position)
2315 (lambda unrestricted u : Nat .
2316 (nat-add
2317 (nat-add
2318 (naturalSelect (nat-less-than time (sm121LowerDrained fixedResults sm121LowerWriterLongest zero)) 1 zero)
2319 (naturalSelect (nat-less-than time (sm121LowerDrained predicates sm121LowerPredicateWait zero)) 1 zero))
2320 (nat-add
2321 (naturalSelect (sm121LowerBoardsEmpty writtenNow) zero 1)
2322 (naturalSelect (sm121LowerBoardsEmpty readingNow) zero 1))))
2323 (lambda unrestricted u : Nat . zero))))
2324 (succ position))))))))))))))))))))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.