From 73729d23ac13275c0d28d23bc1b1f6056104e5d9 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 4 Sep 2006 15:08:29 +0000
Subject: Fusion de la branche "traces": - Ajout de traces d'evenements d'E/S
 dans les semantiques - Ajout constructions switch et allocation dynamique -
 Initialisation des variables globales - Portage Coq 8.1 beta Debut
 d'integration du front-end C: - Traduction Clight -> Csharpminor dans
 cfrontend/ - Modifications de Csharpminor et Globalenvs en consequence.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@72 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 backend/Main.v | 58 +++++++++++++++++++++++++++++-----------------------------
 1 file changed, 29 insertions(+), 29 deletions(-)

(limited to 'backend/Main.v')

diff --git a/backend/Main.v b/backend/Main.v
index 80a0577f..95dc4e6c 100644
--- a/backend/Main.v
+++ b/backend/Main.v
@@ -78,34 +78,34 @@ Notation "a @@ b" :=
   
   The translation of a Cminor function to a PPC function is as follows. *)
 
-Definition transf_cminor_function (f: Cminor.function) : option PPC.code :=
+Definition transf_cminor_fundef (f: Cminor.fundef) : option PPC.fundef :=
   Some f
-  @@@ RTLgen.transl_function
-   @@ Constprop.transf_function
-   @@ CSE.transf_function
-  @@@ Allocation.transf_function
-   @@ Tunneling.tunnel_function
-   @@ Linearize.transf_function
-  @@@ Stacking.transf_function
-  @@@ PPCgen.transf_function.
+  @@@ RTLgen.transl_fundef
+   @@ Constprop.transf_fundef
+   @@ CSE.transf_fundef
+  @@@ Allocation.transf_fundef
+   @@ Tunneling.tunnel_fundef
+   @@ Linearize.transf_fundef
+  @@@ Stacking.transf_fundef
+  @@@ PPCgen.transf_fundef.
 
 (** And here is the translation for Csharpminor functions. *)
 
-Definition transf_csharpminor_function 
-     (gce: Cminorgen.compilenv) (f: Csharpminor.function) : option PPC.code :=
+Definition transf_csharpminor_fundef
+     (gce: Cminorgen.compilenv) (f: Csharpminor.fundef) : option PPC.fundef :=
   Some f 
-  @@@ Cminorgen.transl_function gce
-  @@@ transf_cminor_function.
+  @@@ Cminorgen.transl_fundef gce
+  @@@ transf_cminor_fundef.
 
 (** The corresponding translations for whole program follow. *)
 
 Definition transf_cminor_program (p: Cminor.program) : option PPC.program :=
-  transform_partial_program transf_cminor_function p.
+  transform_partial_program transf_cminor_fundef p.
 
 Definition transf_csharpminor_program (p: Csharpminor.program) : option PPC.program :=
   let gce := Cminorgen.build_global_compilenv p in
   transform_partial_program 
-    (transf_csharpminor_function gce)
+    (transf_csharpminor_fundef gce)
     (Csharpminor.program_of_program p).
 
 (** * Equivalence with whole program transformations *)
@@ -194,7 +194,7 @@ Qed.
 Lemma transf_cminor_program_equiv:
   forall p, transf_cminor_program2 p = transf_cminor_program p.
 Proof.
-  intro. unfold transf_cminor_program, transf_cminor_program2, transf_cminor_function.
+  intro. unfold transf_cminor_program, transf_cminor_program2, transf_cminor_fundef.
   simpl. 
   unfold RTLgen.transl_program,
          Constprop.transf_program, RTL.program.
@@ -223,7 +223,7 @@ Lemma transf_csharpminor_program_equiv:
   forall p, transf_csharpminor_program2 p = transf_csharpminor_program p.
 Proof.
   intros. 
-  unfold transf_csharpminor_program2, transf_csharpminor_program, transf_csharpminor_function.
+  unfold transf_csharpminor_program2, transf_csharpminor_program, transf_csharpminor_fundef.
   simpl. 
   replace transf_cminor_program2 with transf_cminor_program.
   unfold transf_cminor_program, Cminorgen.transl_program, Cminor.program, PPC.program.
@@ -237,10 +237,10 @@ Qed.
   composes the semantic preservation results for each pass. *)
 
 Lemma transf_cminor_program2_correct:
-  forall p tp n,
+  forall p tp t n,
   transf_cminor_program2 p = Some tp ->
-  Cminor.exec_program p (Vint n) ->
-  PPC.exec_program tp (Vint n).
+  Cminor.exec_program p t (Vint n) ->
+  PPC.exec_program tp t (Vint n).
 Proof.
   intros until n.
   unfold transf_cminor_program2.
@@ -274,10 +274,10 @@ Proof.
 Qed.
 
 Lemma transf_csharpminor_program2_correct:
-  forall p tp n,
+  forall p tp t n,
   transf_csharpminor_program2 p = Some tp ->
-  Csharpminor.exec_program p (Vint n) ->
-  PPC.exec_program tp (Vint n).
+  Csharpminor.exec_program p t (Vint n) ->
+  PPC.exec_program tp t (Vint n).
 Proof.
   intros until n; unfold transf_csharpminor_program2; simpl.
   caseEq (Cminorgen.transl_program p).
@@ -291,20 +291,20 @@ Qed.
 (** It follows that the whole compiler is semantic-preserving. *)
 
 Theorem transf_cminor_program_correct:
-  forall p tp n,
+  forall p tp t n,
   transf_cminor_program p = Some tp ->
-  Cminor.exec_program p (Vint n) ->
-  PPC.exec_program tp (Vint n).
+  Cminor.exec_program p t (Vint n) ->
+  PPC.exec_program tp t (Vint n).
 Proof.
   intros. apply transf_cminor_program2_correct with p. 
   rewrite transf_cminor_program_equiv. assumption. assumption.
 Qed.
 
 Theorem transf_csharpminor_program_correct:
-  forall p tp n,
+  forall p tp t n,
   transf_csharpminor_program p = Some tp ->
-  Csharpminor.exec_program p (Vint n) ->
-  PPC.exec_program tp (Vint n).
+  Csharpminor.exec_program p t (Vint n) ->
+  PPC.exec_program tp t (Vint n).
 Proof.
   intros. apply transf_csharpminor_program2_correct with p. 
   rewrite transf_csharpminor_program_equiv. assumption. assumption.
-- 
cgit