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 763–785

aarch64StackScaledWord

Full file
763def aarch64StackScaledWord =
764  (lambda unrestricted base2 : Nat .
765    (lambda unrestricted base3 : Nat .
766      (lambda unrestricted register : (family AArch64Register) .
767        (lambda unrestricted offset : Nat .
768          (nat-eliminate
769            (lambda unrestricted aligned : Nat . (family AArch64EncodeResult))
770            (constructor AArch64EncodeResult AArch64MisalignedOffset offset)
771            (lambda unrestricted predecessor : Nat .
772              (lambda unrestricted induction : (family AArch64EncodeResult) .
773                (aarch64EncodeBounded
774                  offset
775                  aarch64ScaledOffsetLimit
776                  (aarch64ByteWord
777                    (naturalAdd (aarch64LowFive register) aarch64StackPointerByte0)
778                    (naturalAdd
779                      aarch64StackPointerByte1
780                      (aarch64Immediate12Byte1 (naturalDivideUnchecked offset aarch64Eight)))
781                    (naturalAdd
782                      base2
783                      (aarch64Immediate12Byte2 (naturalDivideUnchecked offset aarch64Eight)))
784                    base3))))
785            (naturalIsZero (naturalModuloUnchecked offset aarch64Eight)))))))

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.