diff --git a/theories/lang/notation.v b/theories/lang/notation.v
index 21e5bb5d10f6ab0c208517d4089b55358ccf4612..66220b29a8e455b766c14ed138f692e23c4357fd 100644
--- a/theories/lang/notation.v
+++ b/theories/lang/notation.v
@@ -6,10 +6,14 @@ Notation "e1 < e2" := (e1+#1 ≤ e2)%E
Notation Newlft := (Lit LitPoison) (only parsing).
Notation Endlft := Skip (only parsing).
-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 "'fnrec:' f xl := e" := (rec: f (BNamed "return"::xl) := e)%E
+ (at level 102, f, xl at level 1, e at level 200) : expr_scope.
+Notation "'fnrec:' f xl := e" := (rec: f (BNamed "return"::xl) := e)%V
+ (at level 102, f, xl at level 1, e at level 200) : val_scope.
+Notation "'fn:' xl := e" := (fnrec: <> xl := e)%E
+ (at level 102, xl at level 1, e at level 200) : expr_scope.
+Notation "'fn:' xl := e" := (fnrec: <> xl := e)%V
+ (at level 102, xl at level 1, e at level 200) : val_scope.
Notation "'return:'" := "return" : expr_scope.
Notation "'letcont:' k xl := e1 'in' e2" :=
diff --git a/theories/typing/examples/get_x.v b/theories/typing/examples/get_x.v
index 58c0a6710a7b7cce326f4a961f33ef5852a9c40d..5da7c4cd07efc311f8d9ccb0ade00c2ed9794a80 100644
--- a/theories/typing/examples/get_x.v
+++ b/theories/typing/examples/get_x.v
@@ -5,7 +5,7 @@ Section get_x.
Context `{!typeG Σ}.
Definition get_x : val :=
- funrec: <> ["p"] :=
+ fn: ["p"] :=
let: "p'" := !"p" in
letalloc: "r" <- "p'" +â‚— #0 in
delete [ #1; "p"] ;; return: ["r"].
diff --git a/theories/typing/examples/init_prod.v b/theories/typing/examples/init_prod.v
index 0a4187ec1338e529c2b427918733162f10262ace..2756e4fc161b7d7ae46b14ea9269db44fd251689 100644
--- a/theories/typing/examples/init_prod.v
+++ b/theories/typing/examples/init_prod.v
@@ -5,7 +5,7 @@ Section init_prod.
Context `{!typeG Σ}.
Definition init_prod : val :=
- funrec: <> ["x"; "y"] :=
+ fn: ["x"; "y"] :=
let: "x'" := !"x" in let: "y'" := !"y" in
let: "r" := new [ #2] in
"r" +â‚— #0 <- "x'";; "r" +â‚— #1 <- "y'";;
diff --git a/theories/typing/examples/lazy_lft.v b/theories/typing/examples/lazy_lft.v
index 6b5416ece24865e0c68f9cd9724b30050197a77a..8203e58019476b372aeabf7e4dbe2e38b0bd252d 100644
--- a/theories/typing/examples/lazy_lft.v
+++ b/theories/typing/examples/lazy_lft.v
@@ -5,7 +5,7 @@ Section lazy_lft.
Context `{!typeG Σ}.
Definition lazy_lft : val :=
- funrec: <> [] :=
+ fn: [] :=
Newlft;;
let: "t" := new [ #2] in let: "f" := new [ #1] in let: "g" := new [ #1] in
let: "42" := #42 in "f" <- "42";;
diff --git a/theories/typing/examples/nonlexical.v b/theories/typing/examples/nonlexical.v
index bef584f9ac4a6029bf223f97be178d4e4c4712d9..de890d8b74d37871eacb3ae4db29d120a8705b61 100644
--- a/theories/typing/examples/nonlexical.v
+++ b/theories/typing/examples/nonlexical.v
@@ -27,7 +27,7 @@ Section non_lexical.
typed_val insert (fn(∀ α, ∅; &uniq{α} hashmap, K, V) → option V).
Definition get_default : val :=
- funrec: <> ["map"; "key"] :=
+ fn: ["map"; "key"] :=
let: "get_mut" := get_mut in
let: "map'" := !"map" in
diff --git a/theories/typing/examples/rebor.v b/theories/typing/examples/rebor.v
index 42f1c255e6f2a5db5c894355c9eeb123d0ec824b..d9498d4565fb7ec15f7ea6a4bb6a962304df2408 100644
--- a/theories/typing/examples/rebor.v
+++ b/theories/typing/examples/rebor.v
@@ -5,7 +5,7 @@ Section rebor.
Context `{!typeG Σ}.
Definition rebor : val :=
- funrec: <> ["t1"; "t2"] :=
+ fn: ["t1"; "t2"] :=
Newlft;;
letalloc: "x" <- "t1" in
let: "x'" := !"x" in let: "y" := "x'" +â‚— #0 in
diff --git a/theories/typing/examples/unbox.v b/theories/typing/examples/unbox.v
index 2815771a313ecc5586c9f51f941cc5069e746852..f681022c887dd285912f2d32079672a65e2e5af9 100644
--- a/theories/typing/examples/unbox.v
+++ b/theories/typing/examples/unbox.v
@@ -5,7 +5,7 @@ Section unbox.
Context `{!typeG Σ}.
Definition unbox : val :=
- funrec: <> ["b"] :=
+ fn: ["b"] :=
let: "b'" := !"b" in let: "bx" := !"b'" in
letalloc: "r" <- "bx" +â‚— #0 in
delete [ #1; "b"] ;; return: ["r"].
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 9f1325a986e5d30eb5edbe369ee422510ba7aaad..99876a8fb71a2c6fb7e105f7b9e22de6e6f94f9d 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -407,7 +407,7 @@ Section typing.
Lemma type_rec {A} E L fb (argsb : list binder) ef e n
(fp : A → fn_params n) T `{!CopyC T, !SendC T, !Closed _ e} :
- IntoVal ef (funrec: fb argsb := e) →
+ IntoVal ef (fnrec: fb argsb := e) →
n = length argsb →
â–¡ (∀ x Ï (f : val) k (args : vec val (length argsb)),
typed_body ((fp x).(fp_E) Ï) [Ï âŠ‘â‚— []]
@@ -430,7 +430,7 @@ Section typing.
Lemma type_fn {A} E L (argsb : list binder) ef e n
(fp : A → fn_params n) T `{!CopyC T, !SendC T, !Closed _ e} :
- IntoVal ef (funrec: <> argsb := e) →
+ IntoVal ef (fn: argsb := e) →
n = length argsb →
â–¡ (∀ x Ï k (args : vec val (length argsb)),
typed_body ((fp x).(fp_E) Ï)
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 92af7db87e46eae02cc2be22d01a1006d5300ddf..65a37602b1b0eca08eb7748f2276273b99cbe778 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -401,7 +401,7 @@ Section arc.
(* Code : constructors *)
Definition arc_new ty : val :=
- funrec: <> ["x"] :=
+ fn: ["x"] :=
let: "arcbox" := new [ #(2 + ty.(ty_size))%nat ] in
let: "arc" := new [ #1 ] in
"arcbox" +â‚— #0 <- #1;;
@@ -444,7 +444,7 @@ Section arc.
Qed.
Definition weak_new ty : val :=
- funrec: <> [] :=
+ fn: [] :=
let: "arcbox" := new [ #(2 + ty.(ty_size))%nat ] in
let: "w" := new [ #1 ] in
"arcbox" +â‚— #0 <- #0;;
@@ -488,7 +488,7 @@ Section arc.
(* Code : deref *)
Definition arc_deref : val :=
- funrec: <> ["arc"] :=
+ fn: ["arc"] :=
let: "x" := new [ #1 ] in
let: "arc'" := !"arc" in
"x" <- (!"arc'" +â‚— #2);;
@@ -531,7 +531,7 @@ Section arc.
(* Code : getters *)
Definition arc_strong_count : val :=
- funrec: <> ["arc"] :=
+ fn: ["arc"] :=
let: "r" := new [ #1 ] in
let: "arc'" := !"arc" in
let: "arc''" := !"arc'" in
@@ -578,7 +578,7 @@ Section arc.
Qed.
Definition arc_weak_count : val :=
- funrec: <> ["arc"] :=
+ fn: ["arc"] :=
let: "r" := new [ #1 ] in
let: "arc'" := !"arc" in
let: "arc''" := !"arc'" in
@@ -625,7 +625,7 @@ Section arc.
(* Code : clone, [up/down]grade. *)
Definition arc_clone : val :=
- funrec: <> ["arc"] :=
+ fn: ["arc"] :=
let: "r" := new [ #1 ] in
let: "arc'" := !"arc" in
let: "arc''" := !"arc'" in
@@ -674,7 +674,7 @@ Section arc.
Qed.
Definition weak_clone : val :=
- funrec: <> ["w"] :=
+ fn: ["w"] :=
let: "r" := new [ #1 ] in
let: "w'" := !"w" in
let: "w''" := !"w'" in
@@ -722,7 +722,7 @@ Section arc.
Qed.
Definition downgrade : val :=
- funrec: <> ["arc"] :=
+ fn: ["arc"] :=
let: "r" := new [ #1 ] in
let: "arc'" := !"arc" in
let: "arc''" := !"arc'" in
@@ -769,7 +769,7 @@ Section arc.
Qed.
Definition upgrade : val :=
- funrec: <> ["w"] :=
+ fn: ["w"] :=
let: "r" := new [ #2 ] in
let: "w'" := !"w" in
let: "w''" := !"w'" in
@@ -832,7 +832,7 @@ Section arc.
(* Code : drop *)
Definition arc_drop ty : val :=
- funrec: <> ["arc"] :=
+ fn: ["arc"] :=
let: "r" := new [ #(option ty).(ty_size) ] in
let: "arc'" := !"arc" in
"r" <-{Σ none} ();;
@@ -901,7 +901,7 @@ Section arc.
Qed.
Definition weak_drop ty : val :=
- funrec: <> ["arc"] :=
+ fn: ["arc"] :=
let: "r" := new [ #0] in
let: "arc'" := !"arc" in
(if: drop_weak ["arc'"] then delete [ #(2 + ty.(ty_size)); "arc'" ]
@@ -938,7 +938,7 @@ Section arc.
(* Code : other primitives *)
Definition arc_try_unwrap ty : val :=
- funrec: <> ["arc"] :=
+ fn: ["arc"] :=
let: "r" := new [ #(Σ[ ty; arc ty ]).(ty_size) ] in
let: "arc'" := !"arc" in
if: try_unwrap ["arc'"] then
@@ -1015,7 +1015,7 @@ Section arc.
Qed.
Definition arc_get_mut : val :=
- funrec: <> ["arc"] :=
+ fn: ["arc"] :=
let: "r" := new [ #2 ] in
let: "arc'" := !"arc" in
let: "arc''" := !"arc'" in
@@ -1081,7 +1081,7 @@ Section arc.
Qed.
Definition arc_make_mut (ty : type) (clone : val) : val :=
- funrec: <> ["arc"] :=
+ fn: ["arc"] :=
let: "r" := new [ #1 ] in
let: "arc'" := !"arc" in
let: "arc''" := !"arc'" in
diff --git a/theories/typing/lib/brandedvec.v b/theories/typing/lib/brandedvec.v
index 76c38b11370452a992dc9407dafb86be7f7e6855..51ccdcc2cb8a28594f37d7102c70e1db487805b5 100644
--- a/theories/typing/lib/brandedvec.v
+++ b/theories/typing/lib/brandedvec.v
@@ -163,7 +163,7 @@ Section typing.
Local Notation iProp := (iProp Σ).
Definition brandvec_new (call_once : val) (R_F : type) : val :=
- funrec: <> ["f"] :=
+ fn: ["f"] :=
let: "call_once" := call_once in
letalloc: "n" <- #0 in
letcall: "r" := "call_once" ["f";"n"]%E in
@@ -233,7 +233,7 @@ Section typing.
Qed.
Definition brandvec_get_index : val :=
- funrec: <> ["v"; "i"] :=
+ fn: ["v"; "i"] :=
let: "r" := new [ #2 ] in
let: "v'" := !"v" in
let: "i'" := !"i" in
@@ -311,7 +311,7 @@ Section typing.
Qed.
Definition brandidx_get : val :=
- funrec: <> ["s";"c"] :=
+ fn: ["s";"c"] :=
let: "len" := !"s" in
let: "idx" := !"c" in
delete [ #1; "s" ];; delete [ #1; "c" ];;
@@ -363,7 +363,7 @@ Section typing.
Qed.
Definition brandvec_push : val :=
- funrec: <> ["s"] :=
+ fn: ["s"] :=
let: "n" := !"s" in
delete [ #1; "s" ];;
let: "r" := new [ #1] in
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 4beedf279001141c6e728fe8334a8c3e9ea5663c..9754ad218ae0a349abd78fc1084ee32d1e4919dd 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -84,7 +84,7 @@ Section typing.
(** The next couple functions essentially show owned-type equalities, as they
are all different types for the identity function. *)
(* Constructing a cell. *)
- Definition cell_new : val := funrec: <> ["x"] := return: ["x"].
+ Definition cell_new : val := fn: ["x"] := return: ["x"].
Lemma cell_new_type ty `{!TyWf ty} : typed_val cell_new (fn(∅; ty) → cell ty).
Proof.
@@ -95,7 +95,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 := fn: ["x"] := return: ["x"].
Lemma cell_into_inner_type ty `{!TyWf ty} :
typed_val cell_into_inner (fn(∅; cell ty) → ty).
@@ -107,7 +107,7 @@ Section typing.
Qed.
Definition cell_get_mut : val :=
- funrec: <> ["x"] := return: ["x"].
+ fn: ["x"] := return: ["x"].
Lemma cell_get_mut_type ty `{!TyWf ty} :
typed_val cell_get_mut (fn(∀ α, ∅; &uniq{α} (cell ty)) → &uniq{α} ty).
@@ -119,7 +119,7 @@ Section typing.
Qed.
Definition cell_from_mut : val :=
- funrec: <> ["x"] := return: ["x"].
+ fn: ["x"] := return: ["x"].
Lemma cell_from_mut_type ty `{!TyWf ty} :
typed_val cell_from_mut (fn(∀ α, ∅; &uniq{α} ty) → &uniq{α} (cell ty)).
@@ -131,7 +131,7 @@ Section typing.
Qed.
Definition cell_into_box : val :=
- funrec: <> ["x"] := return: ["x"].
+ fn: ["x"] := return: ["x"].
Lemma cell_into_box_type ty `{!TyWf ty} :
typed_val cell_into_box (fn(∅;box (cell ty)) → box ty).
@@ -143,7 +143,7 @@ Section typing.
Qed.
Definition cell_from_box : val :=
- funrec: <> ["x"] := return: ["x"].
+ fn: ["x"] := return: ["x"].
Lemma cell_from_box_type ty `{!TyWf ty} :
typed_val cell_from_box (fn(∅; box ty) → box (cell ty)).
@@ -156,7 +156,7 @@ Section typing.
(** Reading from a cell *)
Definition cell_get ty : val :=
- funrec: <> ["x"] :=
+ fn: ["x"] :=
let: "x'" := !"x" in
letalloc: "r" <-{ty.(ty_size)} !"x'" in
delete [ #1; "x"];; return: ["r"].
@@ -177,7 +177,7 @@ Section typing.
(** Writing to a cell *)
Definition cell_replace ty : val :=
- funrec: <> ["c"; "x"] :=
+ fn: ["c"; "x"] :=
let: "c'" := !"c" in
letalloc: "r" <-{ty.(ty_size)} !"c'" in
"c'" <-{ty.(ty_size)} !"x";;
@@ -229,7 +229,7 @@ Section typing.
Called alias::one in Rust.
This is really just [cell_from_mut] followed by sharing. *)
Definition fake_shared_cell : val :=
- funrec: <> ["x"] :=
+ fn: ["x"] :=
let: "x'" := !"x" in
letalloc: "r" <- "x'" in
delete [ #1; "x"];; return: ["r"].
diff --git a/theories/typing/lib/diverging_static.v b/theories/typing/lib/diverging_static.v
index 8d0768aa9a19d5013c81ff4b3ea0790385b9aa7e..1c985a36742b5f30668cad9db79d47bd486c5662 100644
--- a/theories/typing/lib/diverging_static.v
+++ b/theories/typing/lib/diverging_static.v
@@ -9,7 +9,7 @@ Section diverging_static.
(* Show that we can convert any live borrow to 'static with an infinite
loop. *)
Definition diverging_static_loop (call_once : val) : val :=
- funrec: <> ["x"; "f"] :=
+ fn: ["x"; "f"] :=
let: "call_once" := call_once in
letcall: "ret" := "call_once" ["f"; "x"]%E in
withcont: "loop":
diff --git a/theories/typing/lib/fake_shared.v b/theories/typing/lib/fake_shared.v
index 1cd113064358ef3f7add80c9be1ae4be592e43c5..0b3db02beed2185a7989b9c84594963b53f295ae 100644
--- a/theories/typing/lib/fake_shared.v
+++ b/theories/typing/lib/fake_shared.v
@@ -6,7 +6,7 @@ Section fake_shared.
Context `{!typeG Σ}.
Definition fake_shared_box : val :=
- funrec: <> ["x"] := Skip ;; return: ["x"].
+ fn: ["x"] := Skip ;; return: ["x"].
Lemma fake_shared_box_type ty `{!TyWf ty} :
typed_val fake_shared_box
@@ -36,7 +36,7 @@ Section fake_shared.
Qed.
Definition fake_shared_uniq : val :=
- funrec: <> ["x"] := Skip ;; return: ["x"].
+ fn: ["x"] := Skip ;; return: ["x"].
Lemma fake_shared_uniq_type ty `{!TyWf ty} :
typed_val fake_shared_box
diff --git a/theories/typing/lib/join.v b/theories/typing/lib/join.v
index 129de0b61a2b66e75f68a59b78d1959972d60f25..ef6a979e5464efa2e01d386caf4aadd4e87565d1 100644
--- a/theories/typing/lib/join.v
+++ b/theories/typing/lib/join.v
@@ -14,7 +14,7 @@ Section join.
One of the closures is executed in another thread, and the
closures can refer to on-stack data (no 'static' bound). *)
Definition join (call_once_A call_once_B : val) (R_A R_B : type) : val :=
- funrec: <> ["fA"; "fB"] :=
+ fn: ["fA"; "fB"] :=
let: "call_once_A" := call_once_A in
let: "call_once_B" := call_once_B in
let: "join" := spawn [λ: ["c"],
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index adb30abf60e5c2ce32d57d19ef77ef2553313d8d..d26dc8f0f2d95c9447cbd75c6c97715bd3114a05 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -124,7 +124,7 @@ Section code.
Context `{!typeG Σ, !lockG Σ}.
Definition mutex_new ty : val :=
- funrec: <> ["x"] :=
+ fn: ["x"] :=
let: "m" := new [ #(mutex ty).(ty_size) ] in
"m" +â‚— #1 <-{ty.(ty_size)} !"x";;
mklock_unlocked ["m" +â‚— #0];;
@@ -165,7 +165,7 @@ Section code.
Qed.
Definition mutex_into_inner ty : val :=
- funrec: <> ["m"] :=
+ fn: ["m"] :=
let: "x" := new [ #ty.(ty_size) ] in
"x" <-{ty.(ty_size)} !("m" +â‚— #1);;
delete [ #(mutex ty).(ty_size); "m"];; return: ["x"].
@@ -204,7 +204,7 @@ Section code.
Qed.
Definition mutex_get_mut : val :=
- funrec: <> ["m"] :=
+ fn: ["m"] :=
let: "m'" := !"m" in
"m" <- ("m'" +â‚— #1);;
return: ["m"].
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index 1c455e50f7648f967a6cea3c4e0e224e287c3ac9..6e31e1e922c5082e0c575779f3f9967a9bb8ae1d 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -145,7 +145,7 @@ Section code.
Context `{!typeG Σ, !lockG Σ}.
Definition mutex_lock : val :=
- funrec: <> ["mutex"] :=
+ fn: ["mutex"] :=
let: "m" := !"mutex" in
let: "guard" := new [ #1 ] in
acquire ["m"];;
@@ -183,7 +183,7 @@ Section code.
Qed.
Definition mutexguard_derefmut : val :=
- funrec: <> ["g"] :=
+ fn: ["g"] :=
let: "g'" := !"g" in
let: "m" := !"g'" in
letalloc: "r" <- ("m" +â‚— #1) in
@@ -269,7 +269,7 @@ Section code.
Qed.
Definition mutexguard_drop : val :=
- funrec: <> ["g"] :=
+ fn: ["g"] :=
let: "m" := !"g" in
release ["m"];;
delete [ #1; "g" ];;
diff --git a/theories/typing/lib/option.v b/theories/typing/lib/option.v
index 15028885d135ac2f641d26659c6cbd4dea9f05c9..66c6d79b7d91b64756aede9d73f14505b48eddb6 100644
--- a/theories/typing/lib/option.v
+++ b/theories/typing/lib/option.v
@@ -18,7 +18,7 @@ Section option.
Definition some := 1%nat.
Definition option_as_mut : val :=
- funrec: <> ["o"] :=
+ fn: ["o"] :=
let: "o'" := !"o" in
let: "r" := new [ #2 ] in
withcont: "k":
@@ -50,7 +50,7 @@ Section option.
Qed.
Definition option_unwrap_or Ï„ : val :=
- funrec: <> ["o"; "def"] :=
+ fn: ["o"; "def"] :=
case: !"o" of
[ delete [ #(S Ï„.(ty_size)); "o"];;
return: ["def"];
@@ -74,7 +74,7 @@ Section option.
Qed.
Definition option_unwrap Ï„ : val :=
- funrec: <> ["o"] :=
+ fn: ["o"] :=
case: !"o" of
[ let: "panic" := panic in
letcall: "emp" := "panic" [] in
diff --git a/theories/typing/lib/panic.v b/theories/typing/lib/panic.v
index 58a6b02eed73ca1f685aa781f16f811f405b3224..f5564c57ba904fc61ff64bd69d2c24a4ca63cc48 100644
--- a/theories/typing/lib/panic.v
+++ b/theories/typing/lib/panic.v
@@ -14,7 +14,7 @@ Section panic.
Context `{!typeG Σ}.
Definition panic : val :=
- funrec: <> [] := #☠.
+ fn: [] := #☠.
Lemma panic_type : typed_val panic (fn(∅) → ∅).
Proof.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 71b859886f56a481cb9c83a1da1f69e8f450a434..e10a8fc092b3deda5cdee2f2660c01db5fd260a4 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -390,7 +390,7 @@ Section code.
Qed.
Definition rc_strong_count : val :=
- funrec: <> ["rc"] :=
+ fn: ["rc"] :=
let: "r" := new [ #1 ] in
let: "rc'" := !"rc" in
let: "rc''" := !"rc'" in
@@ -447,7 +447,7 @@ Section code.
Qed.
Definition rc_weak_count : val :=
- funrec: <> ["rc"] :=
+ fn: ["rc"] :=
let: "r" := new [ #1 ] in
let: "rc'" := !"rc" in
let: "rc''" := !"rc'" in
@@ -508,7 +508,7 @@ Section code.
Qed.
Definition rc_new ty : val :=
- funrec: <> ["x"] :=
+ fn: ["x"] :=
let: "rcbox" := new [ #(2 + ty.(ty_size))%nat ] in
let: "rc" := new [ #1 ] in
"rcbox" +â‚— #0 <- #1;;
@@ -551,7 +551,7 @@ Section code.
Qed.
Definition rc_clone : val :=
- funrec: <> ["rc"] :=
+ fn: ["rc"] :=
let: "r" := new [ #1 ] in
let: "rc'" := !"rc" in
let: "rc''" := !"rc'" in
@@ -616,7 +616,7 @@ Section code.
Qed.
Definition rc_deref : val :=
- funrec: <> ["rc"] :=
+ fn: ["rc"] :=
let: "x" := new [ #1 ] in
let: "rc'" := !"rc" in
"x" <- (!"rc'" +â‚— #2);;
@@ -658,7 +658,7 @@ Section code.
Qed.
Definition rc_try_unwrap ty : val :=
- funrec: <> ["rc"] :=
+ fn: ["rc"] :=
let: "r" := new [ #(Σ[ ty; rc ty ]).(ty_size) ] in
withcont: "k":
let: "rc'" := !"rc" in
@@ -756,7 +756,7 @@ Section code.
Qed.
Definition rc_drop ty : val :=
- funrec: <> ["rc"] :=
+ fn: ["rc"] :=
let: "r" := new [ #(option ty).(ty_size) ] in
withcont: "k":
let: "rc'" := !"rc" in
@@ -850,7 +850,7 @@ Section code.
Qed.
Definition rc_get_mut : val :=
- funrec: <> ["rc"] :=
+ fn: ["rc"] :=
let: "r" := new [ #2 ] in
withcont: "k":
let: "rc'" := !"rc" in
@@ -941,7 +941,7 @@ Section code.
(* TODO : it is not nice that we have to inline the definition of
rc_new and of rc_deref. *)
Definition rc_make_mut (ty : type) (clone : val) : val :=
- funrec: <> ["rc"] :=
+ fn: ["rc"] :=
let: "r" := new [ #1 ] in
withcont: "k":
let: "rc'" := !"rc" in
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index ed5b7d8837ebda83cd580993bfe02a7799139fc3..4dc0ad6348306762d2e718cc1cd104b66e1ccc19 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -112,7 +112,7 @@ Section code.
Context `{!typeG Σ, !rcG Σ}.
Definition rc_upgrade : val :=
- funrec: <> ["w"] :=
+ fn: ["w"] :=
let: "r" := new [ #2 ] in
withcont: "k":
let: "w'" := !"w" in
@@ -227,7 +227,7 @@ Section code.
Qed.
Definition rc_downgrade : val :=
- funrec: <> ["rc"] :=
+ fn: ["rc"] :=
let: "r" := new [ #1 ] in
let: "rc'" := !"rc" in
let: "rc''" := !"rc'" in
@@ -290,7 +290,7 @@ Section code.
(* Exact same code as downgrade *)
Definition weak_clone : val :=
- funrec: <> ["w"] :=
+ fn: ["w"] :=
let: "r" := new [ #1 ] in
let: "w'" := !"w" in
let: "w''" := !"w'" in
@@ -362,7 +362,7 @@ Section code.
Qed.
Definition weak_drop ty : val :=
- funrec: <> ["w"] :=
+ fn: ["w"] :=
withcont: "k":
let: "w'" := !"w" in
let: "weak" := !("w'" +â‚— #1) in
@@ -443,7 +443,7 @@ Section code.
Qed.
Definition weak_new ty : val :=
- funrec: <> [] :=
+ fn: [] :=
let: "rcbox" := new [ #(2 + ty.(ty_size))%nat ] in
let: "w" := new [ #1 ] in
"rcbox" +â‚— #0 <- #0;;
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 82ced030145b076eb7684c0aa9bcc645835e92c2..642303b4618f8ca08c28cf0ee7a3fe1d1e67819d 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -35,7 +35,7 @@ Section ref_functions.
(* Cloning a ref. We need to increment the counter. *)
Definition ref_clone : val :=
- funrec: <> ["x"] :=
+ fn: ["x"] :=
let: "x'" := !"x" in
let: "rc" := !("x'" +â‚— #1) in
let: "n" := !"rc" in
@@ -97,7 +97,7 @@ Section ref_functions.
(* Turning a ref into a shared borrow. *)
Definition ref_deref : val :=
- funrec: <> ["x"] :=
+ fn: ["x"] :=
let: "x'" := !"x" in
let: "r'" := !"x'" in
letalloc: "r" <- "r'" in
@@ -133,7 +133,7 @@ Section ref_functions.
(* Dropping a ref and decrement the count in the corresponding refcell. *)
Definition ref_drop : val :=
- funrec: <> ["x"] :=
+ fn: ["x"] :=
let: "rc" := !("x" +â‚— #1) in
let: "n" := !"rc" in
"rc" <- "n" - #1;;
@@ -195,7 +195,7 @@ Section ref_functions.
(* Apply a function within the ref, typically for accessing a component. *)
Definition ref_map (call_once : val) : val :=
- funrec: <> ["ref"; "f"] :=
+ fn: ["ref"; "f"] :=
let: "call_once" := call_once in
let: "x'" := !"ref" in
letalloc: "x" <- "x'" in
@@ -255,7 +255,7 @@ Section ref_functions.
(* Apply a function within the ref, and create two ref,
typically for splitting the reference. *)
Definition ref_map_split (call_once : val) : val :=
- funrec: <> ["ref"; "f"] :=
+ fn: ["ref"; "f"] :=
let: "call_once" := call_once in
let: "x'" := !"ref" in
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index 8e46f894ffe8be47411d1161529ccf80000db75a..cbb23dcbad48d96f690b8dce8917a66cb787d25c 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -11,7 +11,7 @@ Section refcell_functions.
(* Constructing a refcell. *)
Definition refcell_new ty : val :=
- funrec: <> ["x"] :=
+ fn: ["x"] :=
let: "r" := new [ #(S ty.(ty_size))] in
"r" +â‚— #0 <- #0;;
"r" +â‚— #1 <-{ty.(ty_size)} !"x";;
@@ -44,7 +44,7 @@ Section refcell_functions.
(* The other direction: getting ownership out of a refcell. *)
Definition refcell_into_inner ty : val :=
- funrec: <> ["x"] :=
+ fn: ["x"] :=
let: "r" := new [ #ty.(ty_size)] in
"r" <-{ty.(ty_size)} !("x" +â‚— #1);;
(* TODO: Can we make it so that the parenthesis above are mandatory?
@@ -78,7 +78,7 @@ Section refcell_functions.
Qed.
Definition refcell_get_mut : val :=
- funrec: <> ["x"] :=
+ fn: ["x"] :=
let: "x'" := !"x" in
"x" <- "x'" +â‚— #1;; (* Get the second field *)
return: ["x"].
@@ -116,7 +116,7 @@ Section refcell_functions.
(* Shared borrowing. *)
Definition refcell_try_borrow : val :=
- funrec: <> ["x"] :=
+ fn: ["x"] :=
let: "r" := new [ #3 ] in
withcont: "k":
let: "x'" := !"x" in
@@ -225,7 +225,7 @@ Section refcell_functions.
(* Unique borrowing. *)
Definition refcell_try_borrow_mut : val :=
- funrec: <> ["x"] :=
+ fn: ["x"] :=
let: "r" := new [ #3 ] in
withcont: "k":
let: "x'" := !"x" in
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 47db4a1ade14c687653adafeeb192af9ad665c6d..4e431eaaa8ccded2effedb5892fc2d4721d4f23f 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -10,7 +10,7 @@ Section refmut_functions.
(* Turning a refmut into a shared borrow. *)
Definition refmut_deref : val :=
- funrec: <> ["x"] :=
+ fn: ["x"] :=
let: "x'" := !"x" in
let: "r'" := !"x'" in
letalloc: "r" <- "r'" in
@@ -101,7 +101,7 @@ Section refmut_functions.
(* Dropping a refmut and set the count to 0 in the corresponding refcell. *)
Definition refmut_drop : val :=
- funrec: <> ["x"] :=
+ fn: ["x"] :=
let: "rc" := !("x" +â‚— #1) in
let: "n" := !"rc" in
"rc" <- "n" + #1;;
@@ -166,7 +166,7 @@ Section refmut_functions.
(* Apply a function within the refmut, typically for accessing a component. *)
Definition refmut_map (call_once : val) : val :=
- funrec: <> ["ref"; "f"] :=
+ fn: ["ref"; "f"] :=
let: "call_once" := call_once in
let: "x'" := !"ref" in
letalloc: "x" <- "x'" in
@@ -226,7 +226,7 @@ Section refmut_functions.
(* Apply a function within the refmut, and create two refmuts,
typically for splitting the reference. *)
Definition refmut_map_split (call_once : val) : val :=
- funrec: <> ["refmut"; "f"] :=
+ fn: ["refmut"; "f"] :=
let: "call_once" := call_once in
let: "x'" := !"refmut" in
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 619284d0a41db33c546eea6b7556cae7d478f99f..9202034f9b38b83c01e4d3333d10913e9933da50 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -26,7 +26,7 @@ Section rwlock_functions.
(* Constructing a rwlock. *)
Definition rwlock_new ty : val :=
- funrec: <> ["x"] :=
+ fn: ["x"] :=
let: "r" := new [ #(S ty.(ty_size))] in
"r" +â‚— #0 <- #0;;
"r" +â‚— #1 <-{ty.(ty_size)} !"x";;
@@ -63,7 +63,7 @@ Section rwlock_functions.
(* The other direction: getting ownership out of a rwlock.
Note: as we ignore poisonning, this cannot fail. *)
Definition rwlock_into_inner ty : val :=
- funrec: <> ["x"] :=
+ fn: ["x"] :=
let: "r" := new [ #ty.(ty_size)] in
"r" <-{ty.(ty_size)} !("x" +â‚— #1);;
delete [ #(S ty.(ty_size)) ; "x"];; return: ["r"].
@@ -96,7 +96,7 @@ Section rwlock_functions.
Qed.
Definition rwlock_get_mut : val :=
- funrec: <> ["x"] :=
+ fn: ["x"] :=
let: "x'" := !"x" in
"x" <- "x'" +â‚— #1;;
return: ["x"].
@@ -133,7 +133,7 @@ Section rwlock_functions.
(* Acquiring a read lock. *)
Definition rwlock_try_read : val :=
- funrec: <> ["x"] :=
+ fn: ["x"] :=
let: "r" := new [ #2 ] in
let: "x'" := !"x" in
withcont: "k":
@@ -315,7 +315,7 @@ Section rwlock_functions.
(* Acquiring a write lock. *)
Definition rwlock_try_write : val :=
- funrec: <> ["x"] :=
+ fn: ["x"] :=
withcont: "k":
let: "r" := new [ #2 ] in
let: "x'" := !"x" in
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 3ac037613404cb0df1884bc6d673353ffd56b955..26ce0133be4798412848c020ae6623b971f10d1c 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -13,7 +13,7 @@ Section rwlockreadguard_functions.
(* Turning a rwlockreadguard into a shared borrow. *)
Definition rwlockreadguard_deref : val :=
- funrec: <> ["x"] :=
+ fn: ["x"] :=
let: "x'" := !"x" in
let: "r'" := !"x'" +â‚— #1 in
letalloc: "r" <- "r'" in
@@ -49,7 +49,7 @@ Section rwlockreadguard_functions.
(* Dropping a rwlockreadguard and releasing the corresponding lock. *)
Definition rwlockreadguard_drop : val :=
- funrec: <> ["x"] :=
+ fn: ["x"] :=
let: "x'" := !"x" in
withcont: "loop":
"loop" []
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index bd17c7904812187258fbf4a0aa7d31aad4beac0e..e5dcb3fdf3cb5ab41d356be4b7398da0d898a146 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -13,7 +13,7 @@ Section rwlockwriteguard_functions.
(* Turning a rwlockwriteguard into a shared borrow. *)
Definition rwlockwriteguard_deref : val :=
- funrec: <> ["x"] :=
+ fn: ["x"] :=
let: "x'" := !"x" in
let: "r'" := !"x'" +â‚— #1 in
letalloc: "r" <- "r'" in
@@ -58,7 +58,7 @@ Section rwlockwriteguard_functions.
(* Turning a rwlockwriteguard into a unique borrow. *)
Definition rwlockwriteguard_derefmut : val :=
- funrec: <> ["x"] :=
+ fn: ["x"] :=
let: "x'" := !"x" in
let: "r'" := !"x'" +â‚— #1 in
letalloc: "r" <- "r'" in
@@ -104,7 +104,7 @@ Section rwlockwriteguard_functions.
(* Drop a rwlockwriteguard and release the lock. *)
Definition rwlockwriteguard_drop : val :=
- funrec: <> ["x"] :=
+ fn: ["x"] :=
let: "x'" := !"x" in
"x'" <-ʳᵉˡ #0;;
delete [ #1; "x"];;
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index bf928a57a36fcf0cc4ad0b5db4b09ac9b8ad1e28..eb57e95fa0468f99e3f34b3b0dfedc117fdec271 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -70,7 +70,7 @@ Section spawn.
Context `{!typeG Σ, !spawnG Σ}.
Definition spawn (call_once : val) : val :=
- funrec: <> ["f"] :=
+ fn: ["f"] :=
let: "call_once" := call_once in
let: "join" := spawn [λ: ["c"],
letcall: "r" := "call_once" ["f":expr] in
@@ -111,7 +111,7 @@ Section spawn.
Qed.
Definition join : val :=
- funrec: <> ["c"] :=
+ fn: ["c"] :=
let: "c'" := !"c" in
let: "r" := spawn.join ["c'"] in
delete [ #1; "c"];; return: ["r"].
diff --git a/theories/typing/lib/swap.v b/theories/typing/lib/swap.v
index cb46baaaa629fc1af4cbbdd6887146bcd0125ed8..c8bf802d69ddfa4d06857e8f844ce6abd2ac4e83 100644
--- a/theories/typing/lib/swap.v
+++ b/theories/typing/lib/swap.v
@@ -6,7 +6,7 @@ Section swap.
Context `{!typeG Σ}.
Definition swap ty : val :=
- funrec: <> ["p1"; "p2"] :=
+ fn: ["p1"; "p2"] :=
let: "p1'" := !"p1" in
let: "p2'" := !"p2" in
swap ["p1'"; "p2'"; #ty.(ty_size)];;
diff --git a/theories/typing/lib/take_mut.v b/theories/typing/lib/take_mut.v
index b8c06c9b21200b2811c3e012e0d2cacc3ef9f463..bcd9e596689529dcecb53ecccfde6738c24a6212 100644
--- a/theories/typing/lib/take_mut.v
+++ b/theories/typing/lib/take_mut.v
@@ -8,7 +8,7 @@ Section code.
Context `{!typeG Σ}.
Definition take ty (call_once : val) : val :=
- funrec: <> ["x"; "f"] :=
+ fn: ["x"; "f"] :=
let: "x'" := !"x" in
let: "call_once" := call_once in
letalloc: "t" <-{ty.(ty_size)} !"x'" in