Type preservation for the Linearize pass
Require Import Coqlib.
Require Import Maps.
Require Import Errors.
Require Import Ast.
Require Import Op.
Require Import Locations.
Require Import LTL.
Require Import LTLtyping.
Require Import LTLin.
Require Import Linearize.
Require Import LTLintyping.
Require Import Conventions.
Type preservation for the linearization pass
Lemma wt_add_instr:
forall f i k,
wt_instr f i ->
wt_code f k ->
wt_code f (
i ::
k).
Proof.
intros; red; intros. elim H1; intro. subst i0; auto. auto.
Qed.
Lemma wt_add_branch:
forall f s k,
wt_code f k ->
wt_code f (
add_branch s k).
Proof.
Lemma wt_linearize_instr:
forall f instr,
LTLtyping.wt_instr f instr ->
forall k,
wt_code f.(
LTL.fn_sig)
k ->
wt_code f.(
LTL.fn_sig) (
linearize_instr instr k).
Proof.
induction 1;
simpl;
intros;
try (
case ifP;
intro);
try (
apply wt_add_instr; [
by constructor;
auto;
try (
rewrite H;
destruct cond)|]);
try (
by apply wt_add_branch);
try done.
Qed.
Lemma wt_linearize_body:
forall f,
(
forall pc instr,
f.(
LTL.fn_code)!
pc =
Some instr ->
LTLtyping.wt_instr f instr) ->
forall enum,
wt_code f.(
LTL.fn_sig) (
linearize_body f enum).
Proof.
Lemma wt_transf_function:
forall f tf,
LTLtyping.wt_function f ->
transf_function f =
OK tf ->
wt_function tf.
Proof.
Lemma wt_transf_fundef:
forall f tf,
LTLtyping.wt_fundef f ->
transf_fundef f =
OK tf ->
wt_fundef tf.
Proof.
induction 1;
intros.
monadInv H.
constructor.
monadInv H0.
constructor;
eapply wt_transf_function;
eauto.
Qed.
Lemma program_typing_preserved:
forall (
p:
LTL.program) (
tp:
LTLin.program),
LTLtyping.wt_program p ->
transf_program p =
OK tp ->
LTLintyping.wt_program tp.
Proof.