From 934ad6580cebee0f1366adf77be82eb21bc13e04 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 19 Apr 2017 18:52:42 +0200
Subject: [PATCH] WF
---
theories/typing/lib/mutex/mutex.v | 4 ++++
theories/typing/lib/mutex/mutexguard.v | 4 ++++
theories/typing/lib/rwlock/rwlock.v | 2 +-
3 files changed, 9 insertions(+), 1 deletion(-)
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index 1030c872..23fb26f0 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -83,4 +83,8 @@ Section mutex.
iExists _, _. iSplit; first by iApply shr_bor_shorten.
iApply lft_incl_trans; done.
Qed.
+
+ Global Instance mutex_wf ty `{!TyWf ty} : TyWf (mutex ty) :=
+ { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+
End mutex.
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index d9c15568..034ed18c 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -75,4 +75,8 @@ Section mguard.
iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
iApply ty_shr_mono; try done. iApply lft_intersect_mono. iApply lft_incl_refl. done.
Qed.
+
+ Global Instance mutexguard_wf α ty `{!TyWf ty} : TyWf (mutexguard α ty) :=
+ { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) α }.
+
End mguard.
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index db17b3e5..a75c30b7 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -149,7 +149,7 @@ Section rwlock.
iExists _, _. iFrame. iApply lft_incl_trans; auto.
Qed.
- Global Instance join_handle_wf ty `{!TyWf ty} : TyWf (rwlock ty) :=
+ Global Instance rwlock_wf ty `{!TyWf ty} : TyWf (rwlock ty) :=
{ ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
Global Instance rwlock_type_ne : TypeNonExpansive rwlock.
--
GitLab