From 0ecd47dc42da15496ee1bbd42116dca37e7c66e3 Mon Sep 17 00:00:00 2001
From: Simon Spies <spies@mpi-sws.org>
Date: Thu, 2 Feb 2023 10:16:57 +0000
Subject: [PATCH] Use primitive projections for all BI records

---
 iris/bi/embedding.v   | 5 +++++
 iris/bi/interface.v   | 6 +++++-
 iris/bi/internal_eq.v | 5 +++++
 iris/bi/plainly.v     | 5 +++++
 iris/bi/updates.v     | 5 +++++
 tests/heap_lang.ref   | 2 +-
 6 files changed, 26 insertions(+), 2 deletions(-)

diff --git a/iris/bi/embedding.v b/iris/bi/embedding.v
index af9cbbdea..21fe9145e 100644
--- a/iris/bi/embedding.v
+++ b/iris/bi/embedding.v
@@ -3,6 +3,11 @@ From iris.bi Require Import interface derived_laws_later big_op.
 From iris.bi Require Import plainly updates internal_eq.
 From iris.prelude Require Import options.
 
+(* We enable primitive projections in this file to improve the performance of the Iris proofmode:
+    primitive projections for the bi-records makes the proofmode faster.
+*)
+Local Set Primitive Projections.
+
 (* The sections add extra BI assumptions, which is only picked up with [Type*]. *)
 Set Default Proof Using "Type*".
 
diff --git a/iris/bi/interface.v b/iris/bi/interface.v
index 656ce7883..a905be189 100644
--- a/iris/bi/interface.v
+++ b/iris/bi/interface.v
@@ -1,7 +1,11 @@
 From iris.algebra Require Export ofe.
 From iris.bi Require Export notation.
 From iris.prelude Require Import options.
-Set Primitive Projections.
+
+(* We enable primitive projections in this file to improve the performance of the Iris proofmode:
+    primitive projections for the bi-records makes the proofmode faster.
+*)
+Local Set Primitive Projections.
 
 Section bi_mixin.
   Context {PROP : Type} `{!Dist PROP, !Equiv PROP}.
diff --git a/iris/bi/internal_eq.v b/iris/bi/internal_eq.v
index 4ad7f1dcd..1353e7ddf 100644
--- a/iris/bi/internal_eq.v
+++ b/iris/bi/internal_eq.v
@@ -2,6 +2,11 @@ From iris.bi Require Import derived_laws_later big_op.
 From iris.prelude Require Import options.
 Import interface.bi derived_laws.bi derived_laws_later.bi.
 
+(* We enable primitive projections in this file to improve the performance of the Iris proofmode:
+    primitive projections for the bi-records makes the proofmode faster.
+*)
+Local Set Primitive Projections.
+
 (** This file defines a type class for BIs with a notion of internal equality.
 Internal equality is not part of the [bi] canonical structure as [internal_eq]
 can only be given a definition that satisfies [NonExpansive2 internal_eq] _and_
diff --git a/iris/bi/plainly.v b/iris/bi/plainly.v
index 4edbb20de..7404ef443 100644
--- a/iris/bi/plainly.v
+++ b/iris/bi/plainly.v
@@ -3,6 +3,11 @@ From iris.bi Require Import derived_laws_later big_op internal_eq.
 From iris.prelude Require Import options.
 Import interface.bi derived_laws.bi derived_laws_later.bi.
 
+(* We enable primitive projections in this file to improve the performance of the Iris proofmode:
+    primitive projections for the bi-records makes the proofmode faster.
+*)
+Local Set Primitive Projections.
+
 (* The sections add [BiAffine] and the like, which is only picked up with "Type"*. *)
 Set Default Proof Using "Type*".
 
diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index 74d22bd32..359a8dc9e 100644
--- a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ -3,6 +3,11 @@ From iris.bi Require Import interface derived_laws_later big_op plainly.
 From iris.prelude Require Import options.
 Import interface.bi derived_laws.bi derived_laws_later.bi.
 
+(* We enable primitive projections in this file to improve the performance of the Iris proofmode:
+    primitive projections for the bi-records makes the proofmode faster.
+*)
+Local Set Primitive Projections.
+
 (* The sections add extra BI assumptions, which is only picked up with "Type"*. *)
 Set Default Proof Using "Type*".
 
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index f85b167b4..0ffa2e841 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -174,7 +174,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   ============================
   @bi_emp_valid (uPredI (iResUR Σ))
     (@fupd (bi_car (uPredI (iResUR Σ)))
-       (@bi_fupd_fupd (uPredI (iResUR Σ))
+       (@bi_fupd_fupd _
           (@uPred_bi_fupd HasLc Σ
              (@iris_invGS HasLc heap_lang Σ (@heapGS_irisGS HasLc Σ heapGS0))))
        (@top coPset coPset_top) (@top coPset coPset_top)
-- 
GitLab