From 6d26c7955e7b37d8e933b8a9f192e6f848974971 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 4 Mar 2023 19:31:19 +0100
Subject: [PATCH] Tests for type-directed unsealing of `monPred` and `uPred`.

---
 tests/monpred.ref | 21 +++++++++++++++++++++
 tests/monpred.v   | 27 +++++++++++++++++++++++++++
 2 files changed, 48 insertions(+)
 create mode 100644 tests/monpred.ref
 create mode 100644 tests/monpred.v

diff --git a/tests/monpred.ref b/tests/monpred.ref
new file mode 100644
index 000000000..4cbbc1118
--- /dev/null
+++ b/tests/monpred.ref
@@ -0,0 +1,21 @@
+"monPred_unseal_test_1"
+     : string
+1 goal
+  
+  I : biIndex
+  M : ucmra
+  P, Q : uPredI M
+  R : monPred
+  i : I
+  ============================
+  (P ∗ Q) ∗ R i ⊣⊢ False
+"monPred_unseal_test_2"
+     : string
+1 goal
+  
+  I : biIndex
+  M : ucmra
+  P, Q : uPredI M
+  R : monPred
+  ============================
+  ⎡ upred.uPred_sep_def P Q ⎤ ∗ R ⊣⊢ False
diff --git a/tests/monpred.v b/tests/monpred.v
new file mode 100644
index 000000000..26e467e11
--- /dev/null
+++ b/tests/monpred.v
@@ -0,0 +1,27 @@
+From stdpp Require Import strings.
+From iris.base_logic Require Import bi.
+From iris.bi Require Import embedding monpred.
+
+Section tests_unseal.
+  Context {I : biIndex} (M : ucmra).
+
+  Local Notation monPred := (monPred I (uPredI M)).
+
+  Check "monPred_unseal_test_1".
+  Lemma monPred_unseal_test_1 P Q (R : monPred) :
+    ⎡ P ∗ Q ⎤ ∗ R ⊣⊢ False.
+  Proof.
+    intros. split=> i. monPred.unseal.
+    (** Make sure [∗] on uPred is not unfolded *)
+    Show.
+  Abort.
+
+  Check "monPred_unseal_test_2".
+  Lemma monPred_unseal_test_2 P Q (R : monPred) :
+    ⎡ P ∗ Q ⎤ ∗ R ⊣⊢ False.
+  Restart.
+    uPred.unseal.
+    (** Make sure [∗] on monPred is not unfolded *)
+    Show.
+  Abort.
+End tests_unseal.
-- 
GitLab