(*
include "Csyntax.ma".
include "AST.ma".

nlet rec skippy_s (s:statement) : statement ≝
match s with
[ Ssequence s1 s2 ⇒ Ssequence (skippy_s s1) (skippy_s s2)
| Scall _ _ _ ⇒ Ssequence Sskip s
| _ ⇒ s
].

ndefinition skippy_f : function → function ≝ λf.
mk_function
  (fn_return f)
  (fn_params f)
  (fn_vars f)
  (skippy_s (fn_body f)).

ndefinition skippy_fd : fundef → fundef ≝ λf.
match f with
[ CL_Internal fd ⇒ Internal (skippy_f fd)
| CL_External id args res ⇒ External id args res
].

ndefinition skippy : program → program ≝ transform_program … skippy_fd.
nremark rewrite_skippy : skippy = transform_program … skippy_fd.
//; nqed.
(*
ndefinition skippy : program → program ≝
λp.
mk_program ??
  (map ?? (λfd. match snd ?? fd with
             [ CL_Internal f ⇒
               〈fst ?? fd,
                CL_Internal 
                 (mk_function (fn_return f) (fn_params f) (fn_vars f) (skippy_s (fn_body f)))〉
             | CL_External _ _ _ ⇒ fd ])
    (prog_funct ?? p))
  (prog_main ?? p)
  (prog_vars ?? p).
*)
include "SmallstepExec.ma".
include "CexecIO.ma".

ndefinition Csem ≝ λp:program.mk_execstep
  ?
  ?
  ?
  ?
  (initial_state p)
  final_state
  exec_step.

nlet rec skippy_k (k:cont) : cont ≝
match k with
[ Kstop ⇒ Kstop
| Kseq s k' ⇒ Kseq (skippy_s s) (skippy_k k')
| Kwhile e s k' ⇒ Kwhile e (skippy_s s) (skippy_k k')
| Kdowhile e s k' ⇒ Kdowhile e (skippy_s s) (skippy_k k')
| Kfor2 e s1 s2 k' ⇒ Kfor2 e (skippy_s s1) (skippy_s s2) (skippy_k k')
| Kfor3 e s1 s2 k' ⇒ Kfor3 e (skippy_s s1) (skippy_s s2) (skippy_k k')
| Kswitch k' ⇒ Kswitch (skippy_k k')
| Kcall r f e k' ⇒ Kcall r f e (skippy_k k')
].


include "Plogic/equality.ma".
include "Plogic/connectives.ma".

ndefinition skippy_state : state → state ≝ λs:state.
match s with
[ State f s k e m ⇒ State (skippy_f f) (skippy_s s) (skippy_k k) e m
| Callstate fd args k m ⇒ Callstate (skippy_fd fd) args (skippy_k k) m
| Returnstate res k m ⇒ Returnstate res (skippy_k k) m
].
(*
ndefinition skippyeq : state → state → Prop ≝ λs,s':state.
match s with
[ State f s k e m ⇒
  match s' with
  [ State f' s' k' e' m' ⇒ (skippy_f f) = f' ∧ (skippy_s s) = s' ∧ (skippy_k k) = k' ∧ m = m'
  | _ ⇒ False
  ]
| Callstate fd args k m ⇒
  match s' with
  [ Callstate fd' args' k' m' ⇒ (skippy_fd fd) = fd' ∧ args = args' ∧ (skippy_k k) = k' ∧ m = m'
  | _ ⇒ False
  ]
| Returnstate res k m ⇒
  match s' with
  [ Returnstate res' k' m' ⇒ res = res' ∧ (skippy_k k) = k' ∧ m = m'
  | _ ⇒ False
  ]
].
*)
ndefinition skippy_eq : state → state → Prop ≝ λs,s':state. (skippy_state s) = s'.

ndefinition skippysim ≝ λp:program.
mk_simulation
  (mk_related_semantics
    (Csem p)
    (Csem (skippy p))
    (globalenv Genv ?? p)
    (globalenv Genv ?? (skippy p))
    ?
    ?
    ?)
  ?.
##[ ##3: napply skippy_eq;
##| #st1 st2 r e H; ninversion H; #i m e1 e2; ndestruct; //;
##| #st1 H; ninversion H; #b f H1 H2 e1; @ (skippy_state st1);
    nrewrite > e1; @; //;
    nwhd; nwhd in ⊢ (??%); napply (initial_state_intro … b);
    nrewrite > rewrite_skippy;
    ##[ nrewrite > (find_symbol_transf Genv …); napply H1;
    ##| nrewrite > (find_funct_ptr_transf Genv …); //;
    ##]
##| #st1 st2 t st1' H e;
    @ (skippy_state st1');
    @; //;
    (* simulation proof *)
    (* First, get a hold of the states being executed. *)
    nelim st1 in H e ⊢ %;
    ##[ #f1 s1 k1 e1 m1; nelim s1;
     ##[ nelim k1;
       ##[ nelim f1; #ty args vars body; ncases ty;
         ##[ #H e; nwhd in H;
             nnormalize in e; @ (1); nrewrite < e; nwhd; ndestruct; //;
         ##| ##2,5,6,7,8: #A B H; nwhd in H; napply (False_ind … H);
         ##| ##3,4,9: #A H; nwhd in H; napply (False_ind … H);
         ##]
       ##|

*)