From 56139a0d2a26008b6ced17747fb5ba9de2307d8d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 13 Jan 2017 17:28:58 +0100
Subject: [PATCH] change notation for memcpy. notation for sum injection has a
\Sigma.
---
theories/lang/memcpy.v | 12 ++++++------
theories/lang/new_delete.v | 4 ++--
theories/lang/notation.v | 11 +++++++----
theories/typing/own.v | 8 ++++----
theories/typing/programs.v | 6 +++---
theories/typing/tests/option_as_mut.v | 4 ++--
theories/typing/tests/unwrap_or.v | 2 +-
theories/typing/type_sum.v | 12 ++++++------
theories/typing/unsafe/cell.v | 2 +-
9 files changed, 32 insertions(+), 29 deletions(-)
diff --git a/theories/lang/memcpy.v b/theories/lang/memcpy.v
index f11083b0..455f9bb0 100644
--- a/theories/lang/memcpy.v
+++ b/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Φ".
diff --git a/theories/lang/new_delete.v b/theories/lang/new_delete.v
index d8f68562..d6a43c54 100644
--- a/theories/lang/new_delete.v
+++ b/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.
diff --git a/theories/lang/notation.v b/theories/lang/notation.v
index dcd053b6..982ee436 100644
--- a/theories/lang/notation.v
+++ b/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.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 7bb2b40c..914a1ba9 100644
--- a/theories/typing/own.v
+++ b/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.
\ No newline at end of file
+Hint Extern 100 (@eq nat _ _) => simpl; lia : lrust_typing.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index ebff0b3d..c35802f3 100644
--- a/theories/typing/programs.v
+++ b/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.
diff --git a/theories/typing/tests/option_as_mut.v b/theories/typing/tests/option_as_mut.v
index 114f89f1..93fac953 100644
--- a/theories/typing/tests/option_as_mut.v
+++ b/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"].
diff --git a/theories/typing/tests/unwrap_or.v b/theories/typing/tests/unwrap_or.v
index 72a29785..fabb11e0 100644
--- a/theories/typing/tests/unwrap_or.v
+++ b/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 Ï„ :
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index e1017869..7fe48853 100644
--- a/theories/typing/type_sum.v
+++ b/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].
diff --git a/theories/typing/unsafe/cell.v b/theories/typing/unsafe/cell.v
index 5114941c..f752401f 100644
--- a/theories/typing/unsafe/cell.v
+++ b/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"].
--
GitLab