diff --git a/theories/typing/function.v b/theories/typing/function.v index a71f505dd52b30807ddc2eb648039ed71c695bca..4e9a4f4c3ad46fd9bf119969bb3dab3dbed4112a 100644 --- a/theories/typing/function.v +++ b/theories/typing/function.v @@ -9,7 +9,7 @@ Section fn. Record fn_params := FP { fp_E : lft → elctx; fp_tys : vec type n; fp_ty : type }. - Definition FP_wf E (tys : vec type n) `{!TyWfLst tys} ty `{!TyWf ty} := + Definition FP_wf E (tys : vec type n) `{!ListTyWf tys} ty `{!TyWf ty} := FP (λ Ï, E Ï ++ tyl_wf_E tys ++ tyl_outlives_E tys Ï ++ ty.(ty_wf_E) ++ ty_outlives_E ty Ï) tys ty. diff --git a/theories/typing/product.v b/theories/typing/product.v index 59ef61916831c436c6f9e15654f389498a1d9539..90f273cd3e1cae6a776ddab8682c2ca5989d68ea 100644 --- a/theories/typing/product.v +++ b/theories/typing/product.v @@ -156,7 +156,7 @@ Section product. Definition product := foldr product2 unit0. Definition unit := product []. - Global Instance product_wf tyl `{!TyWfLst tyl} : TyWf (product tyl) := + Global Instance product_wf tyl `{!ListTyWf tyl} : TyWf (product tyl) := { ty_lfts := tyl_lfts tyl; ty_wf_E := tyl_wf_E tyl }. Lemma outlives_product ty1 ty2 Ï `{!TyWf ty1, !TyWf ty2} : @@ -179,11 +179,11 @@ Section product. Lemma product_proper' E L tyl1 tyl2 : Forall2 (eqtype E L) tyl1 tyl2 → eqtype E L (product tyl1) (product tyl2). Proof. apply product_proper. Qed. - Global Instance product_copy tys : LstCopy tys → Copy (product tys). + Global Instance product_copy tys : ListCopy tys → Copy (product tys). Proof. induction 1; apply _. Qed. - Global Instance product_send tys : LstSend tys → Send (product tys). + Global Instance product_send tys : ListSend tys → Send (product tys). Proof. induction 1; apply _. Qed. - Global Instance product_sync tys : LstSync tys → Sync (product tys). + Global Instance product_sync tys : ListSync tys → Sync (product tys). Proof. induction 1; apply _. Qed. Definition product_cons ty tyl : @@ -252,7 +252,7 @@ Section typing. eqtype E L (Î [Î tyl1; Î tyl2]) (Î (tyl1 ++ tyl2)). Proof. by rewrite -prod_flatten_r -prod_flatten_l. Qed. - Lemma ty_outlives_E_elctx_sat_product E L tyl {Wf : TyWfLst tyl} α: + Lemma ty_outlives_E_elctx_sat_product E L tyl {Wf : ListTyWf tyl} α: elctx_sat E L (tyl_outlives_E tyl α) → elctx_sat E L (ty_outlives_E (Î tyl) α). Proof. diff --git a/theories/typing/sum.v b/theories/typing/sum.v index 991d199f4f4f5e155b6eed72b6aed85e2bd83465..e68edb4fa5318d43e957519dd836bfef7a416ff4 100644 --- a/theories/typing/sum.v +++ b/theories/typing/sum.v @@ -84,7 +84,7 @@ Section sum. - iApply ((nth i tyl emp0).(ty_shr_mono) with "Hord"); done. Qed. - Global Instance sum_wf tyl `{!TyWfLst tyl} : TyWf (sum tyl) := + Global Instance sum_wf tyl `{!ListTyWf tyl} : TyWf (sum tyl) := { ty_lfts := tyl_lfts tyl; ty_wf_E := tyl_wf_E tyl }. Global Instance sum_type_ne n : Proper (Forall2 (type_dist2 n) ==> type_dist2 n) sum. @@ -174,7 +174,7 @@ Section sum. nth i [] d = d. Proof. by destruct i. Qed. - Global Instance sum_copy tyl : LstCopy tyl → Copy (sum tyl). + Global Instance sum_copy tyl : ListCopy tyl → Copy (sum tyl). Proof. intros HFA. split. - intros tid vl. @@ -215,7 +215,7 @@ Section sum. iMod ("Hclose" with "[$Hown1 $Hown2]") as "$". by iFrame. Qed. - Global Instance sum_send tyl : LstSend tyl → Send (sum tyl). + Global Instance sum_send tyl : ListSend tyl → Send (sum tyl). Proof. iIntros (Hsend tid1 tid2 vl) "H". iDestruct "H" as (i vl' vl'') "(% & % & Hown)". iExists _, _, _. iSplit; first done. iSplit; first done. iApply @send_change_tid; last done. @@ -223,7 +223,7 @@ Section sum. iIntros (???) "[]". Qed. - Global Instance sum_sync tyl : LstSync tyl → Sync (sum tyl). + Global Instance sum_sync tyl : ListSync tyl → Sync (sum tyl). Proof. iIntros (Hsync κ tid1 tid2 l) "H". iDestruct "H" as (i) "[Hframe Hown]". iExists _. iFrame "Hframe". iApply @sync_change_tid; last done. diff --git a/theories/typing/type.v b/theories/typing/type.v index 926b38e706529d7cd18c274213c4523cdf6dfbc3..a3d4977e61b9b56cbecf1d25b16f528a4e4d7084 100644 --- a/theories/typing/type.v +++ b/theories/typing/type.v @@ -73,34 +73,34 @@ Proof. Qed. (* Lift TyWf to lists. We cannot use `Forall` because that one is restricted to Prop. *) -Inductive TyWfLst `{!typeG Σ} : list type → Type := -| tyl_wf_nil : TyWfLst [] -| tyl_wf_cons ty tyl `{!TyWf ty, !TyWfLst tyl} : TyWfLst (ty::tyl). -Existing Class TyWfLst. -Existing Instances tyl_wf_nil tyl_wf_cons. +Inductive ListTyWf `{!typeG Σ} : list type → Type := +| list_ty_wf_nil : ListTyWf [] +| list_ty_wf_cons ty tyl `{!TyWf ty, !ListTyWf tyl} : ListTyWf (ty::tyl). +Existing Class ListTyWf. +Existing Instances list_ty_wf_nil list_ty_wf_cons. -Fixpoint tyl_lfts `{!typeG Σ} tyl {WF : TyWfLst tyl} : list lft := +Fixpoint tyl_lfts `{!typeG Σ} tyl {WF : ListTyWf tyl} : list lft := match WF with - | tyl_wf_nil => [] - | tyl_wf_cons ty [] => ty.(ty_lfts) - | tyl_wf_cons ty tyl => ty.(ty_lfts) ++ tyl.(tyl_lfts) + | list_ty_wf_nil => [] + | list_ty_wf_cons ty [] => ty.(ty_lfts) + | list_ty_wf_cons ty tyl => ty.(ty_lfts) ++ tyl.(tyl_lfts) end. -Fixpoint tyl_wf_E `{!typeG Σ} tyl {WF : TyWfLst tyl} : elctx := +Fixpoint tyl_wf_E `{!typeG Σ} tyl {WF : ListTyWf tyl} : elctx := match WF with - | tyl_wf_nil => [] - | tyl_wf_cons ty [] => ty.(ty_wf_E) - | tyl_wf_cons ty tyl => ty.(ty_wf_E) ++ tyl.(tyl_wf_E) + | list_ty_wf_nil => [] + | list_ty_wf_cons ty [] => ty.(ty_wf_E) + | list_ty_wf_cons ty tyl => ty.(ty_wf_E) ++ tyl.(tyl_wf_E) end. -Fixpoint tyl_outlives_E `{!typeG Σ} tyl {WF : TyWfLst tyl} (κ : lft) : elctx := +Fixpoint tyl_outlives_E `{!typeG Σ} tyl {WF : ListTyWf tyl} (κ : lft) : elctx := match WF with - | tyl_wf_nil => [] - | tyl_wf_cons ty [] => ty_outlives_E ty κ - | tyl_wf_cons ty tyl => ty_outlives_E ty κ ++ tyl.(tyl_outlives_E) κ + | list_ty_wf_nil => [] + | list_ty_wf_cons ty [] => ty_outlives_E ty κ + | list_ty_wf_cons ty tyl => ty_outlives_E ty κ ++ tyl.(tyl_outlives_E) κ end. -Lemma tyl_outlives_E_elctx_sat `{!typeG Σ} E L tyl {WF : TyWfLst tyl} α β : +Lemma tyl_outlives_E_elctx_sat `{!typeG Σ} E L tyl {WF : ListTyWf tyl} α β : tyl_outlives_E tyl β ⊆+ E → lctx_lft_incl E L α β → elctx_sat E L (tyl_outlives_E tyl α). @@ -402,31 +402,31 @@ Class Copy `{!typeG Σ} (t : type) := { Existing Instances copy_persistent. Instance: Params (@Copy) 2 := {}. -Class LstCopy `{!typeG Σ} (tys : list type) := lst_copy : Forall Copy tys. -Instance: Params (@LstCopy) 2 := {}. -Global Instance lst_copy_nil `{!typeG Σ} : LstCopy [] := List.Forall_nil _. +Class ListCopy `{!typeG Σ} (tys : list type) := lst_copy : Forall Copy tys. +Instance: Params (@ListCopy) 2 := {}. +Global Instance lst_copy_nil `{!typeG Σ} : ListCopy [] := List.Forall_nil _. Global Instance lst_copy_cons `{!typeG Σ} ty tys : - Copy ty → LstCopy tys → LstCopy (ty :: tys) := List.Forall_cons _ _ _. + Copy ty → ListCopy tys → ListCopy (ty :: tys) := List.Forall_cons _ _ _. Class Send `{!typeG Σ} (t : type) := send_change_tid tid1 tid2 vl : t.(ty_own) tid1 vl -∗ t.(ty_own) tid2 vl. Instance: Params (@Send) 2 := {}. -Class LstSend `{!typeG Σ} (tys : list type) := lst_send : Forall Send tys. -Instance: Params (@LstSend) 2 := {}. -Global Instance lst_send_nil `{!typeG Σ} : LstSend [] := List.Forall_nil _. +Class ListSend `{!typeG Σ} (tys : list type) := lst_send : Forall Send tys. +Instance: Params (@ListSend) 2 := {}. +Global Instance lst_send_nil `{!typeG Σ} : ListSend [] := List.Forall_nil _. Global Instance lst_send_cons `{!typeG Σ} ty tys : - Send ty → LstSend tys → LstSend (ty :: tys) := List.Forall_cons _ _ _. + Send ty → ListSend tys → ListSend (ty :: tys) := List.Forall_cons _ _ _. Class Sync `{!typeG Σ} (t : type) := sync_change_tid κ tid1 tid2 l : t.(ty_shr) κ tid1 l -∗ t.(ty_shr) κ tid2 l. Instance: Params (@Sync) 2 := {}. -Class LstSync `{!typeG Σ} (tys : list type) := lst_sync : Forall Sync tys. -Instance: Params (@LstSync) 2 := {}. -Global Instance lst_sync_nil `{!typeG Σ} : LstSync [] := List.Forall_nil _. +Class ListSync `{!typeG Σ} (tys : list type) := lst_sync : Forall Sync tys. +Instance: Params (@ListSync) 2 := {}. +Global Instance lst_sync_nil `{!typeG Σ} : ListSync [] := List.Forall_nil _. Global Instance lst_sync_cons `{!typeG Σ} ty tys : - Sync ty → LstSync tys → LstSync (ty :: tys) := List.Forall_cons _ _ _. + Sync ty → ListSync tys → ListSync (ty :: tys) := List.Forall_cons _ _ _. Section type. Context `{!typeG Σ}. diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v index 9c4f033e24026c6dac4ea1059e4c2dcb604a2d59..5e3dedaf1260220904cb5ea19929e913b1418db4 100644 --- a/theories/typing/type_sum.v +++ b/theories/typing/type_sum.v @@ -285,7 +285,7 @@ Section case. by iApply type_seq; [eapply type_sum_memcpy_instr, Hr|done|done]. Qed. - Lemma ty_outlives_E_elctx_sat_sum E L tyl {Wf : TyWfLst tyl} α: + Lemma ty_outlives_E_elctx_sat_sum E L tyl {Wf : ListTyWf tyl} α: elctx_sat E L (tyl_outlives_E tyl α) → elctx_sat E L (ty_outlives_E (sum tyl) α). Proof.