From d7e85f575fe6a41a700da9cd50236bef8ab03cf8 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Mon, 12 Jun 2017 17:50:18 +0200
Subject: romega: avoid potential slowdown when changing concl by reified
 version

 On some benchmarks provided by Chantal Keller a long time ago,
 romega was abnormally slow compared to omega (or lia).
 It turned out that the change of concl by reified version was
 triggering unnecessary unfolds of Z.add, instead of unfolding
 ReflOmegaCore.Z_as_Int.plus into Z.add. This is now fixed by
 the various Parameter Inline : no more indirections, Z_as_Int.plus
 is directly Z.add.

 Also use Tactics.convert_concl_no_check for this "change", as
 recommended by PMP.
---
 plugins/romega/ReflOmegaCore.v | 20 ++++++++++----------
 plugins/romega/refl_omega.ml   |  2 +-
 2 files changed, 11 insertions(+), 11 deletions(-)

(limited to 'plugins')

diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index d242264a91..51b99b9935 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -18,12 +18,12 @@ Module Type Int.
 
   Bind Scope Int_scope with t.
 
-  Parameter zero : t.
-  Parameter one : t.
-  Parameter plus : t -> t -> t.
-  Parameter opp : t -> t.
-  Parameter minus : t -> t -> t.
-  Parameter mult : t -> t -> t.
+  Parameter Inline zero : t.
+  Parameter Inline one : t.
+  Parameter Inline plus : t -> t -> t.
+  Parameter Inline opp : t -> t.
+  Parameter Inline minus : t -> t -> t.
+  Parameter Inline mult : t -> t -> t.
 
   Notation "0" := zero : Int_scope.
   Notation "1" := one : Int_scope.
@@ -39,10 +39,10 @@ Module Type Int.
 
   (** Int should also be ordered: *)
 
-  Parameter le : t -> t -> Prop.
-  Parameter lt : t -> t -> Prop.
-  Parameter ge : t -> t -> Prop.
-  Parameter gt : t -> t -> Prop.
+  Parameter Inline le : t -> t -> Prop.
+  Parameter Inline lt : t -> t -> Prop.
+  Parameter Inline ge : t -> t -> Prop.
+  Parameter Inline gt : t -> t -> Prop.
   Notation "x <= y" := (le x y): Int_scope.
   Notation "x < y" := (lt x y) : Int_scope.
   Notation "x >= y" := (ge x y) : Int_scope.
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 1a53862ec4..60e6e7de79 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -1016,7 +1016,7 @@ let resolution unsafe env (reified_concl,reified_hyps) systems_list =
 
   Tactics.generalize
     (l_generalize_arg @ List.map EConstr.mkVar useful_hypnames) >>
-  Tactics.change_concl (EConstr.of_constr reified) >>
+  Tactics.convert_concl_no_check (EConstr.of_constr reified) Term.DEFAULTcast >>
   Tactics.apply (EConstr.of_constr (app coq_do_omega [|decompose_tactic|])) >>
   show_goal >>
   (if unsafe then
-- 
cgit v1.2.3