A local move remains an explicit copy. A remote move is prepare,
transfer, consume in that order, and never invokes numerical arithmetic.
The payload binding cannot change the derived canonical identity.
130def combineMove =
131 (lambda erased payload : Type 0 .
132 (lambda unrestricted anchor : (family RegionTransferIdentity) .
133 (lambda unrestricted digest : Bytes .
134 (lambda unrestricted stage : (family CombineStage) .
135 (lambda unrestricted binding : (pi unrestricted stage : (family CombineStage) . (pi unrestricted source : (family CombineReference) . (pi unrestricted destination : (family CombineReference) . (pi unrestricted identity : (family RegionTransferIdentity) . payload)))) .
136 (lambda unrestricted source : (family CombineReference) .
137 (lambda unrestricted destination : (family CombineReference) .
138 (lambda unrestricted tail : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
139 (nat-eliminate
140 (lambda unrestricted flag : Nat .
141 (family
142 GlobalProtocol
143 (family OrderedCombineOperation payload)
144 payload
145 (family ProtocolNoDecision)))
146 (let unrestricted identity =
147 (combineTransferIdentity anchor digest stage source destination)
148 in
149 (let unrestricted value =
150 (binding stage source destination identity)
151 in
152 (combineLocal
153 payload
154 (combineReferenceOwner source)
155 (constructor OrderedCombineOperation CombinePrepare payload source value)
156 (protocolTransfer
157 (family OrderedCombineOperation payload)
158 payload
159 (family ProtocolNoDecision)
160 identity
161 value
162 (combineLocal
163 payload
164 (combineReferenceOwner destination)
165 (constructor
166 OrderedCombineOperation
167 CombineConsume
168 payload
169 value
170 destination)
171 tail)))))
172 (lambda unrestricted prior : Nat .
173 (lambda unrestricted ignored : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
174 (combineLocal
175 payload
176 (combineReferenceOwner source)
177 (constructor
178 OrderedCombineOperation
179 CombineCopy
180 payload
181 source
182 destination)
183 tail)))
184 (naturalEqual
185 (combineReferenceOwner source)
186 (combineReferenceOwner destination)))))))))))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.