From cde2f2625b3cf859bd3de8de50744073f4e872f5 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 9 Mar 2017 13:35:28 +0100
Subject: [PATCH] introduce notation for the magic return variable name
---
theories/lang/notation.v | 3 ++-
theories/typing/examples/init_prod.v | 2 +-
theories/typing/lib/cell.v | 10 +++++-----
theories/typing/lib/fake_shared_box.v | 2 +-
theories/typing/lib/option.v | 6 +++---
theories/typing/lib/rc.v | 4 ++--
theories/typing/lib/refcell/ref_code.v | 8 ++++----
theories/typing/lib/refcell/refcell_code.v | 10 +++++-----
theories/typing/lib/refcell/refmut_code.v | 8 ++++----
theories/typing/lib/rwlock/rwlock_code.v | 10 +++++-----
theories/typing/lib/rwlock/rwlockreadguard_code.v | 4 ++--
theories/typing/lib/rwlock/rwlockwriteguard_code.v | 6 +++---
theories/typing/lib/spawn.v | 4 ++--
13 files changed, 39 insertions(+), 38 deletions(-)
diff --git a/theories/lang/notation.v b/theories/lang/notation.v
index bfe0a862..e06e8827 100644
--- a/theories/lang/notation.v
+++ b/theories/lang/notation.v
@@ -60,11 +60,12 @@ Notation "λ: xl , e" := (Lam xl%RustB e%E)
(at level 102, xl at level 1, e at level 200) : expr_scope.
Notation "λ: xl , e" := (locked (LamV xl%RustB e%E))
(at level 102, xl at level 1, e at level 200) : val_scope.
-(* RJ TODO: let the user pick the name of the return continuation. *)
+
Notation "'funrec:' f xl := e" := (rec: f ("return"::xl) := e)%E
(only parsing, at level 102, f, xl at level 1, e at level 200) : expr_scope.
Notation "'funrec:' f xl := e" := (rec: f ("return"::xl) := e)%V
(only parsing, at level 102, f, xl at level 1, e at level 200) : val_scope.
+Notation "'return:'" := "return" : expr_scope.
Notation "'let:' x := e1 'in' e2" :=
((Lam (@cons binder x%RustB nil) e2%E) (@cons expr e1%E nil))
diff --git a/theories/typing/examples/init_prod.v b/theories/typing/examples/init_prod.v
index be375087..b7da2ea5 100644
--- a/theories/typing/examples/init_prod.v
+++ b/theories/typing/examples/init_prod.v
@@ -10,7 +10,7 @@ Section init_prod.
let: "x'" := !"x" in let: "y'" := !"y" in
let: "r" := new [ #2] in
"r" +â‚— #0 <- "x'";; "r" +â‚— #1 <- "y'";;
- delete [ #1; "x"] ;; delete [ #1; "y"] ;; "return" ["r"].
+ delete [ #1; "x"] ;; delete [ #1; "y"] ;; return: ["r"].
Lemma init_prod_type :
typed_val init_prod (fn([]; int, int) → Π[int;int]).
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index bfbe7e4a..6a729cc5 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -82,7 +82,7 @@ Section typing.
Arguments ty_own : simpl never.
(* Constructing a cell. *)
- Definition cell_new : val := funrec: <> ["x"] := "return" ["x"].
+ Definition cell_new : val := funrec: <> ["x"] := return: ["x"].
Lemma cell_new_type ty :
typed_val cell_new (fn([]; ty) → cell ty).
@@ -94,7 +94,7 @@ Section typing.
Qed.
(* The other direction: getting ownership out of a cell. *)
- Definition cell_into_inner : val := funrec: <> ["x"] := "return" ["x"].
+ Definition cell_into_inner : val := funrec: <> ["x"] := return: ["x"].
Lemma cell_into_inner_type ty :
typed_val cell_into_inner (fn([]; cell ty) → ty).
@@ -106,7 +106,7 @@ Section typing.
Qed.
Definition cell_get_mut : val :=
- funrec: <> ["x"] := "return" ["x"].
+ funrec: <> ["x"] := return: ["x"].
Lemma cell_get_mut_type ty :
typed_val cell_get_mut (fn(∀ α, [α]; &uniq{α} (cell ty)) → &uniq{α} ty).
@@ -123,7 +123,7 @@ Section typing.
funrec: <> ["x"] :=
let: "x'" := !"x" in
letalloc: "r" <-{ty.(ty_size)} !"x'" in
- delete [ #1; "x"];; "return" ["r"].
+ delete [ #1; "x"];; return: ["r"].
Lemma cell_get_type `(!Copy ty) :
typed_val (cell_get ty) (fn(∀ α, [α]; &shr{α} (cell ty)) → ty).
@@ -143,7 +143,7 @@ Section typing.
let: "c'" := !"c" in
letalloc: "r" <-{ty.(ty_size)} !"c'" in
"c'" <-{ty.(ty_size)} !"x";;
- delete [ #1; "c"] ;; delete [ #ty.(ty_size); "x"] ;; "return" ["r"].
+ delete [ #1; "c"] ;; delete [ #ty.(ty_size); "x"] ;; return: ["r"].
Lemma cell_replace_type ty :
typed_val (cell_replace ty) (fn(∀ α, [α]; &shr{α} cell ty, ty) → ty).
diff --git a/theories/typing/lib/fake_shared_box.v b/theories/typing/lib/fake_shared_box.v
index 82ef21c1..56d4d9db 100644
--- a/theories/typing/lib/fake_shared_box.v
+++ b/theories/typing/lib/fake_shared_box.v
@@ -7,7 +7,7 @@ Section fake_shared_box.
Context `{typeG Σ}.
Definition fake_shared_box : val :=
- funrec: <> ["x"] := Skip ;; "return" ["x"].
+ funrec: <> ["x"] := Skip ;; return: ["x"].
Lemma cell_replace_type ty :
typed_val fake_shared_box
diff --git a/theories/typing/lib/option.v b/theories/typing/lib/option.v
index 10e930a3..720310ac 100644
--- a/theories/typing/lib/option.v
+++ b/theories/typing/lib/option.v
@@ -15,7 +15,7 @@ Section option.
[ "r" <-{Σ 0} ();; "k" ["r"];
"r" <-{Σ 1} "o'" +ₗ #1;; "k" ["r"] ]
cont: "k" ["r"] :=
- delete [ #1; "o"];; "return" ["r"].
+ delete [ #1; "o"];; return: ["r"].
Lemma option_as_mut_type Ï„ :
typed_val
@@ -42,11 +42,11 @@ Section option.
funrec: <> ["o"; "def"] :=
case: !"o" of
[ delete [ #(S Ï„.(ty_size)); "o"];;
- "return" ["def"];
+ return: ["def"];
letalloc: "r" <-{Ï„.(ty_size)} !("o" +â‚— #1) in
delete [ #(S Ï„.(ty_size)); "o"];; delete [ #Ï„.(ty_size); "def"];;
- "return" ["r"]].
+ return: ["r"]].
Lemma option_unwrap_or_type Ï„ :
typed_val (option_unwrap_or τ) (fn([]; option τ, τ) → τ).
diff --git a/theories/typing/lib/rc.v b/theories/typing/lib/rc.v
index f037596d..f6b8962f 100644
--- a/theories/typing/lib/rc.v
+++ b/theories/typing/lib/rc.v
@@ -123,12 +123,12 @@ Section code.
Definition rc_new ty : val :=
funrec: <> ["x"] :=
- let: "rcbox" := new [ #(S ty.(ty_size))] in
+ let: "rcbox" := new [ #(S ty.(ty_size)) ] in
let: "rc" := new [ #1 ] in
"rcbox" +â‚— #0 <- #1;;
"rcbox" +â‚— #1 <-{ty.(ty_size)} !"x";;
"rc" +â‚— #0 <- "rcbox";;
- delete [ #ty.(ty_size) ; "x"];; "return" ["rc"].
+ delete [ #ty.(ty_size); "x"];; return: ["rc"].
Lemma rc_new_type ty :
typed_val (rc_new ty) (fn([]; ty) → rc ty).
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index e1575126..a7ee9b1f 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -50,7 +50,7 @@ Section ref_functions.
let: "n" := !"rc" in
"rc" <- "n" + #1;;
letalloc: "r" <-{2} !"x'" in
- delete [ #1; "x"];; "return" ["r"].
+ delete [ #1; "x"];; return: ["r"].
(* FIXME : using λ instead of fun triggers an anomaly.
See: https://coq.inria.fr/bugs/show_bug.cgi?id=5326 *)
@@ -112,7 +112,7 @@ Section ref_functions.
let: "x'" := !"x" in
let: "r'" := !"x'" in
letalloc: "r" <- "r'" in
- delete [ #1; "x"];; "return" ["r"].
+ delete [ #1; "x"];; return: ["r"].
Lemma ref_deref_type ty :
typed_val ref_deref
@@ -150,7 +150,7 @@ Section ref_functions.
"rc" <- "n" - #1;;
Endlft;;
delete [ #2; "x"];;
- let: "r" := new [ #0] in "return" ["r"].
+ let: "r" := new [ #0] in return: ["r"].
Lemma ref_drop_type ty :
typed_val ref_drop (fn(∀ α, [α]; ref α ty) → unit).
@@ -214,7 +214,7 @@ Section ref_functions.
"ref" <- "r'";;
delete [ #1; "f"];; "k" []
cont: "k" [] :=
- "return" ["ref"].
+ return: ["ref"].
Lemma ref_map_type ty1 ty2 envty E :
typed_val ref_map
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index 91f67707..c5b433be 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -17,7 +17,7 @@ Section refcell_functions.
let: "r" := new [ #(S ty.(ty_size))] in
"r" +â‚— #0 <- #0;;
"r" +â‚— #1 <-{ty.(ty_size)} !"x";;
- delete [ #ty.(ty_size) ; "x"];; "return" ["r"].
+ delete [ #ty.(ty_size) ; "x"];; return: ["r"].
Lemma refcell_new_type ty :
typed_val (refcell_new ty) (fn([]; ty) → refcell ty).
@@ -54,7 +54,7 @@ Section refcell_functions.
"r" <-{ty.(ty_size)} !("x" +â‚— #1);;
(* TODO RJ: Can we make it so that the parenthesis above are mandatory?
Leaving them away is inconsistent with `let ... := !"x" +â‚— #1`. *)
- delete [ #(S ty.(ty_size)) ; "x"];; "return" ["r"].
+ delete [ #(S ty.(ty_size)) ; "x"];; return: ["r"].
Lemma refcell_into_inner_type ty :
typed_val (refcell_into_inner ty) (fn([]; refcell ty) → ty).
@@ -88,7 +88,7 @@ Section refcell_functions.
funrec: <> ["x"] :=
let: "x'" := !"x" in
"x" <- "x'" +â‚— #1;;
- "return" ["x"].
+ return: ["x"].
Lemma refcell_get_mut_type ty :
typed_val refcell_get_mut (fn(∀ α, [α]; &uniq{α} (refcell ty)) → &uniq{α} ty)%T.
@@ -137,7 +137,7 @@ Section refcell_functions.
delete [ #2; "ref"];;
"k" ["r"]
cont: "k" ["r"] :=
- delete [ #1; "x"];; "return" ["r"].
+ delete [ #1; "x"];; return: ["r"].
Lemma refcell_try_borrow_type ty :
typed_val refcell_try_borrow (fn(∀ α, [α] ; &shr{α}(refcell ty)) → option (ref α ty)).
@@ -241,7 +241,7 @@ Section refcell_functions.
"r" <-{Σ 0} ();;
"k" ["r"]
cont: "k" ["r"] :=
- delete [ #1; "x"];; "return" ["r"].
+ delete [ #1; "x"];; return: ["r"].
Lemma refcell_try_borrow_mut_type ty :
typed_val refcell_try_borrow_mut
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index a9534a10..c5039c18 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -16,7 +16,7 @@ Section refmut_functions.
let: "x'" := !"x" in
let: "r'" := !"x'" in
letalloc: "r" <- "r'" in
- delete [ #1; "x"];; "return" ["r"].
+ delete [ #1; "x"];; return: ["r"].
Lemma refmut_deref_type ty :
typed_val refmut_deref
@@ -56,7 +56,7 @@ Section refmut_functions.
let: "x'" := !"x" in
let: "r'" := !"x'" in
letalloc: "r" <- "r'" in
- delete [ #1; "x"];; "return" ["r"].
+ delete [ #1; "x"];; return: ["r"].
Lemma refmut_derefmut_type ty :
typed_val refmut_derefmut
@@ -111,7 +111,7 @@ Section refmut_functions.
"rc" <- #0;;
Endlft;;
delete [ #2; "x"];;
- let: "r" := new [ #0] in "return" ["r"].
+ let: "r" := new [ #0] in return: ["r"].
Lemma refmut_drop_type ty :
typed_val refmut_drop (fn(∀ α, [α]; refmut α ty) → unit).
@@ -164,7 +164,7 @@ Section refmut_functions.
"ref" <- "r'";;
delete [ #1; "f"];; "k" []
cont: "k" [] :=
- "return" ["ref"].
+ return: ["ref"].
Lemma refmut_map_type ty1 ty2 envty E :
typed_val refmut_map
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 2a6caa17..18b83f25 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -17,7 +17,7 @@ Section rwlock_functions.
let: "r" := new [ #(S ty.(ty_size))] in
"r" +â‚— #0 <- #0;;
"r" +â‚— #1 <-{ty.(ty_size)} !"x";;
- delete [ #ty.(ty_size) ; "x"];; "return" ["r"].
+ delete [ #ty.(ty_size) ; "x"];; return: ["r"].
Lemma rwlock_new_type ty :
typed_val (rwlock_new ty) (fn([]; ty) → rwlock ty).
@@ -53,7 +53,7 @@ Section rwlock_functions.
funrec: <> ["x"] :=
let: "r" := new [ #ty.(ty_size)] in
"r" <-{ty.(ty_size)} !("x" +â‚— #1);;
- delete [ #(S ty.(ty_size)) ; "x"];; "return" ["r"].
+ delete [ #(S ty.(ty_size)) ; "x"];; return: ["r"].
Lemma rwlock_into_inner_type ty :
typed_val (rwlock_into_inner ty) (fn([] ; rwlock ty) → ty).
@@ -87,7 +87,7 @@ Section rwlock_functions.
funrec: <> ["x"] :=
let: "x'" := !"x" in
"x" <- "x'" +â‚— #1;;
- "return" ["x"].
+ return: ["x"].
Lemma rwlock_get_mut_type ty :
typed_val rwlock_get_mut (fn(∀ α, [α]; &uniq{α} (rwlock ty)) → &uniq{α} ty).
@@ -135,7 +135,7 @@ Section rwlock_functions.
"k" ["r"]
else "loop" [])
cont: "k" ["r"] :=
- delete [ #1; "x"];; "return" ["r"].
+ delete [ #1; "x"];; return: ["r"].
Lemma rwlock_try_read_type ty :
typed_val rwlock_try_read
@@ -250,7 +250,7 @@ Section rwlock_functions.
"r" <-{Σ 0} ();;
"k" ["r"]
cont: "k" ["r"] :=
- delete [ #1; "x"];; "return" ["r"].
+ delete [ #1; "x"];; return: ["r"].
Lemma rwlock_try_write_type ty :
typed_val rwlock_try_write
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 353f6b72..967055ed 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -16,7 +16,7 @@ Section rwlockreadguard_functions.
let: "x'" := !"x" in
let: "r'" := !"x'" +â‚— #1 in
letalloc: "r" <- "r'" in
- delete [ #1; "x"];; "return" ["r"].
+ delete [ #1; "x"];; return: ["r"].
Lemma rwlockreadguard_deref_type ty :
typed_val rwlockreadguard_deref
@@ -56,7 +56,7 @@ Section rwlockreadguard_functions.
let: "n" := !ˢᶜ"x'" in
if: CAS "x'" "n" ("n" - #1) then
delete [ #1; "x"];;
- let: "r" := new [ #0] in "return" ["r"]
+ let: "r" := new [ #0] in return: ["r"]
else "loop" []).
Lemma rwlockreadguard_drop_type ty :
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index 68741c9e..e652202a 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -16,7 +16,7 @@ Section rwlockwriteguard_functions.
let: "x'" := !"x" in
let: "r'" := !"x'" +â‚— #1 in
letalloc: "r" <- "r'" in
- delete [ #1; "x"];; "return" ["r"].
+ delete [ #1; "x"];; return: ["r"].
Lemma rwlockwriteguard_deref_type ty :
typed_val rwlockwriteguard_deref
@@ -58,7 +58,7 @@ Section rwlockwriteguard_functions.
let: "x'" := !"x" in
let: "r'" := !"x'" +â‚— #1 in
letalloc: "r" <- "r'" in
- delete [ #1; "x"];; "return" ["r"].
+ delete [ #1; "x"];; return: ["r"].
Lemma rwlockwriteguard_derefmut_type ty :
typed_val rwlockwriteguard_derefmut
@@ -105,7 +105,7 @@ Section rwlockwriteguard_functions.
let: "x'" := !"x" in
"x'" <-ˢᶜ #0;;
delete [ #1; "x"];;
- let: "r" := new [ #0] in "return" ["r"].
+ let: "r" := new [ #0] in return: ["r"].
Lemma rwlockwriteguard_drop_type ty :
typed_val rwlockwriteguard_drop
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index 390d44c3..9b4d2ebb 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -65,7 +65,7 @@ Section spawn.
letcall: "r" := "f'" ["env":expr] in
finish ["c"; "r"]] in
letalloc: "r" <- "join" in
- delete [ #1; "f"];; "return" ["r"].
+ delete [ #1; "f"];; return: ["r"].
Lemma spawn_type `(!Send envty, !Send retty) :
typed_val spawn (fn([]; fn([] ; envty) → retty, envty) → join_handle retty).
@@ -111,7 +111,7 @@ Section spawn.
funrec: <> ["c"] :=
let: "c'" := !"c" in
let: "r" := join ["c'"] in
- delete [ #1; "c"];; "return" ["r"].
+ delete [ #1; "c"];; return: ["r"].
Lemma join_type retty :
typed_val join (fn([]; join_handle retty) → retty).
--
GitLab