1868def cgChunkTransfer =
1869 (lambda unrestricted load : Nat .
1870 (lambda unrestricted chunk : Nat .
1871 (cgPhase
1872 cgPhaseCheckpoint
1873 (let unrestricted start =
1874 (naturalMultiply chunk cgChunkBytes)
1875 in
1876 (let unrestricted end =
1877 (cgMinimum (naturalAdd start cgChunkBytes) cgCheckpointBytes)
1878 in
1879 (app
1880 (nat-eliminate
1881 (lambda unrestricted current : Nat .
1882 (pi unrestricted cursor : Nat . (family NvidiaLaunchSchedule)))
1883 (lambda unrestricted cursor : Nat . cgNothing)
1884 (lambda unrestricted p : Nat .
1885 (lambda unrestricted induction : (pi unrestricted cursor : Nat . (family NvidiaLaunchSchedule)) .
1886 (lambda unrestricted cursor : Nat .
1887 (cgIf
1888 (naturalLess cursor end)
1889 (let unrestricted bank =
1890 (cgBankOf cursor)
1891 in
1892 (let unrestricted bankEnd =
1893 (naturalMultiply (succ bank) cgParameterBytes)
1894 in
1895 (let unrestricted bytes =
1896 (cgMinimum
1897 cgPieceBytes
1898 (cgMinimum
1899 (naturalSaturatingSubtract bankEnd cursor)
1900 (naturalSaturatingSubtract end cursor)))
1901 in
1902 (let unrestricted video =
1903 (cgArena
1904 (naturalAdd
1905 (cgBankBase bank)
1906 (naturalSaturatingSubtract
1907 cursor
1908 (naturalMultiply bank cgParameterBytes))))
1909 in
1910 (let unrestricted host =
1911 (cgStaging (naturalSaturatingSubtract cursor start))
1912 in
1913 (cgThen
1914 (cgLaunch
1915 cgImageCopy
1916 (naturalDivideUnchecked
1917 (naturalDivideUnchecked bytes 4)
1918 cgThreads)
1919 1
1920 1
1921 (cgPointer
1922 (cgArgument 0)
1923 (naturalSelect load video host)
1924 (cgPointer
1925 (cgArgument 1)
1926 (naturalSelect load host video)
1927 cgNoSlots)))
1928 (induction (naturalAdd cursor bytes))))))))
1929 cgNothing))))
1930 cgTransferPieces)
1931 start))))))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.