From 76555ffd2403b3ebf1ea353063c16763e6493722 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 6 May 2013 11:32:22 +0000
Subject: Refactoring: move definition of chunk_of_type to AST.v.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2238 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 arm/Asm.v           |  3 ---
 backend/LTL.v       | 10 ----------
 backend/Locations.v |  2 +-
 backend/Mach.v      |  3 ---
 common/AST.v        | 10 ++++++++++
 ia32/Asm.v          |  3 ---
 powerpc/Asm.v       |  3 ---
 7 files changed, 11 insertions(+), 23 deletions(-)

diff --git a/arm/Asm.v b/arm/Asm.v
index 60dae47..6d5edf7 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -608,9 +608,6 @@ Definition preg_of (r: mreg) : preg :=
     We exploit the calling conventions from module [Conventions], except that
     we use ARM registers instead of locations. *)
 
-Definition chunk_of_type (ty: typ) :=
-  match ty with Tint => Mint32 | Tfloat => Mfloat64al32 | Tlong => Mint64 end.
-
 Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop :=
   | extcall_arg_reg: forall r,
       extcall_arg rs m (R r) (rs (preg_of r))
diff --git a/backend/LTL.v b/backend/LTL.v
index de10845..27fee8a 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -197,16 +197,6 @@ Definition parent_locset (stack: list stackframe) : locset :=
   | Stackframe f sp ls bb :: stack' => ls
   end.
 
-(* REVISE
-(** [getslot sl ofs ty rs] looks up the value of location [S sl ofs ty] in [rs],
-  and normalizes it to the type [ty] of this location. *)
-
-Definition getslot (sl: slot) (ofs: Z) (ty: typ) (rs: locset) : val :=
-  Val.load_result
-    (match ty with Tint => Mint32 | Tfloat => Mfloat64 | Tlong => Mint64 end)
-    (rs (S sl ofs ty)).
-*)
-
 Inductive step: state -> trace -> state -> Prop :=
   | exec_start_block: forall s f sp pc rs m bb,
       (fn_code f)!pc = Some bb ->
diff --git a/backend/Locations.v b/backend/Locations.v
index 2f2dae8..f7fb607 100644
--- a/backend/Locations.v
+++ b/backend/Locations.v
@@ -273,7 +273,7 @@ End Loc.
 
 (** The [Locmap] module defines mappings from locations to values,
   used as evaluation environments for the semantics of the [LTL] 
-  and [LTLin] intermediate languages.  *)
+  and [Linear] intermediate languages.  *)
 
 Set Implicit Arguments.
 
diff --git a/backend/Mach.v b/backend/Mach.v
index 5030de1..ec48195 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -123,9 +123,6 @@ value of the return address that the Asm code generated later will
 store in the reserved location.
 *)
 
-Definition chunk_of_type (ty: typ) :=
-  match ty with Tint => Mint32 | Tfloat => Mfloat64al32 | Tlong => Mint64 end.
-
 Definition load_stack (m: mem) (sp: val) (ty: typ) (ofs: int) :=
   Mem.loadv (chunk_of_type ty) m (Val.add sp (Vint ofs)).
 
diff --git a/common/AST.v b/common/AST.v
index fb80b46..fba5354 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -115,6 +115,16 @@ Definition type_of_chunk (c: memory_chunk) : typ :=
   | Mfloat64al32 => Tfloat
   end.
 
+(** The chunk that is appropriate to store and reload a value of
+  the given type, without losing information. *)
+
+Definition chunk_of_type (ty: typ) :=
+  match ty with
+  | Tint => Mint32
+  | Tfloat => Mfloat64al32
+  | Tlong => Mint64
+  end.
+
 (** Initialization data for global variables. *)
 
 Inductive init_data: Type :=
diff --git a/ia32/Asm.v b/ia32/Asm.v
index 2757061..09dead3 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -720,9 +720,6 @@ Definition preg_of (r: mreg) : preg :=
     We exploit the calling conventions from module [Conventions], except that
     we use machine registers instead of locations. *)
 
-Definition chunk_of_type (ty: typ) :=
-  match ty with Tint => Mint32 | Tfloat => Mfloat64al32 | Tlong => Mint64 end.
-
 Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop :=
   | extcall_arg_reg: forall r,
       extcall_arg rs m (R r) (rs (preg_of r))
diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 115d846..55a23f2 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -806,9 +806,6 @@ Definition preg_of (r: mreg) : preg :=
     We exploit the calling conventions from module [Conventions], except that
     we use PPC registers instead of locations. *)
 
-Definition chunk_of_type (ty: typ) :=
-  match ty with Tint => Mint32 | Tfloat => Mfloat64al32 | Tlong => Mint64 end.
-
 Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop :=
   | extcall_arg_reg: forall r,
       extcall_arg rs m (R r) (rs (preg_of r))
-- 
cgit v1.2.3