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 359–380

resourceUsageAdd

Full file
359def resourceUsageAdd =
360  (lambda unrestricted total : (family ResourceUsage) .
361    (lambda unrestricted amount : Nat .
362      (eliminate
363        ResourceUsage
364        (lambda unrestricted current : (family ResourceUsage) . (family ResourceUsage))
365        total
366        (branch
367          ResourceUsageWithin
368          value
369          .
370          (eliminate
371            StdBool
372            (lambda unrestricted flag : (family StdBool) . (family ResourceUsage))
373            (stdBoolFromNatural
374              (naturalLessOrEqual amount (naturalSaturatingSubtract resourceWordLimit value)))
375            (branch
376              StdTrue
377              .
378              (constructor ResourceUsage ResourceUsageWithin (naturalAdd value amount)))
379            (branch StdFalse . (constructor ResourceUsage ResourceUsageOverflow))))
380        (branch ResourceUsageOverflow . (constructor ResourceUsage ResourceUsageOverflow)))))

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.