diff --git a/theories/lang/notation.v b/theories/lang/notation.v
index d44fc14da5ca294e6da6ebe7c0c0bf42909918bc..53850236ca8519d9571db72fc72788afb9d0f4fb 100644
--- a/theories/lang/notation.v
+++ b/theories/lang/notation.v
@@ -61,10 +61,14 @@ Notation "λ: xl , e" := (Lam xl%binder e%E)
Notation "λ: xl , e" := (locked (LamV xl%binder e%E))
(at level 102, xl at level 1, e at level 200) : val_scope.
-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 "'let:' x := e1 'in' e2" :=
diff --git a/theories/typing/examples/get_x.v b/theories/typing/examples/get_x.v
index 68a0e6108007cd3db91c4134d1c636a27529e768..3da2f4acec9826138bf4babf07ab669c7f8140b0 100644
--- a/theories/typing/examples/get_x.v
+++ b/theories/typing/examples/get_x.v
@@ -6,7 +6,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 46cf5855131aa1f3631cdba779161268a162ce28..2da3607365d18fb53a6cff2113d52a3fe1ea4881 100644
--- a/theories/typing/examples/init_prod.v
+++ b/theories/typing/examples/init_prod.v
@@ -6,7 +6,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 0286a518f9eb870fbc32322cb32322c09c596fee..ca5b804e20ce6be74571c94b92fe2457c8320cc9 100644
--- a/theories/typing/examples/lazy_lft.v
+++ b/theories/typing/examples/lazy_lft.v
@@ -6,7 +6,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 eecd7e71b7ca30ae9e4f3255c5f0a51a801d4054..64ad88b12cc50784249a399a485fb00eba60fe8a 100644
--- a/theories/typing/examples/nonlexical.v
+++ b/theories/typing/examples/nonlexical.v
@@ -28,7 +28,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 bb56fe9ca9d6e0465db8132053b70005c03cc3b2..1dbac6cee2d109e58e62716b4f7b5a5384f34956 100644
--- a/theories/typing/examples/rebor.v
+++ b/theories/typing/examples/rebor.v
@@ -6,7 +6,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 05fa741487a6824eaceefcf2bb75d9156fb774de..843b715f00b33a1a8d3003833f19aa8eec09e018 100644
--- a/theories/typing/examples/unbox.v
+++ b/theories/typing/examples/unbox.v
@@ -6,7 +6,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 688d22ca447e6a11e358e089f1db24ae338fa3a2..a71f505dd52b30807ddc2eb648039ed71c695bca 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -404,7 +404,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) Ï) [Ï âŠ‘â‚— []]
@@ -427,7 +427,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 beca6e4ff8324c25c405ea92ae2f739c4bf52961..0e21a9807ddd3e961068f171bf310dfbf875f906 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -328,7 +328,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;;
@@ -371,7 +371,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;;
@@ -414,7 +414,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);;
@@ -457,7 +457,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
@@ -500,7 +500,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
@@ -544,7 +544,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
@@ -588,7 +588,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
@@ -632,7 +632,7 @@ Section arc.
Qed.
Definition downgrade : val :=
- funrec: <> ["arc"] :=
+ fn: ["arc"] :=
let: "r" := new [ #1 ] in
let: "arc'" := !"arc" in
let: "arc''" := !"arc'" in
@@ -676,7 +676,7 @@ Section arc.
Qed.
Definition upgrade : val :=
- funrec: <> ["w"] :=
+ fn: ["w"] :=
let: "r" := new [ #2 ] in
let: "w'" := !"w" in
let: "w''" := !"w'" in
@@ -733,7 +733,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} ();;
@@ -801,7 +801,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'" ]
@@ -837,7 +837,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
@@ -912,7 +912,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
@@ -975,7 +975,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 4779c28bd2574462e8410c8698d618ef26158ae1..8a12af7611d96e067b836246ea9ea055bd4ba581 100644
--- a/theories/typing/lib/brandedvec.v
+++ b/theories/typing/lib/brandedvec.v
@@ -150,7 +150,7 @@ Section brandedvec.
iIntros "Hn Hm".
iDestruct "Hn" as (γn) "(Hidx1 & Hn)".
iDestruct "Hm" as (γm) "(Hidx2 & Hm)".
- iDestruct (lft_meta_agree with "Hidx1 Hidx2") as %<-.
+ iDestruct (lft_meta_agree with "Hidx1 Hidx2") as %<-.
iDestruct (own_valid_2 with "Hn Hm") as %[?%max_nat_included ?]%auth_both_valid_discrete.
iPureIntro. simpl in *. lia.
Qed.
@@ -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
@@ -310,7 +310,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" ];;
@@ -360,7 +360,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 dd05fb91c73ee4feff0cec3be27b51af87989a95..213fa339ce587a3979b3666fbc4f150e2ec33cf1 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";;
@@ -231,7 +231,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/ghostcell.v b/theories/typing/lib/ghostcell.v
index 8bf2ae43bdeaaa80bd9b48aa73d5f1effbe2a49e..07242d83898de629041ff57bf43e4e00157da4d7 100644
--- a/theories/typing/lib/ghostcell.v
+++ b/theories/typing/lib/ghostcell.v
@@ -351,7 +351,7 @@ Section ghostcell.
Qed.
Definition ghosttoken_new (call_once : val) (R_F : type) : val :=
- funrec: <> ["f"] :=
+ fn: ["f"] :=
let: "call_once" := call_once in
let: "n" := new [ #0] in
letcall: "r" := "call_once" ["f";"n"]%E in
@@ -406,7 +406,7 @@ Section ghostcell.
Qed.
Definition ghostcell_new : val :=
- funrec: <> ["n"] :=
+ fn: ["n"] :=
return: ["n"].
Lemma ghostcell_new_type `{!TyWf ty} :
@@ -426,7 +426,7 @@ Section ghostcell.
Qed.
Definition ghostcell_borrow : val :=
- funrec: <> ["c";"s"] :=
+ fn: ["c";"s"] :=
(* Skips needed for laters *)
Skip ;; Skip ;;
return: ["c"].
@@ -583,7 +583,7 @@ Section ghostcell.
Qed.
Definition ghostcell_borrow_mut : val :=
- funrec: <> ["c";"s"] :=
+ fn: ["c";"s"] :=
(* Skips needed for laters *)
Skip ;; Skip ;;
return: ["c"].
@@ -686,7 +686,7 @@ Section ghostcell.
Qed.
Definition ghostcell_as_mut : val :=
- funrec: <> ["c"] :=
+ fn: ["c"] :=
return: ["c"].
Lemma ghostcell_as_mut_type `{!TyWf ty} :
diff --git a/theories/typing/lib/join.v b/theories/typing/lib/join.v
index 1bb028605b6de63d2423c5de5dee0a121874adb4..9de2211b4b52804c4fef43ef2e43962193b41117 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 ccd41e0fb2205754d4d3fee464a0db11e8d1220d..f6a5a350054bc9c3cb1729edc64a7588d677d240 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -129,7 +129,7 @@ Section code.
Context `{!typeG Σ}.
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];;
@@ -169,7 +169,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"].
@@ -208,7 +208,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 dd7ed656b36bd57ad2597e2a23dae9ecf952d62c..acc66566aa9f646ab61f7103a0a76d4ad2c59570 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -160,7 +160,7 @@ Section code.
Qed.
Definition mutex_lock : val :=
- funrec: <> ["mutex"] :=
+ fn: ["mutex"] :=
let: "m" := !"mutex" in
let: "guard" := new [ #1 ] in
acquire ["m"];;
@@ -197,7 +197,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
@@ -283,7 +283,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 d82971859628539bbd370a16c7889e600f979b96..38f7b51a9aec4418f101b6969ecd401d80edf71e 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -383,7 +383,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
@@ -440,7 +440,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
@@ -501,7 +501,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;;
@@ -544,7 +544,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
@@ -609,7 +609,7 @@ Section code.
Qed.
Definition rc_deref : val :=
- funrec: <> ["rc"] :=
+ fn: ["rc"] :=
let: "x" := new [ #1 ] in
let: "rc'" := !"rc" in
"x" <- (!"rc'" +â‚— #2);;
@@ -651,7 +651,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
@@ -749,7 +749,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
@@ -843,7 +843,7 @@ Section code.
Qed.
Definition rc_get_mut : val :=
- funrec: <> ["rc"] :=
+ fn: ["rc"] :=
let: "r" := new [ #2 ] in
withcont: "k":
let: "rc'" := !"rc" in
@@ -934,7 +934,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 5bfb08eaad286c227cab60d3ab213460f3913af8..c7f3a8b02fad971c489099dca5fbd60d72ed301e 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -106,7 +106,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
@@ -221,7 +221,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
@@ -284,7 +284,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
@@ -356,7 +356,7 @@ Section code.
Qed.
Definition weak_drop ty : val :=
- funrec: <> ["w"] :=
+ fn: ["w"] :=
withcont: "k":
let: "w'" := !"w" in
let: "weak" := !("w'" +â‚— #1) in
@@ -437,7 +437,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 dec7138de8efb067c6c4fce50a0f650f5f83079f..ab9fce4c6fd3b7168ba10d8b10ba8f8d502488b4 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -36,7 +36,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
@@ -98,7 +98,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
@@ -134,7 +134,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;;
@@ -196,7 +196,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
@@ -256,7 +256,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 40277f10ce438de85bb79b8f03489d0b58be2c91..3b721072a328c13ee9353dec6f862f1b48a5a301 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -12,7 +12,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";;
@@ -45,7 +45,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?
@@ -79,7 +79,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"].
@@ -117,7 +117,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
@@ -226,7 +226,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 8d8514d336fc87799a655034769507a0999d7cbb..4dfdcf69852acb3c13b15480282f1b906c0fe164 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -11,7 +11,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
@@ -102,7 +102,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;;
@@ -167,7 +167,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
@@ -227,7 +227,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 f12aad293a493d4a9a75aa347500eedf6e8d971e..0582ee3b27aa3f1d180e74fcfbc97363a8c5c3ed 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -12,7 +12,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";;
@@ -48,7 +48,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"].
@@ -81,7 +81,7 @@ Section rwlock_functions.
Qed.
Definition rwlock_get_mut : val :=
- funrec: <> ["x"] :=
+ fn: ["x"] :=
let: "x'" := !"x" in
"x" <- "x'" +â‚— #1;;
return: ["x"].
@@ -117,7 +117,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":
@@ -236,7 +236,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 c8ab78fc9d37776396e38e2191671040e217d9d9..d7d5245306da3ebae341cf3cbd745279b2e83801 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -11,7 +11,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
@@ -47,7 +47,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 c529dfecb2b101b2687ca69abe454c55aa29d9ad..8dfc98913d117aac5534d6641ad9b9c5b087c435 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -11,7 +11,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
@@ -56,7 +56,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
@@ -102,7 +102,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 569cf5571f846903edbf49f58c7ea5cb72ec9474..f2d2859e5f260f5f4b6776cb7d086fef616f26ef 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -68,7 +68,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
@@ -108,7 +108,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 7003310894651374420c0b4782e90620b36fece9..b6d4cb182c0dfb934f17e1108e064fd5e0e2f2fb 100644
--- a/theories/typing/lib/swap.v
+++ b/theories/typing/lib/swap.v
@@ -7,7 +7,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 953378718ae9a405e1699b252d06fd43e4d037a8..9adb5ff76498be29678dac6cbd3881a60950f32e 100644
--- a/theories/typing/lib/take_mut.v
+++ b/theories/typing/lib/take_mut.v
@@ -9,7 +9,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