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 732–745

aarch64ByteMemoryWord

Full file
A byte load or store: an unscaled imm12 offset.
732def aarch64ByteMemoryWord =
733  (lambda unrestricted base2 : Nat .
734    (lambda unrestricted base3 : Nat .
735      (lambda unrestricted register : (family AArch64Register) .
736        (lambda unrestricted address : (family AArch64Register) .
737          (lambda unrestricted offset : Nat .
738            (aarch64EncodeBounded
739              offset
740              aarch64Immediate12Limit
741              (aarch64ByteWord
742                (naturalAdd (aarch64LowFive register) (aarch64RnByte0 address))
743                (naturalAdd (aarch64RnByte1 address) (aarch64Immediate12Byte1 offset))
744                (naturalAdd base2 (aarch64Immediate12Byte2 offset))
745                base3)))))))

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.