Commit 284ccdd5 authored by Robbert Krebbers's avatar Robbert Krebbers

Let stateful tactics try all decompositions.

This problem has been reported by Léon Gondelman.

Before, when using, for example wp_alloc, in an expression like:

  ref (ref v)

It would apply `tac_wp_alloc` to the outermost ref, after which it
fails to establish that the argument `ref v` is a value. In this
commit, other evaluation positions will be tried whenever it turn
out that the argument of the construct is not a value. The same
applies to store/cas/...

I have implemented this by making use of the new `IntoVal` class.
parent 85498a9a
...@@ -46,7 +46,7 @@ Tactic Notation "wp_pure" open_constr(efoc) := ...@@ -46,7 +46,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => | |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
unify e' efoc; unify e' efoc;
eapply (tac_wp_pure K); eapply (tac_wp_pure K);
[unlock; simpl; apply _ (* PureExec *) [unlock; simpl; apply _ (* PureExec *)
|wp_pure_done (* The pure condition for PureExec *) |wp_pure_done (* The pure condition for PureExec *)
|apply _ (* IntoLaters *) |apply _ (* IntoLaters *)
|simpl_subst; try wp_value_head (* new goal *)]) |simpl_subst; try wp_value_head (* new goal *)])
...@@ -86,7 +86,7 @@ Implicit Types Φ : val → iProp Σ. ...@@ -86,7 +86,7 @@ Implicit Types Φ : val → iProp Σ.
Implicit Types Δ : envs (iResUR Σ). Implicit Types Δ : envs (iResUR Σ).
Lemma tac_wp_alloc Δ Δ' E j K e v Φ : Lemma tac_wp_alloc Δ Δ' E j K e v Φ :
to_val e = Some v IntoVal e v
IntoLaterNEnvs 1 Δ Δ' IntoLaterNEnvs 1 Δ Δ'
( l, Δ'', ( l, Δ'',
envs_app false (Esnoc Enil j (l v)) Δ' = Some Δ'' envs_app false (Esnoc Enil j (l v)) Δ' = Some Δ''
...@@ -111,7 +111,7 @@ Proof. ...@@ -111,7 +111,7 @@ Proof.
Qed. Qed.
Lemma tac_wp_store Δ Δ' Δ'' E i K l v e v' Φ : Lemma tac_wp_store Δ Δ' Δ'' E i K l v e v' Φ :
to_val e = Some v' IntoVal e v'
IntoLaterNEnvs 1 Δ Δ' IntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l v)%I envs_lookup i Δ' = Some (false, l v)%I
envs_simple_replace i false (Esnoc Enil i (l v')) Δ' = Some Δ'' envs_simple_replace i false (Esnoc Enil i (l v')) Δ' = Some Δ''
...@@ -124,7 +124,7 @@ Proof. ...@@ -124,7 +124,7 @@ Proof.
Qed. Qed.
Lemma tac_wp_cas_fail Δ Δ' E i K l q v e1 v1 e2 v2 Φ : Lemma tac_wp_cas_fail Δ Δ' E i K l q v e1 v1 e2 v2 Φ :
to_val e1 = Some v1 to_val e2 = Some v2 IntoVal e1 v1 IntoVal e2 v2
IntoLaterNEnvs 1 Δ Δ' IntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l {q} v)%I v v1 envs_lookup i Δ' = Some (false, l {q} v)%I v v1
(Δ' WP fill K (Lit (LitBool false)) @ E {{ Φ }}) (Δ' WP fill K (Lit (LitBool false)) @ E {{ Φ }})
...@@ -136,7 +136,7 @@ Proof. ...@@ -136,7 +136,7 @@ Proof.
Qed. Qed.
Lemma tac_wp_cas_suc Δ Δ' Δ'' E i K l v e1 v1 e2 v2 Φ : Lemma tac_wp_cas_suc Δ Δ' Δ'' E i K l v e1 v1 e2 v2 Φ :
to_val e1 = Some v1 to_val e2 = Some v2 IntoVal e1 v1 IntoVal e2 v2
IntoLaterNEnvs 1 Δ Δ' IntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l v)%I v = v1 envs_lookup i Δ' = Some (false, l v)%I v = v1
envs_simple_replace i false (Esnoc Enil i (l v2)) Δ' = Some Δ'' envs_simple_replace i false (Esnoc Enil i (l v2)) Δ' = Some Δ''
...@@ -166,11 +166,10 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) := ...@@ -166,11 +166,10 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
lazymatch goal with lazymatch goal with
| |- _ wp ?E ?e ?Q => | |- _ wp ?E ?e ?Q =>
first first
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_alloc _ _ _ H K)) [reshape_expr e ltac:(fun K e' =>
eapply (tac_wp_alloc _ _ _ H K); [apply _|..])
|fail 1 "wp_alloc: cannot find 'Alloc' in" e]; |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
[let e' := match goal with |- to_val ?e' = _ => e' end in [apply _
wp_done || fail "wp_alloc:" e' "not a value"
|apply _
|first [intros l | fail 1 "wp_alloc:" l "not fresh"]; |first [intros l | fail 1 "wp_alloc:" l "not fresh"];
eexists; split; eexists; split;
[env_cbv; reflexivity || fail "wp_alloc:" H "not fresh" [env_cbv; reflexivity || fail "wp_alloc:" H "not fresh"
...@@ -200,11 +199,10 @@ Tactic Notation "wp_store" := ...@@ -200,11 +199,10 @@ Tactic Notation "wp_store" :=
lazymatch goal with lazymatch goal with
| |- _ wp ?E ?e ?Q => | |- _ wp ?E ?e ?Q =>
first first
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_store _ _ _ _ _ K)) [reshape_expr e ltac:(fun K e' =>
eapply (tac_wp_store _ _ _ _ _ K); [apply _|..])
|fail 1 "wp_store: cannot find 'Store' in" e]; |fail 1 "wp_store: cannot find 'Store' in" e];
[let e' := match goal with |- to_val ?e' = _ => e' end in [apply _
wp_done || fail "wp_store:" e' "not a value"
|apply _
|let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in |let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
iAssumptionCore || fail "wp_store: cannot find" l "↦ ?" iAssumptionCore || fail "wp_store: cannot find" l "↦ ?"
|env_cbv; reflexivity |env_cbv; reflexivity
...@@ -217,13 +215,10 @@ Tactic Notation "wp_cas_fail" := ...@@ -217,13 +215,10 @@ Tactic Notation "wp_cas_fail" :=
lazymatch goal with lazymatch goal with
| |- _ wp ?E ?e ?Q => | |- _ wp ?E ?e ?Q =>
first first
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_cas_fail _ _ _ _ K)) [reshape_expr e ltac:(fun K e' =>
eapply (tac_wp_cas_fail _ _ _ _ K); [apply _|apply _|..])
|fail 1 "wp_cas_fail: cannot find 'CAS' in" e]; |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
[let e' := match goal with |- to_val ?e' = _ => e' end in [apply _
wp_done || fail "wp_cas_fail:" e' "not a value"
|let e' := match goal with |- to_val ?e' = _ => e' end in
wp_done || fail "wp_cas_fail:" e' "not a value"
|apply _
|let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in |let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?" iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?"
|try congruence |try congruence
...@@ -236,13 +231,10 @@ Tactic Notation "wp_cas_suc" := ...@@ -236,13 +231,10 @@ Tactic Notation "wp_cas_suc" :=
lazymatch goal with lazymatch goal with
| |- _ wp ?E ?e ?Q => | |- _ wp ?E ?e ?Q =>
first first
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_cas_suc _ _ _ _ _ K)) [reshape_expr e ltac:(fun K e' =>
eapply (tac_wp_cas_suc _ _ _ _ _ K); [apply _|apply _|..])
|fail 1 "wp_cas_suc: cannot find 'CAS' in" e]; |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
[let e' := match goal with |- to_val ?e' = _ => e' end in [apply _
wp_done || fail "wp_cas_suc:" e' "not a value"
|let e' := match goal with |- to_val ?e' = _ => e' end in
wp_done || fail "wp_cas_suc:" e' "not a value"
|apply _
|let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in |let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?" iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?"
|try congruence |try congruence
......
...@@ -42,6 +42,16 @@ Section LiftingTests. ...@@ -42,6 +42,16 @@ Section LiftingTests.
by repeat (wp_pure _). by repeat (wp_pure _).
Qed. Qed.
Definition heap_e4 : expr :=
let: "x" := (let: "y" := ref (ref #1) in ref "y") in
! ! !"x".
Lemma heap_e4_spec : WP heap_e4 {{ v, v = #1 }}%I.
Proof.
rewrite /heap_e4. wp_alloc l. wp_alloc l'. wp_let.
wp_alloc l''. wp_let. by repeat wp_load.
Qed.
Definition FindPred : val := Definition FindPred : val :=
rec: "pred" "x" "y" := rec: "pred" "x" "y" :=
let: "yp" := "y" + #1 in let: "yp" := "y" + #1 in
......
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