Fix notation for dereferencing.

memcpy.v

@@ -4,23 +4,23 @@ From lrust Require Import heap proofmode.
 Definition memcpy : val :=
   rec: "memcpy" ["dst";"len";"src"] :=
     if: "len" ≤ #0 then #()
-    else "dst" <- * "src";;
+    else "dst" <- !"src";;
          "memcpy" ["dst" +ₗ #1 ; "len" - #1 ; "src" +ₗ #1].
 Opaque memcpy.
 
-Notation "e1 <-{ n } * e2" := (App memcpy [e1%E ; Lit (LitInt n) ; e2%E])
-  (at level 80, n at next level, format "e1  <-{ n }  * e2") : expr_scope.
+Notation "e1 <-{ n } ! e2" := (App memcpy [e1%E ; Lit (LitInt n) ; e2%E])
+  (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 <-[ i ]{ n } ! e2" :=
+  (e1 <-[i] ☇ ;; e1+ₗ#1 <-{n} !e2)%E
   (at level 80, n, i at next level,
-   format "e1  <-[ i ]{ n }  * e2") : lrust_expr_scope.
+   format "e1  <-[ i ]{ n }  ! e2") : lrust_expr_scope.
 
 Lemma wp_memcpy `{heapG Σ} E l1 l2 vl1 vl2 q n Φ:
   nclose heapN ⊆ E →
   length vl1 = n → length vl2 = n →
   heap_ctx ★ l1 ↦★ vl1 ★ l2 ↦★{q} vl2 ★
-  ▷ (l1 ↦★ vl2 ★ l2 ↦★{q} vl2 ={E}=★ Φ #()) ⊢ WP #l1 <-{n} *#l2 @ E {{ Φ }}.
+  ▷ (l1 ↦★ vl2 ★ l2 ↦★{q} vl2 ={E}=★ Φ #()) ⊢ WP #l1 <-{n} !#l2 @ E {{ Φ }}.
 Proof.
   iIntros (? Hvl1 Hvl2) "(#Hinv&Hl1&Hl2&HΦ)".
   iLöb as "IH" forall (n l1 l2 vl1 vl2 Hvl1 Hvl2). wp_rec. wp_op=> ?; wp_if.

notation.v

@@ -24,9 +24,9 @@ Notation "'case:' e0 'of' [ e1 , .. , en ]" :=
 Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E)
   (at level 200, e1, e2, e3 at level 200) : expr_scope.
 Notation "()" := LitUnit : val_scope.
-Notation "* e" := (Read Na1Ord e%E)
+Notation "! e" := (Read Na1Ord e%E)
   (at level 9, right associativity) : expr_scope.
-Notation "*ˢᶜ e" := (Read ScOrd e%E)
+Notation "!ˢᶜ e" := (Read ScOrd e%E)
   (at level 9, right associativity) : expr_scope.
 Notation "e1 + e2" := (BinOp PlusOp e1%E e2%E)
   (at level 50, left associativity) : expr_scope.

type.v

@@ -526,7 +526,7 @@ Hint Extern 1 (Types.LstTySize _ (_ :: _)) =>
 
 Import Types.
 
-Notation "!" := emp : lrust_type_scope.
+Notation "∅" := emp : lrust_type_scope.
 Notation "&uniq{ κ } ty" := (uniq_borrow κ ty)
   (format "&uniq{ κ } ty", at level 20, right associativity) : lrust_type_scope.
 Notation "&shr{ κ } ty" := (shared_borrow κ ty)

type_incl.v

@@ -44,7 +44,7 @@ Section ty_incl.
     eauto using ty_incl_weaken, ty_incl_trans, perm_incl_duplicable.
   Qed.
 
-  Lemma ty_incl_emp ρ ty : ty_incl ρ ! ty.
+  Lemma ty_incl_emp ρ ty : ty_incl ρ ∅ ty.
   Proof. iIntros (tid) "_!>". iSplit; iIntros "!#*/=[]". Qed.
 
   Lemma ty_incl_own ρ ty1 ty2 q :
@@ -148,8 +148,8 @@ Section ty_incl.
   Proof.
     iIntros (DUP FA tid) "#Hρ". rewrite /sum /=. iSplitR "".
     - assert (Hincl : ρ tid ={⊤}=★
-         (□ ∀ i vl, (nth i tyl1 !%T).(ty_own) tid vl
-                  → (nth i tyl2 !%T).(ty_own) tid vl)).
+         (□ ∀ i vl, (nth i tyl1 ∅%T).(ty_own) tid vl
+                  → (nth i tyl2 ∅%T).(ty_own) tid vl)).
       { clear -FA DUP. induction FA as [|ty1 ty2 tyl1 tyl2 Hincl _ IH].
         - iIntros "_!>*!#". eauto.
         - iIntros "#Hρ".  iMod (IH with "Hρ") as "#IH". iMod (Hincl with "Hρ") as "[#Hh _]".
@@ -158,8 +158,8 @@ Section ty_incl.
       iDestruct "H" as (i vl') "[% Hown]". subst. iExists _, _. iSplit. done.
         by iApply "Hincl".
     - assert (Hincl : ρ tid ={⊤}=★
-         (□ ∀ i κ E l, (nth i tyl1 !%T).(ty_shr) κ tid E l
-                     → (nth i tyl2 !%T).(ty_shr) κ tid E l)).
+         (□ ∀ i κ E l, (nth i tyl1 ∅%T).(ty_shr) κ tid E l
+                     → (nth i tyl2 ∅%T).(ty_shr) κ tid E l)).
       { clear -FA DUP. induction FA as [|ty1 ty2 tyl1 tyl2 Hincl _ IH].
         - iIntros "_!>*!#". eauto.
         - iIntros "#Hρ".

typing.v

@@ -244,7 +244,7 @@ Section typing.
 
   Lemma typed_step_deref ty ρ1 ρ2 e:
     ty.(ty_size) = 1%nat → consumes ty ρ1 ρ2 →
-    typed_step (ρ1 (Valuable.of_expr e)) ( *e) (λ v, v ◁ ty ★ ρ2 (Valuable.of_expr e))%P.
+    typed_step (ρ1 (Valuable.of_expr e)) (!e) (λ v, v ◁ ty ★ ρ2 (Valuable.of_expr e))%P.
   Proof.
     (* FIXME : I need to use [fupd_mask_mono], but I do not expect so. *)
     iIntros (Hsz Hconsumes tid) "#HEAP!#H". iApply fupd_wp. iApply fupd_mask_mono.
@@ -258,7 +258,7 @@ Section typing.
 
   Lemma typed_step_deref_uniq_borrow_own ty e κ κ' q q':
     typed_step (Valuable.of_expr e ◁ &uniq{κ} own q' ty ★ κ' ⊑ κ ★ [κ']{q})
-               ( *e)
+               (!e)
                (λ v, v ◁ &uniq{κ} ty ★ κ' ⊑ κ ★ [κ']{q})%P.
   Proof.
     iIntros (tid) "#HEAP !# [(H◁ & #H⊑ & Htok & #Hκ') Htl]".
@@ -280,7 +280,7 @@ Section typing.
 
   Lemma typed_step_deref_shr_borrow_own ty e κ κ' q q':
     typed_step (Valuable.of_expr e ◁ &shr{κ} own q' ty ★ κ' ⊑ κ ★ [κ']{q})
-               ( *e)
+               (!e)
                (λ v, v ◁ &shr{κ} ty ★ κ' ⊑ κ ★ [κ']{q})%P.
   Proof.
     iIntros (tid) "#HEAP !# [(H◁ & #H⊑ & Htok & #Hκ') Htl]".
@@ -314,7 +314,7 @@ Section typing.
 
   Lemma typed_step_deref_uniq_borrow_borrow ty e κ κ' κ'' q:
     typed_step (Valuable.of_expr e ◁ &uniq{κ'} &uniq{κ''} ty ★ κ ⊑ κ' ★ [κ]{q} ★ κ' ⊑ κ'')
-               ( *e)
+               (!e)
                (λ v, v ◁ &uniq{κ'} ty ★ κ ⊑ κ' ★ [κ]{q})%P.
   Proof.
     iIntros (tid) "#HEAP !# [(H◁ & #H⊑1 & [Htok #Hκ'] & #H⊑2) Htl]".
@@ -338,7 +338,7 @@ Section typing.
 
   Lemma typed_step_deref_shr_borrow_borrow ty e κ κ' κ'' q:
     typed_step (Valuable.of_expr e ◁ &shr{κ'} &uniq{κ''} ty ★ κ ⊑ κ' ★ [κ]{q} ★ κ' ⊑ κ'')
-               ( *e)
+               (!e)
                (λ v, v ◁ &shr{κ'} ty ★ κ ⊑ κ' ★ [κ]{q})%P.
   Proof.
     (* TODO : fix the definition of sharing unique borrows before. *)