Require Export core.

Local  Notation π := fst.
Local  Notation π := snd.

Set Implicit Arguments.
Class RosTopicType (RT : Type) {deq : DecEq RT}
each topic is associated with a type of messages
    topicType : RTType

Record Header := mkHeader
how much should message be delayed from the soonest time it can be sent If it is the first message resulting from processing of an event, the soonest time is the time when the processing was compete. If this is a later message, then the soonest time is the time when the provious message was sent
  delay : Q

Section RosCore.

Context `{RosTopicType RosTopic}.

Definition Message := (sigT topicType) × Header .

Require Export MsgHandler.

needs to be made more general. previously it used to depend on a proces. it needs to do so again. such a dependence was useless for the coniductive type because the process will change in the next step.
Definition ProcessTiming :=

Set Implicit Arguments.

Require Export Coq.Unicode.Utf8.

Definition TopicInfo := (list RosTopic) × (list RosTopic).

Definition subscribeTopics (t: TopicInfo ):= fst t.
Definition publishTopics (t: TopicInfo ):= snd t.

Require Export CoRN.model.structures.Qpossec.
Record RosSwNode :=
    process :> Process Message (list Message);

The following is only for reasoning purposes and will not be extracted

    pTiming : QTime × Qpos
processing time and accuracy of message timing, used by ball of MetricSpace

Require Export Program.Basics.
Open Scope program_scope.

Definition procTime :=
  (π) pTiming.

Definition timingAcc :=
  (π) pTiming.

Definition SimplePureProcess (inT outT : RosTopic)
  := (topicType inT) → (topicType outT).

Definition transport {T:Type} {a b:T} {P:TType} (eq:a=b) (pa: P a) : (P b):=
@eq_rect T a P pa b eq.

Definition getPayloadR (topic : RosTopic) (m : sigT topicType) :
option (topicType topic) :=
match m with
| (existT tp pl) ⇒ match (eqdec tp topic) with
                  | left peqSome (@transport _ _ _ (fun tpp ⇒ ( (topicType tpp))) peq pl)
                  | right _None

Definition getPayload (topic : RosTopic) (m : Message) :
option (topicType topic) := getPayloadR topic (fst m).

Definition defHdr := mkHeader 0.

Definition mkImmMesg (outTopic : RosTopic)
  (payload : ( (topicType outTopic))) : Message.
econstructor; eauto;[].
exact defHdr.

Definition liftToMesg {InTopic OutTopic}
  (f : SimplePureProcess InTopic OutTopic)
    : Message → (list Message) :=
( fun inpMesg : Message
match (getPayload InTopic inpMesg ) with
| Some tmesgcons ((mkImmMesg _ (f tmesg))) nil
| Nonenil

Definition mtopicR (m : sigT topicType) :=
(proj1_sigT _ _ m).

Definition mtopic (m : Message) :=
mtopicR (fst m).

Definition mPayload (m : Message) : topicType (mtopic m) :=
(proj2_sigT _ _ (fst m)).

Definition getPayloadOp t := opBind (getPayload t).

Definition validRecvMesg (rn : TopicInfo) (m : Message) :=
  In (mtopic m) (subscribeTopics rn).

Definition validSendMesg (rn : TopicInfo) (m : Message) :=
  In (mtopic m) (publishTopics rn).

Definition mkMesg (outTopic : RosTopic)
  (payload : ( (topicType outTopic))) : (sigT topicType).
econstructor; eauto.

Definition mkDelayedMesg {outTopic : RosTopic}
  (delay : Q) (payload : ( (topicType outTopic))) : Message.
econstructor; eauto;[].
exact (mkHeader delay).

Definition filterMegsByTopic (lm : list Message)
  (topic : RosTopic) : list ( (topicType topic)) :=
flat_map (fun mop2List (getPayload topic m)) lm.

Lemma moveMapInsideFst : tp lm,
  opBind (getPayload tp) (head lm)
  = opBind (getPayloadR tp) (head (map fst lm)).
  intros ?. destruct lm; reflexivity.

Definition PureProcWDelay (inT outT : RosTopic)
  := (topicType inT) → list (Q × (topicType outT)).

Definition delayedLift2Mesg {InTopic OutTopic}
  (f : PureProcWDelay InTopic OutTopic)
   (inpMesg : Message) : (list Message) :=
  match (getPayload InTopic inpMesg ) with
  | Some tmesgmap (λ p, (mkDelayedMesg (π p) (π p))) (f tmesg)
  | Nonenil

End RosCore.