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
Rice Wine
Iris
Commits
89bc9c1f
Commit
89bc9c1f
authored
Jul 04, 2018
by
Ralf Jung
Browse files
make `wp_alloc l as "?"` behave as expected
parent
aa6ecfbb
Changes
3
Hide whitespace changes
Inline
Side-by-side
tests/heap_lang.ref
View file @
89bc9c1f
...
...
@@ -18,6 +18,18 @@
--------------------------------------∗
WP #l <- #1 + #1;; ! #l @ E {{ v, ⌜v = #2⌝ }}
1 subgoal
Σ : gFunctors
H : heapG Σ
E : coPset
l : loc
============================
"Hl" : l ↦ #1
--------------------------------------∗
WP let: "x" := #l in let: "y" := ref #1 in "x" <- ! "x" + #1;; ! "x"
@ E [{ v, ⌜v = #2⌝ }]
1 subgoal
Σ : gFunctors
...
...
tests/heap_lang.v
View file @
89bc9c1f
...
...
@@ -27,7 +27,7 @@ Section tests.
Lemma
heap_e_spec
E
:
WP
heap_e
@
E
{{
v
,
⌜
v
=
#
2
⌝
}}%
I
.
Proof
.
iIntros
""
.
rewrite
/
heap_e
.
Show
.
wp_alloc
l
.
wp_let
.
wp_load
.
Show
.
wp_alloc
l
as
"?"
.
wp_let
.
wp_load
.
Show
.
wp_op
.
wp_store
.
by
wp_load
.
Qed
.
...
...
@@ -39,7 +39,7 @@ Section tests.
Lemma
heap_e2_spec
E
:
WP
heap_e2
@
E
[{
v
,
⌜
v
=
#
2
⌝
}]%
I
.
Proof
.
iIntros
""
.
rewrite
/
heap_e2
.
wp_alloc
l
.
wp_let
.
wp_alloc
l'
.
wp_let
.
wp_alloc
l
as
"Hl"
.
Show
.
wp_let
.
wp_alloc
l'
.
wp_let
.
wp_load
.
wp_op
.
wp_store
.
wp_load
.
done
.
Qed
.
...
...
theories/heap_lang/proofmode.v
View file @
89bc9c1f
...
...
@@ -360,31 +360,32 @@ Tactic Notation "wp_apply" open_constr(lem) :=
end
).
Tactic
Notation
"wp_alloc"
ident
(
l
)
"as"
constr
(
H
)
:
=
let
Htmp
:
=
iFresh
in
let
finish
_
:
=
first
[
intros
l
|
fail
1
"wp_alloc:"
l
"not fresh"
]
;
eexists
;
split
;
[
pm_reflexivity
||
fail
"wp_alloc:"
H
"not fresh"
|
wp_expr_simpl
;
try
wp_value_head
]
in
|
iDestruct
Htmp
as
H
;
wp_expr_simpl
;
try
wp_value_head
]
in
iStartProof
;
lazymatch
goal
with
|
|-
envs_entails
_
(
wp
?s
?E
?e
?Q
)
=>
first
[
reshape_expr
e
ltac
:
(
fun
K
e'
=>
eapply
(
tac_wp_alloc
_
_
_
_
H
K
)
;
[
iSolveTC
|..])
eapply
(
tac_wp_alloc
_
_
_
_
H
tmp
K
)
;
[
iSolveTC
|..])
|
fail
1
"wp_alloc: cannot find 'Alloc' in"
e
]
;
[
iSolveTC
|
finish
()]
|
|-
envs_entails
_
(
twp
?s
?E
?e
?Q
)
=>
first
[
reshape_expr
e
ltac
:
(
fun
K
e'
=>
eapply
(
tac_twp_alloc
_
_
_
H
K
)
;
[
iSolveTC
|..])
eapply
(
tac_twp_alloc
_
_
_
H
tmp
K
)
;
[
iSolveTC
|..])
|
fail
1
"wp_alloc: cannot find 'Alloc' in"
e
]
;
finish
()
|
_
=>
fail
"wp_alloc: not a 'wp'"
end
.
Tactic
Notation
"wp_alloc"
ident
(
l
)
:
=
let
H
:
=
iFresh
in
wp_alloc
l
as
H
.
wp_alloc
l
as
"?"
.
Tactic
Notation
"wp_load"
:
=
let
solve_mapsto
_
:
=
...
...
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