1614def deviceArenaSubmissionInstances =
1615 (lambda unrestricted runs : (family DeviceArenaRuns) .
1616 (lambda unrestricted submissions : (family NvidiaSubmissionSchedule) .
1617 (eliminate
1618 NvidiaSubmissionSchedule
1619 (lambda unrestricted current : (family NvidiaSubmissionSchedule) .
1620 (pi unrestricted shift : Nat .
1621 (pi unrestricted rest : (family DeviceArenaInstances) . (family DeviceArenaInstances))))
1622 submissions
1623 (branch
1624 NvidiaSubmissionScheduleEmpty
1625 .
1626 (lambda unrestricted shift : Nat .
1627 (lambda unrestricted rest : (family DeviceArenaInstances) . rest)))
1628 (branch
1629 NvidiaSubmissionScheduleOne
1630 batch
1631 .
1632 (lambda unrestricted shift : Nat .
1633 (lambda unrestricted rest : (family DeviceArenaInstances) .
1634 (eliminate
1635 NvidiaSubmissionBatch
1636 (lambda unrestricted current : (family NvidiaSubmissionBatch) .
1637 (family DeviceArenaInstances))
1638 batch
1639 (branch
1640 NvidiaSubmissionBatchValue
1641 identity
1642 semaphore
1643 references
1644 .
1645 (deviceArenaReferenceInstances runs references shift rest))))))
1646 (branch
1647 NvidiaSubmissionScheduleAppend
1648 left
1649 right
1650 il
1651 ir
1652 .
1653 (lambda unrestricted shift : Nat .
1654 (lambda unrestricted rest : (family DeviceArenaInstances) . (il shift (ir shift rest)))))
1655 (branch
1656 NvidiaSubmissionScheduleRepeat
1657 count
1658 referenceStride
1659 semaphoreStride
1660 body
1661 ib
1662 .
1663 (lambda unrestricted shift : Nat .
1664 (lambda unrestricted rest : (family DeviceArenaInstances) .
1665 (app
1666 (nat-eliminate
1667 (lambda unrestricted remaining : Nat .
1668 (pi unrestricted iterationShift : Nat . (family DeviceArenaInstances)))
1669 (lambda unrestricted iterationShift : Nat . rest)
1670 (lambda unrestricted p : Nat .
1671 (lambda unrestricted induction : (pi unrestricted iterationShift : Nat . (family DeviceArenaInstances)) .
1672 (lambda unrestricted iterationShift : Nat .
1673 (ib iterationShift (induction (naturalAdd iterationShift referenceStride))))))
1674 count)
1675 shift))))
1676 -- a profile's releases touch only the semaphore region: the launches
1677 -- are the body's
1678 (branch
1679 NvidiaSubmissionScheduleProfiled
1680 offset
1681 body
1682 ib
1683 .
1684 ib)
1685 -- a timed schedule runs its body's submissions unchanged
1686 (branch
1687 NvidiaSubmissionScheduleTimed
1688 offset
1689 body
1690 ib
1691 .
1692 ib))))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.