From 647cc8dc9699277cb1e77ae3b07c007186720d59 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 26 Dec 2016 16:55:06 +0100 Subject: 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 --- x86/Op.v | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'x86') 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. -- cgit