Encode a label-relative word: look the target up, then build the
instruction with the direction and distance from this word.
319def aarch64EncodeToLabel =
320 (lambda unrestricted name : Bytes .
321 (lambda unrestricted labels : (family AArch64LabelTable) .
322 (lambda unrestricted source : Nat .
323 (lambda unrestricted build : (pi unrestricted direction : (family AArch64Direction) . (pi unrestricted distance : Nat . (family AArch64Instruction))) .
324 (lambda unrestricted tailResult : (family AArch64AssemblyResult) .
325 (eliminate
326 AArch64LabelLookupResult
327 (lambda unrestricted lookup : (family AArch64LabelLookupResult) .
328 (family AArch64AssemblyResult))
329 (aarch64LookupLabel name labels)
330 (branch
331 AArch64LabelFound
332 target
333 .
334 (aarch64PrependWord
335 name
336 (aarch64EncodeInstruction
337 (build (aarch64DirectionTo source target) (aarch64DistanceTo source target)))
338 tailResult))
339 (branch
340 AArch64LabelMissing
341 .
342 (constructor AArch64AssemblyResult AArch64AssemblyMissingLabel name))))))))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.