diff options
Diffstat (limited to 'backend/CleanupLabelstyping.v')
-rw-r--r-- | backend/CleanupLabelstyping.v | 59 |
1 files changed, 0 insertions, 59 deletions
diff --git a/backend/CleanupLabelstyping.v b/backend/CleanupLabelstyping.v deleted file mode 100644 index 11b516fe..00000000 --- a/backend/CleanupLabelstyping.v +++ /dev/null @@ -1,59 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** Type preservation for the CleanupLabels pass *) - -Require Import Coqlib. -Require Import Maps. -Require Import AST. -Require Import Op. -Require Import Locations. -Require Import LTLin. -Require Import CleanupLabels. -Require Import LTLintyping. - -Lemma in_remove_unused_labels: - forall bto i c, In i (remove_unused_labels bto c) -> In i c. -Proof. - unfold remove_unused_labels, remove_unused. induction c; simpl. - auto. - rewrite list_fold_right_eq. destruct a; simpl; intuition. - destruct (Labelset.mem l bto); simpl in H; intuition. -Qed. - -Lemma wt_transf_function: - forall f, - wt_function f -> - wt_function (transf_function f). -Proof. - intros. inv H. constructor; simpl; auto. - unfold cleanup_labels; red; intros. - apply wt_instrs. eapply in_remove_unused_labels; eauto. -Qed. - -Lemma wt_transf_fundef: - forall f, - wt_fundef f -> - wt_fundef (transf_fundef f). -Proof. - induction 1. constructor. constructor. apply wt_transf_function; auto. -Qed. - -Lemma program_typing_preserved: - forall p, - wt_program p -> - wt_program (transf_program p). -Proof. - intros; red; intros. - exploit transform_program_function; eauto. intros [f1 [A B]]. subst f. - apply wt_transf_fundef. eapply H; eauto. -Qed. |