From 766dbcd2415df9256f197dc562a0a15f9b0ddeac Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 13 Dec 2016 18:03:41 +0100
Subject: [PATCH] Use different module structuring of uPred.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This fixes the following issue by JH Jourdan:

  The fact of including uPred_[...] in the module uPred (in base_logic.v),
  implies that typeclasses instances are declared twice. Once in module
  uPred and once in module uPred_[...]. This has the unfortunate
  consequence that it has to backtrack to both instances each time the
  first one fails, making failure of type class search for e.g.
  PersistentP potentially exponential.

  Goal ((□ ∀ (x1 x2 x3 x4 x5: nat), True -∗ True) -∗ True : iProp Σ).
    Time iIntros "#H".
    Undo.
    Remove Hints uPred_derived.forall_persistent : typeclass_instances.
    Time iIntros "#H".

Thanks to Jason Gross @ Coq club for suggesting this fix.
---
 theories/base_logic/base_logic.v      | 9 ++++-----
 theories/base_logic/derived.v         | 7 +++----
 theories/base_logic/double_negation.v | 1 -
 theories/base_logic/lib/fractional.v  | 2 +-
 theories/base_logic/primitive.v       | 4 ++--
 theories/base_logic/soundness.v       | 4 ++--
 theories/base_logic/upred.v           | 4 ++--
 7 files changed, 14 insertions(+), 17 deletions(-)

diff --git a/theories/base_logic/base_logic.v b/theories/base_logic/base_logic.v
index 2ea42a57a..79029f48e 100644
--- a/theories/base_logic/base_logic.v
+++ b/theories/base_logic/base_logic.v
@@ -1,13 +1,12 @@
 From iris.base_logic Require Export derived.
 
-Module uPred.
-  Include uPred_entails.
-  Include uPred_primitive.
-  Include uPred_derived.
+Module Import uPred.
+  Export upred.uPred.
+  Export primitive.uPred.
+  Export derived.uPred.
 End uPred.
 
 (* Hint DB for the logic *)
-Import uPred.
 Hint Resolve pure_intro.
 Hint Resolve or_elim or_intro_l' or_intro_r' : I.
 Hint Resolve and_intro and_elim_l' and_elim_r' : I.
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 7361ad147..80f7d2e17 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -1,5 +1,5 @@
 From iris.base_logic Require Export primitive.
-Import uPred_entails uPred_primitive.
+Import upred.uPred primitive.uPred.
 
 Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P → Q) ∧ (Q → P))%I.
 Instance: Params (@uPred_iff) 1.
@@ -34,7 +34,7 @@ Arguments timelessP {_} _ {_}.
 Class PersistentP {M} (P : uPred M) := persistentP : P ⊢ □ P.
 Arguments persistentP {_} _ {_}.
 
-Module uPred_derived.
+Module uPred.
 Section derived.
 Context {M : ucmraT}.
 Implicit Types φ : Prop.
@@ -858,5 +858,4 @@ Proof. by rewrite -(always_always Q); apply always_entails_l'. Qed.
 Lemma always_entails_r P Q `{!PersistentP Q} : (P ⊢ Q) → P ⊢ P ∗ Q.
 Proof. by rewrite -(always_always Q); apply always_entails_r'. Qed.
 End derived.
-
-End uPred_derived.
+End uPred.
diff --git a/theories/base_logic/double_negation.v b/theories/base_logic/double_negation.v
index 566343342..7a31c8d93 100644
--- a/theories/base_logic/double_negation.v
+++ b/theories/base_logic/double_negation.v
@@ -1,5 +1,4 @@
 From iris.base_logic Require Import base_logic.
-Import upred.
 
 (* In this file we show that the bupd can be thought of a kind of
    step-indexed double-negation when our meta-logic is classical *)
diff --git a/theories/base_logic/lib/fractional.v b/theories/base_logic/lib/fractional.v
index cce3c8057..49a856103 100644
--- a/theories/base_logic/lib/fractional.v
+++ b/theories/base_logic/lib/fractional.v
@@ -40,7 +40,7 @@ Section fractional.
   (** Fractional and logical connectives *)
   Global Instance persistent_fractional P :
     PersistentP P → Fractional (λ _, P).
-  Proof. intros HP q q'. by apply uPred_derived.always_sep_dup. Qed.
+  Proof. intros HP q q'. by apply uPred.always_sep_dup. Qed.
 
   Global Instance fractional_sep Φ Ψ :
     Fractional Φ → Fractional Ψ → Fractional (λ q, Φ q ∗ Ψ q)%I.
diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v
index 85dfdb49e..0a6c7239e 100644
--- a/theories/base_logic/primitive.v
+++ b/theories/base_logic/primitive.v
@@ -192,7 +192,7 @@ Coercion uPred_valid {M} (P : uPred M) : Prop := True%I ⊢ P.
 Notation "P -∗ Q" := (P ⊢ Q)
   (at level 99, Q at level 200, right associativity) : C_scope.
 
-Module uPred_primitive.
+Module uPred.
 Definition unseal :=
   (uPred_pure_eq, uPred_and_eq, uPred_or_eq, uPred_impl_eq, uPred_forall_eq,
   uPred_exist_eq, uPred_internal_eq_eq, uPred_sep_eq, uPred_wand_eq, uPred_always_eq,
@@ -596,4 +596,4 @@ Proof. by unseal. Qed.
 Lemma cofe_morC_equivI {A B : ofeT} (f g : A -n> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
 Proof. by unseal. Qed.
 End primitive.
-End uPred_primitive.
+End uPred.
diff --git a/theories/base_logic/soundness.v b/theories/base_logic/soundness.v
index 501d8f1a2..b2c7d8abf 100644
--- a/theories/base_logic/soundness.v
+++ b/theories/base_logic/soundness.v
@@ -1,5 +1,5 @@
-From iris.base_logic Require Export primitive derived.
-Import uPred_entails uPred_primitive.
+From iris.base_logic Require Export base_logic.
+Import uPred.
 
 Section adequacy.
 Context {M : ucmraT}.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index ac98bdddc..cb12bf33d 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -138,7 +138,7 @@ Notation "P ⊣⊢ Q" := (equiv (A:=uPred _) P%I Q%I)
   (at level 95, no associativity) : C_scope.
 Notation "(⊣⊢)" := (equiv (A:=uPred _)) (only parsing) : C_scope.
 
-Module uPred_entails.
+Module uPred.
 Section entails.
 Context {M : ucmraT}.
 Implicit Types P Q : uPred M.
@@ -173,4 +173,4 @@ Proof. by intros ->. Qed.
 Lemma entails_equiv_r (P Q R : uPred M) : (P ⊢ Q) → (Q ⊣⊢ R) → (P ⊢ R).
 Proof. by intros ? <-. Qed.
 End entails.
-End uPred_entails.
+End uPred.
-- 
GitLab