Coppelius.System

1module Coppelius.System
2
3import Coppelius.Learner
4import Coppelius.Model
5import Coppelius.TrainingRun
6import Model.Architecture
7import Model.Config
8
9family CoppeliusSystemConfiguration : Type 0
10constructor CoppeliusSystemConfigurationValue
11field unrestricted coppeliusSystemModel : (family ModelConfig)
12field unrestricted coppeliusSystemLearning : (family CoppeliusLearningSemantics)
13field unrestricted coppeliusSystemTrainingRun : (family CoppeliusTrainingRunSemantics)
14field unrestricted coppeliusSystemCheckpointSchema : (family CoppeliusCheckpointTransportSchema)
15
16end-family
17
18-- The semantic system deliberately stops before any hardware requirement,
19-- address plan or launch policy.  Those enter only in Coppelius.Build.*.
20def coppeliusSystem : (family CoppeliusSystemConfiguration) =
21  (record
22    CoppeliusSystemConfiguration
23    (coppeliusSystemModel = modelCoppelius)
24    (coppeliusSystemLearning = coppeliusLearningSemantics)
25    (coppeliusSystemTrainingRun = coppeliusTrainingRunSemantics)
26    (coppeliusSystemCheckpointSchema = coppeliusCheckpointSchema))
27
28-- The readable artifact identity is projected through the complete system
29-- value so release roots retain one structural connection to model, learner,
30-- training-run and checkpoint semantics before whole-program erasure.
31def coppeliusSystemIdentity : Bytes =
32  (eliminate
33    CoppeliusSystemConfiguration
34    (lambda unrestricted current : (family CoppeliusSystemConfiguration) . Bytes)
35    coppeliusSystem
36    (branch
37      CoppeliusSystemConfigurationValue
38      model
39      learning
40      trainingRun
41      checkpointSchema
42      .
43      b"coppelius"))