344def aarch64EncodeAssemblyFrom :
345 (pi unrestricted assembly : (family AArch64Assembly) .
346 (pi unrestricted labels : (family AArch64LabelTable) .
347 (pi unrestricted offset : Nat . (family AArch64AssemblyResult)))) =
348 (lambda unrestricted assembly : (family AArch64Assembly) .
349 (eliminate
350 AArch64Assembly
351 (lambda unrestricted current : (family AArch64Assembly) .
352 (pi unrestricted labels : (family AArch64LabelTable) .
353 (pi unrestricted offset : Nat . (family AArch64AssemblyResult))))
354 assembly
355 (branch
356 AArch64AssemblyEnd
357 .
358 (lambda unrestricted labels : (family AArch64LabelTable) .
359 (lambda unrestricted offset : Nat .
360 (constructor AArch64AssemblyResult AArch64AssemblyEncoded b""))))
361 (branch
362 AArch64AssemblyEmit
363 instruction
364 tail
365 encodeTail
366 .
367 (lambda unrestricted labels : (family AArch64LabelTable) .
368 (lambda unrestricted offset : Nat .
369 (aarch64PrependWord
370 b""
371 (aarch64EncodeInstruction instruction)
372 (encodeTail labels (naturalAdd offset 4))))))
373 (branch
374 AArch64AssemblyLabel
375 name
376 tail
377 encodeTail
378 .
379 (lambda unrestricted labels : (family AArch64LabelTable) .
380 (lambda unrestricted offset : Nat . (encodeTail labels offset))))
381 (branch
382 AArch64AssemblyBranch
383 target
384 tail
385 encodeTail
386 .
387 (lambda unrestricted labels : (family AArch64LabelTable) .
388 (lambda unrestricted offset : Nat .
389 (aarch64EncodeToLabel
390 target
391 labels
392 offset
393 (lambda unrestricted direction : (family AArch64Direction) .
394 (lambda unrestricted distance : Nat .
395 (constructor AArch64Instruction AArch64Branch direction distance)))
396 (encodeTail labels (naturalAdd offset 4))))))
397 (branch
398 AArch64AssemblyBranchLink
399 target
400 tail
401 encodeTail
402 .
403 (lambda unrestricted labels : (family AArch64LabelTable) .
404 (lambda unrestricted offset : Nat .
405 (aarch64EncodeToLabel
406 target
407 labels
408 offset
409 (lambda unrestricted direction : (family AArch64Direction) .
410 (lambda unrestricted distance : Nat .
411 (constructor AArch64Instruction AArch64BranchLink direction distance)))
412 (encodeTail labels (naturalAdd offset 4))))))
413 (branch
414 AArch64AssemblyBranchIf
415 condition
416 target
417 tail
418 encodeTail
419 .
420 (lambda unrestricted labels : (family AArch64LabelTable) .
421 (lambda unrestricted offset : Nat .
422 (aarch64EncodeToLabel
423 target
424 labels
425 offset
426 (lambda unrestricted direction : (family AArch64Direction) .
427 (lambda unrestricted distance : Nat .
428 (constructor AArch64Instruction AArch64BranchIf condition direction distance)))
429 (encodeTail labels (naturalAdd offset 4))))))
430 (branch
431 AArch64AssemblyCompareBranchIfZero
432 register
433 target
434 tail
435 encodeTail
436 .
437 (lambda unrestricted labels : (family AArch64LabelTable) .
438 (lambda unrestricted offset : Nat .
439 (aarch64EncodeToLabel
440 target
441 labels
442 offset
443 (lambda unrestricted direction : (family AArch64Direction) .
444 (lambda unrestricted distance : Nat .
445 (constructor
446 AArch64Instruction
447 AArch64CompareBranchIfZero
448 register
449 direction
450 distance)))
451 (encodeTail labels (naturalAdd offset 4))))))
452 (branch
453 AArch64AssemblyCompareBranchIfNotZero
454 register
455 target
456 tail
457 encodeTail
458 .
459 (lambda unrestricted labels : (family AArch64LabelTable) .
460 (lambda unrestricted offset : Nat .
461 (aarch64EncodeToLabel
462 target
463 labels
464 offset
465 (lambda unrestricted direction : (family AArch64Direction) .
466 (lambda unrestricted distance : Nat .
467 (constructor
468 AArch64Instruction
469 AArch64CompareBranchIfNotZero
470 register
471 direction
472 distance)))
473 (encodeTail labels (naturalAdd offset 4))))))
474 (branch
475 AArch64AssemblyAddressOf
476 destination
477 target
478 tail
479 encodeTail
480 .
481 (lambda unrestricted labels : (family AArch64LabelTable) .
482 (lambda unrestricted offset : Nat .
483 (aarch64EncodeToLabel
484 target
485 labels
486 offset
487 (lambda unrestricted direction : (family AArch64Direction) .
488 (lambda unrestricted distance : Nat .
489 (constructor
490 AArch64Instruction
491 AArch64AddressRelative
492 destination
493 direction
494 distance)))
495 (encodeTail labels (naturalAdd offset 4))))))))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.