Commit c32e111d authored by Dan Frumin's avatar Dan Frumin
Browse files

fix the tp_ tactics

parent 15dac0c4
......@@ -33,10 +33,9 @@ Section rules.
repeat rel_pure_r. rel_fork_r i as "Hi".
{ simpl. eauto. }
repeat rel_pure_r.
tp_rec i. simpl.
tp_bind i e1.
tp_pure i _. tp_bind i e1.
iMod ("H" with "Hi") as (v1) "[Hi H]".
iSimpl in "Hi". tp_pure i (InjR v1). tp_store i.
iSimpl in "Hi". tp_pure i _. tp_store i.
Abort.
(* rewrite refines_eq /refines_def. *)
(* iIntros (ρ') "_". clear ρ'. *)
......@@ -77,7 +76,7 @@ Section rules.
repeat rel_pure_r. rel_fork_r i as "Hi".
repeat rel_pure_r.
tp_rec i. simpl.
tp_pure i (InjR _). tp_store i.
tp_pure i _. tp_store i.
rel_bind_l e. rel_bind_r e.
iApply (refines_bind with "H").
iIntros (v v') "Hv". simpl.
......@@ -123,17 +122,11 @@ Section rules.
iApply (join_spec with "l_hndl").
iNext. iIntros (w1). iDestruct 1 as (w2) "[Hj Hw]".
unfold C. iSimpl in "Hi". iSimpl in "Hj".
tp_pure i (InjR v2). iSimpl in "Hi".
tp_store i.
(* TODO: better tp_pure tactics *)
tp_pure j (Lam _ _). simpl.
tp_rec j. simpl.
tp_bind j (spawn.join _). unlock spawn.join.
tp_pure j (App _ #c2). simpl.
iApply fupd_wp. tp_load j. simpl.
tp_pure j (Case _ _ _). tp_pure j (Lam _ _). simpl.
tp_pure j (App _ v2). simpl. tp_pure j (Lam _ _). simpl.
tp_pure j _. simpl. tp_pure j _.
tp_pures i. tp_store i.
tp_pures j.
tp_rec j.
tp_pures j. iApply fupd_wp. tp_load j. tp_normalise j.
tp_pures j.
iModIntro. wp_pures. iExists (v2, w2)%V. eauto.
Qed.
......@@ -167,17 +160,11 @@ Section rules.
iApply (wp_wand with "He2"). iIntros (w1).
iDestruct 1 as (w2) "[Hj Hw]".
iSimpl in "Hi". iSimpl in "Hj".
tp_pure i (InjR v2). iSimpl in "Hi".
tp_pure i _. iSimpl in "Hi".
tp_store i.
(* TODO: better tp_pure tactics *)
tp_pure j (Lam _ _). simpl.
tp_rec j. simpl.
tp_bind j (spawn.join _). unlock spawn.join.
tp_pure j (App _ #c2). simpl.
tp_load j. simpl.
tp_pure j (Case _ _ _). tp_pure j (Lam _ _). simpl.
tp_pure j (App _ v2). simpl. tp_pure j (Lam _ _). simpl.
tp_pure j _. simpl. tp_pure j _.
tp_pures j. tp_rec j.
tp_load j. tp_normalise j.
tp_pures j.
iModIntro. iExists _. iFrame.
Qed.
......@@ -219,12 +206,7 @@ Section rules.
wp_pures. wp_bind (spawn.join _).
iApply (join_spec with "Hdl").
iNext. iIntros (av). iDestruct 1 as (av') "[Hj HA]".
wp_pures.
(* TODO why is this so annoying *)
tp_pure j (Lam _ _). iSimpl in "Hj".
tp_pure j (App _ av'). iSimpl in "Hj".
tp_pure i (Lam _ _). iSimpl in "Hi".
tp_pure i (App _ bv'). iSimpl in "Hi".
wp_pures. tp_pures j. tp_pures i.
wp_rec. wp_pures.
wp_apply (spawn_spec N with "[Hc Hi]").
{ wp_pures.
......@@ -242,12 +224,9 @@ Section rules.
iIntros (cv). iDestruct 1 as (cv') "[Hi HC]".
iApply wp_fupd.
wp_pures. iExists (cv', dv')%V. simpl.
tp_pure i (InjR _). tp_store i.
tp_pure j (Lam _ _). tp_pure j _. simpl.
rewrite /spawn.join. tp_pure j (App _ #c2). simpl.
tp_load j. tp_case j. simpl.
tp_pure j (Lam _ _). tp_pure j (App _ cv'). simpl.
tp_pure j (Lam _ _). tp_pure j (App _ cv'). simpl.
tp_pure j (Pair _ _). eauto with iFrame.
tp_pures i. tp_store i.
tp_pures j.
rewrite /spawn.join. tp_pures j.
tp_load j. iSimpl in "Hj". tp_pures j. eauto with iFrame.
Qed.
End rules.
......@@ -27,14 +27,14 @@ From reloc Require Import examples.stack.CG_stack lib.list.
(** * Source code *)
Definition pop_st_no_offer : val := λ: "r" "mb" "pop",
(match: !"r" with
NONE => NONE
| SOME "l" =>
let: "pair" := !"l" in
if: CAS "r" (SOME "l") (Snd "pair")
then SOME (Fst "pair")
else "pop" "r" "mb"
end).
match: !"r" with
NONE => NONE
| SOME "l" =>
let: "pair" := !"l" in
if: CAS "r" (SOME "l") (Snd "pair")
then SOME (Fst "pair")
else "pop" "r" "mb"
end.
Definition pop_st : val := rec: "pop" "r" "mb" :=
match: !"mb" with
......@@ -49,18 +49,18 @@ Definition pop_st : val := rec: "pop" "r" "mb" :=
end
end.
Definition push_st : val := rec: "push" "r" "mb" "n" :=
let: "off" := mk_offer "n" in
Definition push_st : val := rec: "push" "r" "mb" "x" :=
let: "off" := mk_offer "x" in
"mb" <- SOME "off";;
match: revoke_offer "off" with
NONE => (* the offer was successfully taken *) #()
| SOME "n" =>
| SOME "x" =>
(* nobody took the offer *)
let: "tail" := !"r" in
let: "new" := SOME (ref ("n", "tail")) in
if: CAS "r" "tail" "new"
let: "hd" := SOME (ref ("x", "tail")) in
if: CAS "r" "tail" "hd"
then #()
else "push" "r" "mb" "n"
else "push" "r" "mb" "x"
end.
Definition mk_stack : val := λ: <>,
......@@ -453,37 +453,16 @@ Section refinement.
iApply (pop_no_helping_refinement with "Hinv IH").
+ (* An offer was accepted *)
iIntros "Hj Hoff". rel_pures_l.
unlock {3}CG_locked_push.
unlock {1}acquire {1}release.
(* THIS IS COPY PASTED :-) *)
tp_pure j (App _ (_,_)%V). iSimpl in "Hj".
tp_pure j (Rec _ _ _). iSimpl in "Hj".
repeat (tp_pure j _; iSimpl in "Hj").
tp_pure j (Snd _). iSimpl in "Hj".
unlock acquire. tp_pure j (App _ lk). iSimpl in "Hj".
tp_rec j. tp_pures j. tp_rec j.
unlock is_locked_r. iDestruct "Hl" as (lk' ->) "Hl".
(* TODO: make all the tp_ tactics work without the need for an explicit Fupd *)
iApply refines_spec_ctx. iIntros "#Hρ".
iApply fupd_refines.
(* because we manually applied `fupd_refines`, the tactical `with_spec_ctx` doesn't work anymore *)
tp_cmpxchg_suc j. iSimpl in "Hj".
tp_pure j (Snd _). iSimpl in "Hj".
tp_if j. iSimpl in "Hj".
tp_pure j (Rec _ _ _). iSimpl in "Hj".
tp_rec j. iSimpl in "Hj".
unlock CG_push.
tp_pure j (Fst _). iSimpl in "Hj".
tp_pure j (App _ #st'). iSimpl in "Hj".
tp_pure j (Rec _ _ _). iSimpl in "Hj".
tp_pure j (App _ v2). iSimpl in "Hj".
tp_load j. iSimpl in "Hj".
tp_pure j (Pair _ _).
tp_pure j (InjR _).
tp_store j. iSimpl in "Hj".
tp_pure j (Rec _ _ _).
tp_rec j. iSimpl in "Hj".
tp_pure j (Snd _). unlock release.
tp_pures j. tp_rec j. tp_pures j.
tp_load j. tp_normalise j. tp_pures j.
tp_store j. tp_normalise j. tp_pures j.
tp_rec j. tp_store j.
iSpecialize ("Hoff" with "Hj").
iSpecialize ("HN" with "Hoff").
......
......@@ -64,22 +64,23 @@ Tactic Notation "tp_bind" constr(j) open_constr(efoc) :=
|reflexivity
|(* new goal *)].
Lemma tac_tp_pure `{relocG Σ} j K' e1 e2 Δ1 Δ2 E1 i1 i2 p e ϕ ψ Q n :
Lemma tac_tp_pure `{relocG Σ} e K' e1 j e2 Δ1 E1 i1 i2 p e' ϕ ψ Q n :
e = fill K' e1
PureExec ϕ n e1 e2
( P, ElimModal ψ false false (|={E1}=> P) P Q Q)
nclose specN E1
envs_lookup i1 Δ1 = Some (p, spec_ctx)
envs_lookup i2 Δ1 = Some (false, j e)%I
e = fill K' e1
PureExec ϕ n e1 e2
ψ
ϕ
envs_simple_replace i2 false
(Esnoc Enil i2
(j fill K' e2)) Δ1 = Some Δ2
envs_entails Δ2 Q
e' = fill K' e2
match envs_simple_replace i2 false (Esnoc Enil i2 (j e')) Δ1 with
| Some Δ2 => envs_entails Δ2 Q
| None => False
end
envs_entails Δ1 Q.
Proof.
rewrite envs_entails_eq. intros ?? HΔ1 ? Hfill Hpure Hψ Hϕ ??.
rewrite envs_entails_eq. intros -> Hpure ?? HΔ1 ? Hψ Hϕ -> ?.
rewrite -(idemp bi_and (of_envs Δ1)).
rewrite {1}(envs_lookup_sound' Δ1 false). 2: apply HΔ1.
rewrite bi.sep_elim_l.
......@@ -89,8 +90,9 @@ Proof.
by rewrite ?(bi.intuitionistic_intuitionistically spec_ctx). }
rewrite bi.persistently_and_intuitionistically_sep_l.
rewrite bi.intuitionistic_intuitionistically.
destruct (envs_simple_replace _ _ _ _) as [Δ2|] eqn:HΔ2; try done.
rewrite (envs_simple_replace_sound Δ1 Δ2 i2) //; simpl.
rewrite right_id Hfill.
rewrite right_id.
rewrite (assoc _ spec_ctx (j _)%I).
rewrite step_pure //.
rewrite -[Q]elim_modal // /=.
......@@ -109,23 +111,37 @@ Ltac with_spec_ctx tac :=
| _ => tac ()
end.
(* TODO: The problem here is that it will fail if the redex is not specified, and is not on the top level *)
Tactic Notation "tp_pure" constr(j) open_constr(ef) :=
iStartProof;
with_spec_ctx ltac:(fun _ =>
eapply (tac_tp_pure j _ ef);
[iSolveTC || fail "tp_pure: cannot eliminate modality in the goal"
|solve_ndisj || fail "tp_pure: cannot prove 'nclose specN ⊆ ?'"
|iAssumptionCore || fail "tp_pure: cannot find spec_ctx" (* spec_ctx *)
|iAssumptionCore || fail "tp_pure: cannot find '" j " ⤇ ?'"
|tp_bind_helper (* e = K'[e1]*)
|iSolveTC (* PureExec ϕ n e1 e2 *)
|try (exact I || reflexivity) (* ψ *)
|try (exact I || reflexivity) (* ϕ *)
|pm_reflexivity || fail "tp_pure: this should not happen"
|(* new goal *)]).
Tactic Notation "tp_rec" constr(j) := tp_pure j (App _ _).
lazymatch goal with
| |- context[environments.Esnoc _ ?H (j fill ?K' ?e)] =>
reshape_expr e ltac:(fun K e' =>
unify e' ef;
eapply (tac_tp_pure (fill K' e) (K++K') e' j);
[by rewrite ?fill_app | iSolveTC | ..])
| |- context[environments.Esnoc _ ?H (j ?e)] =>
reshape_expr e ltac:(fun K e' =>
unify e' ef;
eapply (tac_tp_pure e K e' j);
[by rewrite ?fill_app | iSolveTC | ..])
end;
[iSolveTC || fail "tp_pure: cannot eliminate modality in the goal"
|solve_ndisj || fail "tp_pure: cannot prove 'nclose specN ⊆ ?'"
|iAssumptionCore || fail "tp_pure: cannot find spec_ctx" (* spec_ctx *)
|iAssumptionCore || fail "tp_pure: cannot find '" j " ⤇ ?'"
|try (exact I || reflexivity) (* ψ *)
|try (exact I || reflexivity) (* ϕ *)
|simpl; reflexivity || fail "tp_pure: this should not happen" (* e' = fill K' e2 *)
|pm_reduce (* new goal *)]).
Tactic Notation "tp_pures" constr (j) := repeat (tp_pure j _; tp_normalise j).
Tactic Notation "tp_rec" constr(j) :=
let H := fresh in
assert (H := AsRecV_recv);
tp_pure j (App _ _);
clear H.
Tactic Notation "tp_seq" constr(j) := tp_rec j.
Tactic Notation "tp_let" constr(j) := tp_rec j.
Tactic Notation "tp_lam" constr(j) := tp_rec j.
......
......@@ -16,9 +16,7 @@ Lemma test1 E1 j K (l : loc) (n : nat) :
Proof.
iIntros (?) "#? Hj Hl".
tp_load j. tp_normalise j.
tp_closure j. tp_normalise j.
tp_lam j. tp_normalise j.
tp_binop j. tp_normalise j.
tp_pures j.
tp_store j. by iFrame.
Qed.
......@@ -32,11 +30,9 @@ Lemma test2 E1 j K (l : loc) (n : nat) :
Proof.
iIntros (?) "#? Hj Hl".
tp_cmpxchg_fail j. tp_normalise j.
tp_pure j (Snd _). tp_normalise j.
tp_closure j. tp_normalise j.
tp_seq j. tp_normalise j.
tp_binop j. tp_normalise j.
tp_cmpxchg_suc j. tp_pure j (Snd _). by iFrame.
tp_pures j.
tp_cmpxchg_suc j. tp_normalise j.
tp_pures j. by iFrame.
Qed.
(* fork *)
......
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