Sequential composition removes the training program's final halt. A
forward branch targeting the old end must now target the first inference
command, not skip that command. Other relative record distances are stable.
originalRestCount comes from the strip fold, avoiding a scan per command.
983def nativePhysicalProgramComposeRemoveFinalHaltJump =
984 (lambda unrestricted originalRestCount : Nat .
985 (lambda unrestricted command : (family NativePhysicalCommand) .
986 (eliminate NativePhysicalCommand
987 (lambda unrestricted current : (family NativePhysicalCommand) . (family NativePhysicalCommand))
988 command
989 (branch NativePhysicalCommandValue original identity .
990 (constructor NativePhysicalCommand NativePhysicalCommandValue
991 (eliminate NativePhysicalOperation
992 (lambda unrestricted current : (family NativePhysicalOperation) . (family NativePhysicalOperation))
993 original
994(branch NativePhysicalSystemCall number arguments payload binding . original)
995(branch NativePhysicalCopyPayloadToState destination extent payload . original)
996(branch NativePhysicalMachineRoutine code arguments binding . original)
997(branch NativePhysicalFencePoll address expected polls . original)
998(branch NativePhysicalTelemetryAppend path record . original)
999(branch NativePhysicalAssertEqual left right error . original)
1000(branch NativePhysicalAssertOneOf observed first second error . original)
1001(branch NativePhysicalHaltSuccess . original)
1002(branch NativePhysicalRepeatBegin count . original)
1003(branch NativePhysicalSkipUnlessEqual left right count . (constructor NativePhysicalOperation NativePhysicalSkipUnlessEqual left right
1004 (modelWord64FromNaturalTruncated
1005 (naturalSaturatingSubtract (modelWord64Natural count)
1006 (naturalEqual (modelWord64Natural count) originalRestCount)))))
1007(branch NativePhysicalRepeatEnd . original)
1008(branch NativePhysicalRepeatEndWhen observed expected . original)
1009(branch NativePhysicalStoreWord64 destination value . original)
1010(branch NativePhysicalFenceWait address expected polls interval . original)
1011(branch NativePhysicalRepeatBeginCounted count . original)
1012(branch NativePhysicalAddWord64 destination left right . original)
1013(branch NativePhysicalFloat64 operation destination left right . original)) identity)))))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.