Module Mod

Require Import Events.
Require Import Values.
Require Import AST.
Require Import Memory.
Require Import Globalenvs.
Require Import Smallstep.
Require Import CoqlibC.
Require Import Skeleton.
Require Import Integers.
Require Import ASTC.
Require Import Maps.

Require Import ModSem.

Set Implicit Arguments.



Module Mod.

  Record t: Type := mk {
    datatype: Type;
    get_sk: datatype -> Sk.t;
    get_modsem: SkEnv.t -> datatype -> ModSem.t;
    data: datatype;
    get_modsem_skenv_spec: forall skenv,
        <<PROJECTED: SkEnv.project skenv data.(get_sk) = data.(get_modsem skenv).(ModSem.skenv)>>;
    get_modsem_skenv_link_spec: forall skenv_link,
        <<EQ: data.(get_modsem skenv_link).(ModSem.skenv_link) = skenv_link>>
  }.

  Lemma get_modsem_projected_sk
        (md: t) skenv
        (INCL: SkEnv.includes skenv (get_sk md (data md))):
      <<PROJECTED: SkEnv.project_spec skenv ((md.(get_sk) md.(data)))
                                      ((md.(get_modsem) skenv) md.(data)).(ModSem.skenv)>>.
Proof.
    erewrite <- get_modsem_skenv_spec. eapply SkEnv.project_impl_spec; et.
  Qed.

  Definition sk (md: t): Sk.t := md.(get_sk) md.(data).

  Definition modsem (md: t) (skenv: SkEnv.t): ModSem.t := md.(get_modsem) skenv md.(data).

  Module Atomic.
  Section Atomic.

    Variable m: t.

    Program Definition trans: t :=
      mk m.(get_sk) (fun ske dat => ModSem.Atomic.trans (m.(get_modsem) ske dat)) m.(data) _ _.
Next Obligation.
exploit get_modsem_skenv_spec; eauto. Qed.
Next Obligation.
exploit get_modsem_skenv_link_spec; eauto. Qed.

  End Atomic.
  End Atomic.

End Mod.

Coercion Mod.sk: Mod.t >-> Sk.t.
Coercion Mod.modsem: Mod.t >-> Funclass.

Hint Unfold Mod.sk Mod.modsem.