Module device_temp

Require Import List.
Import ListNotations.
Require Import Relations.
Require Import util.
Require Import device.
Require Import ctypes.

Module dev_temp : DEV_Sig.



  Definition t := unit.
  Definition init : t := tt.

  Inductive ops_query_ : Type := temp_sample : unit -> ops_query_.
  Definition ops_query := ops_query_.

  Definition ops_response (q : ops_query): Type :=
    match q with
    | temp_sample _ => int
    end.

  Inductive op_sem_: forall q: ops_query, t -> ops_response q -> t -> Prop :=
  | sample: forall n,
      op_sem_
        (temp_sample tt) tt
        n tt.

  Definition op_sem := op_sem_.

  Definition equiv : relation t := fun x y => x = y.
  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_temp.