diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-12-26 16:55:06 +0100 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-12-26 16:55:06 +0100 |
commit | 647cc8dc9699277cb1e77ae3b07c007186720d59 (patch) | |
tree | a37eba4eb015f8b093793858c8f25589fd816af8 /x86 | |
parent | e65eeecf7f34076cbfad6876ec21623ad25e9cf7 (diff) | |
download | compcert-647cc8dc9699277cb1e77ae3b07c007186720d59.tar.gz compcert-647cc8dc9699277cb1e77ae3b07c007186720d59.zip |
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
Diffstat (limited to 'x86')
-rw-r--r-- | x86/Op.v | 16 |
1 files changed, 8 insertions, 8 deletions
@@ -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. |