Accelerator.SM121.Lowering

1879def sm121LowerStep =
1880  (lambda unrestricted barrier : Nat .
1881  (lambda unrestricted waitAll : Nat .
1882    (lambda unrestricted waitPlace : Nat .
1883      (lambda unrestricted schedule : (family SM121LowerSchedule) .
1884        (lambda unrestricted op : (family SM121LowerOp) .
1885          (eliminate
1886            SM121LowerSchedule
1887            (lambda unrestricted current : (family SM121LowerSchedule) . (family SM121LowerSchedule))
1888            schedule
1889            (branch SM121LowerScheduleValue time registers predicates loads guardedReads placed .
1890              (eliminate
1891                SM121LowerOp
1892                (lambda unrestricted current : (family SM121LowerOp) . (family SM121LowerSchedule))
1893                op
1894                (branch SM121LowerOpValue low high class reads writes predicateReads predicateWrites constantLoad label join target .
1895                  (let unrestricted before =
1896                    (sm121LowerSelectLazy (family SM121LowerOps) constantLoad
1897                      (lambda unrestricted u : Nat . (sm121LowerDropReuse placed))
1898                      (lambda unrestricted u : Nat . placed)) in
1899                  -- this step's reader row, dispatched once for every cell below
1900                  (let unrestricted row = (sm121LowerReaderRowOf class) in
1901                  (let unrestricted operandsReady =
1902                    (sm121LowerLatest reads (sm121LowerReady registers row)
1903                      (sm121LowerLatest writes (sm121LowerReady registers sm121LowerRowAlu)
1904                        (sm121LowerLatest
1905                          (sm121LowerAppend predicateReads predicateWrites)
1906                          (sm121LowerPredicateReady predicates)
1907                          time))) in
1908                  (let unrestricted required =
1909                    (sm121LowerSelectLazy Nat join
1910                      (lambda unrestricted u : Nat . (sm121LowerMaximum operandsReady
1911                        (sm121LowerDrained registers sm121LowerWriterLongest
1912                          (sm121LowerDrained predicates sm121LowerPredicateWait time))))
1913                      (lambda unrestricted u : Nat . operandsReady)) in
1914                  (let unrestricted deficit = (nat-subtract required time) in
1915                  (let unrestricted issue =
1916                    (naturalSelect (sm121LowerHasPlaced before) deficit zero) in
1917                  (let unrestricted waits =
1918                    (naturalOr join
1919                    (naturalOr
1920                      (sm121LowerAny (sm121LowerAppend reads writes) loads)
1921                      (sm121LowerAny writes guardedReads))) in
1922                  (let unrestricted waited =
1923                    (sm121LowerSelectLazy Nat join
1924                      (lambda unrestricted u : Nat . (sm121LowerWithWaits waitAll high))
1925                      (lambda unrestricted u : Nat . (naturalSelect waits (sm121LowerWithWait waitPlace high) high))) in
1926                  (let unrestricted fixed = (sm121LowerFixed class) in
1927                  (let unrestricted unguarded =
1928                    (naturalAnd
1929                      (naturalAnd (naturalIsZero fixed) (sm121LowerHasResult class))
1930                      (naturalAnd
1931                        (naturalIsZero constantLoad)
1932                        (naturalAnd
1933                          (naturalEqual
1934                            (sm121LowerField waited sm121LowerReadBarrierPlace sm121LowerBarrierSpan)
1935                            sm121LowerNoBarrier)
1936                          (naturalIsZero (sm121LowerIsEmpty reads))))) in
1937                  (let unrestricted placedHigh =
1938                    (naturalSelect unguarded (sm121LowerWithReadBarrier barrier waited) waited) in
1939                  (let unrestricted loadsKept =
1940                    (sm121LowerSelect (family SM121LowerRegisters) waits sm121LowerNone loads) in
1941                  (let unrestricted readsKept =
1942                    (sm121LowerSelect (family SM121LowerRegisters) waits sm121LowerNone guardedReads) in
1943                  (let unrestricted issued = (nat-add time issue) in
1944                  (let unrestricted next = (nat-add issued (sm121LowerStall placedHigh)) in
1945                    (sm121LowerSelect (family SM121LowerSchedule)
1946                      (naturalIsZero (sm121LowerStall placedHigh))
1947                      (constructor SM121LowerSchedule SM121LowerScheduleRefused (constructor SM121LowerRefusal SM121LowerRefusedNoStall))
1948                      (constructor SM121LowerSchedule SM121LowerScheduleValue
1949                        next
1950                        (sm121LowerPendingPrune
1951                          (sm121LowerPendingWrite registers writes issued class fixed)
1952                          next
1953                          sm121LowerLongestReadAfterWrite)
1954                        (sm121LowerPendingPrune
1955                          (sm121LowerPendingWrite predicates predicateWrites issued (constructor SM121LowerClass SM121LowerDualAlu) 1)
1956                          next
1957                          sm121LowerPredicateLatency)
1958                        (sm121LowerSelectLazy (family SM121LowerRegisters) constantLoad
1959                          (lambda unrestricted u : Nat . (sm121LowerUnion loadsKept writes))
1960                          (lambda unrestricted u : Nat . loadsKept))
1961                        (sm121LowerSelectLazy (family SM121LowerRegisters) unguarded
1962                          (lambda unrestricted u : Nat . (sm121LowerUnion readsKept reads))
1963                          (lambda unrestricted u : Nat . readsKept))
1964                        (sm121LowerPush
1965                          (constructor SM121LowerOp SM121LowerOpValue low placedHigh class reads writes
1966                            predicateReads predicateWrites constantLoad label join target)
1967                          (sm121LowerDelay deficit before))))))))))))))))))))))
1968            (branch SM121LowerScheduleRefused refusal . schedule)))))))