module Learning.Transformation

import Std.Foundation
import Representation.Schema

family LearningTransformation : Type 0
constructor ReverseDifferentiation
constructor RegisteredDerivative
field unrestricted registeredDerivativeComponent : (family ParameterIdentity)
field unrestricted registeredDerivativeIdentity : Bytes
field unrestricted registeredDerivativeConformanceTest : Bytes
constructor LocalUpdate
constructor StateEvolution
end-family

family LearningIncompatibility : Type 0
constructor LearningRepresentationMismatch
constructor LearningEffectMismatch
constructor LearningResourceMismatch
constructor LearningTimingMismatch
end-family

-- Compatibility is structured evidence supplied by composition. Keeping the
-- four dimensions separate makes unsupported cases visible and testable.
family LearningCompatibility : Type 0
constructor LearningCompatibilityOf
field unrestricted learningRepresentationCompatible : (family StdBool)
field unrestricted learningEffectsCompatible : (family StdBool)
field unrestricted learningResourcesCompatible : (family StdBool)
field unrestricted learningTimingCompatible : (family StdBool)
end-family

def learningCompositionFailure =
  (lambda unrestricted problem : (family LearningIncompatibility) .
    (lambda unrestricted transformation : (family LearningTransformation) .
      (constructor StdResult StdFailure
        (family LearningIncompatibility) (family LearningTransformation) problem)))

-- Every learning mode uses the same composition boundary. The result names the
-- first incompatible contract dimension instead of silently selecting a path.
def composeLearningTransformation =
  (lambda unrestricted transformation : (family LearningTransformation) .
    (lambda unrestricted compatibility : (family LearningCompatibility) .
      (eliminate LearningCompatibility
        (lambda unrestricted current : (family LearningCompatibility) .
          (family StdResult (family LearningIncompatibility) (family LearningTransformation)))
        compatibility
        (branch LearningCompatibilityOf representation effects resources timing .
          (eliminate StdBool
            (lambda unrestricted current : (family StdBool) .
              (family StdResult (family LearningIncompatibility) (family LearningTransformation)))
            representation
            (branch StdTrue .
              (eliminate StdBool
                (lambda unrestricted current : (family StdBool) .
                  (family StdResult (family LearningIncompatibility) (family LearningTransformation)))
                effects
                (branch StdTrue .
                  (eliminate StdBool
                    (lambda unrestricted current : (family StdBool) .
                      (family StdResult (family LearningIncompatibility) (family LearningTransformation)))
                    resources
                    (branch StdTrue .
                      (eliminate StdBool
                        (lambda unrestricted current : (family StdBool) .
                          (family StdResult (family LearningIncompatibility) (family LearningTransformation)))
                        timing
                        (branch StdTrue .
                          (constructor StdResult StdSuccess
                            (family LearningIncompatibility) (family LearningTransformation)
                            transformation))
                        (branch StdFalse .
                          (learningCompositionFailure
                            (constructor LearningIncompatibility LearningTimingMismatch)
                            transformation))))
                    (branch StdFalse .
                      (learningCompositionFailure
                        (constructor LearningIncompatibility LearningResourceMismatch)
                        transformation))))
                (branch StdFalse .
                  (learningCompositionFailure
                    (constructor LearningIncompatibility LearningEffectMismatch)
                    transformation))))
            (branch StdFalse .
              (learningCompositionFailure
                (constructor LearningIncompatibility LearningRepresentationMismatch)
                transformation)))))))

def learningCompositionCode =
  (lambda unrestricted result :
      (family StdResult (family LearningIncompatibility) (family LearningTransformation)) .
    (eliminate StdResult
      (lambda unrestricted current :
        (family StdResult (family LearningIncompatibility) (family LearningTransformation)) . Nat)
      result
      (branch StdFailure problem .
        (eliminate LearningIncompatibility
          (lambda unrestricted current : (family LearningIncompatibility) . Nat)
          problem
          (branch LearningRepresentationMismatch . (succ zero))
          (branch LearningEffectMismatch . (succ (succ zero)))
          (branch LearningResourceMismatch . (succ (succ (succ zero))))
          (branch LearningTimingMismatch . (succ (succ (succ (succ zero)))))))
      (branch StdSuccess value . zero)))