Coq-defined equality functions for Allocation.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2225 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

6 files changed, 56 insertions, 45 deletions

diff --git a/backend/Allocation.v b/backend/Allocation.v
index 8674335..e4d0972 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -127,14 +127,6 @@ Definition check_succ (s: node) (b: LTL.bblock) : bool :=
   | _ => false
   end.
 
-Parameter eq_operation: forall (x y: operation), {x=y} + {x<>y}.
-Parameter eq_addressing: forall (x y: addressing), {x=y} + {x<>y}.
-Parameter eq_opt_addressing: forall (x y: option addressing), {x=y} + {x<>y}.
-Parameter eq_condition: forall (x y: condition), {x=y} + {x<>y}.
-Parameter eq_chunk: forall (x y: memory_chunk), {x=y} + {x<>y}.
-Parameter eq_external_function: forall (x y: external_function), {x=y} + {x<>y}.
-Parameter eq_signature: forall (x y: signature), {x=y} + {x<>y}.
-
 Notation "'do' X <- A ; B" := (match A with Some X => B | None => None end)
          (at level 200, X ident, A at level 100, B at level 200)
          : option_monad_scope.
@@ -205,15 +197,15 @@ Definition pair_instr_block
       let (mv1, b1) := extract_moves nil b in
       match b1 with
       | Lload chunk' addr' args' dst' :: b2 =>
-          if eq_chunk chunk Mint64 then
-            assertion (eq_chunk chunk' Mint32);
+          if chunk_eq chunk Mint64 then
+            assertion (chunk_eq chunk' Mint32);
             let (mv2, b3) := extract_moves nil b2 in
             match b3 with
             | Lload chunk'' addr'' args'' dst'' :: b4 =>
                 let (mv3, b5) := extract_moves nil b4 in
-                assertion (eq_chunk chunk'' Mint32);
+                assertion (chunk_eq chunk'' Mint32);
                 assertion (eq_addressing addr addr');
-                assertion (eq_opt_addressing (offset_addressing addr (Int.repr 4)) (Some addr''));
+                assertion (option_eq eq_addressing (offset_addressing addr (Int.repr 4)) (Some addr''));
                 assertion (check_succ s b5);
                 Some(BSload2 addr addr'' args dst mv1 args' dst' mv2 args'' dst'' mv3 s)
             | _ =>
@@ -221,12 +213,12 @@ Definition pair_instr_block
                 if (eq_addressing addr addr') then
                   Some(BSload2_1 addr args dst mv1 args' dst' mv2 s)
                 else
-                 (assertion (eq_opt_addressing (offset_addressing addr (Int.repr 4)) (Some addr'));
+                 (assertion (option_eq eq_addressing (offset_addressing addr (Int.repr 4)) (Some addr'));
                   Some(BSload2_2 addr addr' args dst mv1 args' dst' mv2 s))
             end
           else (
             let (mv2, b3) := extract_moves nil b2 in
-            assertion (eq_chunk chunk chunk');
+            assertion (chunk_eq chunk chunk');
             assertion (eq_addressing addr addr');
             assertion (check_succ s b3);
             Some(BSload chunk addr args dst mv1 args' dst' mv2 s))
@@ -238,20 +230,20 @@ Definition pair_instr_block
       let (mv1, b1) := extract_moves nil b in
       match b1 with
       | Lstore chunk' addr' args' src' :: b2 =>
-          if eq_chunk chunk Mint64 then
+          if chunk_eq chunk Mint64 then
             let (mv2, b3) := extract_moves nil b2 in
             match b3 with
             | Lstore chunk'' addr'' args'' src'' :: b4 =>
-                assertion (eq_chunk chunk' Mint32);
-                assertion (eq_chunk chunk'' Mint32);
+                assertion (chunk_eq chunk' Mint32);
+                assertion (chunk_eq chunk'' Mint32);
                 assertion (eq_addressing addr addr');
-                assertion (eq_opt_addressing (offset_addressing addr (Int.repr 4)) (Some addr''));
+                assertion (option_eq eq_addressing (offset_addressing addr (Int.repr 4)) (Some addr''));
                 assertion (check_succ s b4);
                 Some(BSstore2 addr addr'' args src mv1 args' src' mv2 args'' src'' s)
             | _ => None
             end
           else (
-            assertion (eq_chunk chunk chunk');
+            assertion (chunk_eq chunk chunk');
             assertion (eq_addressing addr addr');
             assertion (check_succ s b2);
             Some(BSstore chunk addr args src mv1 args' src' s))
@@ -262,7 +254,7 @@ Definition pair_instr_block
       match b1 with
       | Lcall sg' ros' :: b2 =>
           let (mv2, b3) := extract_moves nil b2 in
-          assertion (eq_signature sg sg');
+          assertion (signature_eq sg sg');
           assertion (check_succ s b3);
           Some(BScall sg ros args res mv1 ros' mv2 s)
       | _ => None
@@ -271,7 +263,7 @@ Definition pair_instr_block
       let (mv1, b1) := extract_moves nil b in
       match b1 with
       | Ltailcall sg' ros' :: b2 =>
-          assertion (eq_signature sg sg');
+          assertion (signature_eq sg sg');
           Some(BStailcall sg ros args mv1 ros')
       | _ => None
       end
@@ -280,11 +272,11 @@ Definition pair_instr_block
       match b1 with
       | Lbuiltin ef' args' res' :: b2 =>
           let (mv2, b3) := extract_moves nil b2 in
-          assertion (eq_external_function ef ef');
+          assertion (external_function_eq ef ef');
           assertion (check_succ s b3);
           Some(BSbuiltin ef args res mv1 args' res' mv2 s)
       | Lannot ef' args' :: b2 =>
-          assertion (eq_external_function ef ef');
+          assertion (external_function_eq ef ef');
           assertion (check_succ s b2);
           match ef with
           | EF_annot txt typ => Some(BSannot txt typ args res mv1 args' s)
@@ -1132,7 +1124,7 @@ Definition check_entrypoints_aux (rtl: RTL.function) (ltl: LTL.function) (e1: eq
                           (loc_parameters (RTL.fn_sig rtl)) e2);
   assertion (can_undef destroyed_at_function_entry e2);
   assertion (zeq (RTL.fn_stacksize rtl) (LTL.fn_stacksize ltl));
-  assertion (eq_signature (RTL.fn_sig rtl) (LTL.fn_sig ltl));
+  assertion (signature_eq (RTL.fn_sig rtl) (LTL.fn_sig ltl));
   Some tt.
 
 Local Close Scope option_monad_scope.
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 76e9744..a4aa861 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -297,7 +297,7 @@ Proof.
   destruct b0.
   MonadInv; UseParsingLemmas.
   destruct i; MonadInv; UseParsingLemmas.
-  destruct (eq_chunk m Mint64).
+  destruct (chunk_eq m Mint64).
   MonadInv; UseParsingLemmas. 
   destruct b; MonadInv; UseParsingLemmas. destruct i; MonadInv; UseParsingLemmas. 
   eapply ebs_load2; eauto.
@@ -308,7 +308,7 @@ Proof.
   inv H. eapply ebs_load_dead; eauto.
 (* store *)
   destruct b0; MonadInv. destruct i; MonadInv; UseParsingLemmas.
-  destruct (eq_chunk m Mint64).
+  destruct (chunk_eq m Mint64).
   MonadInv; UseParsingLemmas.
   destruct b; MonadInv. destruct i; MonadInv; UseParsingLemmas.
   eapply ebs_store2; eauto.
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 :=
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 804ccef..211569e 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -19,7 +19,6 @@ Require RTLgen.
 Require Inlining.
 Require ConstpropOp.
 Require Constprop.
-Require Allocation.
 Require Compiler.
 
 (* Standard lib *)
@@ -73,16 +72,6 @@ Extract Constant ConstpropOp.propagate_float_constants =>
 Extract Constant Constprop.generate_float_constants =>
   "fun _ -> !Clflags.option_ffloatconstprop >= 2".
 
-(* Allocation *)
-Extract Constant Allocation.eq_operation => "(=)".
-Extract Constant Allocation.eq_addressing => "(=)".
-Extract Constant Allocation.eq_opt_addressing => "(=)".
-Extract Constant Allocation.eq_condition => "(=)".
-Extract Constant Allocation.eq_chunk => "(=)".
-Extract Constant Allocation.eq_external_function => "(=)".
-Extract Constant Allocation.eq_signature => "(=)".
-Extract Constant Allocation.regalloc => "Regalloc.regalloc".
-
 (* Linearize *)
 Extract Constant Linearize.enumerate_aux => "Linearizeaux.enumerate_aux".
 
diff --git a/ia32/Op.v b/ia32/Op.v
index 3dc1f77..998f34d 100644
--- a/ia32/Op.v
+++ b/ia32/Op.v
@@ -122,7 +122,14 @@ Definition Oaddrsymbol (id: ident) (ofs: int) : operation := Olea (Aglobal id of
 Definition Oaddrstack (ofs: int) : operation := Olea (Ainstack ofs).
 Definition Oaddimm (n: int) : operation := Olea (Aindexed n).
 
-(** Comparison functions (used in module [CSE]). *)
+(** Comparison functions (used in modules [CSE] and [Allocation]). *)
+
+Definition eq_condition (x y: condition) : {x=y} + {x<>y}.
+Proof.
+  generalize Int.eq_dec; intro.
+  assert (forall (x y: comparison), {x=y}+{x<>y}). decide equality.
+  decide equality.
+Defined.
 
 Definition eq_addressing (x y: addressing) : {x=y} + {x<>y}.
 Proof.
@@ -136,14 +143,13 @@ Proof.
   generalize Int.eq_dec; intro.
   generalize Float.eq_dec; intro.
   generalize Int64.eq_dec; intro.
-  assert (forall (x y: ident), {x=y}+{x<>y}). exact peq.
-  assert (forall (x y: comparison), {x=y}+{x<>y}). decide equality.
-  assert (forall (x y: condition), {x=y}+{x<>y}). decide equality.
   decide equality.
+  apply peq.
   apply eq_addressing.
+  apply eq_condition.
 Defined.
 
-Global Opaque eq_addressing eq_operation.
+Global Opaque eq_condition eq_addressing eq_operation.
 
 (** * Evaluation functions *)
 
diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index ce5d94e..58c9572 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -633,6 +633,13 @@ Qed.
 
 Set Implicit Arguments.
 
+(** Comparing option types. *)
+
+Definition option_eq (A: Type) (eqA: forall (x y: A), {x=y} + {x<>y}):
+  forall (x y: option A), {x=y} + {x<>y}.
+Proof. decide equality. Defined.
+Global Opaque option_eq.
+
 (** Mapping a function over an option type. *)
 
 Definition option_map (A B: Type) (f: A -> B) (x: option A) : option B :=