Module System

Require Import EventsC.
Require Import Values.
Require Import AST.
Require Import Memory.
Require Import Globalenvs.
Require Import Smallstep Simulation.
Require Import CoqlibC.

Require Import Mod ModSem Skeleton.

Set Implicit Arguments.

Local Obligation Tactic := ii; des; ss; all_prop_inv; ss.


Section SYSMODSEM.

  Variable skenv_link: SkEnv.t.

  Definition genvtype: Type := SkEnv.t.

  Definition globalenv: genvtype := skenv_link.

  Definition skenv: SkEnv.t :=
    skenv_link.(Genv_map_defs)(fun _ gd =>
                                 match gd with
                                 | Gfun (External ef) => Some (Gfun (Internal (ef.(ef_sig))))
                                 | Gfun _ => None
                                 | Gvar gv => Some gd
                                 end).

  Lemma skenv_globlaenv_equiv: Senv.equiv skenv globalenv.
Proof.
    rr. splits; ii; ss; eauto. unfold skenv, globalenv.
    (* unfold skenv, globalenv. *)
    unfold Genv.block_is_volatile, Genv.find_var_info.
    des_ifs; repeat (apply_all_once Genv_map_defs_def; des); ss; des_ifs.
    eapply_all_once Genv_map_defs_def_inv.
    all_once_fast ltac:(fun H => try erewrite H in *; ss).
  Qed.

  Inductive state: Type :=
  | Callstate
      (fptr: val)
      (vs: list val)
      (m: mem)
  | Returnstate
      (v: val)
      (m: mem).

  Inductive step (se: Senv.t) (ge: genvtype): state -> trace -> state -> Prop :=
  | step_intro
      ef fptr vs m0 v m1 tr
      (FPTR: ge.(Genv.find_funct) fptr = Some (External ef))
      (EXTCALL: external_call ef ge vs m0 tr v m1):
      step se ge (Callstate fptr vs m0) tr (Returnstate v m1).

  Inductive initial_frame (args: Args.t): state -> Prop :=
  | initial_frame_intro
      fptr vs m
      (CSTYLE: args = Args.Cstyle fptr vs m)
    :
      initial_frame args (Callstate fptr vs m).

  Inductive final_frame: state -> Retv.t -> Prop :=
  | final_frame_intro v m :
      final_frame (Returnstate v m) (Retv.Cstyle v m).

  Program Definition modsem: ModSem.t := {|
    ModSem.state := state;
    ModSem.genvtype := genvtype;
    ModSem.step := step;
    ModSem.at_external := bot2;
    ModSem.initial_frame := initial_frame;
    ModSem.final_frame := final_frame;
    ModSem.after_external := bot3;
    ModSem.globalenv:= globalenv;
    ModSem.skenv := skenv;
    ModSem.skenv_link := skenv_link;
  |}.

  Lemma modsem_receptive st:receptive_at modsem st.
Proof.
    econs; ii; ss.
    - inv H. exploit external_call_receptive; eauto. i; des.
      esplits; et. econs; et.
    - inv H. eapply external_call_trace_length; et.
  Qed.

  Lemma modsem_determinate: forall st, determinate_at modsem st.
Proof.
    econs; ii; ss.
    - inv H; inv H0. clarify.
      determ_tac external_call_match_traces.
      esplits; et.
      i; clarify.
      determ_tac external_call_deterministic.
    - inv H. eapply external_call_trace_length; et.
  Qed.

End SYSMODSEM.