Commit 96f5c3a3 authored by Léon Gondelman's avatar Léon Gondelman
Browse files

fix the compilation after the change of a_store_spec rule.

parent 5b5d7cbc
......@@ -31,11 +31,12 @@ Section derived.
Proof.
iIntros "H".
iApply ((a_store_spec _ _
(λ l1, l1 = l)%I
(λ w, v, (l C v (l C[LLvl] w - Φ w)))%I ) with "[] [H] []").
(λ l1, l1 = #l)%I
(λ w, v, (l C v (l C[LLvl] w - Φ w)))%I ) with "[] [$H] []").
- iApply awp_ret; iApply wp_value; eauto.
- done.
- iNext. iIntros (? w) "-> H". eauto with iFrame.
- iNext. iIntros (? w) "-> H".
iDestruct "H" as (v) "H".
eauto with iFrame.
Qed.
Ltac awp_load_ret l := iApply (a_load_ret l); iFrame; eauto.
......
......@@ -13,7 +13,7 @@ Section test.
awp (a_store (a_ret #x) (a_bin_op PlusOp (a_load (a_ret #x)) (a_load (a_ret #x)))) True (λ _, x C[LLvl] #2).
Proof.
iIntros "[Hx Hx']".
iApply (a_store_spec _ _ (λ v, v = x) (λ v, v = #2 x C #1) with "[] [Hx Hx']")%I.
iApply (a_store_spec _ _ (λ v, v = #x) (λ v, v = #2 x C #1) with "[] [Hx Hx']")%I.
{ iApply awp_ret. wp_value_head. eauto. }
- iApply (a_bin_op_spec _ _ (λ v, v = #1 x C{1 / 2} #1)
(λ v, v = #1 x C{1 / 2} #1)
......@@ -24,6 +24,6 @@ Section test.
iExists _; eauto. repeat iSplit; eauto.
by iFrame.
- iNext. iIntros (? ? ->) "[% Hx]"; simplify_eq/=.
iExists _; iFrame. eauto.
iExists _; iFrame. eauto with iFrame.
Qed.
End test.
......@@ -61,6 +61,7 @@ Section tests_vcg.
(a_store (a_ret #l) (a_ret #2)))%E True (λ v, True).
Proof. iIntros "Hl". vcg_solver. Abort.
Lemma test4 (l k : loc) (e: expr) `{Closed [] e}:
( Φ v, k C v - (k C #12 - Φ v) - awp e True Φ) -
l C #1 -
......
......@@ -571,14 +571,14 @@ Section vcg_spec.
eapply tac_envs_split_mapsto; try eassumption.
revert Hgoal. rewrite environments.envs_entails_eq.
rewrite (vcg_wp_correct R); last done.
iIntros (->) "H1 H2".
iIntros (->) "H1 H2".
iSpecialize ("H2" with "H1"). iApply (awp_wand with "H2").
iIntros (v) "H". iDestruct "H" as (E' dv m' Hpre) "(-> & Hmwf & Hm & Hwp)".
rewrite mapsto_wand_list_spec. iApply ("Hwp" with "Hm"). done.
Qed.
End vcg_spec.
Arguments wp_interp : simpl never.
(* Arguments wp_interp : simpl never. *)
Ltac vcg_solver :=
eapply tac_vcg_sound;
......
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