From 53d600fc0bd675987928fc60bcd5eea6977ebb2e Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jjourdan@mpi-sws.org>
Date: Mon, 6 Mar 2017 18:16:29 +0100
Subject: [PATCH] Notation FP' as a wrapper for FP, so that the arguments are
in the right order.
---
theories/typing/function.v | 14 ++++++++++----
theories/typing/lib/fake_shared_box.v | 4 ++--
theories/typing/lib/refcell/ref_code.v | 4 ++--
theories/typing/lib/refcell/refmut_code.v | 8 ++++----
theories/typing/lib/rwlock/rwlockreadguard_code.v | 4 ++--
theories/typing/lib/rwlock/rwlockwriteguard_code.v | 10 ++++------
theories/typing/lib/spawn.v | 2 +-
7 files changed, 25 insertions(+), 21 deletions(-)
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 9f9b9bcb..b09e8af1 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -98,6 +98,12 @@ End fn.
Arguments fn_params {_ _} _.
+(* The parameter of [FP] are in the wrong order in order to make sure
+ that type-checking is done in that order, so that the [ELCtx_Alive]
+ is taken as a coercion. We reestablish the intuitive order with
+ [FP'] *)
+Notation FP' E tys ty := (FP tys ty E).
+
(* We use recursive notation for binders as well, to allow patterns
like '(a, b) to be used. In practice, only one binder is ever used,
but using recursive binders is the only way to make Coq accept
@@ -106,19 +112,19 @@ Arguments fn_params {_ _} _.
printing. Once on 8.6pl1, this should work. *)
Notation "'fn(∀' x .. x' ',' E ';' T1 ',' .. ',' TN ')' '→' R" :=
(fn (λ x, (.. (λ x',
- FP (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..)%T R%T E%EL)..)))
+ FP' E%EL (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..)%T R%T)..)))
(at level 99, R at level 200, x binder, x' binder,
format "'fn(∀' x .. x' ',' E ';' T1 ',' .. ',' TN ')' '→' R") : lrust_type_scope.
Notation "'fn(∀' x .. x' ',' E ')' '→' R" :=
- (fn (λ x, (.. (λ x', FP Vector.nil R%T E%EL)..)))
+ (fn (λ x, (.. (λ x', FP' E%EL Vector.nil R%T)..)))
(at level 99, R at level 200, x binder, x' binder,
format "'fn(∀' x .. x' ',' E ')' '→' R") : lrust_type_scope.
Notation "'fn(' E ';' T1 ',' .. ',' TN ')' '→' R" :=
- (fn (λ _:(), FP (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..) R%T E%EL) )
+ (fn (λ _:(), FP' E%EL (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..) R%T))
(at level 99, R at level 200,
format "'fn(' E ';' T1 ',' .. ',' TN ')' '→' R") : lrust_type_scope.
Notation "'fn(' E ')' '→' R" :=
- (fn (λ _:(), FP Vector.nil R%T E%EL))
+ (fn (λ _:(), FP' E%EL Vector.nil R%T))
(at level 99, R at level 200,
format "'fn(' E ')' '→' R") : lrust_type_scope.
diff --git a/theories/typing/lib/fake_shared_box.v b/theories/typing/lib/fake_shared_box.v
index 0d18dc23..b0dc67a5 100644
--- a/theories/typing/lib/fake_shared_box.v
+++ b/theories/typing/lib/fake_shared_box.v
@@ -11,8 +11,8 @@ Section fake_shared_box.
Lemma cell_replace_type ty :
typed_val fake_shared_box
- (fn (fun '(α, β) => FP [# &shr{α}(&shr{β} ty)]
- (&shr{α}box ty) [α; β; α ⊑ β]%EL)).
+ (fn (fun '(α, β) => FP' [α; β; α ⊑ β]%EL
+ [# &shr{α}(&shr{β} ty)] (&shr{α}box ty))).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index fd406c49..c1012db9 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -56,7 +56,7 @@ Section ref_functions.
See: https://coq.inria.fr/bugs/show_bug.cgi?id=5326 *)
Lemma ref_clone_type ty :
typed_val ref_clone
- (fn (fun '(α, β) => FP [# &shr{α}(ref β ty)]%T (ref β ty)%T [α; β]%EL)).
+ (fn (fun '(α, β) => FP' [α; β]%EL [# &shr{α}(ref β ty)]%T (ref β ty)%T)).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
@@ -116,7 +116,7 @@ Section ref_functions.
Lemma ref_deref_type ty :
typed_val ref_deref
- (fn (fun '(α, β) => FP [# &shr{α}(ref β ty)]%T (&shr{α}ty)%T [α; β; α ⊑ β]%EL)).
+ (fn (fun '(α, β) => FP' [α; β; α ⊑ β]%EL [# &shr{α}(ref β ty)]%T (&shr{α}ty)%T)).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 07088ab1..8c6fd235 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -20,7 +20,7 @@ Section refmut_functions.
Lemma refmut_deref_type ty :
typed_val refmut_deref
- (fn (fun '(α, β) => FP [# &shr{α}(refmut β ty)]%T (&shr{α}ty) [α; β; α ⊑ β]%EL)).
+ (fn (fun '(α, β) => FP' [α; β; α ⊑ β]%EL [# &shr{α}(refmut β ty)]%T (&shr{α}ty))).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
@@ -60,9 +60,9 @@ Section refmut_functions.
Lemma refmut_derefmut_type ty :
typed_val refmut_derefmut
- (fn (fun '(α, β) => FP [# &uniq{α}(refmut β ty)]%T
- (&uniq{α}ty)%T [α; β; α ⊑ β]%EL)).
- Proof.
+ (fn (fun '(α, β) => FP' [α; β; α ⊑ β]%EL [# &uniq{α}(refmut β ty)]%T
+ (&uniq{α}ty)%T)).
+ Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (x').
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index d76e2b77..c2eaab67 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -20,8 +20,8 @@ Section rwlockreadguard_functions.
Lemma rwlockreadguard_deref_type ty :
typed_val rwlockreadguard_deref
- (fn (fun '(α, β) => FP [# &shr{α}(rwlockreadguard β ty)]
- (&shr{α}ty) [α; β; α ⊑ β]%EL)).
+ (fn (fun '(α, β) => FP' [α; β; α ⊑ β]%EL
+ [# &shr{α}(rwlockreadguard β ty)] (&shr{α}ty))).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index 3e3d4ee0..0ebe2612 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -20,9 +20,8 @@ Section rwlockwriteguard_functions.
Lemma rwlockwriteguard_deref_type ty :
typed_val rwlockwriteguard_deref
- (fn (fun '(α, β) => FP [# &shr{α}(rwlockwriteguard β ty)]
- (&shr{α}ty)
- [α; β; α ⊑ β]%EL)).
+ (fn (fun '(α, β) => FP' [α; β; α ⊑ β]%EL
+ [# &shr{α}(rwlockwriteguard β ty)] (&shr{α}ty))).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
@@ -63,9 +62,8 @@ Section rwlockwriteguard_functions.
Lemma rwlockwriteguard_derefmut_type ty :
typed_val rwlockwriteguard_derefmut
- (fn (fun '(α, β) => FP [# &uniq{α}(rwlockwriteguard β ty)]
- (&uniq{α}ty)
- [α; β; α ⊑ β]%EL)).
+ (fn (fun '(α, β) => FP' [α; β; α ⊑ β]%EL
+ [# &uniq{α}(rwlockwriteguard β ty)] (&uniq{α}ty))).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index 45cf25e5..e19b166b 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -84,7 +84,7 @@ Section spawn.
iIntros "?". iExists retty. iFrame. iApply type_incl_refl. }
iIntros (c) "Hfin". iMod na_alloc as (tid') "Htl". wp_let. wp_let.
(* FIXME this is horrible. *)
- assert (Hcall := type_call' [] [] [] f' [env:expr] (λ _:(), FP [# envty] retty [])).
+ assert (Hcall := type_call' [] [] [] f' [env:expr] (λ _:(), FP' [] [# envty] retty)).
specialize (Hcall (rec: "_k" ["r"] := finish [ #c; "r"])%V ()).
erewrite of_val_unlock in Hcall; last done.
iApply (Hcall $! _ 1%Qp with "LFT Htl [] [] [Hfin]").
--
GitLab