From 4f911f1bed8aac299cbe5bf3152808ad7a48a296 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 | 8 +++---
theories/typing/lib/cell.v | 18 ++++++------
theories/typing/lib/diverging_static.v | 2 +-
theories/typing/lib/fake_shared.v | 4 +--
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 +-
29 files changed, 99 insertions(+), 95 deletions(-)
diff --git a/theories/lang/notation.v b/theories/lang/notation.v
index 21e5bb5d..66220b29 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 58c0a671..5da7c4cd 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 0a4187ec..2756e4fc 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 6b5416ec..8203e580 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 bef584f9..de890d8b 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 42f1c255..d9498d45 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 2815771a..f681022c 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 9f1325a9..99876a8f 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 92af7db8..65a37602 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 76c38b11..51ccdcc2 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 4beedf27..9754ad21 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 8d0768aa..1c985a36 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 1cd11306..0b3db02b 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 129de0b6..ef6a979e 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 adb30abf..d26dc8f0 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 1c455e50..6e31e1e9 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 15028885..66c6d79b 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 58a6b02e..f5564c57 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 71b85988..e10a8fc0 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 ed5b7d88..4dc0ad63 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 82ced030..642303b4 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 8e46f894..cbb23dcb 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 47db4a1a..4e431eaa 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 619284d0..9202034f 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 3ac03761..26ce0133 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 bd17c790..e5dcb3fd 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 bf928a57..eb57e95f 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 cb46baaa..c8bf802d 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 b8c06c9b..bcd9e596 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
--
GitLab