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, 51 insertions, 13 deletions

diff --git a/lib/Iteration.v b/lib/Iteration.v
index 3c4b5998..85c5ded8 100644
--- a/lib/Iteration.v
+++ b/lib/Iteration.v
@@ -1,6 +1,5 @@
 (* Bounded and unbounded iterators *)
 
-Require Recdef.
 Require Import Coqlib.
 Require Import Classical.
 Require Import Max.
@@ -72,15 +71,51 @@ Fixpoint iterate (a: A) : B :=
 
 Definition num_iterations := 1000000000000%positive.
 
-Function iter (niter: positive) (s: A) {wf Plt niter} : option B :=
-  if peq niter xH then None else
-    match step s with
-    | inl res => Some res
-    | inr s'  => iter (Ppred niter) s'
-    end.
+(** The simple definition of bounded iteration is:
+<<
+Fixpoint iterate (niter: nat) (a: A) {struct niter} : option B :=
+  match niter with
+  | O => None
+  | S niter' =>
+      match step a with
+      | inl b => b
+      | inr a' => iterate niter' a'
+      end
+  end.
+>>
+  This function is structural recursive over the parameter [niter]
+  (number of iterations), represented here as a Peano integer (type [nat]).
+  However, we want to use very large values of [niter].  As Peano integers,
+  these values would be much too large to fit in memory.  Therefore,
+  we must express iteration counts as a binary integer (type [positive]).
+  However, Peano induction over type [positive] is not structural recursion,
+  so we cannot define [iterate] as a Coq fixpoint and must use
+  Noetherian recursion instead. *)
+
+Definition iter_step (x: positive)
+                     (next: forall y, Plt y x -> A -> option B)
+                     (s: A) : option B :=
+  match peq x xH with
+  | left EQ => None
+  | right NOTEQ =>
+      match step s with
+      | inl res => Some res
+      | inr s'  => next (Ppred x) (Ppred_Plt x NOTEQ) s'
+      end
+  end.
+
+Definition iter: positive -> A -> option B :=
+  Fix Plt_wf (fun _ => A -> option B) iter_step.
+
+(** We then prove the expected unrolling equations for [iter]. *)
+
+Remark unroll_iter:
+  forall x, iter x = iter_step x (fun y _ => iter y).
 Proof.
-  intros. apply Ppred_Plt. auto.
-  apply Plt_wf.
+  unfold iter; apply (Fix_eq Plt_wf (fun _ => A -> option B) iter_step).
+  intros. unfold iter_step. apply extensionality. intro s. 
+  case (peq x xH); intro. auto. 
+  rewrite H. auto. 
 Qed.
 
 (** The [iterate] function is defined as [iter] up to
@@ -100,10 +135,13 @@ Hypothesis step_prop:
 Lemma iter_prop:
   forall n a b, P a -> iter n a = Some b -> Q b.
 Proof.
-  intros n a. functional induction (iter n a); intros.
-  discriminate.
-  inversion H0; subst b. generalize (step_prop s H). rewrite e0. auto.
-  apply IHo. generalize (step_prop s H). rewrite e0. auto. auto.
+  apply (well_founded_ind Plt_wf 
+         (fun p => forall a b, P a -> iter p a = Some b -> Q b)).
+  intros until b. intro. rewrite unroll_iter.
+  unfold iter_step. case (peq x 1); intro. congruence.
+  generalize (step_prop a H0).
+  case (step a); intros. congruence. 
+  apply H with (Ppred x) a0. apply Ppred_Plt; auto. auto. auto.
 Qed.
 
 Lemma iterate_prop: