1603def deviceArenaSubmissionInstances =
1604 (lambda unrestricted runs : (family DeviceArenaRuns) .
1605 (lambda unrestricted submissions : (family NvidiaSubmissionSchedule) .
1606 (eliminate
1607 NvidiaSubmissionSchedule
1608 (lambda unrestricted current : (family NvidiaSubmissionSchedule) .
1609 (pi unrestricted shift : Nat .
1610 (pi unrestricted rest : (family DeviceArenaInstances) . (family DeviceArenaInstances))))
1611 submissions
1612 (branch
1613 NvidiaSubmissionScheduleEmpty
1614 .
1615 (lambda unrestricted shift : Nat .
1616 (lambda unrestricted rest : (family DeviceArenaInstances) . rest)))
1617 (branch
1618 NvidiaSubmissionScheduleOne
1619 batch
1620 .
1621 (lambda unrestricted shift : Nat .
1622 (lambda unrestricted rest : (family DeviceArenaInstances) .
1623 (eliminate
1624 NvidiaSubmissionBatch
1625 (lambda unrestricted current : (family NvidiaSubmissionBatch) .
1626 (family DeviceArenaInstances))
1627 batch
1628 (branch
1629 NvidiaSubmissionBatchValue
1630 identity
1631 semaphore
1632 references
1633 .
1634 (deviceArenaReferenceInstances runs references shift rest))))))
1635 (branch
1636 NvidiaSubmissionScheduleAppend
1637 left
1638 right
1639 il
1640 ir
1641 .
1642 (lambda unrestricted shift : Nat .
1643 (lambda unrestricted rest : (family DeviceArenaInstances) . (il shift (ir shift rest)))))
1644 (branch
1645 NvidiaSubmissionScheduleRepeat
1646 count
1647 referenceStride
1648 semaphoreStride
1649 body
1650 ib
1651 .
1652 (lambda unrestricted shift : Nat .
1653 (lambda unrestricted rest : (family DeviceArenaInstances) .
1654 (app
1655 (nat-eliminate
1656 (lambda unrestricted remaining : Nat .
1657 (pi unrestricted iterationShift : Nat . (family DeviceArenaInstances)))
1658 (lambda unrestricted iterationShift : Nat . rest)
1659 (lambda unrestricted p : Nat .
1660 (lambda unrestricted induction : (pi unrestricted iterationShift : Nat . (family DeviceArenaInstances)) .
1661 (lambda unrestricted iterationShift : Nat .
1662 (ib iterationShift (induction (naturalAdd iterationShift referenceStride))))))
1663 count)
1664 shift))))
1665 -- a profile's releases touch only the semaphore region: the launches
1666 -- are the body's
1667 (branch
1668 NvidiaSubmissionScheduleProfiled
1669 offset
1670 body
1671 ib
1672 .
1673 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.