Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
Iris
Commits
b46d3056
Commit
b46d3056
authored
Feb 21, 2022
by
Ike Mulder
Committed by
Ralf Jung
Feb 21, 2022
Browse files
Prevent cbn from unfolding the 'heap_lang' term.
parent
1bff65be
Changes
4
Hide whitespace changes
Inline
Side-by-side
iris/program_logic/ectx_language.v
View file @
b46d3056
...
...
@@ -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
.
iris/program_logic/ectxi_language.v
View file @
b46d3056
...
...
@@ -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
.
tests/heap_lang.ref
View file @
b46d3056
...
...
@@ -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
...
...
tests/heap_lang.v
View file @
b46d3056
...
...
@@ -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
.
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment