change notation for memcpy. notation for sum injection has a \Sigma.

theories/lang/memcpy.v

@@ -10,22 +10,22 @@ Definition memcpy : val :=
          "memcpy" ["dst" +ₗ #1 ; "len" - #1 ; "src" +ₗ #1].
 Global Opaque memcpy.
 
-Notation "e1 <⋯ !{ n } e2" :=
+Notation "e1 <-{ n } ! e2" :=
   (memcpy (@cons expr e1%E
           (@cons expr (Lit n)
           (@cons expr e2%E nil))))
-  (at level 80, n at next level, format "e1  <⋯  !{ n } e2") : expr_scope.
+  (at level 80, n at next level, format "e1  <-{ n }  ! e2") : expr_scope.
 
-Notation "e1 <⋯{ i } !{ n } e2" :=
-  (e1 <-{i} ☇ ;; e1+ₗ#1 <⋯ !{n}e2)%E
+Notation "e1 <-{ n ',Σ' i } ! e2" :=
+  (e1 <-{Σ i} () ;; e1+ₗ#1 <-{n} !e2)%E
   (at level 80, n, i at next level,
-   format "e1  <⋯{ i }  !{ n } e2") : expr_scope.
+   format "e1  <-{ n ,Σ  i }  ! e2") : expr_scope.
 
 Lemma wp_memcpy `{heapG Σ} E l1 l2 vl1 vl2 q n:
   ↑heapN ⊆ E →
   length vl1 = n → length vl2 = n →
   {{{ heap_ctx ∗ l1 ↦∗ vl1 ∗ l2 ↦∗{q} vl2 }}}
-    #l1 <⋯ !{n}#l2 @ E
+    #l1 <-{n} !#l2 @ E
   {{{ RET #(); l1 ↦∗ vl2 ∗ l2 ↦∗{q} vl2 }}}.
 Proof.
   iIntros (? Hvl1 Hvl2 Φ) "(#Hinv & Hl1 & Hl2) HΦ".

theories/lang/new_delete.v

@@ -45,6 +45,6 @@ End specs.
 Notation "'letalloc:' x <- e1 'in' e2" :=
   ((Lam (@cons binder x%E%E%E nil) (x <- e1 ;; e2)) [new [ #1]])%E
   (at level 102, x at level 1, e1, e2 at level 200) : expr_scope.
-Notation "'letalloc:' x <⋯ !{ n } e1 'in' e2" :=
-  ((Lam (@cons binder x%E%E%E nil) (x <⋯ !{n%Z%V}e1 ;; e2)) [new [ #n]])%E
+Notation "'letalloc:' x <-{ n } ! e1 'in' e2" :=
+  ((Lam (@cons binder x%E%E%E nil) (x <-{n%Z%V} !e1 ;; e2)) [new [ #n]])%E
   (at level 102, x at level 1, e1, e2 at level 200) : expr_scope.

theories/lang/notation.v

@@ -85,7 +85,10 @@ Notation "'letcall:' x := f args 'in' e" :=
   (call: f args → "_k" cont: "_k" [ x ] := e)%E
   (at level 102, x, f, args at level 1, e at level 150) : expr_scope.
 
-Notation "e1 <-{ i } '☇'" := (e1 <- #i)%E
-  (only parsing, at level 80) : expr_scope.
-Notation "e1 <-{ i } e2" := (e1 <-{i} ☇ ;; e1+ₗ#1 <- e2)%E
-  (at level 80) : expr_scope.
+(* RJ: These notations unfortunately do not print.  Also, I don't think
+   we would even want them to print in general.
+   TODO: Introduce a Definition. *)
+Notation "e1 '<-{Σ' i } '()'" := (e1 <- #i)%E
+  (only parsing, at level 80, format "e1  <-{Σ  i }  ()" ) : expr_scope.
+Notation "e1 '<-{Σ' i } e2" := (e1 <-{Σ i} () ;; e1+ₗ#1 <- e2)%E
+  (at level 80, format "e1 <-{Σ  i }  e2") : expr_scope.

theories/typing/own.v

@@ -274,15 +274,15 @@ Section typing.
     tctx_extract_hasty E L p ty1 T T' →
     (∀ (v : val),
         typed_body E L C ((v ◁ own_ptr (ty.(ty_size)) ty)::(p ◁ ty2)::T') (subst x v e)) →
-    typed_body E L C T (letalloc: x <⋯ !{ty.(ty_size)}p in e).
+    typed_body E L C T (letalloc: x <-{ty.(ty_size)} !p in e).
   Proof.
     intros. eapply type_new.
     - rewrite /Closed /=. rewrite !andb_True.
       eauto 100 using is_closed_weaken with set_solver.
     - lia.
     - move=>xv /=.
-      assert (subst x xv (x <⋯ !{ty.(ty_size)}p ;; e)%E =
-              (xv <⋯ !{ty.(ty_size)}p ;; subst x xv e)%E) as ->.
+      assert (subst x xv (x <-{ty.(ty_size)} !p ;; e)%E =
+              (xv <-{ty.(ty_size)} !p ;; subst x xv e)%E) as ->.
       { (* TODO : simpl_subst should be able to do this. *)
         unfold subst=>/=. repeat f_equal.
         - eapply (is_closed_subst []). done. set_solver.
@@ -306,4 +306,4 @@ Hint Resolve own_mono' own_proper' : lrust_typing.
 
 Hint Extern 100 (_ ≤ _) => simpl; lia : lrust_typing.
 Hint Extern 100 (@eq Z _ _) => simpl; lia : lrust_typing.
-Hint Extern 100 (@eq nat _ _) => simpl; lia : lrust_typing.
+Hint Extern 100 (@eq nat _ _) => simpl; lia : lrust_typing.
\ No newline at end of file

theories/typing/programs.v

@@ -234,7 +234,7 @@ Section typing_rules.
     typed_write E L ty1 ty ty1' -∗ typed_read E L ty2 ty ty2' -∗
     {{{ heap_ctx ∗ lft_ctx ∗ na_own tid ⊤ ∗ elctx_interp E qE ∗ llctx_interp L qL ∗
         tctx_elt_interp tid (p1 ◁ ty1) ∗ tctx_elt_interp tid (p2 ◁ ty2) }}}
-      (p1 <⋯ !{n}p2)
+      (p1 <-{n} !p2)
     {{{ RET #(); na_own tid ⊤ ∗ elctx_interp E qE ∗ llctx_interp L qL ∗
                  tctx_elt_interp tid (p1 ◁ ty1') ∗ tctx_elt_interp tid (p2 ◁ ty2') }}}.
   Proof.
@@ -257,7 +257,7 @@ Section typing_rules.
   Lemma type_memcpy_instr {E L} ty ty1 ty1' ty2 ty2' (n : Z) p1 p2 :
     Z.of_nat (ty.(ty_size)) = n →
     typed_write E L ty1 ty ty1' → typed_read E L ty2 ty ty2' →
-    typed_instruction E L [p1 ◁ ty1; p2 ◁ ty2] (p1 <⋯ !{n}p2)
+    typed_instruction E L [p1 ◁ ty1; p2 ◁ ty2] (p1 <-{n} !p2)
                       (λ _, [p1 ◁ ty1'; p2 ◁ ty2']%TC).
   Proof.
     iIntros (Hsz Hwrt Hread) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL HT".
@@ -276,7 +276,7 @@ Section typing_rules.
     typed_read E L ty2 ty ty2' →
     Z.of_nat (ty.(ty_size)) = n →
     typed_body E L C ((p1 ◁ ty1') :: (p2 ◁ ty2') :: T') e →
-    typed_body E L C T (p1 <⋯ !{n}p2;; e).
+    typed_body E L C T (p1 <-{n} !p2;; e).
   Proof.
     intros. by eapply type_seq; [|by eapply (type_memcpy_instr ty ty1 ty1')|..].
   Qed.

theories/typing/tests/option_as_mut.v

@@ -7,8 +7,8 @@ Section option_as_mut.
   Definition option_as_mut : val :=
     funrec: <> ["o"] :=
       let: "o'" := !"o" in case: !"o'" of
-        [ let: "r" := new [ #2 ] in "r" <-{0} ☇;; "k" ["r"];
-          let: "r" := new [ #2 ] in "r" <-{1} "o'" +ₗ #1;; "k" ["r"] ]
+        [ let: "r" := new [ #2 ] in "r" <-{Σ 0} ();; "k" ["r"];
+          let: "r" := new [ #2 ] in "r" <-{Σ 1} "o'" +ₗ #1;; "k" ["r"] ]
       cont: "k" ["r"] :=
         delete [ #1; "o"];; "return" ["r"].
 

theories/typing/tests/unwrap_or.v

@@ -8,7 +8,7 @@ Section unwrap_or.
     funrec: <> ["o"; "def"] :=
       case: !"o" of
       [ delete [ #(S τ.(ty_size)); "o"];; "return" ["def"];
-        letalloc: "r" <⋯ !{τ.(ty_size)}("o" +ₗ #1) in
+        letalloc: "r" <-{τ.(ty_size)} !("o" +ₗ #1) in
         delete [ #(S τ.(ty_size)); "o"];; delete [ #τ.(ty_size); "def"];; "return" ["r"]].
 
   Lemma unwrap_or_type τ :

theories/typing/type_sum.v

@@ -154,7 +154,7 @@ Section case.
   Lemma type_sum_assign_instr {E L} (i : nat) ty1 tyl ty ty2 p1 p2 :
     typed_write E L ty1 (sum tyl) ty2 →
     tyl !! i = Some ty →
-    typed_instruction E L [p1 ◁ ty1; p2 ◁ ty] (p1 <-{i} p2) (λ _, [p1 ◁ ty2]%TC).
+    typed_instruction E L [p1 ◁ ty1; p2 ◁ ty] (p1 <-{Σ i} p2) (λ _, [p1 ◁ ty2]%TC).
   Proof.
     iIntros (Hw Hty) "!# * #HEAP #LFT $ HE HL Hp".
     rewrite tctx_interp_cons tctx_interp_singleton.
@@ -185,7 +185,7 @@ Section case.
     typed_write E L ty1 (sum tyl) ty1' →
     tyl !! (Z.to_nat i) = Some ty →
     typed_body E L C ((p1 ◁ ty1') :: T') e →
-    typed_body E L C T (p1 <-{i} p2 ;; e).
+    typed_body E L C T (p1 <-{Σ i} p2 ;; e).
   Proof.
     intros. rewrite -(Z2Nat.id i) //.
     eapply type_seq; [done|by eapply type_sum_assign_instr|done|done].
@@ -194,7 +194,7 @@ Section case.
   Lemma type_sum_assign_unit_instr {E L} (i : nat) tyl ty1 ty2 p :
     tyl !! i = Some unit →
     typed_write E L ty1 (sum tyl) ty2 →
-    typed_instruction E L [p ◁ ty1] (p <-{i} ☇) (λ _, [p ◁ ty2]%TC).
+    typed_instruction E L [p ◁ ty1] (p <-{Σ i} ()) (λ _, [p ◁ ty2]%TC).
   Proof.
     iIntros (Hty Hw) "!# * #HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
     wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v Hv) "Hty".
@@ -213,7 +213,7 @@ Section case.
     typed_write E L ty1 (sum tyl) ty1' →
     tyl !! (Z.to_nat i) = Some unit →
     typed_body E L C ((p ◁ ty1') :: T') e →
-    typed_body E L C T (p <-{i} ☇ ;; e).
+    typed_body E L C T (p <-{Σ i} () ;; e).
   Proof.
     intros. rewrite -(Z2Nat.id i) //.
     eapply type_seq; [done|by eapply type_sum_assign_unit_instr|solve_typing|done].
@@ -224,7 +224,7 @@ Section case.
     typed_write E L ty1 (sum tyl) ty1' →
     typed_read E L ty2 ty ty2' →
     typed_instruction E L [p1 ◁ ty1; p2 ◁ ty2]
-               (p1 <⋯{i} !{ty.(ty_size)}p2) (λ _, [p1 ◁ ty1'; p2 ◁ ty2']%TC).
+               (p1 <-{ty.(ty_size),Σ i} !p2) (λ _, [p1 ◁ ty1'; p2 ◁ ty2']%TC).
   Proof.
     iIntros (Hty Hw Hr) "!# * #HEAP #LFT Htl [HE1 HE2] [HL1 HL2] Hp".
     rewrite tctx_interp_cons tctx_interp_singleton.
@@ -266,7 +266,7 @@ Section case.
     Z.of_nat (ty.(ty_size)) = n →
     tyl !! (Z.to_nat i) = Some ty →
     typed_body E L C ((p1 ◁ ty1') :: (p2 ◁ ty2') :: T') e →
-    typed_body E L C T (p1 <⋯{i} !{n}p2 ;; e).
+    typed_body E L C T (p1 <-{n,Σ i} !p2 ;; e).
   Proof.
     intros ???? Hr ???. subst. rewrite -(Z2Nat.id i) //.
     by eapply type_seq; [done|eapply type_sum_memcpy_instr, Hr|done|done].

theories/typing/unsafe/cell.v

@@ -81,7 +81,7 @@ Section typing.
   Definition cell_write ty : val :=
     funrec: <> ["c"; "x"] :=
        let: "c'" := !"c" in
-       "c'" <⋯ !{ty.(ty_size)} "x";;
+       "c'" <-{ty.(ty_size)} !"x";;
        let: "r" := new [ #0 ] in
        delete [ #1; "c"] ;; delete [ #ty.(ty_size); "x"] ;; "return" ["r"].