diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-10-27 10:23:16 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-10-27 10:23:16 +0000 |
commit | e882493e2c4b91024b42f0603ca6869e95695e85 (patch) | |
tree | 1d90dda6b56b541310d8b8703152fdcd49e8a7fa /backend/Linearizetyping.v | |
parent | 7f6ac3209e7fb7d822780c7e990fb604b11a6409 (diff) | |
download | compcert-e882493e2c4b91024b42f0603ca6869e95695e85.tar.gz compcert-e882493e2c4b91024b42f0603ca6869e95695e85.zip |
Linearize: utilisation d'une heuristique externe d'enumeration des noeuds du CFG
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@437 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Linearizetyping.v')
-rw-r--r-- | backend/Linearizetyping.v | 28 |
1 files changed, 15 insertions, 13 deletions
diff --git a/backend/Linearizetyping.v b/backend/Linearizetyping.v index c930ca52..473b3421 100644 --- a/backend/Linearizetyping.v +++ b/backend/Linearizetyping.v @@ -2,6 +2,7 @@ Require Import Coqlib. Require Import Maps. +Require Import Errors. Require Import AST. Require Import Op. Require Import Locations. @@ -65,33 +66,34 @@ Proof. Qed. Lemma wt_transf_function: - forall f, + forall f tf, LTLtyping.wt_function f -> - wt_function (transf_function f). + transf_function f = OK tf -> + wt_function tf. Proof. - intros. inv H. constructor; auto. + intros. inv H. monadInv H0. constructor; auto. simpl. apply wt_add_branch. apply wt_linearize_body. auto. Qed. Lemma wt_transf_fundef: - forall f, + forall f tf, LTLtyping.wt_fundef f -> - wt_fundef (transf_fundef f). + transf_fundef f = OK tf -> + wt_fundef tf. Proof. - induction 1; simpl. - constructor; assumption. - constructor; apply wt_transf_function; assumption. + induction 1; intros. monadInv H. constructor. + monadInv H0. constructor; eapply wt_transf_function; eauto. Qed. Lemma program_typing_preserved: - forall (p: LTL.program), + forall (p: LTL.program) (tp: LTLin.program), LTLtyping.wt_program p -> - LTLintyping.wt_program (transf_program p). + transf_program p = OK tp -> + LTLintyping.wt_program tp. Proof. intros; red; intros. - generalize (transform_program_function transf_fundef p i f H0). + generalize (transform_partial_program_function transf_fundef _ _ _ H0 H1). intros [f0 [IN TR]]. - subst f. apply wt_transf_fundef; auto. - apply (H i f0 IN). + eapply wt_transf_fundef; eauto. Qed. |