Commit 96883dbd authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'ike/heaplang-cbn' into 'master'

Prevent cbn from unfolding the 'heap_lang' term.

See merge request iris/iris!779
parents 1bff65be b46d3056
Pipeline #63524 passed with stage
in 14 minutes and 7 seconds
......@@ -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.
......@@ -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.
......@@ -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
......
......@@ -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.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment