From 5043bd70472eb2c612eb6fe924fb2d32d59038f9 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Sun, 25 Dec 2016 17:05:11 +0100
Subject: [PATCH] Rules for case.
---
_CoqProject | 1 +
theories/lang/lang.v | 2 +-
theories/lang/lifting.v | 2 +-
theories/lang/notation.v | 6 +-
theories/typing/case.v | 125 +++++++++++++++++++++++++++++++++++++++
theories/typing/own.v | 1 +
theories/typing/sum.v | 15 +++--
7 files changed, 138 insertions(+), 14 deletions(-)
create mode 100644 theories/typing/case.v
diff --git a/_CoqProject b/_CoqProject
index e0d8ab8b..40ecd9a4 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -41,3 +41,4 @@ theories/typing/programs.v
theories/typing/borrow.v
theories/typing/cont.v
theories/typing/fixpoint.v
+theories/typing/case.v
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index 05c665b1..62342edc 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -295,7 +295,7 @@ Inductive head_step : expr → state → expr → state → list expr → Prop :
[]
| CaseS i el e σ :
0 ≤ i →
- nth_error el (Z.to_nat i) = Some e →
+ el !! (Z.to_nat i) = Some e →
head_step (Case (Lit $ LitInt i) el) σ e σ []
| ForkS e σ:
head_step (Fork e) σ (Lit LitUnit) σ [e].
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index f0c96434..cfd392c0 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -178,7 +178,7 @@ Qed.
Lemma wp_case E i e el Φ :
0 ≤ i →
- nth_error el (Z.to_nat i) = Some e →
+ el !! (Z.to_nat i) = Some e →
▷ WP e @ E {{ Φ }} -∗ WP Case (Lit $ LitInt i) el @ E {{ Φ }}.
Proof.
iIntros (??) "?". iApply ownP_lift_pure_det_head_step; eauto.
diff --git a/theories/lang/notation.v b/theories/lang/notation.v
index 3b693065..af9528f2 100644
--- a/theories/lang/notation.v
+++ b/theories/lang/notation.v
@@ -23,10 +23,8 @@ Notation "'case:' e0 'of' el" := (Case e0%E el%E)
Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E)
(at level 200, e1, e2, e3 at level 200) : expr_scope.
Notation "()" := LitUnit : val_scope.
-Notation "! e" := (Read Na1Ord e%E)
- (at level 9, right associativity) : expr_scope.
-Notation "!ˢᶜ e" := (Read ScOrd e%E)
- (at level 9, right associativity) : expr_scope.
+Notation "! e" := (Read Na1Ord e%E) (at level 9, format "! e") : expr_scope.
+Notation "!ˢᶜ e" := (Read ScOrd e%E) (at level 9, format "!ˢᶜ e") : expr_scope.
Notation "e1 + e2" := (BinOp PlusOp e1%E e2%E)
(at level 50, left associativity) : expr_scope.
Notation "e1 - e2" := (BinOp MinusOp e1%E e2%E)
diff --git a/theories/typing/case.v b/theories/typing/case.v
new file mode 100644
index 00000000..138b4080
--- /dev/null
+++ b/theories/typing/case.v
@@ -0,0 +1,125 @@
+From iris.proofmode Require Import tactics.
+From lrust.lang Require Import heap.
+From lrust.lifetime Require Import borrow frac_borrow.
+From lrust.typing Require Export uninit uniq_bor shr_bor own sum.
+From lrust.typing Require Import lft_contexts type_context programs.
+
+Section case.
+ Context `{typeG Σ}.
+
+ (* FIXME : the doc does not give [p +â‚— #(S (ty.(ty_size))) â— ...]. *)
+ Lemma type_case_own E L C T p n tyl el:
+ Forall2 (λ ty e,
+ typed_body E L C ((p +â‚— #0 â— own n (uninit 1)) :: (p +â‚— #1 â— own n ty) ::
+ (p +â‚— #(S (ty.(ty_size))) â—
+ own n (uninit (list_max (map ty_size tyl) - ty_size ty))) :: T) e ∨
+ typed_body E L C ((p ◠own n (sum tyl)) :: T) e) tyl el →
+ typed_body E L C ((p â— own n (sum tyl)) :: T) (case: !p of el).
+ Proof.
+ iIntros (Hel tid qE) "#HEAP #LFT Hna HE HL HC HT". wp_bind p.
+ rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
+ iApply (wp_hasty with "Hp"). iIntros (v Hv) "Hp".
+ iDestruct "Hp" as (l) "[EQ [H↦ Hf]]". iDestruct "EQ" as %[=->].
+ iDestruct "H↦" as (vl) "[H↦ Hown]".
+ iDestruct "Hown" as (i vl' vl'') "(>% & >EQlen & Hown)". subst.
+ simpl ty_size. iDestruct "EQlen" as %[=EQlen]. rewrite -EQlen. simpl length.
+ rewrite -Nat.add_1_l app_length -!freeable_sz_split
+ heap_mapsto_vec_cons heap_mapsto_vec_app.
+ iDestruct "H↦" as "(H↦i & H↦vl' & H↦vl'')".
+ iDestruct "Hf" as "(Hfi & Hfvl' & Hfvl'')".
+ rewrite nth_lookup.
+ destruct (tyl !! i) as [ty|] eqn:EQty; last iDestruct "Hown" as ">[]".
+ edestruct @Forall2_lookup_l as (e & He & Hety); eauto.
+ wp_read. iApply wp_case; [lia|by rewrite Nat2Z.id|]. iNext.
+ destruct Hety as [Hety|Hety]; iApply (Hety with "HEAP LFT Hna HE HL HC");
+ rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //; iFrame "HT".
+ - iDestruct (ty.(ty_size_eq) with "Hown") as %<-.
+ iSplitL "H↦i Hfi"; last iSplitR "H↦vl'' Hfvl''".
+ + rewrite shift_loc_0. iExists _. iFrame. iSplit. done. iExists [ #i].
+ rewrite heap_mapsto_vec_singleton.
+ iFrame. iExists [_], []. auto.
+ + iExists _. iFrame. iSplit. done. iExists _. iFrame.
+ + rewrite -EQlen app_length minus_plus uninit_sz -(shift_loc_assoc_nat _ 1).
+ iExists _. iFrame. iSplit. done. iExists _. iFrame. rewrite uninit_own. auto.
+ - iExists _. iSplit. done.
+ assert (EQf:=freeable_sz_split n 1). simpl in EQf. rewrite -EQf. clear EQf.
+ rewrite -EQlen app_length -freeable_sz_split. iFrame.
+ iExists (#i :: vl' ++ vl''). iNext.
+ rewrite heap_mapsto_vec_cons heap_mapsto_vec_app.
+ iFrame. iExists i, vl', vl''. rewrite /= app_length nth_lookup EQty. auto.
+ Qed.
+
+ Lemma type_case_uniq E L C T p κ tyl el:
+ lctx_lft_alive E L κ →
+ Forall2 (λ ty e,
+ typed_body E L C ((p +ₗ #1 ◠&uniq{κ}ty) :: T) e ∨
+ typed_body E L C ((p ◠&uniq{κ}sum tyl) :: T) e) tyl el →
+ typed_body E L C ((p ◠&uniq{κ}sum tyl) :: T) (case: !p of el).
+ Proof.
+ iIntros (Halive Hel tid qE) "#HEAP #LFT Hna HE HL HC HT". wp_bind p.
+ rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
+ iApply (wp_hasty with "Hp"). iIntros (v Hv) "Hp".
+ iDestruct "Hp" as (l P) "[[EQ HP] Hb]". iDestruct "EQ" as %[=->].
+ iMod (bor_iff with "LFT HP Hb") as "Hb". done.
+ iMod (Halive with "HE HL") as (q) "[Htok Hclose]". done.
+ iMod (bor_acc_cons with "LFT Hb Htok") as "[H↦ Hclose']". done.
+ iDestruct "H↦" as (vl) "[H↦ Hown]".
+ iDestruct "Hown" as (i vl' vl'') "(>% & >EQlen & Hown)". subst.
+ iDestruct "EQlen" as %[=EQlen].
+ rewrite heap_mapsto_vec_cons heap_mapsto_vec_app nth_lookup.
+ iDestruct "H↦" as "(H↦i & H↦vl' & H↦vl'')".
+ destruct (tyl !! i) as [ty|] eqn:EQty; last iDestruct "Hown" as ">[]".
+ edestruct @Forall2_lookup_l as (e & He & Hety); eauto.
+ wp_read. iApply wp_case; [lia|by rewrite Nat2Z.id|]. iNext.
+ iDestruct (ty.(ty_size_eq) with "Hown") as %EQlenvl'.
+ destruct Hety as [Hety|Hety].
+ - iMod ("Hclose'" $! (shift_loc l 1 ↦∗: ty.(ty_own) tid)%I
+ with "[H↦vl' Hown] [H↦i H↦vl'']") as "[Hb Htok]".
+ { iExists vl'. iFrame. }
+ { iIntros "!>Hown". iDestruct "Hown" as (vl'2) "[H↦ Hown]".
+ iExists (#i::vl'2++vl''). iIntros "!>". iNext.
+ iDestruct (ty.(ty_size_eq) with "Hown") as %EQlenvl'2.
+ rewrite heap_mapsto_vec_cons heap_mapsto_vec_app EQlenvl' EQlenvl'2.
+ iFrame. iExists _, _, _. iSplit. by auto.
+ rewrite /= -EQlen !app_length EQlenvl' EQlenvl'2 nth_lookup EQty /=. auto. }
+ iMod ("Hclose" with "Htok") as "[HE HL]".
+ iApply (Hety with "HEAP LFT Hna HE HL HC").
+ rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //. iFrame "HT".
+ iExists _, _. iFrame. iSplit. done. iSplit; iIntros "!>!#$".
+ - iMod ("Hclose'" with "* [H↦i H↦vl' H↦vl'' Hown] []") as "[Hb Htok]";
+ [|by iIntros "!>$"|].
+ { iExists (#i::vl'++vl'').
+ rewrite heap_mapsto_vec_cons heap_mapsto_vec_app -EQlen. iFrame. iNext.
+ iExists i, vl', vl''. rewrite nth_lookup EQty. auto. }
+ iMod ("Hclose" with "Htok") as "[HE HL]".
+ iApply (Hety with "HEAP LFT Hna HE HL HC").
+ rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //. iFrame "HT".
+ iExists _, _. iFrame. iSplit. done. iSplit; iIntros "!>!#$".
+ Qed.
+
+ Lemma type_case_shr E L C T p κ tyl el:
+ lctx_lft_alive E L κ →
+ Forall2 (λ ty e,
+ typed_body E L C ((p +ₗ #1 ◠&shr{κ}ty) :: T) e ∨
+ typed_body E L C ((p ◠&shr{κ}sum tyl) :: T) e) tyl el →
+ typed_body E L C ((p ◠&shr{κ}sum tyl) :: T) (case: !p of el).
+ Proof.
+ iIntros (Halive Hel tid qE) "#HEAP #LFT Hna HE HL HC HT". wp_bind p.
+ rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
+ iApply (wp_hasty with "Hp"). iIntros (v Hv) "Hp".
+ iDestruct "Hp" as (l) "[EQ Hl]". iDestruct "EQ" as %[=->].
+ iDestruct "Hl" as (i) "[#Hb Hshr]".
+ iMod (Halive with "HE HL") as (q) "[Htok Hclose]". done.
+ iMod (frac_bor_acc with "LFT Hb Htok") as (q') "[[H↦i H↦vl''] Hclose']". done.
+ rewrite nth_lookup.
+ destruct (tyl !! i) as [ty|] eqn:EQty; last iDestruct "Hshr" as "[]".
+ edestruct @Forall2_lookup_l as (e & He & Hety); eauto.
+ wp_read. iApply wp_case; [lia|by rewrite Nat2Z.id|]. iNext.
+ iMod ("Hclose'" with "[$H↦i $H↦vl'']") as "Htok".
+ iMod ("Hclose" with "Htok") as "[HE HL]".
+ destruct Hety as [Hety|Hety]; iApply (Hety with "HEAP LFT Hna HE HL HC");
+ rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //; iFrame "HT".
+ - iExists _. auto.
+ - iExists _. iSplit. done. iExists i. rewrite nth_lookup EQty /=. auto.
+ Qed.
+End case.
\ No newline at end of file
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 367c3ab7..60b534d2 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -16,6 +16,7 @@ Section own.
| sz, n => †{mk_Qp (sz / n) _}l…sz
end%I.
Next Obligation. intros _ _ _ sz0 ? n ?. by apply Qcmult_pos_pos. Qed.
+ Arguments freeable_sz : simpl never.
Global Instance freable_sz_timeless n sz l : TimelessP (freeable_sz n sz l).
Proof. destruct sz, n; apply _. Qed.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 2f33dc40..4adb9c51 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -42,13 +42,12 @@ Section sum.
Definition list_max (l : list nat) := foldr max 0%nat l.
Definition is_pad i tyl (vl : list val) : iProp Σ :=
- ⌜((nth i tyl ∅).(ty_size) + length vl)%nat =
- (list_max $ map ty_size $ tyl)âŒ%I.
+ ⌜((nth i tyl ∅).(ty_size) + length vl)%nat = (list_max $ map ty_size tyl)âŒ%I.
Lemma split_sum_mt l tid q tyl :
(l ↦∗{q}: λ vl,
∃ (i : nat) vl' vl'', ⌜vl = #i :: vl' ++ vl''⌠∗
- ⌜length vl = S (list_max $ map ty_size $ tyl)⌠∗
+ ⌜length vl = S (list_max $ map ty_size tyl)⌠∗
ty_own (nth i tyl ∅) tid vl')%I
⊣⊢ ∃ (i : nat), (l ↦{q} #i ∗
shift_loc l (S $ (nth i tyl ∅).(ty_size)) ↦∗{q}: is_pad i tyl) ∗
@@ -75,10 +74,10 @@ Section sum.
Qed.
Program Definition sum (tyl : list type) :=
- {| ty_size := S (list_max $ map ty_size $ tyl);
+ {| ty_size := S (list_max $ map ty_size tyl);
ty_own tid vl :=
(∃ (i : nat) vl' vl'', ⌜vl = #i :: vl' ++ vl''⌠∗
- ⌜length vl = S (list_max $ map ty_size $ tyl)⌠∗
+ ⌜length vl = S (list_max $ map ty_size tyl)⌠∗
(nth i tyl ∅).(ty_own) tid vl')%I;
ty_shr κ tid l :=
(∃ (i : nat),
@@ -122,9 +121,9 @@ Section sum.
edestruct @Forall2_lookup_l as (ty2 & Hl2 & Hty2); [done..|].
rewrite (nth_lookup_Some tyl2 _ _ ty2) //.
by iApply (Hty2 with "* [] []"). }
- clear -Hleq. iSplit; last (iSplit; iAlways).
- - simpl. by rewrite Hleq.
- - iIntros (tid vl) "H". iDestruct "H" as (i vl' vl'') "(% & % & Hown)".
+ clear -Hleq. iSplit; last iSplit.
+ - simpl. by rewrite Hleq.
+ - iNext. iAlways. iIntros (tid vl) "H". iDestruct "H" as (i vl' vl'') "(% & % & Hown)".
iExists i, vl', vl''. iSplit; first done.
iSplit; first by rewrite -Hleq.
iDestruct ("Hty" $! i) as "(_ & #Htyi & _)". by iApply "Htyi".
--
GitLab