Commit e76ca2de authored by Ralf Jung's avatar Ralf Jung
Browse files

fix build after merging

parent c5fa01fe
Pipeline #5778 passed with stages
in 11 minutes and 3 seconds
...@@ -180,9 +180,9 @@ Proof. ...@@ -180,9 +180,9 @@ Proof.
iModIntro. iSplit=>//. by iApply "HΦ". iModIntro. iSplit=>//. by iApply "HΦ".
Qed. Qed.
Lemma wp_faa E l i1 e2 i2 : Lemma wp_faa s E l i1 e2 i2 :
IntoVal e2 (LitV (LitInt i2)) IntoVal e2 (LitV (LitInt i2))
{{{ l LitV (LitInt i1) }}} FAA (Lit (LitLoc l)) e2 @ E {{{ l LitV (LitInt i1) }}} FAA (Lit (LitLoc l)) e2 @ s; E
{{{ RET LitV (LitInt i1); l LitV (LitInt (i1 + i2)) }}}. {{{ RET LitV (LitInt i1); l LitV (LitInt (i1 + i2)) }}}.
Proof. Proof.
iIntros (<-%of_to_val Φ) ">Hl HΦ". iIntros (<-%of_to_val Φ) ">Hl HΦ".
......
...@@ -162,16 +162,16 @@ Proof. ...@@ -162,16 +162,16 @@ Proof.
rewrite right_id. by apply later_mono, sep_mono_r, wand_mono. rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed. Qed.
Lemma tac_wp_faa Δ Δ' Δ'' E i K l i1 e2 i2 Φ : Lemma tac_wp_faa Δ Δ' Δ'' s E i K l i1 e2 i2 Φ :
IntoVal e2 (LitV (LitInt i2)) IntoVal e2 (LitV (LitInt i2))
IntoLaterNEnvs 1 Δ Δ' IntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l LitV (LitInt i1))%I envs_lookup i Δ' = Some (false, l LitV (LitInt i1))%I
envs_simple_replace i false (Esnoc Enil i (l LitV (LitInt (i1 + i2)))) Δ' = Some Δ'' envs_simple_replace i false (Esnoc Enil i (l LitV (LitInt (i1 + i2)))) Δ' = Some Δ''
envs_entails Δ'' (WP fill K (Lit (LitInt i1)) @ E {{ Φ }}) envs_entails Δ'' (WP fill K (Lit (LitInt i1)) @ s; E {{ Φ }})
envs_entails Δ (WP fill K (FAA (Lit (LitLoc l)) e2) @ E {{ Φ }}). envs_entails Δ (WP fill K (FAA (Lit (LitLoc l)) e2) @ s; E {{ Φ }}).
Proof. Proof.
rewrite /envs_entails=> ?????; subst. rewrite /envs_entails=> ?????; subst.
rewrite -wp_bind. eapply wand_apply; first exact: (wp_faa _ _ i1 _ i2). rewrite -wp_bind. eapply wand_apply; first exact: (wp_faa _ _ _ i1 _ i2).
rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl. rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
rewrite right_id. by apply later_mono, sep_mono_r, wand_mono. rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed. Qed.
...@@ -274,10 +274,10 @@ Tactic Notation "wp_cas_suc" := ...@@ -274,10 +274,10 @@ Tactic Notation "wp_cas_suc" :=
Tactic Notation "wp_faa" := Tactic Notation "wp_faa" :=
iStartProof; iStartProof;
lazymatch goal with lazymatch goal with
| |- envs_entails _ (wp ?E ?e ?Q) => | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
first first
[reshape_expr e ltac:(fun K e' => [reshape_expr e ltac:(fun K e' =>
eapply (tac_wp_faa _ _ _ _ _ K); [apply _|..]) eapply (tac_wp_faa _ _ _ _ _ _ K); [apply _|..])
|fail 1 "wp_faa: cannot find 'CAS' in" e]; |fail 1 "wp_faa: cannot find 'CAS' in" e];
[apply _ [apply _
|let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in |let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end 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