module Learning.Transition

import Learning.Transformation
import Std.Natural

-- Epoch fences a replaced execution; version identifies one logical state.
-- They are independent: restarting a worker need not advance the learner.
family LearningRound : Type 0
constructor LearningRoundOf
field unrestricted learningMembershipEpoch : Nat
field unrestricted learningStateVersion : Nat

end-family

-- A pure transition has no replay-sensitive external effect. Interaction is
-- explicit and may only be replayed through the retained-boundary protocol.
-- This vocabulary extends the existing transformation modes; it does not
-- infer differentiation or invent an optimizer for a state evolution rule.
family TransitionReplay : Type 0
constructor ReplayPureTransition
constructor ReplayRetainedInteraction
constructor RestartExternalInteraction

end-family

family LearningTransition : Type 0
parameter erased transitionState : Type 0
parameter erased transitionInput : Type 0
parameter erased transitionOutput : Type 0
constructor LearningTransitionOf
field unrestricted transitionMode : (family LearningTransformation)
field unrestricted transitionReplay : (family TransitionReplay)
field unrestricted transitionStep : (pi unrestricted state : transitionState . (pi unrestricted input : transitionInput . transitionOutput))

end-family

def learningRoundEqual =
  (lambda unrestricted left : (family LearningRound) .
    (lambda unrestricted right : (family LearningRound) .
      (eliminate
        LearningRound
        (lambda unrestricted current : (family LearningRound) . Nat)
        left
        (branch
          LearningRoundOf
          leftEpoch
          leftVersion
          .
          (eliminate
            LearningRound
            (lambda unrestricted current : (family LearningRound) . Nat)
            right
            (branch
              LearningRoundOf
              rightEpoch
              rightVersion
              .
              (naturalAnd
                (naturalEqual leftEpoch rightEpoch)
                (naturalEqual leftVersion rightVersion))))))))

def runLearningTransition =
  (lambda erased state : Type 0 .
    (lambda erased input : Type 0 .
      (lambda erased output : Type 0 .
        (lambda unrestricted transition : (family LearningTransition state input output) .
          (eliminate
            LearningTransition
            (lambda unrestricted current : (family LearningTransition state input output) .
              (pi unrestricted oldState : state . (pi unrestricted observation : input . output)))
            transition
            (branch LearningTransitionOf mode replay step . step))))))