1351def compileMemoryPlan =
1352 (lambda unrestricted arenaBytes : ByteCount .
1353 (lambda unrestricted lifetimes : (family Lifetimes) .
1354 (app
1355 (lambda unrestricted initial : (family LivenessPlacementState) .
1356 (app
1357 (lambda unrestricted lifetimeCount : Nat .
1358 (nat-eliminate
1359 (lambda unrestricted unique : Nat . (family MemoryPlanCompileResult))
1360 (compileMemoryPlanFail
1361 lifetimeCount
1362 arenaBytes
1363 initial
1364 (constructor LivenessErrorCode LifetimeTensorDuplicate))
1365 (lambda unrestricted predecessor : Nat .
1366 (lambda unrestricted induction : (family MemoryPlanCompileResult) .
1367 (eliminate
1368 LivenessOptionalError
1369 (lambda unrestricted current : (family LivenessOptionalError) .
1370 (family MemoryPlanCompileResult))
1371 (firstLifetimeError lifetimes)
1372 (branch
1373 LivenessNoError
1374 .
1375 (eliminate
1376 LivenessPlacementStep
1377 (lambda unrestricted current : (family LivenessPlacementStep) .
1378 (family MemoryPlanCompileResult))
1379 (livenessPlaceAll
1380 (lifetimesSort lifetimes)
1381 (stdByteCountValue arenaBytes)
1382 initial)
1383 (branch
1384 LivenessPlacementAdvanced
1385 state
1386 .
1387 (eliminate
1388 LivenessPlacementState
1389 (lambda unrestricted current : (family LivenessPlacementState) .
1390 (family MemoryPlanCompileResult))
1391 state
1392 (branch
1393 LivenessPlacementStateValue
1394 peak
1395 slots
1396 placements
1397 reused
1398 fresh
1399 .
1400 (app
1401 (lambda unrestricted plan : (family MemoryPlan) .
1402 (eliminate
1403 LivenessValidationResult
1404 (lambda unrestricted result : (family LivenessValidationResult) .
1405 (family MemoryPlanCompileResult))
1406 (validateMemoryPlan plan)
1407 (branch
1408 LivenessValidationPassed
1409 checked
1410 telemetry
1411 .
1412 (constructor
1413 MemoryPlanCompileResult
1414 MemoryPlanCompiled
1415 checked
1416 (livenessCompileTelemetryFor
1417 lifetimeCount
1418 arenaBytes
1419 state
1420 (succ zero)
1421 (constructor LivenessOptionalError LivenessNoError))))
1422 (branch
1423 LivenessValidationFailed
1424 code
1425 telemetry
1426 .
1427 (compileMemoryPlanFail
1428 lifetimeCount
1429 arenaBytes
1430 state
1431 (constructor LivenessErrorCode CompiledPlanRejected)))))
1432 (constructor
1433 MemoryPlan
1434 MemoryPlanValue
1435 arenaBytes
1436 peak
1437 (placementsReverse placements))))))
1438 (branch
1439 LivenessPlacementStopped
1440 code
1441 stopped
1442 .
1443 (compileMemoryPlanFail lifetimeCount arenaBytes stopped code))))
1444 (branch
1445 LivenessSomeError
1446 code
1447 .
1448 (compileMemoryPlanFail lifetimeCount arenaBytes initial code)))))
1449 (lifetimesUnique lifetimes)))
1450 (lifetimeCount lifetimes)))
1451 (constructor
1452 LivenessPlacementState
1453 LivenessPlacementStateValue
1454 (stdByteCount modelWord64Zero)
1455 (constructor LivenessSlots LivenessSlotsEnd)
1456 (constructor Placements PlacementsEnd)
1457 zero
1458 zero))))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.