module Coppelius.System

import Coppelius.Learner
import Coppelius.Model
import Coppelius.TrainingRun
import Model.Architecture
import Model.Config

family CoppeliusSystemConfiguration : Type 0
constructor CoppeliusSystemConfigurationValue
field unrestricted coppeliusSystemModel : (family ModelConfig)
field unrestricted coppeliusSystemLearning : (family CoppeliusLearningSemantics)
field unrestricted coppeliusSystemTrainingRun : (family CoppeliusTrainingRunSemantics)
field unrestricted coppeliusSystemCheckpointSchema : (family CoppeliusCheckpointTransportSchema)

end-family

-- The semantic system deliberately stops before any hardware requirement,
-- address plan or launch policy.  Those enter only in Coppelius.Build.*.
def coppeliusSystem : (family CoppeliusSystemConfiguration) =
  (record
    CoppeliusSystemConfiguration
    (coppeliusSystemModel = modelCoppelius)
    (coppeliusSystemLearning = coppeliusLearningSemantics)
    (coppeliusSystemTrainingRun = coppeliusTrainingRunSemantics)
    (coppeliusSystemCheckpointSchema = coppeliusCheckpointSchema))

-- The readable artifact identity is projected through the complete system
-- value so release roots retain one structural connection to model, learner,
-- training-run and checkpoint semantics before whole-program erasure.
def coppeliusSystemIdentity : Bytes =
  (eliminate
    CoppeliusSystemConfiguration
    (lambda unrestricted current : (family CoppeliusSystemConfiguration) . Bytes)
    coppeliusSystem
    (branch
      CoppeliusSystemConfigurationValue
      model
      learning
      trainingRun
      checkpointSchema
      .
      b"coppelius"))