Fusion des modifications faites sur les branches "tailcalls" et "smallstep".

En particulier:
- Semantiques small-step depuis RTL jusqu'a PPC
- Cminor independant du processeur
- Ajout passes Selection et Reload
- Ajout des langages intermediaires CminorSel et LTLin correspondants
- Ajout des tailcalls depuis Cminor jusqu'a PPC


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 40 insertions, 0 deletions

diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 184fe28f..7bee366b 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -23,6 +23,8 @@ Axiom proof_irrelevance:
 
 (** * Useful tactics *)
 
+Ltac inv H := inversion H; clear H; subst.
+
 Ltac predSpec pred predspec x y :=
   generalize (predspec x y); case (pred x y); intro.
 
@@ -753,6 +755,44 @@ Proof.
   generalize list_norepet_app; firstorder.
 Qed.
 
+(** [is_tail l1 l2] holds iff [l2] is of the form [l ++ l1] for some [l]. *)
+
+Inductive is_tail (A: Set): list A -> list A -> Prop :=
+  | is_tail_refl:
+      forall c, is_tail c c
+  | is_tail_cons:
+      forall i c1 c2, is_tail c1 c2 -> is_tail c1 (i :: c2).
+
+Lemma is_tail_in:
+  forall (A: Set) (i: A) c1 c2, is_tail (i :: c1) c2 -> In i c2.
+Proof.
+  induction c2; simpl; intros.
+  inversion H.
+  inversion H. tauto. right; auto.
+Qed.
+
+Lemma is_tail_cons_left:
+  forall (A: Set) (i: A) c1 c2, is_tail (i :: c1) c2 -> is_tail c1 c2.
+Proof.
+  induction c2; intros; inversion H.
+  constructor. constructor. constructor. auto. 
+Qed.
+
+Hint Resolve is_tail_refl is_tail_cons is_tail_in is_tail_cons_left: coqlib.
+
+Lemma is_tail_incl:
+  forall (A: Set) (l1 l2: list A), is_tail l1 l2 -> incl l1 l2.
+Proof.
+  induction 1; eauto with coqlib.
+Qed.
+
+Lemma is_tail_trans:
+  forall (A: Set) (l1 l2: list A),
+  is_tail l1 l2 -> forall (l3: list A), is_tail l2 l3 -> is_tail l1 l3.
+Proof.
+  induction 1; intros. auto. apply IHis_tail. eapply is_tail_cons_left; eauto.
+Qed.
+
 (** [list_forall2 P [x1 ... xN] [y1 ... yM] holds iff [N = M] and
   [P xi yi] holds for all [i]. *)