From 196cf83ed48b462eba6b000aed2a1f3592c2f797 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 24 Apr 2017 15:22:57 +0200
Subject: [PATCH] notice some type properties that still need proving
---
theories/typing/lib/mutex/mutex.v | 2 ++
theories/typing/lib/mutex/mutexguard.v | 3 +++
theories/typing/lib/rwlock/rwlockreadguard.v | 2 ++
theories/typing/lib/rwlock/rwlockwriteguard.v | 2 ++
4 files changed, 9 insertions(+)
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index a5c20914..f6c4e359 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -87,6 +87,8 @@ Section mutex.
Global Instance mutex_wf ty `{!TyWf ty} : TyWf (mutex ty) :=
{ ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+ (* TODO: Non-expansiveness, compat with eqtype, Send+Sync if ty is Send. *)
+
End mutex.
Section code.
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index d602d839..0a04209e 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -79,6 +79,9 @@ Section mguard.
Global Instance mutexguard_wf α ty `{!TyWf ty} : TyWf (mutexguard α ty) :=
{ ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) α }.
+ (* TODO: Contractivity, compat with lft_incl and eqtype.
+ MutexGuard is Sync if T is Send. *)
+
End mguard.
Section code.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 3f44a88e..e21b832d 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -112,6 +112,8 @@ Section rwlockreadguard.
lctx_lft_eq E L α1 α2 → eqtype E L ty1 ty2 →
eqtype E L (rwlockreadguard α1 ty1) (rwlockreadguard α2 ty2).
Proof. intros. by eapply rwlockreadguard_proper. Qed.
+
+ (* TODO: In Rust, the read guard is Sync if ty is Send+Sync. *)
End rwlockreadguard.
Hint Resolve rwlockreadguard_mono' rwlockreadguard_proper' : lrust_typing.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index 9da6cf50..40002208 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -115,6 +115,8 @@ Section rwlockwriteguard.
lctx_lft_eq E L α1 α2 → eqtype E L ty1 ty2 →
eqtype E L (rwlockwriteguard α1 ty1) (rwlockwriteguard α2 ty2).
Proof. intros. by eapply rwlockwriteguard_proper. Qed.
+
+ (* TODO: In Rust, the read guard is Sync if ty is Send+Sync. *)
End rwlockwriteguard.
Hint Resolve rwlockwriteguard_mono' rwlockwriteguard_proper' : lrust_typing.
--
GitLab