From c48b9097201dc9a1e326acdbce491fe16cab01e6 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Tue, 28 Aug 2007 12:57:58 +0000
Subject: Fusion de la branche restr-cminor.  En Clight, C#minor et Cminor, les
 expressions sont maintenant pures et les appels de fonctions sont des
 statements.  Ajout de semantiques coinductives pour la divergence en Clight,
 C#minor, Cminor.  Preuve de preservation semantique pour les programmes qui
 divergent.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@409 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 common/Smallstep.v | 31 ++++++++++++++++++-------------
 1 file changed, 18 insertions(+), 13 deletions(-)

(limited to 'common/Smallstep.v')

diff --git a/common/Smallstep.v b/common/Smallstep.v
index f60746d3..8039ba43 100644
--- a/common/Smallstep.v
+++ b/common/Smallstep.v
@@ -172,12 +172,17 @@ Qed.
     for coinductive reasoning. *)
 
 CoInductive forever_N (ge: genv): nat -> state -> traceinf -> Prop :=
-  | forever_N_star: forall s1 t s2 p q T,
-      star ge s1 t s2 -> (p < q)%nat -> forever_N ge p s2 T ->
-      forever_N ge q s1 (t *** T)
-  | forever_N_plus: forall s1 t s2 p q T,
-      plus ge s1 t s2 -> forever_N ge p s2 T ->
-      forever_N ge q s1 (t *** T).
+  | forever_N_star: forall s1 t s2 p q T1 T2,
+      star ge s1 t s2 -> 
+      (p < q)%nat ->
+      forever_N ge p s2 T2 ->
+      T1 = t *** T2 ->
+      forever_N ge q s1 T1
+  | forever_N_plus: forall s1 t s2 p q T1 T2,
+      plus ge s1 t s2 ->
+      forever_N ge p s2 T2 ->
+      T1 = t *** T2 ->
+      forever_N ge q s1 T1.
 
 Remark Peano_induction:
   forall (P: nat -> Prop),
@@ -202,14 +207,14 @@ Proof.
   (* star case *)
   inv H1.
   (* no transition *)
-  change (E0 *** T0) with T0. apply H with p1. auto. auto. 
+  change (E0 *** T2) with T2. apply H with p1. auto. auto. 
   (* at least one transition *)
-  exists t1; exists s0; exists p0; exists (t2 *** T0).
+  exists t1; exists s0; exists p0; exists (t2 *** T2).
   split. auto. split. eapply forever_N_star; eauto.
   apply Eappinf_assoc.
   (* plus case *)
   inv H1.
-  exists t1; exists s0; exists (S p1); exists (t2 *** T0).
+  exists t1; exists s0; exists (S p1); exists (t2 *** T2).
   split. auto. split. eapply forever_N_star; eauto. 
   apply Eappinf_assoc.
 Qed.
@@ -348,12 +353,12 @@ Proof.
     forever_N step2 ge2 (measure st1) st2 T).
   cofix COINDHYP; intros.
   inversion H; subst. elim (simulation H1 H0).
-  intros [st2' [A B]]. apply forever_N_plus with st2' (measure s2).
-  auto. apply COINDHYP. assumption. assumption.
+  intros [st2' [A B]]. apply forever_N_plus with t st2' (measure s2) T0.
+  auto. apply COINDHYP. assumption. assumption. auto.
   intros [A [B C]].
-  apply forever_N_star with st2 (measure s2).
+  apply forever_N_star with t st2 (measure s2) T0.
   rewrite B. apply star_refl. auto.
-  apply COINDHYP. assumption. auto.
+  apply COINDHYP. assumption. auto. auto.
   intros. eapply forever_N_forever; eauto.
 Qed.
 
-- 
cgit