From 7717d9e5f781a0b0d79f72c5439cf822f4ea78d0 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 1 May 2013 09:22:49 +0000
Subject: Coq-defined equality functions for Allocation.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2225 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 common/AST.v | 23 ++++++++++++++++++++---
 1 file changed, 20 insertions(+), 3 deletions(-)

(limited to 'common')

diff --git a/common/AST.v b/common/AST.v
index 1f7f7d3..fb80b46 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -54,9 +54,8 @@ Lemma typ_eq: forall (t1 t2: typ), {t1=t2} + {t1<>t2}.
 Proof. decide equality. Defined.
 Global Opaque typ_eq.
 
-Lemma opt_typ_eq: forall (t1 t2: option typ), {t1=t2} + {t1<>t2}.
-Proof. decide equality. apply typ_eq. Defined.
-Global Opaque opt_typ_eq.
+Definition opt_typ_eq: forall (t1 t2: option typ), {t1=t2} + {t1<>t2}
+                     := option_eq typ_eq.
 
 Definition list_typ_eq: forall (l1 l2: list typ), {l1=l2} + {l1<>l2}
                      := list_eq_dec typ_eq.
@@ -78,6 +77,10 @@ Definition proj_sig_res (s: signature) : typ :=
   | Some t => t
   end.
 
+Definition signature_eq: forall (s1 s2: signature), {s1=s2} + {s1<>s2}.
+Proof. generalize opt_typ_eq, list_typ_eq; intros; decide equality. Defined.
+Global Opaque signature_eq.
+
 (** Memory accesses (load and store instructions) are annotated by
   a ``memory chunk'' indicating the type, size and signedness of the
   chunk of memory being accessed. *)
@@ -93,6 +96,10 @@ Inductive memory_chunk : Type :=
   | Mfloat64        (**r 64-bit double-precision float *)
   | Mfloat64al32.   (**r 64-bit double-precision float, 4-aligned *)
 
+Definition chunk_eq: forall (c1 c2: memory_chunk), {c1=c2} + {c1<>c2}.
+Proof. decide equality. Defined.
+Global Opaque chunk_eq.
+
 (** The type (integer/pointer or float) of a chunk. *)
 
 Definition type_of_chunk (c: memory_chunk) : typ :=
@@ -526,6 +533,16 @@ Definition ef_reloads (ef: external_function) : bool :=
   | _ => true
   end.
 
+(** Equality between external functions.  Used in module [Allocation]. *)
+
+Definition external_function_eq: forall (ef1 ef2: external_function), {ef1=ef2} + {ef1<>ef2}.
+Proof.
+  generalize ident_eq signature_eq chunk_eq typ_eq zeq Int.eq_dec; intros.
+  decide equality.
+  apply list_eq_dec. decide equality. apply Float.eq_dec. 
+Defined.
+Global Opaque external_function_eq.
+
 (** Function definitions are the union of internal and external functions. *)
 
 Inductive fundef (F: Type): Type :=
-- 
cgit v1.2.3