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 1013–1024

aarch64FloatData64Word

Full file
The same two-source form in double precision: the type field (bits 22-23) is 01, the 64 in byte 2.
1013def aarch64FloatData64Word =
1014  (lambda unrestricted opcode : Nat .
1015    (lambda unrestricted destination : (family AArch64FloatRegister) .
1016      (lambda unrestricted left : (family AArch64FloatRegister) .
1017        (lambda unrestricted right : (family AArch64FloatRegister) .
1018          (aarch64ByteWord
1019            (naturalAdd (aarch64FloatRdByte0 destination) (aarch64FloatRnByte0 left))
1020            (naturalAdd
1021              (naturalMultiply opcode 16)
1022              (naturalAdd aarch64Eight (aarch64FloatRnByte1 left)))
1023            (naturalAdd aarch64SixtyFour (naturalAdd aarch64ThirtyTwo (aarch64FloatRegisterCode right)))
1024            30)))))

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.