Require Export Cminor.
Require Import tactics.
Require Import Events.
Require Export Values.
Require Export Mem.
Load param.

Inductive cminor_loop (g : genv) (sp : val) (body : stmt) : env -> mem -> trace -> env -> mem -> outcome -> Prop :=
| Cminor_loop_loop : forall e m t t1 e1 m1 t2 e2 m2 out,
      exec_stmt g sp e m body t1 e1 m1 Out_normal ->
      cminor_loop g sp body e1 m1 t2 e2 m2 out ->
      t = t1 ** t2 ->
      cminor_loop g sp body e m t e2 m2 out
| Cminor_loop_stop : forall e m t e1 m1 out,
      exec_stmt g sp e m body t e1 m1 out ->
      out <> Out_normal ->
      cminor_loop g sp body e m t e1 m1 out
.

Hint Constructors cminor_loop.

Theorem cminor_loop_exec_Sloop : forall g sp body e m t e2 m2 out,
cminor_loop g sp body e m t e2 m2 out ->
exec_stmt g sp e m (Sloop body) t e2 m2 out.
Proof.
induction 1.
 eapply exec_Sloop_loop.
   eassumption.
  eassumption.
 assumption.
eapply exec_Sloop_stop.
 eassumption.
assumption.
Qed.

(* A failed attempt *)
(*
Theorem exec_Sloop_cminor_loop_buggy : forall g sp body e m t e2 m2 out,
exec_stmt g sp e m (Sloop body) t e2 m2 out ->
cminor_loop g sp body e m t e2 m2 out.
Proof.
induction 1.
*)

(* A successful one *)

Lemma exec_Sloop_cminor_loop_0 : forall g sp loop e m t e2 m2 out,
exec_stmt g sp e m loop t e2 m2 out ->
forall body,
loop = Sloop body ->
cminor_loop g sp body e m t e2 m2 out.
Proof.
induction 1; try (intros; discriminate);
injection 1; intro ; subst s; eauto.
Qed.

Theorem exec_Sloop_cminor_loop : forall g sp body e m t e2 m2 out,
exec_stmt g sp e m (Sloop body) t e2 m2 out ->
cminor_loop g sp body e m t e2 m2 out.
Proof (fun _ _ _ _ _ _ _ _ _ H => exec_Sloop_cminor_loop_0 H (refl_equal _)).