From 208141ca31d2af454627a2c09606db17b1cc55af Mon Sep 17 00:00:00 2001 From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org> Date: Wed, 26 Oct 2016 23:03:57 +0200 Subject: [PATCH] Dereferencing : done. --- typing.v | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/typing.v b/typing.v index 9b4b31cf..1f92fd54 100644 --- a/typing.v +++ b/typing.v @@ -312,4 +312,36 @@ Section typing. iModIntro. iExists _. eauto. Qed. + Lemma typed_step_deref_uniq_borrow_borrow ty e κ κ' κ'' q: + typed_step (Valuable.of_expr e ◁ &uniq{κ'} &uniq{κ''} ty ★ κ ⊑ κ' ★ [κ]{q} ★ κ' ⊑ κ'') + ( *e) + (λ v, v ◁ &uniq{κ'} ty ★ κ ⊑ κ' ★ [κ]{q})%P. + Proof. + iIntros (tid) "#HEAP !# [(H◁ & #H⊑1 & [Htok #Hκ'] & #H⊑2) Htl]". + destruct (Valuable.of_expr e) eqn:He; last by iDestruct "H◁" as "[]". + iDestruct "H◁" as (l) "[Heq H↦]". iDestruct "Heq" as %[=->]. + iMod (lft_incl_trade with "H⊑1 Htok") as (q'') "[Htok Hclose]". done. + iMod (lft_borrow_exists with "H↦ Htok") as (vl) "[Hbor Htok]". done. + iMod (lft_borrow_split with "Hbor") as "[H↦ Hbor]". done. + iMod (lft_borrow_exists with "Hbor Htok") as (l') "[Hbor Htok]". done. + iMod (lft_borrow_split with "Hbor") as "[Heq Hbor]". done. + iMod (lft_borrow_persistent with "Heq Htok") as "[>% [Htok1 Htok2]]". done. subst. + iMod (lft_borrow_open with "H↦ Htok1") as "[>H↦ Hclose']". done. + iMod (lft_borrow_open with "Hbor Htok2") as "[Hbor Hclose'']". done. + rewrite heap_mapsto_vec_singleton. + wp_bind e. iApply Valuable.of_expr_wp. done. wp_read. + iMod (lft_borrow_close with "[H↦] Hclose'") as "[_ Htok1]". done. by auto. + iMod (lft_borrow_unnest with "H⊑2 [Hbor Hclose'']") as "[Htok2 Hbor]". done. by iFrame. + iCombine "Htok1" "Htok2" as "Htok". iMod ("Hclose" with "Htok") as "$". iFrame "★#". + iModIntro. iExists _. eauto. + Qed. + + Lemma typed_step_deref_shr_borrow_borrow ty e κ κ' κ'' q: + typed_step (Valuable.of_expr e ◁ &shr{κ'} &uniq{κ''} ty ★ κ ⊑ κ' ★ [κ]{q} ★ κ' ⊑ κ'') + ( *e) + (λ v, v ◁ &shr{κ'} ty ★ κ ⊑ κ' ★ [κ]{q})%P. + Proof. + (* TODO : fix the definition of sharing unique borrows before. *) + Admitted. + End typing. -- GitLab