744def nativePhysicalTrainingGenerateCheckedAddressBitPatchRoutine =
745 (lambda unrestricted destinationWidth : (family NativePhysicalTrainingBitPatchDestinationWidth) .
746 (lambda unrestricted sourceShift : Nat .
747 (lambda unrestricted destinationShift : Nat .
748 (lambda unrestricted width : Nat .
749 (lambda unrestricted addressBits : Nat .
750 (lambda unrestricted alignmentBits : Nat .
751 (app
752 (lambda unrestricted destinationBits : Nat .
753 (app
754 nativePhysicalTrainingCheckedBitPatchRequire
755 (app naturalNonzero width)
756 (constructor
757 NativePhysicalTrainingCheckedBitPatchParameterError
758 NativePhysicalTrainingCheckedBitPatchWidthZero)
759 (lambda unrestricted ignored : Nat .
760 (app
761 nativePhysicalTrainingCheckedBitPatchRequire
762 (app
763 nativePhysicalTrainingCheckedBitPatchFieldFits
764 sourceShift
765 width
766 (byte-to-nat (byte 64)))
767 (constructor
768 NativePhysicalTrainingCheckedBitPatchParameterError
769 NativePhysicalTrainingCheckedBitPatchSourceBounds)
770 (lambda unrestricted ignored : Nat .
771 (app
772 nativePhysicalTrainingCheckedBitPatchRequire
773 (app
774 nativePhysicalTrainingCheckedBitPatchFieldFits
775 destinationShift
776 width
777 destinationBits)
778 (constructor
779 NativePhysicalTrainingCheckedBitPatchParameterError
780 NativePhysicalTrainingCheckedBitPatchDestinationBounds)
781 (lambda unrestricted ignored : Nat .
782 (app
783 nativePhysicalTrainingCheckedBitPatchRequire
784 (app
785 naturalAnd
786 (app naturalNonzero addressBits)
787 (app naturalLessOrEqual addressBits (byte-to-nat (byte 64))))
788 (constructor
789 NativePhysicalTrainingCheckedBitPatchParameterError
790 NativePhysicalTrainingCheckedBitPatchAddressBits)
791 (lambda unrestricted ignored : Nat .
792 (app
793 nativePhysicalTrainingCheckedBitPatchRequire
794 (app
795 naturalAnd
796 (nat-less-than alignmentBits (byte-to-nat (byte 64)))
797 (app naturalLessOrEqual alignmentBits addressBits))
798 (constructor
799 NativePhysicalTrainingCheckedBitPatchParameterError
800 NativePhysicalTrainingCheckedBitPatchAlignmentBits)
801 (lambda unrestricted ignored : Nat .
802 (constructor
803 NativePhysicalTrainingCheckedBitPatchGeneration
804 NativePhysicalTrainingCheckedBitPatchAssemblyGenerated
805 (app
806 x86NativeAssemble
807 (app
808 nativePhysicalTrainingCheckedBitPatchAssemblyGuard
809 (app
810 nativePhysicalTrainingImmediate64FromWord
811 (app
812 modelWord64Complement
813 (app nativePhysicalTrainingBitMask addressBits)))
814 (app
815 nativePhysicalTrainingImmediate64FromWord
816 (app nativePhysicalTrainingBitMask alignmentBits))
817 (app
818 nativePhysicalTrainingBitPatchAssembly
819 destinationWidth
820 sourceShift
821 destinationShift
822 width)))))))))))))))
823 (eliminate
824 NativePhysicalTrainingBitPatchDestinationWidth
825 (lambda unrestricted current : (family NativePhysicalTrainingBitPatchDestinationWidth) .
826 Nat)
827 destinationWidth
828 (branch NativePhysicalTrainingBitPatchDestination32 . (byte-to-nat (byte 32)))
829 (branch NativePhysicalTrainingBitPatchDestination64 . (byte-to-nat (byte 64)))))))))))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.