an instance of a phase declaring `planes`: every tracked plane they
overlap (under another name) is clobbered, and those some phase carries
(the only ones a later instance can need) are tracked afresh
1325def deviceArenaDeclare =
1326 (lambda unrestricted carried : (family ArenaResidents) .
1327 (lambda unrestricted tracked : (family DeviceArenaTracked) .
1328 (lambda unrestricted planes : (family ArenaResidents) .
1329 (eliminate
1330 ArenaResidents
1331 (lambda unrestricted current : (family ArenaResidents) . (family DeviceArenaTracked))
1332 planes
1333 (branch
1334 ArenaResidentsEnd
1335 .
1336 (eliminate
1337 DeviceArenaTracked
1338 (lambda unrestricted current : (family DeviceArenaTracked) .
1339 (family DeviceArenaTracked))
1340 tracked
1341 (branch DeviceArenaTrackedEnd . deviceArenaTrackedEnd)
1342 (branch
1343 DeviceArenaTrackedNext
1344 head
1345 clobbered
1346 tail
1347 induction
1348 .
1349 (nat-eliminate
1350 (lambda unrestricted redeclared : Nat . (family DeviceArenaTracked))
1351 (constructor
1352 DeviceArenaTracked
1353 DeviceArenaTrackedNext
1354 head
1355 (naturalOr clobbered (deviceArenaOverlapsOther head planes))
1356 induction)
1357 (lambda unrestricted p : Nat .
1358 (lambda unrestricted ignored : (family DeviceArenaTracked) . induction))
1359 (deviceArenaAnyNamed planes head)))))
1360 (branch
1361 ArenaResidentsNext
1362 head
1363 tail
1364 induction
1365 .
1366 (nat-eliminate
1367 (lambda unrestricted kept : Nat . (family DeviceArenaTracked))
1368 induction
1369 (lambda unrestricted p : Nat .
1370 (lambda unrestricted ignored : (family DeviceArenaTracked) .
1371 (constructor DeviceArenaTracked DeviceArenaTrackedNext head 0 induction)))
1372 (deviceArenaAnyNamed carried head)))))))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.