From 55e3185a4ff155256a65e39779b2b2ea3c22bb0f Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jjourdan@mpi-sws.org>
Date: Wed, 4 Jan 2017 17:59:21 +0100
Subject: [PATCH] Writing the discriminant of a sum.

---
 _CoqProject                            |  2 +-
 theories/lang/memcpy.v                 | 12 ++--
 theories/lang/new_delete.v             |  2 +-
 theories/lang/notation.v               |  4 +-
 theories/typing/own.v                  |  6 +-
 theories/typing/programs.v             |  4 +-
 theories/typing/type_context.v         | 15 +++++
 theories/typing/{case.v => type_sum.v} | 84 +++++++++++++++++++++++++-
 8 files changed, 112 insertions(+), 17 deletions(-)
 rename theories/typing/{case.v => type_sum.v} (64%)

diff --git a/_CoqProject b/_CoqProject
index 40ecd9a4..6f953fda 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -41,4 +41,4 @@ theories/typing/programs.v
 theories/typing/borrow.v
 theories/typing/cont.v
 theories/typing/fixpoint.v
-theories/typing/case.v
+theories/typing/type_sum.v
diff --git a/theories/lang/memcpy.v b/theories/lang/memcpy.v
index 59c8c117..e65919f1 100644
--- a/theories/lang/memcpy.v
+++ b/theories/lang/memcpy.v
@@ -9,22 +9,22 @@ Definition memcpy : val :=
          "memcpy" ["dst" +â‚— #1 ; "len" - #1 ; "src" +â‚— #1].
 Global Opaque memcpy.
 
-Notation "e1 <-{ n } ! e2" :=
+Notation "e1 <⋯ !{ n } e2" :=
   (memcpy (@cons expr e1%E
           (@cons expr (Lit n)
           (@cons expr e2%E nil))))
-  (at level 80, n at next level, format "e1  <-{ n }  ! e2") : expr_scope.
+  (at level 80, n at next level, format "e1  <⋯  !{ n } e2") : expr_scope.
 
-Notation "e1 <-[ i ]{ n } ! e2" :=
-  (e1 <-[i] ☇ ;; e1+ₗ#1 <-{n} !e2)%E
+Notation "e1 <⋯{ i } !{ n } e2" :=
+  (e1 <-{i} ☇ ;; e1+ₗ#1 <⋯ !{n}e2)%E
   (at level 80, n, i at next level,
-   format "e1  <-[ i ]{ n }  ! e2") : lrust_expr_scope.
+   format "e1  <⋯{ i }  !{ n } e2") : expr_scope.
 
 Lemma wp_memcpy `{heapG Σ} E l1 l2 vl1 vl2 q n:
   ↑heapN ⊆ E →
   length vl1 = n → length vl2 = n →
   {{{ heap_ctx ∗ l1 ↦∗ vl1 ∗ l2 ↦∗{q} vl2 }}}
-    #l1 <-{n} !#l2 @ E
+    #l1 <⋯ !{n}#l2 @ E
   {{{ RET #(); l1 ↦∗ vl2 ∗ l2 ↦∗{q} vl2 }}}.
 Proof.
   iIntros (? Hvl1 Hvl2 Φ) "(#Hinv & Hl1 & Hl2) HΦ".
diff --git a/theories/lang/new_delete.v b/theories/lang/new_delete.v
index 6318799b..5c6c407c 100644
--- a/theories/lang/new_delete.v
+++ b/theories/lang/new_delete.v
@@ -45,5 +45,5 @@ Notation "'letalloc:' x := e1 'in' e2" :=
   ((Lam (@cons binder x%E%E%E nil) (x <- e1 ;; e2)) [new [ #1]])%E
   (at level 102, x at level 1, e1, e2 at level 200) : expr_scope.
 Notation "'letalloc:' x :={ n } ! e1 'in' e2" :=
-  ((Lam (@cons binder x%E%E%E nil) (x <-{ n%Z%V } ! e1 ;; e2)) [new [ #n]%E%E])%E
+  ((Lam (@cons binder x%E%E%E nil) (x <⋯ !{n%Z%V}e1 ;; e2)) [new [ #n]%E%E])%E
   (at level 102, x at level 1, e1, e2 at level 200) : expr_scope.
diff --git a/theories/lang/notation.v b/theories/lang/notation.v
index 176b7adb..86ab9ab4 100644
--- a/theories/lang/notation.v
+++ b/theories/lang/notation.v
@@ -79,7 +79,7 @@ Notation "'letcall:' x := f args 'in' e" :=
   (letcont: "_k" [ x ] := e in call: f args → "_k")%E
   (at level 102, x, f, args at level 1, e at level 200) : expr_scope.
 
-Notation "e1 <-[ i ] '☇'" := (e1 <- #i)%E
+Notation "e1 <-{ i } '☇'" := (e1 <- #i)%E
   (only parsing, at level 80) : expr_scope.
-Notation "e1 <-[ i ] e2" := (e1 <-[i] ☇ ;; e1+ₗ#1 <- e2)%E
+Notation "e1 <-{ i } e2" := (e1 <-{i} ☇ ;; e1+ₗ#1 <- e2)%E
   (at level 80) : expr_scope.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 256d7b41..8b1f5bc8 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -63,7 +63,7 @@ Section own.
     move=>n ty N κ l tid ?? /=. iIntros "#LFT Hshr Htok".
     iMod (bor_exists with "LFT Hshr") as (vl) "Hb". set_solver.
     iMod (bor_sep with "LFT Hb") as "[Hb1 Hb2]". set_solver.
-    iMod (bor_exists with "LFT Hb2") as (l') "Hb2". set_solver. 
+    iMod (bor_exists with "LFT Hb2") as (l') "Hb2". set_solver.
     iMod (bor_sep with "LFT Hb2") as "[EQ Hb2]". set_solver.
     iMod (bor_persistent_tok with "LFT EQ Htok") as "[>% $]". set_solver.
     iExists l'. subst. rewrite heap_mapsto_vec_singleton.
@@ -256,8 +256,8 @@ Section typing.
     - apply type_new.
     - solve_typing.
     - move=>xv /=.
-      assert (subst x xv (x <-{ty.(ty_size)} !p ;; e)%E =
-              (xv <-{ty.(ty_size)} !p ;; subst x xv e)%E) as ->.
+      assert (subst x xv (x <⋯ !{ty.(ty_size)}p ;; e)%E =
+              (xv <⋯ !{ty.(ty_size)}p ;; subst x xv e)%E) as ->.
       { (* TODO : simpl_subst should be able to do this. *)
         unfold subst=>/=. repeat f_equal.
         - eapply (is_closed_subst []). done. set_solver.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 5ce9ce92..bc05db76 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -177,7 +177,7 @@ Section typing_rules.
     ty.(ty_size) = n → typed_write E L ty1 ty ty1' → typed_read E L ty2 ty ty2' →
     {{{ heap_ctx ∗ lft_ctx ∗ na_own tid ⊤ ∗ elctx_interp E qE ∗ llctx_interp L qL ∗
         tctx_elt_interp tid (p1 ◁ ty1) ∗ tctx_elt_interp tid (p2 ◁ ty2) }}}
-      (p1 <-{n} !p2)
+      (p1 <⋯ !{n}p2)
     {{{ RET #(); na_own tid ⊤ ∗ elctx_interp E qE ∗ llctx_interp L qL ∗
                  tctx_elt_interp tid (p1 ◁ ty1') ∗ tctx_elt_interp tid (p2 ◁ ty2') }}}.
   Proof.
@@ -199,7 +199,7 @@ Section typing_rules.
 
   Lemma type_memcpy {E L} ty ty1 ty1' ty2 ty2' n p1 p2 :
     ty.(ty_size) = n → typed_write E L ty1 ty ty1' → typed_read E L ty2 ty ty2' →
-    typed_instruction E L [p1 ◁ ty1; p2 ◁ ty2] (p1 <-{n} !p2)
+    typed_instruction E L [p1 ◁ ty1; p2 ◁ ty2] (p1 <⋯ !{n}p2)
                       (λ _, [p1 ◁ ty1'; p2 ◁ ty2']%TC).
   Proof.
     iIntros (Hsz Hwrt Hread tid qE) "#HEAP #LFT Htl HE HL HT".
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 33596b8e..258f7572 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -63,6 +63,16 @@ Section type_context.
     iIntros (v) "%". subst v. wp_op. done.
   Qed.
 
+  Lemma eval_path_closed p v :
+    eval_path p = Some v → Closed [] p.
+  Proof.
+    intros Hpv. revert v Hpv.
+    induction p as [| | |[] p IH [|[]| | | | | | | | | |] _| | | | | | | |]=>//.
+    - unfold eval_path=>? /of_to_val <-. apply is_closed_of_val.
+    - simpl. destruct (eval_path p) as [[[]|]|]; intros ? [= <-].
+      specialize (IH _ eq_refl). apply _.
+  Qed.
+
   (** Type context element *)
   Definition tctx_elt_interp (tid : thread_id) (x : tctx_elt) : iProp Σ :=
     match x with
@@ -106,6 +116,11 @@ Section type_context.
     iIntros (v') "%". subst v'. iApply ("HΦ" with "* [] Hown"). by auto.
   Qed.
 
+  Lemma closed_hasty tid p ty : tctx_elt_interp tid (p ◁ ty) -∗ ⌜Closed [] p⌝.
+  Proof.
+    iIntros "H". iDestruct "H" as (?) "[% _]". eauto using eval_path_closed.
+  Qed.
+
   (** Type context *)
   Definition tctx_interp (tid : thread_id) (T : tctx) : iProp Σ :=
     ([∗ list] x ∈ T, tctx_elt_interp tid x)%I.
diff --git a/theories/typing/case.v b/theories/typing/type_sum.v
similarity index 64%
rename from theories/typing/case.v
rename to theories/typing/type_sum.v
index 99bb0d84..8276d880 100644
--- a/theories/typing/case.v
+++ b/theories/typing/type_sum.v
@@ -1,8 +1,8 @@
 From iris.proofmode Require Import tactics.
-From lrust.lang Require Import heap.
+From lrust.lang Require Import heap memcpy.
 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.
+From lrust.typing Require Import lft_contexts type_context programs product.
 
 Section case.
   Context `{typeG Σ}.
@@ -151,4 +151,84 @@ Section case.
     intros. rewrite ->copy_elem_of_tctx_incl; last done; last apply _.
     apply type_case_shr; first done. eapply Forall2_impl; first done. auto.
   Qed.
+
+  Lemma type_sum_assign {E L} (i : nat) tyl ty1 ty2 ty p1 p2 :
+    Closed [] p1 → Closed [] p2 →
+    tyl !! i = Some ty →
+    typed_write E L ty1 (sum tyl) ty2 →
+    typed_instruction E L [p1 ◁ ty1; p2 ◁ ty] (p1 <-{i} p2) (λ _, [p1 ◁ ty2]%TC).
+  Proof.
+    iIntros (?? Hty Hw ??) "#HEAP #LFT $ HE HL Hp".
+    rewrite tctx_interp_cons tctx_interp_singleton.
+    iDestruct "Hp" as "[Hp1 Hp2]". wp_bind p1. iApply (wp_hasty with "Hp1").
+    iIntros (v1 Hv1) "Hty1".
+    iMod (Hw with "LFT HE HL Hty1") as (l vl) "(H & H↦ & Hw)"=>//=.
+    destruct vl as [|? vl]; iDestruct "H" as %[[= Hlen] ->].
+    rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[H↦0 H↦vl]".
+    wp_write. iApply wp_seq. done. iNext. wp_bind p1.
+    iApply (wp_wand with "[]"); first by iApply (wp_eval_path).
+    iIntros (? ->). wp_op. wp_bind p2. iApply (wp_hasty with "Hp2").
+    iIntros (v2 Hv2) "Hty2". iDestruct (ty_size_eq with "Hty2") as %Hlenty.
+    destruct vl as [|? vl].
+    { exfalso. revert i Hty. clear - Hlen Hlenty. induction tyl=>//= -[|i] /=.
+      - intros [= ->]. simpl in *. lia.
+      - apply IHtyl. simpl in *. lia. }
+    rewrite heap_mapsto_vec_cons. iDestruct "H↦vl" as "[H↦ H↦vl]". wp_write.
+    rewrite tctx_interp_singleton tctx_hasty_val' //. iApply "Hw". iNext.
+    iExists (_::_::_). rewrite !heap_mapsto_vec_cons. iFrame.
+    iExists i, [_], _. rewrite -Hlen nth_lookup Hty. auto.
+  Qed.
+
+  Lemma type_sum_assign_unit {E L} (i : nat) tyl ty1 ty2 p :
+    tyl !! i = Some unit →
+    typed_write E L ty1 (sum tyl) ty2 →
+    typed_instruction E L [p ◁ ty1] (p <-{i} ☇) (λ _, [p ◁ ty2]%TC).
+  Proof.
+    iIntros (Hty Hw ??) "#HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
+    wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v Hv) "Hty".
+    iMod (Hw with "LFT HE HL Hty") as (l vl) "(H & H↦ & Hw)". done.
+    simpl. destruct vl as [|? vl]; iDestruct "H" as %[[= Hlen] ->].
+    rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[H↦0 H↦vl]".
+    wp_write. rewrite tctx_interp_singleton tctx_hasty_val' //.
+    iApply "Hw". iModIntro. iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame.
+    iExists i, [], _. rewrite -Hlen nth_lookup Hty. auto.
+  Qed.
+
+  Lemma type_sum_memcpy {E L} (i : nat) tyl ty1 ty1' ty2 ty2' ty p1 p2 :
+    Closed [] p1 → Closed [] p2 →
+    tyl !! i = Some ty →
+    typed_write E L ty1 (sum tyl) ty1' →
+    typed_read E L ty2 ty ty2' →
+    typed_instruction E L [p1 ◁ ty1; p2 ◁ ty2]
+               (p1 <⋯{i} !{ty.(ty_size)}p2) (λ _, [p1 ◁ ty1'; p2 ◁ ty2']%TC).
+  Proof.
+    iIntros (?? Hty Hw Hr ??) "#HEAP #LFT Htl [HE1 HE2] [HL1 HL2] Hp".
+    rewrite tctx_interp_cons tctx_interp_singleton.
+    iDestruct "Hp" as "[Hp1 Hp2]". wp_bind p1. iApply (wp_hasty with "Hp1").
+    iIntros (v1 Hv1) "Hty1".
+    iMod (Hw with "LFT HE1 HL1 Hty1") as (l1 vl1) "(H & H↦ & Hw)"=>//=.
+    destruct vl1 as [|? vl1]; iDestruct "H" as %[[= Hlen] ->].
+    rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[H↦0 H↦vl1]". wp_write.
+    iApply wp_seq. done. iNext. wp_bind p1.
+    iApply (wp_wand with "[]"); first by iApply (wp_eval_path). iIntros (? ->).
+    wp_op. wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2 Hv2) "Hty2".
+    iMod (Hr with "LFT Htl HE2 HL2 Hty2") as (l2 vl2 q) "(% & H↦2 & Hty & Hr)"=>//=. subst.
+    assert (ty.(ty_size) ≤ length vl1).
+    { revert i Hty. rewrite Hlen. clear. induction tyl=>//= -[|i] /=.
+      - intros [= ->]. lia.
+      - specialize (IHtyl i). intuition lia. }
+    rewrite -(take_drop (ty.(ty_size)) vl1) heap_mapsto_vec_app.
+    iDestruct "H↦vl1" as "[H↦vl1 H↦pad]".
+    iAssert (▷ ⌜length vl2 = ty.(ty_size)⌝)%I with "[#]" as ">%". by rewrite -ty_size_eq.
+    iApply wp_fupd. iApply (wp_memcpy with "[$HEAP $H↦vl1 $H↦2]"); try done.
+    { rewrite take_length. lia. }
+    iNext; iIntros "[H↦vl1 H↦2]".
+    rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //.
+    iMod ("Hr" with "H↦2") as "($ & $ & $ & $)". iApply "Hw". iNext.
+    rewrite split_sum_mt /is_pad. iExists i. rewrite nth_lookup Hty. iFrame.
+    iSplitL "H↦pad".
+    - rewrite (shift_loc_assoc_nat _ 1) take_length Nat.min_l; last lia.
+      iExists _. iFrame. rewrite /= drop_length. iPureIntro. lia.
+    - iExists _. iFrame.
+  Qed.
 End case.
\ No newline at end of file
-- 
GitLab