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 1030–1040

aarch64FloatUnaryWord

Full file
One-source FP forms: Rd in bits 0-4 and Rn in bits 5-9, so byte 0 carries Rd and Rn's low three bits and byte 1 Rn's high two bits over the form's own byte-1 bits (fsqrt d: 1e61c000; fcvt s<-d: 1e624000; fcvt d<-s: 1e22c000).
1030def aarch64FloatUnaryWord =
1031  (lambda unrestricted byte1 : Nat .
1032    (lambda unrestricted byte2 : Nat .
1033      (lambda unrestricted byte3 : Nat .
1034        (lambda unrestricted destination : (family AArch64FloatRegister) .
1035          (lambda unrestricted source : (family AArch64FloatRegister) .
1036            (aarch64ByteWord
1037              (naturalAdd (aarch64FloatRdByte0 destination) (aarch64FloatRnByte0 source))
1038              (naturalAdd byte1 (aarch64FloatRnByte1 source))
1039              byte2
1040              byte3))))))

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.