From 53c9ae3150f8c7e64c35701c679bc432bf1dbdf2 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 9 Mar 2017 22:11:56 +0100
Subject: [PATCH] update to latest Iris
---
opam.pins | 2 +-
theories/lang/lifting.v | 24 +++++++++++++++++-------
theories/typing/type.v | 2 +-
3 files changed, 19 insertions(+), 9 deletions(-)
diff --git a/opam.pins b/opam.pins
index 0af3bc66..5957dcd0 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 5874f41e10c229d0b7df07a1e4e58f5e61a1af0a
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 5180d1cd4548b2ae5193fe9e76b97cbf6ffbc345
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index 887fbc2c..faa9932c 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -214,10 +214,21 @@ Lemma wp_fork E e :
{{{ ▷ WP e {{ _, True }} }}} Fork e @ E {{{ RET LitV LitUnit; True }}}.
Proof.
iIntros (?) "?HΦ". iApply wp_lift_pure_det_head_step; eauto.
- by intros; inv_head_step; eauto. iNext.
+ by intros; inv_head_step; eauto. iApply step_fupd_intro; first done. iNext.
rewrite big_sepL_singleton. iFrame. iApply wp_value. done. by iApply "HΦ".
Qed.
+Lemma wp_rec_step_fupd E E' e f xl erec erec' el Φ :
+ e = Rec f xl erec →
+ Forall (λ ei, is_Some (to_val ei)) el →
+ Closed (f :b: xl +b+ []) erec →
+ subst_l (f::xl) (e::el) erec = Some erec' →
+ (|={E,E'}▷=> WP erec' @ E {{ Φ }}) -∗ WP App e el @ E {{ Φ }}.
+Proof.
+ iIntros (-> ???) "H". iApply wp_lift_pure_det_head_step_no_fork; subst; eauto.
+ by intros; inv_head_step; eauto.
+Qed.
+
Lemma wp_rec E e f xl erec erec' el Φ :
e = Rec f xl erec →
Forall (λ ei, is_Some (to_val ei)) el →
@@ -225,8 +236,8 @@ Lemma wp_rec E e f xl erec erec' el Φ :
subst_l (f::xl) (e::el) erec = Some erec' →
▷ WP erec' @ E {{ Φ }} -∗ WP App e el @ E {{ Φ }}.
Proof.
- iIntros (-> ???) "?". iApply wp_lift_pure_det_head_step; subst; eauto.
- by intros; inv_head_step; eauto. iNext. rewrite big_sepL_nil. by iFrame.
+ iIntros (-> ???) "?". iApply wp_rec_step_fupd; [done..|].
+ iApply step_fupd_intro; done.
Qed.
(* TODO: wp_eq for locations, if needed.
@@ -249,12 +260,11 @@ Lemma wp_bin_op_pure E op l1 l2 l' :
Proof.
iIntros (? Φ) "HΦ". iApply wp_lift_pure_head_step; eauto.
{ intros. by inv_head_step. }
- iNext. iIntros (e2 efs σ Hs).
+ iApply step_fupd_intro; first done. iNext. iIntros (e2 efs σ Hs).
inv_head_step; rewrite big_sepL_nil right_id.
rewrite -wp_value //. iApply "HΦ". eauto.
Qed.
-
Lemma wp_le E (n1 n2 : Z) P Φ :
(n1 ≤ n2 → P -∗ ▷ Φ (LitV $ true)) →
(n2 < n1 → P -∗ ▷ Φ (LitV false)) →
@@ -309,8 +319,8 @@ Lemma wp_case E i e el Φ :
el !! (Z.to_nat i) = Some e →
▷ WP e @ E {{ Φ }} -∗ WP Case (Lit $ LitInt i) el @ E {{ Φ }}.
Proof.
- iIntros (??) "?". iApply wp_lift_pure_det_head_step; eauto.
- by intros; inv_head_step; eauto. iNext. rewrite big_sepL_nil. by iFrame.
+ iIntros (??) "?". iApply wp_lift_pure_det_head_step_no_fork'; eauto.
+ by intros; inv_head_step; eauto.
Qed.
Lemma wp_if E (b : bool) e1 e2 Φ :
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 563a333e..e083ca78 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -51,7 +51,7 @@ Instance: Params (@ty_size) 2.
Instance: Params (@ty_own) 2.
Instance: Params (@ty_shr) 2.
-Arguments ty_own {_ _} !_ _ !_ /.
+Arguments ty_own {_ _} _ _ !_ /.
Record simple_type `{typeG Σ} :=
{ st_own : thread_id → list val → iProp Σ;
--
GitLab