Module unseqproof
Semantic preservation for the unseq pass.
Require Import Clight.
Require Import AST.
Require Import Integers.
Require Import Ctypes.
Require Import Maps.
Require Import Cop.
Require Import Coqlib.
Require Import Smallstep.
Require Import Errors.
Require Import Globalenvs.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Floats.
Require Import unseq.
Open Scope error_monad_scope.
Section PRESERVATION.
Variable prog:
Clight.program.
Variable tprog:
Clight.program.
Hypothesis TRANSF:
transf_program prog =
OK tprog.
Let ge :=
Clight.globalenv prog.
Let tge :=
Clight.globalenv tprog.
Usual lemmata on partial program transformations.
Lemma comp_env_preserved:
Clight.genv_cenv tge =
Clight.genv_cenv ge.
Proof.
monadInv TRANSF.
unfold tge;
rewrite <-
H0;
auto.
Qed.
Lemma transf_programs:
AST.transform_partial_program transf_fundef (
program_of_program prog) =
OK (
program_of_program tprog).
Proof.
monadInv TRANSF.
rewrite EQ.
destruct x;
reflexivity.
Qed.
Lemma symbols_preserved:
forall (
s:
ident),
Genv.find_symbol tge s =
Genv.find_symbol ge s.
Proof.
Lemma public_preserved:
forall (
s:
ident),
Genv.public_symbol tge s =
Genv.public_symbol ge s.
Proof.
Lemma varinfo_preserved:
forall b,
Genv.find_var_info tge b =
Genv.find_var_info ge b.
Proof.
Lemma functions_translated:
forall (
v:
val) (
f:
Clight.fundef),
Genv.find_funct ge v =
Some f ->
exists tf,
Genv.find_funct tge v =
Some tf /\
transf_fundef f =
OK tf.
Proof.
Lemma function_ptr_translated:
forall (
b:
block) (
f:
Clight.fundef),
Genv.find_funct_ptr ge b =
Some f ->
exists tf,
Genv.find_funct_ptr tge b =
Some tf /\
transf_fundef f =
OK tf.
Proof.
Lemma type_of_fundef_preserved:
forall fd tfd,
transf_fundef fd =
OK tfd ->
type_of_fundef tfd =
type_of_fundef fd.
Proof.
intros. destruct fd; monadInv H; auto.
monadInv EQ; auto.
Qed.
Lemma alloc_variables_preserved:
forall e m l e'
m',
alloc_variables ge e m l e'
m' ->
alloc_variables tge e m l e'
m'.
Proof.
Lemma bind_parameters_preserved:
forall e m params args m',
bind_parameters ge e m params args m' ->
bind_parameters tge e m params args m'.
Proof.
Evaluation of expressions is unchanged.
Lemma eval_expr_unchanged:
forall e le m a v,
eval_expr ge e le m a v ->
eval_expr tge e le m a v
with eval_lvalue_unchanged:
forall e le m a loc ofs,
eval_lvalue ge e le m a loc ofs ->
eval_lvalue tge e le m a loc ofs.
Proof.
{
destruct a;
intros;
inv H;
try (
inv H0;
fail).
-
econstructor.
-
econstructor.
-
econstructor.
-
econstructor.
-
inv H0.
+
econstructor.
econstructor.
eexact H5.
eexact H1.
+
econstructor.
eapply eval_Evar_global.
eexact H3.
rewrite symbols_preserved.
eexact H6.
exact H1.
-
econstructor.
exact H3.
-
inv H0.
econstructor.
econstructor.
eapply eval_expr_unchanged.
exact H5.
exact H1.
-
econstructor.
eapply eval_lvalue_unchanged.
exact H3.
-
econstructor.
eapply eval_expr_unchanged.
exact H4.
exact H5.
-
econstructor.
eapply eval_expr_unchanged.
exact H5.
eapply eval_expr_unchanged.
exact H6.
rewrite comp_env_preserved.
exact H7.
-
econstructor.
eapply eval_expr_unchanged.
exact H2.
exact H4.
-
inv H0.
+
econstructor.
econstructor.
eapply eval_expr_unchanged.
exact H4.
exact H5.
rewrite comp_env_preserved.
exact H8.
rewrite comp_env_preserved.
exact H9.
exact H1.
+
econstructor.
eapply eval_Efield_union.
eapply eval_expr_unchanged.
exact H4.
exact H7.
rewrite comp_env_preserved.
exact H8.
exact H1.
-
rewrite <-
comp_env_preserved.
econstructor.
-
rewrite <-
comp_env_preserved.
econstructor. }
{
destruct a;
intros;
inv H;
try (
inv H0;
fail).
-
econstructor.
exact H4.
-
eapply eval_Evar_global.
exact H2.
rewrite symbols_preserved.
exact H5.
-
econstructor.
eapply eval_expr_unchanged.
exact H4.
-
econstructor.
eapply eval_expr_unchanged.
exact H3.
exact H4.
rewrite comp_env_preserved.
exact H7.
rewrite comp_env_preserved.
exact H8.
-
eapply eval_Efield_union.
eapply eval_expr_unchanged.
exact H3.
exact H6.
rewrite comp_env_preserved.
exact H7. }
Qed.
:
forall e le m al tyl vl,
eval_exprlist ge e le m al tyl vl ->
eval_exprlist tge e le m al tyl vl.
Proof.
induction 1;
intros.
-
econstructor.
-
econstructor.
+
eapply eval_expr_unchanged;
eauto.
+
eapply H0.
+
eapply IHeval_exprlist.
Qed.
To avoid infinite stuttering, a decreasing measure
must be defined. It respects the following inequalities:
m (Sskip, Kseq s2 k) < m (Ssequence Sskip s2, k)
m (s2, k) < m (Sskip, Kseq s2 k)
Fixpoint num_stmt (
s:
statement):
nat :=
match s with
|
Ssequence s1 s2 =>
S (
S (
num_stmt s1 +
num_stmt s2))
|
_ =>
O
end.
Fixpoint num_cont (
k:
cont):
nat :=
match k with
|
Kseq s k =>
S (
num_cont k +
num_stmt s)
|
_ =>
O
end.
Definition measure (
st:
Clight.state):
nat :=
match st with
|
State _ s k _ _ _ =>
S (
num_stmt s +
num_cont k)
|
_ =>
O
end.
Lemma unseq_break_context:
forall k,
unseq k Sbreak =
unseq (
context k)
Sbreak.
Proof.
induction k; simpl; auto.
Qed.
Lemma unseq_continue_context:
forall k,
unseq k Scontinue =
unseq (
context'
k)
Scontinue.
Proof.
induction k; simpl; auto.
Qed.
Matching statements and continuations.
Inductive match_stmt_cont:
statement ->
statement ->
cont ->
cont ->
Prop :=
|
match_assign:
forall a1 a2 k tk,
match_stmt_cont Sskip Sskip k tk ->
match_stmt_cont (
Sassign a1 a2) (
Sassign a1 a2)
k tk
|
match_set:
forall id a k tk,
match_stmt_cont Sskip Sskip k tk ->
match_stmt_cont (
Sset id a) (
Sset id a)
k tk
|
match_call:
forall optid a al k tk,
match_stmt_cont Sskip Sskip k tk ->
match_stmt_cont (
Scall optid a al) (
Scall optid a al)
k tk
|
match_builtin:
forall optid ef tyargs al k tk,
match_stmt_cont Sskip Sskip k tk ->
match_stmt_cont (
Sbuiltin optid ef tyargs al) (
Sbuiltin optid ef tyargs al)
k tk
|
match_skip_seq1:
forall s s'
k tk,
match_stmt_cont s s'
k tk ->
match_stmt_cont Sskip Sskip (
Kseq s k) (
Kseq s'
tk)
|
match_skip_seq2:
forall s s'
k tk,
match_stmt_cont s s'
k tk ->
match_stmt_cont Sskip s' (
Kseq s k)
tk
|
match_seq1:
forall s s'
k tk,
unseq k s =
OK s' ->
match_stmt_cont Sskip s' (
Kseq s k)
tk ->
match_stmt_cont (
Ssequence Sskip s)
s'
k tk
|
match_seq2:
forall s1 s2 s1'
s2'
k tk,
unseq (
Kseq s2 k)
s1 =
OK s1' ->
match_stmt_cont s1 s1' (
Kseq s2 k) (
Kseq s2'
tk) ->
match_stmt_cont s2 s2'
k tk ->
We cannot guarantee s1 <> Sskip due to the semantics of
Sswitch: seq_of_labeled_statement (LScons (Some 42) Sskip LSnil) = Ssequence Sskip Sskip
match_stmt_cont (
Ssequence s1 s2) (
Ssequence s1'
s2')
k tk
|
match_continue_seq1:
forall s s'
k tk,
unseq k Scontinue =
OK Scontinue ->
match_stmt_cont Scontinue Scontinue k tk ->
match_stmt_cont Scontinue Scontinue (
Kseq s k) (
Kseq s'
tk)
|
match_continue_seq2:
forall s k tk,
unseq k Scontinue =
OK Scontinue ->
match_stmt_cont Scontinue Scontinue k tk ->
match_stmt_cont Scontinue Scontinue (
Kseq s k)
tk
|
match_break_seq1:
forall s s'
k tk,
unseq k Sbreak =
OK Sbreak ->
match_stmt_cont Sbreak Sbreak k tk ->
match_stmt_cont Sbreak Sbreak (
Kseq s k) (
Kseq s'
tk)
|
match_break_seq2:
forall s k tk,
unseq k Sbreak =
OK Sbreak ->
match_stmt_cont Sbreak Sbreak k tk ->
match_stmt_cont Sbreak Sbreak (
Kseq s k)
tk
|
match_ifthenelse:
forall e s1 s2 s1'
s2'
k tk,
unseq k s1 =
OK s1' ->
unseq k s2 =
OK s2' ->
match_stmt_cont s1 s1'
k tk ->
match_stmt_cont s2 s2'
k tk ->
match_stmt_cont (
Sifthenelse e s1 s2) (
Sifthenelse e s1'
s2')
k tk
|
match_loop:
forall s1 s2 s1'
s2'
k tk,
unseq (
Kloop1 s1 s2 k)
s1 =
OK s1' ->
unseq (
Kloop2 s1 s2 k)
s2 =
OK s2' ->
match_stmt_cont s1 s1' (
Kloop1 s1 s2 k) (
Kloop1 s1'
s2'
tk) ->
match_stmt_cont (
Sloop s1 s2) (
Sloop s1'
s2')
k tk
|
match_skip_loop1:
forall s1 s2 s1'
s2'
k tk,
unseq (
Kloop1 s1 s2 k)
s1 =
OK s1' ->
unseq (
Kloop2 s1 s2 k)
s2 =
OK s2' ->
match_stmt_cont s2 s2' (
Kloop2 s1 s2 k) (
Kloop2 s1'
s2'
tk) ->
match_stmt_cont Sskip Sskip (
Kloop1 s1 s2 k) (
Kloop1 s1'
s2'
tk)
|
match_continue_loop1:
forall s1 s2 s1'
s2'
k tk,
unseq (
Kloop1 s1 s2 k)
s1 =
OK s1' ->
unseq (
Kloop2 s1 s2 k)
s2 =
OK s2' ->
match_stmt_cont s2 s2' (
Kloop2 s1 s2 k) (
Kloop2 s1'
s2'
tk) ->
match_stmt_cont Scontinue Scontinue (
Kloop1 s1 s2 k) (
Kloop1 s1'
s2'
tk)
|
match_break_loop1:
forall s1 s2 s1'
s2'
k tk,
unseq (
Kloop1 s1 s2 k)
s1 =
OK s1' ->
unseq (
Kloop2 s1 s2 k)
s2 =
OK s2' ->
match_stmt_cont Sskip Sskip k tk ->
match_stmt_cont Sbreak Sbreak (
Kloop1 s1 s2 k) (
Kloop1 s1'
s2'
tk)
|
match_skip_loop2:
forall s1 s2 s1'
s2'
k tk,
unseq (
Kloop1 s1 s2 k)
s1 =
OK s1' ->
unseq (
Kloop2 s1 s2 k)
s2 =
OK s2' ->
match_stmt_cont Sskip Sskip (
Kloop2 s1 s2 k) (
Kloop2 s1'
s2'
tk)
|
match_break_loop2:
forall s1 s2 s1'
s2'
k tk,
unseq (
Kloop1 s1 s2 k)
s1 =
OK s1' ->
unseq (
Kloop2 s1 s2 k)
s2 =
OK s2' ->
match_stmt_cont Sskip Sskip k tk ->
match_stmt_cont Sbreak Sbreak (
Kloop2 s1 s2 k) (
Kloop2 s1'
s2'
tk)
|
match_return:
forall a k tk,
match_stmt_cont (
Sreturn a) (
Sreturn a)
k tk
|
match_skip_call:
forall optid f tf e le k tk,
match_stmt_cont Sskip Sskip (
Kcall optid f e le k) (
Kcall optid tf e le tk)
|
match_skip_stop:
match_stmt_cont Sskip Sskip Kstop Kstop
|
match_switch:
forall a ls ls'
k tk,
(
unseq_ls (
Kswitch k)
ls) =
OK ls' ->
(
forall n,
match_stmt_cont (
seq_of_labeled_statement (
select_switch n ls)) (
seq_of_labeled_statement (
select_switch n ls')) (
Kswitch k) (
Kswitch tk)) ->
match_stmt_cont (
Sswitch a ls) (
Sswitch a ls')
k tk
|
match_skip_switch:
forall k tk,
match_stmt_cont Sskip Sskip k tk ->
match_stmt_cont Sskip Sskip (
Kswitch k) (
Kswitch tk)
|
match_break_switch:
forall k tk,
match_stmt_cont Sskip Sskip k tk ->
match_stmt_cont Sbreak Sbreak (
Kswitch k) (
Kswitch tk)
|
match_continue_switch:
forall k tk,
unseq k Scontinue =
OK Scontinue ->
match_stmt_cont Scontinue Scontinue k tk ->
match_stmt_cont Scontinue Scontinue (
Kswitch k) (
Kswitch tk)
|
match_label:
forall lbl s s'
k tk,
unseq k s =
OK s' ->
match_stmt_cont s s'
k tk ->
match_stmt_cont (
Slabel lbl s) (
Slabel lbl s')
k tk
|
match_goto:
forall lbl k tk,
match_stmt_cont (
Sgoto lbl) (
Sgoto lbl)
k tk.
Lemma context_context_is_context:
forall k,
context (
context k) =
context k.
Proof.
induction k; simpl; eauto.
Qed.
Matching loops in continuations.
Inductive match_loops:
cont ->
cont ->
Prop :=
|
match_loop1:
forall s1 s2 s1'
s2'
k tk,
unseq (
Kloop1 s1 s2 k)
s1 =
OK s1' ->
unseq (
Kloop2 s1 s2 k)
s2 =
OK s2' ->
match_stmt_cont (
Sloop s1 s2) (
Sloop s1'
s2')
k tk ->
match_loops (
context k) (
context tk) ->
match_loops (
Kloop1 s1 s2 k) (
Kloop1 s1'
s2'
tk)
|
match_loop2:
forall s1 s2 s1'
s2'
k tk,
unseq (
Kloop1 s1 s2 k)
s1 =
OK s1' ->
unseq (
Kloop2 s1 s2 k)
s2 =
OK s2' ->
match_stmt_cont (
Sloop s1 s2) (
Sloop s1'
s2')
k tk ->
match_loops (
context k) (
context tk) ->
match_loops (
Kloop2 s1 s2 k) (
Kloop2 s1'
s2'
tk)
|
match_kswitch:
forall k tk,
match_loops (
context k) (
context tk) ->
match_loops (
Kswitch k) (
Kswitch tk)
|
match_stop:
match_loops Kstop Kstop
|
match_kcall:
forall optid f tf e le k tk,
match_loops (
context k) (
context tk) ->
match_loops (
Kcall optid f e le k) (
Kcall optid tf e le tk)
|
match_context:
forall k tk,
match_loops (
context k) (
context tk) ->
match_loops k tk.
Matching the call stack in the continuations.
Inductive match_call_cont:
cont ->
cont ->
Prop :=
|
match_Kstop:
forall k tk,
call_cont k =
Kstop ->
call_cont tk =
Kstop ->
match_loops k tk ->
match_call_cont k tk
|
match_Kcall:
forall k tk optid f tf e le k'
tk',
call_cont k =
Kcall optid f e le k' ->
call_cont tk =
Kcall optid tf e le tk' ->
match_stmt_cont Sskip Sskip k'
tk' ->
match_loops k tk ->
match_call_cont k'
tk' ->
transf_function f =
OK tf ->
match_call_cont k tk.
Require Import Coq.Program.Equality.
Lemma match_loop1_stmt_cont:
forall s1 s2 s1'
s2'
k tk,
unseq (
Kloop1 s1 s2 k)
s1 =
OK s1' ->
unseq (
Kloop2 s1 s2 k)
s2 =
OK s2' ->
match_loops (
Kloop1 s1 s2 k) (
Kloop1 s1'
s2'
tk) ->
match_stmt_cont (
Sloop s1 s2) (
Sloop s1'
s2')
k tk.
Proof.
clear TRANSF; clear ge; clear tge; intros; dependent induction H1.
eauto.
eapply IHmatch_loops; eauto.
Qed.
Lemma match_loop1_context:
forall s1 s2 s1'
s2'
k tk,
unseq (
Kloop1 s1 s2 k)
s1 =
OK s1' ->
unseq (
Kloop2 s1 s2 k)
s2 =
OK s2' ->
match_loops (
Kloop1 s1 s2 k) (
Kloop1 s1'
s2'
tk) ->
match_loops (
context k) (
context tk).
Proof.
clear TRANSF; clear ge; clear tge; intros; dependent induction H1.
eauto.
eapply IHmatch_loops; eauto.
Qed.
Lemma match_loop2_stmt_cont:
forall s1 s2 s1'
s2'
k tk,
unseq (
Kloop1 s1 s2 k)
s1 =
OK s1' ->
unseq (
Kloop2 s1 s2 k)
s2 =
OK s2' ->
match_loops (
Kloop2 s1 s2 k) (
Kloop2 s1'
s2'
tk) ->
match_stmt_cont (
Sloop s1 s2) (
Sloop s1'
s2')
k tk.
Proof.
clear TRANSF; clear ge; clear tge; intros; dependent induction H1.
eauto.
eapply IHmatch_loops; eauto.
Qed.
Lemma match_loop2_context:
forall s1 s2 s1'
s2'
k tk,
unseq (
Kloop1 s1 s2 k)
s1 =
OK s1' ->
unseq (
Kloop2 s1 s2 k)
s2 =
OK s2' ->
match_loops (
Kloop2 s1 s2 k) (
Kloop2 s1'
s2'
tk) ->
match_loops (
context k) (
context tk).
Proof.
clear TRANSF; clear ge; clear tge; intros; dependent induction H1.
eauto.
eapply IHmatch_loops; eauto.
Qed.
Lemma match_switch_context:
forall k tk,
match_loops (
Kswitch k) (
Kswitch tk) ->
match_loops (
context k) (
context tk).
Proof.
clear TRANSF; clear ge; clear tge; intros; dependent induction H.
eauto.
eapply IHmatch_loops; eauto.
Qed.
Lemma match_call_context:
forall k tk optid f tf e le,
match_loops (
Kcall optid f e le k) (
Kcall optid tf e le tk) ->
match_loops (
context k) (
context tk).
Proof.
clear TRANSF; clear ge; clear tge; intros; dependent induction H.
eauto.
eapply IHmatch_loops; simpl; eauto.
Qed.
Lemma call_cont_context:
forall k,
call_cont (
context k) =
call_cont k.
Proof.
induction k; intros; auto.
Qed.
Lemma match_loops_call_cont:
forall k tk,
match_loops k tk ->
match_loops (
call_cont k) (
call_cont tk).
Proof.
Lemma is_call_cont_call_cont:
forall k,
is_call_cont (
call_cont k).
Proof.
induction k; simpl; eauto.
Qed.
Definition expr_eq_dec:
forall (
e1 e2:
expr), {
e1 =
e2} + {
e1 <>
e2}.
decide equality;
try (
eapply type_eq;
fail);
try (
eapply Int.eq_dec;
fail);
try (
eapply Float.eq_dec;
fail);
try (
eapply Float32.eq_dec);
try (
eapply Int64.eq_dec);
try (
eapply peq;
fail).
decide equality.
decide equality. Defined.
Definition external_function_eq_dec: forall (ef1 ef2: external_function), {ef1 = ef2} + {ef1 <> ef2}.
repeat decide equality. eapply Int.eq_dec. eapply Int.eq_dec. Defined.
Equality over statements is decidable, only used to distinguish if s1 in
Ssequence s1 s2 is a Sskip.
Fixpoint statement_eq_dec (s1 s2: statement): {s1 = s2} + {s1 <> s2}
with labeled_statements_eq_dec (ls1 ls2: labeled_statements): {ls1 = ls2} + {ls1 <> ls2}.
decide equality; try (eapply expr_eq_dec; fail); try (eapply peq; fail). decide equality. eapply expr_eq_dec. decide equality. eapply peq. decide equality. eapply expr_eq_dec. decide equality. eapply type_eq. eapply external_function_eq_dec. decide equality. eapply peq. decide equality. eapply expr_eq_dec. decide equality. decide equality. eapply Z.eq_dec. Defined.
Lemma unseq_break_ok:
forall s k,
unseq k Sbreak = OK s ->
s = Sbreak.
Proof.
induction k; intros; try (monadInv H); eauto.
Qed.
Lemma unseq_continue_ok:
forall s k,
unseq k Scontinue = OK s ->
s = Scontinue.
Proof.
induction k; intros; try (monadInv H); eauto.
Qed.
Lemma context_loop1_context':
forall k s1 s2 k',
context k = Kloop1 s1 s2 k' ->
context k = context' k.
Proof.
induction k; simpl; intros; eauto. inv H.
Qed.
Lemma context_loop2_context':
forall k s1 s2 k',
context k = Kloop2 s1 s2 k' ->
context k = context' k.
Proof.
induction k; simpl; intros; eauto. inv H.
Qed.
Lemma unseq_break_ok_context:
forall s k,
unseq k Sbreak = OK s ->
((exists s1 s2 k', context k = Kloop1 s1 s2 k') \/
(exists s1 s2 k', context k = Kloop2 s1 s2 k') \/
(exists k', context k = Kswitch k')).
Proof.
induction k; intros; try (monadInv H); simpl; eauto.
right; left; eauto.
Qed.
Lemma unseq_continue_ok_context:
forall s k,
unseq k Scontinue = OK s ->
((exists s1 s2 k', context' k = Kloop1 s1 s2 k') \/
(exists s1 s2 k', context' k = Kloop2 s1 s2 k')).
Proof.
induction k; intros; try (monadInv H); simpl; eauto.
Qed.
Commutativity of unseq_ls and select_switch_case.
Lemma unseq_ls_select_switch_case:
forall n ls ls' k k' ls1,
context k = Kswitch k' ->
unseq_ls k ls = OK ls' ->
select_switch_case n ls = Some ls1 ->
exists ls2, select_switch_case n ls' = Some ls2 /\
unseq_ls k ls1 = OK ls2.
Proof.
induction ls;
intros.
-
inv H1.
-
monadInv H0.
simpl in H1;
simpl.
destruct o.
*
destruct (
zeq z n).
{
eexists;
split;
eauto.
inv H1.
simpl.
rewrite EQ.
simpl.
rewrite EQ1.
simpl.
reflexivity. }
{
eapply IHls;
eauto. }
*
eapply IHls;
eauto.
Qed.
Commutativity of unseq_ls and select_switch_default.
Lemma unseq_ls_select_switch_default:
forall ls ls' k k' ls1,
context k = Kswitch k' ->
unseq_ls k ls = OK ls' ->
select_switch_default ls = ls1 ->
exists ls2, select_switch_default ls' = ls2 /\
unseq_ls k ls1 = OK ls2.
Proof.
induction ls;
intros.
-
inv H1.
exists LSnil.
inv H0.
split;
simpl;
eauto.
-
monadInv H0.
simpl.
destruct o.
+
eapply IHls;
eauto.
+
econstructor;
split;
simpl;
eauto.
rewrite EQ;
simpl.
rewrite EQ1;
eauto.
Qed.
Counting consecutively nested Ssequences.
Fixpoint num_seq s :=
match s with
| Ssequence _ s2 => 1 + num_seq s2
| _ => 0
end.
Conservation of num_seq by unseq_ls.
Lemma num_seq_seq_of_labeled_statement:
forall k ls1 ls2,
unseq_ls k ls1 = OK ls2 ->
num_seq (seq_of_labeled_statement ls1) = num_seq (seq_of_labeled_statement ls2).
Proof.
unseq decreases num_seq.
Lemma num_seq_unseq:
forall s s' k,
unseq k s = OK s' ->
num_seq s' <= num_seq s.
Proof.
induction s;
intros;
try (
monadInv H;
simpl;
omega;
fail).
-
simpl in H.
destruct (
statement_eq_dec s1 Sskip).
+
subst s1.
unfold num_seq;
fold num_seq.
generalize (
IHs2 _ _ H);
omega.
+
assert ((
do s1' <-
unseq (
Kseq s2 k)
s1;
do s2' <-
unseq k s2;
OK (
Ssequence s1'
s2')) =
OK s').
destruct s1;
try congruence.
clear H.
monadInv H0.
unfold num_seq;
fold num_seq.
generalize (
IHs2 _ _ EQ1).
omega.
-
generalize (
unseq_break_ok _ _ H).
intros;
subst s';
simpl;
omega.
-
generalize (
unseq_continue_ok _ _ H);
intros;
subst s';
simpl;
omega.
Qed.
match_stmt_cont is invariant by select_switch_case.
Lemma match_stmt_cont_seq_of_labeled_statements_select_switch_case:
forall n k tk ls1 ls2 ls1' ls2',
unseq_ls (Kswitch k) ls1 = OK ls2 ->
select_switch_case n ls1 = Some ls1' ->
select_switch_case n ls2 = Some ls2' ->
match_stmt_cont (seq_of_labeled_statement ls1)
(seq_of_labeled_statement ls2)
(Kswitch k) (Kswitch tk) ->
match_stmt_cont (seq_of_labeled_statement ls1')
(seq_of_labeled_statement ls2')
(Kswitch k) (Kswitch tk).
Proof.
induction ls1;
intros.
-
inv H0.
-
monadInv H.
simpl in H0.
simpl in H1.
destruct o.
+
destruct (
zeq z n).
*
inv H0.
inv H1.
simpl.
simpl in H2.
exact H2.
*
eapply IHls1;
eauto.
simpl in H2.
inv H2.
{
monadInv EQ1.
generalize (
num_seq_unseq _ _ _ H4).
intros.
generalize (
num_seq_seq_of_labeled_statement _ _ _ EQ).
intros.
rewrite H2 in H.
unfold num_seq in H;
fold num_seq in H.
omega. }
{
exact H10. }
+
eapply IHls1;
eauto.
simpl in H2.
inv H2.
*
monadInv EQ1.
generalize (
num_seq_unseq _ _ _ H4).
intros.
generalize (
num_seq_seq_of_labeled_statement _ _ _ EQ).
intros.
rewrite H2 in H.
unfold num_seq in H;
fold num_seq in H.
omega.
*
exact H10.
Qed.
match_stmt_cont is invariant by select_switch_default.
Lemma match_stmt_cont_seq_of_labeled_statements_select_switch_default:
forall k tk ls1 ls2 ls1' ls2',
unseq_ls (Kswitch k) ls1 = OK ls2 ->
select_switch_default ls1 = ls1' ->
select_switch_default ls2 = ls2' ->
match_stmt_cont (seq_of_labeled_statement ls1)
(seq_of_labeled_statement ls2)
(Kswitch k) (Kswitch tk) ->
match_stmt_cont (seq_of_labeled_statement ls1')
(seq_of_labeled_statement ls2')
(Kswitch k) (Kswitch tk).
Proof.
induction ls1;
intros.
-
inv H0.
inv H.
eauto.
-
monadInv H.
destruct o;
simpl.
+
simpl in H2.
eapply IHls1;
eauto.
inv H2.
monadInv EQ1.
*
generalize (
num_seq_unseq _ _ _ H1).
intros.
generalize (
num_seq_seq_of_labeled_statement _ _ _ EQ).
intros.
rewrite H0 in H.
unfold num_seq in H;
fold num_seq in H.
omega.
*
exact H8.
+
simpl in H2.
exact H2.
Qed.
select_switch_case is invariant by unseq_ls.
Lemma unseq_ls_select_switch_case_none:
forall n k ls1 ls2,
unseq_ls k ls1 = OK ls2 ->
select_switch_case n ls1 = None ->
select_switch_case n ls2 = None.
Proof.
induction ls1;
intros.
-
monadInv H.
auto.
-
monadInv H.
simpl in H0;
simpl.
destruct o.
+
destruct (
zeq z n).
*
inv H0.
*
eapply IHls1;
eauto.
+
eapply IHls1;
eauto.
Qed.
First big theorem: unseq verifies the match_stmt_cont specification.
Fixpoint unseq_match_lstmt_cont (ls: labeled_statements):
forall ls' k tk,
(is_call_cont k ->
is_call_cont tk /\
match_call_cont k tk) ->
(forall s' k',
k = Kseq s' k' ->
exists s'' tk', unseq k' s' = OK s'' /\
tk = Kseq s'' tk' /\
match_stmt_cont s' s'' k' tk') ->
(forall k',
k = Kswitch k' ->
exists tk', tk = Kswitch tk' /\
match_stmt_cont Sskip Sskip k tk) ->
match_stmt_cont Sbreak Sbreak k tk ->
(forall (s1 s2 : statement) (k' : cont),
context' k = Kloop1 s1 s2 k' ->
match_stmt_cont Scontinue Scontinue k tk) ->
(exists k', context k = Kswitch k') ->
unseq_ls k ls = OK ls' ->
match_stmt_cont (seq_of_labeled_statement ls) (seq_of_labeled_statement ls') k tk
with unseq_match_stmt_cont s:
forall s' k tk,
(is_call_cont k ->
is_call_cont tk /\
match_call_cont k tk) ->
(forall s' k',
k = Kseq s' k' ->
exists s'' tk', tk = Kseq s'' tk' /\
match_stmt_cont s' s'' k' tk') ->
(forall s1 s2 k',
k = Kloop1 s1 s2 k' ->
exists s1' s2' tk', unseq (Kloop1 s1 s2 k') s1 = OK s1' /\
unseq (Kloop2 s1 s2 k') s2 = OK s2' /\
tk = Kloop1 s1' s2' tk' /\
match_stmt_cont Sskip Sskip k tk /\
match_stmt_cont Sskip Sskip k' tk') ->
(forall s1 s2 k',
k = Kloop2 s1 s2 k' ->
exists s1' s2' tk', unseq (Kloop1 s1 s2 k') s1 = OK s1' /\
unseq (Kloop2 s1 s2 k') s2 = OK s2' /\
tk = Kloop2 s1' s2' tk' /\
match_stmt_cont Sskip Sskip k tk /\
match_stmt_cont Sskip Sskip k' tk') ->
(forall k',
k = Kswitch k' ->
exists tk', tk = Kswitch tk' /\
match_stmt_cont Sskip Sskip k tk) ->
(forall k' s1 s2,
context k = Kloop1 s1 s2 k' ->
match_stmt_cont Sbreak Sbreak k tk) ->
(forall k' s1 s2,
context k = Kloop2 s1 s2 k' ->
match_stmt_cont Sbreak Sbreak k tk) ->
(forall k',
context k = Kswitch k' ->
match_stmt_cont Sbreak Sbreak k tk) ->
(forall s1 s2 k',
context' k = Kloop1 s1 s2 k' ->
match_stmt_cont Scontinue Scontinue k tk) ->
unseq k s = OK s' ->
match_stmt_cont s s' k tk.
Proof.
{
destruct ls;
intros.
-
clear unseq_match_lstmt_cont;
clear unseq_match_stmt_cont.
destruct H4 as [
k'
H4].
monadInv H5.
simpl.
destruct k.
+
inv H4.
+
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
A [
B C]]]].
rewrite B.
econstructor;
eauto.
+
inv H4.
+
inv H4.
+
generalize (
H1 _ eq_refl).
intros [
tk' [
A B]].
exact B.
+
inv H4.
-
monadInv H5.
simpl.
econstructor.
+
exact EQ1.
+
eapply unseq_match_stmt_cont.
*
intros.
inv H5.
*
intros.
inv H5.
econstructor.
econstructor.
repeat split;
eauto.
*
intros.
inv H5.
*
intros.
inv H5.
*
intros.
inv H5.
*
intros.
simpl in H5.
destruct H4 as [
k'''
H4].
rewrite H4 in H5.
inv H5.
*
intros.
simpl in H5.
destruct H4 as [
k'''
H4].
rewrite H4 in H5.
inv H5.
*
intros.
simpl in H5.
econstructor;
eauto.
simpl;
rewrite H5;
auto.
*
intros.
simpl in H5.
econstructor;
eauto.
simpl;
rewrite H5;
auto.
*
exact EQ1.
+
eapply unseq_match_lstmt_cont;
assumption. }
{
destruct s;
intros.
-
monadInv H8;
destruct k.
+
generalize (
H I).
intros [
A B].
destruct tk;
inv A.
*
econstructor.
*
inv B.
simpl in H9.
inv H9.
inv H8.
+
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
B C]]].
rewrite B.
econstructor;
eauto.
+
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
A [
B [
C [
D E]]]]]]].
exact D.
+
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
A [
B [
C [
D E]]]]]]].
exact D.
+
generalize (
H3 _ eq_refl).
intros [
tk' [
A B]].
exact B.
+
generalize (
H I).
intros [
A B].
destruct tk;
inv A.
*
inv B.
simpl in H8.
inv H8.
inv H9.
*
inv B.
inv H8.
inv H8;
inv H9.
econstructor.
-
monadInv H8;
destruct k.
+
generalize (
H I).
intros [
A B].
destruct tk;
inv A.
*
econstructor.
econstructor.
*
inv B.
simpl in H9.
inv H9.
inv H8.
+
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
B C]]].
rewrite B.
econstructor;
eauto.
econstructor;
eauto.
+
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
A [
B [
C [
D E]]]]]]].
rewrite C in D;
rewrite C.
econstructor.
exact D.
+
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
A [
B [
C [
D E]]]]]]].
rewrite C in D;
rewrite C.
econstructor.
exact D.
+
generalize (
H3 _ eq_refl).
intros [
tk' [
A B]].
rewrite A in B.
rewrite A.
econstructor.
exact B.
+
generalize (
H I).
intros [
A B].
destruct tk;
inv A.
*
inv B.
simpl in H8.
inv H8.
inv H9.
*
econstructor.
inv B.
inv H8.
inv H8;
inv H9.
econstructor.
-
monadInv H8;
destruct k.
+
generalize (
H I).
intros [
A B].
destruct tk;
inv A.
*
econstructor.
econstructor.
*
inv B.
simpl in H9.
inv H9.
inv H8.
+
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
B C]]].
rewrite B.
econstructor;
eauto.
econstructor;
eauto.
+
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
A [
B [
C [
D E]]]]]]].
rewrite C in D;
rewrite C.
econstructor.
exact D.
+
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
A [
B [
C [
D E]]]]]]].
rewrite C in D;
rewrite C.
econstructor.
exact D.
+
generalize (
H3 _ eq_refl).
intros [
tk' [
A B]].
rewrite A in B.
rewrite A.
econstructor.
exact B.
+
generalize (
H I).
intros [
A B].
destruct tk;
inv A.
*
inv B.
simpl in H8.
inv H8.
inv H9.
*
econstructor.
inv B.
inv H8.
inv H8;
inv H9.
econstructor.
-
monadInv H8;
destruct k.
+
generalize (
H I).
intros [
A B].
destruct tk;
inv A.
*
econstructor.
econstructor.
*
inv B.
simpl in H9.
inv H9.
inv H8.
+
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
B C]]].
rewrite B.
econstructor;
eauto.
econstructor;
eauto.
+
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
A [
B [
C [
D E]]]]]]].
rewrite C in D;
rewrite C.
econstructor.
exact D.
+
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
A [
B [
C [
D E]]]]]]].
rewrite C in D;
rewrite C.
econstructor.
exact D.
+
generalize (
H3 _ eq_refl).
intros [
tk' [
A B]].
rewrite A in B.
rewrite A.
econstructor.
exact B.
+
generalize (
H I).
intros [
A B].
destruct tk;
inv A.
*
inv B.
simpl in H8.
inv H8.
inv H9.
*
econstructor.
inv B.
inv H8.
inv H8;
inv H9.
econstructor.
-
monadInv H8;
destruct k.
+
generalize (
H I).
intros [
A B].
destruct tk;
inv A.
*
econstructor.
econstructor.
*
inv B.
simpl in H9.
inv H9.
inv H8.
+
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
B C]]].
rewrite B.
econstructor;
eauto.
econstructor;
eauto.
+
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
A [
B [
C [
D E]]]]]]].
rewrite C in D;
rewrite C.
econstructor.
exact D.
+
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
A [
B [
C [
D E]]]]]]].
rewrite C in D;
rewrite C.
econstructor.
exact D.
+
generalize (
H3 _ eq_refl).
intros [
tk' [
A B]].
rewrite A in B.
rewrite A.
econstructor.
exact B.
+
generalize (
H I).
intros [
A B].
destruct tk;
inv A.
*
inv B.
simpl in H8.
inv H8.
inv H9.
*
econstructor.
inv B.
inv H8.
inv H8;
inv H9.
econstructor.
-
simpl in H8.
destruct (
statement_eq_dec s1 Sskip).
+
subst s1.
econstructor;
eauto.
econstructor;
eauto.
+
assert ((
do s1' <-
unseq (
Kseq s2 k)
s1;
do s2' <-
unseq k s2;
OK (
Ssequence s1'
s2')) =
OK s').
destruct s1;
try congruence.
clear H8.
monadInv H9.
econstructor;
eauto.
eapply unseq_match_stmt_cont;
eauto.
*
intros.
inv H8.
*
intros.
inversion H8;
subst s';
subst k';
clear H8.
econstructor;
eauto.
*
intros.
inv H8.
*
intros.
inv H8.
*
intros.
inv H8.
*
intros.
econstructor.
simpl;
simpl in H8;
rewrite H8;
auto.
eapply H4;
eauto.
*
intros.
econstructor.
simpl;
simpl in H8;
rewrite H8;
auto.
eapply H5;
eauto.
*
intros.
econstructor.
simpl;
simpl in H8;
rewrite H8;
auto.
eapply H6;
eauto.
*
simpl.
intros.
econstructor.
simpl;
rewrite H8;
auto.
eapply H7;
eauto.
-
monadInv H8.
econstructor;
eauto.
-
monadInv H8.
econstructor;
eauto.
eapply unseq_match_stmt_cont;
eauto.
+
intros.
inv H8.
+
intros.
inv H8.
+
intros.
inversion H8.
subst s0;
subst s3;
subst k';
clear H8.
econstructor;
econstructor;
econstructor;
repeat split;
try assumption.
econstructor;
eauto.
eapply unseq_match_stmt_cont;
eauto.
*
intros.
inv H8.
*
intros.
inv H8.
*
intros.
inv H8.
*
intros.
inv H8.
econstructor;
econstructor;
econstructor;
repeat split;
try assumption.
econstructor;
eauto.
{
destruct k'.
+
generalize (
H I).
intros [
A B].
destruct tk;
inv A.
*
econstructor.
*
inv B.
simpl in H9.
inv H9.
inv H8.
+
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
B C]]].
rewrite B.
econstructor;
eauto.
+
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
A [
B [
C [
D E]]]]]]].
exact D.
+
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
A [
B [
C [
D E]]]]]]].
exact D.
+
generalize (
H3 _ eq_refl).
intros [
tk' [
A B]].
exact B.
+
generalize (
H I).
intros [
A B].
destruct tk;
inv A.
*
inv B.
simpl in H8.
inv H8.
inv H9.
*
inv B.
inv H8.
inv H8;
inv H9.
econstructor. }
*
intros.
inv H8.
*
intros.
inv H8.
*
intros.
inv H8.
econstructor;
try assumption.
{
destruct k'.
+
generalize (
H I).
intros [
A B].
destruct tk;
inv A.
*
econstructor.
*
inv B.
simpl in H9.
inv H9.
inv H8.
+
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
B C]]].
rewrite B.
econstructor;
eauto.
+
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
A [
B [
C [
D E]]]]]]].
exact D.
+
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
A [
B [
C [
D E]]]]]]].
exact D.
+
generalize (
H3 _ eq_refl).
intros [
tk' [
A B]].
exact B.
+
generalize (
H I).
intros [
A B].
destruct tk;
inv A.
*
inv B.
simpl in H8.
inv H8.
inv H9.
*
inv B.
inv H8.
inv H8;
inv H9.
econstructor. }
*
intros.
inv H8.
*
intros.
inv H8.
*
destruct k.
{
generalize (
H I).
intros [
A B].
destruct tk;
inv A.
*
econstructor.
*
inv B.
simpl in H9.
inv H9.
inv H8. }
{
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
B C]]].
rewrite B.
econstructor;
eauto. }
{
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
A [
B [
C [
D E]]]]]]].
exact D. }
{
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
A [
B [
C [
D E]]]]]]].
exact D. }
{
generalize (
H3 _ eq_refl).
intros [
tk' [
A B]].
exact B. }
{
generalize (
H I).
intros [
A B].
destruct tk;
inv A.
*
inv B.
simpl in H8.
inv H8.
inv H9.
*
inv B.
inv H8.
inv H8;
inv H9.
econstructor. }
+
intros.
inv H8.
+
intros.
inv H8.
+
intros.
inv H8.
econstructor;
try assumption.
destruct k'.
{
generalize (
H I).
intros [
A B].
destruct tk;
inv A.
*
econstructor.
*
inv B.
simpl in H9.
inv H9.
inv H8. }
{
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
B C]]].
rewrite B.
econstructor;
eauto. }
{
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
A [
B [
C [
D E]]]]]]].
exact D. }
{
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
A [
B [
C [
D E]]]]]]].
exact D. }
{
generalize (
H3 _ eq_refl).
intros [
tk' [
A B]].
exact B. }
{
generalize (
H I).
intros [
A B].
destruct tk;
inv A.
*
inv B.
simpl in H8.
inv H8.
inv H9.
*
inv B.
inv H8.
inv H8;
inv H9.
econstructor. }
+
intros.
inv H8.
+
intros.
inv H8.
+
intros.
simpl in H8;
inversion H8;
subst s0;
subst s3;
subst k';
clear H8.
econstructor;
try assumption.
eapply unseq_match_stmt_cont;
eauto.
*
intros.
inv H8.
*
intros.
inv H8.
*
intros.
inv H8.
*
intros.
inv H8.
econstructor;
econstructor;
econstructor;
repeat split;
try assumption.
econstructor;
eauto.
{
destruct k'.
+
generalize (
H I).
intros [
A B].
destruct tk;
inv A.
*
econstructor.
*
inv B.
simpl in H9.
inv H9.
inv H8.
+
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
B C]]].
rewrite B.
econstructor;
eauto.
+
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
A [
B [
C [
D E]]]]]]].
exact D.
+
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
A [
B [
C [
D E]]]]]]].
exact D.
+
generalize (
H3 _ eq_refl).
intros [
tk' [
A B]].
exact B.
+
generalize (
H I).
intros [
A B].
destruct tk;
inv A.
*
inv B.
simpl in H8.
inv H8.
inv H9.
*
inv B.
inv H8.
inv H8;
inv H9.
econstructor. }
*
intros.
inv H8.
*
intros.
inv H8.
*
intros.
inv H8.
econstructor;
try assumption.
{
destruct k'.
+
generalize (
H I).
intros [
A B].
destruct tk;
inv A.
*
econstructor.
*
inv B.
simpl in H9.
inv H9.
inv H8.
+
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
B C]]].
rewrite B.
econstructor;
eauto.
+
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
A [
B [
C [
D E]]]]]]].
exact D.
+
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
A [
B [
C [
D E]]]]]]].
exact D.
+
generalize (
H3 _ eq_refl).
intros [
tk' [
A B]].
exact B.
+
generalize (
H I).
intros [
A B].
destruct tk;
inv A.
*
inv B.
simpl in H8.
inv H8.
inv H9.
*
inv B.
inv H8.
inv H8;
inv H9.
econstructor. }
*
intros.
inv H8.
*
intros.
inv H8.
-
destruct k.
+
monadInv H8.
+
generalize (
unseq_break_ok _ _ H8).
intros;
subst s'.
generalize (
unseq_break_ok_context _ _ H8).
intros [[
s1 [
s2 [
k'
A]]] | [[
s1 [
s2 [
k'
A]]] | [
k'
A]]].
*
eapply H4;
eauto.
*
eapply H5;
eauto.
*
eapply H6;
eauto.
+
generalize (
unseq_break_ok _ _ H8).
intros;
subst s'.
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
A [
B [
C [
D E]]]]]]].
rewrite C.
econstructor;
eauto.
+
generalize (
unseq_break_ok _ _ H8).
intros;
subst s'.
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
A [
B [
C [
D E]]]]]]].
rewrite C.
econstructor;
eauto.
+
generalize (
unseq_break_ok _ _ H8).
intros;
subst s'.
generalize (
H3 _ eq_refl).
intros [
tk' [
A B]].
rewrite A.
rewrite A in B;
inv B.
econstructor;
eauto.
+
simpl in H8.
inv H8.
-
destruct k.
+
monadInv H8.
+
generalize (
unseq_continue_ok _ _ H8).
intros;
subst s'.
generalize (
unseq_continue_ok_context _ _ H8).
intros [[
s1 [
s2 [
k'
A]]] | [
s1 [
s2 [
k'
A]]]].
*
eapply H7;
eauto.
*
simpl in H8;
simpl in A;
rewrite A in H8;
inv H8.
+
generalize (
unseq_continue_ok _ _ H8).
intros;
subst s'.
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
A [
B [
C [
D E]]]]]]].
rewrite C.
rewrite C in D;
inv D;
econstructor;
eauto.
+
monadInv H8.
+
generalize (
unseq_continue_ok _ _ H8).
intros;
subst s'.
generalize (
unseq_continue_ok_context _ _ H8).
intros [[
s1 [
s2 [
k'
A]]] | [
s1 [
s2 [
k'
A]]]].
*
eapply H7;
eauto.
*
simpl in H8;
simpl in A;
rewrite A in H8;
inv H8.
+
simpl in H8.
inv H8.
-
monadInv H8.
econstructor.
-
monadInv H8.
econstructor;
eauto.
intros.
unfold select_switch.
case_eq (
select_switch_case n l).
+
intros.
generalize (
unseq_ls_select_switch_case n l x (
Kswitch k)
k l0 eq_refl EQ H8).
intros [
l1 [
A B]].
rewrite A.
eapply match_stmt_cont_seq_of_labeled_statements_select_switch_case.
*
exact EQ.
*
exact H8.
*
exact A.
*
eapply unseq_match_lstmt_cont;
eauto.
{
intros.
inv H9. }
{
intros.
inv H9. }
{
intros.
inv H9.
exists tk.
split;
auto.
econstructor.
destruct k'.
+
generalize (
H I).
intros [
C D].
destruct tk;
inv C.
*
econstructor.
*
inv D.
simpl in H10.
inv H10.
inv H9.
+
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
C D]]].
rewrite C.
econstructor;
eauto.
+
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
E [
F [
C [
D Q]]]]]]].
exact D.
+
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
E [
F [
C [
D Q]]]]]]].
exact D.
+
generalize (
H3 _ eq_refl).
intros [
tk' [
C D]].
exact D.
+
generalize (
H I).
intros [
C D].
destruct tk;
inv C.
*
inv D.
simpl in H9.
inv H9.
inv H10.
*
inv D.
inv H9.
inv H9;
inv H10.
econstructor. }
{
econstructor.
clear H8.
clear A.
clear B.
destruct k.
+
generalize (
H I).
intros [
A B].
destruct tk;
inv A.
*
econstructor.
*
inv B.
simpl in H9.
inv H9.
inv H8.
+
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
B C]]].
rewrite B.
econstructor;
eauto.
+
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
A [
B [
C [
D E]]]]]]].
exact D.
+
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
A [
B [
C [
D E]]]]]]].
exact D.
+
generalize (
H3 _ eq_refl).
intros [
tk' [
A B]].
exact B.
+
generalize (
H I).
intros [
A B].
destruct tk;
inv A.
*
inv B.
simpl in H8.
inv H8.
inv H9.
*
inv B.
inv H8.
inv H8;
inv H9.
econstructor. }
{
econstructor.
simpl in H9.
simpl;
rewrite H9;
eauto.
eapply H7;
eauto. }
{
simpl;
eauto. }
+
intros.
generalize (
unseq_ls_select_switch_case_none _ _ _ _ EQ H8).
intros QQ.
rewrite QQ.
eapply match_stmt_cont_seq_of_labeled_statements_select_switch_default.
*
exact EQ.
*
eauto.
*
eauto.
*
eapply unseq_match_lstmt_cont;
eauto.
{
intros.
inv H9. }
{
intros.
inv H9. }
{
intros.
inv H9.
exists tk.
split;
auto.
econstructor.
destruct k'.
+
generalize (
H I).
intros [
A B].
destruct tk;
inv A.
*
econstructor.
*
inv B.
simpl in H10.
inv H10.
inv H9.
+
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
B C]]].
rewrite B.
econstructor;
eauto.
+
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
A [
B [
C [
D E]]]]]]].
exact D.
+
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
A [
B [
C [
D E]]]]]]].
exact D.
+
generalize (
H3 _ eq_refl).
intros [
tk' [
A B]].
exact B.
+
generalize (
H I).
intros [
A B].
destruct tk;
inv A.
*
inv B.
simpl in H9.
inv H9.
inv H10.
*
inv B.
inv H9.
inv H9;
inv H10.
econstructor. }
{
econstructor.
destruct k.
+
generalize (
H I).
intros [
A B].
destruct tk;
inv A.
*
econstructor.
*
inv B.
simpl in H10.
inv H10.
inv H9.
+
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
B C]]].
rewrite B.
econstructor;
eauto.
+
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
A [
B [
C [
D E]]]]]]].
exact D.
+
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
A [
B [
C [
D E]]]]]]].
exact D.
+
generalize (
H3 _ eq_refl).
intros [
tk' [
A B]].
exact B.
+
generalize (
H I).
intros [
A B].
destruct tk;
inv A.
*
inv B.
simpl in H9.
inv H9.
inv H10.
*
inv B.
inv H9.
inv H9;
inv H10.
econstructor. }
{
intros.
econstructor.
simpl;
simpl in H9;
rewrite H9;
auto.
eapply H7;
eauto. }
{
simpl;
eauto. }
-
monadInv H8.
econstructor;
eauto.
-
monadInv H8.
econstructor;
eauto. }
Qed.
Lemma context'_no_kseq:
forall k s k',
context' k <> Kseq s k'.
Proof.
induction k; simpl; try congruence.
Qed.
Lemma context'_no_kswitch:
forall k k',
context' k <> Kswitch k'.
Proof.
induction k; simpl; congruence. Qed.
Matching continuation types.
Inductive match_cont_ty: cont -> cont -> Prop :=
| match_call_stop:
forall f e le m k,
match_cont_ty (Kcall f e le m k) Kstop
| match_stop_call:
forall f e le m k,
match_cont_ty Kstop (Kcall f e le m k)
| match_stop_stop:
match_cont_ty Kstop Kstop
| match_call_call:
forall f tf e te le tle m tm k tk,
match_cont_ty (Kcall f e le m k) (Kcall tf te tle tm tk)
| match_loop1_loop1:
forall s1 s1' s2 s2' k k',
match_cont_ty (context k) (context k') ->
match_cont_ty (Kloop1 s1 s2 k) (Kloop1 s1' s2' k')
| match_loop2_loop2:
forall s1 s1' s2 s2' k k',
match_cont_ty (context k) (context k') ->
match_cont_ty (Kloop2 s1 s2 k) (Kloop2 s1' s2' k')
| match_switch_switch:
forall k k',
match_cont_ty (context k) (context k') ->
match_cont_ty (Kswitch k) (Kswitch k')
| match_seq_any:
forall s k k',
match_cont_ty (context k) (context k') ->
match_cont_ty (Kseq s k) k'
| match_any_seq:
forall s' k k',
match_cont_ty (context k) (context k') ->
match_cont_ty k (Kseq s' k').
Lemma match_cont_ty_seq:
forall s s' k k',
match_cont_ty k k' ->
match_cont_ty (Kseq s k) (Kseq s' k').
Proof.
induction 1; intros; try (econstructor; simpl; econstructor; eauto; fail).
- econstructor. simpl. eauto.
- econstructor. simpl. eauto.
Qed.
Lemma match_cont_ty_context:
forall k k',
match_cont_ty k k' ->
match_cont_ty (context k) (context k').
Proof.
induction 1; intros; try (simpl; econstructor; eauto; fail).
- simpl; eauto.
- simpl; eauto.
Qed.
Lemma context_no_seq:
forall k s k',
context k <> Kseq s k'.
Proof.
induction k; intros; simpl; try congruence.
Qed.
Lemma context'_context:
forall k,
context' (context k) = context' k.
Proof.
induction k; simpl; eauto.
Qed.
Lemma match_cont_ty_context':
forall k k',
match_cont_ty k k' ->
match_cont_ty (context' k) (context' k').
Proof.
induction 1; intros; simpl; try (econstructor; eauto).
- rewrite (context'_context k) in IHmatch_cont_ty.
rewrite (context'_context k') in IHmatch_cont_ty.
eauto.
- rewrite (context'_context k) in IHmatch_cont_ty.
rewrite (context'_context k') in IHmatch_cont_ty.
eauto.
- rewrite (context'_context k) in IHmatch_cont_ty.
rewrite (context'_context k') in IHmatch_cont_ty.
eauto.
Qed.
The result of unseq depends only the continuation type, not the continuation itself.
Lemma unseq_cont_ty:
forall s k k',
match_cont_ty k k' ->
unseq k s = unseq k' s
with unseq_ls_cont_ty:
forall s k k',
match_cont_ty k k' ->
unseq_ls k s = unseq_ls k' s.
Proof.
{
destruct s;
intros;
try (
simpl;
auto;
fail).
-
simpl.
repeat rewrite (
unseq_cont_ty s1 (
Kseq s2 k) (
Kseq s2 k') (
match_cont_ty_seq s2 s2 k k'
H)).
repeat rewrite (
unseq_cont_ty s2 k k'
H).
reflexivity.
-
simpl.
repeat rewrite (
unseq_cont_ty s1 k k'
H).
repeat rewrite (
unseq_cont_ty s2 k k'
H).
reflexivity.
-
simpl.
repeat rewrite (
unseq_cont_ty s1 (
Kloop1 s1 s2 k) (
Kloop1 s1 s2 k') (
match_loop1_loop1 s1 s1 s2 s2 k k' (
match_cont_ty_context k k'
H))).
repeat rewrite (
unseq_cont_ty s2 (
Kloop2 s1 s2 k) (
Kloop2 s1 s2 k') (
match_loop2_loop2 s1 s1 s2 s2 k k' (
match_cont_ty_context k k'
H))).
reflexivity.
-
simpl.
generalize (
match_cont_ty_context k k'
H).
intros.
generalize (
context_no_seq k).
generalize (
context_no_seq k').
intros.
destruct H0;
simpl;
eauto.
+
generalize (
H2 s k);
congruence.
+
generalize (
H1 s'
k'0);
congruence.
-
simpl.
generalize (
match_cont_ty_context'
k k'
H).
intros.
generalize (
context'
_no_kseq k).
generalize (
context'
_no_kseq k').
intros.
destruct H0;
simpl;
eauto.
+
generalize (
H2 s k0);
congruence.
+
generalize (
H1 s'
k'0);
congruence.
-
simpl.
rewrite (
unseq_ls_cont_ty l (
Kswitch k) (
Kswitch k')).
reflexivity.
econstructor.
destruct H;
simpl;
try econstructor;
eauto.
-
simpl.
rewrite (
unseq_cont_ty s k k'
H).
reflexivity. }
{
destruct s;
intros.
-
simpl;
reflexivity.
-
simpl.
rewrite (
unseq_cont_ty s (
Kseq (
seq_of_labeled_statement s0)
k) (
Kseq (
seq_of_labeled_statement s0)
k') (
match_cont_ty_seq _ _ k k'
H)).
rewrite (
unseq_ls_cont_ty s0 k k'
H).
reflexivity. }
Qed.
Lemma match_loops_context:
forall k tk,
match_loops k tk ->
match_loops (context k) (context tk).
Proof.
induction 1; try (simpl; econstructor; eauto; fail).
Qed.
Lemma match_call_cont_call_cont:
forall k tk,
match_call_cont k tk ->
match_call_cont (call_cont k) (call_cont tk).
Proof.
induction 1.
-
rewrite H;
rewrite H0;
econstructor;
simpl;
eauto.
econstructor.
-
rewrite H;
rewrite H0;
econstructor 2;
simpl;
eauto.
econstructor;
eauto.
inv H3;
eauto;
eapply match_loops_context;
eauto.
Qed.
Lemma unseq_skip_find_label:
forall lbl s k,
unseq k s = OK Sskip ->
find_label lbl s k = None.
Proof.
induction s;
intros;
try (
simpl;
eauto;
fail).
-
simpl in H.
destruct (
statement_eq_dec s1 Sskip).
+
subst s1.
simpl.
eapply IHs2;
eauto.
+
assert ((
do s1' <-
unseq (
Kseq s2 k)
s1;
do s2' <-
unseq k s2;
OK (
Ssequence s1'
s2')) =
OK Sskip).
destruct s1;
congruence.
clear H.
monadInv H0.
-
monadInv H.
-
monadInv H.
-
monadInv H.
-
monadInv H.
Qed.
Lemma match_call_cont_seq:
forall s s' k k',
match_call_cont k k' ->
match_call_cont (Kseq s k) (Kseq s' k').
Proof.
induction 1;
intros.
-
econstructor;
eauto.
econstructor;
simpl;
eauto.
eapply match_loops_context;
eauto.
-
econstructor 2;
simpl;
eauto.
econstructor;
simpl;
eauto.
eapply match_loops_context;
eauto.
Qed.
Second big theorem: match_stmt_cont is invariant by find_label.
Theorem find_label_match_stmt_cont:
forall lbl s k ts tk,
(is_call_cont k ->
is_call_cont tk /\
match_call_cont k tk) ->
(forall s' k',
k = Kseq s' k' ->
exists s'' tk', tk = Kseq s'' tk' /\
match_stmt_cont s' s'' k' tk') ->
(forall s1 s2 k',
k = Kloop1 s1 s2 k' ->
exists s1' s2' tk', unseq (Kloop1 s1 s2 k') s1 = OK s1' /\
unseq (Kloop2 s1 s2 k') s2 = OK s2' /\
tk = Kloop1 s1' s2' tk' /\
match_stmt_cont Sskip Sskip k tk /\
match_stmt_cont Sskip Sskip k' tk') ->
(forall s1 s2 k',
k = Kloop2 s1 s2 k' ->
exists s1' s2' tk', unseq (Kloop1 s1 s2 k') s1 = OK s1' /\
unseq (Kloop2 s1 s2 k') s2 = OK s2' /\
tk = Kloop2 s1' s2' tk' /\
match_stmt_cont Sskip Sskip k tk /\
match_stmt_cont Sskip Sskip k' tk') ->
(forall k',
k = Kswitch k' ->
exists tk', tk = Kswitch tk' /\
match_stmt_cont Sskip Sskip k tk) ->
(forall k' s1 s2,
context k = Kloop1 s1 s2 k' ->
match_stmt_cont Sbreak Sbreak k tk) ->
(forall k' s1 s2,
context k = Kloop2 s1 s2 k' ->
match_stmt_cont Sbreak Sbreak k tk) ->
(forall k',
context k = Kswitch k' ->
match_stmt_cont Sbreak Sbreak k tk) ->
(forall s1 s2 k',
context' k = Kloop1 s1 s2 k' ->
match_stmt_cont Scontinue Scontinue k tk) ->
unseq k s = OK ts ->
match_call_cont k tk ->
match_loops k tk ->
match find_label lbl s k with
| Some (s', k') =>
exists ts' tk',
find_label lbl ts tk = Some (ts', tk') /\
match_stmt_cont s' ts' k' tk' /\
match_call_cont k' tk' /\
match_loops k' tk'
| None => find_label lbl ts tk = None
end
with find_label_ls_match_stmt_cont:
forall lbl ls ls' k tk,
(is_call_cont k ->
is_call_cont tk /\
match_call_cont k tk) ->
(forall s' k',
k = Kseq s' k' ->
exists s'' tk', unseq k' s' = OK s'' /\
tk = Kseq s'' tk' /\
match_stmt_cont s' s'' k' tk') ->
(forall k',
k = Kswitch k' ->
exists tk', tk = Kswitch tk' /\
match_stmt_cont Sskip Sskip k tk) ->
match_stmt_cont Sbreak Sbreak k tk ->
(forall (s1 s2 : statement) (k' : cont),
context' k = Kloop1 s1 s2 k' ->
match_stmt_cont Scontinue Scontinue k tk) ->
(exists k', context k = Kswitch k') ->
unseq_ls k ls = OK ls' ->
match_call_cont k tk ->
match_loops k tk ->
match find_label_ls lbl ls k with
| Some (s', k') =>
exists (ts' : statement) (tk' : cont),
find_label_ls lbl ls' tk = Some (ts', tk') /\
match_stmt_cont s' ts' k' tk' /\
match_call_cont k' tk' /\ match_loops k' tk'
| None => find_label_ls lbl ls' tk = None
end.
Proof.
{
induction s;
intros;
try (
monadInv H8;
simpl;
eauto;
fail).
-
generalize (
unseq_match_stmt_cont _ _ _ _ H H0 H1 H2 H3 H4 H5 H6 H7 H8).
intros A.
simpl.
case_eq (
find_label lbl s1 (
Kseq s2 k));
intros.
+
destruct p.
simpl in H8.
destruct (
statement_eq_dec s1 Sskip).
*
subst s1.
simpl in H11.
inv H11.
*
assert ((
do s1' <-
unseq (
Kseq s2 k)
s1;
do s2' <-
unseq k s2;
OK (
Ssequence s1'
s2')) =
OK ts).
destruct s1;
congruence.
clear H8.
monadInv H12.
simpl.
generalize (
IHs1 (
Kseq s2 k)
x (
Kseq x0 tk)).
clear IHs1.
intros.
rewrite H11 in H8.
assert (
exists (
ts' :
statement) (
tk' :
cont),
find_label lbl x (
Kseq x0 tk) =
Some (
ts',
tk') /\
match_stmt_cont s ts'
c tk' /\
match_call_cont c tk' /\
match_loops c tk').
eapply H8;
eauto.
{
intros.
inv H12. }
{
intros.
econstructor.
econstructor.
split;
eauto.
inv A;
eauto;
try congruence. }
{
intros.
inv H12. }
{
intros.
inv H12. }
{
intros.
inv H12. }
{
simpl;
intros.
econstructor.
simpl;
rewrite H12;
eauto.
eapply (
H4 _ _ _ H12). }
{
simpl;
intros.
econstructor.
simpl;
rewrite H12;
eauto.
eapply (
H5 _ _ _ H12). }
{
simpl;
intros.
econstructor.
simpl;
rewrite H12;
eauto.
eapply (
H6 _ H12). }
{
simpl;
intros.
econstructor.
simpl;
rewrite H12;
eauto.
eapply (
H7 _ _ _ H12). }
{
eapply (
match_call_cont_seq s2 x0 k tk H9). }
{
econstructor.
simpl.
eapply match_loops_context;
eauto. }
destruct H12 as [
ts' [
tk' [
B [
C [
D E]]]]].
rewrite B.
exists ts';
exists tk';
repeat split;
eauto.
+
case_eq (
find_label lbl s2 k);
intros.
*
destruct p.
simpl in H8.
destruct (
statement_eq_dec s1 Sskip).
{
subst s1.
clear IHs1.
generalize (
IHs2 k ts tk);
intros;
clear IHs2.
rewrite H12 in H13.
eapply H13;
eauto. }
{
assert ((
do s1' <-
unseq (
Kseq s2 k)
s1;
do s2' <-
unseq k s2;
OK (
Ssequence s1'
s2')) =
OK ts).
destruct s1;
try congruence.
clear H8.
monadInv H13.
simpl.
generalize (
IHs1 (
Kseq s2 k)
x (
Kseq x0 tk)).
clear IHs1.
intros.
rewrite H11 in H8.
assert (
find_label lbl x (
Kseq x0 tk) =
None).
eapply H8;
clear H8.
-
intros.
inv H8.
-
intros.
econstructor.
econstructor.
split;
eauto.
inv A;
eauto;
try congruence.
-
intros.
inv H8.
-
intros.
inv H8.
-
intros.
inv H8.
-
simpl;
intros.
econstructor.
simpl;
rewrite H8;
eauto.
eapply (
H4 _ _ _ H8).
-
simpl;
intros.
econstructor.
simpl;
rewrite H8;
eauto.
eapply (
H5 _ _ _ H8).
-
simpl;
intros.
econstructor.
simpl;
rewrite H8;
eauto.
eapply (
H6 _ H8).
-
simpl;
intros.
econstructor.
simpl;
rewrite H8;
eauto.
eapply (
H7 _ _ _ H8).
-
eapply EQ.
-
eapply (
match_call_cont_seq s2 x0 k tk H9).
-
econstructor.
simpl.
eapply match_loops_context;
eauto.
-
rewrite H13.
clear H8.
generalize (
IHs2 k x0 tk);
intros;
clear IHs2.
rewrite H12 in H8.
eapply H8;
eauto. }
*
destruct (
statement_eq_dec s1 Sskip).
{
subst s1.
clear IHs1.
generalize (
IHs2 k ts tk);
intros;
clear IHs2.
rewrite H12 in H13.
eapply H13;
eauto. }
{
simpl in H8;
assert ((
do s1' <-
unseq (
Kseq s2 k)
s1;
do s2' <-
unseq k s2;
OK (
Ssequence s1'
s2')) =
OK ts).
destruct s1;
try congruence.
clear H8.
monadInv H13.
simpl.
generalize (
IHs1 (
Kseq s2 k)
x (
Kseq x0 tk)).
clear IHs1.
intros.
rewrite H11 in H8.
assert (
find_label lbl x (
Kseq x0 tk) =
None).
eapply H8;
clear H8.
-
intros.
inv H8.
-
intros.
econstructor.
econstructor.
split;
eauto.
inv A;
eauto;
try congruence.
-
intros.
inv H8.
-
intros.
inv H8.
-
intros.
inv H8.
-
simpl;
intros.
econstructor.
simpl;
rewrite H8;
eauto.
eapply (
H4 _ _ _ H8).
-
simpl;
intros.
econstructor.
simpl;
rewrite H8;
eauto.
eapply (
H5 _ _ _ H8).
-
simpl;
intros.
econstructor.
simpl;
rewrite H8;
eauto.
eapply (
H6 _ H8).
-
simpl;
intros.
econstructor.
simpl;
rewrite H8;
eauto.
eapply (
H7 _ _ _ H8).
-
eapply EQ.
-
eapply (
match_call_cont_seq s2 x0 k tk H9).
-
econstructor.
simpl.
eapply match_loops_context;
eauto.
-
rewrite H13.
clear H8.
generalize (
IHs2 k x0 tk);
intros;
clear IHs2.
rewrite H12 in H8.
eapply H8;
eauto. }
-
generalize (
unseq_match_stmt_cont _ _ _ _ H H0 H1 H2 H3 H4 H5 H6 H7 H8).
intros A.
simpl in H8.
monadInv H8.
simpl.
case_eq (
find_label lbl s1 k);
intros.
+
destruct p.
generalize (
IHs1 _ _ _ H H0 H1 H2 H3 H4 H5 H6 H7 EQ H9 H10).
rewrite H8.
intros [
ts' [
tk' [
B [
C [
D E]]]]].
rewrite B.
exists ts';
exists tk';
repeat split;
eauto.
+
case_eq (
find_label lbl s2 k);
intros.
*
destruct p.
generalize (
IHs1 _ _ _ H H0 H1 H2 H3 H4 H5 H6 H7 EQ H9 H10).
rewrite H8.
intros.
rewrite H12.
generalize (
IHs2 _ _ _ H H0 H1 H2 H3 H4 H5 H6 H7 EQ1 H9 H10).
rewrite H11.
intros [
ts' [
tk' [
B [
C [
D E]]]]].
exists ts';
exists tk';
rewrite B;
repeat split;
eauto.
*
generalize (
IHs1 _ _ _ H H0 H1 H2 H3 H4 H5 H6 H7 EQ H9 H10).
rewrite H8.
intros.
rewrite H12.
generalize (
IHs2 _ _ _ H H0 H1 H2 H3 H4 H5 H6 H7 EQ1 H9 H10).
rewrite H11.
eauto.
-
generalize (
unseq_match_stmt_cont _ _ _ _ H H0 H1 H2 H3 H4 H5 H6 H7 H8).
intros A.
simpl in H8.
monadInv H8.
simpl.
case_eq (
find_label lbl s1 (
Kloop1 s1 s2 k));
intros.
+
destruct p.
generalize (
IHs1 (
Kloop1 s1 s2 k)
x (
Kloop1 x x0 tk)).
clear IHs1;
intros.
rewrite H8 in H11.
assert (
exists (
ts' :
statement) (
tk' :
cont),
find_label lbl x (
Kloop1 x x0 tk) =
Some (
ts',
tk') /\
match_stmt_cont s ts'
c tk' /\
match_call_cont c tk' /\
match_loops c tk').
{
eapply H11;
clear H11;
eauto.
-
intros.
inv H11.
-
intros.
inv H11.
-
intros.
inv H11.
exists x;
exists x0;
exists tk.
repeat split;
eauto.
+
econstructor;
eauto.
eapply unseq_match_stmt_cont;
eauto.
*
intros.
inv H11.
*
intros.
inv H11.
*
intros.
inv H11.
*
intros.
inv H11.
exists x;
exists x0;
exists tk;
repeat split;
eauto.
econstructor;
eauto.
clear IHs2;
destruct k'0.
{
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
-
econstructor.
-
econstructor.
-
simpl in H12;
inv H12.
-
simpl in H11;
inv H11. }
{
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
U V]]].
rewrite U;
econstructor;
eauto. }
{
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto. }
{
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto. }
{
generalize (
H3 _ eq_refl).
intros [
tk' [
U V]].
eauto. }
{
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
-
simpl in H11;
inv H11.
-
simpl in H12;
inv H12.
-
simpl in H11;
inv H11.
-
simpl in H11;
simpl in H12;
inv H11;
inv H12;
econstructor. }
*
intros.
inv H11.
*
simpl;
intros;
inv H11.
*
simpl;
intros;
inv H11.
econstructor;
eauto.
clear IHs2.
destruct k'0.
{
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
-
econstructor.
-
econstructor.
-
simpl in H12;
inv H12.
-
simpl in H11;
inv H11. }
{
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
U V]]].
rewrite U;
econstructor;
eauto. }
{
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto. }
{
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto. }
{
generalize (
H3 _ eq_refl).
intros [
tk' [
U V]].
eauto. }
{
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
-
simpl in H11;
inv H11.
-
simpl in H12;
inv H12.
-
simpl in H11;
inv H11.
-
simpl in H11;
simpl in H12;
inv H11;
inv H12;
econstructor. }
*
simpl;
intros.
inv H11.
*
simpl;
intros.
inv H11.
+
destruct k'.
*
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
{
econstructor. }
{
econstructor. }
{
simpl in H12;
inv H12. }
{
simpl in H11;
inv H11. }
*
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
U V]]].
rewrite U;
econstructor;
eauto.
*
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto.
*
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto.
*
generalize (
H3 _ eq_refl).
intros [
tk' [
U V]].
eauto.
*
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
{
simpl in H11;
inv H11. }
{
simpl in H12;
inv H12. }
{
simpl in H11;
inv H11. }
{
simpl in H11;
simpl in H12;
inv H11;
inv H12;
econstructor. }
-
intros.
inv H11.
-
intros.
inv H11.
-
simpl;
intros.
inv H11.
econstructor;
eauto.
destruct k'.
*
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
{
econstructor. }
{
econstructor. }
{
simpl in H12;
inv H12. }
{
simpl in H11;
inv H11. }
*
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
U V]]].
rewrite U;
econstructor;
eauto.
*
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto.
*
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto.
*
generalize (
H3 _ eq_refl).
intros [
tk' [
U V]].
eauto.
*
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
{
simpl in H11;
inv H11. }
{
simpl in H12;
inv H12. }
{
simpl in H11;
inv H11. }
{
simpl in H11;
simpl in H12;
inv H11;
inv H12;
econstructor. }
-
simpl;
intros;
inv H11.
-
simpl;
intros;
inv H11.
-
simpl;
intros;
inv H11.
econstructor;
eauto.
eapply unseq_match_stmt_cont;
eauto.
*
intros.
inv H11.
*
intros.
inv H11.
*
intros.
inv H11.
*
intros.
inv H11.
exists x;
exists x0;
exists tk;
repeat split;
eauto.
econstructor;
eauto.
clear IHs2;
destruct k'0.
{
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
-
econstructor.
-
econstructor.
-
simpl in H12;
inv H12.
-
simpl in H11;
inv H11. }
{
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
U V]]].
rewrite U;
econstructor;
eauto. }
{
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto. }
{
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto. }
{
generalize (
H3 _ eq_refl).
intros [
tk' [
U V]].
eauto. }
{
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
-
simpl in H11;
inv H11.
-
simpl in H12;
inv H12.
-
simpl in H11;
inv H11.
-
simpl in H11;
simpl in H12;
inv H11;
inv H12;
econstructor. }
*
intros.
inv H11.
*
simpl;
intros;
inv H11.
*
simpl;
intros;
inv H11.
econstructor;
eauto.
clear IHs2.
destruct k'0.
{
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
-
econstructor.
-
econstructor.
-
simpl in H12;
inv H12.
-
simpl in H11;
inv H11. }
{
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
U V]]].
rewrite U;
econstructor;
eauto. }
{
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto. }
{
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto. }
{
generalize (
H3 _ eq_refl).
intros [
tk' [
U V]].
eauto. }
{
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
-
simpl in H11;
inv H11.
-
simpl in H12;
inv H12.
-
simpl in H11;
inv H11.
-
simpl in H11;
simpl in H12;
inv H11;
inv H12;
econstructor. }
*
simpl;
intros.
inv H11.
*
simpl;
intros.
inv H11.
-
inv H9.
+
econstructor;
simpl;
eauto.
econstructor;
eauto.
eapply match_loops_context;
eauto.
+
econstructor 2;
simpl;
eauto.
econstructor;
eauto.
eapply match_loops_context;
eauto.
-
econstructor;
eauto.
eapply match_loops_context;
eauto. }
{
destruct H12 as [
ts' [
tk' [
U [
V [
W X]]]]].
rewrite U.
exists ts';
exists tk';
repeat split;
eauto. }
+
case_eq (
find_label lbl s2 (
Kloop2 s1 s2 k)).
*
intros [
s c Q].
generalize (
IHs1 (
Kloop1 s1 s2 k)
x (
Kloop1 x x0 tk)).
clear IHs1;
intros.
rewrite H8 in H11.
assert (
find_label lbl x (
Kloop1 x x0 tk) =
None).
{
eapply H11;
clear H11;
eauto.
-
intros.
inv H11.
-
intros.
inv H11.
-
intros.
inv H11.
exists x;
exists x0;
exists tk.
repeat split;
eauto.
+
econstructor;
eauto.
eapply unseq_match_stmt_cont;
eauto.
*
intros.
inv H11.
*
intros.
inv H11.
*
intros.
inv H11.
*
intros.
inv H11.
exists x;
exists x0;
exists tk;
repeat split;
eauto.
econstructor;
eauto.
clear IHs2;
destruct k'0.
{
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
-
econstructor.
-
econstructor.
-
simpl in H12;
inv H12.
-
simpl in H11;
inv H11. }
{
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
U V]]].
rewrite U;
econstructor;
eauto. }
{
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto. }
{
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto. }
{
generalize (
H3 _ eq_refl).
intros [
tk' [
U V]].
eauto. }
{
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
-
simpl in H11;
inv H11.
-
simpl in H12;
inv H12.
-
simpl in H11;
inv H11.
-
simpl in H11;
simpl in H12;
inv H11;
inv H12;
econstructor. }
*
intros.
inv H11.
*
simpl;
intros;
inv H11.
*
simpl;
intros;
inv H11.
econstructor;
eauto.
clear IHs2.
destruct k'0.
{
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
-
econstructor.
-
econstructor.
-
simpl in H12;
inv H12.
-
simpl in H11;
inv H11. }
{
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
U V]]].
rewrite U;
econstructor;
eauto. }
{
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto. }
{
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto. }
{
generalize (
H3 _ eq_refl).
intros [
tk' [
U V]].
eauto. }
{
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
-
simpl in H11;
inv H11.
-
simpl in H12;
inv H12.
-
simpl in H11;
inv H11.
-
simpl in H11;
simpl in H12;
inv H11;
inv H12;
econstructor. }
*
simpl;
intros.
inv H11.
*
simpl;
intros.
inv H11.
+
destruct k'.
*
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
{
econstructor. }
{
econstructor. }
{
simpl in H12;
inv H12. }
{
simpl in H11;
inv H11. }
*
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
U V]]].
rewrite U;
econstructor;
eauto.
*
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto.
*
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto.
*
generalize (
H3 _ eq_refl).
intros [
tk' [
U V]].
eauto.
*
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
{
simpl in H11;
inv H11. }
{
simpl in H12;
inv H12. }
{
simpl in H11;
inv H11. }
{
simpl in H11;
simpl in H12;
inv H11;
inv H12;
econstructor. }
-
intros.
inv H11.
-
intros.
inv H11.
-
simpl;
intros.
inv H11.
econstructor;
eauto.
destruct k'.
*
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
{
econstructor. }
{
econstructor. }
{
simpl in H12;
inv H12. }
{
simpl in H11;
inv H11. }
*
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
U V]]].
rewrite U;
econstructor;
eauto.
*
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto.
*
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto.
*
generalize (
H3 _ eq_refl).
intros [
tk' [
U V]].
eauto.
*
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
{
simpl in H11;
inv H11. }
{
simpl in H12;
inv H12. }
{
simpl in H11;
inv H11. }
{
simpl in H11;
simpl in H12;
inv H11;
inv H12;
econstructor. }
-
simpl;
intros;
inv H11.
-
simpl;
intros;
inv H11.
-
simpl;
intros;
inv H11.
econstructor;
eauto.
eapply unseq_match_stmt_cont;
eauto.
*
intros.
inv H11.
*
intros.
inv H11.
*
intros.
inv H11.
*
intros.
inv H11.
exists x;
exists x0;
exists tk;
repeat split;
eauto.
econstructor;
eauto.
clear IHs2;
destruct k'0.
{
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
-
econstructor.
-
econstructor.
-
simpl in H12;
inv H12.
-
simpl in H11;
inv H11. }
{
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
U V]]].
rewrite U;
econstructor;
eauto. }
{
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto. }
{
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto. }
{
generalize (
H3 _ eq_refl).
intros [
tk' [
U V]].
eauto. }
{
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
-
simpl in H11;
inv H11.
-
simpl in H12;
inv H12.
-
simpl in H11;
inv H11.
-
simpl in H11;
simpl in H12;
inv H11;
inv H12;
econstructor. }
*
intros.
inv H11.
*
simpl;
intros;
inv H11.
*
simpl;
intros;
inv H11.
econstructor;
eauto.
clear IHs2.
destruct k'0.
{
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
-
econstructor.
-
econstructor.
-
simpl in H12;
inv H12.
-
simpl in H11;
inv H11. }
{
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
U V]]].
rewrite U;
econstructor;
eauto. }
{
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto. }
{
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto. }
{
generalize (
H3 _ eq_refl).
intros [
tk' [
U V]].
eauto. }
{
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
-
simpl in H11;
inv H11.
-
simpl in H12;
inv H12.
-
simpl in H11;
inv H11.
-
simpl in H11;
simpl in H12;
inv H11;
inv H12;
econstructor. }
*
simpl;
intros.
inv H11.
*
simpl;
intros.
inv H11.
-
inv H9.
+
econstructor;
simpl;
eauto.
econstructor;
eauto.
eapply match_loops_context;
eauto.
+
econstructor 2;
simpl;
eauto.
econstructor;
eauto.
eapply match_loops_context;
eauto.
-
econstructor;
eauto.
eapply match_loops_context;
eauto. }
{
rewrite H12.
clear H11.
generalize (
IHs2 (
Kloop2 s1 s2 k)
x0 (
Kloop2 x x0 tk)).
clear IHs2;
intros.
rewrite Q in H11.
eapply H11.
-
intros.
inv H13.
-
intros.
inv H13.
-
intros.
inv H13.
-
intros.
inv H13.
exists x;
exists x0;
exists tk;
repeat split;
eauto.
econstructor;
eauto.
destruct k'.
{
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
-
econstructor.
-
econstructor.
-
simpl in H14;
inv H14.
-
simpl in H13;
inv H13. }
{
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
U V]]].
rewrite U;
econstructor;
eauto. }
{
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto. }
{
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto. }
{
generalize (
H3 _ eq_refl).
intros [
tk' [
U V]].
eauto. }
{
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
-
simpl in H13;
inv H13.
-
simpl in H14;
inv H14.
-
simpl in H13;
inv H13.
-
simpl in H13;
simpl in H14;
inv H13;
inv H14;
econstructor. }
-
intros.
inv H13.
-
simpl;
intros.
inv H13.
-
simpl;
intros.
inv H13.
econstructor;
eauto.
destruct k'.
{
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
-
econstructor.
-
econstructor.
-
simpl in H14;
inv H14.
-
simpl in H13;
inv H13. }
{
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
U V]]].
rewrite U;
econstructor;
eauto. }
{
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto. }
{
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto. }
{
generalize (
H3 _ eq_refl).
intros [
tk' [
U V]].
eauto. }
{
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
-
simpl in H13;
inv H13.
-
simpl in H14;
inv H14.
-
simpl in H13;
inv H13.
-
simpl in H13;
simpl in H14;
inv H13;
inv H14;
econstructor. }
-
simpl;
intros;
inv H13.
-
simpl;
intros;
inv H13.
-
eauto.
-
inv H9.
+
econstructor;
simpl;
eauto.
econstructor;
eauto.
eapply match_loops_context;
eauto.
+
econstructor 2;
simpl;
eauto.
econstructor;
eauto.
eapply match_loops_context;
eauto.
-
econstructor;
eauto.
eapply match_loops_context;
eauto. }
*
intros Q.
generalize (
IHs1 (
Kloop1 s1 s2 k)
x (
Kloop1 x x0 tk)).
clear IHs1;
intros.
rewrite H8 in H11.
assert (
find_label lbl x (
Kloop1 x x0 tk) =
None).
{
eapply H11;
clear H11;
eauto.
-
intros.
inv H11.
-
intros.
inv H11.
-
intros.
inv H11.
exists x;
exists x0;
exists tk.
repeat split;
eauto.
+
econstructor;
eauto.
eapply unseq_match_stmt_cont;
eauto.
*
intros.
inv H11.
*
intros.
inv H11.
*
intros.
inv H11.
*
intros.
inv H11.
exists x;
exists x0;
exists tk;
repeat split;
eauto.
econstructor;
eauto.
clear IHs2;
destruct k'0.
{
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
-
econstructor.
-
econstructor.
-
simpl in H12;
inv H12.
-
simpl in H11;
inv H11. }
{
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
U V]]].
rewrite U;
econstructor;
eauto. }
{
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto. }
{
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto. }
{
generalize (
H3 _ eq_refl).
intros [
tk' [
U V]].
eauto. }
{
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
-
simpl in H11;
inv H11.
-
simpl in H12;
inv H12.
-
simpl in H11;
inv H11.
-
simpl in H11;
simpl in H12;
inv H11;
inv H12;
econstructor. }
*
intros.
inv H11.
*
simpl;
intros;
inv H11.
*
simpl;
intros;
inv H11.
econstructor;
eauto.
clear IHs2.
destruct k'0.
{
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
-
econstructor.
-
econstructor.
-
simpl in H12;
inv H12.
-
simpl in H11;
inv H11. }
{
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
U V]]].
rewrite U;
econstructor;
eauto. }
{
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto. }
{
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto. }
{
generalize (
H3 _ eq_refl).
intros [
tk' [
U V]].
eauto. }
{
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
-
simpl in H11;
inv H11.
-
simpl in H12;
inv H12.
-
simpl in H11;
inv H11.
-
simpl in H11;
simpl in H12;
inv H11;
inv H12;
econstructor. }
*
simpl;
intros.
inv H11.
*
simpl;
intros.
inv H11.
+
destruct k'.
*
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
{
econstructor. }
{
econstructor. }
{
simpl in H12;
inv H12. }
{
simpl in H11;
inv H11. }
*
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
U V]]].
rewrite U;
econstructor;
eauto.
*
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto.
*
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto.
*
generalize (
H3 _ eq_refl).
intros [
tk' [
U V]].
eauto.
*
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
{
simpl in H11;
inv H11. }
{
simpl in H12;
inv H12. }
{
simpl in H11;
inv H11. }
{
simpl in H11;
simpl in H12;
inv H11;
inv H12;
econstructor. }
-
intros.
inv H11.
-
intros.
inv H11.
-
simpl;
intros.
inv H11.
econstructor;
eauto.
destruct k'.
*
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
{
econstructor. }
{
econstructor. }
{
simpl in H12;
inv H12. }
{
simpl in H11;
inv H11. }
*
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
U V]]].
rewrite U;
econstructor;
eauto.
*
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto.
*
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto.
*
generalize (
H3 _ eq_refl).
intros [
tk' [
U V]].
eauto.
*
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
{
simpl in H11;
inv H11. }
{
simpl in H12;
inv H12. }
{
simpl in H11;
inv H11. }
{
simpl in H11;
simpl in H12;
inv H11;
inv H12;
econstructor. }
-
simpl;
intros;
inv H11.
-
simpl;
intros;
inv H11.
-
simpl;
intros;
inv H11.
econstructor;
eauto.
eapply unseq_match_stmt_cont;
eauto.
*
intros.
inv H11.
*
intros.
inv H11.
*
intros.
inv H11.
*
intros.
inv H11.
exists x;
exists x0;
exists tk;
repeat split;
eauto.
econstructor;
eauto.
clear IHs2;
destruct k'0.
{
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
-
econstructor.
-
econstructor.
-
simpl in H12;
inv H12.
-
simpl in H11;
inv H11. }
{
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
U V]]].
rewrite U;
econstructor;
eauto. }
{
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto. }
{
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto. }
{
generalize (
H3 _ eq_refl).
intros [
tk' [
U V]].
eauto. }
{
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
-
simpl in H11;
inv H11.
-
simpl in H12;
inv H12.
-
simpl in H11;
inv H11.
-
simpl in H11;
simpl in H12;
inv H11;
inv H12;
econstructor. }
*
intros.
inv H11.
*
simpl;
intros;
inv H11.
*
simpl;
intros;
inv H11.
econstructor;
eauto.
clear IHs2.
destruct k'0.
{
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
-
econstructor.
-
econstructor.
-
simpl in H12;
inv H12.
-
simpl in H11;
inv H11. }
{
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
U V]]].
rewrite U;
econstructor;
eauto. }
{
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto. }
{
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto. }
{
generalize (
H3 _ eq_refl).
intros [
tk' [
U V]].
eauto. }
{
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
-
simpl in H11;
inv H11.
-
simpl in H12;
inv H12.
-
simpl in H11;
inv H11.
-
simpl in H11;
simpl in H12;
inv H11;
inv H12;
econstructor. }
*
simpl;
intros.
inv H11.
*
simpl;
intros.
inv H11.
-
inv H9.
+
econstructor;
simpl;
eauto.
econstructor;
eauto.
eapply match_loops_context;
eauto.
+
econstructor 2;
simpl;
eauto.
econstructor;
eauto.
eapply match_loops_context;
eauto.
-
econstructor;
eauto.
eapply match_loops_context;
eauto. }
{
rewrite H12.
clear H11.
generalize (
IHs2 (
Kloop2 s1 s2 k)
x0 (
Kloop2 x x0 tk)).
clear IHs2;
intros.
rewrite Q in H11.
eapply H11.
-
intros.
inv H13.
-
intros.
inv H13.
-
intros.
inv H13.
-
intros.
inv H13.
exists x;
exists x0;
exists tk;
repeat split;
eauto.
econstructor;
eauto.
destruct k'.
{
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
-
econstructor.
-
econstructor.
-
simpl in H14;
inv H14.
-
simpl in H13;
inv H13. }
{
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
U V]]].
rewrite U;
econstructor;
eauto. }
{
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto. }
{
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto. }
{
generalize (
H3 _ eq_refl).
intros [
tk' [
U V]].
eauto. }
{
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
-
simpl in H13;
inv H13.
-
simpl in H14;
inv H14.
-
simpl in H13;
inv H13.
-
simpl in H13;
simpl in H14;
inv H13;
inv H14;
econstructor. }
-
intros.
inv H13.
-
simpl;
intros.
inv H13.
-
simpl;
intros.
inv H13.
econstructor;
eauto.
destruct k'.
{
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
-
econstructor.
-
econstructor.
-
simpl in H14;
inv H14.
-
simpl in H13;
inv H13. }
{
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
U V]]].
rewrite U;
econstructor;
eauto. }
{
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto. }
{
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto. }
{
generalize (
H3 _ eq_refl).
intros [
tk' [
U V]].
eauto. }
{
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V.
-
simpl in H13;
inv H13.
-
simpl in H14;
inv H14.
-
simpl in H13;
inv H13.
-
simpl in H13;
simpl in H14;
inv H13;
inv H14;
econstructor. }
-
simpl;
intros;
inv H13.
-
simpl;
intros;
inv H13.
-
eauto.
-
inv H9.
+
econstructor;
simpl;
eauto.
econstructor;
eauto.
eapply match_loops_context;
eauto.
+
econstructor 2;
simpl;
eauto.
econstructor;
eauto.
eapply match_loops_context;
eauto.
-
econstructor;
eauto.
eapply match_loops_context;
eauto. }
-
simpl.
simpl in H8.
destruct (
context k);
inv H8;
simpl;
eauto.
-
simpl.
simpl in H8.
destruct (
context'
k);
inv H8;
simpl;
eauto.
-
simpl.
simpl in H8.
monadInv H8.
simpl.
eapply find_label_ls_match_stmt_cont;
eauto.
+
intros.
inv H8.
+
intros.
inv H8.
+
intros.
inv H8.
exists tk;
split;
eauto.
econstructor;
eauto.
destruct k'.
*
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V;
try (
econstructor;
eauto;
fail).
{
simpl in H11;
inv H11. }
{
simpl in H8;
inv H8. }
*
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
U V]]].
rewrite U;
econstructor;
eauto.
*
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto.
*
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto.
*
generalize (
H3 _ eq_refl).
intros [
tk' [
U V]].
eauto.
*
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V;
try (
econstructor;
eauto).
{
simpl in H8;
inv H8. }
{
simpl in H11;
inv H11. }
{
simpl in H8;
inv H8. }
{
simpl in H8;
simpl in H11;
inv H8;
inv H11;
econstructor. }
+
econstructor;
eauto.
destruct k.
*
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V;
try (
econstructor;
eauto;
fail).
{
simpl in H11;
inv H11. }
{
simpl in H8;
inv H8. }
*
generalize (
H0 _ _ eq_refl).
intros [
s'' [
tk' [
U V]]].
rewrite U;
econstructor;
eauto.
*
generalize (
H1 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto.
*
generalize (
H2 _ _ _ eq_refl).
intros [
s1' [
s2' [
tk' [
U [
V [
W [
X Y]]]]]]].
eauto.
*
generalize (
H3 _ eq_refl).
intros [
tk' [
U V]].
eauto.
*
generalize (
H I).
intros [
U V].
destruct tk;
inv U;
inv V;
try (
econstructor;
eauto).
{
simpl in H8;
inv H8. }
{
simpl in H11;
inv H11. }
{
simpl in H8;
inv H8. }
{
simpl in H8;
simpl in H11;
inv H8;
inv H11;
econstructor. }
+
simpl;
intros;
inv H8.
econstructor;
eauto.
simpl;
rewrite H12;
eauto.
+
simpl;
eauto.
+
inv H9.
*
econstructor;
eauto.
econstructor;
eauto.
eapply match_loops_context;
eauto.
*
econstructor 2;
eauto.
econstructor;
eauto.
eapply match_loops_context;
eauto.
+
econstructor;
eauto.
eapply match_loops_context;
eauto.
-
monadInv H8.
simpl.
destruct (
ident_eq lbl l).
+
exists x;
exists tk;
repeat split;
eauto.
eapply unseq_match_stmt_cont;
eauto.
+
eapply IHs;
eauto. }
{
induction ls;
intros.
-
simpl.
monadInv H5.
simpl;
eauto.
-
generalize (
unseq_match_lstmt_cont (
LScons o s ls)
ls'
k tk H H0 H1 H2 H3 H4 H5).
intros QQ.
simpl.
simpl in H5.
monadInv H5.
case_eq (
find_label lbl s (
Kseq (
seq_of_labeled_statement ls)
k));
intros.
+
destruct p.
simpl.
generalize (
find_label_match_stmt_cont lbl s (
Kseq (
seq_of_labeled_statement ls)
k)
x0 (
Kseq (
seq_of_labeled_statement x)
tk)).
clear find_label_ls_match_stmt_cont;
clear find_label_match_stmt_cont.
intros.
rewrite H5 in H8.
assert (
exists (
ts' :
statement) (
tk' :
cont),
find_label lbl x0 (
Kseq (
seq_of_labeled_statement x)
tk) =
Some (
ts',
tk') /\
match_stmt_cont s0 ts'
c tk' /\
match_call_cont c tk' /\
match_loops c tk').
eapply H8;
clear H8.
*
intros.
inv H8.
*
intros;
inv H8.
econstructor;
econstructor;
split;
eauto.
eapply unseq_match_lstmt_cont;
eauto.
*
intros;
inv H8.
*
intros;
inv H8.
*
intros;
inv H8.
*
simpl.
intros.
econstructor;
eauto.
simpl;
rewrite H8;
eauto.
*
simpl.
intros.
econstructor;
eauto.
simpl;
rewrite H8;
eauto.
*
simpl;
intros.
econstructor;
eauto.
simpl;
rewrite H8;
eauto.
*
simpl;
intros.
econstructor;
eauto.
simpl;
rewrite H8;
eauto.
*
exact EQ1.
*
inv H6.
{
econstructor;
eauto.
econstructor;
eauto.
simpl;
eapply match_loops_context;
eauto. }
{
econstructor 2;
eauto.
econstructor;
eauto.
simpl;
eapply match_loops_context;
eauto. }
*
econstructor;
eauto.
simpl;
eapply match_loops_context;
eauto.
*
clear H8.
destruct H9 as [
ts' [
tk' [
A [
B [
C D]]]]].
rewrite A.
exists ts';
exists tk'.
repeat split;
eauto.
+
simpl.
generalize (
find_label_match_stmt_cont lbl s (
Kseq (
seq_of_labeled_statement ls)
k)
x0 (
Kseq (
seq_of_labeled_statement x)
tk)).
clear find_label_match_stmt_cont.
intros.
rewrite H5 in H8.
assert (
find_label lbl x0 (
Kseq (
seq_of_labeled_statement x)
tk) =
None).
eapply H8;
clear H8.
*
intros.
inv H8.
*
intros;
inv H8.
econstructor;
econstructor;
split;
eauto.
eapply unseq_match_lstmt_cont;
eauto.
*
intros;
inv H8.
*
intros;
inv H8.
*
intros;
inv H8.
*
simpl.
intros.
econstructor;
eauto.
simpl;
rewrite H8;
eauto.
*
simpl.
intros.
econstructor;
eauto.
simpl;
rewrite H8;
eauto.
*
simpl;
intros.
econstructor;
eauto.
simpl;
rewrite H8;
eauto.
*
simpl;
intros.
econstructor;
eauto.
simpl;
rewrite H8;
eauto.
*
exact EQ1.
*
inv H6.
{
econstructor;
eauto.
econstructor;
eauto.
simpl;
eapply match_loops_context;
eauto. }
{
econstructor 2;
eauto.
econstructor;
eauto.
simpl;
eapply match_loops_context;
eauto. }
*
econstructor;
eauto.
simpl;
eapply match_loops_context;
eauto.
*
clear H8.
rewrite H9.
eapply IHls;
eauto. }
Qed.
Matching states.
Inductive match_states: Clight.state -> Clight.state -> Prop :=
| match_call_states:
forall fd vargs k m tfd tk targs tres cconv
(TRFD: transf_fundef fd = OK tfd)
(MCONT: match_call_cont k tk)
(FUNTY: type_of_fundef fd = Tfunction targs tres cconv)
(CCONT: is_call_cont k)
(TCONT: is_call_cont tk),
match_states (Callstate fd vargs k m)
(Callstate tfd vargs tk m)
| match_return_state:
forall v k m tk
(MCONT: match_call_cont k tk)
(CCONT: is_call_cont k)
(TCONT: is_call_cont tk),
match_states (Returnstate v k m)
(Returnstate v tk m)
| match_regular_states:
forall f s k e le m tf ts tk
(MCONT: match_call_cont k tk)
(TRF: transf_function f = OK tf)
(MSTMT: match_stmt_cont s ts k tk)
(MLOOPS: match_loops k tk),
match_states (State f s k e le m)
(State tf ts tk e le m).
Lemma initial_states_simulation:
forall S, Clight.initial_state prog S ->
exists R, Clight.initial_state tprog R /\ match_states S R.
Proof.
Lemma final_states_simulation:
forall S R r,
match_states S R -> Clight.final_state S r -> Clight.final_state R r.
Proof.
intros; inv H0; inv H; inv MCONT.
- destruct tk; inv TCONT; simpl in H0; inv H0.
econstructor.
- simpl in H; inv H.
Qed.
Simulation diagram.
Lemma simulation:
forall s1 t s1', Clight.step1 ge s1 t s1' ->
forall s2 (MS: match_states s1 s2),
(exists s2', Clight.step1 tge s2 t s2' /\ match_states s1' s2')
\/ (measure s1' < measure s1 /\ t = E0 /\ match_states s1' s2)%nat.
Proof.
induction 1;
simpl;
intros;
inv MS.
-
left.
inv MSTMT.
econstructor.
split.
+
econstructor;
eauto.
*
eapply eval_lvalue_unchanged;
eauto.
*
eapply eval_expr_unchanged;
eauto.
*
rewrite comp_env_preserved;
eauto.
+
econstructor;
eauto.
-
left;
inv MSTMT;
econstructor;
split.
+
econstructor;
eauto.
eapply eval_expr_unchanged;
eauto.
+
econstructor;
eauto.
-
left;
inv MSTMT.
generalize (
functions_translated vf fd H2).
intros [
tfd [
A B]].
econstructor;
split.
+
econstructor.
*
exact H.
*
eapply eval_expr_unchanged;
eauto.
*
eapply eval_exprlist_unchanged;
eauto.
*
exact A.
*
rewrite <-
H3;
eapply type_of_fundef_preserved;
eauto.
+
econstructor;
eauto.
econstructor 2;
simpl;
eauto.
econstructor.
inv MLOOPS;
simpl;
try econstructor;
eauto.
repeat rewrite context_context_is_context;
eauto.
econstructor.
econstructor.
-
left;
inv MSTMT;
econstructor;
split.
+
econstructor;
eauto.
*
eapply eval_exprlist_unchanged;
eauto.
*
eapply external_call_symbols_preserved;
eauto.
eapply symbols_preserved.
eapply public_preserved.
eapply varinfo_preserved.
+
econstructor;
eauto.
-
inv MSTMT.
+
right;
repeat split;
eauto.
*
omega.
*
econstructor;
eauto.
inv MCONT.
econstructor;
eauto.
inv MLOOPS;
econstructor;
simpl;
try econstructor;
eauto.
repeat rewrite context_context_is_context;
eauto.
econstructor 2;
eauto.
inv MLOOPS;
econstructor;
simpl;
try econstructor;
eauto.
repeat rewrite context_context_is_context;
eauto.
inv MLOOPS;
econstructor;
simpl;
try econstructor;
eauto.
repeat rewrite context_context_is_context.
eauto.
+
left;
econstructor;
split.
*
econstructor;
eauto.
*
econstructor;
eauto.
inv MCONT.
econstructor;
eauto.
inv MLOOPS;
econstructor;
simpl;
try econstructor;
eauto.
repeat rewrite context_context_is_context;
eauto.
econstructor 2;
eauto.
inv MLOOPS;
econstructor;
simpl;
try econstructor;
eauto.
repeat rewrite context_context_is_context;
eauto.
inv MLOOPS;
econstructor;
simpl;
try econstructor;
eauto.
repeat rewrite context_context_is_context.
eauto.
-
inv MSTMT.
+
left;
econstructor;
split.
*
econstructor;
eauto.
*
econstructor;
eauto.
inv MCONT.
econstructor;
eauto.
inv MLOOPS.
simpl in H.
econstructor;
eauto.
econstructor 2;
eauto.
inv MLOOPS.
simpl in H.
econstructor;
eauto.
inv MLOOPS.
simpl in H.
econstructor;
eauto.
+
right;
repeat split;
eauto.
*
omega.
*
econstructor;
eauto.
inv MCONT.
econstructor;
eauto.
inv MLOOPS.
simpl in H.
econstructor;
eauto.
econstructor 2;
eauto.
inv MLOOPS.
simpl in H.
econstructor;
eauto.
inv MLOOPS.
simpl in H.
econstructor;
eauto.
-
inv MSTMT.
+
left.
econstructor;
split.
*
econstructor.
*
econstructor;
eauto.
inv MCONT.
econstructor;
eauto.
inv MLOOPS.
simpl in H.
econstructor;
eauto.
econstructor 2;
eauto.
inv MLOOPS.
simpl in H;
econstructor;
eauto.
inv MLOOPS.
simpl in H.
econstructor;
eauto.
+
right;
repeat split;
eauto.
*
omega.
*
econstructor;
eauto.
inv MCONT.
econstructor;
eauto.
inv MLOOPS.
simpl in H.
econstructor;
eauto.
econstructor 2;
eauto.
inv MLOOPS.
simpl in H.
econstructor;
eauto.
inv MLOOPS.
simpl in H.
econstructor;
eauto.
-
inv MSTMT.
+
left.
econstructor;
split.
*
econstructor.
*
econstructor;
eauto.
inv MCONT.
econstructor;
eauto.
inv MLOOPS.
simpl in H.
econstructor;
eauto.
econstructor 2;
eauto.
inv MLOOPS.
simpl in H;
econstructor;
eauto.
inv MLOOPS.
simpl in H.
econstructor;
eauto.
+
right;
repeat split;
eauto.
*
omega.
*
econstructor;
eauto.
inv MCONT.
econstructor;
eauto.
inv MLOOPS.
simpl in H.
econstructor;
eauto.
econstructor 2;
eauto.
inv MLOOPS.
simpl in H.
econstructor;
eauto.
econstructor;
eauto.
inv MLOOPS.
simpl in H.
econstructor;
eauto.
repeat rewrite context_context_is_context;
eauto.
-
inv MSTMT;
left;
econstructor;
split.
+
econstructor.
*
eapply eval_expr_unchanged;
eauto.
*
exact H0.
+
destruct b;
econstructor;
eauto.
-
inv MSTMT;
left;
econstructor;
split.
+
econstructor;
eauto.
+
econstructor;
eauto.
inv MCONT.
*
econstructor;
eauto.
econstructor;
eauto.
econstructor;
eauto.
inv MLOOPS;
eauto;
try (
simpl;
econstructor;
eauto).
*
econstructor 2;
eauto.
econstructor;
eauto.
econstructor;
eauto.
inv MLOOPS;
eauto;
try (
simpl;
econstructor;
eauto).
*
econstructor;
eauto.
econstructor;
eauto.
inv MLOOPS;
eauto;
try (
simpl;
econstructor;
eauto).
-
destruct H;
subst x;
inv MSTMT.
+
left;
econstructor;
split.
*
econstructor;
eauto.
*
econstructor;
eauto.
inv MCONT.
{
econstructor;
eauto.
econstructor;
eauto.
eapply match_loop1_stmt_cont;
eauto.
eapply match_loop1_context;
eauto. }
{
econstructor 2;
eauto.
econstructor;
eauto.
eapply match_loop1_stmt_cont;
eauto.
eapply match_loop1_context;
eauto. }
{
econstructor;
eauto.
eapply match_loop1_stmt_cont;
eauto.
eapply match_loop1_context;
eauto. }
+
left;
econstructor;
split.
*
econstructor;
eauto.
*
econstructor;
eauto.
inv MCONT.
{
econstructor;
eauto.
econstructor;
eauto.
eapply match_loop1_stmt_cont;
eauto.
eapply match_loop1_context;
eauto. }
{
econstructor 2;
eauto.
econstructor;
eauto.
eapply match_loop1_stmt_cont;
eauto.
eapply match_loop1_context;
eauto. }
{
econstructor;
eauto.
eapply match_loop1_stmt_cont;
eauto.
eapply match_loop1_context;
eauto. }
-
inv MSTMT;
left;
econstructor;
split.
+
eapply step_break_loop1;
eauto.
+
econstructor;
eauto.
inv MCONT.
econstructor;
eauto.
econstructor.
eapply match_loop1_context;
eauto.
econstructor 2;
eauto.
econstructor.
eapply match_loop1_context;
eauto.
econstructor.
eapply match_loop1_context;
eauto.
-
inv MSTMT;
left;
econstructor;
split.
+
econstructor;
eauto.
+
econstructor;
eauto.
*
inv MCONT.
econstructor;
eauto.
econstructor;
eapply match_loop2_context;
eauto.
econstructor 2;
eauto.
econstructor;
eapply match_loop2_context;
eauto.
*
eapply match_loop2_stmt_cont;
eauto.
*
econstructor;
eapply match_loop2_context;
eauto.
-
inv MSTMT;
left;
econstructor;
split.
+
eapply step_break_loop2;
eauto.
+
econstructor;
eauto.
inv MCONT;
eauto.
econstructor;
eauto.
econstructor;
eapply match_loop2_context;
eauto.
econstructor 2;
eauto.
econstructor;
eapply match_loop2_context;
eauto.
econstructor.
eapply match_loop2_context;
eauto.
-
inv MSTMT;
left;
econstructor;
split.
+
econstructor;
eauto.
unfold blocks_of_env.
unfold block_of_binding.
rewrite comp_env_preserved;
eauto.
+
econstructor;
eauto.
*
inv MCONT;
eauto.
{
rewrite H0;
rewrite H1;
econstructor;
simpl;
eauto.
econstructor. }
{
rewrite H0;
rewrite H1;
econstructor 2;
simpl;
eauto.
rewrite <-
H0;
rewrite <-
H1;
eapply match_loops_call_cont;
eauto. }
*
eapply is_call_cont_call_cont.
*
eapply is_call_cont_call_cont.
-
inv MSTMT;
left;
econstructor;
split.
+
econstructor;
eauto.
*
eapply eval_expr_unchanged;
eauto.
*
monadInv TRF;
simpl;
eauto.
*
unfold blocks_of_env.
unfold block_of_binding.
rewrite comp_env_preserved;
eauto.
+
econstructor;
eauto.
*
inv MCONT;
eauto.
{
rewrite H2;
rewrite H3;
econstructor;
simpl;
eauto.
econstructor. }
{
rewrite H2;
rewrite H3;
econstructor 2;
simpl;
eauto.
rewrite <-
H2;
rewrite <-
H3;
eapply match_loops_call_cont;
eauto. }
*
eapply is_call_cont_call_cont.
*
eapply is_call_cont_call_cont.
-
destruct k;
inv H.
+
inv MSTMT;
left;
econstructor;
split.
*
econstructor;
eauto.
econstructor.
unfold blocks_of_env.
unfold block_of_binding.
rewrite comp_env_preserved;
eauto.
*
econstructor;
eauto.
econstructor.
econstructor.
+
inv MSTMT;
left;
econstructor;
split.
*
econstructor;
eauto.
econstructor.
unfold blocks_of_env.
unfold block_of_binding.
rewrite comp_env_preserved;
eauto.
*
econstructor;
eauto.
econstructor.
econstructor.
-
inv MSTMT;
left;
econstructor;
split.
+
simpl;
econstructor;
eauto.
eapply eval_expr_unchanged;
eauto.
+
econstructor;
eauto.
*
inv MCONT.
econstructor;
eauto.
inv MLOOPS;
econstructor;
simpl;
eauto;
try (
econstructor;
eauto;
fail).
econstructor 2;
eauto.
inv MLOOPS;
econstructor;
simpl;
eauto;
try (
econstructor;
eauto;
fail).
*
inv MLOOPS;
econstructor;
simpl;
eauto;
try (
econstructor;
eauto;
fail).
-
destruct H;
subst x.
+
inv MSTMT;
left;
econstructor;
split.
*
eapply step_skip_break_switch;
eauto.
*
econstructor;
eauto.
{
inv MCONT.
econstructor;
eauto.
econstructor;
eapply match_switch_context;
eauto.
econstructor 2;
eauto.
econstructor;
eapply match_switch_context;
eauto. }
{
econstructor;
eapply match_switch_context;
eauto. }
+
inv MSTMT;
left;
econstructor;
split.
*
eapply step_skip_break_switch;
eauto.
*
econstructor;
eauto.
{
inv MCONT.
econstructor;
eauto.
econstructor;
eapply match_switch_context;
eauto.
econstructor 2;
eauto.
econstructor;
eapply match_switch_context;
eauto. }
{
econstructor;
eapply match_switch_context;
eauto. }
-
inv MSTMT;
left;
econstructor;
split.
+
eapply step_continue_switch.
+
econstructor;
eauto.
*
inv MCONT.
econstructor;
eauto.
econstructor;
eapply match_switch_context;
eauto.
econstructor 2;
eauto.
econstructor;
eapply match_switch_context;
eauto.
*
econstructor;
eapply match_switch_context;
eauto.
-
inv MSTMT;
left;
econstructor;
split.
+
econstructor.
+
econstructor;
eauto.
-
inv MSTMT.
monadInv TRF.
generalize (
find_label_match_stmt_cont lbl (
fn_body f) (
call_cont k)
x (
call_cont tk)).
rewrite H;
intros.
assert (
exists (
ts' :
statement) (
tk' :
cont),
find_label lbl x (
call_cont tk) =
Some (
ts',
tk') /\
match_stmt_cont s'
ts'
k'
tk' /\
match_call_cont k'
tk' /\
match_loops k'
tk').
apply H0;
clear H0.
{
intros.
split.
eapply is_call_cont_call_cont.
eapply match_call_cont_call_cont;
eauto. }
{
intros.
generalize (
is_call_cont_call_cont k);
intros.
destruct (
call_cont k);
inv H1;
inv H0. }
{
intros.
generalize (
is_call_cont_call_cont k);
intros.
destruct (
call_cont k);
inv H1;
inv H0. }
{
intros.
generalize (
is_call_cont_call_cont k);
intros.
destruct (
call_cont k);
inv H1;
inv H0. }
{
intros.
generalize (
is_call_cont_call_cont k);
intros.
destruct (
call_cont k);
inv H1;
inv H0. }
{
intros.
generalize (
is_call_cont_call_cont k);
intros.
destruct (
call_cont k);
inv H1;
inv H0. }
{
intros.
generalize (
is_call_cont_call_cont k);
intros.
destruct (
call_cont k);
inv H1;
inv H0. }
{
intros.
generalize (
is_call_cont_call_cont k);
intros.
destruct (
call_cont k);
inv H1;
inv H0. }
{
intros.
generalize (
is_call_cont_call_cont k);
intros.
destruct (
call_cont k);
inv H1;
inv H0. }
{
rewrite (
unseq_cont_ty (
fn_body f) (
call_cont k)
Kstop).
assumption.
generalize (
is_call_cont_call_cont k);
intros CCONT.
destruct (
call_cont k);
inv CCONT;
econstructor. }
{
eapply match_call_cont_call_cont;
eauto. }
{
eapply match_loops_call_cont;
eauto. }
clear H0.
destruct H1 as [
ts' [
tk' [
A [
B [
C D]]]]].
left.
econstructor.
split.
+
econstructor;
simpl;
eauto.
+
econstructor;
eauto.
unfold transf_function.
rewrite EQ;
eauto.
-
monadInv TRFD;
inv H;
left;
simpl;
econstructor;
split.
+
econstructor;
eauto.
econstructor;
simpl;
eauto.
monadInv EQ;
eauto.
monadInv EQ;
eapply alloc_variables_preserved;
eauto.
monadInv EQ;
eapply bind_parameters_preserved;
eauto.
+
simpl.
monadInv EQ;
econstructor;
eauto.
*
unfold transf_function.
rewrite EQ0;
simpl;
auto.
*
simpl.
eapply unseq_match_stmt_cont;
eauto.
{
intros.
subst k;
inv CCONT. }
{
intros;
subst k;
inv CCONT. }
{
intros;
subst k;
inv CCONT. }
{
intros;
subst k;
inv CCONT. }
{
intros.
destruct k;
inv CCONT;
inv H. }
{
intros.
destruct k;
inv CCONT;
inv H. }
{
intros.
destruct k;
inv CCONT;
inv H. }
{
intros.
destruct k;
inv CCONT;
inv H. }
{
rewrite (
unseq_cont_ty (
fn_body f)
k Kstop).
assumption.
destruct k;
inv CCONT;
econstructor. }
*
inv MCONT;
eauto.
-
monadInv TRFD.
left;
econstructor;
split.
+
econstructor;
eauto.
eapply external_call_symbols_preserved;
eauto.
exact symbols_preserved.
exact public_preserved.
exact varinfo_preserved.
+
econstructor;
eauto.
-
inv MCONT.
+
simpl in H;
inv H.
+
simpl in H;
inv H.
destruct tk;
inv TCONT.
simpl in H0;
inv H0.
simpl in H0;
inv H0.
left.
econstructor;
split.
*
econstructor.
*
econstructor;
eauto.
econstructor;
eapply match_call_context;
eauto.
Qed.
Theorem transf_program_correct:
forward_simulation (semantics1 prog) (semantics1 tprog).
Proof.
End PRESERVATION.