Module device_msp430

Require Import List.
Import ListNotations.
Require Import Relations.
Require Import Coq.Program.Equality.

Require Import util.
Require Import specification.
Require Import ctypes.

Require Import device.
Require Import device_temp.
Require Import device_smclk.
Require Import device_cc2500.

Module dev_msp430 : DEV_Sig.


  Record t_ := MSP430 { temp: dev_temp.t
                     ; smclk: dev_smclk.t
                     ; cc2500: dev_cc2500.t }.
  Definition t := t_.
  Definition init : t := MSP430 dev_temp.init dev_smclk.init dev_cc2500.init.

  Inductive ops_query_ : Type :=
  | q_temp: dev_temp.ops_query -> ops_query_
  | q_smclk: dev_smclk.ops_query -> ops_query_
  | q_cc2500: dev_cc2500.ops_query -> ops_query_.
  Definition ops_query := ops_query_.

  Definition ops_response (q : ops_query): Type :=
    match q with
    | q_temp q => dev_temp.ops_response q
    | q_smclk q => dev_smclk.ops_response q
    | q_cc2500 q => dev_cc2500.ops_response q
    end.

  Inductive op_sem_: forall q: ops_query, t -> ops_response q -> t -> Prop :=
  | op_temp: forall q st r st' s s',
      dev_temp.op_sem q st r st' ->
      s.(temp) = st ->
      s'.(temp) = st' ->
      s.(smclk) = s'.(smclk) ->
      s.(cc2500) = s'.(cc2500) ->
      op_sem_ (q_temp q) s r s'
  | op_smclk: forall q st r st' s s',
      dev_smclk.op_sem q st r st' ->
      s.(smclk) = st ->
      s'.(smclk) = st' ->
      s.(temp) = s'.(temp) ->
      s.(cc2500) = s'.(cc2500) ->
      op_sem_ (q_smclk q) s r s'
  | op_cc2500: forall q st r st' s s',
      dev_cc2500.op_sem q st r st' ->
      s.(cc2500) = st ->
      s'.(cc2500) = st' ->
      s.(temp) = s'.(temp) ->
      s.(smclk) = s'.(smclk) ->
      op_sem_ (q_cc2500 q) s r s'.
  Definition op_sem := op_sem_.

  Definition equiv : relation t :=
    fun x y =>
      dev_temp.equiv x.(temp) y.(temp)
      /\ dev_smclk.equiv x.(smclk) y.(smclk)
      /\ dev_cc2500.equiv x.(cc2500) y.(cc2500).
  Lemma equiv_equiv: equivalence t equiv.

  Lemma op_sem_equiv: forall op_query op_resp dev1 dev2 dev3 dev4,
    op_sem op_query dev1 op_resp dev2 ->
    equiv dev1 dev3 ->
    op_sem op_query dev3 op_resp dev4 ->
    equiv dev2 dev4.

End dev_msp430.