From 7f20c4712dd6d2e560c1c83e1cc13d891d9179c6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 21 Feb 2017 15:38:12 +0100
Subject: [PATCH] RefCell: add comments explaining the data layout

---
 theories/typing/unsafe/refcell/ref.v         |  8 ++++++++
 theories/typing/unsafe/refcell/refcell.v     |  7 +++++++
 theories/typing/unsafe/refcell/refmut.v      | 10 ++++++++++
 theories/typing/unsafe/refcell/refmut_code.v |  2 +-
 4 files changed, 26 insertions(+), 1 deletion(-)

diff --git a/theories/typing/unsafe/refcell/ref.v b/theories/typing/unsafe/refcell/ref.v
index 9e9f8c0a..0d8000a6 100644
--- a/theories/typing/unsafe/refcell/ref.v
+++ b/theories/typing/unsafe/refcell/ref.v
@@ -11,6 +11,14 @@ Definition refcell_refN := refcellN .@ "ref".
 Section ref.
   Context `{typeG Σ, refcellG Σ}.
 
+  (* The Rust type looks as follows (after some unfolding):
+
+     pub struct Ref<'b, T: ?Sized + 'b> {
+       value: &'b T,
+       borrow: &'b Cell<BorrowFlag>,
+     }
+  *)
+
   Program Definition ref (α : lft) (ty : type) :=
     {| ty_size := 2;
        ty_own tid vl :=
diff --git a/theories/typing/unsafe/refcell/refcell.v b/theories/typing/unsafe/refcell/refcell.v
index 0eb1bb4d..1f30af14 100644
--- a/theories/typing/unsafe/refcell/refcell.v
+++ b/theories/typing/unsafe/refcell/refcell.v
@@ -83,6 +83,13 @@ End refcell_inv.
 Section refcell.
   Context `{typeG Σ, refcellG Σ}.
 
+  (* Original Rust type:
+     pub struct RefCell<T: ?Sized> {
+       borrow: Cell<BorrowFlag>,
+       value: UnsafeCell<T>,
+     }
+  *)
+
   Program Definition refcell (ty : type) :=
     {| ty_size := S ty.(ty_size);
        ty_own tid vl :=
diff --git a/theories/typing/unsafe/refcell/refmut.v b/theories/typing/unsafe/refcell/refmut.v
index 36a86ad3..df19723e 100644
--- a/theories/typing/unsafe/refcell/refmut.v
+++ b/theories/typing/unsafe/refcell/refmut.v
@@ -9,6 +9,16 @@ Set Default Proof Using "Type".
 Section refmut.
   Context `{typeG Σ, refcellG Σ}.
 
+  (* The Rust type looks as follows (after some unfolding):
+
+     pub struct RefMut<'b, T: ?Sized + 'b> {
+       value: &'b mut T,
+       borrow: &'b Cell<BorrowFlag>,
+     }
+
+     In other words, we have a pointer to the data, and a pointer
+     to the refcount field of the RefCell. *)
+
   Program Definition refmut (α : lft) (ty : type) :=
     {| ty_size := 2;
        ty_own tid vl :=
diff --git a/theories/typing/unsafe/refcell/refmut_code.v b/theories/typing/unsafe/refcell/refmut_code.v
index 61efe2a7..3b67b964 100644
--- a/theories/typing/unsafe/refcell/refmut_code.v
+++ b/theories/typing/unsafe/refcell/refmut_code.v
@@ -173,7 +173,7 @@ Section refmut_functions.
   Lemma refmut_map_type ty1 ty2 envty E :
     typed_instruction_ty [] [] [] refmut_map
       (fn(∀ β, [☀β] ++ E; refmut β ty1,
-                          fn(∀ α, [☀α] ++ E; envty, &uniq{α}ty1) → &uniq{α}ty2,
+                          fn(∀ α, [☀α] ++ E; envty, &uniq{α} ty1) → &uniq{α} ty2,
                           envty)
        → refmut β ty2).
   Proof.
-- 
GitLab