From b46d3056454e7f4e0da3ad26742acba90400eff1 Mon Sep 17 00:00:00 2001
From: Ike Mulder <i.mulder@cs.ru.nl>
Date: Mon, 21 Feb 2022 14:25:03 +0000
Subject: [PATCH] Prevent cbn from unfolding the 'heap_lang' term.

---
 iris/program_logic/ectx_language.v  |  2 ++
 iris/program_logic/ectxi_language.v |  2 ++
 tests/heap_lang.ref                 | 14 ++++++++++++++
 tests/heap_lang.v                   | 10 ++++++++++
 4 files changed, 28 insertions(+)

diff --git a/iris/program_logic/ectx_language.v b/iris/program_logic/ectx_language.v
index a30b5a7d6..1e051b486 100644
--- a/iris/program_logic/ectx_language.v
+++ b/iris/program_logic/ectx_language.v
@@ -324,3 +324,5 @@ Definition LanguageOfEctx (Λ : ectxLanguage) : language :=
   let '@EctxLanguage E V C St K of_val to_val empty comp fill head mix := Λ in
   @Language E V St K of_val to_val _
     (@ectx_lang_mixin (@EctxLanguage E V C St K of_val to_val empty comp fill head mix)).
+
+Global Arguments LanguageOfEctx : simpl never.
diff --git a/iris/program_logic/ectxi_language.v b/iris/program_logic/ectxi_language.v
index 55dc11ff8..0f083de0a 100644
--- a/iris/program_logic/ectxi_language.v
+++ b/iris/program_logic/ectxi_language.v
@@ -164,3 +164,5 @@ Definition EctxLanguageOfEctxi (Λ : ectxiLanguage) : ectxLanguage :=
   let '@EctxiLanguage E V C St K of_val to_val fill head mix := Λ in
   @EctxLanguage E V (list C) St K of_val to_val _ _ _ _
     (@ectxi_lang_ectx_mixin (@EctxiLanguage E V C St K of_val to_val fill head mix)).
+
+Global Arguments EctxLanguageOfEctxi : simpl never.
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 67af46d8f..2c9207a87 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -165,6 +165,20 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   ============================
   --------------------------------------∗
   |={⊤}=> True
+"test_heaplang_not_unfolded"
+     : string
+1 goal
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  ============================
+  @bi_emp_valid (uPredI (iResUR Σ))
+    (@fupd (bi_car (uPredI (iResUR Σ)))
+       (@bi_fupd_fupd (uPredI (iResUR Σ))
+          (@uPred_bi_fupd Σ
+             (@iris_invGS heap_lang Σ (@heapGS_irisGS Σ heapGS0))))
+       (@top coPset coPset_top) (@top coPset coPset_top)
+       (@bi_pure (uPredI (iResUR Σ)) True))
 1 goal
   
   Σ : gFunctors
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 0e80ada63..c20fdf92b 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -326,6 +326,16 @@ Section tests.
   Proof.
     wp_pures. Show. (* No second fupd was added. *)
   Abort.
+
+  Check "test_heaplang_not_unfolded".
+  Lemma test_heaplang_not_unfolded :
+    ⊢@{iPropI Σ} |={⊤}=> True.
+  Proof.
+    cbn.
+    Set Printing All.
+    Show.
+    Unset Printing All.
+  Abort.
 End tests.
 
 Section mapsto_tests.
-- 
GitLab