AlphaGitHub
Source/Packages

Compiler.Planning.Resources

packages/compiler/planning/src/Compiler/Planning/Resources.alpha

636 lines34 declarations25.9 KiBSHA-256 773ccd6b9504
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 419–439

resourceLeaseFits

Full file
419def resourceLeaseFits =
420  (lambda unrestricted graph : (family ResourceGraph) .
421    (lambda unrestricted leases : (family StdList (family ResourceLease)) .
422      (lambda unrestricted lease : (family ResourceLease) .
423        (eliminate
424          ResourceUsage
425          (lambda unrestricted current : (family ResourceUsage) . Nat)
426          (resourceUsageAt leases (resourceLeaseDomain lease) (resourceLeaseBegin lease))
427          (branch
428            ResourceUsageWithin
429            total
430            .
431            (naturalNonzero
432              (resourceCount
433                (family ResourceDomain)
434                (lambda unrestricted domain : (family ResourceDomain) .
435                  (naturalAnd
436                    (naturalEqual (resourceDomainId domain) (resourceLeaseDomain lease))
437                    (resourceDomainAllows domain total)))
438                (resourceGraphDomains graph))))
439          (branch ResourceUsageOverflow . 0)))))

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.