221def vaTake =
222 (lambda unrestricted size : ByteCount .
223 (lambda unrestricted allocator : (family VAAllocator) .
224 (eliminate
225 VAAllocator
226 (lambda unrestricted current : (family VAAllocator) . (family VAResult))
227 allocator
228 (branch
229 VAAllocatorValue
230 next
231 .
232 (nat-eliminate
233 (lambda unrestricted requestIsZero : Nat . (family VAResult))
234 (nat-eliminate
235 (lambda unrestricted belowBase : Nat . (family VAResult))
236 (app
237 (lambda unrestricted alignment : (family VAAlignment) .
238 (eliminate
239 VAAlignResult
240 (lambda unrestricted result : (family VAAlignResult) . (family VAResult))
241 (vaAlignUp (stdDeviceAddressValue next) alignment)
242 (branch
243 VAAligned
244 start
245 .
246 (eliminate
247 VAAlignResult
248 (lambda unrestricted result : (family VAAlignResult) . (family VAResult))
249 (vaAlignUp (stdByteCountValue size) alignment)
250 (branch
251 VAAligned
252 extent
253 .
254 (eliminate
255 ModelWord64CheckedResult
256 (lambda unrestricted result : (family ModelWord64CheckedResult) .
257 (family VAResult))
258 (modelWord64AddChecked start extent)
259 (branch
260 ModelWord64CheckedSucceeded
261 nextAddress
262 .
263 (constructor
264 VAResult
265 VASucceeded
266 (constructor
267 VAAllocation
268 VAAllocationValue
269 (stdDeviceAddress start)
270 (stdByteCount extent)
271 alignment
272 (constructor
273 VAAllocator
274 VAAllocatorValue
275 (stdDeviceAddress nextAddress)))))
276 (branch
277 ModelWord64CheckedFailed
278 error
279 .
280 (constructor
281 VAResult
282 VAFailed
283 (constructor VAErrorCode VAAllocatorOverflow)))))
284 (branch
285 VAAlignFailed
286 .
287 (constructor
288 VAResult
289 VAFailed
290 (constructor VAErrorCode VAAlignmentOverflow)))))
291 (branch
292 VAAlignFailed
293 .
294 (constructor VAResult VAFailed (constructor VAErrorCode VAAlignmentOverflow)))))
295 (vaSelectAlignment size))
296 (lambda unrestricted predecessor : Nat .
297 (lambda unrestricted induction : (family VAResult) .
298 (constructor VAResult VAFailed (constructor VAErrorCode VAAllocatorBelowBase))))
299 (modelWord64LessThan (stdDeviceAddressValue next) (stdDeviceAddressValue vaBase)))
300 (lambda unrestricted predecessor : Nat .
301 (lambda unrestricted induction : (family VAResult) .
302 (constructor VAResult VAFailed (constructor VAErrorCode VARequestZero))))
303 (modelWord64IsZero (stdByteCountValue size)))))))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.