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