These are protocol states, not claims of physical DMA completion. A native
realization must obtain events from its actual transport and visibility
primitives. One edge's state has one execution owner.
152def advanceTransferPhase =
153 (lambda unrestricted phase : (family TransferPhase) .
154 (lambda unrestricted event : (family TransferEvent) .
155 (eliminate
156 TransferEvent
157 (lambda unrestricted current : (family TransferEvent) .
158 (family StdResult (family TransferFailure) (family TransferPhase)))
159 event
160 (branch
161 TransferBeginRead
162 .
163 (transferRequirePhase 0 (constructor TransferPhase TransferSourceReading) phase))
164 (branch
165 TransferFinishRead
166 .
167 (transferRequirePhase 1 (constructor TransferPhase TransferSourceReleased) phase))
168 (branch
169 TransferValidatePayload
170 .
171 (transferRequirePhase 2 (constructor TransferPhase TransferPayloadReceived) phase))
172 (branch
173 TransferEstablishVisibility
174 .
175 (transferRequirePhase 3 (constructor TransferPhase TransferDestinationVisible) phase))
176 (branch
177 TransferConsume
178 .
179 (transferRequirePhase 4 (constructor TransferPhase TransferConsumed) phase))
180 (branch
181 TransferAbort
182 .
183 (nat-eliminate
184 (lambda unrestricted flag : Nat .
185 (family StdResult (family TransferFailure) (family TransferPhase)))
186 (constructor
187 StdResult
188 StdFailure
189 (family TransferFailure)
190 (family TransferPhase)
191 (constructor TransferFailure TransferIllegalPhase))
192 (lambda unrestricted previous : Nat .
193 (lambda unrestricted ignored : (family StdResult (family TransferFailure) (family TransferPhase)) .
194 (constructor
195 StdResult
196 StdSuccess
197 (family TransferFailure)
198 (family TransferPhase)
199 (constructor TransferPhase TransferAborted))))
200 (naturalLess (transferPhaseCode phase) 5))))))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.