AlphaGitHub
Source/Packages

Compiler.MachineAArch64

packages/compiler/src/Compiler/MachineAArch64.alpha

1,480 lines362 declarations58.2 KiBSHA-256 16c7a1ba00f1
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 802–814

aarch64SignedField

Full file
Two's-complement field for a signed distance whose magnitude is in `units`.
802def aarch64SignedField =
803  (lambda unrestricted direction : (family AArch64Direction) .
804    (lambda unrestricted units : Nat .
805      (lambda unrestricted modulus : Nat .
806        (eliminate
807          AArch64Direction
808          (lambda unrestricted current : (family AArch64Direction) . Nat)
809          direction
810          (branch AArch64Forward . units)
811          (branch
812            AArch64Backward
813            .
814            (naturalModuloUnchecked (naturalSaturatingSubtract modulus units) modulus))))))

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.