module Runtime.NativeBranch

import Runtime.NativePhysicalProgram
import Runtime.NativePhysicalProgramComposer
import Runtime.NativeLaunchRecipeLoad

-- The branch's distance is derived from its actual command body. Counts refer
-- to records, so packed and aligned images share the same control semantics.
-- The image validator rejects a body which enters or leaves a repeat frame.
def nativeWhenEqual =
  (lambda unrestricted left : (family NativePhysicalOperand) .
    (lambda unrestricted right : (family NativePhysicalOperand) .
      (lambda unrestricted label : Bytes .
        (lambda unrestricted body : (family NativePhysicalCommands) .
          (lambda unrestricted tail : (family NativePhysicalCommands) .
            (nativeLaunchRecipeCommand
              (constructor
                NativePhysicalOperation
                NativePhysicalSkipUnlessEqual
                left
                right
                (nativeLaunchRecipeWord (nativePhysicalCommandsLength body)))
              label
              (nativePhysicalProgramComposeCommandsAppend body tail)))))))

-- The first guard skips the true body and its following forward jump. That
-- jump skips the false body. Nested choices retain the surrounding loop's
-- iteration coordinate, unlike encoding each guard as a counted loop.
def nativeIfEqual =
  (lambda unrestricted left : (family NativePhysicalOperand) .
    (lambda unrestricted right : (family NativePhysicalOperand) .
      (lambda unrestricted label : Bytes .
        (lambda unrestricted whenEqual : (family NativePhysicalCommands) .
          (lambda unrestricted whenDifferent : (family NativePhysicalCommands) .
            (lambda unrestricted tail : (family NativePhysicalCommands) .
              (nativeLaunchRecipeCommand
                (constructor
                  NativePhysicalOperation
                  NativePhysicalSkipUnlessEqual
                  left
                  right
                  (nativeLaunchRecipeWord (succ (nativePhysicalCommandsLength whenEqual))))
                (bytes-append label b":choose")
                (nativePhysicalProgramComposeCommandsAppend
                  whenEqual
                  (nativeWhenEqual
                    (nativeLaunchRecipeImmediate 0)
                    (nativeLaunchRecipeImmediate 1)
                    (bytes-append label b":join")
                    whenDifferent
                    tail)))))))))