From b234965c9019a0ee73e1e5398cacf2a20808331c Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Sat, 1 May 2021 13:04:28 +0200
Subject: [PATCH] Improve notations for functions
We use fnrec: for recursive functions and fn: for non-recursve functions. This is both shorter and closer to Rust.
---
theories/lang/notation.v | 12 +++++---
theories/typing/examples/get_x.v | 2 +-
theories/typing/examples/init_prod.v | 2 +-
theories/typing/examples/lazy_lft.v | 2 +-
theories/typing/examples/nonlexical.v | 2 +-
theories/typing/examples/rebor.v | 2 +-
theories/typing/examples/unbox.v | 2 +-
theories/typing/function.v | 4 +--
theories/typing/lib/arc.v | 28 +++++++++----------
theories/typing/lib/brandedvec.v | 10 +++----
theories/typing/lib/cell.v | 18 ++++++------
theories/typing/lib/diverging_static.v | 2 +-
theories/typing/lib/fake_shared.v | 4 +--
theories/typing/lib/ghostcell.v | 10 +++----
theories/typing/lib/join.v | 2 +-
theories/typing/lib/mutex/mutex.v | 6 ++--
theories/typing/lib/mutex/mutexguard.v | 6 ++--
theories/typing/lib/option.v | 6 ++--
theories/typing/lib/panic.v | 2 +-
theories/typing/lib/rc/rc.v | 18 ++++++------
theories/typing/lib/rc/weak.v | 10 +++----
theories/typing/lib/refcell/ref_code.v | 10 +++----
theories/typing/lib/refcell/refcell_code.v | 10 +++----
theories/typing/lib/refcell/refmut_code.v | 8 +++---
theories/typing/lib/rwlock/rwlock_code.v | 10 +++----
.../typing/lib/rwlock/rwlockreadguard_code.v | 4 +--
.../typing/lib/rwlock/rwlockwriteguard_code.v | 6 ++--
theories/typing/lib/spawn.v | 4 +--
theories/typing/lib/swap.v | 2 +-
theories/typing/lib/take_mut.v | 2 +-
30 files changed, 105 insertions(+), 101 deletions(-)
diff --git a/theories/lang/notation.v b/theories/lang/notation.v
index d44fc14d..53850236 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 e71c3dec..bf18e709 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 49723aed..0d80d3ae 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 0bc054bc..eb39bd7e 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 7e78bb31..1ec12ab6 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 e761beeb..acab6075 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 b27bbd92..28456056 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 534f80e5..9411f29c 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 88ad58aa..2cfdd8d3 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 95685ec3..fd7a55f1 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 b0e90f84..909f7c01 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 93bebbe2..a1000d8e 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 9d6b7152..e2983f0e 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 778e0c3d..61df5d7a 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 d73ae6d5..fe18843f 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 70b5b362..ac7a8757 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 d57fac59..d4b2d0c9 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 5ced33ac..2a586177 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 7190f6cc..62414372 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 6f0494ed..42fbfda1 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 83042cbf..b0ee7775 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 f279e518..c0ab47d4 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 c494d485..d2cec77b 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 23e1ce16..83a6d603 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 41bd404c..a30e6814 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 f6dccc46..b16e0e0f 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 9ff16886..d3bcfccd 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 a546ad15..c44dc6d2 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 e76b730c..0fa37789 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 7acd8b79..259e758c 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
--
GitLab