module Coppelius.Build.PhysicalComponents

import Coppelius.Build.DeviceImages
import Coppelius.Build.Graph
import Coppelius.ArenaPlan
import Coppelius.Build.Placement
import Data.Bytes
import Hardware.Nvidia.SM86.Command.WholeProgramPlan
import Model.Config
import Model.Word64
import Std.Physical

-- The source closure retains device images and the typed launch description.
-- The compiler realizes their wire representation only after target
-- specialization and proof erasure; no file path or intermediate executable
-- participates in this construction.
family CoppeliusPhysicalComponents : Type 0
constructor CoppeliusPhysicalComponentsReady
field unrestricted coppeliusPhysicalProgram : BytesBuilder
field unrestricted coppeliusPhysicalQMD : BytesBuilder
field unrestricted coppeliusPhysicalPushbuffer : BytesBuilder
field unrestricted coppeliusPhysicalGPFIFO : BytesBuilder
constructor CoppeliusPhysicalComponentsFailed
end-family

-- The device placement of the plan's tables and of the host's other
-- buffers outside the video arena: the plan encodes launches against these
-- bases and the host (Coppelius.Build.NativeHost) allocates the buffers at
-- them.

-- over a submission schedule: the plan's own (coppeliusSubmissionSchedule)
-- or the same one profiled (coppeliusProfiledSubmissionSchedule)
def coppeliusWholeProgramPlanFor =
  (lambda unrestricted submissions : (family NvidiaSubmissionSchedule) .
  (lambda unrestricted component : (family NvidiaWholeProgramComponent) .
    (lambda unrestricted architecture : (family ModelWord32) .
      (lambda unrestricted computeClass : (family ModelWord32) .
        (lambda unrestricted spaVersion : (family ModelWord32) .
        (lambda unrestricted qmdTableBytes : Nat .
          (constructor
            NvidiaWholeProgramPlan
            NvidiaWholeProgramPlanValue
            component
            architecture
            computeClass
            spaVersion
            (modelWord64FromNaturalTruncated coppeliusProgramBase)
            (modelWord64FromNaturalTruncated coppeliusQMDBase)
            (modelWord64FromNaturalTruncated coppeliusPushbufferBase)
            (modelWord64FromNaturalTruncated coppeliusSemaphoreBase)
            256
            coppeliusSM86CompatProgramBytesNatural
            coppeliusWholeProgramDeviceRegions
            coppeliusLaunchSchedule
            coppeliusLaunchCount
            qmdTableBytes
            submissions
            coppeliusSubmissionCount
            coppeliusSubmissionReferenceCount)))))))

def coppeliusWholeProgramPlan = (coppeliusWholeProgramPlanFor coppeliusSubmissionSchedule)

def coppeliusWholeProgramComponentFor =
  (lambda unrestricted submissions : (family NvidiaSubmissionSchedule) .
  (lambda unrestricted component : (family NvidiaWholeProgramComponent) .
    (lambda unrestricted architecture : (family ModelWord32) .
      (lambda unrestricted computeClass : (family ModelWord32) .
        (lambda unrestricted spaVersion : (family ModelWord32) .
        (lambda unrestricted qmdTableBytes : Nat .
          (bytes-builder-chunk
            (compiler-native-encode
              (family NvidiaWholeProgramPlan)
              (coppeliusWholeProgramPlanFor submissions
                component architecture computeClass spaVersion qmdTableBytes)))))))))

def coppeliusWholeProgramComponent = (coppeliusWholeProgramComponentFor coppeliusSubmissionSchedule)

def coppeliusPhysicalComponents =
  (lambda unrestricted architecture : (family ModelWord32) .
    (lambda unrestricted computeClass : (family ModelWord32) .
      (lambda unrestricted spaVersion : (family ModelWord32) .
      (lambda unrestricted qmdTableBytes : Nat .
        (constructor
          CoppeliusPhysicalComponents
          CoppeliusPhysicalComponentsReady
          (coppeliusWholeProgramComponent
            (constructor NvidiaWholeProgramComponent NvidiaWholeProgramProgram)
            architecture computeClass spaVersion qmdTableBytes)
          (coppeliusWholeProgramComponent
            (constructor NvidiaWholeProgramComponent NvidiaWholeProgramQMD)
            architecture computeClass spaVersion qmdTableBytes)
          (coppeliusWholeProgramComponent
            (constructor NvidiaWholeProgramComponent NvidiaWholeProgramPushbuffer)
            architecture computeClass spaVersion qmdTableBytes)
          (coppeliusWholeProgramComponent
            (constructor NvidiaWholeProgramComponent NvidiaWholeProgramGPFIFO)
            architecture computeClass spaVersion qmdTableBytes))))))