From e29c16ffd28f10bbd74c3bd8e2ac2d953b40021a Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 13 Mar 2017 14:36:14 +0100
Subject: [PATCH] Make type_jump easier to use by not having to give it the
list of parameters.
---
theories/typing/cont.v | 16 ++++++++++-----
theories/typing/examples/get_x.v | 2 +-
theories/typing/examples/init_prod.v | 2 +-
theories/typing/examples/lazy_lft.v | 2 +-
theories/typing/examples/rebor.v | 2 +-
theories/typing/examples/unbox.v | 2 +-
theories/typing/lib/cell.v | 10 +++++-----
theories/typing/lib/fake_shared_box.v | 2 +-
theories/typing/lib/option.v | 10 +++++-----
theories/typing/lib/rc.v | 18 ++++++++---------
theories/typing/lib/refcell/ref_code.v | 8 ++++----
theories/typing/lib/refcell/refcell_code.v | 18 ++++++++---------
theories/typing/lib/refcell/refmut_code.v | 8 ++++----
theories/typing/lib/rwlock/rwlock_code.v | 20 +++++++++----------
.../typing/lib/rwlock/rwlockreadguard_code.v | 8 ++++----
.../typing/lib/rwlock/rwlockwriteguard_code.v | 6 +++---
theories/typing/lib/spawn.v | 4 ++--
17 files changed, 72 insertions(+), 66 deletions(-)
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index 8bb2f484..0a4a6c78 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -8,15 +8,21 @@ Section typing.
Context `{typeG Σ}.
(** Jumping to and defining a continuation. *)
- Lemma type_jump args E L C T k T' :
+ Lemma type_jump args argsv E L C T k T' :
+ (* We use this rather complicated way to state that
+ args = of_val <$> argsv, only because then solve_typing
+ is able to prove it easily. *)
+ Forall2 (λ a av, to_val a = Some av ∨ a = of_val av) args argsv →
(k â—cont(L, T'))%CC ∈ C →
- tctx_incl E L T (T' (list_to_vec args)) →
- typed_body E L C T (k (of_val <$> args)).
+ tctx_incl E L T (T' (list_to_vec argsv)) →
+ typed_body E L C T (k args).
Proof.
- iIntros (HC Hincl tid qE) "#LFT Htl HE HL HC HT".
+ iIntros (Hargs HC Hincl tid qE) "#LFT Hna HE HL HC HT".
iMod (Hincl with "LFT HE HL HT") as "(HE & HL & HT)".
iSpecialize ("HC" with "HE []"); first done.
- rewrite -{3}(vec_to_list_of_list args). iApply ("HC" with "Htl HL HT").
+ assert (args = of_val <$> argsv) as ->.
+ { clear -Hargs. induction Hargs as [|a av ?? [<-%of_to_val| ->] _ ->]=>//=. }
+ rewrite -{3}(vec_to_list_of_list argsv). iApply ("HC" with "Hna HL HT").
Qed.
Lemma type_cont argsb L1 (T' : vec val (length argsb) → _) E L2 C T econt e2 kb :
diff --git a/theories/typing/examples/get_x.v b/theories/typing/examples/get_x.v
index 1eabd4e3..91b7f709 100644
--- a/theories/typing/examples/get_x.v
+++ b/theories/typing/examples/get_x.v
@@ -22,6 +22,6 @@ Section get_x.
iApply type_deref; [solve_typing..|]. iIntros (p'); simpl_subst.
iApply (type_letalloc_1 (&shr{α}int)); [solve_typing..|]. iIntros (r). simpl_subst.
iApply type_delete; [solve_typing..|].
- iApply (type_jump [_]); solve_typing.
+ iApply type_jump; solve_typing.
Qed.
End get_x.
diff --git a/theories/typing/examples/init_prod.v b/theories/typing/examples/init_prod.v
index b7da2ea5..76c97b27 100644
--- a/theories/typing/examples/init_prod.v
+++ b/theories/typing/examples/init_prod.v
@@ -25,6 +25,6 @@ Section init_prod.
iApply type_assign; [solve_typing..|].
iApply type_delete; [solve_typing..|].
iApply type_delete; [solve_typing..|].
- iApply (type_jump [_]); solve_typing.
+ iApply type_jump; solve_typing.
Qed.
End init_prod.
diff --git a/theories/typing/examples/lazy_lft.v b/theories/typing/examples/lazy_lft.v
index 4c25cf38..c498e9a9 100644
--- a/theories/typing/examples/lazy_lft.v
+++ b/theories/typing/examples/lazy_lft.v
@@ -41,6 +41,6 @@ Section lazy_lft.
iApply (type_delete (Î [&shr{_}_;&shr{_}_])%T); [solve_typing..|].
iApply type_delete; [solve_typing..|].
iApply type_delete; [solve_typing..|].
- iApply (type_jump [_]); solve_typing.
+ iApply type_jump; solve_typing.
Qed.
End lazy_lft.
diff --git a/theories/typing/examples/rebor.v b/theories/typing/examples/rebor.v
index 9d7a1297..f3a30336 100644
--- a/theories/typing/examples/rebor.v
+++ b/theories/typing/examples/rebor.v
@@ -32,6 +32,6 @@ Section rebor.
iApply type_delete; [solve_typing..|].
iApply type_delete; [solve_typing..|].
iApply type_delete; [solve_typing..|].
- iApply (type_jump [_]); solve_typing.
+ iApply type_jump; solve_typing.
Qed.
End rebor.
diff --git a/theories/typing/examples/unbox.v b/theories/typing/examples/unbox.v
index b9b57343..85fb12ea 100644
--- a/theories/typing/examples/unbox.v
+++ b/theories/typing/examples/unbox.v
@@ -20,6 +20,6 @@ Section unbox.
iApply type_deref_uniq_own; [solve_typing..|]. iIntros (bx); simpl_subst.
iApply type_letalloc_1; [solve_typing..|]. iIntros (r). simpl_subst.
iApply type_delete; [solve_typing..|].
- iApply (type_jump [_]); solve_typing.
+ iApply type_jump; solve_typing.
Qed.
End unbox.
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index f67534e7..469d46d9 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -89,7 +89,7 @@ Section typing.
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (_ ret arg). inv_vec arg=>x. simpl_subst.
- iApply (type_jump [_]); first solve_typing.
+ iApply type_jump; [solve_typing..|].
iIntros (???) "#LFT $ $ Hty". rewrite !tctx_interp_singleton /=. done.
Qed.
@@ -101,7 +101,7 @@ Section typing.
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (_ ret arg). inv_vec arg=>x. simpl_subst.
- iApply (type_jump [_]); first solve_typing.
+ iApply type_jump; [solve_typing..|].
iIntros (???) "#LFT $ $ Hty". rewrite !tctx_interp_singleton /=. done.
Qed.
@@ -113,7 +113,7 @@ Section typing.
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
- iApply (type_jump [_]). solve_typing. rewrite /tctx_incl /=.
+ iApply type_jump; [solve_typing..|]. rewrite /tctx_incl /=.
iIntros (???) "_ $$". rewrite !tctx_interp_singleton /tctx_elt_interp /=.
by iIntros "$".
Qed.
@@ -134,7 +134,7 @@ Section typing.
iApply type_letalloc_n; [solve_typing| |iIntros (r); simpl_subst].
{ apply (read_shr _ _ _ (cell ty)); solve_typing. }
iApply type_delete; [solve_typing..|].
- iApply (type_jump [_]); solve_typing.
+ iApply type_jump; solve_typing.
Qed.
(* Writing to a cell *)
@@ -186,7 +186,7 @@ Section typing.
{ rewrite /elctx_interp big_opL_singleton. done. }
iApply type_delete; [solve_typing..|].
iApply type_delete; [solve_typing..|].
- iApply (type_jump [ #_]); solve_typing.
+ iApply type_jump; solve_typing.
Qed.
End typing.
diff --git a/theories/typing/lib/fake_shared_box.v b/theories/typing/lib/fake_shared_box.v
index 56d4d9db..819cbba2 100644
--- a/theories/typing/lib/fake_shared_box.v
+++ b/theories/typing/lib/fake_shared_box.v
@@ -34,6 +34,6 @@ Section fake_shared_box.
with "[] LFT Hna [Hα Hβ Hαβ] HL Hk [HT]"); last first.
{ by rewrite tctx_interp_singleton tctx_hasty_val. }
{ rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
- iApply (type_jump [_]); simpl; solve_typing.
+ iApply type_jump; simpl; solve_typing.
Qed.
End fake_shared_box.
diff --git a/theories/typing/lib/option.v b/theories/typing/lib/option.v
index afe2a07f..356aa385 100644
--- a/theories/typing/lib/option.v
+++ b/theories/typing/lib/option.v
@@ -34,12 +34,12 @@ Section option.
iApply type_case_uniq; [solve_typing..|].
constructor; last constructor; last constructor; left.
+ iApply (type_sum_unit (option $ &uniq{α}τ)%T); [solve_typing..|].
- iApply (type_jump [_]); solve_typing.
+ iApply type_jump; solve_typing.
+ iApply (type_sum_assign (option $ &uniq{α}τ)%T); [solve_typing..|].
- iApply (type_jump [_]); solve_typing.
+ iApply type_jump; solve_typing.
- iIntros "/= !#". iIntros (k r). inv_vec r=>r. simpl_subst.
iApply type_delete; [solve_typing..|].
- iApply (type_jump [_]); solve_typing.
+ iApply type_jump; solve_typing.
Qed.
Definition option_unwrap_or Ï„ : val :=
@@ -59,10 +59,10 @@ Section option.
inv_vec p=>o def. simpl_subst.
iApply type_case_own; [solve_typing|]. constructor; last constructor; last constructor.
+ right. iApply type_delete; [solve_typing..|].
- iApply (type_jump [_]); solve_typing.
+ iApply type_jump; solve_typing.
+ left. iApply type_letalloc_n; [solve_typing..|]. iIntros (r). simpl_subst.
iApply (type_delete (Î [uninit _;uninit _;uninit _])); [solve_typing..|].
iApply type_delete; [solve_typing..|].
- iApply (type_jump [_]); solve_typing.
+ iApply type_jump; solve_typing.
Qed.
End option.
diff --git a/theories/typing/lib/rc.v b/theories/typing/lib/rc.v
index b208c196..ee751268 100644
--- a/theories/typing/lib/rc.v
+++ b/theories/typing/lib/rc.v
@@ -169,7 +169,7 @@ Section code.
iNext. iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame. iFrame. iLeft.
rewrite freeable_sz_full_S. iFrame. iExists _. iFrame. }
iApply type_delete; [solve_typing..|].
- iApply (type_jump [ #_]); solve_typing.
+ iApply type_jump; solve_typing.
Qed.
Definition rc_clone : val :=
@@ -236,7 +236,7 @@ Section code.
iFrame "Hrc2". iNext. iRight. iExists _, ν, _. iFrame "#∗". }
{ rewrite /elctx_interp big_sepL_singleton. iFrame. }
iApply type_delete; [solve_typing..|].
- iApply (type_jump [ #_ ]); solve_typing.
+ iApply type_jump; solve_typing.
Qed.
Definition rc_deref : val :=
@@ -279,7 +279,7 @@ Section code.
iFrame "Hx". iNext. iApply ty_shr_mono; done. }
{ rewrite /elctx_interp big_sepL_singleton. iFrame. }
iApply type_delete; [solve_typing..|].
- iApply (type_jump [ #_ ]); solve_typing.
+ iApply type_jump; solve_typing.
Qed.
Definition rc_drop ty : val :=
@@ -361,7 +361,7 @@ Section code.
iApply (type_cont [] [] (λ r, [rcx ◠box (uninit 1); x ◠box (option ty)])%TC) ; [solve_typing..| |]; last first.
{ simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
iApply type_delete; [solve_typing..|].
- iApply (type_jump [_]); solve_typing. }
+ iApply type_jump; solve_typing. }
iIntros (k). simpl_subst.
iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
iIntros (tid qE) "#LFT Hna HE HL Hk".
@@ -387,7 +387,7 @@ Section code.
auto with iFrame. }
iApply (type_sum_memcpy (option _)); [solve_typing..|].
iApply (type_delete (Î [uninit _; uninit _])); [solve_typing..|].
- iApply (type_jump []); solve_typing.
+ iApply type_jump; solve_typing.
- iDestruct "Hproto" as (γ ν q q') "(#Hinv & Hrctok & Hrc◠& Hν & _ & _ & Hclose)".
(* FIXME: linebreaks in "Hclose" do not look as expected. *)
wp_write. wp_op; intros Hc.
@@ -406,7 +406,7 @@ Section code.
{ rewrite tctx_interp_cons tctx_interp_singleton.
rewrite !tctx_hasty_val. unlock. iFrame. }
iApply (type_sum_unit (option ty)); [solve_typing..|].
- iApply (type_jump []); solve_typing.
+ iApply type_jump; solve_typing.
Qed.
Definition rc_get_mut : val :=
@@ -433,7 +433,7 @@ Section code.
iApply (type_cont [] [] (λ r, [rcx ◠box (uninit 1); x ◠box (option $ &uniq{α} ty)])%TC) ; [solve_typing..| |]; last first.
{ simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
iApply type_delete; [solve_typing..|].
- iApply (type_jump [_]); solve_typing. }
+ iApply type_jump; solve_typing. }
iIntros (k). simpl_subst.
iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
iIntros (tid qE) "#LFT Hna HE HL Hk".
@@ -464,7 +464,7 @@ Section code.
unlock. iFrame. }
{ rewrite /elctx_interp big_sepL_singleton. done. }
iApply (type_sum_assign (option (&uniq{_} _))); [solve_typing..|].
- iApply (type_jump []); solve_typing.
+ iApply type_jump; solve_typing.
- wp_if. iDestruct "Hc" as "[(% & _)|(% & Hna & Hproto)]".
{ exfalso. subst c. done. }
iDestruct "Hproto" as (γ ν q q') "(#Hinv & Hrctok & Hrc◠& Hν & #Hshr & #Hν†& Hclose2)".
@@ -480,7 +480,7 @@ Section code.
unlock. iFrame. }
{ rewrite /elctx_interp big_sepL_singleton. done. }
iApply (type_sum_unit (option (&uniq{_} _))); [solve_typing..|].
- iApply (type_jump []); solve_typing.
+ iApply type_jump; solve_typing.
Qed.
(* TODO: * fn make_mut(this: &mut Rc<T>) -> &mut T
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 95e02245..be431b89 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -103,7 +103,7 @@ Section ref_functions.
iFrame "∗#". }
{ rewrite /elctx_interp big_sepL_cons big_sepL_singleton. iFrame. }
iApply type_delete; [solve_typing..|].
- iApply (type_jump [ #_]); solve_typing.
+ iApply type_jump; solve_typing.
Qed.
(* Turning a ref into a shared borrow. *)
@@ -139,7 +139,7 @@ Section ref_functions.
{ rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
iApply (type_letalloc_1 (&shr{α}ty)); [solve_typing..|].
iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
- iApply (type_jump [_]); solve_typing.
+ iApply type_jump; solve_typing.
Qed.
(* Dropping a ref and decrement the count in the corresponding refcell. *)
@@ -200,7 +200,7 @@ Section ref_functions.
{ by rewrite /elctx_interp big_sepL_singleton. }
iApply type_delete; [solve_typing..|].
iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
- iApply (type_jump [_]); solve_typing.
+ iApply type_jump; solve_typing.
Qed.
(* Apply a function within the ref, typically for accessing a component. *)
@@ -267,6 +267,6 @@ Section ref_functions.
iApply type_deref; [solve_typing..|]. iIntros (r'). simpl_subst.
iApply type_assign; [solve_typing..|].
iApply type_delete; [solve_typing..|].
- iApply (type_jump []); solve_typing.
+ iApply type_jump; solve_typing.
Qed.
End ref_functions.
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index 8fd01e4c..75eec338 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -44,7 +44,7 @@ Section refcell_functions.
- iExists _. rewrite uninit_own. auto.
- iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame. simpl. iFrame. auto. }
iApply type_delete; [solve_typing..|].
- iApply (type_jump [ #_]); solve_typing.
+ iApply type_jump; solve_typing.
Qed.
(* The other direction: getting ownership out of a refcell. *)
@@ -81,7 +81,7 @@ Section refcell_functions.
- iExists (_::_). rewrite heap_mapsto_vec_cons uninit_own -Hsz. iFrame. auto.
- iExists vl. iFrame. }
iApply type_delete; [solve_typing..|].
- iApply (type_jump [ #_]); solve_typing.
+ iApply type_jump; solve_typing.
Qed.
Definition refcell_get_mut : val :=
@@ -116,7 +116,7 @@ Section refcell_functions.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
iNext. iExists _. rewrite uninit_own. iFrame. }
iApply type_assign; [solve_typing..|].
- iApply (type_jump [ #_]); solve_typing.
+ iApply type_jump; solve_typing.
Qed.
(* Shared borrowing. *)
@@ -148,7 +148,7 @@ Section refcell_functions.
r!!!0 ◠box (option (ref α ty))])%TC);
[iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg=>r]; simpl_subst; last first.
{ iApply type_delete; [solve_typing..|].
- iApply (type_jump [_]); solve_typing. }
+ iApply type_jump; solve_typing. }
iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
iApply type_deref; [solve_typing..|].
iIntros (x' tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
@@ -167,7 +167,7 @@ Section refcell_functions.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
{ rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
iApply (type_sum_unit (option $ ref α ty)); [solve_typing..|]; first last.
- simpl. iApply (type_jump [_]); solve_typing.
+ simpl. iApply type_jump; solve_typing.
- wp_op. wp_write. wp_apply wp_new; [done..|].
iIntros (lref vl) "(EQ & H†& Hlref)". iDestruct "EQ" as %?%(inj Z.of_nat 2%nat).
destruct vl as [|?[|?[]]]; try done. wp_let.
@@ -220,7 +220,7 @@ Section refcell_functions.
{ rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
iApply (type_sum_memcpy (option $ ref α ty)); [solve_typing..|].
simpl. iApply type_delete; [solve_typing..|].
- iApply (type_jump [_]); solve_typing.
+ iApply type_jump; solve_typing.
Qed.
(* Unique borrowing. *)
@@ -254,7 +254,7 @@ Section refcell_functions.
[iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg=>r];
simpl_subst; last first.
{ iApply type_delete; [solve_typing..|].
- iApply (type_jump [_]); solve_typing. }
+ iApply type_jump; solve_typing. }
iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
iApply type_deref; [solve_typing..|].
iIntros (x' tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
@@ -292,7 +292,7 @@ Section refcell_functions.
{ rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
iApply (type_sum_memcpy (option $ refmut α ty)); [solve_typing..|].
simpl. iApply type_delete; [solve_typing..|].
- iApply (type_jump [_]); solve_typing.
+ iApply type_jump; solve_typing.
- iMod ("Hclose'" with "[Hlx Hownst Hb] Hna") as "[Hβtok Hna]";
first by iExists st; iFrame.
iApply (type_type _ _ _
@@ -301,6 +301,6 @@ Section refcell_functions.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
{ rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
iApply (type_sum_unit (option $ refmut α ty)); [solve_typing..|].
- simpl. iApply (type_jump [_]); solve_typing.
+ simpl. iApply type_jump; solve_typing.
Qed.
End refcell_functions.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 72dd7335..03092079 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -47,7 +47,7 @@ Section refmut_functions.
{ rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
iApply (type_letalloc_1 (&shr{α}ty)); [solve_typing..|].
iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
- iApply (type_jump [_]); solve_typing.
+ iApply type_jump; solve_typing.
Qed.
(* Turning a refmut into a unique borrow. *)
@@ -101,7 +101,7 @@ Section refmut_functions.
{ rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
iApply (type_letalloc_1 (&uniq{α}ty)); [solve_typing..|].
iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
- iApply (type_jump [_]); solve_typing.
+ iApply type_jump; solve_typing.
Qed.
(* Dropping a refmut and set the count to 0 in the corresponding refcell. *)
@@ -150,7 +150,7 @@ Section refmut_functions.
{ by rewrite /elctx_interp big_sepL_singleton. }
iApply type_delete; [solve_typing..|].
iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
- iApply (type_jump [_]); solve_typing.
+ iApply type_jump; solve_typing.
Qed.
(* Apply a function within the refmut, typically for accessing a component. *)
@@ -219,6 +219,6 @@ Section refmut_functions.
iApply type_deref; [solve_typing..|]. iIntros (r'). simpl_subst.
iApply type_assign; [solve_typing..|].
iApply type_delete; [solve_typing..|].
- iApply (type_jump []); solve_typing.
+ iApply type_jump; solve_typing.
Qed.
End refmut_functions.
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 92ae8769..ed3aeea9 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -44,7 +44,7 @@ Section rwlock_functions.
- iExists _. rewrite uninit_own. auto.
- iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame. simpl. iFrame. auto. }
iApply type_delete; [solve_typing..|].
- iApply (type_jump [ #_]); solve_typing.
+ iApply type_jump; solve_typing.
Qed.
(* The other direction: getting ownership out of a rwlock.
@@ -80,7 +80,7 @@ Section rwlock_functions.
- iExists (_::_). rewrite heap_mapsto_vec_cons uninit_own -Hsz. iFrame. auto.
- iExists vl. iFrame. }
iApply type_delete; [solve_typing..|].
- iApply (type_jump [ #_]); solve_typing.
+ iApply type_jump; solve_typing.
Qed.
Definition rwlock_get_mut : val :=
@@ -115,7 +115,7 @@ Section rwlock_functions.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
iNext. iExists _. rewrite uninit_own. iFrame. }
iApply type_assign; [solve_typing..|].
- iApply (type_jump [ #_]); solve_typing.
+ iApply type_jump; solve_typing.
Qed.
(* Acquiring a read lock. *)
@@ -148,13 +148,13 @@ Section rwlock_functions.
[iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg=>r];
simpl_subst; last first.
{ iApply type_delete; [solve_typing..|].
- iApply (type_jump [_]); solve_typing. }
+ iApply type_jump; solve_typing. }
iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
iApply (type_cont [] [] (λ _, [x ◠_; x' ◠_; r ◠_])%TC);
[iIntros (loop)|iIntros "/= !#"; iIntros (loop arg); inv_vec arg];
simpl_subst.
- { iApply (type_jump []); solve_typing. }
+ { iApply type_jump; solve_typing. }
iIntros (tid qE) "#LFT Hna HE HL Hk HT".
rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
iDestruct "HT" as "(Hx & Hx' & Hr)". destruct x' as [[|lx|]|]; try done.
@@ -173,7 +173,7 @@ Section rwlock_functions.
{ rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
iApply (type_sum_unit (option $ rwlockreadguard α ty));
[solve_typing..|]; first last.
- simpl. iApply (type_jump [_]); solve_typing.
+ simpl. iApply type_jump; solve_typing.
- wp_op. wp_bind (CAS _ _ _).
iMod (shr_bor_acc_tok with "LFT Hinv Hβtok1") as "[INV Hclose']"; try done.
iDestruct "INV" as (st') "(Hlx & Hownst & Hst)". revert Hm1.
@@ -226,7 +226,7 @@ Section rwlock_functions.
iApply lft_intersect_mono; first done. iApply lft_incl_refl. }
{ rewrite {1}/elctx_interp big_sepL_singleton //. }
iApply (type_sum_assign (option $ rwlockreadguard α ty)); [solve_typing..|].
- simpl. iApply (type_jump [_]); solve_typing.
+ simpl. iApply type_jump; solve_typing.
+ iApply (wp_cas_int_fail with "Hlx"); try done. iNext. iIntros "Hlx".
iMod ("Hclose'" with "[Hlx Hownst Hst]") as "Hβtok1"; first by iExists _; iFrame.
iModIntro. iApply (wp_if _ false). iNext.
@@ -262,7 +262,7 @@ Section rwlock_functions.
r!!!0 ◠box (option (rwlockwriteguard α ty))])%TC);
[iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg=>r];
simpl_subst; last first.
- { iApply type_delete; [solve_typing..|]. iApply (type_jump [_]); solve_typing. }
+ { iApply type_delete; [solve_typing..|]. iApply type_jump; solve_typing. }
iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
iApply type_deref; [solve_typing..|].
iIntros (x' tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
@@ -285,7 +285,7 @@ Section rwlock_functions.
{ rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
iApply (type_sum_unit (option $ rwlockwriteguard α ty));
[solve_typing..|]; first last.
- rewrite /option /=. iApply (type_jump [_]); solve_typing.
+ rewrite /option /=. iApply type_jump; solve_typing.
- iApply (wp_cas_int_suc with "Hlx"). done. iIntros "!> Hlx".
iMod (own_update with "Hownst") as "[Hownst ?]".
{ by eapply auth_update_alloc, (op_local_update_discrete _ _ writing_st). }
@@ -299,6 +299,6 @@ Section rwlock_functions.
tctx_hasty_val' //. iFrame. iExists _, _. iFrame "∗#". }
{ rewrite {1}/elctx_interp big_sepL_singleton //. }
iApply (type_sum_assign (option $ rwlockwriteguard α ty)); [solve_typing..|].
- simpl. iApply (type_jump [_]); solve_typing.
+ simpl. iApply type_jump; solve_typing.
Qed.
End rwlock_functions.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 7e353fe1..52d67eb4 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -44,7 +44,7 @@ Section rwlockreadguard_functions.
{ rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
iApply (type_letalloc_1 (&shr{α}ty)); [solve_typing..|].
iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
- iApply (type_jump [_]); solve_typing.
+ iApply type_jump; solve_typing.
Qed.
(* Dropping a rwlockreadguard and releasing the corresponding lock. *)
@@ -70,7 +70,7 @@ Section rwlockreadguard_functions.
iApply (type_cont [] [] (λ _, [x ◠_; x' ◠_])%TC);
[iIntros (loop)|iIntros "/= !#"; iIntros (loop arg); inv_vec arg];
simpl_subst.
- { iApply (type_jump []); solve_typing. }
+ { iApply type_jump; solve_typing. }
iIntros (tid qE) "#LFT Hna Hα HL Hk HT".
rewrite {1}/elctx_interp big_sepL_singleton tctx_interp_cons
tctx_interp_singleton !tctx_hasty_val.
@@ -132,7 +132,7 @@ Section rwlockreadguard_functions.
{ rewrite /elctx_interp big_sepL_singleton //. }
iApply type_delete; [solve_typing..|].
iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
- iApply (type_jump [_]); solve_typing.
+ iApply type_jump; solve_typing.
+ iApply (wp_cas_int_fail with "Hlx"); try done. iNext. iIntros "Hlx".
iMod ("Hcloseβ" with "[Hlx H◠Hst]") as "Hβ". by iExists _; iFrame.
iMod ("Hcloseα" with "Hβ") as "HE". iApply (wp_if _ false). iIntros "!> !>".
@@ -141,6 +141,6 @@ Section rwlockreadguard_functions.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val
tctx_hasty_val' //. iFrame. iExists _, _, _, _. iFrame "∗#". }
{ rewrite /elctx_interp big_sepL_singleton //. }
- iApply (type_jump []); solve_typing.
+ iApply type_jump; solve_typing.
Qed.
End rwlockreadguard_functions.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index 9dc6b47f..af415324 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -49,7 +49,7 @@ Section rwlockwriteguard_functions.
{ rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
iApply (type_letalloc_1 (&shr{α}ty)); [solve_typing..|].
iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
- iApply (type_jump [_]); solve_typing.
+ iApply type_jump; solve_typing.
Qed.
(* Turning a rwlockwriteguard into a unique borrow. *)
@@ -96,7 +96,7 @@ Section rwlockwriteguard_functions.
{ rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
iApply (type_letalloc_1 (&uniq{α}ty)); [solve_typing..|].
iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
- iApply (type_jump [_]); solve_typing.
+ iApply type_jump; solve_typing.
Qed.
(* Drop a rwlockwriteguard and release the lock. *)
@@ -139,6 +139,6 @@ Section rwlockwriteguard_functions.
{ rewrite /elctx_interp big_sepL_singleton //. }
iApply type_delete; [solve_typing..|].
iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
- iApply (type_jump [_]); solve_typing.
+ iApply type_jump; solve_typing.
Qed.
End rwlockwriteguard_functions.
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index 9b4d2ebb..f65bb499 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -104,7 +104,7 @@ Section spawn.
iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
iApply type_assign; [solve_typing..|].
iApply type_delete; [solve_typing..|].
- iApply (type_jump [_]); solve_typing.
+ iApply type_jump; solve_typing.
Qed.
Definition join : val :=
@@ -129,6 +129,6 @@ Section spawn.
iDestruct (box_type_incl with "[$Hsub]") as "(_ & Hincl & _)".
iApply "Hincl". done. }
iIntros (r); simpl_subst. iApply type_delete; [solve_typing..|].
- iApply (type_jump [_]); solve_typing.
+ iApply type_jump; solve_typing.
Qed.
End spawn.
--
GitLab