machblockgen.v recursion terminale

1 files changed, 47 insertions, 535 deletions

diff --git a/mppa_k1c/Machblockgen.v b/mppa_k1c/Machblockgen.v
index 1d5555df..a0786ac1 100644
--- a/mppa_k1c/Machblockgen.v
+++ b/mppa_k1c/Machblockgen.v
@@ -15,552 +15,64 @@ Require Import Mach.
 Require Import Linking.
 Require Import Machblock.
 
+Inductive Machblock_inst: Type :=
+| MB_label (lbl: label) 
+| MB_basic (bi: basic_inst)
+| MB_cfi   (cfi: control_flow_inst).
 
-Fixpoint to_bblock_header (c: Mach.code): list label * Mach.code :=
-  match c with
-  | (Mlabel l)::c' => 
-      let (h, c'') := to_bblock_header c' in
-      (l::h, c'')
-  | _ => (nil, c)
-  end.
-
-Definition to_basic_inst(i: Mach.instruction): option basic_inst :=
+Definition trans_inst (i:Mach.instruction) : Machblock_inst :=
   match i with
-  | Mgetstack ofs ty dst          => Some (MBgetstack ofs ty dst)
-  | Msetstack src ofs ty          => Some (MBsetstack src ofs ty)
-  | Mgetparam ofs ty dst          => Some (MBgetparam ofs ty dst)
-  | Mop       op args res         => Some (MBop       op args res)
-  | Mload     chunk addr args dst => Some (MBload     chunk addr args dst)
-  | Mstore    chunk addr args src => Some (MBstore    chunk addr args src)
-  | _ => None
-  end.
-
-Fixpoint to_bblock_body(c: Mach.code): bblock_body * Mach.code :=
-  match c with
-  | nil => (nil,nil)
-  | i::c' =>
-    match to_basic_inst i with
-    | Some bi =>
-       let (p,c'') := to_bblock_body c' in
-       (bi::p, c'')
-    | None => (nil, c)
-    end
+  | Mcall sig ros         => MB_cfi (MBcall sig ros)
+  | Mtailcall sig ros     => MB_cfi (MBtailcall sig ros)
+  | Mbuiltin ef args res  => MB_cfi (MBbuiltin ef args res)
+  | Mgoto lbl             => MB_cfi (MBgoto lbl)
+  | Mcond cond args lbl   => MB_cfi (MBcond cond args lbl)
+  | Mjumptable arg tbl    => MB_cfi (MBjumptable arg tbl)
+  | Mreturn               => MB_cfi (MBreturn)
+  | Mgetstack ofs ty dst          => MB_basic (MBgetstack ofs ty dst)
+  | Msetstack src ofs ty          => MB_basic (MBsetstack src ofs ty)
+  | Mgetparam ofs ty dst          => MB_basic (MBgetparam ofs ty dst)
+  | Mop       op args res         => MB_basic (MBop       op args res)
+  | Mload     chunk addr args dst => MB_basic (MBload     chunk addr args dst)
+  | Mstore    chunk addr args src => MB_basic (MBstore    chunk addr args src)
+  | Mlabel l => MB_label l
   end.
 
-
-Definition to_cfi (i: Mach.instruction): option control_flow_inst :=
+Definition add_to_new_bblock (i:Machblock_inst) : bblock :=
   match i with
-  | Mcall sig ros         => Some (MBcall sig ros)
-  | Mtailcall sig ros     => Some (MBtailcall sig ros)
-  | Mbuiltin ef args res  => Some (MBbuiltin ef args res)
-  | Mgoto lbl             => Some (MBgoto lbl)
-  | Mcond cond args lbl   => Some (MBcond cond args lbl)
-  | Mjumptable arg tbl    => Some (MBjumptable arg tbl)
-  | Mreturn               => Some (MBreturn)
-  | _ => None
+  | MB_label l => {| header := l::nil; body := nil; exit := None |}
+  | MB_basic i => {| header := nil; body := i::nil; exit := None |}
+  | MB_cfi i => {| header := nil; body := nil; exit := Some i |}
   end.
 
-Definition to_bblock_exit (c: Mach.code): option control_flow_inst * Mach.code :=
-  match c with
-  | nil => (None,nil)
-  | i::c' =>
-    match to_cfi i with
-    | Some bi as o => (o, c')
-    | None => (None, c)
-    end
+(* ajout d'une instruction en début d'une liste de blocks *)
+(* Soit /1\ ajout en tête de block, soit /2\ ajout dans un nouveau block*)
+(* bl est vide -> /2\ *)
+(* cfi -> /2\ (ajout dans exit)*)
+(* basic -> /1\ si header vide, /2\ si a un header *)
+(* label -> /1\ (dans header)*)
+Definition add_to_code (i:Machblock_inst) (bl:code) : code :=
+  match bl with
+  | h::bl0 => match i with
+              | MB_label l => {| header := l::(header h); body := (body h); exit := (exit h) |}::bl0
+              | MB_cfi i0 => add_to_new_bblock(i)::bl
+              | MB_basic i0 => match (header h) with
+                               |_::_ => (add_to_new_bblock i)::bl
+                               | nil => {| header := (header h); body := i0::(body h); exit := (exit h) |}::bl0
+                               end
+              end
+  | _ => (add_to_new_bblock i)::nil
   end.
-
-Inductive code_nature: Set := IsEmpty | IsLabel | IsBasicInst | IsCFI.
-
-Definition get_code_nature (c: Mach.code): code_nature :=
+  
+Fixpoint trans_code_rev (c: Mach.code) (bl:code) : code := 
   match c with
-  | nil => IsEmpty
-  | (Mlabel _)::_ => IsLabel
-  | i::_ => match to_basic_inst i with
-         | Some _ => IsBasicInst
-         | None => IsCFI
-         end
+  | nil => bl
+  | i::c0 =>
+    trans_code_rev c0 (add_to_code (trans_inst i) bl)
   end.
 
-Lemma cn_eqdec (cn1 cn2: code_nature): { cn1=cn2 } + {cn1 <> cn2}.
-Proof.
-  decide equality.
-Qed.
-
-Lemma get_code_nature_nil c: c<>nil -> get_code_nature c <> IsEmpty.
-Proof.
-  intros H. unfold get_code_nature.
-  destruct c; try (contradict H; auto; fail).
-  destruct i; discriminate.
-Qed.
-
-Lemma get_code_nature_empty c: get_code_nature c = IsEmpty -> c = nil.
-Proof.
-  intros H. destruct c; auto. exploit (get_code_nature_nil (i::c)); discriminate || auto.
-  intro F. contradict F.
-Qed.
-
-Lemma to_bblock_header_noLabel c:
-  get_code_nature c <> IsLabel ->
-  to_bblock_header c = (nil, c).
-Proof.
-  intros H. destruct c as [|i c]; auto.
-  destruct i; simpl; auto.
-  contradict H; simpl; auto.
-Qed.
-
-Lemma to_bblock_header_wfe c:
-  forall h c0,
-  to_bblock_header c = (h, c0) ->
-  (length c >= length c0)%nat.
-Proof.
-  induction c as [ |i c]; simpl; intros h c' H.
-  - inversion H; subst; clear H; simpl; auto.
-  - destruct i; try (inversion H; subst; simpl; auto; fail).
-    remember (to_bblock_header c) as bhc; destruct bhc as [h0 c0].
-    inversion H; subst.
-    lapply (IHc h0 c'); auto.
-Qed.
-
-Lemma to_bblock_header_wf c b c0:
-  get_code_nature c = IsLabel ->
-  to_bblock_header c = (b, c0) ->
-  (length c > length c0)%nat.
-Proof.
-  intros H1 H2; destruct c; [ contradict H1; simpl; discriminate | ].
-  destruct i; try discriminate.
-  simpl in H2.
-  remember (to_bblock_header c) as bh; destruct bh as [h c''].
-  inversion H2; subst.
-  exploit to_bblock_header_wfe; eauto.
-  simpl; omega.
-Qed.
-
-Lemma to_bblock_body_noBasic c:
-  get_code_nature c <> IsBasicInst ->
-  to_bblock_body c = (nil, c).
-Proof.
-  intros H. destruct c as [|i c]; simpl; auto.
-  destruct i; simpl; auto.
-  all: contradict H; simpl; auto.
-Qed.
-
-Lemma to_bblock_body_wfe c b c0:
-  to_bblock_body c = (b, c0) ->
-  (length c >= length c0)%nat.
-Proof.
-  generalize b c0; clear b c0.
-  induction c as [|i c].
-  - intros b c0 H. simpl in H. inversion H; subst; auto.
-  - intros b c0 H. simpl in H. destruct (to_basic_inst i).
-    + remember (to_bblock_body c) as tbbc; destruct tbbc as [p c''].
-      exploit (IHc p c''); auto. inversion H; subst; simpl; omega.
-    + inversion H; subst; auto.
-Qed.
-
-(** Attempt to eliminate cons_to_bblock_body *)
-(*
-Lemma to_bblock_body_basic c:
-  get_code_nature c = IsBasicInst ->
-  exists i bi b c',
-     to_basic_inst i = Some bi
-  /\ c = i :: c'
-  /\ to_bblock_body c = (bi::b, snd (to_bblock_body c')).
-Proof.
-  intros H.
-  destruct c as [|i c]; try (contradict H; simpl; discriminate).
-  destruct i eqn:I; try (contradict H; simpl; discriminate).
-  all: simpl; destruct (to_bblock_body c)  as [p c''] eqn:TBBC; repeat (eapply ex_intro); (repeat split);
-    simpl; eauto; rewrite TBBC; simpl; eauto.
-Qed.
-
-Lemma to_bblock_body_wf c b c0:
-  get_code_nature c = IsBasicInst ->
-  to_bblock_body c = (b, c0) ->
-  (length c > length c0)%nat.
-Proof.
-  intros H1 H2; exploit to_bblock_body_basic; eauto.
-  intros X. destruct X as (i & bi & b' & c' & X1 & X2 & X3).
-  exploit to_bblock_body_wfe. eauto. subst. simpl.
-  rewrite X3 in H2. inversion H2; clear H2; subst.
-  simpl; omega.
-Qed.
-*)
-
-Inductive cons_to_bblock_body c0: Mach.code -> bblock_body -> Prop :=
-  Cons_to_bbloc_body i bi c' b':
-    to_basic_inst i = Some bi
-    -> to_bblock_body c' = (b', c0)
-    -> cons_to_bblock_body c0 (i::c') (bi::b').
-
-Lemma to_bblock_body_IsBasicInst c b c0:
-  get_code_nature c = IsBasicInst ->
-  to_bblock_body c = (b, c0) ->
-  cons_to_bblock_body c0 c b.
-Proof.
-  intros H1 H2. destruct c; [ contradict H1; simpl; discriminate | ].
-  remember (to_basic_inst i) as tbii. destruct tbii.
-  - simpl in H2. rewrite <- Heqtbii in H2.
-    remember (to_bblock_body c) as tbbc. destruct tbbc as [p1 c1].
-    inversion H2. subst. eapply Cons_to_bbloc_body; eauto.
-  - destruct i; try discriminate.
-Qed.
-
-Lemma to_bblock_body_wf c b c0:
-  get_code_nature c = IsBasicInst ->
-  to_bblock_body c = (b, c0) ->
-  (length c > length c0)%nat.
-Proof.
-  intros H1 H2; exploit to_bblock_body_IsBasicInst; eauto.
-  intros X. destruct X.
-  exploit to_bblock_body_wfe; eauto. subst. simpl.
-  simpl; omega.
-Qed.
-
-Lemma to_bblock_exit_noCFI c:
-  get_code_nature c <> IsCFI ->
-  to_bblock_exit c = (None, c).
-Proof.
-  intros H. destruct c as [|i c]; simpl; auto.
-  destruct i; simpl; auto.
-  all: contradict H; simpl; auto.
-Qed.
-
-Lemma to_bblock_exit_wf c b c0:
-  get_code_nature c = IsCFI ->
-  to_bblock_exit c = (b, c0) ->
-  (length c > length c0)%nat.
-Proof.
-  intros H1 H2. destruct c as [|i c]; try discriminate.
-  destruct i; try discriminate;
-  unfold to_bblock_header in H2; inversion H2; auto.
-Qed.
-
-Lemma to_bblock_exit_wfe c b c0:
-  to_bblock_exit c = (b, c0) ->
-  (length c >= length c0)%nat.
-Proof.
-  intros H. destruct c as [|i c].
-  - simpl in H. inversion H; subst; clear H; auto.
-  - destruct i; try ( simpl in H; inversion H; subst; clear H; auto ).
-    all: simpl; auto.
-Qed.
-
-Definition to_bblock(c: Mach.code): bblock * Mach.code :=
-  let (h,c0) := to_bblock_header c in
-  let (bdy, c1) := to_bblock_body c0 in
-  let (ext, c2) := to_bblock_exit c1 in
-  ({| header := h; body := bdy; exit := ext |}, c2)
-  .
-
-Lemma to_bblock_acc_label c l b c':
-  to_bblock c = (b, c') ->
-  to_bblock (Mlabel l :: c) = ({| header := l::(header b); body := (body b); exit := (exit b) |}, c').
-Proof.
-  unfold to_bblock; simpl.
-  remember (to_bblock_header c) as bhc; destruct bhc as [h c0].
-  remember (to_bblock_body c0) as bbc; destruct bbc as [bdy c1].
-  remember (to_bblock_exit c1) as bbc; destruct bbc as [ext c2].
-  intros H; inversion H; subst; clear H; simpl; auto.
-Qed.
-
-Lemma to_bblock_basic_then_label i c bi:
-  get_code_nature (i::c) = IsBasicInst ->
-  get_code_nature c = IsLabel ->
-  to_basic_inst i = Some bi ->
-  fst (to_bblock (i::c)) = {| header := nil; body := bi::nil; exit := None |}.
-Proof.
-  intros H1 H2 H3.
-  destruct c as [|i' c]; try (contradict H1; simpl; discriminate).
-  destruct i'; try (contradict H1; simpl; discriminate).
-  destruct i; simpl in *; inversion H3; subst; auto.
-Qed.
-
-Lemma to_bblock_CFI i c cfi:
-  get_code_nature (i::c) = IsCFI ->
-  to_cfi i = Some cfi ->
-  fst (to_bblock (i::c)) = {| header := nil; body := nil; exit := Some cfi |}.
-Proof.
-  intros H1 H2.
-  destruct i; try discriminate.
-  all: subst; rewrite <- H2; simpl; auto.
-Qed.
-
-Lemma to_bblock_noLabel c:
-  get_code_nature c <> IsLabel ->
-  fst (to_bblock c) = {|
-    header := nil;
-    body := body (fst (to_bblock c));
-    exit := exit (fst (to_bblock c))
-  |}.
-Proof.
-  intros H.
-  destruct c as [|i c]; simpl; auto.
-  apply bblock_eq; simpl;
-  destruct i; (
-      try (
-        remember (to_bblock _) as bb;
-        unfold to_bblock in *;
-        remember (to_bblock_header _) as tbh;
-        destruct tbh;
-        destruct (to_bblock_body _);
-        destruct (to_bblock_exit _);
-        subst; simpl; inversion Heqtbh; auto; fail
-      )
-    || contradict H; simpl; auto ).
-Qed.
-
-Lemma to_bblock_body_nil c c':
-  to_bblock_body c = (nil, c') ->
-  c = c'.
-Proof.
-  intros H.
-  destruct c as [|i c]; [ simpl in *; inversion H; auto |].
-  destruct i; try ( simpl in *; remember (to_bblock_body c) as tbc; destruct tbc as [p c'']; inversion H ).
-  all: auto.
-Qed.
-
-Lemma to_bblock_exit_nil c c':
-  to_bblock_exit c = (None, c') ->
-  c = c'.
-Proof.
-  intros H.
-  destruct c as [|i c]; [ simpl in *; inversion H; auto |].
-  destruct i; try ( simpl in *; remember (to_bblock_exit c) as tbe; destruct tbe as [p c'']; inversion H ).
-  all: auto.
-Qed.
-
-Lemma to_bblock_label b l c c':
-  to_bblock (Mlabel l :: c) = (b, c') ->
-  (header b) = l::(tail (header b)) /\ to_bblock c = ({| header:=tail (header b); body := body b; exit := exit b |}, c').
-Proof.
-  unfold to_bblock; simpl.
-  remember (to_bblock_header c) as bhc; destruct bhc as [h c0].
-  remember (to_bblock_body c0) as bbc; destruct bbc as [bdy c1].
-  remember (to_bblock_exit c1) as bbc; destruct bbc as [ext c2].
-  intros H; inversion H; subst; clear H; simpl; auto.
-Qed.
-
-Lemma to_bblock_basic c i bi:
-  get_code_nature (i::c) = IsBasicInst ->
-  to_basic_inst i = Some bi ->
-  get_code_nature c <> IsLabel ->
-  fst (to_bblock (i::c)) = {|
-    header := nil;
-    body := bi :: body (fst (to_bblock c));
-    exit := exit (fst (to_bblock c))
-  |}.
-Proof.
-  intros.
-  destruct c; try (destruct i; inversion H0; subst; simpl; auto; fail).
-  apply bblock_eq; simpl.
-(* header *)
-  + destruct i; simpl; auto; (
-      exploit to_bblock_noLabel; [rewrite H; discriminate | intro; rewrite H2; simpl; auto]).
-(* body *)
-(* FIXME - the proof takes some time to prove.. N² complexity :( *)
-  + unfold to_bblock.
-    remember (to_bblock_header _) as tbh; destruct tbh.
-    remember (to_bblock_body _) as tbb; destruct tbb.
-    remember (to_bblock_exit _) as tbe; destruct tbe.
-    simpl.
-    destruct i; destruct i0.
-    all: try (simpl in H1; contradiction).
-    all: try discriminate.
-    all: try (
-    simpl in Heqtbh; inversion Heqtbh; clear Heqtbh; subst;
-    simpl in Heqtbb; remember (to_bblock_body c) as tbbc; destruct tbbc;
-    inversion Heqtbb; clear Heqtbb; subst; simpl in *; clear H H1;
-    inversion H0; clear H0; subst; destruct (to_bblock_body c);
-    inversion Heqtbbc; clear Heqtbbc; subst;
-    destruct (to_bblock_exit c1); simpl; auto; fail).
-(* exit *)
-  + unfold to_bblock.
-    remember (to_bblock_header _) as tbh; destruct tbh.
-    remember (to_bblock_body _) as tbb; destruct tbb.
-    remember (to_bblock_exit _) as tbe; destruct tbe.
-    simpl.
-    destruct i; destruct i0.
-    all: try (simpl in H1; contradiction).
-    all: try discriminate.
-    all: try (
-    simpl in Heqtbh; inversion Heqtbh; clear Heqtbh; subst;
-    simpl in Heqtbb; remember (to_bblock_body c) as tbbc; destruct tbbc; 
-    inversion Heqtbb; clear Heqtbb; subst; simpl in *; clear H H1;
-    inversion H0; clear H0; subst; destruct (to_bblock_body c) eqn:TBBC;
-    inversion Heqtbbc; clear Heqtbbc; subst;
-    destruct (to_bblock_exit c1) eqn:TBBE; simpl;
-    inversion Heqtbe; clear Heqtbe; subst; auto; fail).
-Qed.
-
-Lemma to_bblock_size_single_label c i:
-  get_code_nature (i::c) = IsLabel ->
-  size (fst (to_bblock (i::c))) = Datatypes.S (size (fst (to_bblock c))).
-Proof.
-  intros H.
-  destruct i; try discriminate.
-  remember (to_bblock c) as bl. destruct bl as [b c'].
-  erewrite to_bblock_acc_label; eauto.
-  unfold size; simpl.
-  auto.
-Qed.
-
-Lemma to_bblock_size_label_neqz c:
-  get_code_nature c = IsLabel ->
-  size (fst (to_bblock c)) <> 0%nat.
-Proof.
-  destruct c as [ |i c]; try discriminate.
-  intros; rewrite to_bblock_size_single_label; auto.
-Qed.
-
-Lemma to_bblock_size_basic_neqz c:
-  get_code_nature c = IsBasicInst ->
-  size (fst (to_bblock c)) <> 0%nat.
-Proof.
-  intros H. destruct c as [|i c]; try (contradict H; auto; simpl; discriminate).
-  destruct i; try (contradict H; simpl; discriminate);
-  (
-    destruct (get_code_nature c) eqn:gcnc;
-    (* Case gcnc is not IsLabel *)
-    try (erewrite to_bblock_basic; eauto; [
-        unfold size; simpl; auto
-      | simpl; auto
-      | rewrite gcnc; discriminate
-    ]);
-    erewrite to_bblock_basic_then_label; eauto; [
-        unfold size; simpl; auto
-      | simpl; auto
-    ]
-  ).
-Qed.
-
-Lemma to_bblock_size_cfi_neqz c:
-  get_code_nature c = IsCFI ->
-  size (fst (to_bblock c)) <> 0%nat.
-Proof.
-  intros H. destruct c as [|i c]; try (contradict H; auto; simpl; discriminate).
-  destruct i; discriminate.
-Qed.
-
-Lemma to_bblock_size_single_basic c i:
-  get_code_nature (i::c) = IsBasicInst ->
-  get_code_nature c <> IsLabel ->
-  size (fst (to_bblock (i::c))) = Datatypes.S (size (fst (to_bblock c))).
-Proof.
-  intros.
-  destruct i; try (contradict H; simpl; discriminate); try (
-    (exploit to_bblock_basic; eauto);
-      [remember (to_basic_inst _) as tbi; destruct tbi; eauto |];
-    intro; rewrite H1; unfold size; simpl;
-    assert ((length (header (fst (to_bblock c)))) = 0%nat);
-      exploit to_bblock_noLabel; eauto; intro; rewrite H2; simpl; auto;
-    rewrite H2; auto
-  ).
-Qed.
-
-Lemma to_bblock_wf c b c0:
-  c <> nil ->
-  to_bblock c = (b, c0) ->
-  (length c > length c0)%nat.
-Proof.
-  intro H; lapply (get_code_nature_nil c); eauto.
-  intro H'; remember (get_code_nature c) as gcn.
-  unfold to_bblock.
-  remember (to_bblock_header c) as p1; eauto.
-  destruct p1 as [h c1].
-  intro H0.
-  destruct gcn.
-  - contradict H'; auto.
-  - exploit to_bblock_header_wf; eauto.
-    remember (to_bblock_body c1) as p2; eauto.
-    destruct p2 as [h2 c2].
-    exploit to_bblock_body_wfe; eauto.
-    remember (to_bblock_exit c2) as p3; eauto.
-    destruct p3 as [h3 c3].
-    exploit to_bblock_exit_wfe; eauto.
-    inversion H0. omega.
-  - exploit to_bblock_header_noLabel; eauto. rewrite <- Heqgcn. discriminate.
-    intro. rewrite H1 in Heqp1. inversion Heqp1. clear Heqp1. subst.
-    remember (to_bblock_body c) as p2; eauto.
-    destruct p2 as [h2 c2].
-    exploit to_bblock_body_wf; eauto.
-    remember (to_bblock_exit c2) as p3; eauto.
-    destruct p3 as [h3 c3].
-    exploit to_bblock_exit_wfe; eauto.
-    inversion H0. omega.
-  - exploit to_bblock_header_noLabel; eauto. rewrite <- Heqgcn. discriminate.
-    intro. rewrite H1 in Heqp1. inversion Heqp1; clear Heqp1; subst.
-    remember (to_bblock_body c) as p2; eauto.
-    destruct p2 as [h2 c2].
-    exploit (to_bblock_body_noBasic c); eauto. rewrite <- Heqgcn. discriminate.
-    intros H2; rewrite H2 in Heqp2; inversion Heqp2; clear Heqp2; subst.
-    remember (to_bblock_exit c) as p3; eauto.
-    destruct p3 as [h3 c3].
-    exploit (to_bblock_exit_wf c h3 c3); eauto.
-    inversion H0. omega.
-Qed.
-
-Lemma to_bblock_nonil i c0:
-  size (fst (to_bblock (i :: c0))) <> 0%nat.
-Proof.
-  intros H. remember (i::c0) as c. remember (get_code_nature c) as gcnc. destruct gcnc.
-  - contradict Heqgcnc. subst. simpl. destruct i; discriminate.
-  - eapply to_bblock_size_label_neqz; eauto.
-  - eapply to_bblock_size_basic_neqz; eauto.
-  - eapply to_bblock_size_cfi_neqz; eauto.
-Qed.
-
-Function trans_code (c: Mach.code) { measure length c }: code :=
-  match c with
-  | nil => nil
-  | _ =>
-     let (b, c0) := to_bblock c in
-     b::(trans_code c0)
-  end.
-Proof.
-  intros; eapply to_bblock_wf; eauto. discriminate.
-Qed.
-
-Lemma trans_code_nonil c:
-  c <> nil -> trans_code c <> nil.
-Proof.
-  intros H.
-  induction c, (trans_code c) using trans_code_ind; simpl; auto. discriminate.
-Qed.
-
-Lemma trans_code_step c b lb0 hb c1 bb c2 eb c3:
-  trans_code c = b :: lb0 ->
-  to_bblock_header c = (hb, c1) ->
-  to_bblock_body c1 = (bb, c2) ->
-  to_bblock_exit c2 = (eb, c3) ->
-  hb = header b /\ bb = body b /\ eb = exit b /\ trans_code c3 = lb0.
-Proof.
-  intros.
-  induction c, (trans_code c) using trans_code_ind. discriminate. clear IHc0.
-  subst. destruct _x as [|i c]; try (contradict y; auto; fail).
-  inversion H; subst. clear H. unfold to_bblock in e0.
-  remember (to_bblock_header (i::c)) as hd. destruct hd as [hb' c1'].
-  remember (to_bblock_body c1') as bd. destruct bd as [bb' c2'].
-  remember (to_bblock_exit c2') as be. destruct be as [eb' c3'].
-  inversion e0. simpl.
-  inversion H0. subst.
-  rewrite <- Heqbd in H1. inversion H1. subst.
-  rewrite <- Heqbe in H2. inversion H2. subst.
-  auto.
-Qed.
-
-Lemma trans_code_cfi i c cfi:
-  to_cfi i = Some cfi ->
-  trans_code (i :: c) = {| header := nil ; body := nil ; exit := Some cfi |} :: trans_code c.
-Proof.
-  intros. rewrite trans_code_equation. remember (to_bblock _) as tb; destruct tb as [b c0].
-  destruct i; try (contradict H; discriminate).
-  all: unfold to_bblock in Heqtb; remember (to_bblock_header _) as tbh; destruct tbh as [h c0'];
-      remember (to_bblock_body c0') as tbb; destruct tbb as [bdy c1'];
-      remember (to_bblock_exit c1') as tbe; destruct tbe as [ext c2]; simpl in *;
-      inversion Heqtbh; subst; inversion Heqtbb; subst; inversion Heqtbe; subst;
-      inversion Heqtb; subst; rewrite H; auto.
-Qed.
+Function trans_code (c: Mach.code) : code :=
+  trans_code_rev (List.rev_append c nil) nil.
 
 (* à finir pour passer des Mach.function au function, etc. *)
 Definition transf_function (f: Mach.function) : function :=