From 505d86a5fbb85abd4e5fada1853136ac690a60bf Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 20 May 2018 16:57:47 +0200
Subject: [PATCH] show save conversion from &mut T to &mut Cell<T>

---
 theories/typing/lib/cell.v | 24 ++++++++++++++++++++----
 1 file changed, 20 insertions(+), 4 deletions(-)

diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 025d2ef1..4c5145d0 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -82,6 +82,8 @@ End cell.
 Section typing.
   Context `{typeG Σ}.
 
+  (** The next couple functions essentially show owned-type equalities, as they
+      are all different types for the identity function. *)
   (* Constructing a cell. *)
   Definition cell_new : val := funrec: <> ["x"] := return: ["x"].
 
@@ -118,7 +120,20 @@ Section typing.
     by iIntros "$".
   Qed.
 
-  (* Reading from a cell *)
+  Definition cell_from_mut : val :=
+    funrec: <> ["x"] := return: ["x"].
+
+  Lemma cell_from_mut_type ty `{!TyWf ty} :
+    typed_val cell_get_mut (fn(∀ α, ∅; &uniq{α} ty) → &uniq{α} (cell ty)).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    iApply type_jump; [solve_typing..|]. rewrite /tctx_incl /=.
+    iIntros (??) "_ _ $". rewrite !tctx_interp_singleton /tctx_elt_interp /=.
+    by iIntros "$".
+  Qed.
+
+  (** Reading from a cell *)
   Definition cell_get ty : val :=
     funrec: <> ["x"] :=
       let: "x'" := !"x" in
@@ -137,7 +152,7 @@ Section typing.
     iApply type_jump; solve_typing.
   Qed.
 
-  (* Writing to a cell *)
+  (** Writing to a cell *)
   Definition cell_replace ty : val :=
     funrec: <> ["c"; "x"] :=
       let: "c'" := !"c" in
@@ -189,8 +204,9 @@ Section typing.
     iApply type_jump; solve_typing.
   Qed.
 
-  (* Create a shared cell from a mutable borrow.
-     Called alias::one in Rust. *)
+  (** Create a shared cell from a mutable borrow.
+      Called alias::one in Rust.
+      This is really just [cell_from_mut] followed by sharing. *)
   Definition fake_shared_cell : val :=
     funrec: <> ["x"] :=
       let: "x'" := !"x" in
-- 
GitLab