Replace 'decide equality' in x86/Op.v by custom tactics from lib/BoolEqual.v

Applied to the 92-constructor 'operation' type, 'decide equality' produces a huge transparent term that causes the VM compiler to generate huge code and exceeed a memory limit of Coq on 32-bit platforms.  (The limit is OCaml's, really.)

The lib/BoolEqual.v file defines alternative tactics to build decidable equalities where the transparent part of the definition is smaller (O(N^2) instead of O(N^3)).  The proof parts are still huge (O(N^3)) but they are opaque.

Fixes #151

1 files changed, 8 insertions, 8 deletions

diff --git a/x86/Op.v b/x86/Op.v
index 0de3e061..43133cfa 100644
--- a/x86/Op.v
+++ b/x86/Op.v
@@ -23,7 +23,7 @@
   For a processor-independent set of operations, see the abstract
   syntax and dynamic semantics of the Cminor language.
 *)
-
+Require Import BoolEqual.
 Require Import Coqlib.
 Require Import AST.
 Require Import Integers.
@@ -184,14 +184,14 @@ Proof.
   decide equality.
 Defined.
 
-Definition eq_operation (x y: operation): {x=y} + {x<>y}.
+Definition beq_operation: forall (x y: operation), bool.
 Proof.
-  generalize Int.eq_dec Int64.eq_dec Float.eq_dec Float32.eq_dec; intros.
-  decide equality.
-  apply ident_eq.
-  apply eq_addressing.
-  apply eq_addressing.
-  apply eq_condition.
+  generalize Int.eq_dec Int64.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_addressing eq_condition; boolean_equality.
+Defined.
+
+Definition eq_operation: forall (x y: operation), {x=y} + {x<>y}.
+Proof.
+  decidable_equality_from beq_operation.
 Defined.
 
 Global Opaque eq_condition eq_addressing eq_operation.