188def compileOrderedCombine =
189 (lambda erased payload : Type 0 .
190 (lambda unrestricted anchor : (family RegionTransferIdentity) .
191 (lambda unrestricted digest : Bytes .
192 (lambda unrestricted binding : (pi unrestricted stage : (family CombineStage) . (pi unrestricted source : (family CombineReference) . (pi unrestricted destination : (family CombineReference) . (pi unrestricted identity : (family RegionTransferIdentity) . payload)))) .
193 (lambda unrestricted tree : (family OrderedCombineTree) .
194 (eliminate
195 OrderedCombineTree
196 (lambda unrestricted current : (family OrderedCombineTree) .
197 (pi unrestricted base : Nat .
198 (pi unrestricted tail : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
199 (family
200 GlobalProtocol
201 (family OrderedCombineOperation payload)
202 payload
203 (family ProtocolNoDecision)))))
204 tree
205 (branch
206 OrderedCombineLeaf
207 owner
208 .
209 (lambda unrestricted base : Nat .
210 (lambda unrestricted tail : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
211 (combineLocal
212 payload
213 owner
214 (constructor
215 OrderedCombineOperation
216 CombineReadLeaf
217 payload
218 (combineReference owner base 0))
219 tail))))
220 (branch
221 OrderedCombineBranch
222 owner
223 left
224 right
225 leftResult
226 rightResult
227 .
228 (lambda unrestricted base : Nat .
229 (lambda unrestricted tail : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
230 (let unrestricted rightBase =
231 (naturalAdd base (combineNodeCount left))
232 in
233 (let unrestricted node =
234 (naturalAdd rightBase (combineNodeCount right))
235 in
236 (let unrestricted leftInput =
237 (combineReference owner node 1)
238 in
239 (let unrestricted rightInput =
240 (combineReference owner node 2)
241 in
242 (leftResult
243 base
244 (rightResult
245 rightBase
246 (combineMove
247 payload
248 anchor
249 digest
250 (constructor CombineStage CombineReduce)
251 binding
252 (combineTreeReference left base)
253 leftInput
254 (combineMove
255 payload
256 anchor
257 digest
258 (constructor CombineStage CombineReduce)
259 binding
260 (combineTreeReference right rightBase)
261 rightInput
262 (combineLocal
263 payload
264 owner
265 (constructor
266 OrderedCombineOperation
267 CombineApply
268 payload
269 leftInput
270 rightInput
271 (combineReference owner node 0))
272 tail))))))))))))))))))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.