From b3de22f7b4b4bb4af38f2adcb462ac512279d12d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=E6=9D=BE=E4=B8=8B=E7=A5=90=E4=BB=8B?= <y.skm24t@gmail.com>
Date: Fri, 8 Apr 2022 18:35:41 +0900
Subject: [PATCH] Minor fix
---
theories/typing/lib/smallvec/smallvec_basic.v | 7 +++----
theories/typing/lib/vec/vec_basic.v | 11 +++++------
2 files changed, 8 insertions(+), 10 deletions(-)
diff --git a/theories/typing/lib/smallvec/smallvec_basic.v b/theories/typing/lib/smallvec/smallvec_basic.v
index e1f09116..58598751 100644
--- a/theories/typing/lib/smallvec/smallvec_basic.v
+++ b/theories/typing/lib/smallvec/smallvec_basic.v
@@ -109,9 +109,8 @@ Section smallvec_basic.
typed_val (smallvec_new n ty) (fn(∅) → smallvec n ty) (λ post _, post []).
Proof.
eapply type_fn; [apply _|]=> _ ???. simpl_subst.
- iIntros (???) "_ #TIME _ _ _ Na L C _ Obs".
- iMod persistent_time_receipt_0 as "⧖". wp_bind (new _).
- iApply (wp_persistent_time_receipt with "TIME ⧖"); [done|].
+ iIntros (???) "_ #TIME _ _ _ Na L C _ Obs". iMod persistent_time_receipt_0 as "⧖".
+ wp_bind (new _). iApply (wp_persistent_time_receipt with "TIME ⧖"); [done|].
iApply wp_new; [done..|]. iIntros "!>" (r).
rewrite !Nat2Z.id/= !heap_mapsto_vec_cons !shift_loc_assoc.
iIntros "[† (↦₀ & ↦₁ & ↦₂ & ↦₃ & ↦ex)] ⧖". wp_seq. wp_write.
@@ -120,7 +119,7 @@ Section smallvec_basic.
iExists _, _. do 2 (iSplit; [done|]). rewrite/= freeable_sz_full.
iFrame "†". iNext. rewrite split_mt_smallvec. iExists true, _, 0, 0, [#].
rewrite/= !heap_mapsto_vec_cons !shift_loc_assoc heap_mapsto_vec_nil.
- iFrame "↦₀ ↦₁ ↦₂ ↦₃". do 2 (iSplit; [done|]). iExists _. iFrame.
+ iFrame "↦₀ ↦₁ ↦₂ ↦₃". do 2 (iSplit; [done|]). iExists _. iFrame "↦ex".
by rewrite repeat_length.
Qed.
diff --git a/theories/typing/lib/vec/vec_basic.v b/theories/typing/lib/vec/vec_basic.v
index 865c9c40..da20c4f2 100644
--- a/theories/typing/lib/vec/vec_basic.v
+++ b/theories/typing/lib/vec/vec_basic.v
@@ -87,11 +87,10 @@ Section vec_basic.
typed_val vec_new (fn(∅) → vec_ty ty) (λ post _, post []).
Proof.
eapply type_fn; [apply _|]=> _ ???. simpl_subst.
- iIntros (???) "_ #TIME _ _ _ Na L C _ Obs".
- wp_apply wp_new; [done..|]. iIntros (r).
- rewrite !heap_mapsto_vec_cons shift_loc_assoc. iIntros "[† (↦₀ & ↦₁ & ↦₂ &_)]".
- wp_seq. iMod persistent_time_receipt_0 as "⧖". wp_bind (new _).
- iApply (wp_persistent_time_receipt with "TIME ⧖"); [done|].
+ iIntros (???) "_ #TIME _ _ _ Na L C _ Obs". wp_apply wp_new; [done..|].
+ iIntros (r). rewrite !heap_mapsto_vec_cons shift_loc_assoc.
+ iIntros "[† (↦₀ & ↦₁ & ↦₂ &_)]". wp_seq. iMod persistent_time_receipt_0 as "⧖".
+ wp_bind (new _). iApply (wp_persistent_time_receipt with "TIME ⧖"); [done|].
iApply wp_new; [done..|]. iIntros "!>" (l) "[†' _] ⧖". wp_bind (_ <- _)%E.
iApply (wp_persistent_time_receipt with "TIME ⧖"); [done|]. wp_write.
iIntros "⧖". wp_seq. wp_op. wp_write. wp_op. wp_write. do 2 wp_seq.
@@ -100,7 +99,7 @@ Section vec_basic.
iExists _, _. do 2 (iSplit; [done|]). rewrite/= freeable_sz_full split_mt_vec'.
iFrame "†". iNext. iExists _, 0, 0, [#]=>/=. iSplit; [done|].
rewrite !heap_mapsto_vec_cons heap_mapsto_vec_nil shift_loc_assoc.
- iFrame "↦₀ ↦₁ ↦₂ †'". iSplit; [by iNext|]. iExists []. by rewrite heap_mapsto_vec_nil.
+ iFrame "↦₀ ↦₁ ↦₂ †'". iSplit; [done|]. iExists []. by rewrite heap_mapsto_vec_nil.
Qed.
Definition vec_drop {𝔄} (ty: type 𝔄) : val :=
--
GitLab