From 2ae43be7b9d4118335c9d2cef6e098f9b9f807fe Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 9 Feb 2006 14:55:48 +0000 Subject: Initial import of compcert git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Tunnelingtyping.v | 44 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 44 insertions(+) create mode 100644 backend/Tunnelingtyping.v (limited to 'backend/Tunnelingtyping.v') diff --git a/backend/Tunnelingtyping.v b/backend/Tunnelingtyping.v new file mode 100644 index 00000000..29b74f12 --- /dev/null +++ b/backend/Tunnelingtyping.v @@ -0,0 +1,44 @@ +(** Type preservation for the Tunneling pass *) + +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Values. +Require Import Mem. +Require Import Globalenvs. +Require Import Op. +Require Import Locations. +Require Import LTL. +Require Import LTLtyping. +Require Import Tunneling. + +(** Tunneling preserves typing. *) + +Lemma wt_tunnel_block: + forall f b, + wt_block f b -> + wt_block (tunnel_function f) (tunnel_block f b). +Proof. + induction 1; simpl; econstructor; eauto. +Qed. + +Lemma wt_tunnel_function: + forall f, wt_function f -> wt_function (tunnel_function f). +Proof. + unfold wt_function; intros until b. + simpl. rewrite PTree.gmap. unfold option_map. + caseEq (fn_code f)!pc. intros b0 AT EQ. + injection EQ; intros; subst b. + apply wt_tunnel_block. eauto. + intros; discriminate. +Qed. + +Lemma program_typing_preserved: + forall (p: LTL.program), + wt_program p -> wt_program (tunnel_program p). +Proof. + intros; red; intros. + generalize (transform_program_function tunnel_function p i f H0). + intros [f0 [IN TRANSF]]. + subst f. apply wt_tunnel_function. eauto. +Qed. -- cgit