Commit 68582b3b authored by Ralf Jung's avatar Ralf Jung

Merge branch 'ralf/wp_alloc' into 'gen_proofmode'

make `wp_alloc l as "?"` behave as expected

See merge request FP/iris-coq!169
parents 34f64c8d 0dc38cb3
......@@ -18,6 +18,38 @@
--------------------------------------∗
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
H : heapG Σ
l : loc
============================
"Hl1" : l ↦{1 / 2} #0
"Hl2" : l ↦{1 / 2} #0
--------------------------------------∗
True
1 subgoal
Σ : gFunctors
H : heapG Σ
l : loc
============================
--------------------------------------∗
True
1 subgoal
Σ : gFunctors
......
......@@ -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.
......@@ -123,6 +123,14 @@ Section tests.
iIntros (?) "?". wp_cas as ? | ?. done. done.
Qed.
Lemma wp_alloc_split :
WP Alloc #0 {{ _, True }}%I.
Proof. wp_alloc l as "[Hl1 Hl2]". Show. done. Qed.
Lemma wp_alloc_drop :
WP Alloc #0 {{ _, True }}%I.
Proof. wp_alloc l as "_". Show. done. Qed.
End tests.
Section printing_tests.
......
......@@ -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 _ _ _ _ Htmp 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 _ _ _ Htmp 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 _ :=
......
Markdown is supported
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