From 1c6f993cf0066a66e99793631a955d96d4080507 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 27 Oct 2016 10:52:43 +0200
Subject: [PATCH] Fix notation for dereferencing.
---
memcpy.v | 14 +++++++-------
notation.v | 4 ++--
type.v | 2 +-
type_incl.v | 10 +++++-----
typing.v | 10 +++++-----
5 files changed, 20 insertions(+), 20 deletions(-)
diff --git a/memcpy.v b/memcpy.v
index 3fd2aeaf..253a17fc 100644
--- a/memcpy.v
+++ b/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.
diff --git a/notation.v b/notation.v
index 07c1bb63..f60e5d3c 100644
--- a/notation.v
+++ b/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.
diff --git a/type.v b/type.v
index 3f0fc938..cd6913e3 100644
--- a/type.v
+++ b/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)
diff --git a/type_incl.v b/type_incl.v
index dd531378..b6999e2d 100644
--- a/type_incl.v
+++ b/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ρ".
diff --git a/typing.v b/typing.v
index 1f92fd54..6c277c9c 100644
--- a/typing.v
+++ b/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. *)
--
GitLab