Merge branch 'jh/fn_notation' into 'master'

Improve notations for functions

See merge request !23

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" :=

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"].

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'";;

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";;

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
 

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

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"].

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) ϝ)

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

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

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"].

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":

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

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} :

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"],

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"].

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" ];;

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

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.

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