diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-08-03 15:32:27 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-08-03 15:32:27 +0000 |
commit | 213bf38509f4f92545d4c5749c25a55b9a9dda36 (patch) | |
tree | a40df8011ab5fabb0de362befc53e7af164c70ae /cfrontend/Cshmgenproof1.v | |
parent | 88b98f00facde51bff705a3fb6c32a73937428cb (diff) | |
download | compcert-213bf38509f4f92545d4c5749c25a55b9a9dda36.tar.gz compcert-213bf38509f4f92545d4c5749c25a55b9a9dda36.zip |
Transition semantics for Clight and Csharpminor
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1119 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend/Cshmgenproof1.v')
-rw-r--r-- | cfrontend/Cshmgenproof1.v | 102 |
1 files changed, 38 insertions, 64 deletions
diff --git a/cfrontend/Cshmgenproof1.v b/cfrontend/Cshmgenproof1.v index bd9cf229..86ecd2a4 100644 --- a/cfrontend/Cshmgenproof1.v +++ b/cfrontend/Cshmgenproof1.v @@ -206,86 +206,60 @@ Proof. simpl. rewrite H6. auto. Qed. -Lemma transl_stmt_Sfor_start: - forall nbrk ncnt s1 e2 s3 s4 ts, - transl_statement nbrk ncnt (Sfor s1 e2 s3 s4) = OK ts -> - s1 <> Csyntax.Sskip -> - exists ts1, exists ts2, - ts = Sseq ts1 ts2 - /\ transl_statement nbrk ncnt s1 = OK ts1 - /\ transl_statement nbrk ncnt (Sfor Csyntax.Sskip e2 s3 s4) = OK ts2. +Lemma is_Sskip_true: + forall (A: Type) (a b: A), + (if is_Sskip Csyntax.Sskip then a else b) = a. Proof. - intros. simpl in H. destruct (is_Sskip s1). contradiction. - monadInv H. econstructor; econstructor. - split. reflexivity. split. auto. simpl. - destruct (is_Sskip Csyntax.Sskip). 2: tauto. - rewrite EQ1; rewrite EQ0; rewrite EQ2; auto. + intros. destruct (is_Sskip Csyntax.Sskip); congruence. Qed. -Open Local Scope error_monad_scope. - -Lemma transl_stmt_Sfor_not_start: - forall nbrk ncnt e2 e3 s1, - transl_statement nbrk ncnt (Sfor Csyntax.Sskip e2 e3 s1) = - (do te2 <- exit_if_false e2; - do te3 <- transl_statement nbrk ncnt e3; - do ts1 <- transl_statement 1%nat 0%nat s1; - OK (Sblock (Sloop (Sseq te2 (Sseq (Sblock ts1) te3))))). +Lemma is_Sskip_false: + forall (A: Type) (a b: A) s, + s <> Csyntax.Sskip -> + (if is_Sskip s then a else b) = b. Proof. - intros. simpl. destruct (is_Sskip Csyntax.Sskip). auto. congruence. + intros. destruct (is_Sskip s); congruence. Qed. -(** Properties related to switch constructs *) - -Fixpoint lblstmts_length (sl: labeled_statements) : nat := - match sl with - | LSdefault _ => 0%nat - | LScase _ _ sl' => S (lblstmts_length sl') - end. +(** Properties of labeled statements *) -Lemma switch_target_table_shift: - forall n sl base dfl, - switch_target n (S dfl) (switch_table sl (S base)) = - S(switch_target n dfl (switch_table sl base)). +Lemma transl_lbl_stmt_1: + forall nbrk ncnt n sl tsl, + transl_lbl_stmt nbrk ncnt sl = OK tsl -> + transl_lbl_stmt nbrk ncnt (Csem.select_switch n sl) = OK (select_switch n tsl). Proof. - induction sl; intros; simpl. - auto. - case (Int.eq n i). auto. auto. + induction sl; intros. + monadInv H. simpl. rewrite EQ. auto. + generalize H; intro TR. monadInv TR. simpl. + destruct (Int.eq i n). auto. auto. Qed. -Lemma length_switch_table: - forall sl base, List.length (switch_table sl base) = lblstmts_length sl. +Lemma transl_lbl_stmt_2: + forall nbrk ncnt sl tsl, + transl_lbl_stmt nbrk ncnt sl = OK tsl -> + transl_statement nbrk ncnt (seq_of_labeled_statement sl) = OK (seq_of_lbl_stmt tsl). Proof. - induction sl; intro; simpl. auto. decEq; auto. + induction sl; intros. + monadInv H. simpl. auto. + monadInv H. simpl. rewrite EQ; simpl. rewrite (IHsl _ EQ1). simpl. auto. Qed. -Lemma block_seq_context_compose: - forall ctx2 ctx1, - block_seq_context ctx1 -> - block_seq_context ctx2 -> - block_seq_context (fun x => ctx1 (ctx2 x)). +Lemma wt_select_switch: + forall n tyenv sl, + wt_lblstmts tyenv sl -> + wt_lblstmts tyenv (Csem.select_switch n sl). Proof. - induction 1; intros; constructor; auto. + induction 1; simpl. + constructor; auto. + destruct (Int.eq n0 n). constructor; auto. auto. Qed. -Lemma transl_lblstmts_context: - forall sl nbrk ncnt body s, - transl_lblstmts nbrk ncnt sl body = OK s -> - exists ctx, block_seq_context ctx /\ s = ctx body. +Lemma wt_seq_of_labeled_statement: + forall tyenv sl, + wt_lblstmts tyenv sl -> + wt_stmt tyenv (seq_of_labeled_statement sl). Proof. - induction sl; simpl; intros. - monadInv H. exists (fun y => Sblock (Sseq y x)); split. - apply block_seq_context_ctx_1. apply block_seq_context_base_2. - auto. - monadInv H. exploit IHsl; eauto. intros [ctx [A B]]. - exists (fun y => ctx (Sblock (Sseq y x))); split. - apply block_seq_context_compose with - (ctx1 := ctx) - (ctx2 := fun y => Sblock (Sseq y x)). - auto. apply block_seq_context_ctx_1. apply block_seq_context_base_2. + induction 1; simpl. auto. + constructor; auto. Qed. - - - - |